track6FalsifierSensitivityCert
plain-language theorem explainer
Fork F endpoint certificate for Track 6 falsifier sensitivity: packages three theorem-grade discriminator sectors, four rival rows with per-rival distinguishability, dataset and likelihood registers, strong-field structural coverage, and a guarded GWTC-3 ringdown runner. Cited by anyone needing the single Lean-facing Track 6 sensitivity handoff. Construction is a structure instance wiring already-proved inhabited certificates and count lemmas.
Claim. There is a Track 6 falsifier-sensitivity certificate with: three theorem-grade discriminator sectors; four rival rows covered by per-rival distinguishability; a nonempty full discriminator-matrix certificate; a nonempty strong-field structural certificate; nonempty dataset and likelihood registers; likelihood row-coverage arithmetic (likelihood-or-status rows plus dataset-only rows equal total falsifier rows); a nonempty guarded GWTC-3 ringdown runner; and a strictly positive guarded ringdown mapping count.
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: a theorem-grade phi-derived discriminator matrix (Gravity.DiscriminatorMatrix), named dataset/sensitivity attachments for every falsifier-register row, likelihood/status coverage for rows upgraded past dataset-only, and the guarded GWTC-3 ringdown family runner that blocks mixed-family posterior aggregation on the QNM/echo damping path.
The certificate structure demands fixed counts (three independent discriminator sectors; four rival rows) plus inhabited certificates for the matrix, strong-field structural deviation, dataset register, likelihood register, and guarded ringdown runner, together with the arithmetic identity that likelihood-or-status rows plus dataset-only rows exhaust the falsifier register.
Upstream, the full discriminator matrix is inhabited, per-rival distinguishability holds for LQG, string, CDT, and Bohmian rivals via explicit margins (including positive echo-damping ratios), the strong-field structural certificate records a strictly positive RS deviation distinct from pure GR, and the dataset/likelihood registers supply one-statement coverage theorems.
proof idea
Pure structure construction. Each field is filled by an existing lemma or count:
- sector and rival counts come from local numeric defs (
theorem_grade_discriminator_sector_count,rival_rows_covered_count); - discriminator matrix from
discriminatorMatrixFull_inhabited; - per-rival distinguishability wrapped as a proof term from
perRivalDistinguishability_holds; - strong-field, dataset register, likelihood register, and guarded ringdown runner from their respective
*_inhabitedtheorems; - likelihood accounting from
row_coverage_arithmetic(decide on unfolded Nat equalities); - positive guarded ringdown mappings from the local positivity lemma
guarded_ringdown_mapping_count_pos.
No new reasoning; the def is the wiring of already-closed certificates.
why it matters
This is the Fork F endpoint instance for Track 6. Downstream, track6FalsifierSensitivityCert_inhabited is the one-statement handoff theorem asserting Nonempty Track6FalsifierSensitivityCert by packaging this value.
It earns its place by proving Track 6 has a single Lean-facing sensitivity package with named channels and guarded reproducibility surfaces, without claiming empirical confirmation or promoting still-structural PTA / strong-field / ringdown physics into a discovery statement. The discriminator side sits on the phi-derived gravity matrix that separates RS from LQG, string, CDT, and Bohmian rivals; the ringdown side enforces family-guarded GWTC-3 processing so echo-damping posteriors are not mixed across incompatible event families.
Conservatively structural: closes the integration handoff, leaves observational confirmation open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.