cell_Bohmian_LeadingLog_distinct
plain-language theorem explainer
RS predicts a strictly negative leading-log coefficient for black-hole entropy corrections, c_RS = −(log φ)/2 < 0. That single inequality is the LeadingLog discriminator cell against Bohmian and Diósi–Penrose substrates, which produce no quantum-gravity signal in this sector. Anyone building or citing the 4×3 rival discriminator matrix uses it. 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 the LeadingLog cell distinguishing Recognition Science from Bohmian / Diósi–Penrose substrates (which predict no quantum-gravity signature in this channel).
background
Track 6.D of the quantum-gravity master plan builds a 4×3 discriminator matrix (rivals: LQG, string, CDT, Bohmian) × (sectors: LeadingLog, EchoDamping, RungPhase). Each cell is a theorem-grade numerical band that separates RS from the rival on an empirically accessible channel.
In the LeadingLog sector the RS coefficient is defined in the black-hole entropy ledger as $c_{\mathrm{RS}} = -(\log\varphi)/2 \approx -0.241$. Because $\varphi > 1$, $\log\varphi > 0$, so the coefficient is negative. Bohmian and Diósi–Penrose substrates are argued not to produce quantum-gravity signatures here (continuous trajectories conflict with T2; stochastic collapse conflicts with T1), so any definite RS prediction discriminates.
The upstream lemma c_RS_neg already records $c_{\mathrm{RS}} < 0$ by unfolding the definition and applying positivity of $\log\varphi$.
proof idea
One-line term proof: the goal is exactly the statement of the upstream theorem that the leading-log coefficient is negative. The proof therefore reduces to that lemma (unfold $c_{\mathrm{RS}}$, use $1 < \varphi$ to get $\log\varphi > 0$, then linear arithmetic).
why it matters
Fills the (Bohmian, LeadingLog) cell of the discriminator matrix. Downstream it is wired into discriminatorMatrixFull, which packages all twelve cells into the Track 6.D certificate. Together with the LQG/String margin cells and the CDT/Bohmian positivity cells, it meets the binding success criterion: a matrix with at least one unambiguous distinction per rival, and three or more theorem-grade discriminators derived from $\varphi$.
The cell is deliberately weak (existence of a sign, not a numerical margin): Bohmian/DP predict no signal, so $c_{\mathrm{RS}} < 0$ already separates RS. It sits beside the parallel CDT LeadingLog cell and the EchoDamping/RungPhase rows that use $1/\varphi$ and $\log\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.