Geometric four-colorings of the Moser lattice

This file formalizes the lattice part of Theorem 3.1 of Ákos Dúcz, A note on geometric colorings of the Moser lattice, arXiv:2606.12325. It derives the exact squared-norm formula, defines both parity colorings from the paper, and proves that each is proper and geometric on the whole lattice.

The uniqueness assertion in Theorem 3.2 is not formalized here.

@[reducible, inline]

abbrev LeanPool.MoserLatticeColorings.R2 : Type

The Euclidean plane with its standard metric.

Equations

• LeanPool.MoserLatticeColorings.R2 = EuclideanSpace ℝ (Fin 2)

structure LeanPool.MoserLatticeColorings.Coeff : Type

Integer coordinates in the basis 1, omega_1, omega_3, omega_1 * omega_3.

• a : ℤ

  Coefficient of 1.

• b : ℤ

  Coefficient of omega_1.

• c : ℤ

  Coefficient of omega_3.

• d : ℤ

  Coefficient of omega_1 * omega_3.

def LeanPool.MoserLatticeColorings.instDecidableEqCoeff.decEq (x✝ x✝¹ : Coeff) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance LeanPool.MoserLatticeColorings.instDecidableEqCoeff : DecidableEq Coeff

Equations

• LeanPool.MoserLatticeColorings.instDecidableEqCoeff = LeanPool.MoserLatticeColorings.instDecidableEqCoeff.decEq

def LeanPool.MoserLatticeColorings.Coeff.sub (p q : Coeff) : Coeff

Coordinatewise subtraction.

Equations

• p.sub q = { a := p.a - q.a, b := p.b - q.b, c := p.c - q.c, d := p.d - q.d }

def LeanPool.MoserLatticeColorings.Coeff.normRational (p : Coeff) : ℤ

Rational coefficient in six times the squared norm.

Equations

• p.normRational = 6 * (p.a ^ 2 + p.a * p.b + p.b ^ 2 + p.c ^ 2 + p.c * p.d + p.d ^ 2) + 10 * p.a * p.c + 5 * p.a * p.d + 5 * p.b * p.c + 10 * p.b * p.d

def LeanPool.MoserLatticeColorings.Coeff.normRadical (p : Coeff) : ℤ

sqrt 33 coefficient in six times the squared norm.

Equations

• p.normRadical = p.b * p.c - p.a * p.d

noncomputable def LeanPool.MoserLatticeColorings.Coeff.toR2 (p : Coeff) : R2

The Euclidean coordinates of a + b * ω₁ + c * ω₃ + d * ω₁ * ω₃, where ω₁ = 1 / 2 + i * √3 / 2 and ω₃ = 5 / 6 + i * √11 / 6.

Equations

• p.toR2 = !₂[↑(12 * p.a + 6 * p.b + 10 * p.c + 5 * p.d) / 12 - ↑p.d * √33 / 12, (3 * ↑(6 * p.b + 5 * p.d) + ↑(2 * p.c + p.d) * √33) / (12 * √3)]

@[simp]

theorem LeanPool.MoserLatticeColorings.Coeff.toR2_zero (p : Coeff) : p.toR2.ofLp 0 = ↑(12 * p.a + 6 * p.b + 10 * p.c + 5 * p.d) / 12 - ↑p.d * √33 / 12

@[simp]

theorem LeanPool.MoserLatticeColorings.Coeff.toR2_one (p : Coeff) : p.toR2.ofLp 1 = (3 * ↑(6 * p.b + 5 * p.d) + ↑(2 * p.c + p.d) * √33) / (12 * √3)

theorem LeanPool.MoserLatticeColorings.Coeff.dist_sq (p q : Coeff) : dist p.toR2 q.toR2 ^ 2 = ↑(p.sub q).normRational / 6 + ↑(p.sub q).normRadical * √33 / 6

def LeanPool.MoserLatticeColorings.Coeff.color (p : Coeff) : ZMod 2 × ZMod 2

Ducz's first parity coloring.

Equations

• p.color = (↑p.a + ↑p.b + ↑p.d, ↑p.a + ↑p.c + ↑p.d)

theorem LeanPool.MoserLatticeColorings.Coeff.color_sub_eq_zero_of_eq {p q : Coeff} (h : p.color = q.color) : (p.sub q).color = 0

theorem LeanPool.MoserLatticeColorings.Coeff.color_sub_eq_zero_iff (p q : Coeff) : (p.sub q).color = 0 ↔ p.color = q.color

theorem LeanPool.MoserLatticeColorings.Coeff.norm_sum_dvd_eight_of_color_zero {p : Coeff} (h : p.color = 0) : 8 ∣ p.normRational + p.normRadical

theorem LeanPool.MoserLatticeColorings.Coeff.color_eq_zero_iff_norm_sum_dvd_four (p : Coeff) : p.color = 0 ↔ 4 ∣ p.normRational + p.normRadical

theorem LeanPool.MoserLatticeColorings.Coeff.unit_norm_coefficients {p : Coeff} (h : (↑p.normRational + ↑p.normRadical * √33) / 6 = 1) : p.normRational = 6 ∧ p.normRadical = 0

theorem LeanPool.MoserLatticeColorings.Coeff.radical_coordinates_unique {a b c d : ℤ} (h : ↑a + ↑b * √33 = ↑c + ↑d * √33) : a = c ∧ b = d

theorem LeanPool.MoserLatticeColorings.Coeff.toR2_injective : Function.Injective toR2

The four integer coordinates give a faithful presentation of the Moser lattice.

theorem LeanPool.MoserLatticeColorings.Coeff.norm_coordinates_eq_of_sqNorm_eq {p q : Coeff} (h : (↑p.normRational + ↑p.normRadical * √33) / 6 = (↑q.normRational + ↑q.normRadical * √33) / 6) : p.normRational = q.normRational ∧ p.normRadical = q.normRadical

def LeanPool.MoserLatticeColorings.Coeff.IsGeometricColoring {κ : Type u_1} (f : Coeff → κ) : Prop

A coloring is geometric when equality of colors for a pair depends only on the Euclidean distance between the pair.

Equations

• LeanPool.MoserLatticeColorings.Coeff.IsGeometricColoring f = ∀ (p q r s : LeanPool.MoserLatticeColorings.Coeff), dist p.toR2 q.toR2 = dist r.toR2 s.toR2 → (f p = f q ↔ f r = f s)

theorem LeanPool.MoserLatticeColorings.Coeff.color_isGeometric : IsGeometricColoring color

def LeanPool.MoserLatticeColorings.Coeff.colorTwo (p : Coeff) : ZMod 2 × ZMod 2

Ducz's second parity coloring.

Equations

• p.colorTwo = (↑p.a + ↑p.d, ↑p.b + ↑p.c + ↑p.d)

theorem LeanPool.MoserLatticeColorings.Coeff.colorTwo_sub_eq_zero_iff (p q : Coeff) : (p.sub q).colorTwo = 0 ↔ p.colorTwo = q.colorTwo

theorem LeanPool.MoserLatticeColorings.Coeff.colorTwo_eq_zero_iff_norm_diff_dvd_four (p : Coeff) : p.colorTwo = 0 ↔ 4 ∣ p.normRational - p.normRadical

theorem LeanPool.MoserLatticeColorings.Coeff.colorTwo_ne_of_dist_eq_one {p q : Coeff} (h : dist p.toR2 q.toR2 = 1) : p.colorTwo ≠ q.colorTwo

theorem LeanPool.MoserLatticeColorings.Coeff.colorTwo_isGeometric : IsGeometricColoring colorTwo

theorem LeanPool.MoserLatticeColorings.Coeff.color_ne_of_dist_eq_one {p q : Coeff} (h : dist p.toR2 q.toR2 = 1) : p.color ≠ q.color

def LeanPool.MoserLatticeColorings.Coeff.unitDistanceGraph : SimpleGraph Coeff

Unit-distance graph induced by the entire Moser lattice.

Equations

• LeanPool.MoserLatticeColorings.Coeff.unitDistanceGraph = SimpleGraph.fromRel fun (p q : LeanPool.MoserLatticeColorings.Coeff) => dist p.toR2 q.toR2 = 1

noncomputable def LeanPool.MoserLatticeColorings.Coeff.coloring : unitDistanceGraph.Coloring (ZMod 2 × ZMod 2)

Dúcz's first parity map as a proper four-coloring.

Equations

• LeanPool.MoserLatticeColorings.Coeff.coloring = SimpleGraph.Coloring.mk LeanPool.MoserLatticeColorings.Coeff.color @LeanPool.MoserLatticeColorings.Coeff.coloring._proof_1

theorem LeanPool.MoserLatticeColorings.Coeff.colorable_four : unitDistanceGraph.Colorable 4

noncomputable def LeanPool.MoserLatticeColorings.Coeff.coloringTwo : unitDistanceGraph.Coloring (ZMod 2 × ZMod 2)

Dúcz's second parity map as a proper four-coloring.

Equations

• LeanPool.MoserLatticeColorings.Coeff.coloringTwo = SimpleGraph.Coloring.mk LeanPool.MoserLatticeColorings.Coeff.colorTwo @LeanPool.MoserLatticeColorings.Coeff.coloringTwo._proof_1

def LeanPool.MoserLatticeColorings.Coeff.scale (n : ℤ) (p : Coeff) : Coeff

Integer scaling of a coefficient vector.

Equations

• LeanPool.MoserLatticeColorings.Coeff.scale n p = { a := n * p.a, b := n * p.b, c := n * p.c, d := n * p.d }

def LeanPool.MoserLatticeColorings.Coeff.zero : Coeff

The zero coefficient vector.

Equations

• LeanPool.MoserLatticeColorings.Coeff.zero = { a := 0, b := 0, c := 0, d := 0 }

theorem LeanPool.MoserLatticeColorings.Coeff.sub_zero (p : Coeff) : p.sub zero = p

theorem LeanPool.MoserLatticeColorings.Coeff.toR2_zero_coeff : zero.toR2 = 0

theorem LeanPool.MoserLatticeColorings.Coeff.toR2_scale (n : ℤ) (p : Coeff) : (scale n p).toR2 = ↑n • p.toR2

theorem LeanPool.MoserLatticeColorings.Coeff.toR2_sub (p q : Coeff) : (p.sub q).toR2 = p.toR2 - q.toR2

theorem LeanPool.MoserLatticeColorings.Coeff.color_scale_three_pow (k : ℕ) (p : Coeff) : (scale (3 ^ k) p).color = p.color

theorem LeanPool.MoserLatticeColorings.Coeff.colorTwo_scale_three_pow (k : ℕ) (p : Coeff) : (scale (3 ^ k) p).colorTwo = p.colorTwo