Connectivity of natural-number Markoff solutions

Every nonzero solution in natural numbers of

x₁² + x₂² + x₃² = 3 * x₁ * x₂ * x₃

is connected to (1, 1, 1) by coordinate transpositions and the natural-number Vieta moves. The proof is the classical descent: after ordering the coordinates a ≤ b ≤ c, replace c by 3ab - c. Away from (1, 1, 1), this is positive and strictly smaller than c.

Natural subtraction is used only after proving the needed lower bound, so reduction to a ring recovers the usual Vieta involution.

def BGS.Markoff.natVieta1 (x : Point ℕ) : Point ℕ

The first Vieta replacement on points with natural-number coordinates.

Equations

• BGS.Markoff.natVieta1 x = { x1 := 3 * x.x2 * x.x3 - x.x1, x2 := x.x2, x3 := x.x3 }

def BGS.Markoff.natVieta2 (x : Point ℕ) : Point ℕ

The second Vieta replacement on points with natural-number coordinates.

Equations

• BGS.Markoff.natVieta2 x = { x1 := x.x1, x2 := 3 * x.x1 * x.x3 - x.x2, x3 := x.x3 }

def BGS.Markoff.natVieta3 (x : Point ℕ) : Point ℕ

The third Vieta replacement on points with natural-number coordinates.

Equations

• BGS.Markoff.natVieta3 x = { x1 := x.x1, x2 := x.x2, x3 := 3 * x.x1 * x.x2 - x.x3 }

theorem BGS.Markoff.isSemiringMarkoff_natVieta1 (x : Point ℕ) (hx : IsSemiringMarkoff x) : IsSemiringMarkoff (natVieta1 x)

theorem BGS.Markoff.isSemiringMarkoff_natVieta2 (x : Point ℕ) (hx : IsSemiringMarkoff x) : IsSemiringMarkoff (natVieta2 x)

theorem BGS.Markoff.isSemiringMarkoff_natVieta3 (x : Point ℕ) (hx : IsSemiringMarkoff x) : IsSemiringMarkoff (natVieta3 x)

def BGS.Markoff.natVieta1Surface (x : SemiringMarkoffSurface ℕ) : SemiringMarkoffSurface ℕ

The first natural-number Vieta move restricted to the Markoff surface.

Equations

• BGS.Markoff.natVieta1Surface x = ⟨BGS.Markoff.natVieta1 ↑x, ⋯⟩

def BGS.Markoff.natVieta2Surface (x : SemiringMarkoffSurface ℕ) : SemiringMarkoffSurface ℕ

The second natural-number Vieta move restricted to the Markoff surface.

Equations

• BGS.Markoff.natVieta2Surface x = ⟨BGS.Markoff.natVieta2 ↑x, ⋯⟩

def BGS.Markoff.natVieta3Surface (x : SemiringMarkoffSurface ℕ) : SemiringMarkoffSurface ℕ

The third natural-number Vieta move restricted to the Markoff surface.

Equations

• BGS.Markoff.natVieta3Surface x = ⟨BGS.Markoff.natVieta3 ↑x, ⋯⟩

def BGS.Markoff.natSwap12Surface (x : SemiringMarkoffSurface ℕ) : SemiringMarkoffSurface ℕ

Exchange the first two coordinates of a natural-number Markoff solution.

Equations

• BGS.Markoff.natSwap12Surface x = ⟨BGS.Markoff.swap12 ↑x, ⋯⟩

def BGS.Markoff.natSwap23Surface (x : SemiringMarkoffSurface ℕ) : SemiringMarkoffSurface ℕ

Exchange the last two coordinates of a natural-number Markoff solution.

Equations

• BGS.Markoff.natSwap23Surface x = ⟨BGS.Markoff.swap23 ↑x, ⋯⟩

@[simp]

theorem BGS.Markoff.natVieta1Surface_coe (x : SemiringMarkoffSurface ℕ) : ↑(natVieta1Surface x) = natVieta1 ↑x

@[simp]

theorem BGS.Markoff.natVieta2Surface_coe (x : SemiringMarkoffSurface ℕ) : ↑(natVieta2Surface x) = natVieta2 ↑x

@[simp]

theorem BGS.Markoff.natVieta3Surface_coe (x : SemiringMarkoffSurface ℕ) : ↑(natVieta3Surface x) = natVieta3 ↑x

@[simp]

theorem BGS.Markoff.natSwap12Surface_coe (x : SemiringMarkoffSurface ℕ) : ↑(natSwap12Surface x) = swap12 ↑x

@[simp]

theorem BGS.Markoff.natSwap23Surface_coe (x : SemiringMarkoffSurface ℕ) : ↑(natSwap23Surface x) = swap23 ↑x

@[simp]

theorem BGS.Markoff.natVieta1Surface_involutive (x : SemiringMarkoffSurface ℕ) : natVieta1Surface (natVieta1Surface x) = x

@[simp]

theorem BGS.Markoff.natVieta2Surface_involutive (x : SemiringMarkoffSurface ℕ) : natVieta2Surface (natVieta2Surface x) = x

@[simp]

theorem BGS.Markoff.natVieta3Surface_involutive (x : SemiringMarkoffSurface ℕ) : natVieta3Surface (natVieta3Surface x) = x

@[simp]

theorem BGS.Markoff.natSwap12Surface_involutive (x : SemiringMarkoffSurface ℕ) : natSwap12Surface (natSwap12Surface x) = x

@[simp]

theorem BGS.Markoff.natSwap23Surface_involutive (x : SemiringMarkoffSurface ℕ) : natSwap23Surface (natSwap23Surface x) = x

def BGS.Markoff.natVieta1SurfaceEquiv : Equiv.Perm (SemiringMarkoffSurface ℕ)

The first natural Vieta move as a permutation of the natural Markoff surface.

Equations

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

def BGS.Markoff.natVieta2SurfaceEquiv : Equiv.Perm (SemiringMarkoffSurface ℕ)

The second natural Vieta move as a permutation of the natural Markoff surface.

Equations

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

def BGS.Markoff.natVieta3SurfaceEquiv : Equiv.Perm (SemiringMarkoffSurface ℕ)

The third natural Vieta move as a permutation of the natural Markoff surface.

Equations

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

def BGS.Markoff.natSwap12SurfaceEquiv : Equiv.Perm (SemiringMarkoffSurface ℕ)

The first coordinate transposition as a permutation of the natural Markoff surface.

Equations

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

def BGS.Markoff.natSwap23SurfaceEquiv : Equiv.Perm (SemiringMarkoffSurface ℕ)

The second coordinate transposition as a permutation of the natural Markoff surface.

Equations

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

def BGS.Markoff.naturalGammaGenerators : Set (Equiv.Perm (SemiringMarkoffSurface ℕ))

The five standard generators acting on natural-number Markoff solutions.

Equations

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

def BGS.Markoff.NaturalGamma : Subgroup (Equiv.Perm (SemiringMarkoffSurface ℕ))

The group generated by natural Vieta moves and coordinate transpositions.

Equations

• BGS.Markoff.NaturalGamma = Subgroup.closure BGS.Markoff.naturalGammaGenerators

theorem BGS.Markoff.natVieta1SurfaceEquiv_mem_NaturalGamma : natVieta1SurfaceEquiv ∈ NaturalGamma

theorem BGS.Markoff.natVieta2SurfaceEquiv_mem_NaturalGamma : natVieta2SurfaceEquiv ∈ NaturalGamma

theorem BGS.Markoff.natVieta3SurfaceEquiv_mem_NaturalGamma : natVieta3SurfaceEquiv ∈ NaturalGamma

theorem BGS.Markoff.natSwap12SurfaceEquiv_mem_NaturalGamma : natSwap12SurfaceEquiv ∈ NaturalGamma

theorem BGS.Markoff.natSwap23SurfaceEquiv_mem_NaturalGamma : natSwap23SurfaceEquiv ∈ NaturalGamma

def BGS.Markoff.SameNatMarkoffComponent (x y : SemiringMarkoffSurface ℕ) : Prop

The orbit relation for the natural Markoff group.

Equations

• BGS.Markoff.SameNatMarkoffComponent x y = (y ∈ MulAction.orbit (↥BGS.Markoff.NaturalGamma) x)

theorem BGS.Markoff.sameNatMarkoffComponent_iff_exists (x y : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x y ↔ ∃ (g : ↥NaturalGamma), g • x = y

inductive BGS.Markoff.NatMarkoffStep : SemiringMarkoffSurface ℕ → SemiringMarkoffSurface ℕ → Prop

A single standard move between natural-number Markoff solutions.

• vieta1 (x : SemiringMarkoffSurface ℕ) : NatMarkoffStep x (natVieta1Surface x)
• vieta2 (x : SemiringMarkoffSurface ℕ) : NatMarkoffStep x (natVieta2Surface x)
• vieta3 (x : SemiringMarkoffSurface ℕ) : NatMarkoffStep x (natVieta3Surface x)
• swap12 (x : SemiringMarkoffSurface ℕ) : NatMarkoffStep x (natSwap12Surface x)
• swap23 (x : SemiringMarkoffSurface ℕ) : NatMarkoffStep x (natSwap23Surface x)

theorem BGS.Markoff.sameNatMarkoffComponent_refl (x : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x x

theorem BGS.Markoff.sameNatMarkoffComponent_symm {x y : SemiringMarkoffSurface ℕ} (h : SameNatMarkoffComponent x y) : SameNatMarkoffComponent y x

theorem BGS.Markoff.sameNatMarkoffComponent_trans {x y z : SemiringMarkoffSurface ℕ} (hxy : SameNatMarkoffComponent x y) (hyz : SameNatMarkoffComponent y z) : SameNatMarkoffComponent x z

theorem BGS.Markoff.sameNatMarkoffComponent_vieta1 (x : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x (natVieta1Surface x)

theorem BGS.Markoff.sameNatMarkoffComponent_vieta2 (x : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x (natVieta2Surface x)

theorem BGS.Markoff.sameNatMarkoffComponent_vieta3 (x : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x (natVieta3Surface x)

theorem BGS.Markoff.sameNatMarkoffComponent_swap12 (x : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x (natSwap12Surface x)

theorem BGS.Markoff.sameNatMarkoffComponent_swap23 (x : SemiringMarkoffSurface ℕ) : SameNatMarkoffComponent x (natSwap23Surface x)

theorem BGS.Markoff.eqvGen_natMarkoffStep_sameComponent {x y : SemiringMarkoffSurface ℕ} (h : Relation.EqvGen NatMarkoffStep x y) : SameNatMarkoffComponent x y

A generated sequence of standard natural moves lies in a single NaturalGamma orbit.

def BGS.Markoff.natMarkoffHeight (x : SemiringMarkoffSurface ℕ) : ℕ

Sum of the coordinates, used as the well-founded descent measure.

Equations

• BGS.Markoff.natMarkoffHeight x = (↑x).x1 + (↑x).x2 + (↑x).x3

theorem BGS.Markoff.natMarkoff_eq_origin_of_x1_eq_zero (x : SemiringMarkoffSurface ℕ) (hx1 : (↑x).x1 = 0) : x = semiringSurfaceOrigin ℕ

theorem BGS.Markoff.natMarkoff_eq_origin_of_x2_eq_zero (x : SemiringMarkoffSurface ℕ) (hx2 : (↑x).x2 = 0) : x = semiringSurfaceOrigin ℕ

theorem BGS.Markoff.natMarkoff_eq_origin_of_x3_eq_zero (x : SemiringMarkoffSurface ℕ) (hx3 : (↑x).x3 = 0) : x = semiringSurfaceOrigin ℕ

theorem BGS.Markoff.natMarkoff_coordinates_pos_of_ne_origin (x : SemiringMarkoffSurface ℕ) (hx : x ≠ semiringSurfaceOrigin ℕ) : 0 < (↑x).x1 ∧ 0 < (↑x).x2 ∧ 0 < (↑x).x3

Every coordinate of a nonzero natural Markoff solution is positive.

theorem BGS.Markoff.natMarkoff_ne_origin_sameComponent_root (x : SemiringMarkoffSurface ℕ) : x ≠ semiringSurfaceOrigin ℕ → SameNatMarkoffComponent (semiringSurfaceRoot ℕ) x

Every nonzero natural-number Markoff solution is in the NaturalGamma orbit of (1,1,1).

theorem BGS.Markoff.natMarkoff_eq_origin_or_sameComponent_root (x : SemiringMarkoffSurface ℕ) : x = semiringSurfaceOrigin ℕ ∨ SameNatMarkoffComponent (semiringSurfaceRoot ℕ) x

The natural Markoff surface consists of the origin and the single orbit rooted at (1,1,1).