phasePerRung_pos
plain-language theorem explainer
The recognition phase accumulated per rung equals log φ and is strictly positive. Anyone deriving black-hole echo delays from the φ-self-similar barrier cites this positivity. The proof unfolds the definition and applies the standard fact that log is positive on arguments greater than one, using φ > 1.
Claim. The recognition phase per rung, defined by $\mathrm{phasePerRung} := \log\varphi$, satisfies $0 < \log\varphi$. Equivalently, the scale-ratio phase accumulated when crossing from length $\ell$ to $\varphi\ell$ is strictly positive.
background
In the echo-reflection module the near-horizon recognition structure is a φ-self-similar potential barrier. Energy at each rung splits by the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$, so the single-rung reflection coefficient is $|R|^2 = \varphi^{-2}$.
The phase accumulated on one rung crossing is the logarithm of the scale ratio: going from $\ell$ to $\varphi\ell$ contributes $\log(\varphi\ell/\ell) = \log\varphi$. That quantity is packaged as phasePerRung. Echo $n$ then arrives with amplitude $\varphi^{-n}$ and delay $n\cdot\Delta t_{\mathrm{echo}}$, where $\Delta t_{\mathrm{echo}}$ is proportional to this phase divided by the ringdown frequency.
The only upstream fact needed here is $\varphi > 1$ (forced already by the self-similar fixed-point step of the forcing chain), which makes the real logarithm strictly positive.
proof idea
One-line term proof. Unfold phasePerRung to expose $\log\varphi$, then apply Real.log_pos to the hypothesis $\varphi > 1$. No further algebraic manipulation.
why it matters
Positivity of the per-rung phase is a tiny but necessary certificate inside the echo package. Downstream, echoReflectionCoefficientCert assembles the full structural claim: golden-ratio energy partition, reflection amplitude $\varphi^{-1}$, constant echo ratio, and positive amplitude. Without $0 < \log\varphi$ the delay formula $\Delta t_{\mathrm{echo}} = (\log\varphi)/(\pi f_{\mathrm{ring}})$ would not be a well-defined positive time.
Framework-wise this sits on T6 (φ forced as the self-similar fixed point) and on the module thesis that the QG-paper echo prediction is not dimensional analysis but a forced consequence of φ-spacing. The same log-φ phase appears in the eight-tick octave story whenever a rung crossing is treated as a discrete scale step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.