individualLikelihoodArtifacts
plain-language theorem explainer
Fixes the count of individual likelihood/status artifacts from Sessions 107–115 at eight. Verification and QG-falsifier coverage work cites it when stating how much of the §7 register has been upgraded beyond bare dataset attachment. It is a bare natural-number definition, not a derived equality.
Claim. The number of individual likelihood/status artifacts attached to the quantum-gravity §7 falsifier register equals $8$.
background
The Falsifier Likelihood Register module is structural coverage accounting over the quantum-gravity master plan §7 falsifier list. Session 106 attached named datasets and positive sensitivity scales to all ten rows. Sessions 107–115 then added likelihood-style or status-style reproducibility artifacts on a subset of those rows.
The eight counted artifacts are: ΩΛ/Planck likelihood, Cassini strong-field, GRAVITY S2 strong-field, EHT M87* strong-field, NANOGrav PTA, EPTA PTA scope-control, dark-energy constant-$w$, and GWTC-3 ringdown/echo/QNM status. Six of the ten §7 rows are thereby upgraded; four (BMV, Hawking temperature, leading-log entropy coefficient, Page curve) remain dataset-only.
This constant is pure inventory: it does not encode fit quality or empirical confirmation.
proof idea
Definitional constant: the natural number is set equal to 8 by fiat, matching the enumerated Session 107–115 artifact list in the module documentation. No lemma application or tactic proof is involved.
why it matters
Gives the numerator for the likelihood/status layer of the §7 register. Downstream, individual_artifact_count_pos proves the count is positive by unfolding and decide. The one-statement coverage theorem packages the equalities (eight artifacts, six upgraded rows, four dataset-only, ten total, and the partition identity) into a single conjunction. The aggregate certificate structure FalsifierLikelihoodRegisterCert witnesses nonempty certificates for each of the eight artifacts. Together they close the Sessions 107–115 coverage claim with zero sorry and no new RS axioms, while leaving the four dataset-only rows explicitly open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.