Foundation Pair Kernel Periodic3 Torus Laplacian Torus Spectral Green Mode Eq Mo

The periodic carrier

A finite periodic three-dimensional torus is a grid of points where each coordinate wraps around, like a video game screen. On such a grid, the discrete Laplacian is a local operation: at each point it takes twice the value there and subtracts the values at the six nearest neighbors, one step in each of the three axis directions. The framework's ledger, a discrete record of events, uses this operator as its carrier for recognition on a periodic structure.

The key fact is that this Laplacian acts on a Fourier mode, a wave that oscillates with a fixed frequency in each direction, by simple multiplication. The multiplier is the cubic-lattice symbol, a number that depends only on the wave's frequency. The declaration torusLaplacian_torusSpectralGreenMode_eq_mode_of_ne_zero establishes that the spectral Green's mode, defined as the inverse of that symbol times the Fourier mode, is an exact eigenmode of the Laplacian with that symbol as eigenvalue, for every nonzero frequency.

This is the discrete analog of the continuous result that the Laplacian of a plane wave is proportional to the wave itself. The proportionality constant is the frequency-dependent symbol. The theorem is proved in the machine-checked library of formal theorems, meaning it follows from the definitions by rules of logic with no gaps. The proof relies on the shift property of Fourier modes: shifting a mode by one step multiplies it by a root of unity, which is the eigenvalue of the shift operator.

What the theorem does not claim is that the periodic carrier is the same as the finite open box or the infinite Fourier readout. The shift-eigenmode equations remain hypotheses, not conclusions. The module does not assert a finite-volume convergence theorem, meaning it does not claim that results on the finite torus converge to results on the infinite lattice as the size grows. It also does not claim that the spectral Green's mode is the unique solution to the Laplacian equation; it only shows that this particular construction is an eigenmode.

In Recognition Science, this result provides the exact spectral response for the periodic carrier. It shows that the framework's recognition cost, the forced expense of registering an event, can be inverted on a torus by a simple Fourier sum. This is a necessary step for building a finite periodic model of recognition that is mathematically closed, though the physical bridge from recognition to three-dimensional space remains open.

/-- 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

/-- 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

/-- The finite-torus spectral Green mode, with the zero frequency removed.
    Its nonzero-mode denominator is exactly the same lattice symbol used by
    the periodic Laplacian and by the infinite Fourier readout. -/
noncomputable def torusSpectralGreenMode
    {N : ℕ} [NeZero N] (m : Fin 3 → Fin N) : TorusSite3 N → ℂ :=
  if m = 0 then 0 else
    fun p => (symbol (torusQuantizedWave N m) : ℂ)⁻¹ * torusFourierMode m p

What this page does not claim

The theorem does not identify the periodic carrier with the finite open box or the infinite Fourier readout. The theorem does not assert a finite-volume convergence theorem. The theorem does not claim the spectral Green's mode is the unique solution to the Laplacian equation.

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: