ringdownCorrectionValue_pos
plain-language theorem explainer
The ringdown echo amplitude ratio equals φ^{-1} and is strictly positive. Anyone citing the ringdown channel prediction or the golden-ratio energy partition needs this positivity fact. The proof is a one-line application of positivity of the reciprocal once φ > 0 is known.
Claim. The ringdown correction value $\varphi^{-1}$ is strictly positive: $0 < \varphi^{-1}$.
background
This module assigns each quantum-gravity falsifier channel a correction at a definite $\varphi$-power, read off the rung address of the observable. The recognition substrate maps a length $L$ to rung $r(L)=\log_\varphi(L/\ell_{\mathrm{sub}})$, and the correction at that rung scales as $\varphi^{-r}$.
For ringdown echoes the relevant scale is a single self-similar barrier rung. The correction is defined as $\mathrm{ringdownCorrectionValue}:=\varphi^{-1}$, the one-rung reflection coefficient. That coefficient comes from the golden-ratio energy partition $1=\varphi^{-1}+\varphi^{-2}$ (equivalent to $\varphi^2=\varphi+1$): at each rung boundary, energy splits into a reflected share $\varphi^{-1}$ and a transmitted share $\varphi^{-2}$.
Positivity of every channel correction is recorded in a short block of lemmas; this is the ringdown instance. Upstream, $\varphi>0$ is a standard constant fact in the RS constants layer.
proof idea
Term-mode one-liner. The definition unfolds to $\varphi^{-1}$, so the goal is $0<\varphi^{-1}$. Apply inv_pos.mpr to reduce to $\varphi>0$, then discharge with phi_pos. No further algebraic work.
why it matters
Feeds ringdownDerived, which packages the ringdown channel as a DerivedChannelPrediction with observable "echo amplitude ratio $A_{n+1}/A_n$", rung $1$, geometric prefactor $1$, and this correction value. Without positivity the derived prediction record would not be a well-formed positive scale factor.
In the channel table, ringdown is the outlier that sits at $\varphi^{-1}$ rather than at the strong-field rung $44$ used by PTA, EHT, S-star, and Cassini. That $\varphi^{-1}$ is the Berry-scale reflection coefficient from the golden-ratio partition, tying the GW echo amplitude ratio directly to the self-similar fixed point forced at T6. The lemma closes the positivity side-condition for that structural claim inside a 0-sorry module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.