eht_m87_strong_field_likelihood_one_statement
plain-language theorem explainer
Single-statement packaging of the EHT M87* strong-field likelihood certificate: shadow and circularity residuals lie below their fractional sensitivities (17% and 10%), the RS target scale sits below both floors, the attachment is marked not currently sensitive, and the certificate type is inhabited. Verification authors cite it to close the M87* falsifier row as a consistency check. Proof is a pure term packing four numeric inequalities, reflexivity, and an inhabited instance.
Claim. The EHT M87* shadow residual is strictly less than the $17\%$ shadow fractional sensitivity, the circularity residual is strictly less than the $10\%$ circularity sensitivity, the RS structural target scale is strictly below both sensitivity scales, the strong-field attachment flag records that the dataset is not currently sensitive, and the EHT M87* strong-field likelihood certificate type is nonempty.
background
This module attaches Event Horizon Telescope M87* first-image data to the Recognition Science strong-field falsifier row. The observational anchors are a ring diameter of $42 \pm 3,\mu\mathrm{as}$, circularity deviation at most $10%$, and shadow-size consistency with Kerr at roughly the $17%$ level. Those percentages become the two fractional sensitivity scales used throughout the certificate.
The RS structural target is a tiny positive fractional deviation from pure GR/Kerr, taken from the section-7 strong-field attachment and represented by $\varphi^{-44}$. Residuals measure the absolute gap between a Kerr-consistent central deviation of zero and that RS target. The module status is structural theorem: zero sorry, zero new RS-internal axioms, closed 2026-05-22.
Upstream lemmas already discharge the four numeric comparisons by unfolding the residual, target, and sigma definitions and running norm_num. The certificate structure packages positivity of both sigmas and the target, the two residual inequalities, and the two non-sensitivity inequalities.
proof idea
Term-mode constructor packing. The six conjuncts are filled in order by: the shadow residual-less-than-sigma lemma, the circularity residual-less-than-sigma lemma, the shadow-sigma-greater-than-RS-target lemma, the circularity-sigma-greater-than-RS-target lemma, reflexivity on the currentlySensitive = false field of the strong-field attachment, and the inhabited instance of the certificate structure. No new arithmetic is performed here; all numeric work lives in the four upstream norm_num lemmas.
why it matters
Closes the third dataset-specific likelihood-style certificate on the section-7 strong-field falsifier row, after earlier attachments, now specialized to EHT M87*. The honest content is twofold: the RS target $\varphi^{-44}$ lies inside the published EHT shadow and circularity sensitivity envelopes, yet both envelopes are far larger than that target, so the dataset is explicitly marked not currently sensitive. This is a consistency and non-sensitivity test, not empirical confirmation of the RS deviation.
In the broader Recognition framework the result sits in the verification layer rather than the T0–T8 forcing chain: it does not derive $\varphi$, the eight-tick octave, or $D=3$, but it records that present strong-field imaging cannot yet resolve the structural RS correction scale. With no downstream dependents yet, the theorem functions as a terminal one-statement export for auditors and for any future multi-dataset conjunction over strong-field likelihood certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.