refactoredFamilyScriptCount
plain-language theorem explainer
Pins the number of GWTC-3 ringdown controlled-family damping scripts moved onto the shared guarded runner at three. Verification and Track-6 sensitivity code cite it as the canonical family count. The body is a bare natural-number literal, equated by reflexivity to the guarded-script count.
Claim. The number of refactored GWTC-3 ringdown controlled-family damping scripts on the shared guarded runner is $3$.
background
The module records a structural refactor of GWTC-3 ringdown verification: controlled-family damping scripts were moved onto one shared guarded runner. That runner calls an eligibility gate before any posterior bytes are read and exposes two mapping labels only: direct damped-sinusoid frequencies and timescales, and Kerr-220 quality-factor mapping. The module states explicitly that this is a safety invariant, not a new physics map and not a likelihood computation.
The three scripts counted here are the damped-sinusoid family and the two Kerr-220 damping families listed in the module header. A sibling constant in the guarded-family-scripts import holds the parallel guarded count; a reflexivity theorem asserts the two counts agree.
proof idea
Definitional constant: the natural number is set to the literal $3$. No tactics, no lemmas. Downstream equality with the guarded-script count is discharged by rfl in a sibling theorem.
why it matters
Gives the certificate structure and the one-statement shared-runner theorem a fixed family cardinality to assert. The certificate requires this count to equal the guarded-script count; the one-statement theorem packages that equality with runner presence, two supported mappings, and smoke-test passage. Track-6 falsifier sensitivity re-exports the same number as the current mapped ringdown-family count accepted by the guarded runner. In the Recognition verification stack this is bookkeeping closure for the GWTC-3 ringdown path, not a forcing-chain or mass-ladder step: it locks the refactor inventory so later sensitivity claims cannot silently drop or add families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.