Rival
plain-language theorem explainer
Enumerates the four rival quantum-gravity programs (LQG, string theory, CDT/causal sets, Bohmian/Diósi–Penrose) that Track 6.D must discriminate against. Anyone building or citing the 4×3 discriminator matrix uses this type as the row index. It is a plain inductive enumeration with decidable equality; no proof content.
Claim. Let $\mathrm{Rival}$ be the finite set of four canonical alternative quantum-gravity programs: loop quantum gravity (area-quantum coefficient $c_{\mathrm{LQG}}=-1/2$), string theory (Strominger–Vafa coefficient $c_{\mathrm{string}}=-3/2$), causal dynamical triangulations / causal-set discreteness, and Bohmian / Diósi–Penrose stochastic-collapse substrates. Equality on this set is decidable.
background
Track 6.D of the quantum-gravity master plan requires a discriminator matrix with rows indexed by rival programs and columns by algebraic sectors, each cell a numerical band that separates Recognition Science (RS) from that rival on an empirically accessible channel.
The three sectors (defined alongside this type) are: leading-log black-hole entropy coefficient; echo-damping amplitude ratio; and rung-phase coefficient. The leading-log sector is treated as physical; the echo-damping and rung-phase sectors are quarantined rung algebra until an echo mechanism is derived.
RS predictions live on the $\varphi$-ladder and eight-tick structure (T6–T7). Rival programs enter only through their published coefficients or through the absence of a signal (CDT, Bohmian), so that any positive RS prediction discriminates by existence.
proof idea
No proof: this is an inductive type with four nullary constructors and a derived DecidableEq instance. The constructors are pure labels; numerical rival values are attached later by the prediction map on pairs (rival, sector).
why it matters
This type is the row index of the Track 6.D discriminator matrix. Downstream, rivalPrediction assigns to each rival–sector pair either a concrete real (e.g. LQG leading-log $-1/2$, string $-3/2$, uniform-discreteness echo $1/2$) or none when the rival predicts no signal. The companion sector type supplies the three columns.
Together with Session 93's theorem-grade discriminator certificates, the filled matrix closes the Track 6 binding criterion: at least three $\varphi$-derived discriminators with named observational channels, and at least one unambiguous cell per rival. Margins against LQG and string are explicit ($>1/4$, $>5/4$, $>1/2$, $<1/2$); against CDT and Bohmian, positivity of the RS signal suffices.
It does not itself invoke T5 J-uniqueness or the Recognition Composition Law; those enter only when RS cell bounds are proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.