DiscriminatorMatrixCert
plain-language theorem explainer
Certificate type for the 4x3 gravity discriminator matrix: each field is an inequality separating Recognition Science from LQG, string theory, CDT, or Bohmian mechanics in leading-log, echo-damping, or rung-phase. Cited by Track 6.D and the QNM distinctness master theorem. Pure structure definition; inhabitation is proved by composing per-cell lemmas elsewhere.
Claim. A certificate is a record of inequalities: against LQG, $c_{\mathrm{RS}}-(-1/2)>1/4$, echo-damping ratio $>1/2$, rung-phase delay $<1/2$; against string theory, $c_{\mathrm{RS}}-(-3/2)>5/4$, echo-damping $>1/2$, rung-phase $>0$; against CDT and Bohmian, $c_{\mathrm{RS}}<0$ with strictly positive echo-damping and rung-phase; plus bands $-1/4<c_{\mathrm{RS}}<0$, $0.617<$ echo-damping $<0.622$, and $0<$ rung-phase $<1/2$.
background
Track 6.D of the quantum-gravity master plan asks for a 4 (rivals) by 3 (sectors) discriminator matrix whose cells are numerical bands separating Recognition Science from LQG, string theory, CDT, and Bohmian mechanics, each row empirically accessible. Sectors are the leading-log coefficient $c_{\mathrm{RS}}$, the black-hole echo damping ratio, and the rung-phase delay tied to $\log\varphi$.
LQG is anchored at leading-log $-1/2$ and string theory at $-3/2$; RS must sit in $(-1/4,0)$. CDT and Bohmian rows treat absence of a quantum-gravity echo or phase signal as the rival baseline, so any strictly positive RS value discriminates. Echo damping and rung phase remain algebraic cells until a horizon-consistent physical echo mechanism exists.
Upstream inputs include the RS leading-log coefficient (structural prefactor lineage from the cosmology bridge) and the bounce-module echo damping ratio. Module status: structural theorem, zero sorry, zero RS-internal axiom.
proof idea
No proof body: this is a structure whose fields are proposition-valued inequalities, not a proved theorem. Inhabitation is supplied downstream by discriminatorMatrixFull, which fills each field from a named per-cell lemma (LQG/String margin cells and CDT/Bohmian sign cells). A coarser packaging in DiscriminatorCert composes three sector-level bundles into a master cert. Nonemptiness theorems wrap those constructions.
why it matters
This is the Lean shape of Track 6 success criterion 2: a discriminator matrix with at least one unambiguous cell per rival. It is inhabited by discriminatorMatrixFull and referenced from DiscriminatorCert and from rs_qnm_distinct_LQG_string in the gravity master theorem (carried QNM margin plus nonempty matrix cert). It also feeds Track6FalsifierSensitivityCert.
It turns Session 93 discriminators into the explicit 4x3 grid with numerical margins against LQG and string and positive-existence cells against CDT and Bohmian. Echo and rung-phase cells stay quarantined algebra until a physical echo channel is fixed; the leading-log row is the sharpest present handle. No T0-T8 forcing step is proved here; content is comparative phenomenology on phi-native constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.