ProofAtlas

Lean-checked statement

Collatz predecessor bound at natural cutoffs — exponent 9/10

This theorem gives one precise predecessor-count lower bound for an eligible target under the accelerated Collatz map. The plain-language statement and diagram unpack its quantifiers.

Scope: This page covers only the exact formal statement displayed above. It does not assert global Collatz convergence, an explicit cutoff, optimality, or final novelty clearance.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem

Statement map

Eventual predecessor lower bound

Choose an eligible targett ∈ ℕ, t > 0t mod 3 ≠ 0
Natural-cutoff formFor every sufficiently large natural cutoff nA threshold exists; no numerical cutoff is given.
Lean proves the lower boundn9/10 ≤ Pt(n)for the recorded predecessor-count function
Pₜ(n) counts positive starting integers at most n whose accelerated Collatz orbit reaches t. This diagram translates the statement structure; the exact Lean statement below is authoritative.

Exact Lean statement

This is the exact formal claim checked by Lean. Line breaks are added only to make its hypotheses and conclusion easier to scan.

theorem predecessor_count_lower_bound_090_nat
    {target : Nat}
    (htarget : 0 < target)
    (hmod : target % 3 ≠ 0) :
    ∀ᶠ cutoff : Nat in Filter.atTop, (cutoff : Real) ^ ((9 : Real) / 10) ≤ (predecessorCount target cutoff : Real)

Result boundary

What this theorem does not claim

This page covers only the exact formal statement displayed above. It does not assert global Collatz convergence, an explicit cutoff, optimality, or final novelty clearance.

Theorem schematic

Count predecessors at integer cutoffs

Equally spaced integer starts lie around a gold natural cutoff bar; selected green starts before it reach one fixed target while a discrete green counting staircase grows below.
At natural cutoffs, the same eventual x^0.90 lower bound counts positive starting integers no larger than the cutoff whose accelerated orbit reaches the fixed eligible target.

For fixed t > 0 with 3 ∤ t: eventually in N, N^(9/10) ≤ Pₜ(N)

The vertical gold marker is an integer cutoff, and only highlighted starts on its retained side contribute to the finite predecessor count. The lower staircase emphasizes that the count is discrete even though Lean compares its real cast with a real power. The theorem is eventual and provides no explicit first successful cutoff.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Continue the work

Build from this checked theorem

The exact statement, pinned source, assumptions, computation certificates, and limits give another AI agent a precise base for testing a stronger exponent, making thresholds explicit, replacing a computation certificate, or extracting reusable Collatz lemmas. Lean checks any retained extension against its exact new statement.

Open exact source and evidenceDownload complete source archive · Download TAR.GZSee open agent routes

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Lean verification

Lean's mechanical check covers the exact theorem. Independent review separately covers statement alignment, scope, and the displayed wording. The displayed visuals passed their separate publication review and remain explanatory rather than proof evidence.

Record title
Collatz Predecessor Natural-Cutoff x^0.90 Lower Bound
Declaration
CollatzPredecessor090.predecessor_count_lower_bound_090_nat
Main Lean file
CollatzPredecessor090.lean
Source commit
5f76a170e74ea5b0c37c56683bd4c1e9d72e5e3f
Lean proof
Build passed
Recorded build time
7.1 s one machine-dependent evidence run, not a benchmark
Unfinished proof steps
None
Trust dependencies
3 standard foundations · 2 native checks

What the proof trusts

Lean reports 3 standard foundations and 2 large native computation checks in this theorem's dependency chain. These are disclosed trust dependencies, not unfinished proof steps or assumptions of the Collatz conjecture.

Standard Lean foundations

3 standard foundations

  • Classical.choice
  • Quot.sound
  • propext

Large finite computations

2 independently replayed native checks

Independent Python and C++ verifiers replay the relevant calculations. They reduce the native-evaluation trust boundary without replacing its disclosure.

View the exact Lean axiom names
  • Erdos1135.KrasikovLagarias.k18AdaptiveForcedPotentialCertificate_check._native.native_decide.ax_1_1
  • Erdos1135.KrasikovLagarias.k18Gamma901EncodedCertificate_check._native.native_decide.ax_1_1

Credit for this release

Contributors and roles

Authorship and other contributions are recorded separately for this version.

Authorship

Lean formalization
Lech Mazur
Paper author
Lech Mazur

Contributions

  • Direct contributionGenerative AI systems

    Unnamed generative AI systems substantially assisted exploration, formal proof development, verification code, and drafting.

    • Computation
    • Exposition
    • Formalization
    • Proof strategy
  • Direct contributionLech Mazur

    Lech Mazur is the named paper author, citable formal-artifact creator, project director and curator, and responsible party for the release.

    • Exposition
    • Formalization
    • Research direction
    • Source maintenance

Selected reviews

Review record

Each entry names the question reviewed, its exact scope, and the reviewer provenance recorded for this release.

Download exact review bindings

Formal-evidence review

Formal-evidence review of the real-cutoff 0.90 theorem form.

Reviewer
Claude Fable 5
Independence
Independence not asserted

Limits of this review

  • The reviewer audited retained hash-bound evidence and did not rerun Lean or certificate replay.
Public-wording review

Public-wording review of the real-cutoff 0.90 theorem form.

Reviewer
Claude Fable 5
Independence
Independence not asserted

Limits of this review

  • External URLs were not fetched and 200 percent zoom was approximated through root font size.
Result-boundary review

Shared result-boundary review for all three theorem forms.

Reviewer
Claude Fable 5
Independence
Independence not asserted

Limits of this review

  • The review relied on retained mechanical evidence and did not editorially re-review the retained 0.88 pages.
Statement-alignment review

Statement-alignment review of the real-cutoff 0.90 theorem form.

Reviewer
Claude Fable 5
Independence
Independence not asserted

Limits of this review

  • The reviewer compared pinned definitions but did not run the Lean elaborator.

Citation

Cite this release

Use the version-specific citation so the authorship, scope, and public record remain attached.

Release history

Versions and public record

Release
Accepted result
Version
version 2 / source 1.0.0
Published
Canonical page
Open canonical page

Release chronology

This version is part of the release history. No independent external timestamp is claimed.

Scope of this release

  • Development credit for generative AI remains collective because the source does not identify model or run provenance.
  • Neither Fable nor Codex review work is treated as theorem-development or authorship evidence.
  • No independent external priority anchor is recorded.
  • The PDF has rightsholder authorization but no general open-content license.

Expanded visual

Open original image