Pith. sign in
module module high

IndisputableMonolith.Gravity.StrongFieldStructural

show as:
view Lean formalization →

Records the structural RS strong-field deviation at scale $\varphi^{-44}$, the same rung that forces the baryon asymmetry $\eta_B$. Supplies positivity and distinct-from-GR witnesses shared by strong-field observable channels. Gravity master-theorem and verification authors cite it when pre-filling strong-field inputs and likelihood certificates. Content is definitional packaging plus arithmetic positivity, not channel dynamics.

claimThe RS strong-field structural deviation scale is $\varphi^{-44}$, identical to the baryogenesis rung $\eta_B = \varphi^{-44}$. For typed strong-field observable channels the RS observable shift is strictly positive while the pure-GR shift vanishes, giving a structural witness that RS predictions differ from pure GR at this scale.

background

Recognition Science places dimensionless ratios on a $\varphi$-ladder. The cosmology rung-ladder module records the baryon-asymmetry rung at $-44$, so $\eta_B = \varphi^{-44}$, and proves its arithmetic factorizations through the eight-tick period. This gravity module reuses that same forcing scale as the structural strong-field deviation signature.

Track 7.A states a master gravity theorem in conditional form and needs structural inputs that discriminate RS from pure GR in the strong-field regime. Target channels include S-star precession, the EHT shadow, and Cassini Shapiro delay. Each channel still needs its own physics derivation; the shared skeleton is positivity of a $\varphi^{-44}$-scale shift away from pure GR.

Imports bring RS-native constants (including $\varphi$), the $\varphi$-rung ladder identities, and the ambient master-theorem statement that consumes the witness.

proof idea

Definition-and-witness module, not a dynamical derivation. It names the deviation $\varphi^{-44}$, records positivity from $\varphi > 1$, and packages a distinct-from-GR proposition with a structural witness. Typed observable-channel factors and RS versus pure-GR shifts appear as definitions with positivity lemmas. No field equations are solved; the work is arithmetic identity plus structural packaging for master-theorem hypothesis slots and downstream likelihood attachments.

why it matters in Recognition Science

Feeds the Gravity Track 7.A master-theorem stack: partial, deeper-partial, fully structural, and unconditional closure surfaces all import this module to pre-fill the strong-field hypothesis input. QG observable signal models hang typed RS-versus-data channels on the same skeleton. Verification modules for Cassini, EHT M87, and S2 attach dataset-specific likelihood certificates on top of the structural positivity.

The module doc ties the scale explicitly to the baryogenesis rung in the $\varphi$-ladder, so one forcing number appears in both cosmology and strong-field gravity. It closes the structural half of strong-field discrimination; upgrading witnesses from structural to dynamical remains future work on the unconditional path.

scope and limits

used by (9)

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

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (20)