Foundation Pair Kernel Finite Heisenberg Weyl Event Operator Omega3 Pow Three

The cubic phase

The number omega3 is the complex cube root of unity: the number whose third power is exactly 1. In the complex plane it is the point at 120 degrees on the unit circle, written as exp(2πi/3). The theorem omega3_pow_three establishes precisely this identity, omega3³ = 1, in the framework's machine-checked library of formal theorems. That is its entire content: a plain algebraic fact about a standard constant, proved from the definition of omega3 and the periodicity of the complex exponential.

The fact matters because the framework uses omega3 as the phase for a clock on a finite 27-site torus. A site is a three-coordinate address, each coordinate taking one of three values, so 3³ = 27 sites in total. On each axis, the clock multiplies an amplitude by omega3 raised to the coordinate value. The theorem omega3_pow_three guarantees that after three steps of the clock on any axis, the phase returns to its starting value. That periodicity is what makes the clock consistent on the torus: a shift of three positions on an axis is the identity, and the phase repeats with the same period.

In Recognition Science, this clock is part of a model for a discrete event operator. The framework defines a primary action as the sum of a shift mismatch and a clock mismatch across the three axes, with no free coefficients. The source response is the first derivative of that action, and the operator is its second derivative. The theorem omega3_pow_three is a supporting lemma inside this construction; it certifies the clock's periodicity but says nothing about whether the action is physically forced. The framework's own documentation is explicit: the equal shift/clock weight and this action as the molecular action are MODEL choices, not derived results.

What the theorem does not claim is as important as what it proves. It does not assert that the 27-site torus is the unique carrier, nor that the action is the unique self-dual action, nor that the clock center is a realized posting endpoint. It does not introduce any empirical constant, and it does not derive a dimensioned continuum radius. The theorem is a narrow algebraic identity, fully proved, that supports a broader model whose physical status remains open.

theorem omega3_pow_three : omega3 ^ 3 = 1 := by
  have h : omega3 ^ 3 =
      Complex.exp (2 * Real.pi * Complex.I) := by
    rw [omega3, ← Complex.exp_nat_mul]
    congr 1
    push_cast
    ring
  rw [h, Complex.exp_two_pi_mul_I]

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

/-- 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 theorem does not assert that the 27-site torus is the unique carrier for the event operator. The theorem does not derive the action as the unique self-dual action; the action is a MODEL choice. The theorem introduces no empirical constant and no dimensioned continuum radius.

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: