rivalRowsCovered
plain-language theorem explainer
Track 6.D requires exactly four rival-theory rows in the discriminator matrix: LQG, string, CDT/causal sets, and Bohmian/Diósi–Penrose. The constant records that coverage count as a Nat. Downstream certificates and the Fork F handoff theorem cite it to assert per-rival distinguishability is present. It is a bare numeric definition, discharged by rfl wherever equality to 4 is needed.
Claim. The Track 6.D rival-row coverage count is the natural number $4$, corresponding to the four named rival frameworks (loop quantum gravity, string theory, CDT/causal sets, and Bohmian/Diósi–Penrose).
background
Track 6 of the Quantum Gravity Discovery Master Plan is the falsifier-sensitivity lane. This module is its Fork F integration endpoint: it packages existing work (phi-derived discriminator matrix, falsifier-register dataset attachments, likelihood/status coverage, and the guarded GWTC-3 ringdown runner) into one Lean-facing certificate without new observational claims.
The discriminator matrix supplies theorem-grade per-rival distinguishability. Track 6.D specifically demands four rival rows: LQG, string, CDT/causal sets, and Bohmian/Diósi–Penrose. This definition is the numeric stand-in for that requirement, parallel to sibling counts for discriminator sectors, dataset attachments, and ringdown families.
The certificate is intentionally conservative: named channels and guarded reproducibility surfaces only, not empirical confirmation or a final discovery statement.
proof idea
Pure definition: the constant is the natural number literal 4. No lemmas or tactics. Downstream equalities such as rival_rows_covered_count close by rfl.
why it matters
Fork F handoff needs an explicit rival-row count so the sensitivity package can assert per-rival matrix coverage. Track6FalsifierSensitivityCert carries a field requiring this constant equal 4 ("the four required rival rows have per-rival distinguishability"). The one-statement theorem track6_falsifier_sensitivity_one_statement and the master handoff Track6SensitivityEndpoint both conjoin rivalRowsCovered = 4 with the other Track 6 counts (three theorem-grade discriminator sectors, ten dataset-attached falsifier rows, six likelihood/status rows, guarded ringdown families).
In the Recognition verification stack this is bookkeeping for QG rival discrimination, not a physics derivation from the forcing chain (T0–T8) or the RCL. It closes the structural claim that the four named rivals sit in the matrix before any empirical lane is upgraded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.