FalsifierLikelihoodRegisterCert
plain-language theorem explainer
Aggregate certificate bundling eight nonempty likelihood/status artifacts (ΩΛ/Planck, Cassini, GRAVITY S2, EHT M87*, NANOGrav, EPTA, dark-energy w, GWTC-3 ringdown) with two coverage equalities over the §7 falsifier register. Verification and Track-6 authors cite it as the structural handoff that the likelihood layer is inhabited and arithmetically closed. As a structure definition there is no proof body; inhabitance is supplied downstream.
Claim. A register certificate is a record of: nonempty certificates for the $\Omega_\Lambda$/Planck, Cassini strong-field, GRAVITY S2, EHT M87*, NANOGrav PTA, EPTA PTA, dark-energy constant-$w$, and GWTC-3 ringdown/status likelihood artifacts; the coverage identity (rows with likelihood or status) $+$ (dataset-only rows) $=$ (total falsifier rows); and the positivity $0 <$ (number of individual likelihood artifacts).
background
The module is the structural closure of Sessions 107--115 over the quantum-gravity master plan §7 falsifier register. Session 106 already attached named datasets and positive sensitivity scales to all ten §7 rows. Sessions 107--115 then upgraded a subset to likelihood-style or status-style reproducibility artifacts.
The eight fields demand nonempty certificates from the corresponding modules: $\Omega_\Lambda$ (Planck), Cassini and GRAVITY S2 and EHT M87* strong-field residuals, NANOGrav and EPTA pulsar-timing arrays, dark-energy $w$, and GWTC-3 ringdown/echo/QNM status. Upstream snippets fix the local meaning: each cert packages positive sigmas/targets, residual bounds, and often an explicit not_currently_sensitive flag.
Coverage arithmetic is internal: datasetOnlyRows = 4, six of ten rows upgraded beyond dataset-only, four remaining future (BMV, Hawking temperature, leading-log entropy, Page curve). The module states this is coverage accounting, not empirical confirmation.
proof idea
No proof body: the declaration is a structure. It packages eight Nonempty fields (one per individual likelihood/status cert) plus two Prop fields, row_coverage (the sum identity over total falsifier rows) and individual_artifacts_positive (strict positivity of the artifact count). Downstream, falsifierLikelihoodRegisterCert fills every field from the corresponding *_inhabited witnesses and the module arithmetic lemmas; falsifierLikelihoodRegisterCert_inhabited is then the one-line ⟨...⟩ wrapper.
why it matters
This is the aggregate type for the §7 likelihood/status layer. It feeds falsifierLikelihoodRegisterCert, the inhabited witness, and the one-statement coverage theorem that pins the counts $(8,6,4,10)$ and the sum identity. Track 6 (Track6FalsifierSensitivityCert) consumes it as the "likelihood/status coverage" handoff among discriminator sectors, rival-row distinguishability, dataset attachments, and guarded GWTC-3 processing.
In the Recognition verification stack it records structural progress on falsifiability infrastructure rather than a forcing-chain step (T0--T8) or a constant derivation. Open remainder: four §7 rows stay dataset-only/future; several upgraded certs still mark currentlySensitive = false. Zero sorry, zero new RS axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.