Encyclopedia Foundation Foundation Pair Kernel Periodic3 Torus Fourier Mode Pointwise Orthogonality Fact

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Periodic3 Torus Fourier Mode Pointwise Orthogonality Fact

On a finite periodic grid, distinct wave patterns cancel out when added across all points, a fact that lets signals be decomposed into independent components.

Verify this page

The orthogonality fact

In mathematics, an orthogonality relation is a precise way of saying that two different patterns do not overlap. On a finite periodic three-dimensional grid, a torus, the patterns in question are the discrete Fourier modes: functions that assign to each grid point a root of unity, essentially a set of evenly spaced points on the complex unit circle. The declaration torusFourierMode_pointwise_orthogonality_factor establishes the exact formula for this cancellation. For any two modes m and n, the sum over all grid points of the conjugate of mode m times mode n equals N cubed if m equals n, and equals zero otherwise. Here N is the number of points along one side of the grid, so N cubed is the total number of grid points. The formula is a theorem in the framework's machine-checked library of formal theorems, and it is proved for every positive integer N.

The result is the finite, discrete analogue of the familiar fact that sine and cosine waves of different frequencies are orthogonal. On the infinite line, integrals of products of distinct frequencies vanish; on the finite torus, sums replace integrals and the vanishing is exact. The proof in the library runs by reducing the three-dimensional sum to a product of three one-dimensional sums, each of which evaluates to N when the frequencies match and to zero otherwise. This is the standard geometric series argument, carried out in full formal detail. The factor N cubed is the normalizing constant that appears when a signal is reconstructed from its Fourier coefficients, and the zero for distinct modes is what makes the decomposition unique.

In Recognition Science, this fact is one piece of a larger construction. The framework models a finite periodic carrier for a recognition process, a discrete record of events on a three-dimensional torus. The orthogonality relation is what allows a source field on the torus to be separated into independent frequency components, each of which can be analyzed or inverted separately. The library uses it to show that a neutral source, one whose values sum to zero, can be reconstructed from its nonzero frequency modes alone. That reconstruction is a theorem, but it depends on the hypothesis that the source satisfies a particular neutrality condition.

The declaration does not claim that the finite periodic torus is identical to the infinite Fourier readout or to a finite open box. It does not assert a convergence theorem as the grid size grows without bound. And it does not establish that the shift-eigenmode equations, the physical equations of motion on the torus, hold; those remain hypotheses in the library. The orthogonality fact is a purely combinatorial and algebraic statement about the modes, independent of any dynamical content.

What the fact changes is the practical mathematics of the framework's periodic carrier. With this relation in hand, any source on the torus can be decomposed into independent frequency channels, the zero mode separated from the rest, and the nonzero modes treated as a self-contained system. That separation is the foundation for the spectral response constructions that follow, and it is a clean, exact result that holds for every finite grid size.

THEOREM torusFourierMode_orthogonality · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
torusFourierMode_orthogonality · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:572 
/-- The finite Fourier modes are orthogonal over the periodic sites.

The scalar is the full site count `N^3`; no normalization is hidden in the
source transform. The proof includes the `N = 1` case through the same
finite root-of-unity argument. -/
theorem torusFourierMode_orthogonality
    {N : ℕ} [NeZero N] (m n : Fin 3 → Fin N) :
    (∑ p : TorusSite3 N,
      (torusFourierMode m p)⁻¹ * torusFourierMode n p)
      = if m = n then (N : ℂ) ^ 3 else 0 := by
  classical
  have hsite_univ :
      (Finset.univ : Finset (TorusSite3 N)) =
        Fintype.piFinset
          (fun _ : Fin 3 => (Finset.univ : Finset (ZMod N))) := by
    ext p
    simp only [Finset.mem_univ, Fintype.mem_piFinset]
    simp
  simp_rw [torusFourierMode_pointwise_orthogonality_factor]
  calc
    (∑ p : TorusSite3 N,
        ∏ i : Fin 3,
          (torusRoot N ^ ((m i).val * (p i).val))⁻¹ *
            torusRoot N ^ ((n i).val * (p i).val)) =
        ∏ i : Fin 3,
          ∑ x : ZMod N,
            (torusRoot N ^ ((m i).val * x.val))⁻¹ *
              torusRoot N ^ ((n i).val * x.val) := by
          rw [hsite_univ]
          simpa [TorusSite3] using
            (Finset.sum_prod_piFinset
              (s := (Finset.univ : Finset (ZMod N)))
              (g := fun i x =>
                (torusRoot N ^ ((m i).val * x.val))⁻¹ *
                  torusRoot N ^ ((n i).val * x.val)))
    _ = if m = n then (N : ℂ) ^ 3 else 0 := by
          by_cases hmn : m = n
          · subst n
            simp [torusRoot_sum_zmod_cross]
          · have hcoord : ∃ i : Fin 3, m i ≠ n i := by
              by_contra h
              apply hmn
              funext i
              by_contra hi
              exact h ⟨i, hi⟩
            rcases hcoord with ⟨i, hi⟩
            rw [if_neg hmn]
            apply Finset.prod_eq_zero (Finset.mem_univ i)
            rw [torusRoot_sum_zmod_cross]
            simp [hi]
THEOREM torusRoot_sum_fin_cross · torusRoot_sum_site_cross · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
torusRoot_sum_fin_cross · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:450 
private theorem torusRoot_sum_fin_cross
    (N : ℕ) [NeZero N] (a b : Fin N) :
    (∑ x : Fin N,
      (torusRoot N ^ (a.val * x.val))⁻¹ *
        torusRoot N ^ (b.val * x.val))
      = if a = b then (N : ℂ) else 0 := by
  classical
  by_cases hab : a = b
  · subst b
    simp only [if_pos rfl]
    calc
      (∑ x : Fin N,
          (torusRoot N ^ (a.val * x.val))⁻¹ *
            torusRoot N ^ (a.val * x.val)) =
          ∑ _ : Fin N, (1 : ℂ) := by
            apply Finset.sum_congr rfl
            intro x hx
            exact inv_mul_cancel₀
              (pow_ne_zero _ (Complex.exp_ne_zero _))
      _ = (N : ℂ) := by simp
  · let r : ℂ :=
      (torusRoot N ^ a.val)⁻¹ * torusRoot N ^ b.val
    have hrN : r ^ N = 1 := by
      dsimp [r]
      rw [mul_pow, inv_pow, ← pow_mul, ← pow_mul,
        torusRoot_pow_mul_card, torusRoot_pow_mul_card]
      simp
    have hroot_ne : torusRoot N ^ a.val ≠ 0 :=
      pow_ne_zero _ (Complex.exp_ne_zero _)
    have hrne : r ≠ 1 := by
      intro hr
      have hpow :
          torusRoot N ^ b.val = torusRoot N ^ a.val := by
        calc
          torusRoot N ^ b.val =
              torusRoot N ^ a.val *
                ((torusRoot N ^ a.val)⁻¹ * torusRoot N ^ b.val) := by
              rw [← mul_assoc, mul_inv_cancel₀ hroot_ne, one_mul]
          _ = torusRoot N ^ a.val * 1 := by
              change torusRoot N ^ a.val * r =
                torusRoot N ^ a.val * 1
              rw [hr]
          _ = torusRoot N ^ a.val := mul_one _
      have hval : a.val = b.val :=
        (torusRoot_isPrimitiveRoot N).pow_inj a.isLt b.isLt hpow.symm
      exact hab (Fin.ext hval)
    calc
      (∑ x : Fin N,
          (torusRoot N ^ (a.val * x.val))⁻¹ *
            torusRoot N ^ (b.val * x.val)) =
          ∑ k ∈ Finset.range N,
            (torusRoot N ^ (a.val * k))⁻¹ *
              torusRoot N ^ (b.val * k) := by
            rw [Finset.sum_fin_eq_sum_range]
            apply Finset.sum_congr rfl
            intro k hk
            simp only [Finset.mem_range] at hk
            simp [hk]
      _ = ∑ k ∈ Finset.range N, r ^ k := by
            apply Finset.sum_congr rfl
            intro k hk
            dsimp [r]
            rw [pow_mul, pow_mul, mul_pow, inv_pow]
      _ = 0 := by
            rw [geom_sum_eq hrne N, hrN]
            simp
      _ = if a = b then (N : ℂ) else 0 := by simp [hab]
torusRoot_sum_site_cross · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:530 
private theorem torusRoot_sum_site_cross
    (N : ℕ) [NeZero N] (x y : ZMod N) :
    (∑ a : Fin N,
      (torusRoot N ^ (a.val * x.val))⁻¹ *
        torusRoot N ^ (a.val * y.val))
      = if x = y then (N : ℂ) else 0 := by
  by_cases hxy : x = y
  · subst y
    simpa [Nat.mul_comm] using
      torusRoot_sum_fin_cross N
        ⟨x.val, ZMod.val_lt x⟩ ⟨x.val, ZMod.val_lt x⟩
  · have hfin :
        (⟨x.val, ZMod.val_lt x⟩ : Fin N) ≠
          ⟨y.val, ZMod.val_lt y⟩ := by
      intro h
      apply hxy
      apply (ZMod.val_injective N)
      exact congrArg Fin.val h
    simpa [hxy, hfin, Nat.mul_comm] using
      torusRoot_sum_fin_cross N
        ⟨x.val, ZMod.val_lt x⟩ ⟨y.val, ZMod.val_lt y⟩
THEOREM torusSourceReconstructedByNonzeroModesNormalized_of_neutral · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
torusSourceReconstructedByNonzeroModesNormalized_of_neutral · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:727 
/-- Neutrality removes the zero term from the normalized finite inversion. -/
theorem torusSourceReconstructedByNonzeroModesNormalized_of_neutral
    {N : ℕ} [NeZero N] (rho : TorusSite3 N → ℂ)
    (hneutral : torusSourceNeutral rho) :
    torusSourceReconstructedByNonzeroModesNormalized rho := by
  classical
  intro p
  have hzero_mem :
      (0 : Fin 3 → Fin N) ∉ torusNonzeroModes N := by
    simp [torusNonzeroModes]
  have huniv :
      (Finset.univ : Finset (Fin 3 → Fin N)) =
        insert 0 (torusNonzeroModes N) := by
    ext m
    by_cases hm : m = 0 <;> simp [torusNonzeroModes, hm]
  have hsplit :
      (∑ m : Fin 3 → Fin N,
        torusSourceTransform rho m * torusFourierMode m p) =
        torusSourceTransform rho 0 * torusFourierMode 0 p +
          (∑ m ∈ torusNonzeroModes N,
            torusSourceTransform rho m * torusFourierMode m p) := by
    change
      (∑ m ∈ (Finset.univ : Finset (Fin 3 → Fin N)),
        torusSourceTransform rho m * torusFourierMode m p) = _
    rw [huniv, Finset.sum_insert hzero_mem]
  have hfull := torusSource_reconstruction rho p
  rw [hsplit, torusSourceTransform_zero_eq_zero_of_neutral rho hneutral,
    torusFourierMode_zero, zero_mul, zero_add] at hfull
  exact hfull.symm

What this page does not claim

The finite periodic torus is not identified with the finite open box or the infinite Fourier readout. No finite-volume convergence theorem is asserted as the grid size grows. The shift-eigenmode equations remain hypotheses, not theorems.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND