track6_falsifier_sensitivity_one_statement
plain-language theorem explainer
Fork F Track 6 integration endpoint: three theorem-grade discriminator sectors, four rival rows covered, ten falsifier rows dataset-attached, six likelihood/status records, three guarded GWTC-3 ringdown families, and two supported observable mappings, plus an inhabited sensitivity certificate. Gravity and verification authors cite it when wiring the master handoff. Proof is a term-mode 7-tuple conjoining six reflexivity count lemmas with certificate inhabitation.
Claim. The following hold simultaneously: there are exactly $3$ theorem-grade discriminator sectors; exactly $4$ rival rows are covered by the discriminator matrix; exactly $10$ falsifier-register rows carry named dataset attachments; exactly $6$ rows have likelihood or status records; exactly $3$ guarded GWTC-3 ringdown families are accepted; exactly $2$ ringdown observable mappings are supported; and the Track 6 falsifier-sensitivity certificate is inhabited.
background
Track 6 is the Fork F integration endpoint of the Quantum Gravity Discovery Master Plan. The module is a structural theorem package: no placeholders and no new RS-internal assumptions. It does not open a new observational lane. It bundles work already in the tree: the theorem-grade phi-derived discriminator matrix, named dataset attachments on every falsifier-register row, likelihood/status coverage for rows upgraded past dataset-only status, and the guarded GWTC-3 ringdown runner that blocks mixed-family posterior aggregation on the QNM/echo damping path.
The certificate structure encodes the handoff requirements: discriminator-sector count $3$, rival-row coverage $4$, a nonempty discriminator-matrix certificate, plus the dataset, likelihood, and ringdown counts. Upstream, each count is a Nat alias into the corresponding register or runner (total falsifier rows, refactored family-script count, supported mapping count) and is discharged by reflexivity. The certificate is intentionally conservative: named channels and guarded reproducibility surfaces only.
proof idea
Pure term-mode conjunction. The proof is the 7-tuple of the six count lemmas plus certificate inhabitation:
theorem_grade_discriminator_sector_countrival_rows_covered_countdataset_attachment_row_countlikelihood_or_status_row_countguarded_ringdown_family_countguarded_ringdown_mapping_counttrack6FalsifierSensitivityCert_inhabited
Each count lemma is itself rfl against its Nat definition (e.g. dataset attachments equal total falsifier rows; ringdown families equal the runner's refactored family-script count; mappings equal the runner's supported-mapping count). The final component supplies Nonempty of the certificate structure whose fields restate those equalities together with the inhabited discriminator-matrix certificate.
why it matters
Single Lean-facing sensitivity package for Track 6 / Fork F. Downstream, track6_sensitivity_endpoint_holds in the master handoff integration is a one-line wrapper that applies this theorem and feeds the integrated certificate covering Forks A–F. The module doc is explicit: the certificate proves only that Track 6 has named channels and guarded reproducibility surfaces. It does not claim empirical confirmation and does not promote still-structural PTA, strong-field, or ringdown physics into a discovery statement. Closes the Fork F handoff requirement without new RS assumptions, packaging the discriminator matrix, falsifier-register datasets, likelihood register, and guarded GWTC-3 ringdown runner into one endpoint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.