feat(Data/Nat/Fib): formalize Lamé's theorem#37584
feat(Data/Nat/Fib): formalize Lamé's theorem#37584kennethgoodman wants to merge 10 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
github-actions
bot
added
the
merge-conflict
Lamé's theorem (1844) bounds the number of division steps in the Euclidean algorithm using the Fibonacci sequence: if the algorithm takes n+1 steps on (a, b) with b ≤ a, then b ≥ fib(n+1) and a ≥ fib(n+2). This is the founding result of computational complexity theory. - `Nat.euclidSteps`: counts division steps in the Euclidean algorithm on natural numbers. - `Nat.fib_le_of_euclidSteps`: Fibonacci lower bound on inputs given a step count. - `Nat.euclidSteps_le_of_lt_fib`: step count upper bound given a Fibonacci bound on the smaller input. Co-Authored-By: Claude Opus 4.6 <[email protected]>
kennethgoodman
force-pushed
the
lame-theorem
branch
from
9edc907 to
3778538
Compare
github-actions
bot
removed
the
merge-conflict
PR summary 290b6cf8beImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
- euclidSteps_of_lt: when a < b, one step swaps to (b, a) - euclidSteps_fib: consecutive Fibonacci numbers achieve the Lamé bound exactly (tightness) - fib_mod_fib_succ: helper for tightness proof Co-Authored-By: Claude Opus 4.6 <[email protected]>
vihdzp
left a comment
vihdzp
left a comment
There was a problem hiding this comment.
Could you reference this in 1000.yaml?
- Remove import Mathlib.Tactic.PushNeg (deleted on master) - Replace push_neg with simp/by_contra patterns - Replace native_decide with explicit proof (banned in mathlib) - Add gcd_euclidSteps connecting euclidSteps to Nat.gcd recursion Co-Authored-By: Claude Opus 4.6 <[email protected]>
Review feedback from vihdzp: - Remove `set_option autoImplicit false` (set globally) - Use `n + 1` not `1 + n` in euclidSteps definition - Rename euclidSteps_succ → euclidSteps_of_ne_zero, take b ≠ 0 - Remove euclidSteps_pos (contrapositive of euclidSteps_zero_right) - Remove gcd_euclidSteps (redundant with the above) - Rephrase main theorem: n ≠ 0 and n ≤ steps, not n+1 ≤ steps - Use `1 < n` not `2 ≤ n` for fib_mod_fib_succ - Use `n ≠ 0` not `0 < n` for euclidSteps_fib - Remove redundant 0 < b from add_mod_le - Add entry to docs/1000.yaml Co-Authored-By: Claude Opus 4.6 <[email protected]>
Lean 4.29 module system requires: - `module` declaration after copyright header - `public import` instead of `import` - `@[expose] public section` to export declarations Verified locally: lake build + lake exe runLinter both pass. Co-Authored-By: Claude Opus 4.6 <[email protected]>
- Move fib_mod_fib_succ to Mathlib.Data.Nat.Fib.Basic where it belongs as a general Fibonacci fact - Remove redundant 0 < b hypothesis from add_mod_le (when b = 0, a % 0 = a in Lean, so b + a % b = a trivially) - Add date: 2026 to 1000.yaml entry Both files pass lake build and lake exe runLinter locally. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Mathlib/Data/Nat/Fib/Lame.lean
Outdated
| simp [hb] | ||
|
|
||
| /-- When `b ≤ a`, we have `b + a % b ≤ a`. -/ | ||
| theorem add_mod_le {a b : ℕ} (hab : b ≤ a) : |
There was a problem hiding this comment.
This should go in an earlier file (you resolved this comment earlier, but it hasn't been addressed)
There was a problem hiding this comment.
moved to Mathlib/Data/Nat/Basic.lean, let me know if you have a better place
- Move `add_mod_le` from Lame.lean to Mathlib/Data/Nat/Basic.lean - Remove redundant docstrings on `euclidSteps_of_ne_zero`, `add_mod_le`, and `fib_mod_fib_succ` - Remove Kenneth Goodman from Fib/Basic.lean authors (minor contribution) - Fix copyright year: 2025 → 2026 - Use `contradiction` instead of `exact absurd rfl hn₀` Co-Authored-By: Claude Opus 4.6 <[email protected]>
- Use `contradiction` consistently - Use `obtain` and `refine` instead of `have`/`constructor` - Inline intermediate hypotheses - Remove docstrings that restate type signatures - Simplify `euclidSteps_fib` base case Co-Authored-By: Claude Opus 4.6 <[email protected]>
2 participants
Summary
Formalize Lamé's theorem (1844), the founding result of computational complexity theory.
Lamé's Theorem: If the Euclidean algorithm on inputs
(a, b)withb ≤ atakesn + 1division steps, thenb ≥ fib(n + 1)anda ≥ fib(n + 2).New definitions
Nat.euclidSteps: counts the number of division steps in the Euclidean algorithm on natural number inputs.New theorems
Nat.fib_le_of_euclidSteps: the main Lamé bound — Fibonacci lower bound on inputs given a step count.Nat.euclidSteps_le_of_lt_fib: the contrapositive — step count upper bound given a Fibonacci bound on the smaller input.Nat.add_mod_le: helper lemma thatb + a % b ≤ awhenb ≤ aand0 < b.Proof strategy
Induction on
n, tracking both elements of the pair. The key insight is that each Euclidean step replaces(a, b)with(b, a % b), and sincea ≥ b + a % b(becausea / b ≥ 1), the Fibonacci recurrencefib(n+3) = fib(n+2) + fib(n+1)matches the structure of the algorithm.References
AI usage disclosure
Per the Mathlib AI guidelines: Claude Code (Claude Opus 4.6) was used to assist with writing the Lean 4 proof code, fixing tactic errors, and drafting this PR description. The mathematical proof (induction on step count, tracking both pair elements through the Fibonacci recurrence) was designed by hand and verified on paper before formalization. I have reviewed and understand every line of the resulting Lean code and can explain all proof steps.
lake build Mathlib.Data.Nat.Fib.Lame)sorryautoImplicit false