datasetOnlyRows
plain-language theorem explainer
Defines the count of quantum-gravity §7 falsifier rows that remain dataset-only (not yet upgraded to likelihood or status artifacts) as the natural number 4. Verification and Track-6 sensitivity certificates cite it when stating coverage arithmetic. The body is a literal constant assignment, not a derived proof.
Claim. The number of §7 falsifier-register rows that are still dataset-only (or future work), rather than upgraded to a likelihood-style or status-style reproducibility artifact, is $4$.
background
The Falsifier Likelihood Register module is structural coverage accounting over the quantum-gravity master-plan §7 falsifier list. Session 106 attached named datasets and positive sensitivity scales to all ten rows. Sessions 107--115 then upgraded a subset to likelihood or status artifacts (ΩΛ/Planck, Cassini, GRAVITY S2, EHT M87*, NANOGrav, EPTA, dark-energy $w$, GWTC-3 ringdown/echo/QNM status).
Six of the ten rows are thereby upgraded beyond dataset-only (echo phenomenology, ΩΛ, dark-energy $w(z)$, QNM/ringdown, PTA stochastic GW, strong-field tests). The remaining four stay dataset-only/future: BMV, Hawking temperature, leading-log entropy coefficient, and the Page curve. This definition names that residual count. The module states explicitly that the accounting is coverage, not empirical confirmation, and carries zero sorry and no new RS-specific axioms.
proof idea
Literal definition: the natural-number constant is set to 4. No lemmas, tactics, or algebraic reduction. Downstream theorems such as row_coverage_arithmetic unfold this name together with the sibling counts and discharge the identity by decide.
why it matters
Feeds the aggregate certificate FalsifierLikelihoodRegisterCert and the one-statement coverage theorem, which packages
$(8$ individual artifacts$) \wedge (6$ upgraded rows$) \wedge (4$ dataset-only$) \wedge (10$ total$) \wedge$ the partition identity. Also appears in Track-6 falsifier-sensitivity certification as the likelihood/status coverage handoff field.
In the Recognition verification stack this is the residual side of the §7 register after Sessions 107--115: it pins how much of the falsifier list still lacks a likelihood or status artifact. It does not touch the forcing chain (T0--T8), RCL, or the mass ladder; it is pure verification bookkeeping that keeps the open BMV / Hawking / entropy-coefficient / Page-curve rows visible rather than silently dropped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.