Pith. sign in
module module moderate

IndisputableMonolith.Verification.GravityS2StrongFieldLikelihood

show as:
view Lean formalization →

Verification module attaching the GRAVITY-S2 Schwarzschild-precession factor measurement to the quantum-gravity falsifier register. It records the observed FSP central value and uncertainty, the RS target scale, the residual, and a one-sigma pass certificate. Downstream likelihood aggregation cites it as the S2 strong-field row. Content is definitional constants plus elementary positivity and residual inequalities.

claimFor the GRAVITY-S2 strong-field row, fix the observed Schwarzschild-precession factor $F_{\mathrm{SP}}$ with central value and $\sigma$, the RS target scale $s_{\mathrm{RS}}>0$, and the predicted $F_{\mathrm{SP}}^{\mathrm{RS}}$. The residual $r=|F_{\mathrm{SP}}-F_{\mathrm{SP}}^{\mathrm{RS}}|$ satisfies $r<\sigma$, and $\sigma>s_{\mathrm{RS}}$. A likelihood certificate packages these facts for the falsifier register.

background

Track 6.C of the quantum-gravity master plan treats strong-field tests as structural discriminators between Recognition Science and standard GR-plus-dark-sector phenomenology. The upstream StrongFieldStructural module supplies the form of those discriminators (status: structural theorem, zero sorry). S2 stellar orbits around Sgr A* constrain the Schwarzschild precession factor $F_{\mathrm{SP}}$; GRAVITY reports a central value and uncertainty that this module pins as named constants.

FalsifierRegisterDatasets attaches concrete named datasets and numerical sensitivity records to every row of the master-plan §7 falsifier register. This module is the S2-specific attachment: observed FSP, RS predicted FSP, residual, and positivity lemmas for $\sigma$ and the RS target scale. The local setting is verification bookkeeping, not a new dynamical derivation.

proof idea

Definitional layer: named constants for the GRAVITY-S2 FSP central value, sigma, RS target scale, RS predicted FSP, and residual. Two positivity facts ($\sigma>0$, target scale $>0$) are immediate from the numeric literals. The residual-less-than-one-sigma and sigma-greater-than-RS-target claims are direct numeric comparisons. A dataset-attachment status flag and a bundled likelihood certificate package the row for the register. No deep tactic proof; the module is constants plus trivial inequalities.

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 S2 strong-field discriminator has no numeric attachment and cannot contribute a pass/fail likelihood. It closes the GRAVITY-S2 cell of Track 6.C under the structural-theorem standard (zero sorry, zero RS-internal axiom) already claimed by the upstream strong-field and dataset modules. Landmark contact is empirical: strong-field GR tests as external checks on the RS forcing chain, not an internal T0--T8 step.

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)