GravitySectorConstantsClosedForm
plain-language theorem explainer
Certificate type bundling closed-form φ-expressions for every gravity-sector constant in the Track 5.B audit: native ℏ, Einstein and RS couplings, BMV phase coefficient, BH entropy/echo parameters, Hawking temperature, leading area-law entropy, and the baryogenesis rung. Cited by anyone claiming the gravity sector has zero free dimensionless parameters. The structure is a pure Prop bundle; the inhabitant fills each field by a named equality or rfl.
Claim. A record asserting: RS-native $\hbar=\phi^{-5}$; Einstein coupling $\kappa_E=8\phi^{5}$; zero-parameter gravity coupling $\kappa_{\mathrm{rs}}=8\phi^{5}$; BMV phase coefficient $\alpha_{\mathrm{RS}}=\phi^{5}/(8\pi)$; BH entropy leading-log coefficient $c_{\mathrm{RS}}=-(\log\phi)/2$; per-echo damping ratio $1/\phi$; per-rung phase delay $\log\phi$; bounce radius at rung $N$ equals $\phi^{N}$; Hawking temperature $T_H(M)=1/(8\pi M)$; leading Bekenstein-Hawking entropy $S_{\mathrm{lead}}(A)=A/4$; and baryogenesis rung integer equal to $-44$.
background
Module Gravity.ZeroFreeParameters implements Track 5.B of the quantum-gravity master plan: every gravity-sector constant must be a closed-form function of $\phi$, with a single empirical dimensional anchor. Status is structural (0 sorry, 0 RS-internal axiom). The audit table pairs each constant with a named anchor theorem.
RS-native units fix $c=1$ and define $\hbar=E_{\mathrm{coh}}\tau_0=\phi^{-5}$. Einstein $\kappa=8\pi G/c^4$ then collapses, via $G=\lambda_{\mathrm{rec}}^2 c^3/(\pi\hbar)$ with $\lambda_{\mathrm{rec}}=c=1$, to $8\phi^5$. Parallel closed forms cover the BMV phase coefficient, ledger-derived BH entropy log coefficient, bounce-echo damping and phase delay, rung-native bounce radius, Hawking $T$, and area-law $S_{\mathrm{lead}}$.
The baryogenesis entry pins the $\phi$-ladder rung $\eta_B$ integer at $-44$, so $\eta_B=\phi^{-44}$ as a pure $\phi$-power. Upstream defs such as Constants.hbar, kappa_einstein, and eta_B_rung_val supply the concrete values being certified.
proof idea
No proof body: this is a structure whose fields are propositions (equalities). Each field names the closed-form claim for one audited constant. The companion inhabitant gravitySectorConstantsClosedForm populates every field by a named lemma (hbar_eq_phi_inv_fifth, kappa_einstein_eq, kappa_rs_closed_form, ...) or by rfl when the def already is the closed form. Downstream, gravity_sector_zero_free_parameters is simply Nonempty of this structure, witnessed by that inhabitant.
why it matters
This is the constants-from-$\phi$ audit certificate required by master-plan §4 Track 5.B. Together with the SI bridge (single CODATA $G_{\mathrm{SI}}$ anchor), it underwrites the claim: zero free dimensionless parameters in the gravity sector; one dimensional anchor.
Parent consumers are gravity_sector_zero_free_parameters in this module and the MasterTheorem packaging that conjoins carried closed-form content with Nonempty GravitySectorConstantsClosedForm. Framework landmarks hit directly: $\hbar=\phi^{-5}$, $G=\phi^5/\pi$ (via the $\kappa_E=8\phi^5$ reduction), and the $\phi$-ladder mass/rung structure for $\eta_B=\phi^{-44}$. Closes the Track 5.B structural theorem rather than leaving an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.