supportedMappingCount
plain-language theorem explainer
Records that the shared GWTC-3 ringdown guarded runner exposes exactly two observable-mapping labels. Verification and Track-6 sensitivity code cite this constant when packing the shared-runner certificate and when counting supported mappings. The body is a literal natural-number definition equal to two.
Claim. The number of supported ringdown observable mappings exposed by the shared guarded family runner is $2$.
background
The module freezes a refactor of GWTC-3 ringdown controlled-family damping scripts onto one shared guarded runner. That runner calls require_eligible_model before any posterior bytes are read and advertises two mapping labels only: direct (damped-sinusoid $f_{t_0}/\tau_{t_0}$) and kerr220 (Kerr 220 quality-factor map $Q(a)$).
This constant is the Lean-side count of those labels. The module is a structural safety invariant: it adds no new physics mapping and computes no likelihood. Sibling counts track how many family scripts were refactored and whether post-refactor smoke tests still pass.
proof idea
Definitional constant: the body is the numeral 2. Downstream positivity is discharged by unfolding and decide.
why it matters
Feeds the shared-runner certificate field requiring a positive mapping count, the one-statement conjunction that pins the count at two, and the Track-6 falsifier-sensitivity alias guardedRingdownMappings. Together these close the structural claim that the refactor preserved exactly the two documented mapping channels without inventing new ones. Landmark relevance is verification hygiene only (GWTC-3 ringdown pipeline), not the T0–T8 forcing chain or mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.