ds_mean_difference_pos
plain-language theorem explainer
The pooled mean residual of the DS 1-mode 10M ringdown family exceeds that of the Kerr 220 0M family by a fixed positive amount (~0.143). Anyone citing the three-family mean order DS > Kerr_0M > Kerr_10M needs this inequality. The proof unfolds the numeric difference constant and discharges positivity by norm_num.
Claim. Let $\Delta_{\mathrm{mean}}$ be the difference between the pooled mean residual of the DS 1-mode 10M damping family and that of the Kerr 220 0M family. Then $0 < \Delta_{\mathrm{mean}}$, with $\Delta_{\mathrm{mean}} = 0.143049219914$.
background
The module aggregates three mapped GWTC-3 ringdown damping families: DS 1-mode 10M, Kerr 220 0M, and Kerr 220 10M. It records structural comparison facts only (mean order, median order, and target-inclusion degradation across that order), not an archive-wide mixed-model likelihood. Status is fully closed: zero sorry, zero new RS-specific axioms.
The quantity compared here is the difference of pooled family means. Upstream it is fixed as the concrete real constant $0.143049219914$. Positivity of that constant is the first link in the mean-order chain DS > Kerr_0M > Kerr_10M stated in the module header.
proof idea
One-line numeric discharge. Unfold the definition of the mean-difference constant to the literal real $0.143049219914$, then apply norm_num to obtain $0 < 0.143049219914$. No lemmas beyond the definition and the numeric tactic are required.
why it matters
This is the first half of the mean-order fact advertised by the module: DS 1-mode 10M sits strictly above Kerr 220 0M in pooled mean residual. Together with the sibling Kerr_0M-minus-Kerr_10M positivity, it underwrites the full chain DS > Kerr_0M > Kerr_10M and the parallel median and hit-count orderings. Downstream consumers of the comparison module use that order to document model/start-time dependence of ringdown residuals. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is invoked; the result is pure verification bookkeeping on GWTC-3 controlled families.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.