sharedRunnerPresent
plain-language theorem explainer
Boolean flag fixed to true that records the presence of the shared guarded-family runner for GWTC-3 ringdown damping scripts. Verification authors cite it when assembling the shared-runner certificate and the one-statement closure theorem. The definition is a literal constant assignment, discharged by reflexivity downstream.
Claim. The shared guarded-family runner for GWTC-3 ringdown controlled-family damping scripts is present: the presence flag equals $\mathsf{true}$.
background
This module sits in the Verification domain and records a pure refactor: controlled-family damping scripts for GWTC-3 ringdown analyses were moved onto one shared guarded runner. The runner enforces require_eligible_model(model) before any posterior bytes are read, and exposes two mapping labels only: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$ mapping).
Four Python scripts were refactored onto that runner (the generic guarded-family runner plus three damping-family variants). The module claims no new physics mapping and computes no posterior likelihood; it is a safety and structure invariant with zero sorry and zero new RS-specific axioms.
The present declaration is the Boolean witness that the shared runner exists in the Lean certificate layer. Sibling counts track how many family scripts were refactored, how many mapping labels are supported, and that smoke tests still pass after the move.
proof idea
Literal definition: the Boolean is assigned true. There is no proof body. Downstream, the theorem shared_runner_present discharges equality to true by rfl, and the certificate structure and one-statement theorem simply require that field.
why it matters
The flag is the first field of GWTC3RingdownSharedRunnerCert (runner_present : sharedRunnerPresent = true) and appears in the conjunctive one-statement theorem gwtc3_ringdown_shared_runner_one_statement, which packages runner presence, refactored-script count equality, supported-mapping positivity, smoke-test parity, and certificate inhabitance.
In the Recognition verification stack this is structural bookkeeping, not a physics claim: it locks the refactor that centralized eligibility gating before posterior I/O. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, mass ladders, or the alpha band. Its value is auditability: any later certificate that claims the shared runner is live must route through this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.