guardedRingdownFamilies
plain-language theorem explainer
Counts the currently mapped GWTC-3 ringdown families accepted by the guarded shared runner. The value is the runner's refactored family-script count, fixed at three. Track 6 sensitivity and Fork F handoff theorems cite it as the ringdown-guard leg of the certificate. The definition is a one-line alias of that upstream Nat.
Claim. Let $N_{\mathrm{rd}}$ be the number of currently mapped GWTC-3 ringdown families accepted by the guarded shared runner. Then $N_{\mathrm{rd}}$ equals the runner's refactored family-script count (presently $3$).
background
Track 6 is the Fork F integration endpoint in the Quantum Gravity Discovery Master Plan. This module packages existing work only: a theorem-grade phi-derived discriminator matrix, named dataset and likelihood attachments on falsifier-register rows, and a guarded GWTC-3 ringdown family runner. The certificate is structural; it does not claim empirical confirmation or upgrade still-structural PTA, strong-field, or ringdown physics into a discovery statement.
The guarded runner exists to block mixed-family posterior aggregation on the QNM/echo damping path. Upstream, refactoredFamilyScriptCount is the Nat fixed at 3 that enumerates the supported family scripts in that runner. This definition re-exports that count under the Track 6 certificate's naming.
proof idea
One-line definitional alias: the Nat is definitionally equal to GWTC3RingdownSharedRunner.refactoredFamilyScriptCount, itself the literal 3. No tactics or lemmas; downstream equalities discharge by rfl.
why it matters
Supplies the ringdown-guard conjunct in the Fork F handoff. Downstream, Track6SensitivityEndpoint and track6_falsifier_sensitivity_one_statement require guardedRingdownFamilies = 3 alongside three theorem-grade discriminator sectors, four rival rows covered, ten dataset-attached falsifier rows, and six likelihood/status rows. The sibling theorem guarded_ringdown_family_count pins the equality by reflexivity.
In the master-plan framing this is the Lean-facing reproducibility surface for GWTC-3 ringdown families, not a physics derivation of QNM spectra. It sits in Verification, not in the T0–T8 forcing chain; its role is certificate packaging so Track 6 can be cited as a single sensitivity endpoint with named, guarded channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.