Foundation Pair Kernel Weyl Self Dual Continuum Scale

The self-dual mesh

The finite Fourier transform pairs a set of N position samples with N frequency samples. In this pairing, position and frequency coordinates are reciprocal: a fine mesh in one domain means a coarse mesh in the other. A mesh coordinate is self-dual when it balances the two domains exactly, so that the product of the mesh scale with itself, times the number of phases N, equals 1. That single condition forces the mesh scale to be 1 over the square root of N. For N equal to 4, the self-dual scale is one half; for N equal to 9, it is one third. The uniqueness is exact: no other positive scale satisfies the balance equation.

The classical story of this scale goes back to the uncertainty principle, where the product of spreads in position and frequency has a fixed lower bound. The finite Fourier transform realizes the same tension in discrete form, and the self-dual scale is the point where the two spreads match. This is the scale at which a signal and its transform occupy the same relative width. It appears in signal processing as the critical sampling rate, and in quantum mechanics as the scale of a coherent state. The balance equation N times meshScale squared equals 1 is the discrete analogue of the continuous relation between a variable and its conjugate momentum.

In Recognition Science, the framework models this balance as a ledger, a discrete record of paired events. The framework constructs a canonical relative continuum chart from the finite Fourier balance, meaning it builds a coordinate system that is self-consistent under the exchange of position and frequency. The framework proves that the self-dual scale is unique, that it is positive for any positive N, and that it satisfies the balance condition. These are exact theorems in the machine-checked library of formal theorems. The framework does not claim that this scale is a physical length: the proof does not establish the Fourier exchange-invariance premise, and no dimensioned unit of event length is supplied.

The consequence is a relative chart, not an atomic radius. The scale 1 over the square root of N is a normalization that makes the finite Fourier pair self-consistent, and it is the only such normalization. This gives a canonical way to compare scales across different N, without committing to any absolute unit. The framework's certificate bundles the three properties, positivity, balance, and uniqueness, into a single scope certificate for the relative chart. What a reader can now see is that the finite Fourier balance is not arbitrary: it has exactly one self-dual point, and that point is the geometric mean of the two domains.

/-- Finite-Fourier self-duality uniquely fixes the relative mesh exponent and
normalization. -/
theorem selfDualWeylMeshBalance_unique
    (N : ℕ) (hN : 0 < N)
    (meshScale : ℝ)
    (hbalance : SelfDualWeylMeshBalance N meshScale) :
    meshScale = selfDualWeylMeshScale N := by
  rcases hbalance with ⟨hmesh, hsq⟩
  have hcanonical :=
    selfDualWeylMeshScale_balance N hN
  rcases hcanonical with ⟨hcanonical_pos, hcanonical_sq⟩
  have hN0 : (N : ℝ) ≠ 0 := by positivity
  have hsquares :
      meshScale ^ 2 =
        selfDualWeylMeshScale N ^ 2 := by
    apply (mul_left_cancel₀ hN0)
    rw [hsq, hcanonical_sq]
  nlinarith

theorem selfDualWeylMeshScale_pos
    (N : ℕ) (hN : 0 < N) :
    0 < selfDualWeylMeshScale N := by
  unfold selfDualWeylMeshScale
  positivity

/-- Scope certificate for the relative chart. -/
structure WeylSelfDualContinuumScaleCert (N : ℕ) (hN : 0 < N) : Prop where
  scale_positive :
    0 < selfDualWeylMeshScale N
  scale_balanced :
    SelfDualWeylMeshBalance N (selfDualWeylMeshScale N)
  scale_unique :
    ∀ meshScale,
      SelfDualWeylMeshBalance N meshScale →
        meshScale = selfDualWeylMeshScale N
  -- Absent by design (were typed `True`, so disciplined nothing):
  -- status_fourier_exchange_from_recognition_open (OPEN ledger status);
  -- status_relative_not_dimensioned (unit interpretation of the relative
  --   chart, not a kernel equation).

What this page does not claim

The self-dual scale is not a measured physical length. The framework does not prove the Fourier exchange-invariance premise. The uniqueness theorem does not apply to continuous Fourier transforms without a finite carrier.

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