Pith. sign in
module module high

IndisputableMonolith.Verification.GravityS2StrongFieldLikelihood

show as:
view Lean formalization →

Attaches the GRAVITY S2 Schwarzschild-precession factor measurement to the quantum-gravity falsifier likelihood layer. Records the observed FSP central value and uncertainty, the RS target scale, the residual, and one-sigma comparison lemmas, then packages them as a named likelihood certificate. Downstream falsifier aggregation imports this certificate. The argument is pure numerical attachment plus positivity and residual inequalities, not a dynamical derivation.

claimFor the GRAVITY S2 strong-field datum, fix the observed Schwarzschild-precession factor $F_{\mathrm{SP}}$ with central value and $\sigma>0$, the RS target scale $s_{\mathrm{RS}}>0$, and the predicted $F_{\mathrm{SP}}^{\mathrm{RS}}$. Define the residual $r=|F_{\mathrm{SP}}-F_{\mathrm{SP}}^{\mathrm{RS}}|$ and certify $r<\sigma$ together with $\sigma>s_{\mathrm{RS}}$, plus a dataset-attachment status and a likelihood certificate object for the falsifier register.

background

Track 6.C of the quantum-gravity master plan isolates strong-field structural discriminators: observables that can separate Recognition Science gravity from pure GR in the near-horizon or high-curvature regime. The upstream structural module states the form of those tests with zero sorry and no RS-internal axioms.

S2 (the star S0-2 orbiting Sgr A*) supplies a concrete Schwarzschild-precession factor measurement. This module does not re-derive orbital dynamics; it binds the published central value, its uncertainty, and the RS-predicted FSP scale into named constants and residual comparisons.

The sibling falsifier-dataset module attaches named datasets and sensitivity records to every row of master-plan §7. Here the attachment is specialized to GRAVITY S2 and exposed as a likelihood certificate consumable by the register.

proof idea

Definition-and-certificate module, not a deep proof development. Constants fix the S2 FSP central value, sigma, RS target scale, and RS-predicted FSP. Residual is the absolute deviation from the RS prediction. Short positivity lemmas discharge $\sigma>0$ and target-scale positivity. Two comparison lemmas assert residual below one sigma and sigma above the RS target scale. A dataset-attachment status flag and a bundled likelihood certificate close the module for import by the falsifier likelihood register.

why it matters in Recognition Science

Feeds FalsifierLikelihoodRegister, which aggregates Sessions 107--115 into the dataset-specific likelihood and status layer over master-plan §7. Without this attachment, the GRAVITY S2 strong-field row would lack a concrete numerical likelihood object.

Closes the S2 instance of Track 6.C structural discrimination: the residual-versus-sigma comparison is the operational falsifier hook. If future GRAVITY reductions move the central value or inflate sigma past the certified inequalities, the certificate and register status must be updated. Sits entirely on the verification side; it does not alter the forcing chain (T0--T8) or the RCL.

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 (14)