shared_runner_present
plain-language theorem explainer
Records that the shared guarded-family runner flag is present (equal to true) after the GWTC-3 ringdown script refactor. Verification authors cite it when assembling the shared-runner certificate bundle. The proof is reflexivity on a Boolean definition fixed to true.
Claim. The Boolean flag asserting that the shared guarded-family runner is present equals $\mathrm{true}$.
background
This module is a structural verification layer for the GWTC-3 ringdown pipeline. It documents a refactor that moved controlled-family damping scripts onto one shared guarded runner. The runner must call require_eligible_model(model) before any posterior bytes are read, and it exposes two mapping labels: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 $Q(a)$ mapping).
The Boolean sharedRunnerPresent is hard-coded to true in this module. It is not a physics claim: the module states explicitly that the refactor adds no new physics mapping and computes no posterior likelihood. Sibling counters track refactored script count, supported mapping count, and post-refactor smoke-test pass status.
proof idea
One-line rfl proof. The definition sharedRunnerPresent is the constant Boolean true, so equality to true holds by definitional reflexivity. No lemmas are invoked.
why it matters
Feeds the certificate structure gwtc3RingdownSharedRunnerCert, which packs this flag with the refactored-count match, positive mapping count, smoke-pass equality, and inhabited guarded-scripts certificate. Also appears as the first conjunct of gwtc3_ringdown_shared_runner_one_statement, the one-statement shared-runner theorem.
In the Recognition verification stack this is a safety invariant only: it locks in that the shared runner is present after the controlled-family damping scripts were consolidated. It does not touch the forcing chain (T0–T8), RCL, mass ladder, or $\alpha$ band. Closure note in the module: zero sorry, zero new RS-internal axioms (dated 2026-05-22).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.