phasePerRung
plain-language theorem explainer
The recognition phase gained on one φ-ladder rung equals log φ. Black-hole echo and near-horizon barrier work cite it as the fixed round-trip phase step per layer. The definition is the real logarithm of the golden ratio, identical to the scale ratio log(φℓ/ℓ) when the barrier spacing is self-similar at φ.
Claim. The recognition phase accumulated on crossing one rung of the $\varphi$-ladder is $\log\varphi$, i.e. the logarithm of the scale ratio from $\ell$ to $\varphi\ell$.
background
This module treats the near-horizon recognition structure as a $\varphi$-self-similar potential barrier. At each rung the energy splits by the golden-ratio partition $1=\varphi^{-1}+\varphi^{-2}$, equivalent to $\varphi^2=\varphi+1$. The single-rung reflection coefficient is then forced: $|R|^2=\varphi^{-2}$ and $|R|=\varphi^{-1}$.
A "rung" is one step of the discrete $\varphi$-ladder of scales. Crossing from scale $\ell$ to $\varphi\ell$ multiplies lengths by $\varphi$, so the natural phase (log of the scale ratio) is $\log\varphi$. The module uses this constant as the round-trip phase increment that sets echo delay: $\Delta t_{\mathrm{echo}}=(\log\varphi)/(2\pi f_{\mathrm{ringdown}})$ in the narrative, and as $n\cdot\log\varphi$ for the $n$-th echo phase separation in the formal defs.
Upstream, $\varphi$ comes from the RS constants stack; the eight-tick Phase type and fermion rung maps are imported only as ambient RS structure and do not enter the body of this definition.
proof idea
Pure definition: the real is set equal to $\mathrm{Real.log},\varphi$. No proof obligations. Positivity is discharged later by unfolding and applying $\log$-positivity from $\varphi>1$.
why it matters
This constant is the phase yardstick for the echo series. Downstream, echo phase separation is exactly $n$ times this value, and the successor identity is the additive step of one more rung. The positivity lemma records $0<\log\varphi$ for amplitude and delay inequalities.
It feeds the certificate structure that packages the full echo reflection theorem: partition identity, amplitude $|R|=\varphi^{-1}$, geometric ratio $A_{n+1}/A_n=\varphi^{-1}$, and positivity. In the module narrative the round-trip phase per rung is what turns the self-similar barrier into a concrete echo delay law, so the QG echo prediction is a forced consequence of $\varphi$-spacing rather than a fit.
Framework landmarks: T6 forces $\varphi$ as the self-similar fixed point; the barrier scattering matrix is identified with $\varphi^2=\varphi+1$. No open scaffold: the module is marked structural with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.