theorem
proved
term proof
octave_loop_neutrality
show as:
view Lean formalization →
formal statement (Lean)
112theorem octave_loop_neutrality {S : Type} (L : OctaveLoop S) (flux : S → ℚ) :
113 (∀ n : Fin 8, flux (L.steps n) = if n.val < 4 then 1 else -1) →
114 (Finset.univ.sum (fun i => flux (L.steps i))) = 0 := by
proof body
Term-mode proof.
115 intro h
116 simp only [h]
117 -- Manual expansion over Fin 8
118 rw [Finset.sum_fin_eq_sum_range]
119 repeat' rw [Finset.sum_range_succ]
120 rw [Finset.sum_range_zero]
121 simp
122 norm_num
123
124/-- **THEOREM: Golden Spiral Optimality**
125 The golden spiral (r = φ^(θ/2π)) is the unique continuous geometry
126 that maintains resonance at every point. -/