falsifier_likelihood_register_one_statement
plain-language theorem explainer
Packages the §7 falsifier likelihood/status layer into one conjunction: eight individual artifacts, six of ten rows upgraded beyond dataset-only, four still dataset-only, ten total rows, the partition identity 6+4=10, and a nonempty aggregate certificate. Verification authors cite it as the closed coverage ledger for Sessions 107–115. The proof is a six-field term constructor of four definitional equalities, the arithmetic lemma, and the inhabited certificate.
Claim. There are exactly $8$ individual likelihood/status artifacts; exactly $6$ of the ten $\S7$ falsifier rows carry a likelihood or status record; exactly $4$ rows remain dataset-only; the total number of falsifier rows is $10$; these counts satisfy $6+4=10$; and the aggregate likelihood/status certificate is inhabited (nonempty).
background
The module is the structural ledger for the quantum-gravity master-plan §7 falsifier register after Sessions 107–115. 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 scope control, constant-$w$ dark energy, GWTC-3 ringdown/echo/QNM status).
Named counts are pure naturals: individualLikelihoodArtifacts := 8, rowsWithLikelihoodOrStatus := 6, datasetOnlyRows := 4, totalFalsifierRows := 10. The remaining four rows (BMV, Hawking temperature, leading-log entropy coefficient, Page curve) stay dataset-only/future. The aggregate certificate is a structure whose fields are nonempty certificates from each of the eight artifact modules.
This is coverage accounting only: zero sorry, zero new RS-internal axioms, and no claim of empirical confirmation.
proof idea
Term-mode six-component constructor. The four numeric equalities are definitional (rfl against the def bodies). The partition identity is discharged by row_coverage_arithmetic, which unfolds the three count definitions and closes by decide. Nonemptiness of the aggregate certificate is falsifierLikelihoodRegisterCert_inhabited, itself a one-line wrapper around the concrete inhabitant falsifierLikelihoodRegisterCert.
why it matters
Closes the §7 likelihood/status layer as a single citeable statement for the Verification domain. Downstream consumers (none yet wired in this graph) can import one theorem instead of eight module certificates plus four count defs. It records the exact upgrade frontier: six rows beyond dataset-only, four still open (BMV, Hawking $T$, leading-log entropy, Page curve). Within Recognition Science this is bookkeeping on the falsifier register, not a forcing-chain step (T0–T8) or a constants claim; its value is auditability of what has and has not been lifted to likelihood/status form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.