dataset_attachment_row_count
plain-language theorem explainer
The falsifier register carries named dataset attachments on exactly ten rows. Track 6 sensitivity packaging and the Fork F handoff cite this count as the dataset-coverage leg of the certificate. The proof is pure reflexivity: the count definition reduces definitionally to ten.
Claim. The number of falsifier-register rows that carry named dataset attachments equals $10$.
background
Track 6 is the Fork F integration endpoint in the Quantum Gravity Discovery Master Plan. It does not open a new observational lane; it packages existing Lean surfaces: the theorem-grade phi-derived discriminator matrix, named dataset and sensitivity attachments on falsifier-register rows, likelihood or status upgrades beyond dataset-only status, and a guarded GWTC-3 ringdown runner that blocks mixed-family posterior aggregation.
The quantity counted here is the number of falsifier-register rows with named dataset attachments. In this module it is defined to equal the total falsifier-row count from the likelihood register (FalsifierLikelihoodRegister.totalFalsifierRows). Sibling counts cover discriminator sectors, rival-row coverage, likelihood/status upgrades, and guarded ringdown families and mappings.
The certificate is intentionally conservative: named channels and guarded reproducibility surfaces only, with no claim of empirical confirmation and no upgrade of still-structural PTA, strong-field, or ringdown physics into a discovery statement.
proof idea
One-line reflexivity proof. The left-hand side is the definition falsifierRowsWithDatasetAttachments, which is definitionally FalsifierLikelihoodRegister.totalFalsifierRows. That constant reduces to the numeral 10, so rfl closes the equality.
why it matters
This count is one conjunct of the Fork F handoff theorem track6_falsifier_sensitivity_one_statement, which asserts a single integration endpoint: three theorem-grade discriminator sectors, four rival rows covered by the discriminator matrix, all ten falsifier-register rows dataset-attached, six rows upgraded to likelihood or status records, and a guarded GWTC-3 ringdown runner with two supported observable mappings.
It therefore closes the dataset-attachment leg of the Track 6 sensitivity package without adding RS-internal assumptions. Downstream readers use it to certify that every falsifier-register row has a named data channel before any likelihood or ringdown claim is discussed. It does not touch the forcing chain (T0–T8), RCL, or the mass ladder; its role is verification bookkeeping for gravity falsifiers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.