ringdownCorrectionValue
plain-language theorem explainer
The ringdown echo amplitude ratio is fixed at φ^{-1}, the one-rung reflection coefficient on the self-similar barrier. GW and strong-field gravity work cites this as the RS prediction for successive echo amplitudes A_{n+1}/A_n. The declaration is a one-line definition equating the correction to the reciprocal of the golden ratio, motivated by the partition 1 = φ^{-1} + φ^{-2}.
Claim. The ringdown correction equals $\varphi^{-1}$, where $\varphi$ is the golden ratio (the self-similar fixed point of the recognition ladder).
background
This module derives φ-powers for five quantum-gravity falsifier channels from the rung address of each observable. A length scale L is assigned rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$, and the recognition correction at that rung scales as $\varphi^{-r}$ relative to the Planck-scale value.
Most channels (PTA, EHT, S-star, Cassini) sit at the strong-field rung $s=44$, the half-area horizon rung that also appears in the baryon asymmetry $\eta_B=\varphi^{-44}$. Ringdown is different: successive echoes sample a single step of the self-similar barrier, so the amplitude ratio is the one-rung reflection coefficient rather than a strong-field injection.
The golden-ratio identity $1=\varphi^{-1}+\varphi^{-2}$ supplies the energy partition between transmitted and reflected pieces at each rung; the reflected amplitude is therefore $\varphi^{-1}$.
proof idea
Pure definitional assignment: the real constant is set equal to $\varphi^{-1}$. No lemmas are applied. Downstream positivity uses inv_pos with phi_pos; the one-rung identity rewrites the same value as $\varphi^{-1}$ in integer-power form via zpow_neg_one.
why it matters
Fills the Ringdown row of the module's channel table (φ-power $\varphi^{-1}$, source: one-rung reflection coefficient), completing the D5 QG falsifier set alongside PTA, EHT, S-star, and Cassini.
Feeds three local consumers: positivity of the correction, the packaged DerivedChannelPrediction record (channel "Ringdown echoes", observable $A_{n+1}/A_n$, rung 1, geometric prefactor 1), and the theorem that the value equals exactly one ladder step $\varphi^{-1}$.
In the broader RS chain this is the local geometric reading of T6 (φ forced as self-similar fixed point): reflection off one rung of the barrier inherits the golden partition rather than the strong-field rung-44 scaling used by the other channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.