rival_rows_covered_count
plain-language theorem explainer
The Track 6 rival-row counter equals four: LQG, string, CDT/causal sets, and Bohmian/Diósi–Penrose. Anyone citing the Fork F sensitivity certificate or the one-statement Track 6 handoff needs this equality. The proof is pure reflexivity on the definitional constant.
Claim. The number of rival-theory rows required by Track 6.D equals $4$.
background
Track 6 is the falsifier-sensitivity lane in the Quantum Gravity Discovery Master Plan. This module is its Fork F integration endpoint: it packages existing theorem-grade pieces (phi-derived discriminator matrix, falsifier-register dataset attachments, likelihood/status coverage, and a guarded GWTC-3 ringdown runner) into one Lean-facing certificate without new observational claims.
The constant being counted is the set of rival rows Track 6.D must cover: loop quantum gravity, string theory, CDT/causal sets, and Bohmian/Diósi–Penrose. Upstream it is defined as the natural number $4$. Downstream certificates and the one-statement handoff theorem assert that this count is exactly four, alongside three discriminator sectors, ten dataset-attached falsifier rows, and related guarded ringdown surfaces.
proof idea
One-line reflexivity. The definition sets the rival-row count to $4$, so rfl discharges equality by definitional reduction. No lemmas are applied.
why it matters
This equality is a field of the Fork F endpoint certificate (rival_row_count) and a conjunct of the Track 6 one-statement handoff theorem, which packages three theorem-grade discriminator sectors, four rival rows, ten dataset-attached falsifier-register rows, six likelihood/status upgrades, and a guarded GWTC-3 ringdown runner with two supported mappings.
In the Recognition verification stack it is bookkeeping, not new physics: it locks the rival coverage claim so the sensitivity package cannot silently drop a competitor. The module is intentionally conservative; it does not claim empirical confirmation or promote still-structural PTA/strong-field/ringdown physics to a discovery statement. Framework landmarks (T0–T8, RCL, mass ladder) are upstream of the discriminator matrix this certificate only counts against, not proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.