falsifierLikelihoodRegisterCert
plain-language theorem explainer
A single aggregate certificate packing eight dataset-specific likelihood or status artifacts for the quantum-gravity falsifier register, plus two coverage arithmetic facts. Verification and cosmology auditors cite it to show that the likelihood layer over §7 is inhabited as one object. Construction is pure structure assembly from the eight inhabited sub-certificates and the two local counting lemmas.
Claim. There is an aggregate likelihood/status register certificate whose fields are: nonempty Planck $\Omega_\Lambda$ likelihood, nonempty Cassini strong-field likelihood, nonempty GRAVITY S2 strong-field likelihood, nonempty EHT M87* strong-field likelihood, nonempty NANOGrav PTA likelihood, nonempty EPTA PTA likelihood, nonempty constant-$w$ dark-energy likelihood, nonempty GWTC-3 ringdown/echo/QNM status, together with the arithmetic identities that six of ten §7 rows are upgraded beyond dataset-only and that the individual-artifact count is positive.
background
The module is the structural closure of Sessions 107--115: the likelihood/status layer 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 reproducibility artifacts that are either likelihood-style or status-style.
The aggregate structure FalsifierLikelihoodRegisterCert records nonempty certificates for eight individual artifacts: Planck $\Omega_\Lambda$, Cassini, GRAVITY S2, EHT M87*, NANOGrav PTA, EPTA PTA, constant-$w$ dark energy, and GWTC-3 ringdown status. Two further fields encode coverage arithmetic: six of ten §7 rows upgraded beyond dataset-only, and a strictly positive individual-artifact count. The remaining four rows (BMV, Hawking temperature, leading-log entropy coefficient, Page curve) stay dataset-only.
Upstream, each field is witnessed by a one-line inhabited theorem from its own module (e.g. Cassini, EHT M87*, EPTA, dark-energy $w_0$). The dark-energy density parameter itself is the fixed observational anchor $\Omega_\Lambda = 0.68$. This is coverage accounting, not empirical confirmation of Recognition Science predictions.
proof idea
Pure structure construction. Each of the eight certificate fields is filled by the corresponding inhabited theorem from its module (omegaLambdaPlanckLikelihoodCert_inhabited, cassiniStrongFieldLikelihoodCert_inhabited, gravityS2StrongFieldLikelihoodCert_inhabited, ehtM87StrongFieldLikelihoodCert_inhabited, nanogravPTALikelihoodCert_inhabited, eptaPTALikelihoodCert_inhabited, darkEnergyWPlanckLikelihoodCert_inhabited, gwtc3RingdownStatusCert_inhabited). The two arithmetic fields are discharged by the local lemmas row_coverage_arithmetic and individual_artifact_count_pos. No further reasoning; the definition is the packed witness.
why it matters
This definition is the single packed object that the one-statement coverage theorem falsifierLikelihoodRegisterCert_inhabited wraps as Nonempty FalsifierLikelihoodRegisterCert. Downstream auditors therefore obtain the entire likelihood/status layer of the §7 falsifier register from one inhabitation fact rather than eight separate imports.
Within Recognition Science verification, it closes the structural side of Sessions 107--115: eight individual artifacts, six of ten rows upgraded, zero sorry, zero new RS-specific axioms. It does not touch the forcing chain (T0--T8), the Recognition Composition Law, or the mass ladder; it sits entirely in the external falsifier-accounting layer that records which observational channels have been attached at likelihood or status depth. The open remainder is explicit: four §7 rows (BMV, Hawking temperature, leading-log entropy, Page curve) remain dataset-only pending future sessions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.