LeadingLogDiscriminator
plain-language theorem explainer
Packages four strict inequalities that separate the RS leading-log black-hole entropy coefficient $c_{RS}=-\log\varphi/2$ from the LQG value $-1/2$ and the string value $-3/2$. Ringdown spectroscopists and holographic-entropy analysts cite it when comparing quantum-gravity programs. Pure structure: the fields are Prop obligations discharged later by Session 90 margin lemmas.
Claim. A record of four separation claims for the RS leading-log entropy coefficient $c_{\mathrm{RS}}=-(\log\varphi)/2$: $c_{\mathrm{RS}}-(-1/2)>1/4$, $c_{\mathrm{RS}}-(-3/2)>5/4$, $|c_{\mathrm{RS}}-(-1/2)|>1/4$, and $|c_{\mathrm{RS}}-(-3/2)|>5/4$.
background
Track 6 of the gravity program aggregates theorem-grade discriminators between Recognition Science and canonical quantum-gravity alternatives (LQG, string theory, no-echo semiclassical Hawking). The binding success criterion demands three or more $\varphi$-derived discriminators with named observational channels; this module supplies that matrix.
The leading-log coefficient is defined in the ledger entropy development as $c_{\mathrm{RS}}=-({\log}\varphi)/2\approx -0.241$. LQG canonically takes $-1/2$ and string theory $-3/2$. Session 90 (BlackHoleEntropySI) already proved the numerical margins $c_{\mathrm{RS}}+1/2>1/4$ and $c_{\mathrm{RS}}+3/2>5/4$, together with the absolute-value forms. The observational channel is quasinormal-mode spectroscopy of black-hole ringdown (and holographic entanglement-entropy probes): sensitivity finer than $0.25$ on the leading-log coefficient distinguishes RS from LQG.
proof idea
No proof body: this is a structure whose four fields are propositions. Inhabitation is deferred to the companion definition that wires in the Session 90 margin lemmas (c_RS_LQG_margin, c_RS_string_margin, and their absolute-value counterparts). The structure itself only names the four inequalities that any valid leading-log discriminator must carry.
why it matters
First of the three theorem-grade discriminators required by Track 6. It is a field of the master DiscriminatorMatrixCert, which bundles leading-log, echo-damping, and rung-phase separations into a single inhabited certificate covering RS vs LQG, RS vs string, RS vs uniform discreteness, and RS vs no-echo. Downstream, the inhabitation lemma fills the four fields from the Session 90 SI margins, so the matrix cert closes without sorry or RS-internal axioms.
Framework link: $c_{\mathrm{RS}}$ is built from $\varphi$, the self-similar fixed point forced at T6 of the unified forcing chain. The observational falsification threshold (margin $>1/4$ against LQG) is therefore a pure $\varphi$-rational prediction, not a fitted parameter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.