echoPhaseSeparation_succ
plain-language theorem explainer
Accumulated echo phase after n+1 φ-rungs equals the phase after n rungs plus one fixed per-rung phase. Anyone building multi-echo delay trains from the near-horizon φ-barrier cites this recurrence. The proof is a three-tactic algebraic identity from the linear definition of the phase accumulator.
Claim. For every natural number $n$, the accumulated echo phase separation after $n+1$ rungs equals the accumulated phase separation after $n$ rungs plus the fixed phase contributed by one rung.
background
The module models the near-horizon recognition structure as a φ-self-similar potential barrier: rung boundaries sit at scales $\ell_n = \ell_0 \cdot \varphi^n$, and each boundary shares the same reflection coefficient by self-similarity. Energy splits by the golden-ratio partition $1 = \varphi^{-1} + \varphi^{-2}$, so a single-rung reflection coefficient is $|R|^2 = \varphi^{-2}$.
Echo delay is tied to phase. The definition echoPhaseSeparation packages total phase after $n$ rungs as the real number $n$ times a fixed phasePerRung (the round-trip phase across one φ-rung, identified in the module narrative with $\log\varphi$ per crossing). The physical delay is then $\Delta t_{\mathrm{echo}} = \mathrm{phasePerRung}/(\pi, f_{\mathrm{ring}})$ times the echo index.
This successor lemma is the discrete additivity statement for that linear accumulator: each extra rung contributes exactly one more copy of the per-rung phase.
proof idea
One short tactic proof. Unfold the definition of the phase accumulator (which is literally $n\cdot\mathrm{phasePerRung}$), push natural-number arithmetic into the reals, and finish by ring. No external lemmas are required; the identity is $(n+1)p = np + p$ in $\mathbb{R}$.
why it matters
The module's structural claim is that GW echo trains are forced by φ-self-similarity, not fitted: amplitude $\varphi^{-n}$ and delay $n\cdot\Delta t_{\mathrm{echo}}$ both come from the same rung ladder. This successor identity is the inductive step that makes total phase (hence total delay) strictly proportional to echo index.
It sits under the Gravity domain's echo-reflection development and supports the narrative that the QG-paper echo prediction is a consequence of the substrate's golden-ratio spacing (linked to T6 φ-forcing and the φ-ladder mass/scale structure). No downstream theorems currently depend on it in the graph; it is local infrastructure for the barrier-phase section.
It does not itself force the value of the per-rung phase or the ringdown frequency; those enter from the surrounding definitions and the eight-tick / φ landmarks of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.