Sequence growth
Natural-division recurrence bounds and eventual exponential domination for sequences of natural numbers.
Quoted from the project description in formalization.yaml of FormalFrontier/sequence-growth at commit ccf81c71, Apache-2.0.
2 articles: 2 for headline results in its README whose declaration link names a declaration the scan finds in the linked file.
Facts
From the repository and its formalization.yaml; the review and automation statements are quoted as written.
- Repository: FormalFrontier/sequence-growth, read at commit ccf81c71 (2026-11-04).
- Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
- License: Apache-2.0.
- Authors: Formal Frontier Agents.
- Review status: “agent-reviewed”.
- Review notes: “The two listed recurrence theorems and their documented hypotheses have been independently agent-reviewed; no complete coverage of an external source is asserted.”
- Reviewers: “Formal Frontier Agents”.
- Automation: agent; framework “Codex CLI and Lean”; tool setup “Agent-assisted Lean formalization using Mathlib.”
- Automation notes: “Formal Frontier Agents developed the Lean proofs with AI assistance and reused Mathlib's arithmetic foundations.”
Literature
The sources its formalization.yaml names, with their relationship to it.
- Natural-division lower-recurrence growth bounds (original formalization), Formal Frontier Agents (original-proof; independently-proves).
Builds on
No other Formal Frontier library.
Used by
Headline results
Quoted from the headline results in README.md of FormalFrontier/sequence-growth at commit ccf81c71, Apache-2.0.
TheoremNat.DivisionGrowth.affine_lower_bound#
Nat.DivisionGrowth.affine_lower_bound: if 0 < s < n and
∀ m, n * (u m / s) ≤ u (m + 1), then for every m : ℕ, with
λ = (n : ℚ) / s and C = (n : ℚ) * ((s - 1 : ℕ) : ℚ) / ((n : ℚ) - s),
λ ^ m * ((u 0 : ℚ) - C) + C ≤ (u m : ℚ). There is no seed condition.
Quoted from the headline results in README.md of FormalFrontier/sequence-growth at commit ccf81c71, Apache-2.0.
Lean
Nat.DivisionGrowth.affine_lower_bound(theorem), declared in SequenceGrowth/Data/Nat/DivisionGrowth.lean, line 71.
Read from the source at commit ccf81c71, without running Lean.
Sources
TheoremNat.DivisionGrowth.eventually_dominates#
Nat.DivisionGrowth.eventually_dominates: under the same recurrence,
0 < s, 0 < b, s * b < n, and the sufficient natural seed
n * (s - 1) < (n - s) * u 0, for each K : ℕ there is M : ℕ
such that every m ≥ M satisfies K * b ^ m < u m.
Quoted from the headline results in README.md of FormalFrontier/sequence-growth at commit ccf81c71, Apache-2.0.
Lean
Nat.DivisionGrowth.eventually_dominates(theorem), declared in SequenceGrowth/Data/Nat/DivisionGrowth.lean, line 99.
Read from the source at commit ccf81c71, without running Lean.
Sources
The seed is sufficient, not necessary. See the mathematical guide for the precise Lean signatures, the rational shift, examples and boundary cases.
Main results
Its formalization.yaml lists 2 main results, and the scan finds 2 of them declared in the file the yaml gives; they are on their own page, not made articles.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.