falsifierLikelihoodRegisterCert_inhabited
plain-language theorem explainer
The aggregate likelihood/status register certificate is inhabited: a single bundled witness packs nonempty certificates for the eight upgraded §7 falsifier artifacts. Verification and Track-6 sensitivity proofs cite it to discharge Nonempty obligations on that bundle. The proof is a one-line term handing over the concrete certificate instance already built in the module.
Claim. The type of aggregate falsifier likelihood/status register certificates is nonempty: there exists a structure packing 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/echo/QNM layers.
background
This module is the coverage ledger for 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 of those rows to likelihood-style or status-style reproducibility artifacts.
Current accounting (explicitly not empirical confirmation): eight individual likelihood/status artifacts; six of ten rows upgraded beyond dataset-only (echo phenomenology, $\Omega_\Lambda$, dark-energy $w(z)$, QNM/ringdown, PTA stochastic GW, strong-field tests); four rows still dataset-only (BMV, Hawking temperature, leading-log entropy coefficient, Page curve). The aggregate certificate is a structure whose fields are Nonempty witnesses for each upgraded artifact.
proof idea
One-line term proof. The module already constructs a concrete value of the aggregate certificate, with each field filled by the corresponding individual likelihood or status certificate instance. The theorem simply packages that value as a Nonempty witness via the anonymous constructor. No further lemmas are applied.
why it matters
Parent consumers are the one-statement coverage theorem (which asserts the arithmetic identities: 8 individual artifacts, 6 upgraded rows, 4 dataset-only, 10 total, and the partition sum) and the Track-6 falsifier sensitivity certificate (Fork F endpoint). Together they close the §7 likelihood/status layer as structural verification infrastructure: zero sorry, zero new RS-specific axioms.
This is coverage accounting inside the Verification domain, not a step of the T0--T8 forcing chain, the Recognition Composition Law, or the mass ladder. It records that the upgraded falsifier rows carry machine-checkable likelihood or status artifacts so downstream sensitivity and discriminator certificates can cite a single inhabited bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.