kerr_mean_difference_pos
plain-language theorem explainer
The mean residual of the Kerr 220 0M damping family exceeds that of Kerr 220 10M by a fixed positive constant. Anyone citing the three-family GWTC-3 mean order uses this inequality as the Kerr-to-Kerr step. The proof unfolds the numeric difference and discharges positivity by exact rational arithmetic.
Claim. Let $\Delta_{\mathrm{Kerr}}$ be the difference between the pooled mean residual of the Kerr $220$ start-at-$0M$ family and that of the Kerr $220$ start-at-$10M$ family. Then $0 < \Delta_{\mathrm{Kerr}}$, with the concrete value $\Delta_{\mathrm{Kerr}} = 0.089478304903$.
background
The module compares three controlled GWTC-3 ringdown damping families: a single-mode dynamical-spacetime family started at $10M$, and two Kerr $220$ families started at $0M$ and $10M$. The comparison is structural only: it orders means, medians, and target-inclusion bands across those three families, not a mixed-model archive likelihood.
The quantity compared here is the difference of the two Kerr family means. Upstream it is fixed as the real constant $0.089478304903$. Sibling facts establish the parallel DS-versus-Kerr mean gap and the corresponding median and hit-count orders. Together they support the module claim that mean residuals satisfy DS $>$ Kerr $0M$ $>$ Kerr $10M$.
proof idea
One-line numeric discharge. Unfold the definition of the Kerr mean difference to the literal real $0.089478304903$, then apply norm_num to prove strict positivity. No lemmas beyond the definition are required.
why it matters
Closes the Kerr-to-Kerr half of the mean-order chain in the GWTC-3 ringdown controlled-family comparison. The module status is a structural theorem with zero sorry and zero new RS-internal axioms; this inequality is one of the elementary positivity facts that make the published order DS $>$ Kerr $0M$ $>$ Kerr $10M$ machine-checkable. Downstream siblings (family_mean_order and related hit/median facts) assemble the full three-family statement. It does not touch the Recognition forcing chain (T0–T8) or the mass ladder; it is verification infrastructure for ringdown model dependence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.