ProofAtlas

Number theory · dynamical systems · formal theorem

Density-one convergence implies convergence of every positive integer

If convergence to 1 has upper natural density one, every positive integer reaches 1. The density-one premise is an assumption, not a result proved here.

Scope: Assume that for every real ε > 0 and every natural N there is a natural X ≥ N with X > 0 and at least (1 − ε)X distinct positive starts below X reaching 1. Then every natural n > 0 reaches 1 under ordinary Collatz iteration. No unconditional density-one premise or full Collatz proof is claimed.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Conditional density-one convergence statement mapSchematic statement map, not numerical data. Assume that for every real ε > 0 and every natural N there is a natural X ≥ N with X > 0 and at least (1 − ε)X distinct positive starts below X reaching 1. Then every natural n > 0 reaches 1 under ordinary Collatz iteration. No unconditional density-one premise or full Collatz proof is claimed.
Exact scope: Assume that for every real ε > 0 and every natural N there is a natural X ≥ N with X > 0 and at least (1 − ε)X distinct positive starts below X reaching 1. Then every natural n > 0 reaches 1 under ordinary Collatz iteration. No unconditional density-one premise or full Collatz proof is claimed.

Exact formal proposition

Hypotheses and conclusion

This is the exact recorded theorem statement, followed by the source definitions that give its named predicates and quantities their full meaning.

Assume that for every real ε > 0 and every natural N, there exists a natural X with N ≤ X and X > 0 such that (1 − ε)X ≤ #{n ∈ ℕ : 0 < n < X and T^[k](n) = 1 for some k ∈ ℕ}. Then every natural n > 0 has some k ∈ ℕ with T^[k](n) = 1. Here T sends even n to n/2 and odd n to 3n+1, and each positive starting integer below X is counted once. This upper-natural-density-one premise is an assumption, not a theorem of this release; natural-density-one convergence would be a sufficient special case.

theorem universal_reaches_one_of_arbitrarily_dense_convergence
    (hstat : ArbitrarilyDenseConvergence) :
    ∀ n : ℕ, 0 < n → Reaches n 1
Definitions used in this proposition

CollatzPredecessorDensity.ArbitrarilyDenseConvergence

abbrev ArbitrarilyDenseConvergence : Prop :=
  Erdos1135.ND.PositiveDensity.ArbitrarilyDenseOrdinaryConvergence

Erdos1135.ND.PositiveDensity.ArbitrarilyDenseOrdinaryConvergence

def ArbitrarilyDenseOrdinaryConvergence : Prop :=
  ∀ epsilon : ℝ, 0 < epsilon → ∀ N : ℕ, ∃ X : ℕ,
    N ≤ X ∧ 0 < X ∧
      (1 - epsilon) * (X : ℝ) ≤ (Terras.natCount (ordinaryPredecessorSet 1) X : ℝ)

Erdos1135.ND.PositiveDensity.ordinaryPredecessorSet

def ordinaryPredecessorSet (a : ℕ) : Set ℕ :=
  {n | 0 < n ∧ Erdos1135.Reaches n a}

CollatzPredecessorDensity.countBelow

abbrev countBelow (s : Set ℕ) (X : ℕ) : ℕ :=
  Erdos1135.Terras.natCount s X

Erdos1135.Terras.natCount

noncomputable def natCount (s : Set ℕ) (N : ℕ) : ℕ :=
  @Nat.count (fun n => n ∈ s) (fun n => Classical.propDecidable (n ∈ s)) N

CollatzPredecessorDensity.Reaches

abbrev Reaches (n a : ℕ) : Prop := Erdos1135.Reaches n a

Erdos1135.Reaches

def Reaches (a b : ℕ) : Prop :=
  ∃ m, collatzStep^[m] a = b

Erdos1135.collatzStep

abbrev collatzStep : ℕ → ℕ :=
  CollatzConjecture.collatzStep

CollatzConjecture.collatzStep

def collatzStep (n : Nat) : Nat :=
  if Even n then n / 2 else 3 * n + 1
Download companion source supplement (ZIP)Download pinned supporting source (ZIP)Verification and Reproduction

Result boundary

What this theorem does—and does not—establish

Assume that for every real ε > 0 and every natural N there is a natural X ≥ N with X > 0 and at least (1 − ε)X distinct positive starts below X reaching 1. Then every natural n > 0 reaches 1 under ordinary Collatz iteration. No unconditional density-one premise or full Collatz proof is claimed.

Line counts exclude blank lines; comments and documentation count. Counts cover the complete checked assembled closure, not the smaller downloadable extension. Mathlib and other third-party dependencies are excluded. Source size is not a proof-quality measure.

Source and reproduction

Source supplement and pinned supporting library

The companion source ZIP contains the narrowed extension, not the complete assembled library. Reproduction also requires the unchanged, hash-pinned supporting source release v2.1. The complete assembled import closure was checked privately; it is not republished here as raw Lean files or a second ZIP.

Companion source ZIP
55,103 bytes · sha256:55ceb4df0cca17ae728dc65b30bf5077000e1b47f2dc322454eea9f637ac75b3
Supporting source revision
830b9d3f38f2a8da8cd921bf6a9310dd69336fd0
Supporting source ZIP SHA-256
sha256:23f5cac4d66e696401144658752cf180a13ce70373a122f00693e1e1fe969c1f
Download companion source supplement (ZIP)Download pinned supporting source (ZIP)Verification and ReproductionDownload checker evidence (JSON)
Technical evidence, source identity, and assumptions
Main Lean declaration
universal_reaches_one_of_arbitrarily_dense_convergence
Source commit
c290ac229b37

Mechanical evidence

Lean verification

These fields support the exact Lean declaration, not a broader informal claim.

Artifact ID
artifact.collatz.universal_reaches_one_of_arbitrarily_dense_convergence.v001
Accepted-result title
Accepted Result: Density-one convergence implies convergence of every positive integer
Accepted-result status
Accepted conditional theorem
Accepted-result boundary
For the ordinary Collatz map, odd n maps to 3n+1 and even n to n/2; reachability allows zero or more iterations. Counts are of distinct positive integers strictly below a natural cutoff X. (1) For each fixed a > 0 with 3 ∤ a, there exist c(a) > 0 and X₀(a) such that every X ≥ X₀(a) has at least c(a)X starts reaching a. No assumption that a reaches 1, or that a is nonperiodic, is required. (2) If some positive integer never reaches 1, the positive integers never reaching 1 have positive lower natural density. (3) If, for every ε > 0 and every N ∈ ℕ, some positive X ≥ N has at least (1−ε)X positive starts below X reaching 1, then every positive integer reaches 1. This upper-natural-density-one hypothesis is not proved; a natural-density-one limit is a sufficient special case. Non-claims: no density limit, target-independent positive constant, effective target-to-constants recipe, general-target time bound, unconditional density-one convergence, full Collatz proof, or exhaustive historical-priority claim. The preceding paper's target-one logarithmic-time result remains separate; only these three companion roots are advertised.
Declarations covered by recorded evidence
CollatzPredecessorDensity.predecessors_positive_lower_density
CollatzPredecessorDensity.nonconvergence_positive_lower_density_of_counterexample
CollatzPredecessorDensity.universal_reaches_one_of_arbitrarily_dense_convergence
Lean build
passed
Recorded build time
1364.7 s one machine-dependent evidence run, not a benchmark
Evidence collected
· clean-source provenance recorded
Unfinished proof check
passed
Lean toolchain
leanprover/lean4:v4.30.0-rc2
Recorded source commit
c290ac229b379d2b51026d3e86140496870d6f39
Source SHA-256
sha256:eb5aef151a767622d1a28ee0dce1473e8b85aafa30f434809462193fa1d383f9
Statement alignment
accepted

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

  • Classical.choice
  • Quot.sound
  • propext

Publication review

Review record

Publication review is accepted for this exact theorem. See review details on the formalization overview.

Credit for this release

Contributors and roles

Authorship and other contributions are recorded separately for this version.

Authorship

Paper author
Lech Mazur

Contributions

  • Direct contributionOpenAI Codex

    The ProofAtlas.ai harness and OpenAI GPT models accessed through Codex contributed substantially to the mathematics, formalization, checking, and exposition. No exact model version is inferred.

    • Computation
    • Exposition
    • Formalization
    • Proof strategy
  • Upstream attributionAnthropic Claude

    Anthropic Claude reviewed the preceding paper only. This upstream disclosure does not claim a Claude review of this companion, human peer review, or a current ProofAtlas independent-review gate.

    • Exposition
  • Direct contributionLech Mazur

    Lech Mazur is the named sole human paper author and is responsible for this companion manuscript and its claims.

    • Exposition
    • Research direction

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
Paper release
Version
manuscript v1.0 of September 6, 2026
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

  • Anthropic Claude reviewed the preceding paper only; no Claude review of this companion, human peer review, or current independent-review gate is claimed.
  • Exact AI model versions are unspecified in the supplied disclosure and are not inferred.
  • Formal checking concerns exactly the three advertised Lean declarations. Cache reuse and the historical source-to-object provenance limitations are stated in the immutable Verification and Reproduction supplement; no independent LeanChecker or all-library cold rebuild is claimed.
  • The density-one premise is unproved. There is no density-limit, uniform target-independent constant, general-target time-bound, full Collatz, or historical-priority claim.
  • The manuscript retains upstream citations to Krasikov–Lagarias, the two preceding Mazur releases, mathlib, Tao, and Wirsching. This snapshot does not adjudicate literature priority or convert supporting sources into companion authors.
  • The paper and infographic have exact hosting permission, not a general open-content license. Apache-2.0 applies only to the new code and verification tools; dependencies retain their licenses and notices.
  • This new companion snapshot does not replace the preceding paper, alter its theorem scope, restore the withdrawn source archive, or grant mathematical acceptance, visibility, publication, or deployment authority.