A.6 The exact phase arithmetic
On this page · Permalink · Source line 175
The structure Cyclo12 represents
Its multiplication explicitly incorporates \((\sqrt3)^2=3\) and \(i^2=-1\). It is a concrete arithmetic representation. The development does not need or install a global field instance to certify the finite example.
Literal source. QuantumArithmeticBridge.lean, physical lines 130–141.
/--
An exact coordinate model for Q(sqrt(3), i). The tuple (a,b,c,d) denotes
a + b*sqrt(3) + i*(c + d*sqrt(3)).
Only the concrete arithmetic needed for the q=12 certificate is used below;
we do not install a global field instance.
-/
structure Cyclo12 where
a : ℚ
b : ℚ
c : ℚ
d : ℚ
deriving DecidableEq, ReprLiteral source. QuantumArithmeticBridge.lean, physical lines 155–173.
/-- Multiplication in Q(sqrt(3), i). -/
def cMul (x y : Cyclo12) : Cyclo12 :=
⟨x.a*y.a + 3*x.b*y.b - x.c*y.c - 3*x.d*y.d,
x.a*y.b + x.b*y.a - x.c*y.d - x.d*y.c,
x.a*y.c + 3*x.b*y.d + x.c*y.a + 3*x.d*y.b,
x.a*y.d + x.b*y.c + x.c*y.b + x.d*y.a⟩
def cConj (x : Cyclo12) : Cyclo12 := ⟨x.a, x.b, -x.c, -x.d⟩
def cPow (x : Cyclo12) : Nat → Cyclo12
| 0 => cOne
| n + 1 => cMul (cPow x n) x
def cSum : List Cyclo12 → Cyclo12
| [] => cZero
| x :: xs => cAdd x (cSum xs)
/-- zeta = exp(2*pi*i/12) = sqrt(3)/2 + i/2. -/
def zeta12 : Cyclo12 := ⟨0, (1/2 : ℚ), (1/2 : ℚ), 0⟩The phase \(\zeta=(0,1/2,1/2,0)\) has complex meaning \(\sqrt3/2+i/2\). Exact finite certificates establish its twelfth power, inverse, and absence of a smaller positive power below twelve. Later the convention module identifies it with \(\exp(\pi i/6)\).
The Ramanujan vector is obtained by summing powers of this phase over \(1,5,7,11\). The negative-sign unnormalized DFT has value 12 at these four frequencies and zero elsewhere. The absolute-value vector has Fourier support on the even frequencies instead. These are exact phase calculations over rational coordinates.