ehtM87RSTargetScale
plain-language theorem explainer
Aliases the RS strong-field structural target fractional deviation for the EHT M87* likelihood module. Anyone comparing Kerr-central residuals to the RS scale cites this constant. It is a one-line projection of the §7 strong-field attachment field `rsTargetScale`, fixed at the structural value φ⁻⁴⁴.
Claim. Define the RS structural target fractional deviation scale for the EHT M87* analysis by $$s_{\mathrm{RS}} := s_{\mathrm{sf}},$$ where $s_{\mathrm{sf}}$ is the strong-field attachment target scale (structurally $\varphi^{-44}$).
background
The module attaches a dataset-specific likelihood-style certificate to Event Horizon Telescope M87* first-image observables: ring diameter $42\pm 3,\mu\mathrm{as}$, circularity deviation at most $10%$, and shadow-size consistency with Kerr at roughly the $17%$ level. Status is structural theorem (zero sorry, no new RS-internal axioms): a consistency / non-sensitivity test, not empirical confirmation.
Recognition Science predicts a tiny positive fractional deviation from pure GR/Kerr in the strong-field regime. That scale is carried by the §7 strong-field attachment record and is represented structurally by $\varphi^{-44}$. The present definition simply names that attachment field for the M87* channel so residuals and sigma comparisons stay local and readable.
Sibling constants fix the observational widths (shadow fractional sigma $\approx 0.17$, circularity fractional sigma $\approx 0.10$). Residuals are absolute deviations of the Kerr-central value $0$ from this RS target.
proof idea
Definitional one-liner: unfold to the rsTargetScale field of the imported strong-field attachment record. No tactics, no lemmas, no arithmetic. Downstream positivity and comparison proofs unfold this alias together with the attachment and discharge the numerical inequalities by norm_num.
why it matters
Anchors every M87* residual and sensitivity statement in the module. Shadow and circularity residuals are $|0 - s_{\mathrm{RS}}|$; the theorems that residual is below observational sigma, and that sigma itself exceeds the RS target, all unfold through this name. The certificate bundle uses the same scale to record that EHT is presently compatible with the RS target yet not sensitive to $\varphi^{-44}$ (far below both $17%$ and $10%$).
In the broader Verification domain this is the third dataset-specific strong-field likelihood attachment, upgrading the §7 falsifier row without adding axioms. It ties the abstract strong-field structural prediction to a concrete EHT channel while keeping the honest non-sensitivity claim explicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.