Encyclopedia Foundation Foundation Pair Kernel Periodic3

ARTICLE 5 claims 4 theorems 1 model

Foundation Pair Kernel Periodic3

A finite, wrap-around grid of points replaces the infinite lattice, and the framework proves the exact Fourier machinery that makes waves on it behave.

Verify this page

The finite periodic carrier

In classical mathematics, a finite torus is a grid of points whose edges wrap around: step past the last point in any direction and you arrive back at the first. The framework's ledger, a discrete record of events, supplies exactly such a carrier. The module builds a three-dimensional torus of N points per side, where every site is a triple of coordinates taken modulo N, so a shift in any coordinate cycles through the whole ring. This is the finite periodic carrier that the framework's earlier open-box construction lacked.

The central achievement is a complete Fourier theory on this finite grid. The module defines the torus Laplacian, the discrete analogue of the continuous second-derivative operator, acting on each site by comparing it with its six axis neighbors. It then proves that the Fourier modes, the complex exponentials e^(2πi m·p/N), are exact eigenfunctions of this Laplacian, with eigenvalues given by the familiar cubic-lattice symbol. Orthogonality of these modes is proved in both the site and frequency directions, and the reconstruction theorem shows that any source field can be recovered exactly from its Fourier coefficients, with the zero mode contributing nothing when the total source vanishes.

The payoff is a spectral Green's function, built from the nonzero modes, that inverts the Laplacian. The module proves that applying the Laplacian to this spectral response returns the original source, provided the source is reconstructed by its nonzero modes. This is the discrete analogue of solving Poisson's equation on a finite box with periodic boundary conditions. The theorems are machine-checked in the framework's library of formal theorems, and they hold for any positive grid size N.

In Recognition Science, this finite periodic carrier is the concrete stage on which the framework's recognition events play out. The shift-eigenmode equations that the carrier supports remain hypotheses, not theorems; the module does not identify this periodic carrier with the finite open box or with the infinite Fourier readout, and it asserts no finite-volume convergence theorem. What it does establish, with certainty, is that the Fourier machinery works exactly on this finite wrap-around grid, giving the framework a sound discrete geometry on which to build further structure.

MODEL TorusSite3 · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
TorusSite3 · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:25 
/-- A site of the finite periodic three-dimensional torus. -/
abbrev TorusSite3 (N : ℕ) := Fin 3 → ZMod N
THEOREM torusFourierMode_shift_plus · torusFourierMode_shift_minus · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
torusFourierMode_shift_plus · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:127 
/-- The concrete periodic Fourier mode satisfies every forward shift equation. -/
theorem torusFourierMode_shift_plus {N : ℕ} [NeZero N]
    (m : Fin 3 → Fin N) (p : TorusSite3 N) (i : Fin 3) :
    torusFourierMode m (torusShift p i 1) =
      torusPlusEigenvalue N m i * torusFourierMode m p := by
  have hfun :
      (fun j : Fin 3 =>
          torusRoot N ^ ((m j).val * (torusShift p i 1 j).val)) =
        Function.update
          (fun j : Fin 3 => torusRoot N ^ ((m j).val * (p j).val))
          i
          (torusRoot N ^ ((m i).val * (p i).val) * torusRoot N ^ (m i).val) := by
    funext j
    by_cases hji : j = i
    · subst j
      simp [torusShift]
      exact torusRoot_pow_zmod_add_one N (m i) (p i)
    · simp [torusShift, hji]
  unfold torusFourierMode torusPlusEigenvalue
  rw [hfun, Finset.prod_update_of_mem (Finset.mem_univ i)]
  have hprod :
      (∏ x : Fin 3, torusRoot N ^ ((m x).val * (p x).val)) =
        (∏ x ∈ Finset.univ.erase i,
          torusRoot N ^ ((m x).val * (p x).val))
          * torusRoot N ^ ((m i).val * (p i).val) := by
    rw [Finset.prod_erase_mul (Finset.univ : Finset (Fin 3))
      (fun x => torusRoot N ^ ((m x).val * (p x).val)) (Finset.mem_univ i)]
  rw [Finset.sdiff_singleton_eq_erase]
  calc
    torusRoot N ^ ((m i).val * (p i).val) *
        torusRoot N ^ (m i).val *
        (∏ x ∈ Finset.univ.erase i,
          torusRoot N ^ ((m x).val * (p x).val)) =
      ((∏ x ∈ Finset.univ.erase i,
          torusRoot N ^ ((m x).val * (p x).val)) *
        torusRoot N ^ ((m i).val * (p i).val)) * torusRoot N ^ (m i).val := by
          ring
    _ = (∏ x : Fin 3, torusRoot N ^ ((m x).val * (p x).val)) *
        torusRoot N ^ (m i).val := by rw [← hprod]
    _ = torusRoot N ^ (m i).val *
        (∏ x : Fin 3, torusRoot N ^ ((m x).val * (p x).val)) := by ring
torusFourierMode_shift_minus · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:169 
/-- The concrete periodic Fourier mode satisfies every backward shift equation. -/
theorem torusFourierMode_shift_minus {N : ℕ} [NeZero N]
    (m : Fin 3 → Fin N) (p : TorusSite3 N) (i : Fin 3) :
    torusFourierMode m (torusShift p i (-1)) =
      torusMinusEigenvalue N m i * torusFourierMode m p := by
  have hplus :=
    torusFourierMode_shift_plus m (torusShift p i (-1)) i
  rw [torusShift_plus_minus] at hplus
  unfold torusMinusEigenvalue
  have hne : torusPlusEigenvalue N m i ≠ 0 := by
    unfold torusPlusEigenvalue
    exact pow_ne_zero _ (Complex.exp_ne_zero _)
  calc
    torusFourierMode m (torusShift p i (-1)) =
        (torusPlusEigenvalue N m i)⁻¹ *
          (torusPlusEigenvalue N m i *
            torusFourierMode m (torusShift p i (-1))) := by
      rw [← mul_assoc, inv_mul_cancel₀ hne, one_mul]
    _ = (torusPlusEigenvalue N m i)⁻¹ * torusFourierMode m p := by
          rw [← hplus]
THEOREM torusFourierMode_orthogonality · torusFourierMode_frequency_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]
torusFourierMode_frequency_orthogonality · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:623 
/-- The finite Fourier modes are also orthogonal over the frequency set.

This dual form is the leaf needed for a genuine finite inversion theorem. -/
theorem torusFourierMode_frequency_orthogonality
    {N : ℕ} [NeZero N] (p q : TorusSite3 N) :
    (∑ m : Fin 3 → Fin N,
      (torusFourierMode m p)⁻¹ * torusFourierMode m q)
      = if p = q then (N : ℂ) ^ 3 else 0 := by
  classical
  simp_rw [torusFourierMode_two_point_factor]
  calc
    (∑ m : Fin 3 → Fin N,
        ∏ i : Fin 3,
          (torusRoot N ^ ((m i).val * (p i).val))⁻¹ *
            torusRoot N ^ ((m i).val * (q i).val)) =
        ∏ i : Fin 3,
          ∑ a : Fin N,
            (torusRoot N ^ (a.val * (p i).val))⁻¹ *
              torusRoot N ^ (a.val * (q i).val) := by
          simpa [TorusSite3] using
            (Finset.sum_prod_piFinset
              (s := (Finset.univ : Finset (Fin N)))
              (g := fun i a =>
                (torusRoot N ^ (a.val * (p i).val))⁻¹ *
                  torusRoot N ^ (a.val * (q i).val)))
    _ = if p = q then (N : ℂ) ^ 3 else 0 := by
          by_cases hpq : p = q
          · subst q
            have hsum (i : Fin 3) :
                (∑ a : Fin N,
                  (torusRoot N ^ (a.val * (p i).val))⁻¹ *
                    torusRoot N ^ (a.val * (p i).val)) = (N : ℂ) := by
              simpa using torusRoot_sum_site_cross N (p i) (p i)
            simp_rw [hsum]
            simp
          · have hcoord : ∃ i : Fin 3, p i ≠ q i := by
              by_contra h
              apply hpq
              funext i
              by_contra hi
              exact h ⟨i, hi⟩
            rcases hcoord with ⟨i, hi⟩
            rw [if_neg hpq]
            apply Finset.prod_eq_zero (Finset.mem_univ i)
            rw [torusRoot_sum_site_cross]
            simp [hi]
THEOREM torusSource_reconstruction · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
torusSource_reconstruction · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:670 
/-- Full finite Fourier inversion with the explicit site-count normalization. -/
theorem torusSource_reconstruction
    {N : ℕ} [NeZero N] (rho : TorusSite3 N → ℂ)
    (p : TorusSite3 N) :
    ((N : ℂ) ^ 3)⁻¹ *
        (∑ m : Fin 3 → Fin N,
          torusSourceTransform rho m * torusFourierMode m p) =
      rho p := by
  classical
  have hN : (N : ℂ) ^ 3 ≠ 0 :=
    pow_ne_zero 3 (Nat.cast_ne_zero.mpr (NeZero.ne N))
  unfold torusSourceTransform
  calc
    ((N : ℂ) ^ 3)⁻¹ *
        (∑ m : Fin 3 → Fin N,
          (∑ q : TorusSite3 N,
            rho q * (torusFourierMode m q)⁻¹) *
            torusFourierMode m p) =
        ((N : ℂ) ^ 3)⁻¹ *
          (∑ q : TorusSite3 N,
            rho q *
              (∑ m : Fin 3 → Fin N,
                (torusFourierMode m q)⁻¹ *
                  torusFourierMode m p)) := by
      congr 1
      simp_rw [Finset.sum_mul]
      rw [Finset.sum_comm]
      apply Finset.sum_congr rfl
      intro q hq
      simp_rw [mul_assoc]
      rw [Finset.mul_sum]
    _ = ((N : ℂ) ^ 3)⁻¹ *
          (∑ q : TorusSite3 N,
            rho q *
              (if q = p then (N : ℂ) ^ 3 else 0)) := by
      apply congrArg (fun z : ℂ => ((N : ℂ) ^ 3)⁻¹ * z)
      apply Finset.sum_congr rfl
      intro q hq
      rw [torusFourierMode_frequency_orthogonality]
    _ = ((N : ℂ) ^ 3)⁻¹ * (rho p * (N : ℂ) ^ 3) := by
      congr 1
      simp
    _ = rho p := by
      calc
        ((N : ℂ) ^ 3)⁻¹ * (rho p * (N : ℂ) ^ 3) =
            rho p * (((N : ℂ) ^ 3)⁻¹ * (N : ℂ) ^ 3) := by ring
        _ = rho p := by rw [inv_mul_cancel₀ hN, mul_one]
THEOREM torusLaplacian_torusSpectralResponse_eq_source_of_reconstructed · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean
torusLaplacian_torusSpectralResponse_eq_source_of_reconstructed · IndisputableMonolith/Foundation/PairKernelPeriodic3.lean:798 
/-- Under explicit nonzero-mode reconstruction, the spectral response solves
the finite periodic source equation. -/
theorem torusLaplacian_torusSpectralResponse_eq_source_of_reconstructed
    {N : ℕ} [NeZero N] (rho : TorusSite3 N → ℂ)
    (hrec : torusSourceReconstructedByNonzeroModes rho)
    (p : TorusSite3 N) :
    torusLaplacian (torusSpectralResponse rho) p = rho p := by
  classical
  unfold torusSpectralResponse
  rw [torusLaplacian_finset_sum]
  calc
    ∑ m ∈ torusNonzeroModes N,
        torusLaplacian
          (fun q => torusSourceTransform rho m * torusSpectralGreenMode m q) p
        =
      ∑ m ∈ torusNonzeroModes N,
        torusSourceTransform rho m * torusFourierMode m p := by
        apply Finset.sum_congr rfl
        intro m hm
        have hm0 : m ≠ 0 := (mem_torusNonzeroModes m).1 hm
        rw [torusLaplacian_smul]
        rw [torusLaplacian_torusSpectralGreenMode_eq_mode_of_ne_zero m hm0]
    _ = rho p := by
        exact (hrec p).symm

What this page does not claim

The shift-eigenmode equations are not proved; they remain hypotheses. The finite periodic carrier is not identified with the finite open box or the infinite Fourier readout. No finite-volume convergence theorem is asserted.

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