Golden Valuation and Non-Decreasing Property

This file formalizes the valuation non-decreasing property for the two-point scale difference operator Δ_{α,β,ε} over the golden integer ring.

Golden Integer Ring

The ring O = Z[φ] of integers in Q(φ), where φ = (1 + √5)/2.

structure FUST.FrourioAlgebra.GoldenInt : Type

The golden integer ring O = Z[φ]. Elements are of the form a + bφ where a, b ∈ Z.

• a : ℤ
• b : ℤ

instance FUST.FrourioAlgebra.instDecidableEqGoldenInt : DecidableEq GoldenInt

Equations

• FUST.FrourioAlgebra.instDecidableEqGoldenInt = FUST.FrourioAlgebra.instDecidableEqGoldenInt.decEq

def FUST.FrourioAlgebra.instDecidableEqGoldenInt.decEq (x✝ x✝¹ : GoldenInt) : Decidable (x✝ = x✝¹)

Equations

• FUST.FrourioAlgebra.instDecidableEqGoldenInt.decEq { a := a, b := a_1 } { a := b, b := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance FUST.FrourioAlgebra.instReprGoldenInt : Repr GoldenInt

Equations

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

def FUST.FrourioAlgebra.instReprGoldenInt.repr : GoldenInt → ℕ → Std.Format

Equations

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

def FUST.FrourioAlgebra.GoldenInt.zero : GoldenInt

Zero element

Equations

• FUST.FrourioAlgebra.GoldenInt.zero = { a := 0, b := 0 }

def FUST.FrourioAlgebra.GoldenInt.one : GoldenInt

One element

Equations

• FUST.FrourioAlgebra.GoldenInt.one = { a := 1, b := 0 }

def FUST.FrourioAlgebra.GoldenInt.phi : GoldenInt

The golden ratio φ as an element of O

Equations

• FUST.FrourioAlgebra.GoldenInt.phi = { a := 0, b := 1 }

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

Addition in O

Equations

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

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

Negation in O

Equations

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

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

Subtraction in O

Equations

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

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

Multiplication in O using φ² = φ + 1

Equations

• x.mul y = { a := x.a * y.a + x.b * y.b, b := x.a * y.b + x.b * y.a + x.b * y.b }

instance FUST.FrourioAlgebra.GoldenInt.instZero : Zero GoldenInt

Equations

• FUST.FrourioAlgebra.GoldenInt.instZero = { zero := FUST.FrourioAlgebra.GoldenInt.zero }

instance FUST.FrourioAlgebra.GoldenInt.instOne : One GoldenInt

Equations

• FUST.FrourioAlgebra.GoldenInt.instOne = { one := FUST.FrourioAlgebra.GoldenInt.one }

instance FUST.FrourioAlgebra.GoldenInt.instAdd : Add GoldenInt

Equations

• FUST.FrourioAlgebra.GoldenInt.instAdd = { add := FUST.FrourioAlgebra.GoldenInt.add }

instance FUST.FrourioAlgebra.GoldenInt.instNeg : Neg GoldenInt

Equations

• FUST.FrourioAlgebra.GoldenInt.instNeg = { neg := FUST.FrourioAlgebra.GoldenInt.neg }

instance FUST.FrourioAlgebra.GoldenInt.instSub : Sub GoldenInt

Equations

• FUST.FrourioAlgebra.GoldenInt.instSub = { sub := FUST.FrourioAlgebra.GoldenInt.sub }

instance FUST.FrourioAlgebra.GoldenInt.instMul : Mul GoldenInt

Equations

• FUST.FrourioAlgebra.GoldenInt.instMul = { mul := FUST.FrourioAlgebra.GoldenInt.mul }

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

The norm N(a + bφ) = a² + ab - b²

Equations

• x.norm = x.a ^ 2 + x.a * x.b - x.b ^ 2

def FUST.FrourioAlgebra.GoldenInt.trace (x : GoldenInt) : ℤ

The trace Tr(a + bφ) = 2a + b

Equations

• x.trace = 2 * x.a + x.b

def FUST.FrourioAlgebra.GoldenInt.conj (x : GoldenInt) : GoldenInt

Galois conjugate: a + bφ ↦ a + bψ = (a + b) - bφ where ψ = (1 - √5)/2 = 1 - φ

Equations

• x.conj = { a := x.a + x.b, b := -x.b }

def FUST.FrourioAlgebra.GoldenInt.isUnit (x : GoldenInt) : Bool

An element is a unit iff its norm is ±1

Equations

• x.isUnit = (x.norm == 1 || x.norm == -1)

theorem FUST.FrourioAlgebra.GoldenInt.isUnit_iff (x : GoldenInt) : x.isUnit = true ↔ x.norm = 1 ∨ x.norm = -1

theorem FUST.FrourioAlgebra.GoldenInt.norm_mul (x y : GoldenInt) : (x.mul y).norm = x.norm * y.norm

Norm is multiplicative: N(xy) = N(x)N(y)

theorem FUST.FrourioAlgebra.GoldenInt.no_sqrt5_rational (n : ℕ) : n > 0 → ∀ (m : ℤ), m ^ 2 ≠ 5 * ↑n ^ 2

√5 is irrational: no integer solutions to m² = 5n² with n ≠ 0

theorem FUST.FrourioAlgebra.GoldenInt.norm_eq_zero_iff (x : GoldenInt) : x.norm = 0 ↔ x = zero

norm x = 0 implies x = 0

theorem FUST.FrourioAlgebra.GoldenInt.mul_eq_zero_iff (x y : GoldenInt) : x.mul y = zero ↔ x = zero ∨ y = zero

GoldenInt has no zero divisors: xy = 0 implies x = 0 or y = 0

theorem FUST.FrourioAlgebra.GoldenInt.unit_mul_eq_zero (u x : GoldenInt) (hu : u.isUnit = true) (h : u.mul x = zero) : x = zero

If u is a unit and u * x = 0, then x = 0

theorem FUST.FrourioAlgebra.GoldenInt.phi_isUnit : phi.isUnit = true

φ is a unit (norm = -1)

theorem FUST.FrourioAlgebra.GoldenInt.neg_one_isUnit : one.neg.isUnit = true

-1 is a unit

def FUST.FrourioAlgebra.GoldenInt.phiInv : GoldenInt

φ⁻¹ = φ - 1 since φ² = φ + 1 implies φ · (φ - 1) = φ² - φ = 1

Equations

• FUST.FrourioAlgebra.GoldenInt.phiInv = { a := -1, b := 1 }

theorem FUST.FrourioAlgebra.GoldenInt.phiInv_isUnit : phiInv.isUnit = true

φ⁻¹ is a unit (norm = -1)

theorem FUST.FrourioAlgebra.GoldenInt.one_isUnit : one.isUnit = true

1 is a unit

theorem FUST.FrourioAlgebra.GoldenInt.isUnit_mul (x y : GoldenInt) (hx : x.isUnit = true) (hy : y.isUnit = true) : (x.mul y).isUnit = true

Product of two units is a unit

def FUST.FrourioAlgebra.GoldenInt.phiPowNat : ℕ → GoldenInt

Powers of φ for natural numbers

Equations

• FUST.FrourioAlgebra.GoldenInt.phiPowNat 0 = FUST.FrourioAlgebra.GoldenInt.one
• FUST.FrourioAlgebra.GoldenInt.phiPowNat n.succ = FUST.FrourioAlgebra.GoldenInt.phi.mul (FUST.FrourioAlgebra.GoldenInt.phiPowNat n)

theorem FUST.FrourioAlgebra.GoldenInt.phiPowNat_isUnit (n : ℕ) : (phiPowNat n).isUnit = true

phiPowNat n is a unit for all n

def FUST.FrourioAlgebra.GoldenInt.phiPowNeg : ℕ → GoldenInt

Negative powers of φ

Equations

• FUST.FrourioAlgebra.GoldenInt.phiPowNeg 0 = FUST.FrourioAlgebra.GoldenInt.one
• FUST.FrourioAlgebra.GoldenInt.phiPowNeg n.succ = FUST.FrourioAlgebra.GoldenInt.phiInv.mul (FUST.FrourioAlgebra.GoldenInt.phiPowNeg n)

theorem FUST.FrourioAlgebra.GoldenInt.phiPowNeg_isUnit (n : ℕ) : (phiPowNeg n).isUnit = true

phiPowNeg n is a unit for all n

def FUST.FrourioAlgebra.GoldenInt.phiPow : ℤ → GoldenInt

Powers of φ for all integers

Equations

• FUST.FrourioAlgebra.GoldenInt.phiPow (Int.ofNat n) = FUST.FrourioAlgebra.GoldenInt.phiPowNat n
• FUST.FrourioAlgebra.GoldenInt.phiPow (Int.negSucc n) = FUST.FrourioAlgebra.GoldenInt.phiPowNeg (n + 1)

theorem FUST.FrourioAlgebra.GoldenInt.phiPow_isUnit (n : ℤ) : (phiPow n).isUnit = true

All powers of φ are units

theorem FUST.FrourioAlgebra.GoldenInt.neg_isUnit (x : GoldenInt) (hx : x.isUnit = true) : x.neg.isUnit = true

Negation of a unit is a unit

def FUST.FrourioAlgebra.GoldenInt.Units : Set GoldenInt

The unit group O× = {±φⁿ | n ∈ Z}

Equations

• FUST.FrourioAlgebra.GoldenInt.Units = {x : FUST.FrourioAlgebra.GoldenInt | ∃ (n : ℤ), x = FUST.FrourioAlgebra.GoldenInt.phiPow n ∨ x = (FUST.FrourioAlgebra.GoldenInt.phiPow n).neg}

theorem FUST.FrourioAlgebra.GoldenInt.units_isUnit (x : GoldenInt) (hx : x ∈ Units) : x.isUnit = true

Elements in Units are units (forward direction)

theorem FUST.FrourioAlgebra.GoldenInt.ext_iff (x y : GoldenInt) : x = y ↔ x.a = y.a ∧ x.b = y.b

Equality of GoldenInt

theorem FUST.FrourioAlgebra.GoldenInt.neg_neg (x : GoldenInt) : x.neg.neg = x

neg (neg x) = x

def FUST.FrourioAlgebra.GoldenInt.size (x : GoldenInt) : ℕ

The "size" of a golden integer for descent argument

Equations

• x.size = x.a.natAbs + x.b.natAbs

theorem FUST.FrourioAlgebra.GoldenInt.mul_phiInv_eq (x : GoldenInt) : phiInv.mul x = { a := -x.a + x.b, b := x.a }

mul phiInv gives the components

theorem FUST.FrourioAlgebra.GoldenInt.mul_phi_eq (x : GoldenInt) : phi.mul x = { a := x.b, b := x.a + x.b }

mul phi gives the components

theorem FUST.FrourioAlgebra.GoldenInt.mul_phi_Units (n : ℤ) : phi.mul (phiPow n) = phiPow (n + 1)

If y ∈ Units, then mul phi y ∈ Units with shifted index

theorem FUST.FrourioAlgebra.GoldenInt.mul_phiInv_Units (n : ℤ) : phiInv.mul (phiPow n) = phiPow (n - 1)

If y ∈ Units, then mul phiInv y ∈ Units with shifted index

theorem FUST.FrourioAlgebra.GoldenInt.mul_phi_neg (x : GoldenInt) : phi.mul x.neg = (phi.mul x).neg

Multiplication by phi commutes with negation

theorem FUST.FrourioAlgebra.GoldenInt.mul_phiInv_neg (x : GoldenInt) : phiInv.mul x.neg = (phiInv.mul x).neg

Multiplication by phiInv commutes with negation

theorem FUST.FrourioAlgebra.GoldenInt.mul_phi_neg_Units (n : ℤ) : phi.mul (phiPow n).neg = (phiPow (n + 1)).neg

mul phi (neg (phiPow n)) = neg (phiPow (n + 1))

theorem FUST.FrourioAlgebra.GoldenInt.mul_phiInv_neg_Units (n : ℤ) : phiInv.mul (phiPow n).neg = (phiPow (n - 1)).neg

mul phiInv (neg (phiPow n)) = neg (phiPow (n - 1))

theorem FUST.FrourioAlgebra.GoldenInt.size_mul_phiInv_lt (x : GoldenInt) (hx : x.isUnit = true) (ha : x.a ≠ 0) (hab : x.a * x.b > 0) : (phiInv.mul x).size < x.size

Key descent lemma: for a unit x with a ≠ 0, b ≠ 0, and a·b > 0, multiplying by phiInv reduces size

theorem FUST.FrourioAlgebra.GoldenInt.size_mul_phi_lt (x : GoldenInt) (hx : x.isUnit = true) (ha : x.a ≠ 0) (hab : x.a * x.b < 0) : (phi.mul x).size < x.size

Key descent lemma: for a unit x with a ≠ 0, b ≠ 0, and a·b < 0, multiplying by phi reduces size

theorem FUST.FrourioAlgebra.GoldenInt.isUnit_mem_Units (x : GoldenInt) (hx : x.isUnit = true) : x ∈ Units

Reverse direction helper: find n such that x = phiPow n or x = neg (phiPow n). This theorem is a consequence of Dirichlet's unit theorem for Q(√5). The proof uses that the fundamental unit is φ and all units are ±φⁿ.

theorem FUST.FrourioAlgebra.GoldenInt.units_iff_norm_pm_one (x : GoldenInt) : x ∈ Units ↔ x.isUnit = true

Characterization of units: full equivalence

Formal Power Series with Golden Integer Coefficients

Laurent series A = O((x)) over the golden integers.

structure FUST.FrourioAlgebra.GoldenLaurent : Type

A formal Laurent series with golden integer coefficients. Represented as a function from Z to GoldenInt with finite negative support.

• coeff : ℤ → GoldenInt
• finiteNegSupport : {n : ℤ | n < 0 ∧ self.coeff n ≠ 0}.Finite

noncomputable def FUST.FrourioAlgebra.GoldenLaurent.valuation (f : GoldenLaurent) : WithTop ℤ

The valuation of a Laurent series: the minimum index with nonzero coefficient

Equations

• f.valuation = sInf {n : WithTop ℤ | ∃ (m : ℤ), ↑m = n ∧ f.coeff m ≠ 0}

def FUST.FrourioAlgebra.GoldenLaurent.zero : GoldenLaurent

Zero Laurent series

Equations

• FUST.FrourioAlgebra.GoldenLaurent.zero = { coeff := fun (x : ℤ) => 0, finiteNegSupport := FUST.FrourioAlgebra.GoldenLaurent.zero._proof_1 }

def FUST.FrourioAlgebra.GoldenLaurent.X : GoldenLaurent

The x variable as a Laurent series

Equations

• FUST.FrourioAlgebra.GoldenLaurent.X = { coeff := fun (n : ℤ) => if n = 1 then 1 else 0, finiteNegSupport := FUST.FrourioAlgebra.GoldenLaurent.X._proof_1 }

def FUST.FrourioAlgebra.GoldenLaurent.monomial (n : ℤ) (c : GoldenInt) : GoldenLaurent

Monomial x^n

Equations

• FUST.FrourioAlgebra.GoldenLaurent.monomial n c = { coeff := fun (m : ℤ) => if m = n then c else 0, finiteNegSupport := ⋯ }

def FUST.FrourioAlgebra.GoldenLaurent.add (f g : GoldenLaurent) : GoldenLaurent

Addition of Laurent series

Equations

• f.add g = { coeff := fun (n : ℤ) => f.coeff n + g.coeff n, finiteNegSupport := ⋯ }

def FUST.FrourioAlgebra.GoldenLaurent.neg (f : GoldenLaurent) : GoldenLaurent

Negation of Laurent series

Equations

• f.neg = { coeff := fun (n : ℤ) => -f.coeff n, finiteNegSupport := ⋯ }

def FUST.FrourioAlgebra.GoldenLaurent.sub (f g : GoldenLaurent) : GoldenLaurent

Subtraction of Laurent series

Equations

• f.sub g = f.add g.neg

instance FUST.FrourioAlgebra.GoldenLaurent.instAdd : Add GoldenLaurent

Equations

• FUST.FrourioAlgebra.GoldenLaurent.instAdd = { add := FUST.FrourioAlgebra.GoldenLaurent.add }

instance FUST.FrourioAlgebra.GoldenLaurent.instNeg : Neg GoldenLaurent

Equations

• FUST.FrourioAlgebra.GoldenLaurent.instNeg = { neg := FUST.FrourioAlgebra.GoldenLaurent.neg }

instance FUST.FrourioAlgebra.GoldenLaurent.instSub : Sub GoldenLaurent

Equations

• FUST.FrourioAlgebra.GoldenLaurent.instSub = { sub := FUST.FrourioAlgebra.GoldenLaurent.sub }

def FUST.FrourioAlgebra.GoldenLaurent.invMulOp (f : GoldenLaurent) : GoldenLaurent

The M_{1/x} operator: shifts indices by -1 (multiplication by 1/x)

Equations

• f.invMulOp = { coeff := fun (n : ℤ) => f.coeff (n + 1), finiteNegSupport := ⋯ }

Valuation Non-Decreasing Property

The main theorem: v_𝔭(Δf) ≥ v_𝔭(f) for the two-point difference operator.

class FUST.FrourioAlgebra.GoldenValuation : Type

Abstract valuation on golden integers (for a prime ideal 𝔭)

• v : GoldenInt → WithTop ℤ
• v_zero : v 0 = ⊤
• v_one : v 1 = 0
• v_mul (x y : GoldenInt) : v (x * y) = v x + v y
• v_add (x y : GoldenInt) : v (x + y) ≥ min (v x) (v y)
• v_unit (x : GoldenInt) : x.isUnit = true → v x = 0
• v_nonneg (x : GoldenInt) : 0 ≤ v x

noncomputable def FUST.FrourioAlgebra.coeffValuation [GoldenValuation] (f : GoldenLaurent) : WithTop ℤ

Coefficient valuation of a Laurent series: the minimum valuation among all coefficients

Equations

• FUST.FrourioAlgebra.coeffValuation f = ⨅ (n : ℤ), FUST.FrourioAlgebra.GoldenValuation.v (f.coeff n)

def FUST.FrourioAlgebra.scaleCoeffByUnit (f : GoldenLaurent) (u : GoldenInt) : GoldenLaurent

The scale operator U multiplies each coefficient by a unit power of φ

Equations

• FUST.FrourioAlgebra.scaleCoeffByUnit f u = { coeff := fun (n : ℤ) => u * f.coeff n, finiteNegSupport := ⋯ }

def FUST.FrourioAlgebra.twoPointDiff (f : GoldenLaurent) (α β : GoldenInt) : GoldenLaurent

The two-point scale difference operator Δ_{α,β,ε} Δf = M_{1/x}(αf - βf) for simplified version

Equations

• FUST.FrourioAlgebra.twoPointDiff f α β = ((FUST.FrourioAlgebra.scaleCoeffByUnit f α).sub (FUST.FrourioAlgebra.scaleCoeffByUnit f β)).invMulOp

Key Lemmas for the Proof

theorem FUST.FrourioAlgebra.unit_valuation_zero [GoldenValuation] (u : GoldenInt) (hu : u.isUnit = true) : GoldenValuation.v u = 0

Units have valuation 0

theorem FUST.FrourioAlgebra.unit_diff_valuation_nonneg [GoldenValuation] (u₁ u₂ : GoldenInt) (hu₁ : u₁.isUnit = true) (hu₂ : u₂.isUnit = true) : 0 ≤ GoldenValuation.v (u₁ - u₂)

The difference of two units has non-negative valuation

theorem FUST.FrourioAlgebra.GoldenInt.mul_sub_distrib (a b c : GoldenInt) : (a.sub b).mul c = (a.mul c).sub (b.mul c)

theorem FUST.FrourioAlgebra.valuation_nonDecreasing [GoldenValuation] (f : GoldenLaurent) (α β : GoldenInt) (hα : α.isUnit = true) (hβ : β.isUnit = true) : coeffValuation (twoPointDiff f α β) ≥ coeffValuation f

Main Theorem: Valuation Non-Decreasing Property

For any Laurent series f and unit coefficients α, β ∈ O×, the two-point difference Δ_{α,β}f satisfies:

v_𝔭(Δf) ≥ v_𝔭(f)

where v_𝔭 denotes the coefficient valuation with respect to a golden prime ideal 𝔭.

This is Proposition 6.1 / 8.1 in the papers.

theorem FUST.FrourioAlgebra.valuation_nonDecreasing_conj [GoldenValuation] (f : GoldenLaurent) (α β : GoldenInt) (hα : α.isUnit = true) (hβ : β.isUnit = true) : coeffValuation (twoPointDiff f α β) ≥ coeffValuation f

Corollary: Conjugate Side

v_{𝔭̄}(Δf) ≥ v_{𝔭̄}(f)

where 𝔭̄ is the conjugate prime ideal.

This follows from applying the same argument with the conjugate valuation.

theorem FUST.FrourioAlgebra.scale_preserves_coeff_valuation [GoldenValuation] (f : GoldenLaurent) (u : GoldenInt) (hu : u.isUnit = true) : coeffValuation (scaleCoeffByUnit f u) = coeffValuation f

Scaling by a unit preserves coefficient valuation

theorem FUST.FrourioAlgebra.invMul_preserves_coeff_valuation [GoldenValuation] (f : GoldenLaurent) : coeffValuation f.invMulOp = coeffValuation f

M_{1/x} shifts indices but preserves coefficient valuations

Specialization to Φ-system and F-system

theorem FUST.FrourioAlgebra.valuation_nonDecreasing_Phi [GoldenValuation] (f : GoldenLaurent) : coeffValuation (twoPointDiff f GoldenInt.phiInv GoldenInt.phi) ≥ coeffValuation f

For the Φ-system with α = φ⁻¹, β = φ

theorem FUST.FrourioAlgebra.valuation_nonDecreasing_F [GoldenValuation] (f : GoldenLaurent) : coeffValuation (twoPointDiff f GoldenInt.one GoldenInt.one.neg) ≥ coeffValuation f

For the F-system with α = 1, β = -1