phi_series_sum
plain-language theorem explainer
The infinite sum of successive powers of the reciprocal golden ratio equals the golden ratio. Workers on self-similar fixed points in Recognition Science cite the identity when closing the emergence argument from J-cost. The proof rewrites the tail sum, invokes the geometric-series closed form under the bound 1/φ < 1, and reduces the resulting expression via the relation φ(φ − 1) = 1.
Claim. $∑_{n=0}^∞ φ^{-(n+1)} = φ$
background
The φ-Emergence module derives the golden ratio from J-cost minimization under the Recognition Composition Law. Here φ denotes the unique positive number satisfying φ² = φ + 1, equivalently the self-similar fixed point of the map r ↦ 1 + 1/r. Upstream lemmas establish that φ is self-similar (phi_is_self_similar) and that φ − 1 = 1/φ (phi_inv_eq). The series arises naturally when summing costs or frequencies along the phi-ladder in the forcing chain from T0 to T8.
proof idea
The tactic proof first factors the sum as (1/φ) times the full geometric series via tsum_mul_left. It then applies tsum_geometric_of_lt_one using the non-negativity and strict inequality 1/φ < 1 supplied by phi_inv_pos and phi_inv_lt_one. The resulting expression (1/φ) / (1 − 1/φ) is reduced by field_simp together with the identity φ(φ − 1) = 1 extracted from phi_is_self_similar via linarith.
why it matters
The identity supplies the concrete summation step that recovers φ from its own inverse powers, confirming the fixed-point property required by T6 of the forcing chain. It supports the subsequent discussion of stable positions in the same module, where J-cost is locally minimized precisely when the ratio satisfies the self-similar equation. No downstream uses are recorded, yet the result closes an algebraic loop inside the phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.