falsifierRowsWithDatasetAttachments
plain-language theorem explainer
Counts how many §7 falsifier-register rows carry named dataset attachments. In the present tree that count equals the full register size, ten. Track 6 sensitivity certificates and the Fork F handoff cite it as the dataset-attachment leg of the package. The body is a one-line alias of the total falsifier-row constant.
Claim. Define $N_{\mathrm{attach}}$ as the number of falsifier-register rows that have named dataset attachments. By definition $N_{\mathrm{attach}}$ equals the total number of $\S 7$ falsifier-register rows (presently $10$).
background
Track 6 is the Fork F integration endpoint in the quantum-gravity master plan. The module packages existing work only: a theorem-grade phi-derived discriminator matrix, named dataset and sensitivity attachments on falsifier-register rows, likelihood or status coverage for rows upgraded past dataset-only status, and a guarded GWTC-3 ringdown runner that blocks mixed-family posterior aggregation.
The falsifier register is the fixed list of observational challenge rows against which Recognition Science gravity claims are scored. Upstream, totalFalsifierRows fixes that list length at ten. Sibling counts track rival-row coverage, likelihood upgrades, and guarded ringdown families. The certificate is structural: it asserts a single Lean-facing sensitivity package with named channels, not empirical confirmation.
proof idea
Definitional one-liner. The value is set equal to the upstream total falsifier-row constant from the likelihood register, so the attachment count is identified with the full register size. No tactics or lemmas; downstream equality theorems discharge by rfl.
why it matters
Supplies the dataset-attachment conjunct in the Fork F handoff. Downstream, Track6SensitivityEndpoint and track6_falsifier_sensitivity_one_statement require this count equal ten, alongside three theorem-grade discriminator sectors, four rival rows covered, six likelihood/status upgrades, and the guarded ringdown family and mapping counts. The local theorem dataset_attachment_row_count records the equality by reflexivity.
In the master-plan framing this closes the "named dataset attachments for all falsifier-register rows" packaging obligation without adding a new observational lane. It does not touch T5–T8 forcing, RCL, or the mass ladder; it only certifies that every register row is dataset-linked inside the verification surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.