discriminatorMatrixFull
plain-language theorem explainer
Assembles the full 4×3 gravity discriminator matrix as a single certificate: every cell is a theorem-grade inequality separating Recognition Science from LQG, string theory, CDT, and Bohmian mechanics in the leading-log, echo-damping, and rung-phase sectors. Gravity and quantum-gravity auditors cite it as the Track 6.D binding object. The body is a pure structure inhabitant wiring twelve cell lemmas plus three RS band facts.
Claim. There exists a filled discriminator certificate whose fields are the twelve cell inequalities of the $4\times 3$ matrix (RS vs LQG, string, CDT, Bohmian across leading-log $c_{\mathrm{RS}}$, echo-damping ratio, and rung-phase delay) together with the three RS numerical bands $c_{\mathrm{RS}}\in(-1/4,0)$, $\mathrm{echoDampingRatio}\in(0.617,0.622)$, and $\mathrm{rungPhaseDelay}\in(0,1/2)$.
background
Track 6.D of the quantum-gravity master plan asks for a $4\times 3$ discriminator matrix: rivals LQG, string, CDT, Bohmian against three observational sectors (leading-log entropy coefficient $c_{\mathrm{RS}}$, echo-damping ratio, rung-phase delay $\log\varphi$). Each cell must be a theorem-grade numerical band that separates RS from the rival and is in principle empirically accessible.
The certificate structure packages twelve such inequalities. Against LQG and string the leading-log cells give explicit margins ($c_{\mathrm{RS}}+1/2>1/4$, $c_{\mathrm{RS}}+3/2>5/4$); echo damping and rung phase give half-unit cuts. Against CDT and Bohmian (which predict no quantum-gravity signal in these channels) the cells are positive-existence statements. Upstream, $c_{\mathrm{RS}}\in(-1/4,0)$ comes from the ledger entropy coefficient and $\log\varphi<1/2$; the echo-damping band is the numerical interval $(0.617,0.622)$ around $1/\varphi$; rung-phase delay is $\log\varphi$ with $0<\log\varphi<1/2$.
proof idea
Pure structure construction: each field of DiscriminatorMatrixCert is assigned the corresponding cell lemma already proved in this module or imported. LQG and string leading-log, echo-damping, and rung-phase cells are wired directly. CDT and Bohmian cells use the positive-existence and distinctness lemmas. The three RS band fields are pairs: $c_{\mathrm{RS}}$ from c_RS_gt_neg_quarter and c_RS_neg; echo damping from echoDampingRatio_band; rung phase from rungPhaseDelay_pos and rungPhaseDelay_below_half. No new arithmetic is performed here.
why it matters
This is the binding object for Track 6.D: it witnesses that a discriminator matrix exists with at least one unambiguous cell per rival, closing the master-plan success criterion that three or more discriminators be theorem-grade derivations from $\varphi$ with named observational channels. Downstream, discriminatorMatrixFull_inhabited is the one-line Nonempty wrapper used by the per-rival distinguishability section. The numerical content sits on the RS constants forced by the T5–T6 chain ($J$-uniqueness and $\varphi$ as self-similar fixed point): $c_{\mathrm{RS}}$ from the ledger entropy expansion, echo damping near $1/\varphi$, rung phase $\log\varphi$. Echo-damping and rung-phase cells remain algebraically quarantined until a horizon-consistent physical echo mechanism is supplied; the certificate still satisfies the structural anti-retreat requirement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.