supported_mapping_count_pos
plain-language theorem explainer
The shared GWTC-3 ringdown runner exposes a strictly positive number of supported mapping labels. Verification and Track-6 sensitivity certificates cite this to guarantee the mapping catalogue is non-empty after the guarded-family refactor. The proof unfolds the constant count to 2 and closes by decidable arithmetic.
Claim. The number of supported ringdown mapping labels on the shared guarded runner is strictly positive: $0 < N_{\mathrm{map}}$, where $N_{\mathrm{map}} = 2$ counts the labels $\texttt{direct}$ (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and $\texttt{kerr220}$ (Kerr 220 $Q(a)$ mapping).
background
This module records a structural refactor of GWTC-3 ringdown controlled-family damping scripts onto one shared guarded runner. The runner calls require_eligible_model(model) before any posterior bytes are read and advertises exactly two mapping labels: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 quality-factor mapping). The module states explicitly that this is a safety invariant only: no new physics mapping and no posterior likelihood is computed.
The quantity supportedMappingCount is the hard-coded natural number 2 equal to that label catalogue. Downstream certificates package several such invariants (runner present, refactored script count, smoke tests, guarded-script availability) into a single inhabited certificate record.
proof idea
Term-mode proof in two steps: unfold the definition supportedMappingCount (which is the literal Nat value 2), then decide discharges $0 < 2$ by the decidable order on naturals. No lemmas beyond definitional unfolding are required.
why it matters
Feeds the shared-runner certificate field mapping_count_pos inside gwtc3RingdownSharedRunnerCert, so the inhabited certificate cannot be assembled unless the mapping catalogue is non-empty. Also re-exported by Track-6 falsifier sensitivity as guarded_ringdown_mapping_count_pos, which unfolds guardedRingdownMappings and applies this theorem verbatim. Together these close the structural side of the GWTC-3 ringdown guarded-family refactor (status: structural theorem, zero sorry, zero RS-internal axioms). It does not touch the RS forcing chain (T0–T8), RCL, or mass ladder; it only locks the verification harness that those physics claims may later ride on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.