guarded_ringdown_mapping_count
plain-language theorem explainer
The guarded GWTC-3 ringdown runner exposes exactly two supported observable mappings. Track-6 auditors and anyone citing the Fork F sensitivity certificate use this count as a fixed inventory fact. The proof is definitional reflexivity against the shared runner's supported-mapping constant.
Claim. The number of supported ringdown observable mappings in the guarded GWTC-3 shared runner equals $2$.
background
Track 6 is the falsifier-sensitivity package for Recognition Science gravity discriminators. The module is a structural certificate only: it aggregates already-present Lean surfaces (discriminator matrix, falsifier-register dataset attachments, likelihood/status coverage, and the guarded GWTC-3 ringdown runner) without adding observational lanes or RS-internal hypotheses.
The guarded ringdown runner exists to keep QNM/echo damping posteriors from being mixed across incompatible event families. Its supported mappings are the named observable channels the runner will actually evaluate. The local definition guardedRingdownMappings is just an alias for that runner's supportedMappingCount.
This count theorem freezes that inventory at a concrete natural number so the Fork F handoff can quote a single conjunction of fixed tallies.
proof idea
One-line definitional proof: rfl. Unfolding guardedRingdownMappings yields GWTC3RingdownSharedRunner.supportedMappingCount, which is definitionally equal to 2, so reflexivity closes the goal.
why it matters
Feeds the Fork F handoff theorem track6_falsifier_sensitivity_one_statement, whose doc-comment lists "a guarded GWTC-3 ringdown runner with two supported observable mappings" as one of the six conjuncts of the Track 6 integration endpoint. That parent packages theorem-grade discriminator sectors, rival-row coverage, dataset attachments, likelihood upgrades, ringdown families, and this mapping count into one Lean-facing sensitivity statement for the Quantum Gravity Discovery Master Plan Track 6 path.
The result is deliberately inventory-level: it certifies that the reproducibility surface is finite and named, not that ringdown data confirm RS. It does not promote still-structural PTA, strong-field, or ringdown physics into a discovery claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.