gwtc3RingdownSharedRunnerCert
plain-language theorem explainer
Packaged certificate that the GWTC-3 ringdown controlled-family damping scripts were refactored onto a shared guarded runner: runner present, script counts match, supported mappings positive, smoke tests pass, and the guarded-family scripts cert is inhabited. Verification engineers auditing the ringdown pipeline cite this. The definition is a structure instance filled from five rfl/decide lemmas plus one upstream inhabited certificate.
Claim. There is a verification certificate asserting that (i) the shared guarded family runner is present, (ii) the refactored family-script count equals the guarded script count, (iii) the supported mapping-label count is positive, (iv) smoke passes after the refactor equal the smoke-test count, and (v) the guarded family scripts certificate is inhabited.
background
This module records a structural refactor that moved GWTC-3 ringdown controlled-family damping scripts onto a shared guarded runner. The runner enforces eligibility checks before posterior bytes are read and exposes two mapping labels: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$). Module status is structural theorem: zero sorry, zero new RS-internal axioms; it adds no physics mapping and computes no posterior likelihood.
The certificate structure bundles five invariants: shared-runner presence, equality of refactored versus guarded script counts, positivity of supported mappings, equality of smoke passes to smoke tests, and availability of the upstream guarded-family-scripts certificate.
Upstream facts are compile-time equalities proved by reflexivity, a positivity fact proved by unfold-and-decide, and the inhabited theorem for the guarded family scripts cert.
proof idea
Structure-instance construction, not a tactic proof. Each field is filled by a named lemma: runner presence, refactored-count equality, and smoke-pass equality are rfl on boolean/Nat constants; mapping-count positivity unfolds the constant and uses decide; guarded-scripts availability is the upstream inhabited theorem packing the guarded-family-scripts certificate.
why it matters
Feeds the one-statement inhabited theorem that GWTC3RingdownSharedRunnerCert is nonempty, the module's master closure for the shared-runner refactor. It sits in the verification layer for GWTC-3 ringdown guarded-family scripts (four listed Python runners/families), recording that the eligibility guard and the two mapping labels survived the move to a shared runner. Not a Recognition Science physics claim (no T0–T8, RCL, mass ladder, or alpha-band content); it is a safety/invariant certificate that script counts, mappings, and smoke tests remain consistent after the refactor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.