PerRivalDistinguishability
plain-language theorem explainer
Packages the Track 6.D requirement that every rival row carry at least one explicit discriminator inequality: RS leading-log coefficient separated from LQG (−1/2) by margin > 1/4 and from string (−3/2) by margin > 5/4, plus strictly positive echo-damping against CDT and Bohmian. Gravity and verification authors cite it when discharging matrix row coverage. Pure structure interface; the witness is filled by a sibling constructor.
Claim. A record of four inequalities that witness per-rival distinguishability: $c_{\mathrm{RS}}-(-1/2)>1/4$ (LQG leading-log), $c_{\mathrm{RS}}-(-3/2)>5/4$ (string leading-log), and $0<r_{\mathrm{echo}}$ for both CDT and Bohmian, where $c_{\mathrm{RS}}=(1-\varphi^{-8})^2$ is the RS leading-log prefactor and $r_{\mathrm{echo}}=1/\varphi$ is the per-echo amplitude damping ratio.
background
Track 6.D of the quantum-gravity master plan asks for a 4×N discriminator matrix (rivals: LQG, string, CDT, Bohmian) whose cells are numerical bands separating Recognition Science from each rival, with every row empirically accessible. This module builds that matrix over three sectors: leading-log coefficient, echo damping, and rung phase.
The RS leading-log entry is $c_{\mathrm{RS}}=(1-\varphi^{-8})^2$, the squared two-sided 8-tick washout prefactor from the $\eta_B$ derivation. LQG and string supply fixed rival anchors $-1/2$ and $-3/2$; the structure records explicit positive margins against those anchors. Echo damping uses $r_{\mathrm{echo}}=1/\varphi$ (per-echo amplitude ratio from the bounce-echo model). CDT and Bohmian predict no quantum-gravity echo signal, so any strictly positive RS ratio discriminates.
The binding success criterion needs both theorem-grade discriminators and "at least one cell per rival showing an unambiguous distinction." This structure is the formal type of that second clause.
proof idea
No proof body: this is a structure whose four fields are propositions. Each field is a concrete inequality (two margin comparisons on $c_{\mathrm{RS}}$, two positivity statements on the echo-damping ratio). Instantiation is deferred to the sibling constructor perRivalDistinguishability_holds, which plugs in the already-proved margin lemmas and the positivity of $1/\varphi$.
why it matters
Closes the row-coverage half of Track 6.D's binding success criterion: every rival must have at least one unambiguous cell. The sibling perRivalDistinguishability_holds builds a concrete inhabitant from the leading-log margin theorems and echo-damping positivity. Downstream, Track6FalsifierSensitivityCert requires "the four required rival rows have per-rival distinguishability," so this type is the handoff object into the Fork F verification certificate.
Together with Session 93's three theorem-grade discriminator sectors, the matrix satisfies both Track 6 bullets (three-plus theorem-grade channels; full per-rival coverage). The LQG/string margins are numerical and observationally named; the CDT/Bohmian cells use the anti-retreat pattern that any positive RS echo signal defeats a null prediction. Landmarks in play: $\varphi$-native echo damping $1/\varphi$ and the eight-tick factor inside $c_{\mathrm{RS}}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.