ehtM87_circularity_sigma_gt_rs_target
plain-language theorem explainer
The RS strong-field target fractional scale sits strictly below the EHT M87* circularity sensitivity band of 10%. Anyone citing the M87* non-sensitivity certificate needs this inequality. The proof is a pure numerical comparison after unfolding the two named constants.
Claim. The Recognition Science structural target fractional deviation (the strong-field attachment scale, $\varphi^{-44}$) is strictly smaller than the EHT M87* circularity fractional sensitivity $0.10$.
background
This module attaches a likelihood-style certificate to the Event Horizon Telescope first 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 RS structural prediction under test is a tiny positive fractional deviation from pure GR/Kerr, written as $\varphi^{-44}$ and packaged in the §7 strong-field attachment.
Two local constants appear. The circularity fractional sigma is the conservative 10% circularity-deviation scale. The RS target scale is exactly the attachment's rsTargetScale field (the $\varphi^{-44}$ structural deviation). The module's stated goal is a consistency / non-sensitivity test: show the RS target lies inside the reported sensitivity windows, yet far below them, so current EHT data cannot resolve it.
Upstream, the attachment itself records that the channel is marked not currently sensitive; positivity and residual comparisons for shadow and circularity are sibling facts in the same file.
proof idea
Term-mode proof by unfolding. Expand the RS target scale to the strong-field attachment's rsTargetScale, expand the circularity fractional sigma to the literal $0.10$, and expand the attachment record. A single norm_num then discharges the strict inequality on the concrete reals. No lemmas beyond definitional unfolding are required.
why it matters
This is one of the four numeric inequalities bundled into the one-statement EHT M87* likelihood theorem, which asserts residual-below-sigma for both shadow and circularity channels, target-below-sigma for both channels, and the explicit currentlySensitive = false flag. It is also a field of the structured certificate record used by downstream verification consumers.
In the Recognition framework this closes the circularity half of the §7 strong-field falsifier row for M87*: the structural target $\varphi^{-44}$ is honest and positive, yet EHT circularity (10%) cannot see it. That matches the module's design as a non-sensitivity certificate, not an empirical confirmation. Together with the parallel shadow-channel inequality it upgrades the strong-field verification surface without new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.