From ad68a7542c6a80866a252e40ab962e98cd05cb21 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 20:29:26 +0200
Subject: [PATCH 1/4] Start Markov tree descent extension

---
 LeanFrontier/NumberTheory/MarkovTree.lean | 123 ++++++++++++++++++++++
 1 file changed, 123 insertions(+)
 create mode 100644 LeanFrontier/NumberTheory/MarkovTree.lean

diff --git a/LeanFrontier/NumberTheory/MarkovTree.lean b/LeanFrontier/NumberTheory/MarkovTree.lean
new file mode 100644
index 00000000..6956c821
--- /dev/null
+++ b/LeanFrontier/NumberTheory/MarkovTree.lean
@@ -0,0 +1,123 @@
+import LeanFrontier.NumberTheory.MarkovEquation
+import Mathlib.Tactic.Omega
+
+/-!
+# Descent for ordered positive Markov triples
+
+The Vieta involution from `LeanFrontier.NumberTheory.MarkovEquation`
+is the local move underlying the Markov tree.
+
+For a positive solution ordered `x ≤ y ≤ z`, the exceptional root
+`(1, 1, 1)` is the only case in which the largest two coordinates can
+coincide without a descending Vieta move. Away from that root, jumping
+the largest coordinate produces another positive coordinate at or below
+the middle one, and hence strictly decreases the largest coordinate.
+-/
+
+namespace LeanFrontier.MarkovTree
+
+private theorem root_of_middle_eq_largest
+    {x y z : ℤ}
+    (hx : 0 < x)
+    (hxy : x ≤ y)
+    (hyz_eq : y = z)
+    (h : MarkovEquation.IsSolution x y z) :
+    x = 1 ∧ y = 1 ∧ z = 1 := by
+  subst z
+  unfold MarkovEquation.IsSolution at h
+
+  have hy : 0 < y := lt_of_lt_of_le hx hxy
+
+  have hsq : x ^ 2 ≤ y ^ 2 := by
+    have hprod : 0 ≤ (y - x) * (y + x) := by
+      exact mul_nonneg (sub_nonneg.mpr hxy) (by linarith)
+    nlinarith
+
+  have hx1 : 1 ≤ x := by omega
+  have hy_sq_pos : 0 < y ^ 2 := by positivity
+
+  have hx_lt_two : x < 2 := by
+    by_contra hx_not
+    have hx2 : 2 ≤ x := by omega
+    nlinarith
+
+  have hx_eq : x = 1 := by omega
+  subst x
+
+  have hy_le : y ≤ 1 := by
+    by_contra hy_not
+    have hy2 : 2 ≤ y := by omega
+    nlinarith
+
+  have hy_eq : y = 1 := by omega
+  subst y
+
+  exact ⟨rfl, rfl, rfl⟩
+
+/--
+For a positive ordered Markov triple other than `(1, 1, 1)`, the Vieta
+jump in the largest coordinate is again positive, lies at or below the
+middle coordinate, and therefore strictly decreases the largest coordinate.
+-/
+theorem jump_descends_ordered_positive
+    {x y z : ℤ}
+    (hx : 0 < x)
+    (hxy : x ≤ y)
+    (hyz : y ≤ z)
+    (h : MarkovEquation.IsSolution x y z)
+    (hne : ¬ (x = 1 ∧ y = 1 ∧ z = 1)) :
+    0 < MarkovEquation.jump x y z ∧
+      MarkovEquation.jump x y z ≤ y ∧
+      MarkovEquation.jump x y z < z := by
+  have hy : 0 < y := lt_of_lt_of_le hx hxy
+  have hz : 0 < z := lt_of_lt_of_le hy hyz
+
+  have hyz_ne : y ≠ z := by
+    intro hyz_eq
+    exact hne (root_of_middle_eq_largest hx hxy hyz_eq h)
+
+  have hyz_lt : y < z := lt_of_le_of_ne hyz hyz_ne
+
+  have hjump_pos : 0 < MarkovEquation.jump x y z :=
+    MarkovEquation.jump_pos hx hz h
+
+  have hsq : x ^ 2 ≤ y ^ 2 := by
+    have hprod : 0 ≤ (y - x) * (y + x) := by
+      exact mul_nonneg (sub_nonneg.mpr hxy) (by linarith)
+    nlinarith
+
+  have hx_minus_one : 0 ≤ x - 1 := by omega
+  have htail : 0 ≤ (x - 1) * y ^ 2 :=
+    mul_nonneg hx_minus_one (sq_nonneg y)
+
+  have hpoly : x ^ 2 + 2 * y ^ 2 - 3 * x * y ^ 2 ≤ 0 := by
+    nlinarith
+
+  have hfactor :
+      (y - z) * (y - MarkovEquation.jump x y z) =
+        x ^ 2 + 2 * y ^ 2 - 3 * x * y ^ 2 := by
+    calc
+      (y - z) * (y - MarkovEquation.jump x y z) =
+          y ^ 2 - 3 * x * y ^ 2 + z * MarkovEquation.jump x y z := by
+            rw [MarkovEquation.jump]
+            ring
+      _ = x ^ 2 + 2 * y ^ 2 - 3 * x * y ^ 2 := by
+            rw [MarkovEquation.mul_jump_eq h]
+            ring
+
+  have hleft_neg : y - z < 0 := by linarith
+
+  have hjump_le : MarkovEquation.jump x y z ≤ y := by
+    have hright_nonneg : 0 ≤ y - MarkovEquation.jump x y z := by
+      by_contra hn
+      have hright_neg : y - MarkovEquation.jump x y z < 0 :=
+        lt_of_not_ge hn
+      have hpositive :
+          0 < (y - z) * (y - MarkovEquation.jump x y z) :=
+        mul_pos_of_neg_of_neg hleft_neg hright_neg
+      nlinarith
+    exact sub_nonneg.mp hright_nonneg
+
+  exact ⟨hjump_pos, hjump_le, lt_of_le_of_lt hjump_le hyz_lt⟩
+
+end LeanFrontier.MarkovTree

From 7a72359223f04ec01859225d05652eac71f316d7 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 20:30:00 +0200
Subject: [PATCH 2/4] Add Markov tree descent submission claim

---
 Submissions/markov-tree-descent.json | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 Submissions/markov-tree-descent.json

diff --git a/Submissions/markov-tree-descent.json b/Submissions/markov-tree-descent.json
new file mode 100644
index 00000000..2c16d455
--- /dev/null
+++ b/Submissions/markov-tree-descent.json
@@ -0,0 +1,17 @@
+{
+  "protocol_version": "0.1",
+  "submission_id": "markov-tree-descent",
+  "producer": {
+    "type": "autonomous_agent",
+    "model": "gpt-5.6-sol",
+    "agent": "chatgpt"
+  },
+  "origin_mode": "target_driven",
+  "statement_origin": "machine",
+  "proof_origin": "machine",
+  "entrypoints": [
+    "LeanFrontier.MarkovTree.jump_descends_ordered_positive"
+  ],
+  "base_mathlib_revision": "v4.33.1",
+  "source_context": "Extension of the accepted Markov-equation Vieta-jumping submission. The human operator chose the Markov-tree direction from a shortlist proposed by the agent; the formal theorem statement and Lean proof were authored by the agent. The accepted MarkovEquation module deliberately leaves the tree's descent ordering for separate work. This submission proves the local descent step for a positive ordered Markov triple x <= y <= z away from the root (1,1,1): the existing Vieta jump in the largest coordinate stays positive, is at most the middle coordinate, and therefore strictly decreases the largest coordinate. The proof imports and depends on the accepted MarkovEquation API, in particular jump_pos and mul_jump_eq, rather than restating the Vieta involution. No claim of new mathematics is made; this is a formalization of the classical Markov-tree descent mechanism."
+}

From 0b5639d85382e0d7a2e1ed0160bcddd61614c845 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 20:30:20 +0200
Subject: [PATCH 3/4] Clarify target-selection provenance

---
 Submissions/markov-tree-descent.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Submissions/markov-tree-descent.json b/Submissions/markov-tree-descent.json
index 2c16d455..ff024eee 100644
--- a/Submissions/markov-tree-descent.json
+++ b/Submissions/markov-tree-descent.json
@@ -13,5 +13,5 @@
     "LeanFrontier.MarkovTree.jump_descends_ordered_positive"
   ],
   "base_mathlib_revision": "v4.33.1",
-  "source_context": "Extension of the accepted Markov-equation Vieta-jumping submission. The human operator chose the Markov-tree direction from a shortlist proposed by the agent; the formal theorem statement and Lean proof were authored by the agent. The accepted MarkovEquation module deliberately leaves the tree's descent ordering for separate work. This submission proves the local descent step for a positive ordered Markov triple x <= y <= z away from the root (1,1,1): the existing Vieta jump in the largest coordinate stays positive, is at most the middle coordinate, and therefore strictly decreases the largest coordinate. The proof imports and depends on the accepted MarkovEquation API, in particular jump_pos and mul_jump_eq, rather than restating the Vieta involution. No claim of new mathematics is made; this is a formalization of the classical Markov-tree descent mechanism."
+  "source_context": "Extension of the accepted Markov-equation Vieta-jumping submission. The agent independently surveyed the LeanFrontier corpus and identified several extension directions it considered worthwhile, including Markov-tree descent, a Ford-circle/Mathlib geometry bridge, a Stern-Brocot positive-rational development, and Thue-Morse cube-freeness. It recommended Markov-tree descent as the best combination of mathematical interest, reuse of accepted LeanFrontier results, and realistic formalization scope. The human operator then selected that recommended Markov-tree direction from the agent's shortlist; the human did not author or materially edit the formal theorem statement or proof. The formal statement and Lean proof in this submission were authored by the agent. The accepted MarkovEquation module deliberately leaves the tree's descent ordering for separate work. This submission proves the local descent step for a positive ordered Markov triple x <= y <= z away from the root (1,1,1): the existing Vieta jump in the largest coordinate stays positive, is at most the middle coordinate, and therefore strictly decreases the largest coordinate. The proof imports and depends on the accepted MarkovEquation API, in particular jump_pos and mul_jump_eq, rather than restating the Vieta involution. No claim of new mathematics is made; this is a formalization of the classical Markov-tree descent mechanism."
 }

From ca6a1c3b092e56a24292d424c4ba389df72c63c6 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sun, 13 Sep 2026 20:42:58 +0200
Subject: [PATCH 4/4] Remove unavailable Omega import from Markov descent proof

---
 LeanFrontier/NumberTheory/MarkovTree.lean | 30 +++++++++++++++++------
 1 file changed, 22 insertions(+), 8 deletions(-)

diff --git a/LeanFrontier/NumberTheory/MarkovTree.lean b/LeanFrontier/NumberTheory/MarkovTree.lean
index 6956c821..c89eb1a7 100644
--- a/LeanFrontier/NumberTheory/MarkovTree.lean
+++ b/LeanFrontier/NumberTheory/MarkovTree.lean
@@ -1,5 +1,4 @@
 import LeanFrontier.NumberTheory.MarkovEquation
-import Mathlib.Tactic.Omega
 
 /-!
 # Descent for ordered positive Markov triples
@@ -33,23 +32,34 @@ private theorem root_of_middle_eq_largest
       exact mul_nonneg (sub_nonneg.mpr hxy) (by linarith)
     nlinarith
 
-  have hx1 : 1 ≤ x := by omega
-  have hy_sq_pos : 0 < y ^ 2 := by positivity
+  have hx1 : 1 ≤ x := by
+    have h1 : 0 + 1 ≤ x := Int.add_one_le_iff.mpr hx
+    simpa using h1
 
   have hx_lt_two : x < 2 := by
     by_contra hx_not
-    have hx2 : 2 ≤ x := by omega
+    have hx2 : 2 ≤ x := le_of_not_gt hx_not
     nlinarith
 
-  have hx_eq : x = 1 := by omega
+  have hx_le_one : x ≤ 1 := by
+    have hlt : x < 1 + 1 := by simpa using hx_lt_two
+    exact Int.lt_add_one_iff.mp hlt
+
+  have hx_eq : x = 1 := le_antisymm hx_le_one hx1
   subst x
 
+  have hy1 : 1 ≤ y := by
+    have h1 : 0 + 1 ≤ y := Int.add_one_le_iff.mpr hy
+    simpa using h1
+
   have hy_le : y ≤ 1 := by
     by_contra hy_not
-    have hy2 : 2 ≤ y := by omega
+    have hy_gt_one : 1 < y := lt_of_not_ge hy_not
+    have hy2' : 1 + 1 ≤ y := Int.add_one_le_iff.mpr hy_gt_one
+    have hy2 : 2 ≤ y := by simpa using hy2'
     nlinarith
 
-  have hy_eq : y = 1 := by omega
+  have hy_eq : y = 1 := le_antisymm hy_le hy1
   subst y
 
   exact ⟨rfl, rfl, rfl⟩
@@ -86,7 +96,11 @@ theorem jump_descends_ordered_positive
       exact mul_nonneg (sub_nonneg.mpr hxy) (by linarith)
     nlinarith
 
-  have hx_minus_one : 0 ≤ x - 1 := by omega
+  have hx1 : 1 ≤ x := by
+    have h1 : 0 + 1 ≤ x := Int.add_one_le_iff.mpr hx
+    simpa using h1
+
+  have hx_minus_one : 0 ≤ x - 1 := sub_nonneg.mpr hx1
   have htail : 0 ≤ (x - 1) * y ^ 2 :=
     mul_nonneg hx_minus_one (sq_nonneg y)