ehtM87ShadowFractionalSigma
plain-language theorem explainer
Conservative EHT M87* fractional shadow-size sensitivity is fixed at the real constant 0.17, the 17% Kerr-consistency scale from the first-image dataset. Verification authors cite it when placing the RS strong-field target against current shadow-size reach. The body is a literal constant assignment, not a derived computation.
Claim. The EHT M87* fractional shadow-size sensitivity is the constant $0.17$, adopted as a conservative Kerr-consistency scale for the first-image shadow-size channel.
background
The module attaches a dataset-specific likelihood-style certificate to the §7 strong-field falsifier row for Event Horizon Telescope observations of M87*. The published first-image summary used here is 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 is deliberately a consistency and non-sensitivity test: it checks that this target sits inside the reported EHT sensitivity scales, and that those scales are still far coarser than $\varphi^{-44}$.
This declaration is the shadow-size half of that sensitivity pair. Its sibling is the 10% circularity fractional scale. Downstream residual and comparison lemmas unfold both constants against the RS target scale.
proof idea
Definitional constant: the real value $0.17$ is assigned directly. No lemmas, tactics, or algebraic reduction. Downstream positivity and comparison theorems simply unfold this name and finish with norm_num.
why it matters
This constant is the shadow-size sensitivity input to the EHT M87* strong-field attachment. It is required by the positivity lemma, by the residual bound (RS residual strictly below the 17% scale), and by the non-sensitivity comparison (RS target $\varphi^{-44}$ strictly below 0.17).
Those facts are packaged in the certificate structure and the one-statement attachment theorem, which jointly record: positive sensitivities, residual inside both channels, target below both channels, and currentlySensitive = false. In framework terms this closes a verification row, not a forcing-chain step: it documents that present EHT M87* shadow-size reach cannot yet probe the RS strong-field rung, while remaining numerically compatible with it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.