gravityS2RSTargetScale
plain-language theorem explainer
Aliases the RS structural target deviation for GRAVITY S2 Schwarzschild precession as the §7 strong-field attachment scale, namely φ⁻⁴⁴. Anyone building the S2 predicted precession factor, residual, or likelihood certificate cites this constant. The body is a one-line projection of the shared attachment record.
Claim. Let the RS structural target deviation scale for the GRAVITY S2 precession factor be the strong-field attachment's target scale (structurally $\varphi^{-44}$). The RS predicted precession factor is then $1$ plus this scale.
background
This module attaches a likelihood-style certificate to the GRAVITY Collaboration (2020) S2 Schwarzschild-precession measurement. The reported factor is $f_{SP} = 1.10 \pm 0.19$, with $f_{SP}=0$ Newtonian and $f_{SP}=1$ pure GR.
Recognition Science predicts a tiny positive deviation from GR, written structurally as $f_{SP} = 1 + \varphi^{-44}$. The shared §7 strong-field attachment record stores that deviation as its target scale; this definition simply names that field for the S2 module.
The certificate is a consistency and non-sensitivity test: the central value must lie within $1\sigma$ of the RS target, and the reported $0.19$ uncertainty must exceed $\varphi^{-44}$. It is not claimed as empirical confirmation of the deviation.
proof idea
Definitional one-liner: project the rsTargetScale field of the shared strong-field attachment record. No tactics, no lemmas. Downstream positivity and comparison proofs unfold this alias together with the attachment and finish by norm_num.
why it matters
Gives a single named real for every S2 strong-field likelihood statement. Downstream, the predicted factor is $1$ plus this scale; the residual is the absolute gap from GRAVITY's central value; positivity of the scale, residual $<1\sigma$, and scale $<\sigma$ all unfold it.
Those facts pack into the S2 likelihood certificate and the one-statement attachment theorem (residual within $1\sigma$, target below reported precision, attachment marked not currently sensitive). In the RS forcing picture the scale is a high negative power of $\varphi$ (T6 fixed point), so present S2 data cannot resolve it; the definition locks that structural claim into the verification layer without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.