GWTC3RingdownSharedRunnerCert
plain-language theorem explainer
Certificate bundle for the GWTC-3 ringdown shared guarded-family runner refactor. It packages five Boolean/Nat equalities: runner present, refactored script count equals guarded count (both 3), positive supported-mapping count, post-refactor smoke passes equal tests, and the guarded-scripts certificate is inhabited. Verification and Track-6 authors cite it as the typed handoff for the safety refactor. Definitional structure only; witnesses live in the inhabited instance.
Claim. A certificate record asserting five facts: the shared runner flag equals true; the refactored family-script count equals the guarded script count; the supported mapping count is strictly positive; the number of smoke passes after the refactor equals the number of smoke tests; and the guarded family-scripts certificate type is inhabited.
background
This module sits in the GWTC-3 ringdown verification lane. It records a pure engineering refactor: controlled-family damping scripts were moved onto one shared guarded runner that calls require_eligible_model(model) before any posterior bytes are read. Supported mapping labels are direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$). The module states explicitly that this adds no new physics mapping and computes no posterior likelihood.
Upstream constants pin the arithmetic: shared runner present is the Boolean true; both the refactored family-script count and the guarded script count equal 3; smoke passes and smoke tests after refactor both equal 7. The sibling guarded-scripts certificate already requires that the guarded count match the eligible-model count and that all smoke checks pass. The present structure simply demands that certificate be inhabited, so the shared-runner lane cannot close without the guarded-family lane.
proof idea
No proof body: this is a structure (certificate type) whose fields are propositions. Inhabitation is discharged downstream by gwtc3RingdownSharedRunnerCert, which fills each field from the corresponding lemma (shared_runner_present, refactored_count_matches_guarded_count, supported_mapping_count_pos, smoke_after_refactor_all_passed, and the inhabited guarded-scripts certificate). Those lemmas are themselves one-line reductions of the Nat/Bool defs above.
why it matters
Closes the shared-runner safety invariant for GWTC-3 ringdown family scripts (module status: structural theorem, 0 sorry, closure 2026-05-22). Downstream, gwtc3RingdownSharedRunnerCert builds a concrete value; gwtc3RingdownSharedRunnerCert_inhabited and gwtc3_ringdown_shared_runner_one_statement collapse the five fields into a single Nonempty/conjunction claim. Track 6 falsifier sensitivity imports this certificate under "guarded GWTC-3 ringdown processing," so the fork-F handoff cannot claim guarded ringdown coverage without this refactor bundle. It is verification scaffolding, not a forcing-chain (T0–T8) physics step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.