Pith. sign in
def

dsPooledZFromMean

definition
show as:
module
IndisputableMonolith.Verification.GWTC3RingdownDS1Mode10MDampingFamily
domain
Verification
line
65 · github
papers citing
none yet

plain-language theorem explainer

Records the pooled z-score of the DS_1mode_10M family mean damping-per-cycle relative to the RS target 1/φ, fixed at the numerical value 0.138989. Citation target for anyone checking that the controlled-family mean sits well under one standard deviation from the Recognition prediction. Pure numeric definition; no proof obligations.

Claim. The pooled $z$-score of the family mean damping-per-cycle against the RS target is the real constant $0.138989$, i.e. $z = |\bar{d} - \varphi^{-1}| / \sigma$ for the DS\_1mode\_10M pooled posterior.

background

This module freezes a controlled-family scaling of the GWTC-3 ringdown damping statistic for the single model class DS_1mode_10M: 22 HDF5 files, 22 events, and 643624 pooled posterior samples. The observable is damping per cycle, $d = \exp(-1/(f_{t_0}\tau_{t_0}))$.

Recognition Science predicts a universal damping target at the Berry threshold $\varphi^{-1}\approx 0.618034$. Empirically the pooled mean is $0.581258$ with pooled standard deviation $0.264599$. The quantity defined here is the absolute $z$-score of that mean relative to the RS target, a dimensionless distance used downstream to assert that the mean lies well inside one sigma.

Sibling constants in the same file fix the pooled mean, std, median, and quantile ladder; this entry is only the derived mean-to-target $z$.

proof idea

There is no proof. The declaration is a bare real definition equal to the precomputed constant $0.138989$. Downstream theorems simply unfold it and discharge numeric comparisons with norm_num.

why it matters

Feeds three local consumers: the inequality proving the pooled $z$ is strictly less than one; the family certificate structure that packages taxonomy counts, positivity, and interval containment; and the one-statement controlled-family damping theorem that asserts member/event/sample counts together with the RS target lying inside both the pooled 90% and 68% intervals.

In the broader Recognition picture the target $\varphi^{-1}$ is the Berry creation threshold from the forcing chain. A sub-unity $z$ on a single-model, non-mixed GWTC-3 ringdown family is structural evidence that the observed damping-per-cycle distribution is consistent with that threshold, without claiming a full archive likelihood or cross-model combination.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.