Pith. sign in
module module high

IndisputableMonolith.Gravity.ZeroFreeParameters

show as:
view Lean formalization →

Audit module packaging every Track 5.B gravity-sector constant as a closed-form φ-rational expression, each field anchored on a named upstream theorem or rfl. Anyone citing the RS claim of zero free dimensionless gravity parameters (one dimensional G_SI anchor) would reference it. Structure is a constants record plus a one-statement audit theorem; proofs are thin wrappers over imported identities.

claimEvery gravity-sector constant in the master-plan Track 5.B audit admits a closed-form $\varphi$-rational expression, each field justified by a named theorem. Together with the single CODATA $G_{\mathrm{SI}}$ dimensional anchor from the SI bridge, the RS gravity sector has zero free dimensionless parameters and one dimensional anchor.

background

Recognition Science fixes gravity-sector quantities from $\varphi$ and the discrete ledger, with RS-native units $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$. This module aggregates that claim for the gravity track.

Upstream inputs include ZeroParameterGravity (dimensionless coupling $\kappa_{rs}=8\varphi^5$ and its numerical band), the no-graviton unit bridge converting $\kappa_{rs}$ to an SI BMV phase rate, black-hole entropy from the ledger (Bekenstein-Hawking $S_{BH}=A/(4\ell_P^2)$ recovered as a count of admissible horizon states, with a $\varphi$-rational leading log correction), Hawking temperature as a structural identity from rung spacing, and the structural $\varphi$-rung algebra for echoes (physical bounce-to-exterior mechanism quarantined).

The $\varphi$-ladder and eight-tick arithmetic (PhiRungLadder; forcing T6--T7) supply the backbone so that closed forms are $\varphi$-rational once the structural identities exist.

proof idea

Definition-and-audit module, not a fresh derivation. It introduces a structure whose fields are the Track 5.B gravity constants, each populated by rfl or by a named theorem from the imported gravity modules (zero-parameter gravity, unit bridge, ledger entropy, Hawking-from-rung, echo rung algebra). Companion theorems package the audit into one statement: every listed constant is closed-form $\varphi$-rational, and the only dimensional input is the single CODATA $G_{SI}$ anchor. Proofs are thin wrappers citing those upstream identities.

why it matters in Recognition Science

Direct import into Gravity.MasterTheorem (Track 7.A master statement). The module doc states this is the constants-from-$\varphi$ audit required by master plan §4 Track 5.B: zero free dimensionless parameters and one dimensional anchor, paired with Foundation.SIBridgeClosure. That audit is load-bearing for the master theorem's conditional gravity closure.

It unifies ZeroParameterGravity, the $\kappa_{rs}\to$SI bridge, ledger entropy, Hawking temperature from rung, and echo rung algebra under one referee-facing object. Framework landmarks: $\varphi$ forced at T6, native $G=\varphi^5/\pi$, and discrete ledger counting that recovers $S_{BH}$. Open upstream caveats (echo mechanism quarantine; SI bridge hypothesis on Hawking) remain inherited, not resolved here.

scope and limits

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (4)