closed_certs_hold
plain-language theorem explainer
The six closed certificate clauses of the quantum-gravity master theorem all hold at once: Lorentzian 1+3 signature, SI Hawking temperature, RS leading-log entropy coefficient distinct from LQG and string, cosmological constant fixed by phi, QNM spectroscopy distinct from LQG and string, and zero free gravity-sector parameters. Non-circularity auditors cite this bundle when assembling the master certificate. The proof is a pure term pairing of six independently proved certificate inhabitants.
Claim. The following six propositions hold simultaneously: spacetime signature is Lorentzian $1+3$; Hawking temperature in SI units equals $\hbar_{\mathrm{SI}} c_{\mathrm{SI}}^3 / (8\pi G_{\mathrm{SI}} k_{B,\mathrm{SI}} M_{\mathrm{SI}})$; the RS leading-log black-hole entropy coefficient is observationally distinct from the LQG and string values; the cosmological constant density parameter is fixed by $\varphi$; the RS quasinormal-mode prediction is theorem-grade distinct from LQG and string; and the gravity sector has zero free dimensionless parameters.
background
This module answers a formal-methods referee objection to the unconditional quantum-gravity master theorem. Witness slots of shape $\Sigma(P:\mathrm{Prop}),P$ carry no content unless the plugged-in propositions are genuine, independently proved physics rather than placeholders or the master conclusion itself. The audit therefore discloses each atom of the master conjunction and proves it holds without assuming any master clause.
After maintenance passes M1–M3, three clauses carry real forcing content (T0–T8, cost uniqueness, BMV positivity). The remaining six are closed certificates: each is either a concrete physics identity or a Nonempty inhabitation of a certificate structure. Among them: the SI Hawking law is definitional equality to $\hbar c^3/(8\pi G k_B M)$; the RS leading-log coefficient $c_{RS}=-\log\varphi/2$ is separated from LQG's $-1/2$ and string's $-3/2$ by explicit numerical margins; gravity-sector constants are packaged as a closed-form bundle with no free dimensionless parameters.
The local setting is field-by-field non-circularity: every atom must be inspectably non-self-referential and proved on its own.
proof idea
Pure term-mode 6-tuple. Each conjunct is discharged by the corresponding independently named proven lemma from the master theorem module: Lorentzian signature proven, SI Hawking temperature proven, observable-distinct $c_{RS}$ proven, $\omega_\Lambda$ from $\varphi$ proven, QNM distinctness from LQG/string proven, and zero free parameters proven. No tactics, no rewriting, no master hypothesis is introduced; the conjunction is just the product of those six certificates.
why it matters
This is clause 4 of the single non-circularity certificate: "the six closed certificate clauses hold by certificate inhabitation." That parent theorem packages T0–T8 carriage, J-cost uniqueness carriage, BMV positivity carriage, these six closed certs, unconditional witness inputs, and a non-vacuous D4 Page field into one audit statement.
In the Recognition framework the six atoms touch concrete gravity landmarks: Lorentzian $1+3$ aligns with the T8 forcing of $D=3$ spatial dimensions; Hawking temperature and the $c_{RS}=-\log\varphi/2$ entropy coefficient are the black-hole thermodynamics surface; QNM distinctness is the ringdown discriminator against LQG and string; zero free parameters is the gravity-sector claim that constants are fixed by $\varphi$ (with RS-native $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$). Without this bundle the master theorem would still look like a $\Sigma$-witness of placeholders. With it, peer-review findings F1/Rec 2 are answered field by field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.