Foundation Pair Kernel Periodic3 Torus Laplacian Torus Spectral Response Eq Sour

The periodic carrier

The declaration torusLaplacian_torusSpectralResponse_eq_source_of_reconstructed establishes a precise inversion identity on a finite periodic three-dimensional grid. The grid is a torus: sites are triples of integers modulo N, so moving in any coordinate direction wraps around. On this grid, the Laplacian (a discrete operator that measures the difference between a field at a site and the average of its six nearest neighbors) is applied to a field called the spectral response. The theorem states that if the source field can be reconstructed from its nonzero Fourier modes, then the Laplacian of the spectral response equals the source field exactly, at every site.

This is a discrete analogue of solving a Poisson equation on a torus. The spectral response is built by taking the source field, decomposing it into Fourier modes (periodic waves at discrete frequencies), dividing each mode by its corresponding eigenvalue (a measure of how the Laplacian acts on that wave), and summing the result. The theorem confirms that this procedure truly inverts the Laplacian: it is not an approximation or a heuristic. The condition that the source be reconstructible from nonzero modes means the source has no constant component; a uniform field would be annihilated by the Laplacian and could not be recovered this way.

In Recognition Science, this result is part of a larger chain that forces three spatial dimensions from a primitive cost function. The framework models physical space as a discrete ledger of recognition events, and this theorem provides a key technical tool: a way to solve for a source field given its Laplacian on a periodic carrier. The theorem is proved in the framework's machine-checked library of formal theorems, meaning the logical steps have been verified by a computer. This is a mathematical fact about a specific discrete operator, not a statement about the physical universe.

The declaration is careful about what it does not claim. It does not identify the periodic torus with the finite open box or with the infinite Fourier readout used elsewhere in the framework. It does not assert a finite-volume convergence theorem, meaning it does not claim that results on this finite grid carry over to the infinite continuum. The shift-eigenmode equations, which describe how waves behave under translations, remain hypotheses in the module. The theorem is a statement about a defined mathematical object, not a physical law.

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

/-- Explicit source reconstruction by the nonzero inverse modes.

This is a hypothesis interface. It does not assert that the displayed
finite sum is an inverse transform for every source. -/
def torusSourceReconstructedByNonzeroModes
    {N : ℕ} [NeZero N] (rho : TorusSite3 N → ℂ) : Prop :=
  ∀ p : TorusSite3 N,
    rho p = (∑ m ∈ torusNonzeroModes N,
      torusSourceTransform rho m * torusFourierMode m p)

/-- The zero-mode-excluded finite spectral response of a source. -/
noncomputable def torusSpectralResponse
    {N : ℕ} [NeZero N] (rho : TorusSite3 N → ℂ) :
    TorusSite3 N → ℂ :=
  fun p => (∑ m ∈ torusNonzeroModes N,
    torusSourceTransform rho m * torusSpectralGreenMode m p)

What this page does not claim

The theorem does not identify the finite periodic torus with the finite open box or the infinite Fourier readout. The theorem does not assert a finite-volume convergence theorem connecting the discrete result to a continuum. The shift-eigenmode equations are hypotheses, not proved theorems, in this module.

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: