rivalPrediction
plain-language theorem explainer
Lookup table of rival quantum-gravity predictions on the 4×3 discriminator matrix: each (rival, sector) pair is either a concrete real coefficient or no prediction. Gravity-track authors cite it when comparing RS bands to LQG, string, CDT, and Bohmian. Pure exhaustive case definition; no proof obligations.
Claim. A function from rival programs $\{LQG, String, CDT, Bohmian\}$ and sectors $\{LeadingLog, EchoDamping, RungPhase\}$ to $\mathrm{Option}\,\mathbb{R}$: $\mathrm{some}(r)$ if the rival states a definite real $r$, else $\mathrm{none}$. LQG: $c=-1/2$, damping $1/2$, phase $1/2$. String: $c=-3/2$, damping $1/2$, no clean rung phase. CDT and Bohmian: no $\phi$-rational signal in any sector.
background
Track 6.D of the quantum-gravity master plan asks for a discriminator matrix with four rival programs (LQG, string, CDT, Bohmian/Diósi–Penrose) against three algebraic sectors. Leading-log is the black-hole entropy coefficient $c$ in the log-area correction (physical, Session 90 / QNM spectroscopy). Echo damping and rung phase are quarantined $\phi$-rung amplitude and phase coefficients until the echo mechanism is fully derived.
Rivals that state a number enter as $\mathrm{some}(r)$: LQG area quantization gives $c=-1/2$ and half-quantum phase/damping $1/2$; Strominger–Vafa string entropy gives $c=-3/2$ with uniform fuzzball damping $1/2$. CDT and Bohmian supply no matching $\phi$-rational algebra, so those cells are $\mathrm{none}$. RS then discriminates either by numerical margin against a stated $r$, or by positive existence when the rival predicts silence.
The module pairs this table with RS lower/upper bands and theorem-grade cell inequalities (margins $>1/4$, $>5/4$, $>1/2$, $<1/2$, or $>0$).
proof idea
Definition by exhaustive pattern match on the product of the two inductives. Each constructor pair is assigned a literal Option ℝ (concrete rationals for LQG/string filled cells; none elsewhere). No lemmas, tactics, or computation beyond the match.
why it matters
Fills the rival half of Track 6.D's binding criterion: a 4×3 matrix with at least one unambiguous distinction per rival, empirically accessible. Downstream cell theorems (LQG/String leading-log margins, echo-damping and rung-phase comparisons, CDT/Bohmian positive-existence cells) read rival values from this table and compare them to RS bands built from $\phi$.
Together with Session 93's theorem-grade discriminators, it closes the structural success line: three or more $\phi$-derived discriminators with named observational channels, and a matrix in which every rival row has a distinguishing cell. Landmark contact is indirect: the RS side of each cell uses the $\phi$-ladder and eight-tick structure; this definition only records the external literature anchors ($-1/2$, $-3/2$, half-quantum echoes) against which those RS predictions are scored.
No used_by edges are recorded yet; sibling cell lemmas are the intended consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.