From bc2cf4cdcf3df9a8273e561458400046219ffdf7 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 09:47:42 +0200 Subject: [PATCH 1/4] docs: mark landed contribution directions A (#197), B (#207), D (#195) and E (#210) have landed; H's path and interval infrastructure has (#208, #209, #211), the bridge itself has not; C is partly covered by D's trace and charpoly identities. Status lines name modules and entrypoints, not pull requests, as the document asks. Co-Authored-By: Claude Opus 5 --- docs/CONTRIBUTION-DIRECTIONS.md | 25 +++++++++++++++++++------ 1 file changed, 19 insertions(+), 6 deletions(-) diff --git a/docs/CONTRIBUTION-DIRECTIONS.md b/docs/CONTRIBUTION-DIRECTIONS.md index 431e1613..e565b133 100644 --- a/docs/CONTRIBUTION-DIRECTIONS.md +++ b/docs/CONTRIBUTION-DIRECTIONS.md @@ -90,7 +90,8 @@ crossing the Markov uniqueness-conjecture boundary. ### A. Largest Ford circle between Farey neighbours -**Current corpus fit:** ready to investigate. +**Status:** landed as `LeanFrontier.FordCircle.mediant_is_unique_largest_in_farey_gap` +(`LeanFrontier/Geometry/FareyFordCircle.lean`). Build on it rather than restating it. **Primary parents:** @@ -133,7 +134,8 @@ gap." ### B. Ford–Farey–Descartes configuration -**Current corpus fit:** ready to investigate. +**Status:** landed as `LeanFrontier.FordCircle.farey_mediant_descartes_configuration` +(`LeanFrontier/Geometry/FordCircleDescartes.lean`). Build on it rather than restating it. **Primary parents:** @@ -176,7 +178,10 @@ gives `DescartesCircle` a genuine geometric interpretation. ### C. Lucas numbers as characteristic-polynomial data of Fibonacci Q-matrix powers -**Current corpus fit:** ready to investigate. +**Status:** partly covered by D. `LeanFrontier.Horadam.trace_fibMatrix_pow_succ_eq_lucas` +proves the trace form, and the general companion-matrix power characteristic polynomial has +landed, so the statement below may now be a short corollary. Check the catalogue before +submitting it. **Primary parents:** @@ -219,8 +224,10 @@ recurrence, determinant, and Binet-style work. ### D. General Horadam companion matrix -**Current corpus fit:** high-value infrastructure; verify the live catalogue before -implementation. +**Status:** landed in `LeanFrontier/LinearAlgebra/HoradamCompanionMatrix.lean` and +`HoradamCompanionMatrixSpecializations.lean`, including the explicit power formula, trace, +determinant and characteristic-polynomial identities, and the Fibonacci/Lucas specialization. +Build on it rather than restating it. **Primary parents:** @@ -272,6 +279,9 @@ specializations, and later Binet-style results. ### E. Circular square/domino tilings counted by Lucas numbers +**Status:** landed as `LeanFrontier.Nat.card_circularOneTwoTilings_add_two` +(`LeanFrontier/Combinatorics/CircularDominoTilings.lean`). + **Primary parents:** `FibonacciComposition` + `LucasNumber`. Classically, linear square/domino tilings are Fibonacci-counted while circular tilings are @@ -320,7 +330,10 @@ Treat it as a good independent Stern extension, not as a top corpus-synthesis ta ### H. Stern diatomic / Calkin–Wilf to Stern–Brocot representation bridge -**Status:** reformulated; high effort. +**Status:** the infrastructure has landed: both path enumerations +(`LeanFrontier.CalkinWilf.exists_code_eq`, `LeanFrontier.SternBrocot.existsUnique_pair_of_coprime`) +and the Stern–Brocot interval invariants (`LeanFrontier/NumberTheory/SternBrocot/Intervals.lean`). +The bridge itself, relating the two path conventions, remains open. **Critical correction:** From 115dce6327b966bed0c876e634501c1b9dc6ea04 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 09:47:42 +0200 Subject: [PATCH 2/4] chore: replace Mathlib v4.34.0 deprecations in the corpus Eleven deprecation warnings in eight modules would become errors in a later Mathlib and fail that upgrade's audit: Mathlib.Data.Real.Basic and Mathlib.Data.Complex.Basic imports (now Mathlib.Basic.*), if_pos and if_neg (now ite_eq_left and ite_eq_right, same signatures), and Set.mem_setOf_eq (now Set.mem_ofPred_eq). Furstenberg's five haveILetI lints are fixed too; the module now builds without warnings. Proofs only. A frontier-audit of the whole corpus before and after reports the same 477 declarations with identical canonical types, kinds and axioms, and leanchecker passes on every edited module. Remaining warnings (11) are style lints. Co-Authored-By: Claude Opus 5 --- LeanFrontier/Analysis/Nesbitt.lean | 2 +- LeanFrontier/Analysis/SlopeMinorant.lean | 2 +- .../Combinatorics/CircularDominoTilings.lean | 2 +- LeanFrontier/Dynamics/LogisticMap.lean | 4 ++-- LeanFrontier/Geometry/InversiveGeometry.lean | 2 +- LeanFrontier/NumberTheory/SternDiatomic.lean | 4 ++-- LeanFrontier/NumberTheory/ThueMorse.lean | 4 ++-- LeanFrontier/Topology/Furstenberg.lean | 12 ++++++------ 8 files changed, 16 insertions(+), 16 deletions(-) diff --git a/LeanFrontier/Analysis/Nesbitt.lean b/LeanFrontier/Analysis/Nesbitt.lean index 40333645..90f9060d 100644 --- a/LeanFrontier/Analysis/Nesbitt.lean +++ b/LeanFrontier/Analysis/Nesbitt.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Real.Basic +import Mathlib.Basic.Real.Basic import Mathlib.Tactic.FieldSimp import Mathlib.Tactic.Linarith import Mathlib.Tactic.Positivity diff --git a/LeanFrontier/Analysis/SlopeMinorant.lean b/LeanFrontier/Analysis/SlopeMinorant.lean index f3543c01..9dd89bc7 100644 --- a/LeanFrontier/Analysis/SlopeMinorant.lean +++ b/LeanFrontier/Analysis/SlopeMinorant.lean @@ -1,5 +1,5 @@ import Mathlib.Data.Finset.Lattice.Fold -import Mathlib.Data.Real.Basic +import Mathlib.Basic.Real.Basic import Mathlib.Tactic.Linarith import Mathlib.Tactic.Ring diff --git a/LeanFrontier/Combinatorics/CircularDominoTilings.lean b/LeanFrontier/Combinatorics/CircularDominoTilings.lean index 64a46e5e..fe7bd506 100644 --- a/LeanFrontier/Combinatorics/CircularDominoTilings.lean +++ b/LeanFrontier/Combinatorics/CircularDominoTilings.lean @@ -56,7 +56,7 @@ theorem card_circularOneTwoTilings_add_two (n : ℕ) : obtain ⟨l, -, rfl⟩ := Finset.mem_image.mp hxFalse obtain ⟨r, -, h⟩ := Finset.mem_image.mp hxTrue simp at h - rw [circularOneTwoTilings, if_pos htwo, hsub, + rw [circularOneTwoTilings, ite_eq_left htwo, hsub, Finset.card_union_of_disjoint hdisj, Finset.card_image_of_injective _ (by intro a b h diff --git a/LeanFrontier/Dynamics/LogisticMap.lean b/LeanFrontier/Dynamics/LogisticMap.lean index 1a9ea555..d66e7d7c 100644 --- a/LeanFrontier/Dynamics/LogisticMap.lean +++ b/LeanFrontier/Dynamics/LogisticMap.lean @@ -58,10 +58,10 @@ noncomputable def tentMap (x : ℝ) : ℝ := if x ≤ 1 / 2 then 2 * x else 2 * /-- The logistic map at parameter four, `x ↦ 4 * x * (1 - x)`, extended to all of `ℝ`. -/ def logisticMap (x : ℝ) : ℝ := 4 * x * (1 - x) -theorem tentMap_of_le {x : ℝ} (h : x ≤ 1 / 2) : tentMap x = 2 * x := if_pos h +theorem tentMap_of_le {x : ℝ} (h : x ≤ 1 / 2) : tentMap x = 2 * x := ite_eq_left h theorem tentMap_of_half_lt {x : ℝ} (h : 1 / 2 < x) : tentMap x = 2 * (1 - x) := - if_neg (not_le.mpr h) + ite_eq_right (not_le.mpr h) /-- The identity behind both branches of the semiconjugacy: doubling the angle inside `sin ^ 2` is applying the logistic map outside. -/ diff --git a/LeanFrontier/Geometry/InversiveGeometry.lean b/LeanFrontier/Geometry/InversiveGeometry.lean index c3a466f2..935c7dc4 100644 --- a/LeanFrontier/Geometry/InversiveGeometry.lean +++ b/LeanFrontier/Geometry/InversiveGeometry.lean @@ -1,4 +1,4 @@ -import Mathlib.Data.Complex.Basic +import Mathlib.Basic.Complex.Basic import Mathlib.Tactic.LinearCombination /-! diff --git a/LeanFrontier/NumberTheory/SternDiatomic.lean b/LeanFrontier/NumberTheory/SternDiatomic.lean index 8a6dcab5..3e07c66b 100644 --- a/LeanFrontier/NumberTheory/SternDiatomic.lean +++ b/LeanFrontier/NumberTheory/SternDiatomic.lean @@ -65,7 +65,7 @@ theorem fusc_two_mul (n : ℕ) : fusc (2 * n) = fusc n := by · have hm : 2 * (k + 1) = 2 * k + 2 := by ring have heven : (2 * k + 2) % 2 = 0 := by omega have hdiv : (2 * k + 2) / 2 = k + 1 := by omega - rw [hm, fusc, if_pos heven, hdiv] + rw [hm, fusc, ite_eq_left heven, hdiv] /-- An odd index splits into the two neighbouring values at half the index. -/ theorem fusc_two_mul_add_one (n : ℕ) : fusc (2 * n + 1) = fusc n + fusc (n + 1) := by @@ -74,7 +74,7 @@ theorem fusc_two_mul_add_one (n : ℕ) : fusc (2 * n + 1) = fusc n + fusc (n + 1 · have hm : 2 * (k + 1) + 1 = (2 * k + 1) + 2 := by ring have hodd : ¬ ((2 * k + 1 + 2) % 2 = 0) := by omega have hdiv : (2 * k + 1 + 2) / 2 = k + 1 := by omega - rw [hm, fusc, if_neg hodd, hdiv] + rw [hm, fusc, ite_eq_right hodd, hdiv] /-- Consecutive values of Stern's diatomic sequence are coprime, so the fraction `fusc n / fusc (n + 1)` is always in lowest terms. -/ diff --git a/LeanFrontier/NumberTheory/ThueMorse.lean b/LeanFrontier/NumberTheory/ThueMorse.lean index 129ad886..f5933901 100644 --- a/LeanFrontier/NumberTheory/ThueMorse.lean +++ b/LeanFrontier/NumberTheory/ThueMorse.lean @@ -82,9 +82,9 @@ theorem thueMorse_two_mul_add_one (n : ℕ) : thueMorse (2 * n + 1) = !thueMorse theorem thueMorseSign_eq_ite (n : ℕ) : thueMorseSign n = if thueMorse n then -1 else 1 := by rcases Nat.even_or_odd (Nat.digits 2 n).sum with h | h - · rw [thueMorseSign, h.neg_one_pow, if_neg] + · rw [thueMorseSign, h.neg_one_pow, ite_eq_right] simp [thueMorse, Nat.not_odd_iff_even, h] - · rw [thueMorseSign, h.neg_one_pow, if_pos] + · rw [thueMorseSign, h.neg_one_pow, ite_eq_left] simp [thueMorse, h] private theorem thueMorseSign_two_mul (n : ℕ) : thueMorseSign (2 * n) = thueMorseSign n := by diff --git a/LeanFrontier/Topology/Furstenberg.lean b/LeanFrontier/Topology/Furstenberg.lean index bf056890..32306276 100644 --- a/LeanFrontier/Topology/Furstenberg.lean +++ b/LeanFrontier/Topology/Furstenberg.lean @@ -76,7 +76,7 @@ topology. -/ theorem isTopologicalBasis_arithProgression : @IsTopologicalBasis ℤ furstenbergTopology {S : Set ℤ | ∃ a b, b ≠ 0 ∧ S = arithProgression a b} := by - letI := furstenbergTopology + let := furstenbergTopology refine ⟨?_, ?_, rfl⟩ · rintro t₁ ⟨a₁, b₁, hb₁, rfl⟩ t₂ ⟨a₂, b₂, hb₂, rfl⟩ x ⟨hx₁, hx₂⟩ refine ⟨arithProgression x (b₁ * b₂), ⟨x, b₁ * b₂, mul_ne_zero hb₁ hb₂, rfl⟩, @@ -94,7 +94,7 @@ theorem isTopologicalBasis_arithProgression : /-- Arithmetic progressions with nonzero step are open. -/ theorem isOpen_arithProgression (a b : ℤ) (hb : b ≠ 0) : IsOpen[furstenbergTopology] (arithProgression a b) := by - letI := furstenbergTopology + let := furstenbergTopology exact isTopologicalBasis_arithProgression.isOpen ⟨a, b, hb, rfl⟩ /-- Arithmetic progressions with nonzero step are closed: after reducing to a positive @@ -103,7 +103,7 @@ residues. Together with `isOpen_arithProgression`, the basic sets of the Fursten topology are clopen. -/ theorem isClosed_arithProgression (a : ℤ) {b : ℤ} (hb : b ≠ 0) : IsClosed[furstenbergTopology] (arithProgression a b) := by - letI := furstenbergTopology + let := furstenbergTopology have habs : arithProgression a b = arithProgression a |b| := Set.ext fun x => (abs_dvd b (x - a)).symm have hpos : 0 < |b| := abs_pos.mpr hb @@ -148,7 +148,7 @@ theorem infinite_arithProgression (a : ℤ) {b : ℤ} (hb : b ≠ 0) : arithmetic progression around each of its points. -/ theorem infinite_of_isOpen {U : Set ℤ} (hU : IsOpen[furstenbergTopology] U) (hne : U.Nonempty) : U.Infinite := by - letI := furstenbergTopology + let := furstenbergTopology obtain ⟨x, hx⟩ := hne obtain ⟨V, ⟨a, b, hb, rfl⟩, -, hVU⟩ := isTopologicalBasis_arithProgression.exists_subset_of_mem_open hx hU @@ -159,7 +159,7 @@ the integers other than `1` and `-1`. -/ theorem iUnion_prime_arithProgression : ⋃ p ∈ {p : ℕ | p.Prime}, arithProgression 0 (p : ℤ) = ({1, -1} : Set ℤ)ᶜ := by ext x - simp only [mem_iUnion, mem_setOf_eq, mem_arithProgression, sub_zero, mem_compl_iff, + simp only [mem_iUnion, mem_ofPred_eq, mem_arithProgression, sub_zero, mem_compl_iff, mem_insert_iff, mem_singleton_iff, exists_prop] constructor · rintro ⟨p, hp, hdvd⟩ h @@ -190,7 +190,7 @@ theorem infinite_of_iUnion_eq_compl {S : Set ℕ} (h0 : 0 ∉ S) by_contra hinf rw [Set.not_infinite] at hinf have hfin : S.Finite := hinf - letI := furstenbergTopology + let := furstenbergTopology have hclosed : IsClosed (⋃ p ∈ S, arithProgression 0 (p : ℤ)) := hfin.isClosed_biUnion fun p hp => isClosed_arithProgression 0 (Int.natCast_ne_zero.mpr (fun h => h0 (h ▸ hp))) From d19e5dbab26418a55064066853de131983e2fe16 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 11:16:32 +0200 Subject: [PATCH 3/4] docs: mark directions G and H landed G landed as SternDiatomic.fib_is_max_on_dyadic_row (#223) and the H bridge as CalkinWilf.pair_reverse_eq_sternBrocot (#225). Traversal orders are still not identified. Co-Authored-By: Claude Opus 5 --- docs/CONTRIBUTION-DIRECTIONS.md | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/docs/CONTRIBUTION-DIRECTIONS.md b/docs/CONTRIBUTION-DIRECTIONS.md index e565b133..981901ef 100644 --- a/docs/CONTRIBUTION-DIRECTIONS.md +++ b/docs/CONTRIBUTION-DIRECTIONS.md @@ -313,6 +313,10 @@ modest. ### G. Maximum Stern-row value is Fibonacci +**Status:** landed as `LeanFrontier.SternDiatomic.fib_is_max_on_dyadic_row` +(`LeanFrontier/NumberTheory/SternDiatomic/RowMaximum.lean`), with attainment in both Fibonacci +orientations. + **Primary parent:** `SternDiatomic`; Fibonacci support would mainly come from Mathlib. The classical extremal theorem says the maximum of Stern's sequence on an appropriate dyadic @@ -330,10 +334,13 @@ Treat it as a good independent Stern extension, not as a top corpus-synthesis ta ### H. Stern diatomic / Calkin–Wilf to Stern–Brocot representation bridge -**Status:** the infrastructure has landed: both path enumerations -(`LeanFrontier.CalkinWilf.exists_code_eq`, `LeanFrontier.SternBrocot.existsUnique_pair_of_coprime`) -and the Stern–Brocot interval invariants (`LeanFrontier/NumberTheory/SternBrocot/Intervals.lean`). -The bridge itself, relating the two path conventions, remains open. +**Status:** landed. Both path enumerations +(`LeanFrontier.CalkinWilf.exists_code_eq`, `LeanFrontier.SternBrocot.existsUnique_pair_of_coprime`), +the Stern–Brocot interval invariants (`LeanFrontier/NumberTheory/SternBrocot/Intervals.lean`), +and the bridge itself: `LeanFrontier.CalkinWilf.pair_reverse_eq_sternBrocot` and +`pair_eq_sternBrocot_iff_reverse` (`LeanFrontier/NumberTheory/CalkinWilfSternBrocot.lean`) +show that a Calkin–Wilf path and a Stern–Brocot path reach the same pair exactly when they are +reverses. Traversal orders are not identified; that remains open. **Critical correction:** From 999ef846fa473e1587859983bcaa2aa583258883 Mon Sep 17 00:00:00 2001 From: Carlo Perassi Date: Tue, 22 Sep 2026 11:20:52 +0200 Subject: [PATCH 4/4] chore: replace if_true/if_false in SternBrocot.NodeInterval Added by #227 after the rest of this PR was written; same v4.34.0 deprecation class (now ite_true/ite_false). Re-verified on current main: 486 declarations with identical canonical types, kinds and axioms before and after the whole PR, 0 deprecation warnings, leanchecker passes on every edited module. Co-Authored-By: Claude Opus 5 --- LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean b/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean index aed0a999..5137bcaf 100644 --- a/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean +++ b/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean @@ -53,12 +53,12 @@ theorem mediant_bounds_eq_pair (path : List Bool) : | cons dir path ih => rw [bounds_cons] cases dir - · simp only [mapBounds, mapPair, Bool.false_eq_true, if_false, Prod.fst, Prod.snd, pair] + · simp only [mapBounds, mapPair, Bool.false_eq_true, ite_false, Prod.fst, Prod.snd, pair] constructor · exact ih.1 · rw [Nat.cast_add] omega - · simp only [mapBounds, mapPair, if_true, Prod.fst, Prod.snd, pair] + · simp only [mapBounds, mapPair, ite_true, Prod.fst, Prod.snd, pair] constructor · rw [Nat.cast_add] omega