ehtM87_dataset_attachment_status
plain-language theorem explainer
The strong-field falsifier row (Cassini / GRAVITY / EHT) has strictly positive sensitivity and RS target scale, and is flagged not currently sensitive. Verification authors cite it when assembling the EHT M87* likelihood certificate. The proof is a three-component term: two positivity lemmas plus reflexivity on the sensitivity flag.
Claim. For the strong-field dataset attachment (Cassini Shapiro delay, GRAVITY S2 precession, EHT M87* shadow), the recorded sensitivity is positive, the RS target scale is positive, and the attachment is marked currently sensitive as false.
background
The module attaches an EHT M87* likelihood-style certificate to the §7 strong-field falsifier row. EHT reports a ring diameter $42 \pm 3,\mu\mathrm{as}$, circularity deviation $\le 10%$, and shadow-size consistency with Kerr at roughly the $17%$ level. The RS structural target is a tiny fractional deviation from pure GR/Kerr, represented by $\varphi^{-44}$.
A DatasetAttachment stores sector, dataset string, units, numerical sensitivity, and RS target scale. HasPositiveSensitivity means $0 < D.\mathrm{sensitivity}$; HasPositiveTargetScale means $0 < D.\mathrm{rsTargetScale}$. The strong-field row records sensitivity $2.3\times 10^{-5}$ (Cassini-class fractional metric precision) and RS target scale $\approx 6.376\times 10^{-10}$.
Upstream lemmas already prove those two inequalities by unfolding the record and norm_num. The module stresses this is a consistency / non-sensitivity test, not empirical confirmation of RS.
proof idea
Term-mode introduction of a three-way conjunction. The first conjunct is strongField_sensitivity_pos (unfolds the attachment and checks $0 < 2.3\times 10^{-5}$ by norm_num). The second is strongField_target_pos (same pattern for the RS target scale). The third is rfl on the boolean field that marks the row not currently sensitive. No further rewriting or case analysis.
why it matters
Feeds the master certificate ehtM87StrongFieldLikelihoodCert in the same module, which packages shadow and circularity residual bounds against EHT sigmas together with positivity of the RS target. That cert upgrades the strong-field falsifier register with a dataset-specific likelihood-style row for M87*.
In the Recognition framework this is verification scaffolding around strong-field / precision-GR tests, not a step in the T0–T8 forcing chain. It records honestly that the RS target ($\varphi^{-44}$-scale fractional deviation) sits far below present EHT shadow and circularity sensitivity, so the row is present and positive yet marked non-sensitive. Closes a structural theorem with zero sorry and no new RS axioms (module status 2026-05-22).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.