refactored_count_matches_guarded_count
plain-language theorem explainer
The refactored controlled-family script inventory has the same cardinality as the guarded-family inventory: both equal three. Verification authors cite this when assembling the GWTC-3 ringdown shared-runner certificate after the damping-family refactor. The proof is pure definitional equality by reflexivity.
Claim. The number of refactored GWTC-3 ringdown family scripts equals the number of guarded family scripts (both are $3$).
background
This module records a structural refactor of GWTC-3 ringdown controlled-family damping scripts onto a shared guarded runner. The runner requires model eligibility before any posterior bytes are read and exposes two mapping labels: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$). It adds no new physics mapping and computes no likelihood.
Upstream, guardedScriptCount is the constant natural $3$ counting the guarded-family scripts, and refactoredFamilyScriptCount is likewise the constant $3$ counting the scripts moved onto the shared runner. Equality of those two counts is the inventory invariant checked here.
proof idea
Both sides reduce definitionally to the numeral $3$. The proof is a one-line rfl establishing definitional equality; no lemmas or tactics beyond reflexivity are used.
why it matters
The equality is a field of the shared-runner certificate bundle gwtc3RingdownSharedRunnerCert, which packages runner presence, matching script counts, positive supported-mapping count, post-refactor smoke passes, and availability of the guarded-family scripts certificate. It closes the inventory half of the refactor safety invariant (status: structural theorem, zero sorry, zero new RS axioms). It does not touch the forcing chain (T0–T8), RCL, or mass ladder; it is pure verification bookkeeping for the GWTC-3 ringdown pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.