module module moderate

`IndisputableMonolith.Verification.GWTC3RingdownOneMemberRSStatistic`

Module packaging a single-event RS check of ringdown amplitude scale against the phi-ladder target log(phi^{-44}), using posterior summaries from GWTC-3 member S190727h. Observers comparing LIGO/Virgo ringdown posteriors to Recognition Science amplitude predictions would cite it. Content is mostly named constants and residual/z-score statistics derived from the upstream HDF5 sample summary.

claimFor the GWTC-3 ringdown posterior of event S190727h (one-mode pyring sample), record the RS target $t = \log(\varphi^{-44})$, the posterior mean/median/quantiles of $\log A$, residuals $\log A - t$, a mean-based $z$-score, and the posterior mass above $t$.

background

Recognition Science places dimensionless scales on a $\varphi$-ladder ($\varphi$ the self-similar fixed point forced at T6). Amplitude-scale comparisons are therefore natural in $\log A$ against a fixed rung offset such as $\varphi^{-44}$.

The upstream module GWTC3RingdownHDF5SampleSummary is a structural, sorry-free record of posterior summaries range-read from the GWTC-3 ringdown HDF5 member rin/rin_S190727h_pyring_DS_1mode_10M.h5. This module lifts those summaries into named RS-facing statistics: target, mean, std, median, 5/16/84/95% quantiles, residuals from mean and median, a $z$-score from the mean, and the fraction of posterior mass above the target.

Setting is pure verification bookkeeping: no new forcing-chain step, only a one-member empirical interface between LIGO ringdown posteriors and the RS amplitude target.

proof idea

Definition-and-statistic module rather than a deep proof development. It imports Mathlib and the GWTC-3 HDF5 sample summary, then exposes named constants and derived quantities (target $\log\varphi^{-44}$, posterior moments and quantiles of $\log A$, residuals, $z$-score, fraction above target). Any one-statement theorem in the module is a thin wrapper equating or bounding those named quantities against the upstream summary values; there is no multi-step analytic argument here.

why it matters in Recognition Science

Gives the first concrete, one-member RS amplitude-scale statistic against real GWTC-3 ringdown posterior mass, so later multi-event or catalog-level verification can cite a single closed interface instead of raw HDF5 fields. Downstream use is not yet wired in-tree (no used_by edges). It sits in the Verification domain as empirical closure support, not as a step of the T0–T8 forcing chain. The doc-comment frames it as the one-statement theorem for that one-member RS amplitude-scale statistic; catalog aggregation and cross-event significance remain outside this file.

scope and limits

Does not claim a multi-event or full GWTC-3 catalog test.
Does not re-derive the phi^{-44} rung from the forcing chain.
Does not assert detection significance or model selection against GR.
Does not read raw strain; only uses the upstream HDF5 posterior summary.
Does not cover modes beyond the recorded one-mode pyring sample.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Verification.GWTC3RingdownHDF5SampleSummary module_import

declarations in this module (22)

def rsLogPhiNeg44Target L52
def logAPosteriorMean L53
def logAPosteriorStd L54
def logAPosteriorMedian L55
def logAQ05 L56
def logAQ16 L57
def logAQ84 L58
def logAQ95 L59
def logAResidualFromMean L60
def logAResidualFromMedian L61
def logAZFromMean L62
def logAFractionAboveTarget L63
theorem target_above_q95 L67
theorem target_outside_90_interval L72
theorem target_outside_68_interval L78
theorem z_from_mean_gt_two L84
theorem fraction_above_target_small L89
theorem posterior_summary_available L94
structure GWTC3RingdownOneMemberRSStatisticCert L100
def gwtc3RingdownOneMemberRSStatisticCert L110
theorem gwtc3RingdownOneMemberRSStatisticCert_inhabited L119
theorem gwtc3_ringdown_one_member_rs_statistic_one_statement L124