guarded_ringdown_mapping_count_pos
plain-language theorem explainer
The number of guarded GWTC-3 ringdown mappings is strictly positive. Anyone assembling the Track 6 falsifier-sensitivity certificate cites this to show the ringdown channel is inhabited, not an empty stub. The proof unfolds the local count alias and hands off to the shared runner's positivity lemma.
Claim. The cardinality of the guarded GWTC-3 ringdown mapping set is strictly positive: $0 < N_{\mathrm{map}}^{\mathrm{guarded}}$.
background
Track 6 is the Fork F integration endpoint for falsifier sensitivity in the Quantum Gravity Discovery Master Plan. It does not open a new observational lane; it packages existing Lean surfaces: the theorem-grade phi-derived discriminator matrix, named dataset and likelihood attachments on falsifier-register rows, and the guarded GWTC-3 ringdown family runner.
The ringdown runner is the QNM/echo damping path. "Guarded" means families are kept separate so posteriors are never mixed across incompatible ringdown families. The local symbol guardedRingdownMappings is the count of supported mappings exposed by that runner; positivity of the count is the minimal inhabitance check that the certificate demands before claiming a reproducibility surface exists.
Upstream status strings (RS-native units, discrete Lichnerowicz axis-sector convergence, four-tet signed deficit) sit in the broader gravity stack but are not used in the proof body; they only locate the module inside the structural gravity tree.
proof idea
One-line reduction. Unfold the local definition of the guarded mapping count, then apply GWTC3RingdownSharedRunner.supported_mapping_count_pos, which already proves the shared runner exposes a positive number of supported mappings. No arithmetic or case split is performed here.
why it matters
Feeds the Fork F endpoint certificate track6FalsifierSensitivityCert, whose fields are exactly the integration-lane handoff requirements: theorem-grade discriminators, per-rival matrix coverage, dataset attachments, likelihood/status coverage, and guarded GWTC-3 ringdown processing. Without a positive mapping count, the ringdown slot of that certificate would be empty.
The module is intentionally conservative: it proves Track 6 has a single Lean-facing sensitivity package with named channels and guarded reproducibility surfaces. It does not claim empirical confirmation and does not upgrade still-structural PTA, strong-field, or ringdown physics into a discovery statement. In the Recognition stack this is verification scaffolding around gravity discriminators, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.