ProofAtlas

Lean-checked statement

Collatz predecessor bound with target-dependent scale — exponent 901/1000

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 theorem supplies some target-dependent constant cₜ > 0. It does not give cₜ explicitly or claim the unit coefficient 1 at exponent 901/1000. It also 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
Positive-constant formFor some target-dependent c > 0 and every sufficiently large real cutoff xA threshold exists; no numerical cutoff is given.
Lean proves the lower boundct · x901/1000 ≤ Pt(x)for the recorded predecessor-count function
Pₜ(x) counts positive starting integers at most floor(x) 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_0901
    {target : Nat}
    (htarget : 0 < target)
    (hmod : target % 3 ≠ 0) :
    ∃ constant : Real, 0 < constant ∧ ∀ᶠ x in Filter.atTop, constant * x ^ ((901 : Real) / 1000) ≤ (predecessorCountReal target x : Real)

Result boundary

What this theorem does not claim

This theorem supplies some target-dependent constant cₜ > 0. It does not give cₜ explicitly or claim the unit coefficient 1 at exponent 901/1000. It also does not assert global Collatz convergence, an explicit cutoff, optimality, or final novelty clearance.

Theorem schematic

Spend the 0.001 exponent reserve

Selected predecessor strands reach one fixed target above a family of positive gold starting scales and two smooth concave growth profiles with an unspecified eventual comparison.
A target-dependent positive scale at exponent 0.901 is enough: its small exponent reserve eventually dominates the unit-coefficient exponent 0.90 bound.

If cₜ > 0 and eventually cₜ x^(901/1000) ≤ Pₜ(x), then eventually x^(9/10) ≤ Pₜ(x)

The separate scale tokens represent that the positive constant may depend on the fixed target and is not claimed to equal one. The two concave growth fans differ only slightly in exponent; the steeper 0.901 fan eventually overtakes the unit-scale 0.90 requirement for every positive constant. The picture does not encode the constant's value or an effective crossing point.

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. Accepted publication-review records separately cover statement alignment, scope, and the displayed wording. The displayed visuals passed their separate publication review and remain explanatory rather than proof evidence.

Artifact title
Collatz Predecessor Positive-Constant x^0.901 Lower Bound
Accepted-result title
Accepted Result: Collatz Predecessor Positive-Constant x^0.901 Lower Bound
Accepted-result status
Accepted formal theorem
Accepted-result boundary
For each fixed positive target not divisible by 3, the retained Lean declarations give eventual unit-coefficient exponent 9/10 lower bounds for real and natural cutoffs and a target-dependent positive-constant exponent 901/1000 real-cutoff bound. No explicit eventual cutoff is asserted. Non-claim: This target record is not proof evidence by itself. Non-claim: The formal results do not establish that every Collatz orbit reaches 1. Non-claim: The target-dependent positive constant is not claimed to equal 1. Non-claim: No optimality or final novelty claim is made. Non-claim: Native-assisted is not kernel-clean. Non-claim: This accepted-result record does not by itself authorize public export or deployment.
Declaration
CollatzPredecessor090.predecessor_count_lower_bound_0901
Main Lean file
CollatzPredecessor090.lean
Source commit
5f76a170e74ea5b0c37c56683bd4c1e9d72e5e3f
Lean proof
Build passed
Recorded build time
8.4 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 review question, exact subject coverage, and reviewer provenance recorded for this release. A selected review concerns only its named question and is not by itself proof or acceptance of a broader claim. These bindings alone do not establish that proof or computation checks were rerun.

Download exact review bindings

Selected review

Formal-evidence review

Coverage
1 exact subject binding
Reviewer
Claude Fable 5
Independence
Independence not asserted
Selected review

Public-wording review

Coverage
1 exact subject binding
Reviewer
Claude Fable 5
Independence
Independence not asserted
Selected review

Result-boundary review

Coverage
3 exact subject bindings
Reviewer
Claude Fable 5
Independence
Independence not asserted
Selected review

Statement-alignment review

Coverage
1 exact subject binding
Reviewer
Claude Fable 5
Independence
Independence not asserted

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