From ea6e131a8ce177e2237ac45b11cb12a676c4acfd Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 20:58:36 -0700 Subject: [PATCH 1/3] feat: formalize parametric families for A280831 --- FormalConjectures/OEIS/A280831Families.lean | 78 +++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 FormalConjectures/OEIS/A280831Families.lean diff --git a/FormalConjectures/OEIS/A280831Families.lean b/FormalConjectures/OEIS/A280831Families.lean new file mode 100644 index 0000000000..8d6aadd0d5 --- /dev/null +++ b/FormalConjectures/OEIS/A280831Families.lean @@ -0,0 +1,78 @@ +/- +Copyright 2026 The Formal Conjectures Authors. + +Licensed under the Apache License, Version 2.0 (the "License"); +you may not use this file except in compliance with the License. +You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + +Unless required by applicable law or agreed to in writing, software +distributed under the License is distributed on an "AS IS" BASIS, +WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +See the License for the specific language governing permissions and +limitations under the License. +-/ + +import FormalConjectures.OEIS.«280831» + +/-! +# Parametric families for Sun's 1680-conjecture + +This file records two concrete reductions toward OEIS A280831. + +First, every three-square representation is automatically admissible by taking +`z = 0`. Thus only the classical Legendre exceptional shape needs additional +work. + +Second, whenever `c^4 + 1680 d = q^2`, choosing + +`x = c y`, `z = d y` + +makes the quartic condition a square identically. This yields an explicit +family of admissible integers + +`(c^2 + 1 + d^2) y^2 + w^2`. +-/ + +namespace OeisA280831 + +/-- Every representation by three squares gives an A280831 representation by taking `z = 0`. -/ +theorem of_three_squares (n x y w : ℕ) (h : n = x ^ 2 + y ^ 2 + w ^ 2) : A n := by + refine ⟨x, y, 0, w, ?_, ?_⟩ + · simpa [h, add_assoc] + · refine ⟨x ^ 2, ?_⟩ + ring + +/-- General algebraic family: a solution of `c^4 + 1680 d = q^2` gives infinitely many +A280831 representations. -/ +theorem parametric_family (c d q y w : ℕ) (h : c ^ 4 + 1680 * d = q ^ 2) : + A ((c ^ 2 + 1 + d ^ 2) * y ^ 2 + w ^ 2) := by + refine ⟨c * y, y, d * y, w, ?_, ?_⟩ + · ring + · refine ⟨q * y ^ 2, ?_⟩ + calc + (c * y) ^ 4 + 1680 * y ^ 3 * (d * y) = + (c ^ 4 + 1680 * d) * y ^ 4 := by ring + _ = q ^ 2 * y ^ 4 := by rw [h] + _ = (q * y ^ 2) * (q * y ^ 2) := by ring + +/-- The identity `1^4 + 1680 = 41^2` gives every number `3 y^2 + w^2`. -/ +theorem family_three (y w : ℕ) : A (3 * y ^ 2 + w ^ 2) := by + simpa using parametric_family 1 1 41 y w (by norm_num) + +/-- The identity `1^4 + 1680 · 3 = 71^2` gives every number `11 y^2 + w^2`. -/ +theorem family_eleven (y w : ℕ) : A (11 * y ^ 2 + w ^ 2) := by + simpa using parametric_family 1 3 71 y w (by norm_num) + +/-- The identity `4^4 + 1680 = 44^2` gives every number `18 y^2 + w^2`. -/ +theorem family_eighteen (y w : ℕ) : A (18 * y ^ 2 + w ^ 2) := by + simpa using parametric_family 4 1 44 y w (by norm_num) + +#print axioms of_three_squares +#print axioms parametric_family +#print axioms family_three +#print axioms family_eleven +#print axioms family_eighteen + +end OeisA280831 From 58797393438be078942dc8c7bc2d456d01779fee Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 21:18:15 -0700 Subject: [PATCH 2/3] fix: target the exact A280831 predicate --- FormalConjectures/OEIS/A280831Families.lean | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/FormalConjectures/OEIS/A280831Families.lean b/FormalConjectures/OEIS/A280831Families.lean index 8d6aadd0d5..62b53d7e00 100644 --- a/FormalConjectures/OEIS/A280831Families.lean +++ b/FormalConjectures/OEIS/A280831Families.lean @@ -38,7 +38,8 @@ family of admissible integers namespace OeisA280831 /-- Every representation by three squares gives an A280831 representation by taking `z = 0`. -/ -theorem of_three_squares (n x y w : ℕ) (h : n = x ^ 2 + y ^ 2 + w ^ 2) : A n := by +theorem of_three_squares (n x y w : ℕ) (h : n = x ^ 2 + y ^ 2 + w ^ 2) : + HasSquareCondition n := by refine ⟨x, y, 0, w, ?_, ?_⟩ · simpa [h, add_assoc] · refine ⟨x ^ 2, ?_⟩ @@ -47,7 +48,7 @@ theorem of_three_squares (n x y w : ℕ) (h : n = x ^ 2 + y ^ 2 + w ^ 2) : A n : /-- General algebraic family: a solution of `c^4 + 1680 d = q^2` gives infinitely many A280831 representations. -/ theorem parametric_family (c d q y w : ℕ) (h : c ^ 4 + 1680 * d = q ^ 2) : - A ((c ^ 2 + 1 + d ^ 2) * y ^ 2 + w ^ 2) := by + HasSquareCondition ((c ^ 2 + 1 + d ^ 2) * y ^ 2 + w ^ 2) := by refine ⟨c * y, y, d * y, w, ?_, ?_⟩ · ring · refine ⟨q * y ^ 2, ?_⟩ @@ -58,15 +59,15 @@ theorem parametric_family (c d q y w : ℕ) (h : c ^ 4 + 1680 * d = q ^ 2) : _ = (q * y ^ 2) * (q * y ^ 2) := by ring /-- The identity `1^4 + 1680 = 41^2` gives every number `3 y^2 + w^2`. -/ -theorem family_three (y w : ℕ) : A (3 * y ^ 2 + w ^ 2) := by +theorem family_three (y w : ℕ) : HasSquareCondition (3 * y ^ 2 + w ^ 2) := by simpa using parametric_family 1 1 41 y w (by norm_num) /-- The identity `1^4 + 1680 · 3 = 71^2` gives every number `11 y^2 + w^2`. -/ -theorem family_eleven (y w : ℕ) : A (11 * y ^ 2 + w ^ 2) := by +theorem family_eleven (y w : ℕ) : HasSquareCondition (11 * y ^ 2 + w ^ 2) := by simpa using parametric_family 1 3 71 y w (by norm_num) /-- The identity `4^4 + 1680 = 44^2` gives every number `18 y^2 + w^2`. -/ -theorem family_eighteen (y w : ℕ) : A (18 * y ^ 2 + w ^ 2) := by +theorem family_eighteen (y w : ℕ) : HasSquareCondition (18 * y ^ 2 + w ^ 2) := by simpa using parametric_family 4 1 44 y w (by norm_num) #print axioms of_three_squares From c39efc8f29479a6111a627fb388a846147a40556 Mon Sep 17 00:00:00 2001 From: DomTheDeveloper Date: Sat, 25 Jul 2026 21:32:35 -0700 Subject: [PATCH 3/3] feat: prove square-scaling closure for A280831 --- FormalConjectures/OEIS/A280831Families.lean | 33 +++++++++++++++++++-- 1 file changed, 31 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/OEIS/A280831Families.lean b/FormalConjectures/OEIS/A280831Families.lean index 62b53d7e00..5b0ae1486e 100644 --- a/FormalConjectures/OEIS/A280831Families.lean +++ b/FormalConjectures/OEIS/A280831Families.lean @@ -19,13 +19,17 @@ import FormalConjectures.OEIS.«280831» /-! # Parametric families for Sun's 1680-conjecture -This file records two concrete reductions toward OEIS A280831. +This file records concrete reductions toward OEIS A280831. First, every three-square representation is automatically admissible by taking `z = 0`. Thus only the classical Legendre exceptional shape needs additional work. -Second, whenever `c^4 + 1680 d = q^2`, choosing +Second, the square condition is stable under multiplying the represented +integer by any square. In particular, once the odd core of a number +`4^a (8b+7)` is handled, the factor `4^a` follows automatically. + +Third, whenever `c^4 + 1680 d = q^2`, choosing `x = c y`, `z = d y` @@ -45,6 +49,29 @@ theorem of_three_squares (n x y w : ℕ) (h : n = x ^ 2 + y ^ 2 + w ^ 2) : · refine ⟨x ^ 2, ?_⟩ ring +/-- The A280831 condition is preserved after multiplying the represented integer by a square. -/ +theorem scale_by_square (n t : ℕ) (h : HasSquareCondition n) : + HasSquareCondition (t ^ 2 * n) := by + rcases h with ⟨x, y, z, w, hn, hsquare⟩ + rcases hsquare with ⟨q, hq⟩ + refine ⟨t * x, t * y, t * z, t * w, ?_, ?_⟩ + · rw [hn] + ring + · refine ⟨t ^ 2 * q, ?_⟩ + calc + (t * x) ^ 4 + 1680 * (t * y) ^ 3 * (t * z) = + t ^ 4 * (x ^ 4 + 1680 * y ^ 3 * z) := by ring + _ = t ^ 4 * (q * q) := by rw [hq] + _ = (t ^ 2 * q) * (t ^ 2 * q) := by ring + +/-- Closure under the exact powers of four occurring in Legendre's three-square obstruction. -/ +theorem scale_by_four_pow (n a : ℕ) (h : HasSquareCondition n) : + HasSquareCondition (4 ^ a * n) := by + have hpow : (2 ^ a) ^ 2 = 4 ^ a := by + rw [pow_two, ← mul_pow] + norm_num + simpa [hpow] using scale_by_square n (2 ^ a) h + /-- General algebraic family: a solution of `c^4 + 1680 d = q^2` gives infinitely many A280831 representations. -/ theorem parametric_family (c d q y w : ℕ) (h : c ^ 4 + 1680 * d = q ^ 2) : @@ -71,6 +98,8 @@ theorem family_eighteen (y w : ℕ) : HasSquareCondition (18 * y ^ 2 + w ^ 2) := simpa using parametric_family 4 1 44 y w (by norm_num) #print axioms of_three_squares +#print axioms scale_by_square +#print axioms scale_by_four_pow #print axioms parametric_family #print axioms family_three #print axioms family_eleven