gravityS2RSTargetScale_pos
plain-language theorem explainer
The RS structural target deviation scale for the GRAVITY S2 strong-field attachment is strictly positive. Builders of the S2 likelihood certificate need this side condition when packing positivity fields. The proof unfolds the attachment constant to its numeric rsTargetScale and closes by norm_num.
Claim. The Recognition Science structural target scale for the GRAVITY S2 attachment satisfies $0 < \sigma_{\mathrm{RS}}$, where $\sigma_{\mathrm{RS}}$ is the fractional metric-deviation scale stored on the strong-field dataset attachment (numerically $6.376\times 10^{-10}$).
background
This module attaches a likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement $f_{SP}=1.10\pm 0.19$ (Newtonian $0$, GR $1$). The RS structural target is a tiny positive deviation from GR, written $f_{SP}=1+\varphi^{-44}$, and the certificate only claims 1σ compatibility plus current non-sensitivity of the data to that scale.
The target scale itself is not recomputed here: it is read off the §7 strong-field dataset attachment, whose rsTargetScale field is the fixed real $6.376\times 10^{-10}$ (fractional metric-deviation units), alongside Cassini/EHT channel metadata. Sibling definitions expose the GRAVITY central value, its reported σ, the residual to the RS prediction, and the positivity lemmas needed to assemble the certificate record.
proof idea
One-line tactic proof. Unfold the local target-scale definition to the strong-field attachment field, then unfold that attachment record so the goal is the concrete inequality $0 < 6.376\times 10^{-10}$. norm_num discharges the numeric comparison. No lemmas beyond definitional unfolding.
why it matters
Feeds the target_pos field of the GRAVITY S2 strong-field likelihood certificate, which packages four proved facts: σ>0, target scale >0, residual inside 1σ of the RS structural target, and reported σ larger than the RS scale (non-sensitivity). Without this positivity side condition the certificate structure cannot be inhabited.
In the broader Verification layer this is part of upgrading the §7 strong-field falsifier row with a second dataset-specific consistency check. It is deliberately not empirical confirmation: the module status is a structural theorem (zero sorry, zero new RS axioms) showing honest compatibility and that present GRAVITY precision cannot resolve $\varphi^{-44}$. Landmark contact is only through the stored RS target scale on the strong-field attachment, not a fresh derivation of T0–T8 or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.