row_coverage_arithmetic
plain-language theorem explainer
Six §7 falsifier-register rows upgraded to likelihood/status artifacts plus four still dataset-only sum to the ten-row register total. Coverage accountants and Track-6 certificate builders cite it to lock the partition arithmetic. The proof unfolds three Nat constants and closes by `decide`.
Claim. If $N_{\mathrm{upgraded}}$ is the number of quantum-gravity master-plan §7 falsifier-register rows carrying likelihood or status artifacts, $N_{\mathrm{dataset}}$ the number still dataset-only, and $N_{\mathrm{total}}$ the full register size, then $N_{\mathrm{upgraded}} + N_{\mathrm{dataset}} = N_{\mathrm{total}}$, i.e. $6 + 4 = 10$.
background
The Falsifier Likelihood Register aggregates Sessions 107--115 over the quantum-gravity master plan §7 falsifier list. Session 106 already attached named datasets and positive sensitivity scales to all ten rows. Later sessions upgraded a subset to likelihood-style or status-style reproducibility artifacts (ΩΛ/Planck, Cassini, GRAVITY S2, EHT M87*, NANOGrav, EPTA, constant-w dark energy, GWTC-3 ringdown/echo/QNM).
Three module-level Nat constants record the partition: total falsifier-register rows equals 10; rows upgraded beyond dataset-only equal 6; rows still dataset-only/future equal 4. The module doc stresses this is coverage accounting, not empirical confirmation, with zero sorry and no new RS-specific axioms.
proof idea
One-line tactic proof. Unfold the three definitions rowsWithLikelihoodOrStatus, datasetOnlyRows, and totalFalsifierRows to the concrete naturals 6, 4, and 10, then close the equality by decide (kernel Nat arithmetic). No lemmas beyond definitional unfolding are required.
why it matters
Locks the additive partition used by the one-statement coverage theorem falsifier_likelihood_register_one_statement, which packages individual-artifact count, upgraded-row count, dataset-only count, total rows, and this sum into a single conjunction. The same equality is part of the structural certificate surface consumed by falsifierLikelihoodRegisterCert and by the Track-6 fork-F endpoint track6FalsifierSensitivityCert.
Inside Recognition Science verification this is bookkeeping for the §7 falsifier layer: it certifies that the six upgraded rows and four remaining dataset-only rows (BMV, Hawking temperature, leading-log entropy coefficient, Page curve) exhaust the ten-row register without double-counting or omission. It does not advance the forcing chain (T0--T8) or any dynamical claim; it closes a coverage invariant so downstream certificates can quote a single arithmetic fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.