rsLogPhiNeg44Target
plain-language theorem explainer
Defines the fixed real constant log(φ^{-44}) ≈ -21.17332 as the Recognition Science amplitude-scale target for one GWTC-3 ringdown posterior. Verification theorems compare the S190727h logA_t_0 posterior against this number. The body is a bare decimal literal, not a derived computation.
Claim. The RS ringdown amplitude target is the real number $\log(\varphi^{-44}) \approx -21.173320302623$, where $\varphi$ is the golden ratio.
background
This module freezes a one-member comparison between an LIGO/Virgo GWTC-3 ringdown posterior and a Recognition Science amplitude scale. The member is rin_S190727h_pyring_DS_1mode_10M.h5, column logA_t_0 from /EXP6/posterior_samples.
In RS units the natural dimensionless scales sit on the $\varphi$-ladder. The structural target used here is $\log(\varphi^{-44}) = -44\log\varphi$. The decimal is the numerical stand-in for that exact expression; sibling defs hold the posterior mean, std, median, and quantiles of the same column.
The module is labeled a structural theorem package (zero sorry, no new RS axioms). It records only an amplitude-scale comparison for this single event, not an archive-wide likelihood or a claim that logA_t_0 is the final RS echo observable.
proof idea
No proof. The declaration is a definition equal to the decimal literal $-21.173320302623$. Downstream comparison lemmas unfold this name and the corresponding quantile constants, then discharge the inequalities by norm_num (or linarith after the q95 strict inequality).
why it matters
This constant is the RS reference point for every certified comparison in the module. It appears in target_above_q95, target_outside_90_interval, and target_outside_68_interval, which together populate the certificate structure GWTC3RingdownOneMemberRSStatisticCert and the one-statement theorem gwtc3_ringdown_one_member_rs_statistic_one_statement.
Those results state that the target lies above the posterior 95% quantile, outside the central 90% and 68% intervals, more than two posterior standard deviations above the mean, with sample fraction above target below $0.001$. The rung $-44$ is an RS $\varphi$-ladder amplitude scale; the module does not yet derive why rung 44 is forced for this observable, only that this numerical target sits where the posterior does not.
It is the first explicitly RS-referenced statistic on a range-read GWTC-3 ringdown table in the verification layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.