structure FUST.FrourioAlgebra.GoldenEisensteinInt : Type

ℤ[φ,ζ₆]: a + bφ + cζ₆ + dφζ₆

• a : ℤ
• b : ℤ
• c : ℤ
• d : ℤ

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.ext_iff {x y : GoldenEisensteinInt} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.c = y.c ∧ x.d = y.d

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.ext {x y : GoldenEisensteinInt} (a : x.a = y.a) (b : x.b = y.b) (c : x.c = y.c) (d : x.d = y.d) : x = y

instance FUST.FrourioAlgebra.instDecidableEqGoldenEisensteinInt : DecidableEq GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.instDecidableEqGoldenEisensteinInt = FUST.FrourioAlgebra.instDecidableEqGoldenEisensteinInt.decEq

def FUST.FrourioAlgebra.instDecidableEqGoldenEisensteinInt.decEq (x✝ x✝¹ : GoldenEisensteinInt) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

instance FUST.FrourioAlgebra.instReprGoldenEisensteinInt : Repr GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.instReprGoldenEisensteinInt = { reprPrec := FUST.FrourioAlgebra.instReprGoldenEisensteinInt.repr }

def FUST.FrourioAlgebra.instReprGoldenEisensteinInt.repr : GoldenEisensteinInt → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def FUST.FrourioAlgebra.GoldenEisensteinInt.zero : GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.zero = { a := 0, b := 0, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.one : GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.one = { a := 1, b := 0, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.add (x y : GoldenEisensteinInt) : GoldenEisensteinInt

Equations

• x.add y = { a := x.a + y.a, b := x.b + y.b, c := x.c + y.c, d := x.d + y.d }

def FUST.FrourioAlgebra.GoldenEisensteinInt.neg (x : GoldenEisensteinInt) : GoldenEisensteinInt

Equations

• x.neg = { a := -x.a, b := -x.b, c := -x.c, d := -x.d }

def FUST.FrourioAlgebra.GoldenEisensteinInt.sub (x y : GoldenEisensteinInt) : GoldenEisensteinInt

Equations

• x.sub y = x.add y.neg

def FUST.FrourioAlgebra.GoldenEisensteinInt.mul (x y : GoldenEisensteinInt) : GoldenEisensteinInt

Multiplication using φ²=φ+1, ζ₆²=ζ₆-1

Equations

• One or more equations did not get rendered due to their size.

Ring axioms

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.add_comm' (x y : GoldenEisensteinInt) : x.add y = y.add x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.add_assoc' (x y z : GoldenEisensteinInt) : (x.add y).add z = x.add (y.add z)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.zero_add' (x : GoldenEisensteinInt) : zero.add x = x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.add_zero' (x : GoldenEisensteinInt) : x.add zero = x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.neg_add_cancel' (x : GoldenEisensteinInt) : x.neg.add x = zero

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.mul_comm' (x y : GoldenEisensteinInt) : x.mul y = y.mul x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.mul_assoc' (x y z : GoldenEisensteinInt) : (x.mul y).mul z = x.mul (y.mul z)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.one_mul' (x : GoldenEisensteinInt) : one.mul x = x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.mul_one' (x : GoldenEisensteinInt) : x.mul one = x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.left_distrib' (x y z : GoldenEisensteinInt) : x.mul (y.add z) = (x.mul y).add (x.mul z)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.right_distrib' (x y z : GoldenEisensteinInt) : (x.add y).mul z = (x.mul z).add (y.mul z)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.zero_mul' (x : GoldenEisensteinInt) : zero.mul x = zero

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.mul_zero' (x : GoldenEisensteinInt) : x.mul zero = zero

Scalar multiplication

def FUST.FrourioAlgebra.GoldenEisensteinInt.nsmul : ℕ → GoldenEisensteinInt → GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.nsmul 0 x✝ = FUST.FrourioAlgebra.GoldenEisensteinInt.zero
• FUST.FrourioAlgebra.GoldenEisensteinInt.nsmul n.succ x✝ = (FUST.FrourioAlgebra.GoldenEisensteinInt.nsmul n x✝).add x✝

def FUST.FrourioAlgebra.GoldenEisensteinInt.zsmul : ℤ → GoldenEisensteinInt → GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.zsmul (Int.ofNat n) x✝ = FUST.FrourioAlgebra.GoldenEisensteinInt.nsmul n x✝
• FUST.FrourioAlgebra.GoldenEisensteinInt.zsmul (Int.negSucc n) x✝ = (FUST.FrourioAlgebra.GoldenEisensteinInt.nsmul (n + 1) x✝).neg

def FUST.FrourioAlgebra.GoldenEisensteinInt.npow : ℕ → GoldenEisensteinInt → GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.npow 0 x✝ = FUST.FrourioAlgebra.GoldenEisensteinInt.one
• FUST.FrourioAlgebra.GoldenEisensteinInt.npow n.succ x✝ = (FUST.FrourioAlgebra.GoldenEisensteinInt.npow n x✝).mul x✝

def FUST.FrourioAlgebra.GoldenEisensteinInt.natCast : ℕ → GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.natCast n = { a := ↑n, b := 0, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.intCast : ℤ → GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.intCast (Int.ofNat n) = { a := ↑n, b := 0, c := 0, d := 0 }
• FUST.FrourioAlgebra.GoldenEisensteinInt.intCast (Int.negSucc n) = { a := -(↑n + 1), b := 0, c := 0, d := 0 }

instance FUST.FrourioAlgebra.GoldenEisensteinInt.instNatCast : NatCast GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.instNatCast = { natCast := FUST.FrourioAlgebra.GoldenEisensteinInt.natCast }

instance FUST.FrourioAlgebra.GoldenEisensteinInt.instIntCast : IntCast GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.instIntCast = { intCast := FUST.FrourioAlgebra.GoldenEisensteinInt.intCast }

CommRing instance

instance FUST.FrourioAlgebra.GoldenEisensteinInt.instCommRing : CommRing GoldenEisensteinInt

Equations

• One or more equations did not get rendered due to their size.

Embedding into ℂ

noncomputable def FUST.FrourioAlgebra.GoldenEisensteinInt.toComplex (x : GoldenEisensteinInt) : ℂ

Equations

• x.toComplex = ↑x.a + ↑x.b * ↑FUST.φ + ↑x.c * FUST.ζ₆ + ↑x.d * ↑FUST.φ * FUST.ζ₆

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.toComplex_zero : zero.toComplex = 0

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.toComplex_one : one.toComplex = 1

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.toComplex_add (x y : GoldenEisensteinInt) : (x.add y).toComplex = x.toComplex + y.toComplex

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.toComplex_neg (x : GoldenEisensteinInt) : x.neg.toComplex = -x.toComplex

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.toComplex_mul (x y : GoldenEisensteinInt) : (x.mul y).toComplex = x.toComplex * y.toComplex

Galois automorphisms: Gal(ℚ(√5,√(-3))/ℚ) ≅ ℤ/2 × ℤ/2

def FUST.FrourioAlgebra.GoldenEisensteinInt.sigma (x : GoldenEisensteinInt) : GoldenEisensteinInt

σ: φ ↦ ψ (fixes ζ₆)

Equations

• x.sigma = { a := x.a + x.b, b := -x.b, c := x.c + x.d, d := -x.d }

def FUST.FrourioAlgebra.GoldenEisensteinInt.tau (x : GoldenEisensteinInt) : GoldenEisensteinInt

τ: ζ₆ ↦ ζ₆' = 1-ζ₆ (fixes φ)

Equations

• x.tau = { a := x.a + x.c, b := x.b + x.d, c := -x.c, d := -x.d }

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigma_add (x y : GoldenEisensteinInt) : (x.add y).sigma = x.sigma.add y.sigma

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigma_mul (x y : GoldenEisensteinInt) : (x.mul y).sigma = x.sigma.mul y.sigma

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigma_one : one.sigma = one

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigma_involution (x : GoldenEisensteinInt) : x.sigma.sigma = x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tau_add (x y : GoldenEisensteinInt) : (x.add y).tau = x.tau.add y.tau

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tau_mul (x y : GoldenEisensteinInt) : (x.mul y).tau = x.tau.mul y.tau

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tau_one : one.tau = one

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tau_involution (x : GoldenEisensteinInt) : x.tau.tau = x

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigma_tau_comm (x : GoldenEisensteinInt) : x.tau.sigma = x.sigma.tau

τ-Norm: x·τ(x) ∈ ℤ[φ]

def FUST.FrourioAlgebra.GoldenEisensteinInt.tauProduct (x : GoldenEisensteinInt) : GoldenEisensteinInt

Equations

• x.tauProduct = x.mul x.tau

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tauProduct_c_zero (x : GoldenEisensteinInt) : x.tauProduct.c = 0

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tauProduct_d_zero (x : GoldenEisensteinInt) : x.tauProduct.d = 0

def FUST.FrourioAlgebra.GoldenEisensteinInt.tauNorm (x : GoldenEisensteinInt) : GoldenInt

Project τ-product to ℤ[φ]

Equations

• x.tauNorm = { a := x.a * x.a + x.a * x.c + x.b * x.b + x.b * x.d + x.c * x.c + x.d * x.d, b := 2 * x.a * x.b + x.a * x.d + x.b * x.b + x.b * x.c + x.b * x.d + 2 * x.c * x.d + x.d * x.d }

def FUST.FrourioAlgebra.GoldenEisensteinInt.norm (x : GoldenEisensteinInt) : ℤ

Full norm: N(x) = N_{ℤ[φ]}(x·τ(x))

Equations

• x.norm = x.tauNorm.norm

σ-Norm: x·σ(x) ∈ ℤ[ζ₆]

The product x·σ(x) always has b=0, d=0, hence lies in the ℤ[ζ₆] sublattice. This gives the canonical projection ℤ[φ,ζ₆] → ℤ[ζ₆] removing scale structure.

def FUST.FrourioAlgebra.GoldenEisensteinInt.sigmaProduct (x : GoldenEisensteinInt) : GoldenEisensteinInt

Equations

• x.sigmaProduct = x.mul x.sigma

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigmaProduct_b_zero (x : GoldenEisensteinInt) : x.sigmaProduct.b = 0

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigmaProduct_d_zero (x : GoldenEisensteinInt) : x.sigmaProduct.d = 0

def FUST.FrourioAlgebra.GoldenEisensteinInt.sigmaNorm (x : GoldenEisensteinInt) : ℤ × ℤ

σ-norm projected to (ℤ × ℤ) ≅ ℤ[ζ₆], where (p, q) represents p + q·ζ₆

Equations

• x.sigmaNorm = (x.a ^ 2 + x.a * x.b - x.b ^ 2 - x.c ^ 2 - x.c * x.d + x.d ^ 2, 2 * x.a * x.c + x.a * x.d + x.b * x.c + x.c ^ 2 + x.c * x.d - 2 * x.b * x.d - x.d ^ 2)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigmaNorm_fst (x : GoldenEisensteinInt) : x.sigmaNorm.1 = { a := x.a, b := x.b }.norm - { a := x.c, b := x.d }.norm

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigmaProduct_eq_sigmaNorm (x : GoldenEisensteinInt) : x.sigmaProduct = { a := x.sigmaNorm.1, b := 0, c := x.sigmaNorm.2, d := 0 }

Embedding from ℤ[φ]

def FUST.FrourioAlgebra.GoldenEisensteinInt.ofGoldenInt (x : GoldenInt) : GoldenEisensteinInt

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.ofGoldenInt x = { a := x.a, b := x.b, c := 0, d := 0 }

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.ofGoldenInt_add (x y : GoldenInt) : ofGoldenInt (x.add y) = (ofGoldenInt x).add (ofGoldenInt y)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.ofGoldenInt_mul (x y : GoldenInt) : ofGoldenInt (x.mul y) = (ofGoldenInt x).mul (ofGoldenInt y)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.ofGoldenInt_one : ofGoldenInt GoldenInt.one = one

Key constants in ℤ[φ,ζ₆]

def FUST.FrourioAlgebra.GoldenEisensteinInt.phi_gei : GoldenEisensteinInt

φ as element of ℤ[φ,ζ₆]

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.phi_gei = { a := 0, b := 1, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.zeta6_gei : GoldenEisensteinInt

ζ₆ as element of ℤ[φ,ζ₆]

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.zeta6_gei = { a := 0, b := 0, c := 1, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei : GoldenEisensteinInt

AF_coeff = 4ζ₆ - 2 ∈ ℤ[ζ₆] ⊂ ℤ[φ,ζ₆]

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei = { a := -2, b := 0, c := 4, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.five_mu_gei : GoldenEisensteinInt

5μ = 6 - 2φ ∈ ℤ[φ] ⊂ ℤ[φ,ζ₆]

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.five_mu_gei = { a := 6, b := -2, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.five_three_plus_mu : GoldenEisensteinInt

5(3+μ) = 21 - 2φ

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.five_three_plus_mu = { a := 21, b := -2, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.five_three_minus_mu : GoldenEisensteinInt

5(3-μ) = 9 + 2φ

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.five_three_minus_mu = { a := 9, b := 2, c := 0, d := 0 }

Units: φ, ζ₆, -1 generate ℤ[φ,ζ₆]×

def FUST.FrourioAlgebra.GoldenEisensteinInt.zeta6_bar : GoldenEisensteinInt

ζ₆' = 1 - ζ₆ is the inverse of ζ₆ (since ζ₆·ζ₆'=1)

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.zeta6_bar = { a := 1, b := 0, c := -1, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.psi_gei : GoldenEisensteinInt

ψ = 1 - φ as GEI element

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.psi_gei = { a := 1, b := -1, c := 0, d := 0 }

def FUST.FrourioAlgebra.GoldenEisensteinInt.neg_psi_gei : GoldenEisensteinInt

-ψ is the inverse of φ (since φ·(-ψ) = -φψ = 1)

Equations

• FUST.FrourioAlgebra.GoldenEisensteinInt.neg_psi_gei = { a := -1, b := 1, c := 0, d := 0 }

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.zeta6_mul_bar : zeta6_gei.mul zeta6_bar = one

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.phi_mul_neg_psi : phi_gei.mul neg_psi_gei = one

Galois-fixed elements: σ(x)=x ∧ τ(x)=x ↔ x ∈ ℤ (b=c=d=0)

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.sigma_fixed_iff (x : GoldenEisensteinInt) : x.sigma = x ↔ x.b = 0 ∧ x.d = 0

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.tau_fixed_iff (x : GoldenEisensteinInt) : x.tau = x ↔ x.c = 0 ∧ x.d = 0

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.galois_fixed_iff (x : GoldenEisensteinInt) : x.sigma = x ∧ x.tau = x ↔ x.b = 0 ∧ x.c = 0 ∧ x.d = 0

Galois-fixed elements are exactly ℤ ⊂ ℤ[φ,ζ₆]

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.galois_fixed_unit_iff (x : GoldenEisensteinInt) : x.sigma = x ∧ x.tau = x ∧ (x.mul x = one ∨ x.mul x.neg = one) → x = one ∨ x = one.neg

The only Galois-fixed units are ±1

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.AF_coeff_gei_eq : AF_coeff_gei.toComplex = DζOperator.AF_coeff

theorem FUST.FrourioAlgebra.GoldenEisensteinInt.five_mu_correct : five_mu_gei.toComplex * (↑φ + 2) = 10