gravitySectorConstantsClosedForm
plain-language theorem explainer
Packages closed-form φ-expressions for every gravity-sector constant on the Track 5.B audit list: native ℏ, Einstein couplings, BMV phase, black-hole entropy and echo coefficients, Hawking temperature, and the baryogenesis rung. Gravity theorists citing the zero-free-parameters claim use this inhabitant as the certificate. Construction is field-by-field wiring of named RS identities and definitional equalities.
Claim. There is a gravity-sector closed-form certificate whose fields assert: $\hbar = \varphi^{-5}$, Einstein coupling $\kappa_E = 8\varphi^5$, zero-parameter gravity coupling $\kappa_{rs} = 8\varphi^5$, BMV coefficient $\alpha_{RS} = \varphi^5/(8\pi)$, black-hole entropy log coefficient $c_{RS} = -(\log\varphi)/2$, echo damping ratio $1/\varphi$, rung phase delay $\log\varphi$, bounce radius $N \mapsto \varphi^N$, Hawking temperature $T(M) = 1/(8\pi M)$, and baryogenesis rung integer equal to $-44$ (so $\eta_B = \varphi^{-44}$).
background
Track 5.B of the quantum-gravity master plan demands a Lean certificate that every gravity-sector constant is a closed-form function of $\varphi$, with the dimensional SI bridge anchored on the single CODATA measurement $G_{SI}$ (plus SI-2019-exact $c$, $\hbar$, $k_B$). The structure GravitySectorConstantsClosedForm is that audit record: one field per constant on the plan's table, each typed as an equality to a $\varphi$-rational expression.
Native units fix $c = 1$ and $\hbar = \varphi^{-5}$ (THEOREM C-004.1: $\hbar = E_{\mathrm{coh}}\tau_0$ with lock $\varphi^{-5}$ and $\tau_0 = 1$; the exponent $5 = D+2$ is forced). Einstein coupling then expands to $\kappa_E = 8\varphi^5$ by unfolding $G$, $\hbar$, and the recognition length. Parallel identities give $\kappa_{rs}$, the BMV phase $\alpha_{RS} = \varphi^5/(8\pi)$, black-hole ledger entropy leading log, per-echo damping $1/\varphi$, rung phase $\log\varphi$, bounce radius $\varphi^N$, and Hawking $T = 1/(8\pi M)$.
The baryogenesis field pins the $\eta_B$ rung integer at $-44$, so $\eta_B = \varphi^{-44}$ on the $\varphi$-ladder.
proof idea
Structure inhabitant, not a derived proof. Each field is filled by a named upstream equality or by rfl against an in-scope definition:
- $\hbar$ and $\kappa_E$ cite
Constants.hbar_eq_phi_inv_fifthandConstants.kappa_einstein_eq(unfold-and-simp / field-simp reductions in native units). - $\kappa_{rs}$ cites
ZeroParameterGravity.kappa_rs_closed_form. - $\alpha_{RS}$, $c_{RS}$, echo damping, rung phase delay, and bounce radius are definitional (
rfl). - Hawking temperature cites
HawkingTemperatureFromRung.T_hawking_def. - Leading black-hole entropy cites
BlackHoleEntropyFromLedger.S_lead_eq_BH. - Baryogenesis rung is
rflto the integer $-44`.
No tactic search; pure record assembly of already-proved anchors.
why it matters
This inhabitant is the concrete witness behind the gravity-sector zero-free-parameters theorem: gravity_sector_zero_free_parameters is simply Nonempty of the structure, proved by packaging this value. The master theorem gravity_sector_zero_free_parameters_proven projects the same fields into the cross-sector cert.
In framework terms it closes master-plan §4 Track 5.B: zero free dimensionless gravity parameters, one dimensional anchor $G_{SI}$. It sits on the RS-native constants forced by the chain ($\hbar = \varphi^{-5}$, $G = \varphi^5/\pi$ in native units) and on the black-hole ledger/echo/Hawking modules that express horizon thermodynamics as $\varphi$-ladder quantities. Downstream consumers only need the nonempty certificate; they do not re-derive each identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.