7. Finite Fourier And Circulant Algebra

Claim boundary proved finite algebra Python diagnostics AI performance separate no quality claim

Finite Fourier analysis is the spectral language of a finite circle. A cyclic character turns addition on ZMod n into multiplication by a phase. Circular convolution is the corresponding circulant token mixer.

The Lean spine is:

The public imports are:

import Circle.Core
import Circle.Applications.Public

Proved Facts

The current formal layer proves:

  • character values are nth roots of unity;
  • finite shifts compose additively;
  • Fourier coefficients are additive in the signal;
  • shifting a signal multiplies each Fourier coefficient by the matching phase;
  • circular convolution is shift-equivariant, commutative, and additive;
  • each Fourier coefficient of c ⋆ x factors into the matching coefficient of c times the matching coefficient of x.

Executable Companion

from circle_math.core import (
    circular_convolution,
    spectral_aliasing_report,
    spectral_convolution_report,
)

signal = [1, 2, 0, -1]
kernel = [2, 0, 1, 0]

print(circular_convolution(kernel, signal))
print(spectral_convolution_report(kernel, signal).passed)
print(spectral_aliasing_report(4, [-1, 0, 3, 4, 7]))

Why It Connects

The same circle algebra shows up in:

  • finite coils and stride orbits;
  • DFT and roots of unity;
  • circular convolution and circulant matrices;
  • RoPE and other phase-bank positional encodings;
  • Fourier features and harmonic networks;
  • cyclic sparse-attention patterns.

The proof layer certifies algebraic structure. It does not certify neural model quality, speed, memory use, training stability, or deployment behavior.