track6FalsifierSensitivityCert_inhabited
plain-language theorem explainer
The Track 6 falsifier-sensitivity certificate type is inhabited: a single Lean package bundles three theorem-grade discriminator sectors, four rival-row coverages, full dataset attachments, likelihood/status upgrades, and a guarded GWTC-3 ringdown runner. Verification and gravity auditors cite it as the Fork F integration endpoint. The proof is a one-line witness: the prebuilt certificate term.
Claim. There exists a Track 6 falsifier-sensitivity certificate: three theorem-grade discriminator sectors, four rival rows with per-rival distinguishability, a nonempty $4\times 3$ discriminator matrix, all ten falsifier-register rows dataset-attached, six rows with likelihood or status records, and a guarded GWTC-3 ringdown runner with supported observable mappings.
background
Track 6 is the Fork F integration lane in the Quantum Gravity Discovery Master Plan. This module does not open a new observational channel. It packages work already in the tree: the phi-derived discriminator matrix (Gravity.DiscriminatorMatrix), named dataset and sensitivity attachments for every falsifier-register row, likelihood/status coverage for rows upgraded past dataset-only status, and the guarded GWTC-3 ringdown family runner that blocks mixed-family posterior aggregation on the QNM/echo damping path.
The certificate structure encodes exactly those handoff requirements as equality and Nonempty fields (sector count equals 3, rival rows covered equals 4, matrix certificate inhabited, and the corresponding dataset, likelihood, and ringdown counts). The module status is structural theorem: no placeholder proofs and no new RS-internal assumptions. Upstream scaffolding includes RS-native units ($c=1$, $\hbar=\varphi^{-5}$), Clifford/8-tick structure, and stable trace-predicate combinators used elsewhere in the verification stack; they are ambient context, not local hypotheses of this inhabitation claim.
proof idea
Term-mode one-liner. The proof supplies the already-constructed certificate value as the witness for Nonempty, via anonymous constructor syntax. No tactics, no case splits, and no additional lemmas are invoked at the inhabitation site; all field equalities and nested Nonempty obligations were discharged when that certificate term was built from the sibling count lemmas and upstream matrix/register/runner certificates.
why it matters
This is the inhabitation hinge for Fork F Track 6. Downstream, the one-statement handoff theorem unpacks the certificate into the explicit conjunction: three theorem-grade discriminator sectors, four rival rows covered, ten dataset-attached falsifier rows, six likelihood/status rows, three guarded ringdown families, and two supported observable mappings. That handoff is the single Lean-facing sensitivity package for Track 6.
In the broader Recognition framework it sits on the verification side of gravity discrimination (phi-ladder discriminators, rival coverage), not on the T0–T8 forcing chain itself. It deliberately stops short of empirical confirmation and does not promote still-structural PTA, strong-field, or ringdown physics into a discovery claim. Its role is reproducibility packaging: named channels and guarded runners so later observational work has a fixed Lean endpoint to cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.