Extension to the Moser ring

Dúcz observes that both geometric four-colorings of the Moser lattice extend to its multiplicative closure, the Moser ring. This file constructs the ring as localization-by-three representatives modulo equal Euclidean embeddings, proves that both colorings descend, and proves their properness and geometricity on the quotient.

As a search consequence, every unit-distance graph realized entirely in the Moser ring is four-colorable. This rules out Moser-ring-only searches for a six-chromatic witness, but it does not determine the chromatic number of the plane.

structure LeanPool.MoserLatticeColorings.RingRep : Type

A representative x / 3^k of a point in the Moser ring, with x in the integer-coordinate presentation of the Moser lattice.

• coeff : Coeff

  The lattice numerator.

• denomPow : ℕ

  The exponent k in the denominator 3^k.

@[implicit_reducible]

instance LeanPool.MoserLatticeColorings.instDecidableEqRingRep : DecidableEq RingRep

Equations

• LeanPool.MoserLatticeColorings.instDecidableEqRingRep = LeanPool.MoserLatticeColorings.instDecidableEqRingRep.decEq

def LeanPool.MoserLatticeColorings.instDecidableEqRingRep.decEq (x✝ x✝¹ : RingRep) : Decidable (x✝ = x✝¹)

Equations

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

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

The Euclidean embedding of a Moser-ring representative.

Equations

• p.toR2 = (3 ^ p.denomPow)⁻¹ • p.coeff.toR2

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

The first parity color of a representative.

Equations

• p.color = p.coeff.color

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

The second parity color of a representative.

Equations

• p.colorTwo = p.coeff.colorTwo

def LeanPool.MoserLatticeColorings.RingRep.crossDiff (p q : RingRep) : Coeff

Common-denominator numerator of p - q.

Equations

• p.crossDiff q = (LeanPool.MoserLatticeColorings.Coeff.scale (3 ^ q.denomPow) p.coeff).sub (LeanPool.MoserLatticeColorings.Coeff.scale (3 ^ p.denomPow) q.coeff)

theorem LeanPool.MoserLatticeColorings.RingRep.crossDiff_color_eq_zero_iff (p q : RingRep) : (p.crossDiff q).color = 0 ↔ p.color = q.color

theorem LeanPool.MoserLatticeColorings.RingRep.crossDiff_colorTwo_eq_zero_iff (p q : RingRep) : (p.crossDiff q).colorTwo = 0 ↔ p.colorTwo = q.colorTwo

theorem LeanPool.MoserLatticeColorings.RingRep.crossDiff_toR2 (p q : RingRep) : (p.crossDiff q).toR2 = 3 ^ (p.denomPow + q.denomPow) • (p.toR2 - q.toR2)

theorem LeanPool.MoserLatticeColorings.RingRep.crossDiff_dist_zero (p q : RingRep) : dist (p.crossDiff q).toR2 0 = 3 ^ (p.denomPow + q.denomPow) * dist p.toR2 q.toR2

theorem LeanPool.MoserLatticeColorings.RingRep.scaled_norm_coordinates_eq_of_dist_eq {p q r s : RingRep} (h : dist p.toR2 q.toR2 = dist r.toR2 s.toR2) : 3 ^ (2 * (r.denomPow + s.denomPow)) * (p.crossDiff q).normRational = 3 ^ (2 * (p.denomPow + q.denomPow)) * (r.crossDiff s).normRational ∧ 3 ^ (2 * (r.denomPow + s.denomPow)) * (p.crossDiff q).normRadical = 3 ^ (2 * (p.denomPow + q.denomPow)) * (r.crossDiff s).normRadical

theorem LeanPool.MoserLatticeColorings.RingRep.dvd_four_iff_of_scaled_eq {x y : ℤ} {m n : ℕ} (h : 3 ^ (2 * m) * x = 3 ^ (2 * n) * y) : 4 ∣ x ↔ 4 ∣ y

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

Geometricity for a coloring on Moser-ring representatives.

Equations

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

theorem LeanPool.MoserLatticeColorings.RingRep.color_isGeometric : IsGeometricColoring color

theorem LeanPool.MoserLatticeColorings.RingRep.colorTwo_isGeometric : IsGeometricColoring colorTwo

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

theorem LeanPool.MoserLatticeColorings.RingRep.crossDiff_norm_coefficients_of_dist_eq_one {p q : RingRep} (h : dist p.toR2 q.toR2 = 1) : (p.crossDiff q).normRational = 6 * 3 ^ (2 * (p.denomPow + q.denomPow)) ∧ (p.crossDiff q).normRadical = 0

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

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

theorem LeanPool.MoserLatticeColorings.RingRep.norm_coefficients_of_toR2_eq {p q : RingRep} (h : p.toR2 = q.toR2) : (p.crossDiff q).normRational = 0 ∧ (p.crossDiff q).normRadical = 0

theorem LeanPool.MoserLatticeColorings.RingRep.color_eq_of_toR2_eq {p q : RingRep} (h : p.toR2 = q.toR2) : p.color = q.color

theorem LeanPool.MoserLatticeColorings.RingRep.colorTwo_eq_of_toR2_eq {p q : RingRep} (h : p.toR2 = q.toR2) : p.colorTwo = q.colorTwo

def LeanPool.MoserLatticeColorings.moserRingSetoid : Setoid RingRep

Representatives are identified precisely when they embed as the same point of the Euclidean plane.

Equations

• LeanPool.MoserLatticeColorings.moserRingSetoid = { r := fun (p q : LeanPool.MoserLatticeColorings.RingRep) => p.toR2 = q.toR2, iseqv := LeanPool.MoserLatticeColorings.moserRingSetoid._proof_1 }

def LeanPool.MoserLatticeColorings.MoserRing : Type

The Moser ring {(a + bω₁ + cω₃ + dω₁ω₃) / 3^k : a, b, c, d ∈ ℤ, k ∈ ℕ}, quotiented by equality of Euclidean embeddings.

Equations

• LeanPool.MoserLatticeColorings.MoserRing = Quotient LeanPool.MoserLatticeColorings.moserRingSetoid

noncomputable def LeanPool.MoserLatticeColorings.MoserRing.toR2 : MoserRing → R2

The well-defined Euclidean embedding of the Moser ring.

Equations

• LeanPool.MoserLatticeColorings.MoserRing.toR2 = Quotient.lift LeanPool.MoserLatticeColorings.RingRep.toR2 ⋯

def LeanPool.MoserLatticeColorings.MoserRing.color : MoserRing → ZMod 2 × ZMod 2

Dúcz's first parity color, descended to the Moser ring.

Equations

• LeanPool.MoserLatticeColorings.MoserRing.color = Quotient.lift LeanPool.MoserLatticeColorings.RingRep.color ⋯

def LeanPool.MoserLatticeColorings.MoserRing.colorTwo : MoserRing → ZMod 2 × ZMod 2

Dúcz's second parity color, descended to the Moser ring.

Equations

• LeanPool.MoserLatticeColorings.MoserRing.colorTwo = Quotient.lift LeanPool.MoserLatticeColorings.RingRep.colorTwo ⋯

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

@[simp]

theorem LeanPool.MoserLatticeColorings.MoserRing.out_toR2 (p : MoserRing) : (Quotient.out p).toR2 = p.toR2

@[simp]

theorem LeanPool.MoserLatticeColorings.MoserRing.out_color (p : MoserRing) : (Quotient.out p).color = p.color

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

A coloring of the Moser ring is geometric when pairwise color equality depends only on Euclidean distance.

Equations

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

theorem LeanPool.MoserLatticeColorings.MoserRing.color_isGeometric : IsGeometricColoring color

theorem LeanPool.MoserLatticeColorings.MoserRing.colorTwo_isGeometric : IsGeometricColoring colorTwo

def LeanPool.MoserLatticeColorings.MoserRing.unitDistanceGraph : SimpleGraph MoserRing

Unit-distance graph induced by the entire Moser ring.

Equations

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

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

The first parity map as a proper four-coloring of the Moser ring.

Equations

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

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

The second parity map as a proper four-coloring of the Moser ring.

Equations

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

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

theorem LeanPool.MoserLatticeColorings.MoserRing.both_colorings_are_geometric : IsGeometricColoring ⇑coloring ∧ IsGeometricColoring ⇑coloringTwo

Both explicit proper four-colorings of the Moser ring are geometric.

theorem LeanPool.MoserLatticeColorings.MoserRing.graph_colorable_four_of_moserRing_realization {V : Type u_1} (G : SimpleGraph V) (f : V → MoserRing) (hedge : ∀ {v w : V}, G.Adj v w → dist (f v).toR2 (f w).toR2 = 1) : G.Colorable 4

Every graph whose vertices are realized in the Moser ring and whose edges have Euclidean length one is four-colorable.