cell_String_LeadingLog
plain-language theorem explainer
RS leading-log coefficient sits strictly more than 5/4 above string theory's canonical −3/2. Gravity-track authors cite it as the (String, LeadingLog) cell of the 4×3 discriminator matrix. Proof is a one-line wrapper of the SI-bridge margin theorem.
Claim. Let $c_{\mathrm{RS}} = -(\log\varphi)/2$ be the RS leading-log coefficient in black-hole entropy. Then $c_{\mathrm{RS}} - (-3/2) > 5/4$, i.e. RS lies more than $5/4$ above the string-theory value $-3/2$.
background
Track 6.D builds a 4×3 discriminator matrix (rivals: LQG, string, CDT, Bohmian; sectors: LeadingLog, EchoDamping, RungPhase). Each cell is a theorem-grade numerical band separating RS from that rival on an observationally accessible channel.
The LeadingLog sector compares the coefficient of the leading logarithmic correction to black-hole entropy. In RS that coefficient is $c_{\mathrm{RS}} = -(\log\varphi)/2 \approx -0.241$ (from BlackHoleEntropyFromLedger). String theory's canonical value is $-3/2$.
The upstream theorem c_RS_string_margin already proves the strict margin: any experimental sensitivity finer than $5/4$ distinguishes the two. This declaration is the matrix-cell packaging of that fact.
proof idea
One-line term wrapper: the goal is definitionally identical to c_RS_string_margin from BlackHoleEntropySI, so the proof is just that name. Upstream, the margin expands as $(3 - \log\varphi)/2$ and uses $\log\varphi < 1/2$ plus linarith.
why it matters
Fills the (String, LeadingLog) slot of discriminatorMatrixFull, the certificate that closes Track 6.D of the quantum-gravity master plan. Combined with Session 93's three theorem-grade discriminators, it meets the binding success criterion: a matrix with at least one unambiguous cell per rival, and three or more φ-derived discriminators with named observational channels.
The explicit margin $> 5/4$ is stronger than the LQG cell ($> 1/4$), so string is the easiest LeadingLog rival to rule out. It does not invoke the eight-tick octave or $D=3$ directly; the separation is pure φ-arithmetic on the entropy log coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.