kerr0HitDiffVsKerr10
plain-language theorem explainer
The integer gap between target-hit counts for the Kerr 220 start-at-0M family and the Kerr 220 start-at-10M family is fixed at 3. Anyone citing the ordered degradation of GWTC-3 ringdown target inclusion across start times uses this constant. It is a bare numeric definition, not a derived theorem.
Claim. The difference in target-inclusion hit counts between the Kerr$_{220}$ damping family started at $0M$ and the same family started at $10M$ equals $3$.
background
The module compares three controlled GWTC-3 ringdown damping families already mapped elsewhere: a single-mode dynamical-spacetime family at $10M$, and two Kerr $220$ families started at $0M$ and at $10M$. The comparison is structural only (means, medians, and pooled target-inclusion hits), not an archive-wide mixed-model likelihood.
Target inclusion is scored by whether a fixed RS target lands inside the family's pooled 68% and 90% intervals. The module records that inclusion degrades in the same order as the means and medians: the DS family hits both bands, Kerr $0M$ hits only the 90% band, and Kerr $10M$ hits neither. Sibling constants record the pairwise hit-count gaps that quantify that degradation.
proof idea
No proof. The declaration is a one-line numeric abbreviation binding the name to the literal natural number 3, placed among the ordering-fact constants that feed the later hit-count order lemmas.
why it matters
It pins the Kerr-start-time half of the hit-count ladder used by the module's ordering facts (mean order, median order, and hit-count order). Together with the DS-versus-Kerr0 gap, it makes the three-family degradation claim fully numeric and machine-checkable without reopening the underlying family tables. The module is marked structural closure (zero sorry, zero new RS axioms) and deliberately stops short of a full GWTC-3 likelihood; this constant is part of that narrow, auditable comparison layer rather than a physics derivation from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.