cRS_clause_is_cert
plain-language theorem explainer
The leading-log entropy discriminator clause of the QG master theorem is definitionally the four strict margin inequalities on the RS coefficient versus LQG and semiclassical values, conjoined with inhabitance of the SI black-hole entropy certificate. Non-circularity auditors cite this to confirm the clause is neither a True placeholder nor the master conclusion in disguise. The proof is pure reflexivity against the clause definition.
Claim. The master-theorem clause that the RS leading-log entropy coefficient is observable-distinct equals, by definition, the conjunction of (i) four strict inequalities placing $c_{\mathrm{RS}}$ more than $1/4$ from the LQG value $-1/2$ and more than $5/4$ from the semiclassical value $-3/2$ (signed and absolute forms), and (ii) inhabitance of the SI black-hole entropy certificate.
background
This module is a field-by-field non-circularity audit of the unconditional quantum-gravity master theorem. A formal-methods referee objected that witness structures of shape $\Sigma(P:\mathrm{Prop}),,P$ carry no content if $P$ is True, so the master theorem is only as strong as the concrete propositions in its five slots. For each atom the audit therefore discloses, by reflexivity, exactly which proposition the field is, and separately proves that field holds unconditionally.
The clause under audit is the Track 3.B leading-log discriminator. Its carried content (M4) asserts four strict separations of the ledger-derived RS coefficient $c_{\mathrm{RS}}$ from the loop value $-1/2$ and the semiclassical value $-3/2$. The second conjunct is inhabitance of the SI black-hole entropy certificate: the master cert for the SI lift of leading entropy plus sharper discriminator margins against LQG and string.
proof idea
One-line reflexivity. The left-hand side is the definition of the master clause whose body is exactly the right-hand side conjunction (carried M4 margins and inhabitance of the SI entropy cert). Both sides unfold to the same proposition, so rfl closes with no lemmas.
why it matters
Answers peer-review finding F1 / Rec 2: the master theorem's witness slots must be genuine physics, not placeholders and not conclusion-bearing self-references. Sibling disclosures in this module cover the T0-T8 forcing chain, cost uniqueness, BMV positivity, Lorentzian structure, and Hawking radiation; this one covers the leading-log discriminator (M4). After disclosure, non-circularity of the assembled master conclusion follows because each conjunct is an independently named, non-self-referential proposition. The clause sits in the gravity domain and supports Track 3.B partial closure on black-hole entropy discriminators. It does not itself invoke T0-T8 or the Recognition Composition Law; it only names the ledger-derived $c_{\mathrm{RS}}$ margins and the SI cert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.