rs_pattern

formal source

 197
 198/-- The RS-coherent 8-beat modulation pattern values.
 199    Derived from s(k) = cos(kπ/4) + (1/φ)·cos(kπ/2). -/
 200noncomputable def rs_pattern : Fin 8 → ℝ
 201  | ⟨0, _⟩ => phi
 202  | ⟨1, _⟩ => Real.sqrt 2 / 2
 203  | ⟨2, _⟩ => 1 - phi
 204  | ⟨3, _⟩ => -(Real.sqrt 2 / 2)
 205  | ⟨4, _⟩ => phi - 2
 206  | ⟨5, _⟩ => -(Real.sqrt 2 / 2)
 207  | ⟨6, _⟩ => 1 - phi
 208  | ⟨7, _⟩ => Real.sqrt 2 / 2
 209
 210/-- **8-WINDOW NEUTRALITY**: The RS modulation pattern sums to zero over
 211    one complete 8-beat cycle. This is the fundamental recognition ledger
 212    constraint — the pattern produces no net strain accumulation.
 213
 214    Algebraically: the φ terms cancel (φ + (1-φ) + (φ-2) + (1-φ) = 0)
 215    and the √2/2 terms cancel (alternating signs). -/
 216theorem rs_pattern_window_neutral :
 217    Finset.univ.sum rs_pattern = 0 := by
 218  rw [Finset.sum_fin_eq_sum_range]
 219  simp only [Finset.sum_range_succ, Finset.sum_range_zero, rs_pattern]
 220  rw [dif_pos (show (0 : ℕ) < 8 by omega),
 221      dif_pos (show (1 : ℕ) < 8 by omega),
 222      dif_pos (show (2 : ℕ) < 8 by omega),
 223      dif_pos (show (3 : ℕ) < 8 by omega),
 224      dif_pos (show (4 : ℕ) < 8 by omega),
 225      dif_pos (show (5 : ℕ) < 8 by omega),
 226      dif_pos (show (6 : ℕ) < 8 by omega),
 227      dif_pos (show (7 : ℕ) < 8 by omega)]
 228  ring
 229
 230/-- A window-neutral modulation pattern for an 8-tick cycle. -/