ehtM87StrongFieldLikelihoodCert
plain-language theorem explainer
Packages the EHT M87* strong-field likelihood certificate: positive shadow and circularity fractional uncertainties, positive RS target scale φ⁻⁴⁴, residuals below those bars, and explicit non-sensitivity of both channels to φ⁻⁴⁴. Cited by anyone using the §7 strong-field falsifier row or the M87* dataset attachment. The body is a pure structure instance wiring eight already-proved numeric lemmas.
Claim. There is an EHT M87* strong-field likelihood certificate asserting: shadow and circularity fractional uncertainties are positive; the RS target scale $\varphi^{-44}$ is positive; both shadow and circularity residuals lie strictly below their uncertainties; $\varphi^{-44}$ is strictly smaller than both uncertainties (channels not currently sensitive); and the dataset attachment is present, positive, and marked not currently sensitive.
background
This module attaches a third dataset-specific likelihood-style certificate to the §7 strong-field falsifier row, using Event Horizon Telescope observations of M87*. The published first-image numbers are a ring diameter $42 \pm 3,\mu\mathrm{as}$, circularity deviation at most 10%, and shadow-size consistency with Kerr at roughly the 17% level.
The RS structural target is a tiny positive fractional deviation from pure GR/Kerr, represented here by $\varphi^{-44}$. Sibling constants encode the shadow and circularity fractional sigmas, the RS target scale, and the corresponding residuals (target versus channel). Upstream lemmas prove each sigma and the target are positive, each residual is strictly below its sigma, and the target lies strictly below both sigmas.
The certificate structure bundles those facts plus a dataset-attachment status lemma: positive sensitivity, positive target scale, and currentlySensitive = false. The module states this is a consistency / non-sensitivity test, not empirical confirmation.
proof idea
Pure structure construction. Each field of the certificate is filled by a named upstream lemma: positivity of the shadow fractional sigma, positivity of the circularity fractional sigma, positivity of the RS target scale, shadow residual below shadow sigma, circularity residual below circularity sigma, target below shadow sigma (shadow not currently sensitive), target below circularity sigma (circularity not currently sensitive), and the dataset-attachment status triple. Those lemmas themselves are short unfold + norm_num proofs on the concrete decimal encodings of the EHT bars and $\varphi^{-44}$.
why it matters
Closes the M87* strong-field likelihood attachment as a zero-sorry, zero-new-axiom certificate in the Verification domain. Downstream, the inhabited theorem simply wraps this value to obtain Nonempty of the certificate type, giving a one-statement handle for the attachment.
In the broader Recognition framework this is the honest strong-field counterpart of other falsifier-register dataset rows: it records that $\varphi^{-44}$ sits inside the published EHT error scales yet far below current sensitivity (17% shadow, 10% circularity). That matches the module claim of consistency without claiming detection. It does not touch the T0–T8 forcing chain or the mass ladder directly; it only anchors the strong-field observational gate for M87*.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.