noncomputable def FUST.DζOperator.Diff2 (f : ℂ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.DζOperator.Diff2 f z = f (↑FUST.φ * z) - f (↑FUST.ψ * z)

noncomputable def FUST.DζOperator.Diff3 (f : ℂ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.DζOperator.Diff3 f z = f (↑FUST.φ * z) - 2 * f z + f (↑FUST.ψ * z)

noncomputable def FUST.DζOperator.Diff4 (f : ℂ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.DζOperator.Diff4 f z = f (↑FUST.φ ^ 2 * z) - ↑FUST.φ ^ 2 * f (↑FUST.φ * z) + ↑FUST.ψ ^ 2 * f (↑FUST.ψ * z) - f (↑FUST.ψ ^ 2 * z)

noncomputable def FUST.DζOperator.Diff5 (f : ℂ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.DζOperator.Diff5 f z = f (↑FUST.φ ^ 2 * z) + f (↑FUST.φ * z) - 4 * f z + f (↑FUST.ψ * z) + f (↑FUST.ψ ^ 2 * z)

noncomputable def FUST.DζOperator.Diff6 (f : ℂ → ℂ) (z : ℂ) : ℂ

Equations

• FUST.DζOperator.Diff6 f z = f (↑FUST.φ ^ 3 * z) - 3 * f (↑FUST.φ ^ 2 * z) + f (↑FUST.φ * z) - f (↑FUST.ψ * z) + 3 * f (↑FUST.ψ ^ 2 * z) - f (↑FUST.ψ ^ 3 * z)

Numerator Coefficient Uniqueness

Diff5 general numerator: f(φ²z) - a·f(φz) + b·f(z) - a·f(ψz) + f(ψ²z) Diff6 general numerator: f(φ³z) - A·f(φ²z) + B·f(φz) - B·f(ψz) + A·f(ψ²z) - f(ψ³z)

The coefficients are uniquely determined by the kernel conditions.

noncomputable def FUST.DζOperator.Diff5_general (a b : ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ

Diff5 general numerator with parameters (a, b)

Equations

• FUST.DζOperator.Diff5_general a b f z = f (↑FUST.φ ^ 2 * z) - a * f (↑FUST.φ * z) + b * f z - a * f (↑FUST.ψ * z) + f (↑FUST.ψ ^ 2 * z)

noncomputable def FUST.DζOperator.Diff6_general (A B : ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ

Diff6 general numerator with parameters (A, B)

Equations

• FUST.DζOperator.Diff6_general A B f z = f (↑FUST.φ ^ 3 * z) - A * f (↑FUST.φ ^ 2 * z) + B * f (↑FUST.φ * z) - B * f (↑FUST.ψ * z) + A * f (↑FUST.ψ ^ 2 * z) - f (↑FUST.ψ ^ 3 * z)

theorem FUST.DζOperator.Diff5_C0_condition (a b : ℂ) : (∀ (z : ℂ), Diff5_general a b (fun (x : ℂ) => 1) z = 0) ↔ b = 2 * a - 2

Condition C0: Diff5[1] = 0 iff 2 - 2a + b = 0

theorem FUST.DζOperator.Diff5_C1_condition (a b : ℂ) : (∀ (z : ℂ), Diff5_general a b id z = 0) ↔ b = a - 3

Condition C1: Diff5[id] = 0 iff (φ² + ψ²) - a(φ + ψ) + b = 0

theorem FUST.DζOperator.Diff5_coefficients_unique (a b : ℂ) : (∀ (z : ℂ), Diff5_general a b (fun (x : ℂ) => 1) z = 0) → (∀ (z : ℂ), Diff5_general a b id z = 0) → a = -1 ∧ b = -4

Diff5 coefficient uniqueness: Diff5[1] = 0 and Diff5[id] = 0 determine a = -1, b = -4

theorem FUST.DζOperator.Diff5_general_eq_Diff5 (f : ℂ → ℂ) (z : ℂ) : Diff5_general (-1) (-4) f z = Diff5 f z

Diff5_general with determined coefficients equals Diff5

theorem FUST.DζOperator.Diff6_D1_condition (A B : ℂ) : (∀ (z : ℂ), Diff6_general A B id z = 0) ↔ B = A - 2

Condition D1: Diff6[id] = 0 iff F₃ - A·F₂ + B·F₁ = 0, i.e., 2 - A + B = 0

theorem FUST.DζOperator.Diff6_D2_condition (A B : ℂ) : (∀ (z : ℂ), Diff6_general A B (fun (t : ℂ) => t ^ 2) z = 0) ↔ B = 3 * A - 8

Condition D2: Diff6[x²] = 0 iff F₆ - A·F₄ + B·F₂ = 0, i.e., 8 - 3A + B = 0

theorem FUST.DζOperator.Diff6_coefficients_unique (A B : ℂ) : (∀ (z : ℂ), Diff6_general A B id z = 0) → (∀ (z : ℂ), Diff6_general A B (fun (t : ℂ) => t ^ 2) z = 0) → A = 3 ∧ B = 1

Diff6 coefficient uniqueness: Diff6[id] = 0 and Diff6[x²] = 0 determine A = 3, B = 1

theorem FUST.DζOperator.Diff6_general_eq_Diff6 (f : ℂ → ℂ) (z : ℂ) : Diff6_general 3 1 f z = Diff6 f z

Diff6_general with determined coefficients equals Diff6

theorem FUST.DζOperator.FUST_coefficient_uniqueness : (∀ (a b : ℂ), (∀ (z : ℂ), Diff5_general a b (fun (x : ℂ) => 1) z = 0) → (∀ (z : ℂ), Diff5_general a b id z = 0) → a = -1 ∧ b = -4) ∧ ∀ (A B : ℂ), (∀ (z : ℂ), Diff6_general A B id z = 0) → (∀ (z : ℂ), Diff6_general A B (fun (t : ℂ) => t ^ 2) z = 0) → A = 3 ∧ B = 1

Complete coefficient uniqueness for Diff5 and Diff6

noncomputable def FUST.DζOperator.halfOrderParam : ℂ

Half-order mixing parameter: λ = 2/(φ + 2) = 2/(φ² + 1) ≈ 0.5528

Equations

• FUST.DζOperator.halfOrderParam = 2 / (↑FUST.φ + 2)

theorem FUST.DζOperator.halfOrderParam_alt : halfOrderParam = 2 / (↑φ ^ 2 + 1)

Alternative form: λ = 2/(φ² + 1)

theorem FUST.DζOperator.halfOrderParam_uniqueness : halfOrderParam * (↑φ ^ 2 + 1) = 2

Uniqueness condition: halfOrderParam satisfies μ·(φ² + 1) = 2

theorem FUST.DζOperator.halfOrderParam_unique_from_condition (μ : ℂ) (h : μ * (↑φ ^ 2 + 1) = 2) : μ = halfOrderParam

If μ·(φ² + 1) = 2, then μ = halfOrderParam

Diff7 Algebraic Reduction to Diff6

Diff7 antisymmetric numerator form: [1, -a, b, -c, +c, -b, +a, -1] Diff7(a,b,c)f = f(φ⁴z) - a·f(φ³z) + b·f(φ²z) - c·f(φz) + c·f(ψz) - b·f(ψ²z) + a·f(ψ³z) - f(ψ⁴z)

Key result: ker(Diff7) = ker(Diff6) implies Diff7 provides no new structure.

noncomputable def FUST.DζOperator.Diff7_general (a b c : ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ

Diff7 general antisymmetric numerator with parameters (a, b, c)

Equations

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

theorem FUST.DζOperator.Diff7_E0_condition (a b c z : ℂ) : Diff7_general a b c (fun (x : ℂ) => 1) z = 0

Condition E0: Diff7[1] = 0 holds for antisymmetric form (coefficient sum = 0)

theorem FUST.DζOperator.Diff7_E1_condition (a b c : ℂ) : (∀ (z : ℂ), Diff7_general a b c id z = 0) ↔ 3 - 2 * a + b - c = 0

Condition E1: Diff7[id] = 0 iff 3 - 2a + b - c = 0 (using Fibonacci: F₄ = 3, F₃ = 2, F₂ = 1, F₁ = 1)

theorem FUST.DζOperator.Diff7_E2_condition (a b c : ℂ) : (∀ (z : ℂ), Diff7_general a b c (fun (t : ℂ) => t ^ 2) z = 0) ↔ 21 - 8 * a + 3 * b - c = 0

Condition E2: Diff7[x²] = 0 iff F₈ - a·F₆ + b·F₄ - c·F₂ = 21 - 8a + 3b - c = 0

theorem FUST.DζOperator.Diff7_coefficients_constrained (a b c : ℂ) : (∀ (z : ℂ), Diff7_general a b c id z = 0) → (∀ (z : ℂ), Diff7_general a b c (fun (t : ℂ) => t ^ 2) z = 0) → c = a - 6 ∧ b = 3 * a - 9

Diff7 coefficient constraint: E1 and E2 imply c = a - 6, b = 3a - 9 (1 free parameter)

noncomputable def FUST.DζOperator.Diff7_constrained (a : ℂ) (f : ℂ → ℂ) (z : ℂ) : ℂ

Diff7 with constrained coefficients: a arbitrary, b = 3a - 9, c = a - 6

Equations

• FUST.DζOperator.Diff7_constrained a f z = FUST.DζOperator.Diff7_general a (3 * a - 9) (a - 6) f z

theorem FUST.DζOperator.Diff7_constrained_const (a k z : ℂ) : Diff7_constrained a (fun (x : ℂ) => k) z = 0

Diff7_constrained annihilates constants

theorem FUST.DζOperator.Diff7_constrained_linear (a z : ℂ) : Diff7_constrained a id z = 0

Diff7_constrained annihilates linear functions

theorem FUST.DζOperator.Diff7_constrained_quadratic (a z : ℂ) : Diff7_constrained a (fun (t : ℂ) => t ^ 2) z = 0

Diff7_constrained annihilates quadratic functions

theorem FUST.DζOperator.Diff7_kernel_equals_Diff6_kernel (a : ℂ) : (∀ (c z : ℂ), Diff7_constrained a (fun (x : ℂ) => c) z = 0) ∧ (∀ (z : ℂ), Diff7_constrained a id z = 0) ∧ ∀ (z : ℂ), Diff7_constrained a (fun (t : ℂ) => t ^ 2) z = 0

ker(Diff7) = ker(Diff6): Diff7 annihilates {1, z, z²} (same as Diff6 kernel)

ζ₆ convolution filters: AFNum and SymNum

Anti-Fibonacci sequence: C_n = C_{n-1} - C_{n-2}, C_0=0, C_1=1. Period 6: [0, 1, 1, 0, -1, -1]. Recurrence mirrors ζ₆²=ζ₆-1.

AFNum: antisymmetric filter with coefficients C_k = [0,1,1,0,-1,-1] SymNum: symmetric filter with coefficients 2Re(ζ₆^k) = [2,1,-1,-2,-1,1]

For s ≡ 1 mod 6: AFNum selects AF_coeff = 2i√3, SymNum selects 6. For s ≡ 5 mod 6: AFNum selects -AF_coeff, SymNum selects 6. For s ≡ 0,2,3,4 mod 6: both filters annihilate.

noncomputable def FUST.DζOperator.AFNum (g : ℂ → ℂ) (z : ℂ) : ℂ

Anti-Fibonacci numerator: Σ C_k · g(ζ₆^k · z) for C_k = [0,1,1,0,-1,-1]

Equations

• FUST.DζOperator.AFNum g z = g (FUST.ζ₆ * z) + g (FUST.ζ₆ ^ 2 * z) - g (FUST.ζ₆ ^ 4 * z) - g (FUST.ζ₆ ^ 5 * z)

noncomputable def FUST.DζOperator.SymNum (g : ℂ → ℂ) (z : ℂ) : ℂ

Symmetric 6-point: Σ 2Re(ζ₆^k) · g(ζ₆^k · z), coefficients [2,1,-1,-2,-1,1]

Equations

• FUST.DζOperator.SymNum g z = 2 * g z + g (FUST.ζ₆ * z) - g (FUST.ζ₆ ^ 2 * z) - 2 * g (FUST.ζ₆ ^ 3 * z) - g (FUST.ζ₆ ^ 4 * z) + g (FUST.ζ₆ ^ 5 * z)

theorem FUST.DζOperator.AFNum_const (c z : ℂ) : AFNum (fun (x : ℂ) => c) z = 0

AFNum annihilates constant functions

theorem FUST.DζOperator.SymNum_const (c z : ℂ) : SymNum (fun (x : ℂ) => c) z = 0

SymNum annihilates constant functions

theorem FUST.DζOperator.AFNum_add (f g : ℂ → ℂ) (z : ℂ) : AFNum (fun (w : ℂ) => f w + g w) z = AFNum f z + AFNum g z

AFNum is additive: AFNum(f+g) = AFNum(f) + AFNum(g)

theorem FUST.DζOperator.SymNum_add (f g : ℂ → ℂ) (z : ℂ) : SymNum (fun (w : ℂ) => f w + g w) z = SymNum f z + SymNum g z

SymNum is additive: SymNum(f+g) = SymNum(f) + SymNum(g)

Dζ operator

Rank-2 operator on ⟨φ,ζ₆⟩ ≅ ℤ × ℤ/6ℤ. C(a,k) = AF_k·Φ_A(a) + SY_k·Φ_S(a) where: Φ_A = Diff6 + Diff2 - Diff4: antisymmetric channel Φ_S = 2·Diff5 + Diff3 + μ·Diff2: symmetric channel, μ = 2/(φ+2) Half-period: C(a, k+3) = -C(a, k) from AF/SY anti-periodicity.

noncomputable def FUST.DζOperator.Φ_A (f : ℂ → ℂ) (z : ℂ) : ℂ

Φ_A: φ-numerator = Diff6 + Diff2 - Diff4, all 6 ops AF channel

Equations

• FUST.DζOperator.Φ_A f z = FUST.DζOperator.Diff6 f z + FUST.DζOperator.Diff2 f z - FUST.DζOperator.Diff4 f z

noncomputable def FUST.DζOperator.Φ_S (f : ℂ → ℂ) (z : ℂ) : ℂ

Φ_S: φ-numerator = 2·Diff5 + Diff3 + μ·Diff2, all 6 ops SY channel

Equations

• FUST.DζOperator.Φ_S f z = 2 * FUST.DζOperator.Diff5 f z + FUST.DζOperator.Diff3 f z + 2 / (↑FUST.φ + 2) * FUST.DζOperator.Diff2 f z

noncomputable def FUST.DζOperator.Dζ (f : ℂ → ℂ) (z : ℂ) : ℂ

Dζ: rank-2 on lattice ⟨φ,ζ₆⟩, encoding all 6 operators

Equations

• FUST.DζOperator.Dζ f z = (FUST.DζOperator.AFNum (FUST.DζOperator.Φ_A f) z + FUST.DζOperator.SymNum (FUST.DζOperator.Φ_S f) z) / z

theorem FUST.DζOperator.phi_plus_two_ne : ↑φ + 2 ≠ 0

theorem FUST.DζOperator.Φ_A_const (c z : ℂ) : Φ_A (fun (x : ℂ) => c) z = (↑φ - ↑ψ) * c

Φ_A on constants: Σ = 1-4+(3+φ)-(3+ψ)+4-1 = φ-ψ (not zero, but AFNum kills it)

theorem FUST.DζOperator.Φ_S_const (c z : ℂ) : Φ_S (fun (x : ℂ) => c) z = 0

Φ_S annihilates constants: 2+(3+μ)-10+(3-μ)+2 = 0

theorem FUST.DζOperator.Dζ_const (z : ℂ) : Dζ (fun (x : ℂ) => 1) z = 0

Dζ annihilates constants (Φ_A gives const, AFNum kills it)

Fourier coefficients: AF = 2i√3, SY = 6

For f = w^s with s coprime to 6, the ζ₆ Fourier coefficients are: AFNum factor = ζ₆^s + ζ₆^{2s} - ζ₆^{4s} - ζ₆^{5s} SymNum factor = 2 + ζ₆^s - ζ₆^{2s} - 2ζ₆^{3s} - ζ₆^{4s} + ζ₆^{5s} For s ≡ 1 mod 6: AF = 2i√3, SY = 6. For s ≡ 5 mod 6: AF = -2i√3, SY = 6.

noncomputable def FUST.DζOperator.AF_coeff : ℂ

AF_coeff = ζ₆+ζ₆²-ζ₆⁴-ζ₆⁵ = (ζ₆-ζ₆⁵)+(ζ₆²-ζ₆⁴)

Equations

• FUST.DζOperator.AF_coeff = FUST.ζ₆ + FUST.ζ₆ ^ 2 - FUST.ζ₆ ^ 4 - FUST.ζ₆ ^ 5

theorem FUST.DζOperator.AF_coeff_eq : AF_coeff = { re := 0, im := 2 * √3 }

AF_coeff = 2i√3

theorem FUST.DζOperator.SY_coeff_val : 2 + ζ₆ - ζ₆ ^ 2 - 2 * ζ₆ ^ 3 - ζ₆ ^ 4 + ζ₆ ^ 5 = 6

2+ζ₆-ζ₆²-2ζ₆³-ζ₆⁴+ζ₆⁵ = 6

Monomial mode selection: (ζ₆^j)^{6k+r} = ζ₆^{jr}

theorem FUST.DζOperator.AFNum_pow_mod6_1 (k : ℕ) (z : ℂ) : AFNum (fun (w : ℂ) => w ^ (6 * k + 1)) z = z ^ (6 * k + 1) * AF_coeff

AFNum on w^{6k+1} = AF_coeff · z^{6k+1}

theorem FUST.DζOperator.SymNum_pow_mod6_1 (k : ℕ) (z : ℂ) : SymNum (fun (w : ℂ) => w ^ (6 * k + 1)) z = 6 * z ^ (6 * k + 1)

SymNum on w^{6k+1} = 6 · z^{6k+1}

theorem FUST.DζOperator.AFNum_pow_mod6_5 (k : ℕ) (z : ℂ) : AFNum (fun (w : ℂ) => w ^ (6 * k + 5)) z = -(z ^ (6 * k + 5) * AF_coeff)

AFNum on w^{6k+5} = -AF_coeff · z^{6k+5}

theorem FUST.DζOperator.SymNum_pow_mod6_5 (k : ℕ) (z : ℂ) : SymNum (fun (w : ℂ) => w ^ (6 * k + 5)) z = 6 * z ^ (6 * k + 5)

SymNum on w^{6k+5} = 6 · z^{6k+5}

Mod 6 vanishing: AFNum and SymNum kill w^n for gcd(n,6) > 1

For n ≡ 0,2,3,4 mod 6, the ζ₆-multiplexing sums vanish: AF_n := ζ₆ⁿ + ζ₆²ⁿ - ζ₆⁴ⁿ - ζ₆⁵ⁿ = 0 SY_n := 2 + ζ₆ⁿ - ζ₆²ⁿ - 2ζ₆³ⁿ - ζ₆⁴ⁿ + ζ₆⁵ⁿ = 0

theorem FUST.DζOperator.AFNum_pow_mod6_0 (k : ℕ) (z : ℂ) : AFNum (fun (w : ℂ) => w ^ (6 * k)) z = 0

AFNum on w^{6k} = 0

theorem FUST.DζOperator.SymNum_pow_mod6_0 (k : ℕ) (z : ℂ) : SymNum (fun (w : ℂ) => w ^ (6 * k)) z = 0

SymNum on w^{6k} = 0

theorem FUST.DζOperator.AFNum_pow_mod6_2 (k : ℕ) (z : ℂ) : AFNum (fun (w : ℂ) => w ^ (6 * k + 2)) z = 0

AFNum on w^{6k+2} = 0 (ζ₆²+ζ₆⁴-ζ₆⁸-ζ₆¹⁰ = 0)

theorem FUST.DζOperator.SymNum_pow_mod6_2 (k : ℕ) (z : ℂ) : SymNum (fun (w : ℂ) => w ^ (6 * k + 2)) z = 0

SymNum on w^{6k+2} = 0

theorem FUST.DζOperator.AFNum_pow_mod6_3 (k : ℕ) (z : ℂ) : AFNum (fun (w : ℂ) => w ^ (6 * k + 3)) z = 0

AFNum on w^{6k+3} = 0 (ζ₆³=-1 cancellation)

theorem FUST.DζOperator.SymNum_pow_mod6_3 (k : ℕ) (z : ℂ) : SymNum (fun (w : ℂ) => w ^ (6 * k + 3)) z = 0

SymNum on w^{6k+3} = 0

theorem FUST.DζOperator.AFNum_pow_mod6_4 (k : ℕ) (z : ℂ) : AFNum (fun (w : ℂ) => w ^ (6 * k + 4)) z = 0

AFNum on w^{6k+4} = 0 (ζ₆⁴=-ζ₆ cancellation)

theorem FUST.DζOperator.SymNum_pow_mod6_4 (k : ℕ) (z : ℂ) : SymNum (fun (w : ℂ) => w ^ (6 * k + 4)) z = 0

SymNum on w^{6k+4} = 0

Norm squared decomposition: |6a + 2i√3·b|² = 12(3a² + b²)

The unified Dζ output for monomial z^s decomposes as: Re(Dζ) = 6·Φ_S (symmetric/rotation channel, weight 3) Im(Dζ) = ±2√3·Φ_A (antisymmetric/boost channel, weight 1) The 3:1 weight ratio in |Dζ|² encodes I4 = Fin 1 ⊕ Fin 3.

theorem FUST.DζOperator.Dζ_normSq_decomposition (a b : ℝ) : Complex.normSq (6 * ↑a + AF_coeff * ↑b) = 12 * (3 * a ^ 2 + b ^ 2)

|6a + AF_coeff·b|² = 12(3a² + b²) for real a, b

theorem FUST.DζOperator.AF_coeff_normSq : Complex.normSq AF_coeff = 12

|AF_coeff|² = 12

Φ_S 3-component decomposition: Diff5 + Diff3 + μ·Diff2

Φ_S decomposes into 3 independent sub-operators (Dn numerators Diff2/Diff3/Diff5). For monomials z^s, the coefficients σ_Diff_n(s) = Diff_n(z^s)/z^s form rank-3 vectors across s=1,5,7, proving Φ_S carries Fin 3 of information.

theorem FUST.DζOperator.Φ_S_decompose (f : ℂ → ℂ) (z : ℂ) : Φ_S f z = 2 * Diff5 f z + Diff3 f z + 2 / (↑φ + 2) * Diff2 f z

Φ_S = 2·Diff5 + Diff3 + μ·Diff2

theorem FUST.DζOperator.Diff2_pow (s : ℕ) (z : ℂ) : Diff2 (fun (w : ℂ) => w ^ s) z = (↑φ ^ s - ↑ψ ^ s) * z ^ s

Diff_n on w^s: monomial coefficients

theorem FUST.DζOperator.Diff3_pow (s : ℕ) (z : ℂ) : Diff3 (fun (w : ℂ) => w ^ s) z = (↑φ ^ s - 2 + ↑ψ ^ s) * z ^ s

theorem FUST.DζOperator.Diff5_pow (s : ℕ) (z : ℂ) : Diff5 (fun (w : ℂ) => w ^ s) z = (↑φ ^ (2 * s) + ↑φ ^ s - 4 + ↑ψ ^ s + ↑ψ ^ (2 * s)) * z ^ s

theorem FUST.DζOperator.Φ_S_pow_via_sub (s : ℕ) (z : ℂ) : Φ_S (fun (w : ℂ) => w ^ s) z = (2 * (↑φ ^ (2 * s) + ↑φ ^ s - 4 + ↑ψ ^ s + ↑ψ ^ (2 * s)) + (↑φ ^ s - 2 + ↑ψ ^ s) + 2 / (↑φ + 2) * (↑φ ^ s - ↑ψ ^ s)) * z ^ s

Φ_S on w^s via sub-operator coefficients

Golden ratio powers as F_n·φ + F_{n-1}

Sub-operator coefficient values

noncomputable def FUST.DζOperator.σ_Diff5 (s : ℕ) : ℝ

σ_Diff5(s) = L_{2s} + L_s - 4, σ_Diff3(s) = L_s - 2, σ_Diff2(s) = √5·F_s

Equations

• FUST.DζOperator.σ_Diff5 s = FUST.φ ^ (2 * s) + FUST.φ ^ s - 4 + FUST.ψ ^ s + FUST.ψ ^ (2 * s)

noncomputable def FUST.DζOperator.σ_Diff3 (s : ℕ) : ℝ

Equations

• FUST.DζOperator.σ_Diff3 s = FUST.φ ^ s - 2 + FUST.ψ ^ s

noncomputable def FUST.DζOperator.σ_Diff2 (s : ℕ) : ℝ

Equations

• FUST.DζOperator.σ_Diff2 s = FUST.φ ^ s - FUST.ψ ^ s

theorem FUST.DζOperator.σ_Diff5_one : σ_Diff5 1 = 0

theorem FUST.DζOperator.σ_Diff3_one : σ_Diff3 1 = -1

theorem FUST.DζOperator.σ_Diff2_one : σ_Diff2 1 = φ - ψ

theorem FUST.DζOperator.σ_Diff5_five : σ_Diff5 5 = 130

theorem FUST.DζOperator.σ_Diff3_five : σ_Diff3 5 = 9

theorem FUST.DζOperator.σ_Diff2_five : σ_Diff2 5 = 5 * (φ - ψ)

theorem FUST.DζOperator.σ_Diff5_seven : σ_Diff5 7 = 868

theorem FUST.DζOperator.σ_Diff3_seven : σ_Diff3 7 = 27

theorem FUST.DζOperator.σ_Diff2_seven : σ_Diff2 7 = 13 * (φ - ψ)

theorem FUST.DζOperator.Φ_S_rank_three : σ_Diff5 1 * (σ_Diff3 5 * σ_Diff2 7 - σ_Diff2 5 * σ_Diff3 7) - σ_Diff3 1 * (σ_Diff5 5 * σ_Diff2 7 - σ_Diff2 5 * σ_Diff5 7) + σ_Diff2 1 * (σ_Diff5 5 * σ_Diff3 7 - σ_Diff3 5 * σ_Diff5 7) ≠ 0

The 3×3 det of [σ_Diff5, σ_Diff3, σ_Diff2] at s=1,5,7 is -6952(φ-ψ) ≠ 0: rank 3.

Dζ Gauge Covariance

Dζ(f(c·))(z) = c · Dζ(f)(c·z) for any c ≠ 0. "Continuity without limits": every observer at scale φⁿ sees identical algebraic structure. A continuous-parameter limit (D_t → θ) would only parametrize the φ-direction and cannot extend to full Dζ, because the ζ₆-direction is compact-discrete (ℤ/6ℤ, period 6).

theorem FUST.DζOperator.Φ_A_translate (f : ℂ → ℂ) (c z : ℂ) : Φ_A (fun (t : ℂ) => f (c * t)) z = Φ_A f (c * z)

Φ_A is translation-equivariant: Φ_A(f(c·))(z) = Φ_A(f)(cz)

theorem FUST.DζOperator.Φ_S_translate (f : ℂ → ℂ) (c z : ℂ) : Φ_S (fun (t : ℂ) => f (c * t)) z = Φ_S f (c * z)

Φ_S is translation-equivariant: Φ_S(f(c·))(z) = Φ_S(f)(cz)

theorem FUST.DζOperator.AFNum_translate (g : ℂ → ℂ) (c z : ℂ) : AFNum (fun (w : ℂ) => g (c * w)) z = AFNum g (c * z)

AFNum is translation-equivariant: AFNum(g(c·))(z) = AFNum(g)(cz)

theorem FUST.DζOperator.SymNum_translate (g : ℂ → ℂ) (c z : ℂ) : SymNum (fun (w : ℂ) => g (c * w)) z = SymNum g (c * z)

SymNum is translation-equivariant: SymNum(g(c·))(z) = SymNum(g)(cz)

theorem FUST.DζOperator.Dζ_gauge_covariance (f : ℂ → ℂ) (c z : ℂ) (hc : c ≠ 0) (hz : z ≠ 0) : Dζ (fun (t : ℂ) => f (c * t)) z = c * Dζ f (c * z)

Dζ gauge covariance: Dζ(f(c·))(z) = c · Dζ(f)(cz)

theorem FUST.DζOperator.Dζ_phi_covariance (f : ℂ → ℂ) (z : ℂ) (hz : z ≠ 0) : Dζ (fun (t : ℂ) => f (↑φ * t)) z = ↑φ * Dζ f (↑φ * z)

φ-gauge covariance: Dζ(f(φ·))(z) = φ · Dζ(f)(φz)

theorem FUST.DζOperator.Dζ_self_similar (f : ℂ → ℂ) (n : ℕ) (z : ℂ) (hz : z ≠ 0) : Dζ (fun (t : ℂ) => f (↑φ ^ n * t)) z = ↑φ ^ n * Dζ f (↑φ ^ n * z)

Iterated φ-scaling: Dζ(f(φⁿ·))(z) = φⁿ · Dζ(f)(φⁿz)

theorem FUST.DζOperator.observer_scale_independence (f : ℂ → ℂ) (n : ℤ) (z : ℂ) (hz : z ≠ 0) : Dζ (fun (t : ℂ) => f (↑φ ^ n * t)) z = ↑φ ^ n * Dζ f (↑φ ^ n * z)

Observer scale independence: no internal measurement distinguishes absolute scale