ehtM87CircularityResidual
plain-language theorem explainer
Defines the EHT M87* circularity-channel residual as the absolute gap between a Kerr-consistent central fractional deviation of zero and the RS strong-field target scale. Observers and auditors of the M87* likelihood certificate cite it when checking that the RS target sits inside the circularity error budget. The body is a one-line absolute-value of zero minus the shared RS target scale.
Claim. The circularity residual for the EHT M87* strong-field attachment is the real number $|0 - s|$, where $s$ is the RS structural target fractional deviation scale (the $\S7$ strong-field attachment scale, structurally $\varphi^{-44}$).
background
This module attaches a dataset-specific likelihood-style certificate to Event Horizon Telescope imaging 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. The RS structural claim is a tiny positive fractional deviation from pure GR/Kerr, represented by the shared strong-field attachment scale (structurally $\varphi^{-44}$).
The circularity residual measures how far that RS target sits from a Kerr-consistent central fractional deviation of zero. Upstream, ehtM87RSTargetScale is defined as strongFieldAttachment.rsTargetScale, documented as the "RS structural target fractional deviation scale, taken from the §7 strong-field attachment." The residual is the absolute difference between that scale and zero, parallel to the shadow residual on the same certificate.
The module is a consistency / non-sensitivity test: it does not claim empirical confirmation of the RS correction, only that the target lies inside present EHT circularity and shadow sensitivity bands and is far below them.
proof idea
Pure definition, not a proved theorem. The value is the absolute value $|0 - s|$ with $s$ the RS target scale from the strong-field attachment. No tactics, lemmas, or rewriting beyond naming that shared scale; downstream theorems unfold this def and discharge numeric comparisons with norm_num.
why it matters
Feeds the circularity half of the EHT M87* strong-field likelihood package. The theorem ehtM87_circularity_residual_lt_sigma states that this residual is strictly less than the circularity fractional sigma (the $\le 10%$ channel), proving "EHT circularity channel is compatible with the RS structural target." The same quantity appears in EHTM87StrongFieldLikelihoodCert (circularity residual bound and positivity side-conditions) and in the one-statement theorem eht_m87_strong_field_likelihood_one_statement, which conjoins shadow and circularity residual bounds, target-below-sigma facts, and currentlySensitive = false.
In the Recognition framework this is a verification attachment, not a forcing-chain step: it records that the $\S7$ strong-field scale is inside present EHT circularity sensitivity and that EHT is not yet sensitive to $\varphi^{-44}$. That keeps the falsifier register honest: consistency without overclaiming detection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.