dsHitDiffVsKerr0
plain-language theorem explainer
Numeric constant recording that the DS 1-mode 10M ringdown family scores ten more target hits than the Kerr 220 0M family in the GWTC-3 controlled comparison. Cited by anyone checking the hit-count ordering among the three mapped damping families. It is a bare natural-number abbreviation, not a derived lemma.
Claim. The hit-count gap between the DS one-mode $10M$ damping family and the Kerr $220$ $0M$ family equals $10$.
background
The module aggregates three GWTC-3 ringdown damping families already mapped elsewhere: DS one-mode at $10M$, Kerr $220$ at $0M$, and Kerr $220$ at $10M$. It records structural comparison facts only (mean order, median order, and target-inclusion degradation), not a mixed-model archive-wide likelihood.
Target inclusion is scored by whether a fixed reference value lands inside the family's pooled 68% and 90% intervals. The module states that inclusion degrades in the same order as the means and medians: DS hits both bands, Kerr $0M$ hits only the 90% band, and Kerr $10M$ hits neither. The present constant is the integer difference of those hit counts between DS and Kerr $0M$.
Sibling constants and theorems package the remaining pairwise gaps and the three-way order statements; all sit in a zero-sorry, zero-new-axiom verification layer.
proof idea
No proof. The declaration is a definitional abbreviation fixing the natural number $10$ as the DS-versus-Kerr-$0M$ hit-count difference. Downstream order lemmas simply unfold or compare against this constant.
why it matters
It freezes the empirical hit gap that the module's hit-count order theorem consumes when it asserts DS outranks Kerr $0M$ on target inclusion. That ordering is one of the three structural claims the GWTC-3 ringdown comparison is built to certify (alongside mean and median order). In the broader Recognition verification stack this is pure observational bookkeeping: it does not invoke the forcing chain, the Recognition Composition Law, or any RS mass or coupling formula. Its value is local reproducibility of the three-family scorecard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.