Documentation

FUST.FrourioAlgebra.GoldenIntegerRing

Golden Integer Ring ℤ[φ] #

This file establishes the commutative ring structure on the golden integer ring ℤ[φ] = {a + bφ | a, b ∈ ℤ}, where φ = (1 + √5)/2 is the golden ratio.

Main Results #

GoldenInt.commRing : ℤ[φ] is a commutative ring
GoldenInt.toReal : Embedding ℤ[φ] → ℝ
GoldenInt.toReal_injective : The embedding is injective
GoldenInt.phiPow_eq_toReal : φ^n in ℤ[φ] corresponds to φ^n in ℝ

Mathematical Background #

The golden integer ring ℤ[φ] is the ring of integers in the quadratic field ℚ(√5). Key properties:

φ² = φ + 1 (golden ratio equation)
Units: ℤ[φ]× = {±φⁿ | n ∈ ℤ}
Norm: N(a + bφ) = a² + ab - b² = (-1)^n for units ±φⁿ

Ring Axioms for GoldenInt #

theorem FUST.FrourioAlgebra.add_comm' (x y : GoldenInt) :

x.add y = y.add x

Addition is commutative

theorem FUST.FrourioAlgebra.add_assoc' (x y z : GoldenInt) :

(x.add y).add z = x.add (y.add z)

Addition is associative

theorem FUST.FrourioAlgebra.zero_add' (x : GoldenInt) :

GoldenInt.zero.add x = x

Zero is left identity for addition

theorem FUST.FrourioAlgebra.add_zero' (x : GoldenInt) :

x.add GoldenInt.zero = x

Zero is right identity for addition

theorem FUST.FrourioAlgebra.add_left_neg' (x : GoldenInt) :

x.neg.add x = GoldenInt.zero

Left inverse for addition

theorem FUST.FrourioAlgebra.neg_add_cancel' (x : GoldenInt) :

x.neg + x = 0

Right inverse for addition (neg_add_cancel)

theorem FUST.FrourioAlgebra.mul_comm' (x y : GoldenInt) :

x.mul y = y.mul x

Multiplication is commutative

theorem FUST.FrourioAlgebra.mul_assoc' (x y z : GoldenInt) :

(x.mul y).mul z = x.mul (y.mul z)

Multiplication is associative

theorem FUST.FrourioAlgebra.one_mul' (x : GoldenInt) :

GoldenInt.one.mul x = x

One is left identity for multiplication

theorem FUST.FrourioAlgebra.mul_one' (x : GoldenInt) :

x.mul GoldenInt.one = x

One is right identity for multiplication

theorem FUST.FrourioAlgebra.left_distrib' (x y z : GoldenInt) :

x.mul (y.add z) = (x.mul y).add (x.mul z)

Left distributivity

theorem FUST.FrourioAlgebra.right_distrib' (x y z : GoldenInt) :

(x.add y).mul z = (x.mul z).add (y.mul z)

Right distributivity

theorem FUST.FrourioAlgebra.sub_eq_add_neg' (x y : GoldenInt) :

x.sub y = x.add y.neg

Subtraction definition

theorem FUST.FrourioAlgebra.zero_mul' (x : GoldenInt) :

GoldenInt.zero.mul x = GoldenInt.zero

Zero times anything is zero

theorem FUST.FrourioAlgebra.mul_zero' (x : GoldenInt) :

x.mul GoldenInt.zero = GoldenInt.zero

Anything times zero is zero

theorem FUST.FrourioAlgebra.neg_add' (x y : GoldenInt) :

(x.add y).neg = x.neg.add y.neg

Negation distributes over addition

theorem FUST.FrourioAlgebra.neg_neg' (x : GoldenInt) :

Double negation

theorem FUST.FrourioAlgebra.neg_zero' :

GoldenInt.zero.neg = GoldenInt.zero

Negation of zero is zero

theorem FUST.FrourioAlgebra.neg_one_mul' (x : GoldenInt) :

GoldenInt.one.neg.mul x = x.neg

Multiplication by -1

def FUST.FrourioAlgebra.nsmul :

ℕ → GoldenInt → GoldenInt

Natural number scalar multiplication

Equations

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

Instances For

def FUST.FrourioAlgebra.zsmul :

ℤ → GoldenInt → GoldenInt

Integer scalar multiplication

Equations

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

Instances For

theorem FUST.FrourioAlgebra.nsmul_zero' (x : GoldenInt) :

nsmul 0 x = GoldenInt.zero

nsmul 0 is zero

theorem FUST.FrourioAlgebra.nsmul_succ' (n : ℕ) (x : GoldenInt) :

nsmul (n + 1) x = (nsmul n x).add x

nsmul (n+1) is add

theorem FUST.FrourioAlgebra.zsmul_zero' (x : GoldenInt) :

zsmul 0 x = GoldenInt.zero

zsmul 0 is zero

theorem FUST.FrourioAlgebra.zsmul_ofNat' (n : ℕ) (x : GoldenInt) :

zsmul (Int.ofNat n) x = nsmul n x

zsmul for positive integers

theorem FUST.FrourioAlgebra.zsmul_negSucc' (n : ℕ) (x : GoldenInt) :

zsmul (Int.negSucc n) x = (nsmul (n + 1) x).neg

zsmul for negative integers

def FUST.FrourioAlgebra.npow :

ℕ → GoldenInt → GoldenInt

Natural number power

Equations

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

Instances For

theorem FUST.FrourioAlgebra.npow_zero' (x : GoldenInt) :

npow 0 x = GoldenInt.one

npow 0 is one

theorem FUST.FrourioAlgebra.npow_succ' (n : ℕ) (x : GoldenInt) :

npow (n + 1) x = (npow n x).mul x

npow (n+1) is mul

def FUST.FrourioAlgebra.intCast :

ℤ → GoldenInt

Integer cast into GoldenInt

Equations

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

Instances For

def FUST.FrourioAlgebra.natCast :

ℕ → GoldenInt

Natural number cast into GoldenInt

Equations

FUST.FrourioAlgebra.natCast n = { a := ↑n, b := 0 }

Instances For

instance FUST.FrourioAlgebra.instNatCastGoldenInt :

NatCast GoldenInt

Equations

FUST.FrourioAlgebra.instNatCastGoldenInt = { natCast := FUST.FrourioAlgebra.natCast }

instance FUST.FrourioAlgebra.instIntCastGoldenInt :

IntCast GoldenInt

Equations

FUST.FrourioAlgebra.instIntCastGoldenInt = { intCast := FUST.FrourioAlgebra.intCast }

theorem FUST.FrourioAlgebra.natCast_zero' :

natCast 0 = GoldenInt.zero

natCast 0 is zero

theorem FUST.FrourioAlgebra.natCast_succ' (n : ℕ) :

natCast (n + 1) = (natCast n).add GoldenInt.one

natCast (n+1) is add one

theorem FUST.FrourioAlgebra.intCast_zero' :

intCast 0 = GoldenInt.zero

intCast 0 is zero

theorem FUST.FrourioAlgebra.intCast_one' :

intCast 1 = GoldenInt.one

intCast 1 is one

CommRing Instance #

instance FUST.FrourioAlgebra.instCommRingGoldenInt :

CommRing GoldenInt

Equations

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

Embedding into ℝ #

noncomputable def FUST.FrourioAlgebra.GoldenInt.toReal (x : GoldenInt) :

Embed GoldenInt into ℝ via a + bφ

Equations

x.toReal = ↑x.a + ↑x.b * FUST.φ

Instances For

theorem FUST.FrourioAlgebra.toReal_zero :

GoldenInt.zero.toReal = 0

toReal of zero is 0

theorem FUST.FrourioAlgebra.toReal_one :

GoldenInt.one.toReal = 1

toReal of one is 1

theorem FUST.FrourioAlgebra.toReal_phi :

GoldenInt.phi.toReal = φ

toReal of phi is φ

theorem FUST.FrourioAlgebra.toReal_add (x y : GoldenInt) :

(x.add y).toReal = x.toReal + y.toReal

toReal preserves addition

theorem FUST.FrourioAlgebra.toReal_neg (x : GoldenInt) :

x.neg.toReal = -x.toReal

toReal preserves negation

theorem FUST.FrourioAlgebra.toReal_mul (x y : GoldenInt) :

(x.mul y).toReal = x.toReal * y.toReal

toReal preserves multiplication

theorem FUST.FrourioAlgebra.toReal_ringHom (x y : GoldenInt) :

(x + y).toReal = x.toReal + y.toReal ∧ (x * y).toReal = x.toReal * y.toReal

toReal is a ring homomorphism

theorem FUST.FrourioAlgebra.phi_irrational :

φ is irrational

theorem FUST.FrourioAlgebra.toReal_injective :

Function.Injective GoldenInt.toReal

toReal is injective

Connection to φ powers #

theorem FUST.FrourioAlgebra.phiPowNat_toReal (n : ℕ) :

(GoldenInt.phiPowNat n).toReal = φ ^ n

phiPowNat n corresponds to φ^n in ℝ

theorem FUST.FrourioAlgebra.phiPowNeg_toReal (n : ℕ) :

(GoldenInt.phiPowNeg n).toReal = φ ^ (-↑n)

phiPowNeg n corresponds to φ^{-n} in ℝ

theorem FUST.FrourioAlgebra.phiPow_toReal (n : ℤ) :

(GoldenInt.phiPow n).toReal = φ ^ n

phiPow n corresponds to φ^n in ℝ

Mass Parameters in ℤ[φ] #

In FUFT, mass parameters have the form φⁿ × [1 + c₁φ^Δ₁ + c₂φ^Δ₂ + c₃φ^Δ₃] where n, Δᵢ ∈ ℤ and cᵢ ∈ ℤ.

For integer exponents, φⁿ ∈ ℤ[φ] (proven above). The correction factors 1 + c₁φ^Δ₁ + ... are sums of elements in ℤ[φ]. Therefore, all FUFT mass parameters naturally live in ℤ[φ].

def FUST.FrourioAlgebra.fuftCorrectionFactor (c₁ c₂ c₃ Δ₁ Δ₂ Δ₃ : ℤ) :

A FUFT-style correction factor: 1 + c₁φ^Δ₁ + c₂φ^Δ₂ + c₃φ^Δ₃

Equations

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

Instances For

def FUST.FrourioAlgebra.fuftMassParameter (n c₁ c₂ c₃ Δ₁ Δ₂ Δ₃ : ℤ) :

A FUFT mass parameter: φⁿ × correction_factor

Equations

FUST.FrourioAlgebra.fuftMassParameter n c₁ c₂ c₃ Δ₁ Δ₂ Δ₃ = FUST.FrourioAlgebra.GoldenInt.phiPow n * FUST.FrourioAlgebra.fuftCorrectionFactor c₁ c₂ c₃ Δ₁ Δ₂ Δ₃

Instances For

theorem FUST.FrourioAlgebra.intCast_toReal (c : ℤ) :

(intCast c).toReal = ↑c

intCast to real conversion

theorem FUST.FrourioAlgebra.fuftMassParameter_toReal (n c₁ c₂ c₃ Δ₁ Δ₂ Δ₃ : ℤ) :

(fuftMassParameter n c₁ c₂ c₃ Δ₁ Δ₂ Δ₃).toReal = φ ^ n * (1 + ↑c₁ * φ ^ Δ₁ + ↑c₂ * φ ^ Δ₂ + ↑c₃ * φ ^ Δ₃)

The real value of a FUFT mass parameter

theorem FUST.FrourioAlgebra.fuftMassParameter_in_goldenInt (n c₁ c₂ c₃ Δ₁ Δ₂ Δ₃ : ℤ) :

∃ (x : GoldenInt), x.toReal = φ ^ n * (1 + ↑c₁ * φ ^ Δ₁ + ↑c₂ * φ ^ Δ₂ + ↑c₃ * φ ^ Δ₃)

All FUFT mass parameters are in ℤ[φ] (by construction)

Galois Conjugation σ: φ ↦ ψ #

The unique non-trivial automorphism of ℤ[φ].

theorem FUST.FrourioAlgebra.conj_add (x y : GoldenInt) :

(x.add y).conj = x.conj.add y.conj

theorem FUST.FrourioAlgebra.conj_mul (x y : GoldenInt) :

(x.mul y).conj = x.conj.mul y.conj

theorem FUST.FrourioAlgebra.conj_one :

GoldenInt.one.conj = GoldenInt.one

theorem FUST.FrourioAlgebra.conj_zero :

GoldenInt.zero.conj = GoldenInt.zero

theorem FUST.FrourioAlgebra.conj_neg (x : GoldenInt) :

x.neg.conj = x.conj.neg

theorem FUST.FrourioAlgebra.conj_involution (x : GoldenInt) :

x.conj.conj = x

theorem FUST.FrourioAlgebra.conj_fixes_int (n : ℤ) :

(intCast n).conj = intCast n

theorem FUST.FrourioAlgebra.conj_phi :

GoldenInt.phi.conj = { a := 1, b := -1 }

theorem FUST.FrourioAlgebra.conj_phi_toReal :

GoldenInt.phi.conj.toReal = ψ

theorem FUST.FrourioAlgebra.conj_norm (x : GoldenInt) :

x.conj.norm = x.norm

theorem FUST.FrourioAlgebra.conj_mul_self_in_Z (x : GoldenInt) :

(x.mul x.conj).b = 0

theorem FUST.FrourioAlgebra.conj_mul_self_eq_norm (x : GoldenInt) :

x.mul x.conj = { a := x.norm, b := 0 }