Number theory · dynamical systems · formal theorem
Positive lower density of exceptions, if any exist
If any positive starting integer never reaches 1, then the set of all positive starting integers that never reach 1 has positive lower natural density.
Scope: Assume there exists a natural n > 0 whose ordinary Collatz orbit never reaches 1. Then there exist c > 0 and a natural X₀ such that every natural X ≥ X₀ has at least cX distinct positive nonconvergent starts below X. The existence of a counterexample is not asserted.
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 there exists a natural n > 0 whose ordinary Collatz orbit never reaches 1: no natural k satisfies T^[k](n) = 1. Then there exist a real c > 0 and a natural X₀ such that every natural X ≥ X₀ satisfies cX ≤ #{n ∈ ℕ : 0 < n < X and no k ∈ ℕ has T^[k](n) = 1}. The count is of distinct positive starting integers below X. T sends even n to n/2 and odd n to 3n+1. The theorem does not assert that a counterexample exists.
theorem nonconvergence_positive_lower_density_of_counterexample
(hbad : ∃ n : ℕ, 0 < n ∧ ¬ Reaches n 1) :
HasPositiveLowerDensity nonconvergentStartsDefinitions used in this proposition
CollatzPredecessorDensity.HasPositiveLowerDensity
def HasPositiveLowerDensity (s : Set ℕ) : Prop :=
∃ c : ℝ, 0 < c ∧ ∃ X0 : ℕ, ∀ X : ℕ, X0 ≤ X →
c * (X : ℝ) ≤ (countBelow s X : ℝ)CollatzPredecessorDensity.nonconvergentStarts
abbrev nonconvergentStarts : Set ℕ :=
Erdos1135.ND.PositiveDensity.positiveNonconvergentSetErdos1135.ND.PositiveDensity.positiveNonconvergentSet
def positiveNonconvergentSet : Set ℕ :=
{n : ℕ | 0 < n ∧ ¬ Erdos1135.Reaches n 1}CollatzPredecessorDensity.countBelow
abbrev countBelow (s : Set ℕ) (X : ℕ) : ℕ :=
Erdos1135.Terras.natCount s XErdos1135.Terras.natCount
noncomputable def natCount (s : Set ℕ) (N : ℕ) : ℕ :=
@Nat.count (fun n => n ∈ s) (fun n => Classical.propDecidable (n ∈ s)) NCollatzPredecessorDensity.Reaches
abbrev Reaches (n a : ℕ) : Prop := Erdos1135.Reaches n aErdos1135.Reaches
def Reaches (a b : ℕ) : Prop :=
∃ m, collatzStep^[m] a = bErdos1135.collatzStep
abbrev collatzStep : ℕ → ℕ :=
CollatzConjecture.collatzStepCollatzConjecture.collatzStep
def collatzStep (n : Nat) : Nat :=
if Even n then n / 2 else 3 * n + 1Result boundary
What this theorem does—and does not—establish
Assume there exists a natural n > 0 whose ordinary Collatz orbit never reaches 1. Then there exist c > 0 and a natural X₀ such that every natural X ≥ X₀ has at least cX distinct positive nonconvergent starts below X. The existence of a counterexample is not asserted.
- The full Collatz conjecture remains open. The statistical criterion does not prove its upper-density-one premise or unconditional almost-all convergence to 1.
- No asymptotic density limit, target-independent positive density constant, effective recipe for the constants, or general-target time bound is claimed.
- The target is fixed and positive, with 3 ∤ a. Counts concern distinct positive starts strictly below a natural cutoff; reaching a target permits zero or more ordinary, unaccelerated Collatz steps.
- Exactly three public Lean roots are advertised. Supporting lemmas, the manuscript’s elementary converse, and later research are not additional formal publication claims.
- The note does not replace the preceding positive-density logarithmic-time paper or make an exhaustive literature or historical-priority claim.
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
Technical evidence, source identity, and assumptions
- Main Lean declaration
nonconvergence_positive_lower_density_of_counterexample- Source commit
c290ac229b37
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.collatz.nonconvergence_positive_lower_density.v001- Accepted-result title
- Accepted Result: Positive lower density of counterexamples, if any exist
- 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_densityCollatzPredecessorDensity.nonconvergence_positive_lower_density_of_counterexampleCollatzPredecessorDensity.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.choiceQuot.soundpropext
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.
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.