Foundation Pair Kernel Weyl Self Dual Continuum Scale Weyl Self Dual Continuum S

The reciprocal scale

When you work with a finite set of equally spaced samples, position and frequency become reciprocal: the finer the mesh in one domain, the coarser it is in the other. This is the discrete Fourier relationship that underlies digital signal processing and lattice calculations. The Recognition Science framework formalizes this reciprocity in a machine-checked library of formal theorems, and its declaration weylSelfDualContinuumScale_cert establishes a precise uniqueness result about the scale that balances the two domains.

The statement is conditional. For any positive integer N, representing the number of phases or samples in the finite Fourier pair, the framework defines a mesh coordinate. A positive mesh coordinate is self-dual exactly when N times the square of the mesh scale equals 1. This equation forces the mesh scale to be 1 divided by the square root of N. The certificate proves three things together: that this value is positive, that it satisfies the balancing equation, and that it is the unique positive solution. In symbols, the condition is N · s² = 1, and the unique solution is s = 1/√N.

The uniqueness theorem is exact within its stated premises. The certificate proves that if a positive real number balances the finite Fourier carrier with its reciprocal carrier, then that number must be the square root reciprocal. This is a theorem in the framework's library, proved without gaps or unstated assumptions. The proof is constructive: the certificate assembles the positivity, the balance condition, and the uniqueness argument into a single scoped structure.

What the certificate does not claim is equally important. It does not assert that this scale corresponds to any physical length. The framework explicitly states that the Fourier exchange-invariance premise is not proved on the present Recognition surface, and no dimensioned event-length unit is supplied. The construction therefore yields a canonical relative continuum chart, not an atomic radius or any measurable distance. It is a mathematical scaling relationship between two reciprocal representations, not a claim about the size of anything in the physical world.

The consequence is that the framework has a clean, exact statement about relative scaling in finite Fourier systems, with the boundary of its applicability drawn explicitly. A reader can rely on the uniqueness result within its conditional scope, and know precisely where the mathematical certainty ends and the open question of physical interpretation begins.

/-- Positive coordinate scale balancing a finite Fourier carrier with its
reciprocal carrier. -/
def SelfDualWeylMeshBalance (N : ℕ) (meshScale : ℝ) : Prop :=
  0 < meshScale ∧ (N : ℝ) * meshScale ^ 2 = 1

theorem selfDualWeylMeshScale_balance
    (N : ℕ) (hN : 0 < N) :
    SelfDualWeylMeshBalance N
      (selfDualWeylMeshScale N) := by
  constructor
  · exact selfDualWeylMeshScale_pos N hN
  · unfold selfDualWeylMeshScale
    have hN0 : (N : ℝ) ≠ 0 := by positivity
    have hsqrt0 : Real.sqrt (N : ℝ) ≠ 0 := by positivity
    rw [one_div, inv_pow]
    field_simp
    exact (Real.sq_sqrt
      (show (0 : ℝ) ≤ (N : ℝ) by
        exact_mod_cast Nat.zero_le N)).symm

theorem weylSelfDualContinuumScale_cert
    (N : ℕ) (hN : 0 < N) :
    WeylSelfDualContinuumScaleCert N hN where
  scale_positive := selfDualWeylMeshScale_pos N hN
  scale_balanced := selfDualWeylMeshScale_balance N hN
  scale_unique :=
    fun meshScale =>
      selfDualWeylMeshBalance_unique N hN meshScale

What this page does not claim

The certificate does not establish any physical length or atomic radius. The Fourier exchange-invariance premise is not proved on the present Recognition surface. No dimensioned event-length unit is supplied by this declaration.

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: