ehtM87RingDiameterSigmaMicroas
plain-language theorem explainer
Fixes the EHT M87* ring-diameter one-sigma uncertainty at 3 microarcseconds, matching the published 42 ± 3 μas first-image datum. Downstream strong-field likelihood and residual checks cite this as the absolute diameter error bar. It is a bare real constant, not a derived quantity.
Claim. The one-sigma uncertainty on the Event Horizon Telescope M87* ring diameter is $\sigma_d = 3\,\mu\mathrm{as}$.
background
The module attaches a dataset-specific likelihood-style certificate to the §7 strong-field falsifier row, using the EHT first image of M87*: 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 predicts only a tiny positive fractional deviation from pure GR/Kerr, structurally represented by $\varphi^{-44}$. The certificate is a consistency and non-sensitivity test: the RS target must lie inside current EHT sensitivity scales, and EHT must not yet resolve $\varphi^{-44}$.
This definition supplies the absolute diameter error bar that pairs with the central value $42,\mu\mathrm{as}$. Sibling constants encode the fractional shadow and circularity sigmas and the RS target scale.
proof idea
No proof. The declaration is a definitional abbreviation equal to the real literal $3.0$, taken directly from the published EHT M87* ring-diameter uncertainty.
why it matters
Anchors the absolute scale of the EHT M87* diameter error in the strong-field verification stack. Together with the central diameter and the fractional shadow/circularity sigmas, it lets residual inequalities show that the RS structural target $\varphi^{-44}$ sits well inside present EHT sensitivity and that EHT is not currently sensitive to that scale.
Module status is structural theorem: zero sorry, zero new RS-internal axioms. This is bookkeeping for an honest non-confirmation test, not empirical support for the forcing chain (T0–T8) or the mass ladder. No downstream consumers are wired yet in the graph; siblings such as the shadow and circularity residual bounds are the natural use sites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.