ehtM87CircularityFractionalSigma
plain-language theorem explainer
Defines the EHT M87* circularity channel sensitivity as the fixed fractional scale 0.10 (10%). Anyone citing the M87* strong-field likelihood certificate uses this as the observational bound against which the RS residual and the φ^{-44} target are compared. The body is a bare real constant, not a derived quantity.
Claim. The EHT M87* circularity fractional sensitivity is the real number $0.10$, i.e. the conservative $\le 10\%$ circularity-deviation scale reported for the first Event Horizon Telescope image of M87*.
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.
Recognition Science predicts a tiny positive fractional deviation from pure GR/Kerr, represented structurally by $\varphi^{-44}$. The certificate is deliberately a consistency / non-sensitivity test: it checks that the RS target sits inside present EHT error bars, and that those bars are still far larger than the target.
Sibling constants fix the shadow fractional sigma, the RS target scale (via the strong-field attachment), and the two residuals. The circularity sigma is the observational yardstick for the circularity channel alone.
proof idea
No proof: a definitional abbreviation that pins the circularity fractional sensitivity to the literal real $0.10$. Downstream positivity and comparison lemmas simply unfold this name and discharge the resulting numerical goals with norm_num.
why it matters
Feeds the circularity half of the M87* strong-field likelihood package. Downstream, ehtM87CircularityFractionalSigma_pos records positivity; ehtM87_circularity_residual_lt_sigma shows the RS residual lies under this $10%$ bar (compatibility); ehtM87_circularity_sigma_gt_rs_target shows $\varphi^{-44}$ is strictly smaller than $0.10$ (current non-sensitivity). Both facts are packaged into EHTM87StrongFieldLikelihoodCert and the one-statement theorem eht_m87_strong_field_likelihood_one_statement.
In the broader RS verification stack this is an observational anchor, not a forcing-chain step: it does not touch T5–T8, the RCL, or the mass ladder. It only records that present EHT circularity precision cannot yet resolve the structural strong-field correction claimed by RS.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.