Track6SensitivityEndpoint
plain-language theorem explainer
Fork F's handoff predicate: Track 6 packages theorem-grade discriminator coverage (3 sectors), four rival-theory rows, ten dataset-attached falsifier rows, six likelihood/status upgrades, and a guarded GWTC-3 ringdown runner (3 families, 2 mappings) into one certificate. Gravity integration cites it as the Track-6 sensitivity endpoint. It is a pure Prop abbreviation, not a proved theorem.
Claim. The Track-6 sensitivity endpoint holds when the theorem-grade discriminator sector count equals $3$, rival-theory rows covered equal $4$, falsifier rows with named dataset attachments equal $10$, rows with likelihood or status records equal $6$, guarded GWTC-3 ringdown families equal $3$, guarded ringdown observable mappings equal $2$, and the Track-6 falsifier-sensitivity certificate is inhabited.
background
Module context is Gravity Track 7 fork-handoff integration: parallel receipts for Forks A–F that record what each endpoint proves without upgrading the discovery claim. Fork F is the Track-6 falsifier-sensitivity package.
Upstream counts are fixed Nat constants from the Track-6 register: rival rows cover LQG, string, CDT/causal sets, and Bohmian/Diósi–Penrose (exactly four); falsifier rows with dataset attachments equal the register total; likelihood/status rows upgrade beyond dataset-only status; guarded ringdown families and mappings come from the shared GWTC-3 runner (refactoredFamilyScriptCount, supportedMappingCount). Discriminator sectors are the theorem-grade sector tally required by the sensitivity lane.
The endpoint is the Prop that those inventory equalities hold and that a Track6FalsifierSensitivityCert witness exists. Sibling endpoints (Track-2 many-body, Track-1 Schläfli reductions, etc.) play the same role for other forks.
proof idea
Definitional packaging only: the declaration is a Prop abbreviation, a seven-way conjunction of six numeric inventory equalities plus Nonempty of the Track-6 falsifier-sensitivity certificate. No tactics or lemmas fire here. The inhabited certificate and the count equalities are discharged later by track6_sensitivity_endpoint_holds, which reduces to the one-statement Track-6 falsifier-sensitivity theorem.
why it matters
Fork F's integration-lane receipt. Downstream, track6_sensitivity_endpoint_holds asserts the Prop; ForkHandoffIntegrationCert stores it as a field; and both fork_A_C_F_handoffs_integrated_one_statement and the full fork_A_B_C_D_E_F_handoffs_integrated_one_statement conjoin it with the other fork endpoints and the structural master certificate.
Per the module doc, Track 7 "records exactly what the new endpoints prove" and does not assert the unconditional discovery theorem. This endpoint therefore closes the sensitivity-packaging handoff (rival coverage, dataset attachments, GWTC-3 ringdown guards) while leaving Track-1 displacement-class leaves and full master closure open. It is the falsifier-sensitivity counterpart to the many-body and Schläfli reduction endpoints in the same integration structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.