gravity_sector_zero_free_parameters_carried_prop
plain-language theorem explainer
Packages the gravity sector's dimensionless constants as a single proposition of φ-closed equalities: action quantum, Einstein coupling, ledger entropy prefactor, echo damping and phase, Bekenstein–Hawking leading term, Hawking temperature, and the baryon-asymmetry rung. Cited by the zero-free-parameter master clause (Track 5.B / Session 96). Pure definitional conjunction; no proof obligations.
Claim. The carried zero-free-parameter content is the conjunction $\hbar = \varphi^{-5}$, $\kappa_E = 8\varphi^{5}$, $c_{\mathrm{RS}} = -(\log\varphi)/2$, echo damping ratio $1/\varphi$, rung phase delay $\log\varphi$, leading black-hole entropy $S_{\mathrm{lead}}(A) = A/4$ for all areas $A$, Hawking temperature $T_H(M) = 1/(8\pi M)$ for all masses $M$, and baryon-asymmetry rung $\eta_B$ equal to $-44$.
background
Module Gravity.MasterTheorem authors the quantum-gravity master statement as a twelve-clause conjunction (Track 7.A). Closed clauses are discharged from existing theorems; open tracks remain as named hypotheses. This declaration is the carried closed-form bundle for the gravity zero-free-parameter clause (M4 / Track 5.B).
In RS-native units one sets $c=1$ and locks the action quantum by $\hbar = E_{\mathrm{coh}}\tau_0 = \varphi^{-5}$. The Einstein coupling then collapses: with $G = \varphi^5/\pi$ one obtains $\kappa_E = 8\varphi^5$. Black-hole ledger entropy supplies the leading area law $S_{\mathrm{lead}}(A)=A/4$ and a structural prefactor $c_{\mathrm{RS}}=-(\log\varphi)/2$. Bounce-echo kinematics fix damping $1/\varphi$ and phase delay $\log\varphi$. Hawking temperature is the standard $1/(8\pi M)$ in these units. Cosmology pins the baryon-asymmetry rung at $-44$ on the $\varphi$-ladder ($\varphi^{44}=1/\eta_B$).
proof idea
No proof. The declaration is a bare Prop abbreviation: an eight-way conjunction of equalities and universal identities naming the closed-form gravity constants. Each conjunct is a literal equality (or a ∀ identity) against an already-defined RS constant or formula; nothing is proved here. Downstream, the parent packages this Prop with a Nonempty witness that the full gravity-sector closed-form bundle is inhabited.
why it matters
Feeds gravity_sector_zero_free_parameters, which conjoins this carried content with Nonempty GravitySectorConstantsClosedForm. That parent is one of the twelve master-theorem clauses under Track 7.A, specifically the Track 5.B / Session 96 zero-free-parameter claim for gravity.
In the Recognition framework this is the gravity-side counterpart of the forcing chain's constant lock: $\hbar=\varphi^{-5}$ and $G\sim\varphi^5$ (primer RS-native units), the area-law entropy and Hawking temperature in those units, echo observables fixed by $\varphi$, and the $\eta_B$ rung $-44$ on the $\varphi$-ladder. It records that none of these dimensionless gravity numbers is a free fit parameter once $\varphi$ is fixed. The unconditional master theorem still waits on five open hypothesis tracks; this clause itself is closed content packaged for the master conjunction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.