rowsWithLikelihoodOrStatusRecords
plain-language theorem explainer
Counts how many falsifier-register rows have been upgraded past dataset-only status to likelihood or status artifacts. Track 6 / Fork F sensitivity packaging cites this constant in the single Lean-facing certificate. It is a one-line alias of the upstream likelihood-register count, fixed at six.
Claim. Let $N_{\mathrm{lik}}$ be the number of falsifier-register rows that carry likelihood or status records (not merely dataset attachments). Then $N_{\mathrm{lik}}$ is defined to equal the corresponding count in the falsifier likelihood register (presently $6$).
background
Track 6 is the Fork F integration endpoint in the Quantum Gravity Discovery Master Plan. This module packages existing work only: a theorem-grade phi-derived discriminator matrix, named dataset attachments on falsifier-register rows, likelihood/status coverage for rows upgraded beyond dataset-only, and a guarded GWTC-3 ringdown runner that blocks mixed-family posterior aggregation.
The falsifier likelihood register maintains a separate tally of rows that already have likelihood or status artifacts, not just dataset pointers. Upstream, that tally is the natural number rowsWithLikelihoodOrStatus, documented as rows upgraded beyond dataset-only to likelihood/status records, and currently equal to 6.
The certificate is intentionally conservative: it proves a single Lean-facing sensitivity package with named channels and guarded reproducibility surfaces. It does not claim empirical confirmation or promote still-structural PTA, strong-field, or ringdown physics into a discovery statement.
proof idea
Definitional one-line wrapper. The local constant is set equal to the upstream natural FalsifierLikelihoodRegister.rowsWithLikelihoodOrStatus (itself the literal 6). No tactics, no lemmas, no computation beyond that alias.
why it matters
This constant is one conjunct in the Fork F handoff. Downstream, Track6SensitivityEndpoint and track6_falsifier_sensitivity_one_statement require rowsWithLikelihoodOrStatusRecords = 6 alongside three theorem-grade discriminator sectors, four rival rows covered, ten dataset-attached falsifier rows, and the guarded GWTC-3 ringdown family/mapping counts.
It closes the "likelihood/status coverage" bullet of the Track 6 packaging claim: six rows are recorded as upgraded beyond dataset-only. That is structural bookkeeping for the sensitivity certificate, not a physics derivation from the forcing chain (T0–T8) or the Recognition Composition Law. Open empirical questions (PTA, strong-field, ringdown discovery claims) remain explicitly out of scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.