Pith. sign in
module module high

IndisputableMonolith.Verification.FalsifierLikelihoodRegister

show as:
view Lean formalization →

Aggregates the §7 falsifier register: counts total rows, rows carrying likelihood or status certificates, and dataset-only attachments across strong-field, PTA, dark-energy, and ringdown probes. Supplies a single inhabited certificate that the coverage arithmetic closes. Downstream Track-6 sensitivity work cites this register as the Fork-F inventory of observational falsifiers.

claimThe module defines the §7 falsifier-likelihood register: total row count $N_{\mathrm{tot}}$, the subset with likelihood or status certificates $N_{\mathrm{cert}}$, dataset-only rows $N_{\mathrm{data}}$, and individual likelihood artifacts, together with the coverage identity $N_{\mathrm{cert}}+N_{\mathrm{data}}=N_{\mathrm{tot}}$ and an inhabited certificate that the register is well-formed.

background

Recognition Science verification attaches concrete observational datasets to named falsifier rows in §7 of the master plan. Each imported module upgrades one row from a bare dataset handle to a structural likelihood-style or status certificate (0 sorry, 0 RS-internal axiom). Covered probes include Cassini and GRAVITY S2 and EHT M87* strong-field tests, NANOGrav and EPTA pulsar-timing arrays, Planck/BAO/SNe dark-energy $w(z)$ and $\Omega_\Lambda$, and GWTC-3 ringdown/echo/QNM status.

This module does not re-derive those certificates. It tallies them into a single register: total falsifier rows, how many already carry a likelihood or status artifact, how many remain dataset-only, and the list of individual artifacts. The arithmetic identity linking those counts is proved once and packaged as an inhabited certificate object.

proof idea

Definition-and-count module. Constants fix the integer tallies (total rows, certified rows, dataset-only rows, artifact list length). A short arithmetic lemma equates certified plus dataset-only to the total. The certificate structure packages those facts; inhabitance is by direct construction from the constants and the arithmetic lemma. A one-statement theorem restates the whole register claim for downstream import. No analytic likelihood integrals are performed here.

why it matters in Recognition Science

Fork F of Track 6 needs a closed inventory of which §7 falsifiers already have Lean likelihood or status attachments versus bare dataset handles. This register is that inventory. Track6FalsifierSensitivity imports it as the integration endpoint for falsifier sensitivity under the Quantum Gravity Discovery Master Plan. Without the coverage arithmetic and the inhabited certificate, sensitivity claims would rest on an uncounted, informal list of observational rows.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (10)