ehtM87RingDiameterCentralMicroas
plain-language theorem explainer
Fixes the EHT M87* ring-diameter central value at 42 microarcseconds, the published first-image mean. Verification and strong-field likelihood modules cite it as the observational anchor for residual and sigma comparisons against the RS structural target. It is a numeric constant definition, not a derived claim.
Claim. The central EHT M87* ring diameter is the real number $42.0$ microarcseconds.
background
The module attaches a dataset-specific likelihood-style certificate to the §7 strong-field falsifier row, using the Event Horizon Telescope first image of M87*. Published summary figures are ring diameter $42 \pm 3,\mu\mathrm{as}$, circularity deviation at most 10%, and shadow-size consistency with Kerr at roughly the 17% level.
Recognition Science supplies a structural strong-field target: a tiny positive fractional deviation from pure GR/Kerr, represented by $\varphi^{-44}$. The certificate checks that this scale sits inside current EHT sensitivity bands and, separately, that EHT is not yet sensitive to it. The present declaration is the fixed central diameter used when forming residuals and fractional sigmas against that target.
proof idea
Pure definition: the real constant is set to the literal $42.0$. No lemmas, tactics, or derivation.
why it matters
Anchors the EHT M87* strong-field consistency / non-sensitivity test. Sibling constants (one-sigma width, shadow and circularity fractional sigmas, RS target scale $\varphi^{-44}$) and residual inequalities build on this central value to prove two honest facts: the RS structural deviation lies within current EHT scales, and $\varphi^{-44}$ is far below both the ~17% shadow and ~10% circularity thresholds. That is a non-confirmation consistency check in the verification layer, not empirical support for the forcing chain (T0–T8) or the mass ladder. Module status is structural theorem with zero sorry and no new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.