noncomputable def FUST.EulerOperator.ζ₁₂ : ℂ

Primitive 12th root of unity: ζ₁₂ = e^{iπ/6} = (√3/2 + i/2)

Equations

• FUST.EulerOperator.ζ₁₂ = { re := √3 / 2, im := 1 / 2 }

theorem FUST.EulerOperator.zeta12_sq : ζ₁₂ ^ 2 = ζ₆

ζ₁₂² = ζ₆

theorem FUST.EulerOperator.zeta12_pow_six : ζ₁₂ ^ 6 = -1

ζ₁₂⁶ = -1

theorem FUST.EulerOperator.zeta12_pow_twelve : ζ₁₂ ^ 12 = 1

ζ₁₂¹² = 1

theorem FUST.EulerOperator.zeta12_cubed : ζ₁₂ ^ 3 = Complex.I

ζ₁₂³ = i

noncomputable def FUST.EulerOperator.N12 (f : ℂ → ℂ) (z : ℂ) : ℂ

N12: 12-point alternating sum at 12th roots of unity. Extracts DFT mode 6: detects n ≡ 6 mod 12.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def FUST.EulerOperator.D12 (f : ℂ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.EulerOperator.D12 f z = FUST.EulerOperator.N12 f z / 12

theorem FUST.EulerOperator.N12_const (c z : ℂ) : N12 (fun (x : ℂ) => c) z = 0

N12 annihilates constants

theorem FUST.EulerOperator.N12_ker_one (z : ℂ) : N12 (fun (w : ℂ) => w ^ 1) z = 0

theorem FUST.EulerOperator.N12_ker_two (z : ℂ) : N12 (fun (w : ℂ) => w ^ 2) z = 0

theorem FUST.EulerOperator.N12_ker_three (z : ℂ) : N12 (fun (w : ℂ) => w ^ 3) z = 0

N12 annihilates z³ (mode 3 is invisible to D₁₂)

theorem FUST.EulerOperator.N12_ker_four (z : ℂ) : N12 (fun (w : ℂ) => w ^ 4) z = 0

theorem FUST.EulerOperator.N12_ker_five (z : ℂ) : N12 (fun (w : ℂ) => w ^ 5) z = 0

theorem FUST.EulerOperator.N12_detects_six (z : ℂ) : N12 (fun (w : ℂ) => w ^ 6) z = 12 * z ^ 6

N12[z⁶] = 12z⁶

theorem FUST.EulerOperator.D12_sixth (z : ℂ) : D12 (fun (w : ℂ) => w ^ 6) z = z ^ 6

D12[z⁶] = z⁶

theorem FUST.EulerOperator.D12_detects_sixth (z : ℂ) (hz : z ≠ 0) : D12 (fun (w : ℂ) => w ^ 6) z ≠ 0

D₁₂ detects z⁶

noncomputable def FUST.EulerOperator.euler (f : ℂ → ℂ) (z : ℂ) : ℂ

Euler operator θ = z·d/dz: the unique complete detector (ker = {constants}). θ[z^n] = n·z^n.

Equations

• FUST.EulerOperator.euler f z = z * deriv f z

theorem FUST.EulerOperator.euler_monomial (n : ℕ) (z : ℂ) : euler (fun (w : ℂ) => w ^ n) z = ↑n * z ^ n

θ[z^n] = n·z^n

theorem FUST.EulerOperator.euler_const (c z : ℂ) : euler (fun (x : ℂ) => c) z = 0

θ[c] = 0

theorem FUST.EulerOperator.euler_linear (z : ℂ) : euler id z = z

θ[z] = z

theorem FUST.EulerOperator.euler_detects (n : ℕ) (hn : 1 ≤ n) (z : ℂ) (hz : z ≠ 0) : euler (fun (w : ℂ) => w ^ n) z ≠ 0

θ detects all n ≥ 1: ker(θ) = {constants}

theorem FUST.EulerOperator.euler_finer_than_D12 : euler (fun (w : ℂ) => w ^ 3) 1 ≠ 0 ∧ N12 (fun (w : ℂ) => w ^ 3) 1 = 0

θ is strictly finer than D₁₂

noncomputable def FUST.EulerOperator.standardDeriv (f : ℂ → ℂ) (z : ℂ) : ℂ

Standard derivative recovered from Euler: d/dz = θ/z

Equations

• FUST.EulerOperator.standardDeriv f z = FUST.EulerOperator.euler f z / z

theorem FUST.EulerOperator.standardDeriv_monomial (n : ℕ) (z : ℂ) (hz : z ≠ 0) : standardDeriv (fun (w : ℂ) => w ^ n) z = ↑n * z ^ (n - 1)

θ/z agrees with d/dz on monomials: n·z^{n-1}

theorem FUST.EulerOperator.standardDeriv_eq_deriv_monomial (n : ℕ) (z : ℂ) (hz : z ≠ 0) : standardDeriv (fun (w : ℂ) => w ^ n) z = deriv (fun (w : ℂ) => w ^ n) z

θ/z = deriv for monomials (matching Mathlib's deriv)

theorem FUST.EulerOperator.standardDeriv_const (c z : ℂ) : standardDeriv (fun (x : ℂ) => c) z = 0

θ/z on constants: d/dz[c] = 0

theorem FUST.EulerOperator.standardDeriv_id (z : ℂ) (hz : z ≠ 0) : standardDeriv id z = 1

θ/z on z: d/dz[z] = 1

theorem FUST.EulerOperator.standardDeriv_sq (z : ℂ) (hz : z ≠ 0) : standardDeriv (fun (w : ℂ) => w ^ 2) z = 2 * z

θ/z on z²: d/dz[z²] = 2z

theorem FUST.EulerOperator.standardDeriv_cube (z : ℂ) (hz : z ≠ 0) : standardDeriv (fun (w : ℂ) => w ^ 3) z = 3 * z ^ 2

θ/z on z³: d/dz[z³] = 3z²

theorem FUST.EulerOperator.standardDeriv_sq_twice (z : ℂ) (hz : z ≠ 0) : standardDeriv (fun (w : ℂ) => 2 * w) z = 2

d²/dz²[z²] = 2 from θ: d/dz(2z) = 2

theorem FUST.EulerOperator.standardDeriv_cube_twice (z : ℂ) (hz : z ≠ 0) : standardDeriv (fun (w : ℂ) => 3 * w ^ 2) z = 6 * z

d²/dz²[z³] = 6z from θ: d/dz(3z²) = 6z