Pith. sign in
module module high

IndisputableMonolith.Verification.CassiniStrongFieldLikelihood

show as:
view Lean formalization →

Module packaging the Cassini radio-science constraint on the PPN parameter deviation γ−1 as a strong-field falsifier likelihood. It records the measured central value and uncertainty, the RS target scale, the residual in sigma units, and positivity/one-sigma comparison lemmas, then wraps them in an inhabited likelihood certificate. Downstream falsifier-register aggregation imports this certificate as the Cassini row of Track 6.C.

claimCassini supplies a measured central value $(\gamma-1)_{\mathrm{obs}}$ with uncertainty $\sigma_\gamma$, an RS target scale $s_{\mathrm{RS}}>0$, and residual $r=|(\gamma-1)_{\mathrm{obs}}-s_{\mathrm{RS}}|/\sigma_\gamma$. The module asserts $\sigma_\gamma>0$, $s_{\mathrm{RS}}>0$, $r<1$, and $\sigma_\gamma>s_{\mathrm{RS}}$, and packages these into a strong-field likelihood certificate for the falsifier register.

background

Recognition Science's gravity track treats parameterized post-Newtonian (PPN) deviations as structural discriminators between GR and RS predictions in the strong-field regime. Track 6.C of the quantum-gravity master plan isolates strong-field tests; the upstream module StrongFieldStructural closes the structural form of that track (zero sorry, zero RS-internal axiom).

Cassini radio science famously bounds $\gamma-1$ near zero. This module attaches that named dataset: a central measurement for $\gamma-1$, its one-sigma width, and an RS-native target scale against which the residual is scored. The sibling falsifier-dataset module attaches concrete numerical sensitivity records to every row of the master-plan §7 register; here the Cassini row is specialized to the strong-field $\gamma$ channel.

Notation in the module is elementary: central value, sigma, RS target scale, residual in units of sigma, and a small certificate structure recording attachment status and the comparison lemmas.

proof idea

Definition-and-certificate module, not a deep derivation. Numeric constants fix the Cassini central $\gamma-1$, sigma, and RS target scale. Positivity of sigma and of the RS scale are immediate arithmetic facts. The residual is the absolute deviation of the central value from the RS scale, divided by sigma; two comparison lemmas discharge residual $<1\sigma$ and sigma greater than the RS target. A certificate structure bundles those facts with a dataset-attachment status flag; an inhabited instance supplies the concrete Cassini certificate for import by the likelihood register.

why it matters in Recognition Science

Closes the Cassini strong-field likelihood row that the falsifier likelihood register aggregates. Downstream FalsifierLikelihoodRegister is the Sessions 107--115 layer over master-plan §7: dataset-specific likelihood and status for every falsifier. Without this module the Cassini $\gamma-1$ channel would be a bare dataset attachment rather than a scored residual-plus-certificate.

In the broader RS gravity program this is the observational face of Track 6.C: structural strong-field discriminators become numerically checkable against a published spacecraft bound. It does not derive $\gamma$ from the forcing chain (T0--T8) or from the Recognition Composition Law; it only scores the published Cassini number against the RS target scale already fixed upstream.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)