dsMeanMinusKerr0Mean
plain-language theorem explainer
Numeric constant equal to the excess of the DS_1mode_10M ringdown-family mean over the Kerr_220_0M mean, fixed at 0.143049219914. Downstream positivity of this gap is the first step in the three-family mean order. The declaration is a bare real literal, not a derived computation.
Claim. Define the real constant $\Delta\bar{m}_{\mathrm{DS}-\mathrm{Kerr0}} := 0.143049219914$, the difference between the pooled mean of the DS one-mode $10M$ damping family and the pooled mean of the Kerr $220$ start-time $0M$ family.
background
The module aggregates three mapped GWTC-3 ringdown damping families: DS one-mode at start time $10M$, Kerr $220$ at $0M$, and Kerr $220$ at $10M$. It records structural comparison facts only (mean order, median order, and target inclusion in pooled 68% and 90% bands), not an archive-wide mixed-model likelihood.
Family means are precomputed offline and injected as concrete reals. This constant is the signed gap between the DS mean and the earlier Kerr mean. Sibling constants play the same role for the Kerr0-versus-Kerr10 gap and for hit-count differences.
Status of the module is a structural theorem package: zero sorry, zero new RS-internal axioms, closed 2026-05-22.
proof idea
No proof. The declaration is a definition that binds a concrete decimal literal of type $\mathbb{R}$. Downstream, positivity is obtained by unfolding the name and running norm_num on the literal.
why it matters
Feeds the theorem ds_mean_difference_pos, which asserts $0 < \Delta\bar{m}_{\mathrm{DS}-\mathrm{Kerr0}}$. That positivity is the first inequality in the module's mean-order chain DS $>$ Kerr0 $>$ Kerr10 (and the parallel median and hit-count orders). The comparison is a controlled three-family check of model and start-time dependence in GWTC-3 ringdown damping, not a claim about the full RS forcing chain (T0–T8) or the mass ladder. It closes a verification ledger entry rather than an open physics derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.