Foundation Pair Kernel Weyl Full Fourier Exchange

The Fourier exchange

The Fourier transform is a tool that rewrites a signal as a sum of smooth waves. It is one of the most widely used operations in science, from audio compression to quantum mechanics. In the Recognition Science framework, a discrete version of this transform acts on a small object: an amplitude defined on three positions, numbered 0, 1, and 2. The framework's library of formal proofs establishes a striking exchange property about this transform.

To see the property, one needs two ways of measuring a cost on the three-position amplitude. The first, called the shift cost, sums the squared sizes of the amplitude at two positions while leaving the third out. The second, called the clock cost, does the same but after rotating which position is left out. Both are examples of an occupation cost, a number that measures how much of the amplitude sits at each position. The library proves that applying the Fourier transform swaps these two costs and multiplies by three: the shift cost of the transformed amplitude equals three times the clock cost of the original, and vice versa.

This exchange is not an accident of the definitions. The library proves it as a result, with no gaps and no extra assumptions. The proof uses the cube root of unity, the complex number omega3, whose square and cube have simple values. It also uses the fact that rotating the amplitude, which cyclically shifts its positions, leaves the shift cost unchanged. These ingredients combine to show that the exchange holds for every amplitude, not just for special ones.

The result matters because it closes the mathematics behind a proposed physical law. The framework's self-dual posting law says that a certain weighted sum of the two costs should be unchanged by the Fourier transform. The exchange property proves that this law holds exactly, with the factor three appearing naturally. The choice of that law as physical, however, is a separate modeling decision, not a proven result. The library keeps that distinction explicit.

In plain language, the module shows that the Fourier transform and the two cost measurements fit together like two sides of the same coin. Transform first, then measure one cost, and you get the same number as measuring the other cost first, then transforming. The factor three is the price of the exchange. This is a clean, checkable fact, and it is now part of the framework's foundation.

/-- Unnormalized cubic DFT sends shift cost to three times clock cost. -/
theorem shiftOccupationCostAxis3_dft
    (ψ : WeylAxisAmplitude3) :
    shiftOccupationCostAxis3 (finiteDFTAxis3 ψ) =
      3 * clockOccupationCostAxis3 ψ := by
  simp only [shiftOccupationCostAxis3,
    clockOccupationCostAxis3]
  rw [finiteDFTAxis3_apply_zero, finiteDFTAxis3_apply_one,
    finiteDFTAxis3_apply_two]
  refine ofReal_injective ?_
  simp only [ofReal_add, ofReal_mul, ofReal_ofNat,
    normSq_eq_conj_mul_self]
  simp only [map_add, map_mul, map_sub, omega3_star,
    omega3_sq_star]
  simp only [omega3_sq_eq, sub_eq_add_neg]
  ring_nf
  simp [omega3_sq_eq]
  ring

/-- Unnormalized cubic DFT sends clock cost to three times shift cost. -/
theorem clockOccupationCostAxis3_dft
    (ψ : WeylAxisAmplitude3) :
    clockOccupationCostAxis3 (finiteDFTAxis3 ψ) =
      3 * shiftOccupationCostAxis3 ψ := by
  simp only [clockOccupationCostAxis3]
  linarith [dft_normSq_pair_eq_shift ψ]

theorem shiftOccupationCostAxis3_rotate
    (center : ZMod 3)
    (ψ : WeylAxisAmplitude3) :
    shiftOccupationCostAxis3
        (rotateAmplitudeAxis3 center ψ) =
      shiftOccupationCostAxis3 ψ := by
  fin_cases center
  · simp [rotateAmplitudeAxis3,
      shiftOccupationCostAxis3, add_zero]
  · have h0 : ((0 : ZMod 3) + 1) = 1 := by
      decide
    have h1 : ((1 : ZMod 3) + 1) = 2 :=
      zmod3_one_add_one
    have h2 : ((2 : ZMod 3) + 1) = 0 :=
      zmod3_two_add_one
    simp [rotateAmplitudeAxis3,
      shiftOccupationCostAxis3, h0, h1, h2]
    ring
  · have h0 : ((0 : ZMod 3) + 2) = 2 := by
      decide
    have h1 : ((1 : ZMod 3) + 2) = 0 :=
      zmod3_one_add_two
    have h2 : ((2 : ZMod 3) + 2) = 1 :=
      zmod3_two_add_two
    simp [rotateAmplitudeAxis3,
      shiftOccupationCostAxis3, h0, h1, h2]
    ring

def twoWeightOccupationCostAxis3At
    (center : ZMod 3)
    (shiftWeight clockWeight : ℝ)
    (ψ : WeylAxisAmplitude3) : ℝ :=
  shiftWeight * shiftOccupationCostAxis3 ψ +
    clockWeight * clockOccupationCostAxis3At center ψ

What this page does not claim

The Fourier exchange theorem does not prove that the self-dual posting law is physically correct. The module does not derive any numerical constant of nature. The exchange property is proved only for the three-position case, not for arbitrary sizes.

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/PairKernelWeylFullFourierExchange.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: