pith. machine review for the scientific record. sign in
def definition def or abbrev

rs_pattern

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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). -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (12)

Lean names referenced from this declaration's body.