c_RS_observable_distinct
plain-language theorem explainer
The Track 3.B discriminator clause: the RS leading-log black-hole entropy coefficient is observationally distinct from both LQG and string/semiclassical values. It packages the carried margin inequalities (M4) with existence of the SI entropy certificate. Gravity auditors cite it inside the twelve-clause quantum-gravity master statement. Definitional conjunction only; inhabitation is discharged by the companion proven theorem from the SI cert fields.
Claim. The proposition that the RS leading-log entropy coefficient $c_{\mathrm{RS}}$ obeys the strict signed margins $c_{\mathrm{RS}}-(-1/2)>1/4$ and $c_{\mathrm{RS}}-(-3/2)>5/4$, together with the matching absolute-value bounds against the LQG value $-1/2$ and the semiclassical value $-3/2$, and that the SI black-hole entropy certificate is inhabited.
background
In the Gravity Master Theorem module (Track 7.A), the quantum-gravity discovery is authored as a twelve-clause conjunction. Eight clauses are closed from existing certificates; five remain hypothesis inputs. This definition is the closed Track 3.B / Session 90 clause on leading-log entropy discriminators.
The carried content asserts four strict inequalities for the RS coefficient $c_{\mathrm{RS}}$ relative to the loop value $-1/2$ and the semiclassical value $-3/2$: signed gaps larger than $1/4$ and $5/4$ respectively, plus the absolute-value forms of the same margins. Upstream, BlackHoleEntropySICert is the master SI-lift certificate: it equates $S_{\mathrm{BH,SI}}(A)$ to the Bekenstein–Hawking formula in SI units and supplies the sharper discriminator margins against LQG and string.
Local setting: the module authors the conditional master statement gated on open tracks, without claiming the discovery is complete. This clause is one of the closed certificates that the conditional proof discharges internally.
proof idea
Definitional, not a tactic proof. The proposition is the conjunction of two pieces: the carried margin content (four strict inequalities on $c_{\mathrm{RS}}$ versus $-1/2$ and $-3/2$) and Nonempty of the SI black-hole entropy certificate structure. No lemmas are applied at this site; the body is pure Prop assembly. Inhabitation is supplied separately by the companion theorem, which packages the four margin fields and the cert instance from the SI entropy certificate.
why it matters
This is clause M4 inside the master statement of the quantum-gravity discovery. The master Prop conjoins it with Hawking temperature SI, QNM discriminators, and the foundation block (T0–T8, cost uniqueness, Lorentzian 1+3) among the closed limbs. Downstream, the companion proven theorem inhabits it from the SI cert; the non-circularity audit lists it among the six closed certificate clauses and discloses that the clause equals carried margins conjoined with Nonempty of the SI cert.
Framework role: it makes the RS leading-log coefficient an observable discriminator against LQG and string, not merely a formal rewrite of Bekenstein–Hawking. It does not touch the still-open strong-field, Page-curve, or PTA hypotheses. Once those close, the unconditional master theorem can drop its five inputs; this clause is already on the closed side of that ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.