Foundation Pair Kernel Finite Heisenberg Weyl Event Operator Axis Weyl Relation2

A finite Weyl relation

The Weyl relation is a standard piece of quantum mechanics: it says that a position shift and a momentum boost do not commute, and that the failure of commutation is a fixed phase factor. On a finite grid the relation takes a discrete form. The declaration axis_weyl_relation27 proves that on a torus with exactly 27 sites, built from three coordinates each taking three values, the shift operator and the clock operator obey this relation on every axis. Concretely, for any complex-valued state on the grid, shifting first and then applying the clock phase gives the same result as applying the clock first and then shifting, multiplied by the cube root of unity omega3. The proof is machine-checked, with no unproved assumptions.

The 27-site carrier is not arbitrary. Each site is a triple of coordinates in the field ZMod 3, so the total count is 3^3 = 27. The shift operator moves a state one step backward along a chosen axis. The clock operator multiplies the state at each site by a power of omega3, the primitive cube root of unity. The theorem states that for every axis and every site, clockAxis27 (shiftAxis27 ψ axis) axis site equals omega3 times shiftAxis27 (clockAxis27 ψ axis) axis site. This is the exact finite analogue of the continuous relation between position and momentum operators.

The declaration is part of a larger construction in the framework's machine-checked library of formal theorems. The construction defines a primary action, a real-valued quantity built from shift mismatches and clock displacements, with no free coefficients. The response and operator are then defined as first and second derivatives of that action. The framework proves the action is nonnegative and that the response and operator arise from it. The Weyl relation is one of the certified properties of this construction.

What the declaration does not claim is as important as what it proves. The Weyl relation is a theorem about the operators on the finite grid. It does not say that the specific action, the equal weighting of shift and clock terms, or the choice of clock center is forced by recognition theory. The framework's own documentation marks the primary action as a model, a definitional choice, not a derived necessity. The relation holds for the defined operators, but the definition itself is not claimed to be unique or physically inevitable.

The practical consequence is that the finite grid supports a consistent quantum-like structure: shifts and clocks interact exactly as in the continuous Weyl algebra, but on a discrete carrier of 27 points. This gives the framework a concrete, finite toy model in which the algebraic heart of quantum mechanics survives. The model is a tool for further exploration, not a claim about the physical world. The relation itself is proved; its physical interpretation remains open.

/-- Exact finite Weyl relation on every production-torus axis. -/
theorem axis_weyl_relation27
    (ψ : WeylEventSite27 → ℂ)
    (axis : Fin 3)
    (site : WeylEventSite27) :
    clockAxis27 (shiftAxis27 ψ axis) axis site =
      omega3 * shiftAxis27 (clockAxis27 ψ axis) axis site := by
  have hval :
      ∀ j : ZMod 3,
        j.val = (j - 1).val + 1 ∨
          (j.val = 0 ∧ (j - 1).val = 2) := by
    decide
  have e :
      omega3 ^ (site axis).val =
        omega3 ^ ((site axis - 1).val + 1) := by
    rcases hval (site axis) with h | ⟨h0, h2⟩
    · rw [h]
    · rw [h0, h2, pow_zero]
      exact omega3_pow_three.symm
  simp only [clockAxis27, shiftAxis27, shiftSite27]
  simp only [Function.update_self]
  rw [e]
  simp [pow_succ, mul_comm, mul_assoc, mul_left_comm]

theorem weylEventSite27_card :
    Nat.card WeylEventSite27 = 27 := by
  change Nat.card (Fin 3 → ZMod 3) = 27
  rw [Nat.card_fun, Nat.card_zmod, Nat.card_fin]
  norm_num

theorem finiteWeylEventAction27_nonneg
    (center : WeylEventSite27)
    (ψ : WeylEventAmplitude27) :
    0 ≤ finiteWeylEventAction27 center ψ := by
  unfold finiteWeylEventAction27
  apply Finset.sum_nonneg
  intro axis _
  apply Finset.sum_nonneg
  intro site _
  exact add_nonneg (sq_nonneg _)
    (mul_nonneg (Complex.normSq_nonneg _) (sq_nonneg _))

theorem sourceResponse_from_primary_action27
    (center : WeylEventSite27)
    (ψ variation : WeylEventAmplitude27) :
    finiteWeylEventSourceResponse27 center ψ variation =
      deriv
        (fun t : ℝ =>
          finiteWeylEventAction27 center
            (fun site => ψ site + t * variation site))
        0 := rfl

theorem operator_from_source_response27
    (center : WeylEventSite27)
    (i j : WeylEventSite27) :
    finiteWeylEventOperatorEntry27 center i j =
      (1 / 2 : ℝ) *
        deriv
          (fun t : ℝ =>
            finiteWeylEventSourceResponse27 center
              (fun site => t * weylSiteBasis27 j site)
              (weylSiteBasis27 i))
          0 := rfl

/-- Coefficient-free self-dual Weyl action. -/
def finiteWeylEventAction27
    (center : WeylEventSite27)
    (ψ : WeylEventAmplitude27) : ℝ :=
  Finset.univ.sum fun axis : Fin 3 =>
    Finset.univ.sum fun site : WeylEventSite27 =>
      (ψ (shiftSite27 axis site) - ψ site) ^ 2 +
        clockDisplacement27 center axis site * (ψ site) ^ 2

What this page does not claim

The specific action with equal shift and clock weights is not forced by recognition theory. The clock center is not shown to be a realized posting endpoint. No continuum limit or dimensioned radius is derived from the finite construction.

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