Foundation Pair Kernel Local Generator Global Green Local Generator Global Green

The local and the global

In physics, some rules act locally, between neighbors, while other effects spread across an entire system. A ledger, a discrete record of events, on a three-dimensional grid can carry both kinds of structure at once. The declaration localGenerator_globalGreen_consumer is a machine-checked theorem in the framework's library of formal theorems that puts these two structures side by side and proves they are compatible.

The local side is a generator, a rule that assigns interaction weights between neighboring points. The theorem proves this generator is finite range: each point only feels the six points directly adjacent to it in the grid. The global side is a Green's function, a standard tool that gives the response to a source spread across the whole system. Here the response is built by summing over every nonzero Fourier mode, the basic wave patterns of the grid, so no point is excluded from the calculation.

The theorem's content is a single equation. When the local generator acts on the global response to a dipole source, a source with one positive and one negative charge, it reproduces that source exactly. In symbols: the Laplacian of the Green response equals the dipole source. This holds for any source scale, and the theorem is proved with no unproven assumptions, no sorry and no new axioms.

What the theorem does not claim is just as important as what it proves. The global response is deliberately not assigned a finite-range predicate: it is not claimed to be local. The theorem works with the canonical torus Laplacian, a specific standard operator, not with an arbitrary graph. The bridge between the local generator and that canonical operator, identifying them as the same object, remains an open target in the framework. The declaration is a consumer, a test that the two pieces compile together, not a proof that they are one.

The practical consequence is that the framework can hold a local rule and a global response in the same formal space without contradiction. A reader can inspect the type separation directly: the generator is local by proof, the response is global by definition. The remaining seam, connecting the arbitrary graph G to the canonical operator, is a named open problem, not a hidden assumption.

/-- **Compiling downstream consumer.** The D=3 action generator is local while
its normalized spectral inverse solves the globally represented source
equation. Source scale is explicit and no response-range conclusion is made. -/
theorem localGenerator_globalGreen_consumer
    {N : ℕ} [NeZero N]
    (sourceScale : ℂ) (a b p : TorusSite3 N) :
    FiniteRangeOn
        (lattice3Generator N).graph (encodedDist3 N) 1 ∧
      torusLaplacian
          (scaledDipoleGreenResponse sourceScale a b) p =
        scaledTorusDipole sourceScale a b p := by
  refine ⟨lattice3Generator_finiteRangeOn N, ?_⟩
  unfold scaledDipoleGreenResponse
  apply
    torusLaplacian_torusSpectralResponseNormalized_eq_source_of_reconstructed
  exact
    torusSourceReconstructedByNonzeroModesNormalized_of_neutral _
      (scaledTorusDipole_neutral sourceScale a b)

/-- **Compiling downstream consumer.** The D=3 action generator is local while
its normalized spectral inverse solves the globally represented source
equation. Source scale is explicit and no response-range conclusion is made. -/
theorem localGenerator_globalGreen_consumer
    {N : ℕ} [NeZero N]
    (sourceScale : ℂ) (a b p : TorusSite3 N) :
    FiniteRangeOn
        (lattice3Generator N).graph (encodedDist3 N) 1 ∧
      torusLaplacian
          (scaledDipoleGreenResponse sourceScale a b) p =
        scaledTorusDipole sourceScale a b p := by
  refine ⟨lattice3Generator_finiteRangeOn N, ?_⟩
  unfold scaledDipoleGreenResponse
  apply
    torusLaplacian_torusSpectralResponseNormalized_eq_source_of_reconstructed
  exact
    torusSourceReconstructedByNonzeroModesNormalized_of_neutral _
      (scaledTorusDipole_neutral sourceScale a b)

/-- Global response to the scaled dipole. The normalized spectral inverse
sums all nonzero Fourier modes; it is deliberately not assigned a
`FiniteRangeOn` predicate. -/
def scaledDipoleGreenResponse {N : ℕ} [NeZero N]
    (sourceScale : ℂ) (a b : TorusSite3 N) :
    TorusSite3 N → ℂ :=
  torusSpectralResponseNormalized (scaledTorusDipole sourceScale a b)

What this page does not claim

The theorem does not claim the global response is local. The theorem does not identify the arbitrary graph G with the canonical torus Laplacian. The theorem does not prove 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/PairKernelLocalGeneratorGlobalGreen.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: