feat(NumberTheory/AdditionChain): addition chains and the doubling bound - #42510
Open
williamjblair wants to merge 1 commit into
Open
feat(NumberTheory/AdditionChain): addition chains and the doubling bound#42510williamjblair wants to merge 1 commit into
williamjblair wants to merge 1 commit into
Conversation
An addition chain for `n` is a strictly increasing list starting at `1` in which every later entry is a sum of two earlier ones. This adds the predicate, the minimal length `Nat.additionChainLength`, and the two bounds that make it usable: an explicit chain bounds it above, and the fact that a step at most doubles bounds it below. Also proves every positive `n` has a chain, so the length is a genuine minimum rather than `sInf ∅`.
grunweg
added
the
t-number-theory
mo271
pushed a commit
to google-deepmind/formal-conjectures
that referenced
this pull request
Aug 7, 2026
`List.le_getLast_of_pairwise_lt`, added in #4752, already exists in Mathlib as `List.Pairwise.rel_getLast`. It needs `(· ≤ ·)` rather than `(· < ·)`, since it asks for a reflexive relation, so the two call sites become ```lean have hsub := (List.pairwise_append.mp hsorted).1.imp le_of_lt have hla := hsub.rel_getLast hays ``` I noticed this while preparing the same file for Mathlib in leanprover-community/mathlib4#42510. `lake --wfail build` is clean over the library.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
An addition chain for
nis a strictly increasing list1 = a₀ < a₁ < ⋯ < a_r = nin which every entry after the first is a sum of two earlier entries.Nat.additionChainLength nis the leastrover all such chains, the classicalℓ(n).additionChainLengthis ansInfoverList ℕ, so an explicit chain bounds it above (Nat.additionChainLength_le), but nothing bounds it below until the search is confined.List.IsAdditionChain.getLast_le_two_powconfines it: a step at most doubles, sorsteps cannot reach past2 ^ r. That givesNat.lt_additionChainLength_of_two_pow_lt, and the two bounds together pin down individual values.Nat.exists_isAdditionChainshows every positivenends some chain, so the length is a minimum of a nonempty set rather thansInf ∅.Mathlib has nothing on addition chains at present. This came out of formal-conjectures, where it underlies the Scholz conjecture.
I could not run
scripts/lint-bib.shlocally (nobibtool), so the newknuth1997entry is formatted by hand to match its neighbours.