TauLib · API Book III

TauLib.BookIII.Doors.SpectralDecomp

Spectral decomposition theory for the lemniscate operator H_L.

Registry Cross-References

[III.D80] Spectral Projector — spectral_projector, projector_check
[III.D81] Spectral Measure — spectral_measure, measure_total_check
[III.T56] Parseval Identity — parseval_check
[III.P48] Spectral Resolution — spectral_resolution_check

Mathematical Content

III.D80 (Spectral Projector): The projector P_n onto the n-th eigenspace of H_L. For the lemniscate with eigenvalues λ_n = n², P_n projects onto the mode with frequency n. At finite stage k, P_n is a rank-1 operator on the M_k-dimensional space.

III.D81 (Spectral Measure): The spectral measure μ_spec assigns weight 1/N to each eigenvalue λ_n for n = 0, …, N-1 (uniform on modes). The total measure is 1. This is the counting measure on the spectrum.

III.T56 (Parseval Identity): For f ∈ L²(L), ‖f‖² = Σ_n |⟨f, e_n⟩|². At finite stage, this is the Pythagorean theorem for orthogonal decomposition.

III.P48 (Spectral Resolution): H_L = Σ_n λ_n P_n. The operator is recovered from its eigenvalues and projectors. Verified at finite stages.

`Tau.BookIII.Doors.spectral_projector`

source **def Tau.BookIII.Doors.spectral_projector (n : ℕ)

(f : ℕ → ℤ)

(N x : ℕ) :ℤ**

[III.D80] Spectral projector: P_n(f) = ⟨f, e_n⟩ · e_n. For the discrete model with N points, e_n(x) = exp(2πinx/N). We use the real part: cos(2πnx/N), approximated by the indicator of the n-th frequency bin.

Simplified: at stage k with M_k points, the n-th mode projector extracts the n-th Fourier coefficient. For computational verification, we use the orthogonal basis of indicator functions. Equations

Tau.BookIII.Doors.spectral_projector n f N x = if (N == 0) = true then 0 else have coeff := if n < N then f n else 0; if (x == n) = true then coeff else 0 Instances For

`Tau.BookIII.Doors.projector_idempotent_check`

source def Tau.BookIII.Doors.projector_idempotent_check (N : ℕ) :Bool

[III.D80] Check projector is idempotent: P_n² = P_n. Equations

Tau.BookIII.Doors.projector_idempotent_check N = Tau.BookIII.Doors.projector_idempotent_check.go_n 0 N N Instances For

`Tau.BookIII.Doors.projector_idempotent_check.go_n`

source@[irreducible]

def Tau.BookIII.Doors.projector_idempotent_check.go_n (n bound fuel : ℕ) :Bool

Equations

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

`Tau.BookIII.Doors.projector_idempotent_check.go_x`

source@[irreducible]

**def Tau.BookIII.Doors.projector_idempotent_check.go_x (n x bound fuel : ℕ)

(pf f : ℕ → ℤ) :Bool**

Equations

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

`Tau.BookIII.Doors.projector_orthogonal_check`

source def Tau.BookIII.Doors.projector_orthogonal_check (N : ℕ) :Bool

[III.D80] Check projectors are orthogonal: P_n · P_m = 0 for n ≠ m. Equations

Tau.BookIII.Doors.projector_orthogonal_check N = Tau.BookIII.Doors.projector_orthogonal_check.go_n 0 N N Instances For

`Tau.BookIII.Doors.projector_orthogonal_check.go_n`

source@[irreducible]

def Tau.BookIII.Doors.projector_orthogonal_check.go_n (n bound fuel : ℕ) :Bool

Equations

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

`Tau.BookIII.Doors.projector_orthogonal_check.go_m`

source@[irreducible]

def Tau.BookIII.Doors.projector_orthogonal_check.go_m (n m bound fuel : ℕ) :Bool

Equations

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

`Tau.BookIII.Doors.projector_orthogonal_check.go_x`

source@[irreducible]

**def Tau.BookIII.Doors.projector_orthogonal_check.go_x (x bound fuel : ℕ)

(result : ℕ → ℤ) :Bool**

Equations

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

`Tau.BookIII.Doors.projector_check`

source def Tau.BookIII.Doors.projector_check (N : ℕ) :Bool

[III.D80] Full projector check: idempotent + orthogonal. Equations

Tau.BookIII.Doors.projector_check N = (Tau.BookIII.Doors.projector_idempotent_check N && Tau.BookIII.Doors.projector_orthogonal_check N) Instances For

`Tau.BookIII.Doors.spectral_measure`

source def Tau.BookIII.Doors.spectral_measure (N n : ℕ) :Bool

[III.D81] Spectral measure: weight of eigenvalue λ_n = n² is 1/N. Total measure = N · (1/N) = 1. Equations

Tau.BookIII.Doors.spectral_measure N n = decide (n < N) Instances For

`Tau.BookIII.Doors.measure_total_check`

source def Tau.BookIII.Doors.measure_total_check (N : ℕ) :Bool

[III.D81] Check total spectral measure = 1 (all N modes counted). Equations

Tau.BookIII.Doors.measure_total_check N = (Tau.BookIII.Doors.measure_total_check.go 0 N 0 == N) Instances For

`Tau.BookIII.Doors.measure_total_check.go`

source@[irreducible]

def Tau.BookIII.Doors.measure_total_check.go (n bound acc : ℕ) :ℕ

Equations

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

`Tau.BookIII.Doors.parseval_check`

source def Tau.BookIII.Doors.parseval_check (N : ℕ) :Bool

[III.T56] Parseval identity: ‖f‖² = Σ_n |c_n|² where c_n = f(n). For the indicator basis, ‖f‖² = Σ_x f(x)² and Σ_n c_n² = Σ_n f(n)². These are the same sum — Parseval is an identity. Equations

Tau.BookIII.Doors.parseval_check N = Tau.BookIII.Doors.parseval_check.go_f 0 N N Instances For

`Tau.BookIII.Doors.parseval_check.go_f`

source@[irreducible]

def Tau.BookIII.Doors.parseval_check.go_f (seed bound fuel : ℕ) :Bool

Equations

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

`Tau.BookIII.Doors.parseval_check.sum_sq`

source@[irreducible]

**def Tau.BookIII.Doors.parseval_check.sum_sq (f : ℕ → ℤ)

(x bound : ℕ)

(acc : ℤ) :ℤ**

Equations

Tau.BookIII.Doors.parseval_check.sum_sq f x bound acc = if x ≥ bound then acc else Tau.BookIII.Doors.parseval_check.sum_sq f (x + 1) bound (acc + f x * f x) Instances For

`Tau.BookIII.Doors.parseval_check.sum_coeff_sq`

source@[irreducible]

**def Tau.BookIII.Doors.parseval_check.sum_coeff_sq (f : ℕ → ℤ)

(n bound : ℕ)

(acc : ℤ)

(N : ℕ) :ℤ**

Equations

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

`Tau.BookIII.Doors.spectral_resolution_check`

source def Tau.BookIII.Doors.spectral_resolution_check (N : ℕ) :Bool

[III.P48] Spectral resolution: H_L = Σ_n λ_n P_n. Check: (Σ_n λ_n P_n)(f)(x) = H_L(f)(x) for test functions. For the discrete Laplacian, H_L(f)(x) = λ_x · f(x) in the eigenbasis. In the indicator basis, this is just f(x) · x². Equations

Tau.BookIII.Doors.spectral_resolution_check N = Tau.BookIII.Doors.spectral_resolution_check.go_f 0 N N Instances For

`Tau.BookIII.Doors.spectral_resolution_check.go_f`

source@[irreducible]

def Tau.BookIII.Doors.spectral_resolution_check.go_f (seed bound fuel : ℕ) :Bool

Equations

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

`Tau.BookIII.Doors.spectral_resolution_check.go_x`

source@[irreducible]

**def Tau.BookIII.Doors.spectral_resolution_check.go_x (seed x bound fuel : ℕ)

(f : ℕ → ℤ) :Bool**

Equations

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

`Tau.BookIII.Doors.spectral_resolution_check.sum_projectors`

source@[irreducible]

**def Tau.BookIII.Doors.spectral_resolution_check.sum_projectors (f : ℕ → ℤ)

(x n bound : ℕ)

(acc : ℤ)

(N : ℕ) :ℤ**

Equations

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

`Tau.BookIII.Doors.projector_check_2`

source theorem Tau.BookIII.Doors.projector_check_2 :projector_check 2 = true

[III.D80] Projectors correct at N = 2.

`Tau.BookIII.Doors.projector_check_6`

source theorem Tau.BookIII.Doors.projector_check_6 :projector_check 6 = true

[III.D80] Projectors correct at N = 6.

`Tau.BookIII.Doors.measure_total_6`

source theorem Tau.BookIII.Doors.measure_total_6 :measure_total_check 6 = true

[III.D81] Spectral measure total at N = 6.

`Tau.BookIII.Doors.measure_total_30`

source theorem Tau.BookIII.Doors.measure_total_30 :measure_total_check 30 = true

[III.D81] Spectral measure total at N = 30.

`Tau.BookIII.Doors.parseval_2`

source theorem Tau.BookIII.Doors.parseval_2 :parseval_check 2 = true

[III.T56] Parseval identity at N = 2.

`Tau.BookIII.Doors.parseval_6`

source theorem Tau.BookIII.Doors.parseval_6 :parseval_check 6 = true

[III.T56] Parseval identity at N = 6.

`Tau.BookIII.Doors.spectral_resolution_2`

source theorem Tau.BookIII.Doors.spectral_resolution_2 :spectral_resolution_check 2 = true

[III.P48] Spectral resolution at N = 2.

`Tau.BookIII.Doors.spectral_resolution_6`

source theorem Tau.BookIII.Doors.spectral_resolution_6 :spectral_resolution_check 6 = true

[III.P48] Spectral resolution at N = 6.