gravity_sector_zero_free_parameters
plain-language theorem explainer
Every gravity-sector dimensionless constant admits a closed-form φ-rational expression, with the SI bridge fixed by the single CODATA anchor G_SI. Quantum-gravity auditors and anyone citing Track 5.B of the master plan use this as the zero-free-parameters certificate. The proof is a one-line term witness: the named closed-form bundle inhabits the structure, so the type is nonempty.
Claim. There exists a closed-form audit record for the gravity sector: every listed dimensionless gravity constant equals an explicit $\varphi$-rational expression ($\hbar=\varphi^{-5}$, $\kappa_E=\kappa_{\mathrm{rs}}=8\varphi^5$, $\alpha_{\mathrm{RS}}=\varphi^5/(8\pi)$, BH entropy leading-log $c_{\mathrm{RS}}=-\log\varphi/2$, echo damping $1/\varphi$, rung phase delay $\log\varphi$, bounce radius $\varphi^N$, Hawking $T=1/(8\pi M)$, and $c=1$, $G=\varphi^5/\pi$ in RS-native units), with the dimensional bridge anchored solely on the CODATA measurement $G_{\mathrm{SI}}$.
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$, plus one empirical dimensional anchor. This module supplies that audit as the structure GravitySectorConstantsClosedForm: a record whose fields are equalities such as $\hbar=\varphi^{-5}$, Einstein coupling $\kappa_E=8\varphi^5$, zero-parameter-gravity $\kappa_{\mathrm{rs}}=8\varphi^5$, BMV phase $\alpha_{\mathrm{RS}}=\varphi^5/(8\pi)$, black-hole entropy leading-log $c_{\mathrm{RS}}=-\log\varphi/2$, per-echo damping $1/\varphi$, per-rung phase $\log\varphi$, bounce radius $\varphi^N$, and Hawking temperature $1/(8\pi M)$.
RS-native units fix $c=1$ and $G=\varphi^5/\pi$ (via $\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$). The SI bridge is deliberately not free: it is pinned to the single CODATA measurement $G_{\mathrm{SI}}$ (with SI-2019-exact $c_{\mathrm{SI}}$, $\hbar_{\mathrm{SI}}$, $k_{B,\mathrm{SI}}$). Upstream named anchors live in Constants, ZeroParameterGravity, NoGraviton.UnitBridge, BlackHoleEntropyFromLedger, BlackHoleEchoesFromBounce, HawkingTemperatureFromRung, and Cosmology.PhiRungLadder.
The master-theorem side packages the same claim as a Prop conjunction of carried closed-form content with nonemptiness of this structure.
proof idea
One-line term proof. The structure is inhabited by the concrete value gravitySectorConstantsClosedForm, whose fields are already discharged by rfl or by the named anchor theorems listed in the module audit table. Nonemptiness is therefore immediate: introduce that witness with anonymous constructor syntax. No further case analysis or algebraic work occurs at this declaration.
why it matters
This is the Track 5.B closure form of the quantum-gravity master plan: zero free dimensionless parameters in the gravity sector, one dimensional anchor. It feeds the master-theorem Prop that conjoins carried closed-form content with nonemptiness of the audit bundle, and the proven wrapper that assembles field-by-field equalities from the same witness.
Downstream it sits inside RSQuantumGravityMaster (Track 7.A template) and the non-circularity audit's closed-certificate conjunction. Framework landmarks it locks are the RS-native constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$ from the forcing chain and the $\varphi$-ladder. Strong-field tests distinct from GR remain an open hypothesis elsewhere; this theorem does not close that clause, only the constants audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.