strongFieldAttachment
plain-language theorem explainer
Named dataset attachment for the strong-field / precision-GR falsifier row: Cassini Shapiro delay, GRAVITY S2 precession, and EHT M87* shadow. It records fractional metric-deviation sensitivity 2.3e-5 against an RS target 6.376e-10, with currentlySensitive = false. Likelihood and certificate modules cite it as the canonical numerical source. The body is a plain structure literal.
Claim. The strong-field falsifier-register attachment is the dataset record with sector "Strong-field / precision-GR tests", channels Cassini Shapiro delay, GRAVITY S2 precession, and EHT M87* shadow, units fractional metric-deviation scale, sensitivity $2.3\times 10^{-5}$, RS target scale $6.376\times 10^{-10}$, and current-sensitivity flag false.
background
The module attaches concrete named datasets and numerical sensitivity records to every row of the quantum-gravity master-plan §7 falsifier register. Status is structural: zero sorry, zero RS-internal axioms. A row is attached when it has a named observational channel, a numerical sensitivity, an RS target scale or band, and an honest flag for whether current data already reach that target. Purpose is falsifiability accounting, not empirical confirmation.
DatasetAttachment is the common record type: sector, dataset string, units, sensitivity, rsTargetScale, and currentlySensitive. Sensitivity and target are dimensionless unless units say otherwise. For several future rows currentlySensitive is honestly false: the channel is named but not yet sensitive to the φ-suppressed target.
Anchor numbers in the module doc include Cassini Shapiro delay γ−1 = (2.1±2.3)×10⁻⁵, GRAVITY S2 Schwarzschild-precession factor f_SP = 1.10±0.19, and EHT M87* ring diameter 42±3 μas with shadow-size Kerr consistency at roughly 17%. This row stores Cassini’s PPN-γ precision as the most precise current solar-system strong/weak-field number while the dataset string lists the full strong-field channel set.
proof idea
Definitional structure literal, not a proved theorem. The six fields of DatasetAttachment are filled by constants: sector and dataset strings, units string, sensitivity 2.3e-5, rsTargetScale 6.376e-10, currentlySensitive false. No lemmas or tactics; downstream positivity and comparison theorems unfold this literal and discharge inequalities by norm_num.
why it matters
This is the canonical numerical source for the strong-field §7 falsifier row. Downstream Cassini likelihood code reads rsTargetScale as cassiniRSTargetScale, proves the residual of the Cassini central value is within 1σ of that target, and proves the one-sigma uncertainty still exceeds the target (hence not currently sensitive). The attachment-status theorem packages positive sensitivity, positive target scale, and currentlySensitive = false. The same record feeds CassiniStrongFieldLikelihoodCert and the one-statement likelihood theorem, and is reused by EHT M87* strong-field residual comparisons.
In the broader RS verification stack this is falsifiability bookkeeping against precision-GR channels, not a claim that Cassini or EHT has confirmed RS. The φ-suppressed target sits far below present solar-system and shadow precision, matching the honest false flag. It sits beside sibling attachments (QNM, PTA, page curve, Ω_Λ, dark-energy w, echoes) that together close the register’s dataset layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.