Foundation Pair Kernel Periodic3 Torus Laplacian Torus Fourier Mode Eq Symbol Mu

The finite torus Laplacian

The discrete Laplacian is the standard way to measure how much a function at a point differs from the average of its neighbors. On a finite three-dimensional torus, a grid whose edges wrap around, each point has six neighbors: two along each of the three axes. The declaration in question establishes that when this operator acts on a Fourier mode, a complex exponential wave that fits the periodic grid, the result is that same mode multiplied by a scalar. That scalar is the Fourier symbol, a number that depends only on the wave's frequency. The operator does not mix modes; it simply scales each one.

This is the discrete analogue of a classical fact about the continuous Laplacian, where exponentials are eigenfunctions. The proof is a direct computation: shifting a Fourier mode by one step multiplies it by a root of unity, and the three pairs of shifts combine to produce the symbol. The result holds for every mode index and every positive grid size N, with no regularity assumptions needed because the space is finite. The library, a machine-checked collection of formal theorems, records this as a proved identity.

In Recognition Science, this identity is part of a larger construction. The framework models a discrete ledger, a record of events on a finite periodic grid, and uses the Fourier modes to analyze how a source distributes over the grid. The Laplacian appears as the operator that links a source to its response. This particular theorem is a technical workhorse: it justifies why the spectral method, solving problems by working in the frequency domain, is valid on the torus. It is the step that lets the framework invert the Laplacian mode by mode.

The theorem does not claim that the periodic carrier is the same as a finite open box or the infinite Fourier readout. It does not assert that solutions on the torus converge to solutions on the infinite lattice as the grid grows. The shift-eigenmode equations, which would connect this operator to the framework's recognition dynamics, remain hypotheses in the source. The identity is a statement about the finite torus alone, a clean algebraic fact that holds exactly as written.

/-- 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 theorem does not identify the finite periodic carrier with the finite open box or the infinite Fourier readout. It does not assert a finite-volume convergence theorem. It does not establish the physical recognition-to-linking bridge.

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: