hit_count_order
plain-language theorem explainer
Among three GWTC-3 ringdown damping families, the number of catalog members with the target inside the pooled 68% interval rises strictly from Kerr 220 at 10M (0) through Kerr 220 at 0M (3) to DS single-mode 10M (13). Anyone citing the controlled-family comparison certificate or the one-statement ringdown theorem needs this hit-count order. The proof unfolds the three Nat constants and closes by decide.
Claim. Writing $N^{(68)}$ for the number of family members whose target lies inside the pooled 68% interval, one has $N^{(68)}_{\mathrm{Kerr}\,220,\,10M} < N^{(68)}_{\mathrm{Kerr}\,220,\,0M} < N^{(68)}_{\mathrm{DS}\,1\mathrm{mode},\,10M}$.
background
The module aggregates three currently mapped GWTC-3 ringdown damping families: DS single-mode at 10M, Kerr 220 at 0M, and Kerr 220 at 10M. It records model and start-time dependence for means, medians, and target inclusion in pooled intervals, as a three-family comparison only (not an archive-wide mixed-model likelihood).
Each family module exports a natural-number count of members whose target falls inside the pooled 68% interval. Those constants are fixed at 13 (DS 1-mode 10M), 3 (Kerr 220 0M), and 0 (Kerr 220 10M). The present theorem is the strict ordering of those three counts, matching the module's claim that target inclusion degrades along the same family order used for means and medians.
proof idea
Term-mode proof: unfold the three count definitions to the concrete naturals 0, 3, and 13, then close the two strict inequalities by decide. No intermediate lemmas are required beyond the upstream Nat definitions.
why it matters
The hit-count order is one of the structural facts packaged into the controlled-family comparison certificate and into the one-statement theorem that asserts family count, total members, total samples, mean order, and related inequalities together. It makes precise the module claim that target inclusion degrades from DS (target in pooled 68% and 90%) through Kerr 220 0M (90% only) to Kerr 220 10M (neither). Within the Verification domain this is empirical closure on GWTC-3 ringdown families, not a step of the T0–T8 forcing chain; it supplies a machine-checked ordering that downstream certificates can quote without re-deciding the Nat comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.