A.8 Why the coordinate certificates mean complex identities
On this page · Permalink · Source line 291
The semantics map is explicitly defined with the positive real square root. Soundness for addition, multiplication, conjugation, powers, and finite sums prevents the exact coordinate layer from being a detached calculation with an unproved interpretation.
Literal source. SemanticBridge.lean, physical lines 14–56.
/-- The exact coordinate arithmetic is interpreted in the ordinary complex numbers. -/
noncomputable def interpret (x : Cyclo12) : ℂ :=
⟨(x.a : ℝ) + (x.b : ℝ) * Real.sqrt 3,
(x.c : ℝ) + (x.d : ℝ) * Real.sqrt 3⟩
@[simp] theorem interpret_zero : interpret cZero = 0 := by
apply Complex.ext <;> simp [interpret, cZero]
@[simp] theorem interpret_one : interpret cOne = 1 := by
apply Complex.ext <;> simp [interpret, cOne]
@[simp] theorem interpret_rat (r : ℚ) : interpret (cRat r) = (r : ℂ) := by
apply Complex.ext <;> simp [interpret, cRat]
@[simp] theorem interpret_add (x y : Cyclo12) :
interpret (cAdd x y) = interpret x + interpret y := by
apply Complex.ext <;> simp [interpret, cAdd] <;> ring
@[simp] theorem interpret_mul (x y : Cyclo12) :
interpret (cMul x y) = interpret x * interpret y := by
apply Complex.ext <;> simp [interpret, cMul, Complex.mul_re, Complex.mul_im] <;>
ring_nf <;> norm_num [Real.sq_sqrt]
@[simp] theorem interpret_conj (x : Cyclo12) :
interpret (cConj x) = star (interpret x) := by
apply Complex.ext <;> simp [interpret, cConj]
ring
@[simp] theorem interpret_pow (x : Cyclo12) (n : Nat) :
interpret (cPow x n) = interpret x ^ n := by
induction n with
| zero => simp [cPow]
| succ n ih => simp [cPow, ih, pow_succ]
@[simp] theorem interpret_sum (xs : List Cyclo12) :
interpret (cSum xs) = (xs.map interpret).sum := by
induction xs with
| nil => simp [cSum]
| cons x xs ih => simp [cSum, ih]
@[simp] theorem interpret_kSum (f : Index → Cyclo12) :
interpret (kSum f) = ∑ i, interpret (f i) := by
simp only [kSum, interpret_sum, List.map_ofFn, List.sum_ofFn]The multiplication proof uses complex extensionality, real polynomial normalization, and the square-root identity. It proves preservation for arbitrary coordinates, not merely for the handful of roots that occur in the example. The power and finite-sum proofs use induction.
Injectivity of this interpretation is not needed to transfer an equality: if two coordinate expressions are proved equal, applying the interpretation gives equal complex expressions. No claim of a globally packaged field equivalence is required by the theorem chain.