gwtc3_ringdown_shared_runner_one_statement
plain-language theorem explainer
Bundles five audit facts about the GWTC-3 ringdown shared guarded-family runner into one conjunction: the runner flag is on, three family scripts were refactored, two mapping labels are supported, post-refactor smoke tests all pass, and the master certificate type is inhabited. Verification engineers cite it as the single entry point for the refactor safety invariant. The proof is a five-component term pairing named boolean lemmas with two definitional equalities and the inhabitedness witness.
Claim. The shared guarded-family runner is present, the count of refactored family scripts equals $3$, the count of supported mapping labels equals $2$, the number of smoke tests that pass after the refactor equals the total number of smoke tests, and the master shared-runner certificate structure is inhabited (nonempty).
background
This module sits in the Verification layer and records a pure refactor: controlled-family damping scripts for GWTC-3 ringdown were moved onto one shared guarded runner. The runner must call require_eligible_model before any posterior bytes are read. It exposes two mapping labels only: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$). Module status is structural: zero sorry, zero new RS-internal axioms, and no new physics mapping or likelihood evaluation.
Named constants in the signature are definitional. The shared-runner presence flag is the boolean true. The refactored family-script count is the natural number $3$. Smoke-pass equality is the identity that every post-refactor smoke test succeeded. The certificate structure packages those facts together with a positive mapping count and nonemptyness of the upstream guarded-family-scripts certificate.
Upstream lemmas already discharge the atomic claims: presence is rfl on the boolean constant, smoke equality is rfl on matching Nat constants, and inhabitedness of the certificate is witnessed by an explicit structure value.
proof idea
Term-mode five-fold conjunction. First component is the lemma that the shared-runner presence flag equals true (itself rfl). Second and third components are bare rfl on the Nat definitions for refactored script count ($=3$) and supported mapping count ($=2$). Fourth component is the lemma that smoke passes equal smoke tests after refactor (again rfl). Fifth component is the inhabitedness theorem for the master certificate structure, which wraps the explicit certificate value. No tactics, no rewriting beyond definitional equality.
why it matters
Closes the shared-runner refactor as a single auditable statement. Downstream consumers (none linked yet in the graph) can import one theorem instead of five atomic facts when asserting that the GWTC-3 ringdown guarded-family stack still enforces eligibility before posterior I/O. The module doc frames this as a safety invariant only: it does not touch the Recognition forcing chain (T0–T8), the J-cost or RCL, mass ladders, or the alpha band. Its value is engineering hygiene inside the verification mirror: after moving four Python family scripts onto one runner, Lean records that the counts, flags, and smoke suite still line up and that the certificate type remains inhabited. That keeps the 2026-05-22 structural closure honest without claiming new physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.