Track6FalsifierSensitivityCert
plain-language theorem explainer
Certificate record packaging Fork F Track 6 falsifier-sensitivity handoff: three theorem-grade discriminator sectors, four rival rows with per-rival distinguishability, inhabited matrix and strong-field certs, dataset and likelihood registers with closed row accounting, and a family-guarded GWTC-3 ringdown runner with positive mappings. Master-handoff consumers cite it as the single Lean-facing Track 6 sensitivity package. As a structure it only states field obligations; a separate instance proves inhabitation.
Claim. A Track 6 falsifier-sensitivity certificate is a record asserting: exactly three theorem-grade discriminator sectors; exactly four rival rows covered; a nonempty discriminator-matrix certificate and a nonempty per-rival distinguishability certificate; a nonempty strong-field structural $\phi$-deviation certificate; a nonempty falsifier dataset-register certificate; a nonempty likelihood/status-register certificate; the identity that likelihood/status rows plus dataset-only rows equal total falsifier rows; a nonempty family-guarded GWTC-3 ringdown runner certificate; and a strictly positive count of guarded ringdown observable mappings.
background
Track 6 is the Fork F integration endpoint in the quantum-gravity discovery master plan. This module does not open a new observational lane. It packages work already in the tree: a theorem-grade $\phi$-derived discriminator matrix, named dataset and sensitivity attachments for every falsifier-register row, likelihood or status coverage for rows upgraded past dataset-only status, and a guarded GWTC-3 ringdown family runner that blocks mixed-family posterior aggregation on the QNM/echo damping path.
The certificate is intentionally conservative. Module status is structural theorem: no placeholder proofs and no new RS-internal assumptions. It proves only that Track 6 exposes one Lean-facing sensitivity package with named channels and guarded reproducibility surfaces. It does not claim empirical confirmation, and it does not promote still-structural PTA, strong-field, or ringdown physics into a discovery statement.
Sibling counters fix the numeric targets: three theorem-grade discriminator sectors, four rival rows covered, ten dataset-attached falsifier rows, six likelihood/status rows, three guarded ringdown families, and a positive mapping count.
proof idea
No proof body: this is a structure definition. Each field is a Prop obligation (equality of a named counter, Nonempty of an upstream certificate type, or a closed arithmetic identity on likelihood-register row counts). Downstream, a single instance fills every field by citing the corresponding count lemmas and inhabited certificates (full discriminator matrix, per-rival distinguishability, strong-field structural, dataset register, likelihood register, guarded GWTC-3 runner). Nonemptiness of the structure is then the one-line constructor wrapping that instance.
why it matters
This is the Lean-facing Fork F Track 6 package. Downstream, the master handoff defines the Track 6 sensitivity endpoint as the conjunction of the same numeric and coverage facts, and the module exports both an inhabited instance and the one-statement handoff theorem summarizing three discriminator sectors, four rival rows, ten dataset attachments, six likelihood/status records, three guarded ringdown families, and positive mappings.
In the Recognition framework it sits on the verification side of gravity discrimination: $\phi$-derived theorem-grade sectors and a full rival matrix give structural distinguishability against alternative gravity stories, while dataset and likelihood registers plus the family-guarded GWTC-3 runner supply named, reproducible sensitivity surfaces. It does not touch the T0–T8 forcing chain directly; it certifies that Track 6 falsifier and ringdown infrastructure is packaged for integration without upgrading structural physics to empirical discovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.