ehtM87RSTargetScale_pos
plain-language theorem explainer
The RS structural target fractional-deviation scale on the EHT M87* strong-field attachment is strictly positive. Anyone assembling the M87 likelihood certificate needs this positivity field. The proof unfolds the scale to the numeric constant stored on the strong-field dataset row and closes with a numeric positivity check.
Claim. Let $s_{\mathrm{RS}}$ be the Recognition Science structural target fractional-deviation scale on the strong-field dataset attachment (the value used for the EHT M87* row). Then $0 < s_{\mathrm{RS}}$.
background
This module attaches a likelihood-style certificate to Event Horizon Telescope M87* data (ring diameter $42\pm 3,\mu\mathrm{as}$, circularity deviation $\le 10%$, 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 structurally by $\varphi^{-44}$ and stored numerically on the strong-field falsifier row.
The scale in question is defined by reading rsTargetScale off the strong-field dataset attachment, whose doc-comment records the sector as strong-field / precision-GR tests (Cassini Shapiro delay, GRAVITY S2 precession, EHT M87* shadow) with units "fractional metric-deviation scale" and rsTargetScale := 6.376e-10. Sibling positivity lemmas do the same for the shadow and circularity sensitivity sigmas.
The local claim is only that this stored target scale is positive, a prerequisite for residual comparisons that show the RS target lies well inside current EHT error bars (a non-sensitivity / consistency statement, not empirical confirmation).
proof idea
One-line tactic proof. Unfold the target-scale definition to the strong-field attachment field, then unfold that attachment record so the goal is $0 < 6.376\times 10^{-10}$. Discharge the numeric inequality with norm_num. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the M87 strong-field likelihood certificate as the target_pos field, alongside shadow/circularity sigma positivity and the two residual-less-than-sigma inequalities. That certificate is the third dataset-specific upgrade of the §7 strong-field falsifier row: it records that the RS structural target ($\varphi^{-44}$-scale fractional deviation) sits inside present EHT shadow and circularity sensitivity, while also proving EHT is not currently sensitive to that scale.
In the broader Recognition framework this is verification scaffolding, not a forcing-chain step (T0–T8). It pins an honest consistency bound between the RS strong-field prediction and published EHT M87* error bars, with zero sorry and no new RS-internal axioms. Downstream consumers of the certificate can quote positivity without re-proving the numeric fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.