ehtM87ShadowResidual
plain-language theorem explainer
Defines the EHT M87* shadow-size residual as the absolute gap between a Kerr-consistent central fractional deviation of zero and the RS structural target scale. Verification and strong-field falsifier work cites it when checking that the RS target sits inside the EHT shadow error bar. The body is a one-line absolute-value definition.
Claim. The M87* shadow residual is the real number $|0 - s|$, where $s$ is the RS structural target fractional deviation scale (from the §7 strong-field attachment, structurally $\varphi^{-44}$) and $0$ is the Kerr-consistent central fractional deviation.
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 $\le 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, written structurally as $\varphi^{-44}$.
The sibling ehtM87RSTargetScale pulls that target from strongFieldAttachment.rsTargetScale. The residual measures distance from the present Kerr-centered point estimate (fractional deviation $0$) to that RS scale. The certificate is a consistency / non-sensitivity test: it shows the target lies inside current EHT scales and that EHT is not yet sensitive to $\varphi^{-44}$.
proof idea
Pure definition: unfold to the absolute value $|0 - \texttt{ehtM87RSTargetScale}|$. No lemmas or tactics. Downstream inequalities (ehtM87_shadow_residual_lt_sigma) unfold this def together with the target and the shadow fractional sigma, then close by norm_num.
why it matters
Feeds the shadow channel of the EHT M87* strong-field likelihood certificate. Parent uses: ehtM87_shadow_residual_lt_sigma (residual strictly below the shadow fractional sigma), the fields of EHTM87StrongFieldLikelihoodCert, and the bundled eht_m87_strong_field_likelihood_one_statement.
In the Recognition framework this is the §7 strong-field falsifier row for M87*, not a mass or coupling derivation. It records that the RS target scale is compatible with, and currently invisible to, EHT shadow-size sensitivity. Landmark contact is only the structural $\varphi$-power target; T0–T8 forcing is upstream of the attachment, not proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.