ehtM87CircularityFractionalSigma_pos
plain-language theorem explainer
The EHT M87* circularity sensitivity scale (10% fractional deviation) is strictly positive. Anyone assembling the M87* strong-field likelihood certificate needs this positivity side-condition. The proof unfolds the constant definition and discharges the inequality by numeric normalization.
Claim. The conservative EHT M87* circularity fractional sensitivity equals $0.10$ and satisfies $0 < 0.10$.
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 at most 10%, and shadow-size consistency with Kerr at roughly the 17% level.
The circularity fractional sigma is the conservative sensitivity scale taken from that $\le 10%$ circularity-deviation bound. It is a plain real constant, not a fitted parameter. The RS structural target in the same module is a tiny positive fractional deviation from pure GR/Kerr, represented by $\varphi^{-44}$; the certificate only checks that this target sits inside the published sensitivity windows and is in fact far below them.
Positivity of each sigma and of the target is required so residual comparisons are well-formed inequalities on positive scales.
proof idea
One-line tactic proof: unfold the definition of the circularity fractional sigma (the constant $0.10$), then apply norm_num to obtain $0 < 0.10$. No lemmas beyond the definition are used.
why it matters
Feeds the circularity_sigma_pos field of the M87* strong-field likelihood certificate structure. That certificate packages five facts: positivity of shadow sigma, circularity sigma, and RS target scale, plus the two residual-less-than-sigma comparisons. Together they establish the honest non-sensitivity claim of the module: the RS structural target $\varphi^{-44}$ lies well below both the 17% shadow and 10% circularity EHT windows, so current data are consistent with the target but do not resolve it. This is a consistency / non-sensitivity test in the Verification domain, not empirical confirmation of Recognition Science. Zero sorry, zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.