ehtM87ShadowFractionalSigma_pos
plain-language theorem explainer
The EHT M87* shadow-size fractional sensitivity scale equals 0.17 and is strictly positive. Anyone assembling the M87* strong-field likelihood certificate needs this positivity hypothesis discharged. The proof unfolds the constant definition and closes by numerical normalization.
Claim. The conservative fractional shadow-size sensitivity for EHT M87* observations, fixed at the $17\%$ Kerr-consistency scale, satisfies $0 < 0.17$.
background
This module attaches a dataset-specific likelihood-style certificate to the §7 strong-field falsifier row, using the first EHT image of M87*: 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, represented by $\varphi^{-44}$. The certificate is a consistency / non-sensitivity test: it shows the RS target lies inside current EHT sensitivity scales, and that EHT is not presently sensitive to that target.
The shadow fractional sigma is defined as the constant $0.17$, the conservative fractional shadow-size sensitivity taken from the Kerr-consistency scale. Positivity of that constant is a trivial but required field of the certificate structure.
proof idea
One-line tactic proof: unfold the definition ehtM87ShadowFractionalSigma (which is the literal real $0.17$), then norm_num discharges $0 < 0.17$. No lemmas beyond the definition itself.
why it matters
Feeds the shadow_sigma_pos field of ehtM87StrongFieldLikelihoodCert, the third dataset-specific strong-field likelihood certificate in the verification layer. Without this positivity fact the certificate structure cannot be inhabited. The parent certificate packages residual-vs-sigma inequalities for both shadow size and circularity against the RS target scale $\varphi^{-44}$, establishing that EHT M87* is consistent with, but not sensitive to, the RS strong-field prediction. Closes a structural (zero-sorry) attachment rather than an empirical claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.