gravityS2_dataset_attachment_status
plain-language theorem explainer
The strong-field falsifier-register attachment (Cassini/GRAVITY/EHT channel) has strictly positive experimental sensitivity and strictly positive RS target scale, and is flagged not currently sensitive. Verification authors cite it when assembling the GRAVITY S2 likelihood certificate. The proof is a three-component term pairing two positivity lemmas with reflexivity on the sensitivity flag.
Claim. The registered strong-field dataset attachment $D$ satisfies $0 < D$'s experimental sensitivity, $0 < D$'s RS target scale, and $D$ is marked not currently sensitive.
background
This module upgrades the strong-field falsifier row with a dataset-specific likelihood-style certificate for 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 $f_{SP}=1+\varphi^{-44}$. The certificate is a consistency and non-sensitivity test, not empirical confirmation.
Falsifier-register attachments carry a numerical sensitivity (experimental precision scale) and an RS target scale. Positive sensitivity means $0<$ sensitivity; positive target scale means $0<$ rsTargetScale. The strong-field attachment stores Cassini Shapiro-delay precision $2.3\times 10^{-5}$ as sensitivity and RS scale $\approx 6.4\times 10^{-10}$, with dataset string covering Cassini, GRAVITY S2, and EHT.
Upstream lemmas already prove both numerical fields positive for this attachment by unfolding the record and norm_num.
proof idea
One-line term proof: a triple constructor. First component is the existing positivity theorem for the strong-field attachment's sensitivity; second is the matching positivity theorem for its RS target scale; third is rfl, because the attachment record sets the currently-sensitive flag to false by definition.
why it matters
Supplies the dataset_status field of the master GRAVITY S2 strong-field likelihood certificate, alongside residual-within-1σ and non-sensitivity inequalities. That certificate packages two honest facts: GRAVITY's central value is statistically compatible with the RS structural target at 1σ, and GRAVITY is not currently sensitive to the RS scale ($\varphi^{-44}$ lies far below the reported $0.19$ one-sigma precision). Closes a verification bookkeeping obligation for the §7 strong-field falsifier row with zero sorry and no new RS-specific axioms. Framework role is register hygiene for strong-field / precision-GR tests, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.