phi_inv_eq

formal source

 143    mechanism 8 φ = 1  -- Some function of 8 ticks and φ gives threshold 1
 144
 145/-- 1/φ = φ - 1 (golden ratio reciprocal property) -/
 146theorem phi_inv_eq : 1/φ = φ - 1 := Inequalities.phi_inv
 147
 148/-- 1/φ is positive -/
 149theorem phi_inv_pos : 1/φ > 0 := by
 150  have := phi_pos
 151  exact one_div_pos.mpr phi_pos
 152
 153/-- |1/φ| < 1, so the geometric series converges -/
 154theorem phi_inv_lt_one : 1/φ < 1 := by
 155  have h := phi_gt_one
 156  have hp := phi_pos
 157  rw [div_lt_one hp]
 158  linarith
 159
 160/-- The sum φ^(-1) + φ^(-2) + ... converges to φ -/
 161theorem phi_series_sum : ∑' (n : ℕ), (1/φ)^(n+1) = φ := by
 162  -- This is the geometric series: ∑_{n≥0} r^(n+1) = r/(1-r) for |r| < 1
 163  -- With r = 1/φ, we get (1/φ)/(1 - 1/φ) = 1/(φ-1) = φ (since 1/φ = φ-1)
 164  have h_inv_pos := phi_inv_pos
 165  have h_inv_lt_one := phi_inv_lt_one
 166  have h_phi_pos := phi_pos
 167  have h_phi_gt_one := phi_gt_one
 168  -- Rewrite the sum as r * geom_series(r) = r/(1-r)
 169  have h_eq : ∑' (n : ℕ), (1/φ)^(n+1) = (1/φ) * ∑' (n : ℕ), (1/φ)^n := by
 170    rw [← tsum_mul_left]
 171    congr 1
 172    ext n
 173    ring
 174  rw [h_eq]
 175  -- Use the geometric series formula: ∑ r^n = 1/(1-r)
 176  have h_nonneg : 0 ≤ 1/φ := le_of_lt h_inv_pos