IndisputableMonolith.Verification.CassiniStrongFieldLikelihood
Module packaging the Cassini radio-science constraint on the PPN parameter deviation γ−1 as a falsifier likelihood row. It records the measured central value and uncertainty, the Recognition Science target scale, and the residual, then certifies that the residual sits inside one sigma and that the observational sigma exceeds the RS target. Downstream falsifier-register aggregation imports this certificate. The argument is pure numerical comparison lemmas plus an inhabited certificate structure.
claimLet $\gamma_{\mathrm{Cass}}-1$ be the Cassini central measurement of the PPN deviation with uncertainty $\sigma_{\mathrm{Cass}}>0$, and let $s_{\mathrm{RS}}>0$ be the Recognition Science strong-field target scale. Define the residual $R=|(\gamma_{\mathrm{Cass}}-1)-s_{\mathrm{RS}}|$. The module asserts $R<\sigma_{\mathrm{Cass}}$, $\sigma_{\mathrm{Cass}}>s_{\mathrm{RS}}$, and packages these facts as an inhabited Cassini strong-field likelihood certificate for the quantum-gravity falsifier register.
background
Track 6.C of the quantum-gravity master plan treats strong-field and high-precision solar-system tests as structural discriminators between Recognition Science gravity and pure GR. The upstream module StrongFieldStructural closes the structural form of that track (zero sorry, zero RS-internal axiom). Cassini’s Shapiro-delay radio link remains the tightest empirical bound on the PPN parameter $\gamma$, conventionally reported as a measurement of $\gamma-1$ near zero.
This verification module attaches that named dataset to the falsifier register. It introduces the Cassini central value for $\gamma-1$, its one-sigma width, and an RS-native target scale against which the residual is scored. Sibling positivity lemmas record that both the observational sigma and the RS target are strictly positive, so residual comparisons are well-defined.
The companion import FalsifierRegisterDatasets supplies the generic dataset-attachment pattern used across §7 of the master plan; this file is the Cassini-specific instance for the strong-field likelihood layer.
proof idea
Definition layer first: named constants for the Cassini central $\gamma-1$, its sigma, the RS target scale, and the absolute residual. Two short positivity lemmas discharge $\sigma>0$ and $s_{\mathrm{RS}}>0$. Two comparison lemmas then prove residual $<$ one sigma and sigma $>$ RS target by direct numerical inequality on the recorded floats. A status flag records dataset attachment. The certificate structure bundles these facts; an inhabitation proof assembles the bundle from the comparison lemmas. No analytic derivation of $\gamma$ itself appears; the module only certifies the likelihood row against fixed published numbers.
why it matters in Recognition Science
Feeds FalsifierLikelihoodRegister, which aggregates Sessions 107–115 into the dataset-specific likelihood and status layer over the quantum-gravity master plan §7 falsifier register. Without this row, the Cassini strong-field discriminator would remain a structural placeholder rather than a scored likelihood entry. In the broader RS program the certificate sits under Gravity Track 6.C: it checks whether the RS strong-field target for $\gamma-1$ is compatible with the best solar-system bound, a necessary consistency gate before claiming that RS gravity survives precision PPN tests. Closure status matches the upstream structural theorem (0 sorry, 0 RS-internal axiom).
scope and limits
- Does not derive γ−1 from RS first principles; only scores a fixed published Cassini number.
- Does not re-analyze raw Doppler or ranging data; trusts the reported central value and sigma.
- Does not claim a new experimental bound tighter than Cassini’s published result.
- Does not address other PPN parameters (β, α1, …) or non-solar-system strong-field probes.
- Does not prove dynamical equivalence of RS gravity to GR beyond the recorded residual test.
used by (1)
depends on (2)
declarations in this module (13)
-
def
cassiniGammaMinusOneCentral -
def
cassiniGammaSigma -
def
cassiniRSTargetScale -
def
cassiniStrongFieldResidual -
theorem
cassiniGammaSigma_pos -
theorem
cassiniRSTargetScale_pos -
theorem
cassini_residual_lt_one_sigma -
theorem
cassini_sigma_gt_rs_target -
theorem
cassini_dataset_attachment_status -
structure
CassiniStrongFieldLikelihoodCert -
def
cassiniStrongFieldLikelihoodCert -
theorem
cassiniStrongFieldLikelihoodCert_inhabited -
theorem
cassini_strong_field_likelihood_one_statement