ehtM87_circularity_residual_lt_sigma
plain-language theorem explainer
The EHT M87* circularity residual (absolute gap between a Kerr-central value of zero and the RS structural target scale) is strictly smaller than the 10% circularity sensitivity. Anyone citing the M87* strong-field likelihood certificate needs this inequality. The proof unfolds the residual, target, and sigma definitions and closes by numeric evaluation.
Claim. The circularity residual $|0 - s|$ is strictly less than the EHT M87* circularity fractional sensitivity $0.10$, where $s$ is the RS strong-field structural target scale (the $\varphi^{-44}$-scale fractional metric deviation stored on the strong-field dataset attachment).
background
This module attaches a dataset-specific likelihood-style certificate to Event Horizon Telescope M87* imaging: 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 by $\varphi^{-44}$ and stored as rsTargetScale on the strong-field falsifier attachment (numeric value $6.376 \times 10^{-10}$).
The circularity residual is defined as the absolute difference between a Kerr-consistent central fractional deviation of zero and that RS target scale. The circularity fractional sigma is the conservative 10% circularity-deviation sensitivity. The certificate is a consistency / non-sensitivity test: it shows the RS target lies inside present EHT circularity tolerance, not that EHT confirms the target.
proof idea
Term-mode numeric proof. Unfold the residual to $|0 - s|$, the target scale $s$ to the strong-field attachment's rsTargetScale, and the circularity sigma to $0.10$. After unfolding, the goal is the concrete real inequality $|0 - 6.376 \times 10^{-10}| < 0.10$, discharged by norm_num. No intermediate lemmas beyond the local definitions.
why it matters
Fills the circularity half of the two residual-vs-sigma inequalities required by the EHT M87* strong-field likelihood certificate structure, and appears as one conjunct in the one-statement attachment theorem. Together with the parallel shadow residual inequality, it upgrades the §7 strong-field falsifier row with an honest M87* channel: RS target inside current circularity sensitivity, yet far below the 10% scale so EHT is not currently sensitive to $\varphi^{-44}$. This is structural verification bookkeeping in the Recognition framework, not a mass or coupling derivation; it sits downstream of the strong-field attachment constants and feeds the closed (0-sorry) likelihood certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.