def
definition
sum8
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.Breath1024 on GitHub at line 26.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
23def flipTick : ℕ := 512
24
25/‑ Sliding sum over 8 ticks. -/
26def sum8 (x : T → ℝ) (t0 : T) : ℝ :=
27 (Finset.range period8).sum (fun k => x (t0 + k))
28
29/‑ Eight‑window neutrality predicate. -/
30def neutral8 (x : T → ℝ) (t0 : T) : Prop :=
31 sum8 x t0 = 0
32
33/‑ Oscillator record (display‑level): generative g and radiative r streams
34 over ticks, assumed period‑8 and period‑1024 periodic respectively. -/
35structure Osc where
36 g : T → ℝ
37 r : T → ℝ
38
39/‑ Flip@512 predicate: radiative stream equals generative shifted by 512. -/
40def flipAt512 (O : Osc) : Prop :=
41 ∀ t, O.r (t + flipTick) = O.g t
42
43/‑ Fixed phase‑lag predicate (diagnostic): r leads g by π/4 on each octave.
44 Here represented at the level of a simple sinusoidal probe (display‑only). -/
45def phaseLagPiOver4 (ω : ℝ) (O : Osc) : Prop :=
46 ∀ t : T,
47 O.r t = Real.sin (ω * (t : ℝ) + Real.pi / 4) ∧
48 O.g t = Real.sin (ω * (t : ℝ))
49
50end Breath1024
51end Foundation
52end IndisputableMonolith
53
54
55
56