individual_artifact_count_pos
plain-language theorem explainer
The count of individual likelihood/status artifacts attached to the §7 falsifier register is strictly positive. Verification and coverage auditors cite it when assembling the aggregate likelihood-register certificate. The proof unfolds the numeric definition and discharges the inequality by `decide`.
Claim. The number of individual likelihood-or-status reproducibility artifacts registered against the quantum-gravity §7 falsifier rows is strictly greater than zero: $0 < N_{\mathrm{indiv}}$.
background
The Falsifier Likelihood Register aggregates Sessions 107--115 over the quantum-gravity master plan §7 falsifier table. Session 106 already attached named datasets and positive sensitivity scales to all ten rows. Later sessions upgrade a subset of those rows from dataset-only stubs to likelihood-style or status-style reproducibility artifacts.
Module accounting records eight such individual artifacts (ΩΛ/Planck, Cassini strong-field, GRAVITY S2, EHT M87*, 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 beyond dataset-only; four (BMV, Hawking temperature, leading-log entropy coefficient, Page curve) remain future work. The constant individualLikelihoodArtifacts is exactly that integer count. This layer is coverage bookkeeping, not empirical confirmation of Recognition Science predictions.
proof idea
One-line computational proof. Unfold the definition of the individual-artifact count (a concrete natural-number literal equal to 8 under the current register) and invoke Lean's decide tactic, which evaluates the closed inequality $0 < 8$ in the kernel.
why it matters
The inequality is a trivial but required positivity guard inside the aggregate certificate falsifierLikelihoodRegisterCert, which packages inhabited certificates for the eight upgraded rows (ΩΛ/Planck, Cassini, GRAVITY S2, EHT M87*, NANOGrav, and the remaining PTA/dark-energy/GWTC-3 entries). Downstream one-statement wrappers and inhabitedness lemmas for the whole register rely on the count being positive so that the coverage claim is not vacuously empty.
In the broader RS verification stack this sits at the dataset-likelihood layer above the forcing chain (T0--T8) and the gravity seven-gaps program; it does not itself touch J-uniqueness, φ, the eight-tick octave, or $D=3$. It only certifies that the falsifier table has begun to carry concrete likelihood/status artifacts rather than pure dataset names.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.