logAFractionAboveTarget
plain-language theorem explainer
Records the empirical fraction 0.000331 of GWTC-3 ringdown posterior samples whose log-amplitude exceeds the RS structural target log(φ^{-44}). Anyone citing the one-member S190727h amplitude-scale comparison uses this constant. It is a bare numeric definition, not a derived inequality.
Claim. The fraction of posterior samples of $\log A_{t_0}$ lying strictly above the Recognition Science target $\log(\varphi^{-44})$ equals $0.000331$.
background
The module freezes a single GWTC-3 ringdown posterior: member rin_S190727h_pyring_DS_1mode_10M.h5, dataset /EXP6/posterior_samples, column logA_t_0. The RS structural amplitude target is $\log(\varphi^{-44})\approx -21.17332$. Sibling constants fix the posterior mean ($\approx -22.245$), std ($\approx 0.398$), median, and quantile endpoints.
Relative to that mean the target sits about $2.69\sigma$ high, outside the central 68% and 90% intervals. The present definition stores the raw sample fraction above the target, the most direct empirical tail weight in the one-member comparison. The module is a structural verification record only: zero sorry, zero new RS axioms, and no claim that $\log A_{t_0}$ is the final echo observable.
proof idea
Pure definition: the real constant is set equal to the decimal $0.000331$ taken from the range-read posterior table. No lemma is applied; downstream proofs simply unfold the name and discharge numeric goals with norm_num.
why it matters
Supplies the tail-fraction atom for the one-member RS amplitude statistic. Downstream, fraction_above_target_small proves the constant is strictly less than $0.001$, and the bundled one-statement theorem conjoins that bound with the $z>2$ residual and the certificate that the target lies above Q95 and outside the 68%/90% intervals. In the broader Verification layer this is the first explicitly RS-referenced numeric on a GWTC-3 ringdown table; it does not yet close an archive-wide likelihood, but it pins the single-event tail weight that any such likelihood would have to reproduce.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.