cell_CDT_LeadingLog_distinct
plain-language theorem explainer
RS predicts a strictly negative leading-log coefficient c_RS = −(log φ)/2 for black-hole entropy corrections, while CDT has no recognition ledger and effectively predicts zero. Anyone building or citing the 4×3 gravity discriminator matrix (Track 6.D) uses this cell. The proof is a one-line appeal to the already-proved negativity of c_RS.
Claim. The RS leading-log coefficient satisfies $c_{\mathrm{RS}} < 0$, where $c_{\mathrm{RS}} = -(\log\varphi)/2$. This is distinct from the CDT (no-ledger) prediction of a vanishing leading-log term.
background
Track 6.D of the quantum-gravity plan builds a 4×3 discriminator matrix: rivals (LQG, string, CDT, Bohmian) against sectors (LeadingLog, EchoDamping, RungPhase). Each cell is a theorem-grade inequality separating RS from that rival in an observationally accessible band.
In the LeadingLog sector the RS coefficient is defined by $c_{\mathrm{RS}} = -(\log\varphi)/2 \approx -0.241$ (from the black-hole entropy ledger). CDT has no recognition ledger and supplies no φ-rational leading-log term, so its effective prediction is zero. Any strict negativity of $c_{\mathrm{RS}}$ therefore discriminates.
The upstream fact used here is the already-established lemma that $c_{\mathrm{RS}}$ is negative.
proof idea
One-line term proof: apply the upstream lemma c_RS_neg, which states that the ledger coefficient $c_{\mathrm{RS}} = -(\log\varphi)/2$ is strictly negative. No further algebraic work is required in this cell.
why it matters
Fills the (CDT, LeadingLog) entry of the discriminator matrix. Downstream it is wired into discriminatorMatrixFull, which packages all twelve cells into the Track 6.D certificate. Together with the Session-93 DiscriminatorCert theorems, this closes the binding success criterion: a matrix with at least one unambiguous cell per rival, and three or more theorem-grade φ-derived discriminators with named channels.
CDT and Bohmian cells are existence-style (RS signal present where the rival predicts none), in contrast to the quantitative margins against LQG and string. The result sits in the gravity track that ultimately ties ledger entropy and echo phenomenology back to the forcing chain (φ from T6, eight-tick structure from T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.