ProofAtlas

Number theory · dynamical systems · formalization overview

Positive Lower Density of Collatz Predecessors

Every fixed positive target not divisible by 3 has ordinary Collatz predecessors of positive lower natural density. A counterexample would force positive lower density of nonconvergence; upper-density-one convergence would imply universal convergence, but that premise is not proved.

Scope: For each fixed a > 0 with 3 ∤ a, there exist c(a) > 0 and X₀(a) such that at least c(a)X distinct positive integers n < X reach a for every natural X ≥ X₀(a), using ordinary Collatz steps. No assumption that a reaches 1 is needed. A positive counterexample implies positive lower natural density of nonconvergence. Upper-natural-density-one convergence implies universal convergence conditionally; the density-one premise is not proved.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formalization
Fixed-target predecessor-density statement mapSchematic statement map: each fixed positive target not divisible by 3 has a set of ordinary Collatz predecessors of positive lower natural density; the constant and cutoff may depend on the target.
Exact scope: For each fixed a > 0 with 3 ∤ a, there exist c(a) > 0 and X₀(a) such that at least c(a)X distinct positive integers n < X reach a for every natural X ≥ X₀(a), using ordinary Collatz steps. No assumption that a reaches 1 is needed. A positive counterexample implies positive lower natural density of nonconvergence. Upper-natural-density-one convergence implies universal convergence conditionally; the density-one premise is not proved.

Main theorem

Positive lower density of predecessors of a fixed target

For every fixed positive target a not divisible by 3, the positive integers whose ordinary Collatz orbits reach a have positive lower natural density. No assumption that a reaches 1 is needed.

For each a > 0 with 3 ∤ a, there exist c(a) > 0 and a natural X₀(a) such that every natural X ≥ X₀(a) has at least c(a)X distinct positive starts n < X reaching a. Zero or more ordinary steps are allowed; no density limit, uniform target-independent constant, or general-target time bound is asserted.

Read exact theorem and checked proof

Supporting 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.

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.

Read exact theorem and checked proof

Supporting 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.

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.

Read exact theorem and checked proof
Original ProofAtlas metadata cover for Positive Lower Density of Collatz Predecessors by Lech Mazur, manuscript v1.0, September 6, 2026, eight pages.

Companion research paper

Positive Lower Density of Collatz Predecessors

Lech Mazur · 2026-09-06 · 8 pages

For every fixed positive target not divisible by 3, the positive integers whose ordinary Collatz orbits reach that target have positive lower natural density. The companion also shows that a counterexample would force positive lower density of nonconvergence, and that upper-natural-density-one convergence would imply universal convergence. The density-one premise is not proved.

Read the paper (PDF) Download PDFDownload the verified narrowed source supplement v1.1 (ZIP; requires the pinned public slim v2.1 baseline)
Paper, rights, and source relationship

Hosting authorized by the rightsholder. Original ProofAtlas metadata cover; not a reproduced paper page or proof evidence.

Lech Mazur, “Positive Lower Density of Collatz Predecessors,” manuscript v1.0, September 6, 2026.

  • The three public Lean roots are CollatzPredecessorDensity.predecessors_positive_lower_density, CollatzPredecessorDensity.nonconvergence_positive_lower_density_of_counterexample, and CollatzPredecessorDensity.universal_reaches_one_of_arbitrarily_dense_convergence. Supporting declarations are not additional advertised results.
  • For each fixed positive a with 3 ∤ a, the lower-density constant and cutoff may depend on a. No assumption that a reaches 1 is needed. Counts concern distinct positive integers strictly below a natural cutoff, under ordinary unaccelerated Collatz iteration.
  • The density-one criterion is conditional: upper-natural-density-one convergence would imply universal convergence, but the density-one premise is not proved. No density limit, target-independent constant, effective constants recipe, general-target time bound, full Collatz proof, or historical-priority claim is made.
  • The supplied check freshly compiled eleven extension/support/interface modules and audited all three roots, reporting only propext, Classical.choice, and Quot.sound. Compiled supporting dependencies were reused; it was not a cold rebuild of all dependencies or an independent LeanChecker run. The exact Verification and Reproduction supplement preserves cache provenance and historical source-to-object limitations.
  • ProofAtlas subsequently rebuilt the complete 388-file local import closure with the owning Lake target and audited all three public roots. The source checkout stayed clean at c290ac229b379d2b51026d3e86140496870d6f39; no sorryAx or unexpected axiom was reported. Pinned third-party compiled dependencies, including Mathlib, were reused. This additional collection is not an independent LeanChecker run and does not rewrite the earlier supplement’s verification history.
  • The 55 KB source revision 1.1 ZIP is a thin supplement, not a standalone library. It assembles with the unchanged public slim v2.1 baseline at source revision 830b9d3f38f2a8da8cd921bf6a9310dd69336fd0 and archive SHA-256 23f5cac4d66e696401144658752cf180a13ce70373a122f00693e1e1fe969c1f. The withdrawn oversized archive is not required or restored.
  • Manuscript v1.0 remains a separately citable companion. Its earlier-paper citation is retained as supplied; the current source dependency is the compatible slim v2.1 release. The preceding paper and its mathematical scope are unchanged.

Paper overview

Positive Lower Density of Collatz Predecessors

Author-supplied schematic, not numerical data or proof evidence. The target is fixed and not divisible by 3; density constants may depend on it. The density-one implication is conditional.

Author-supplied schematic explains positive lower natural density of predecessors for each fixed positive target a with 3 not dividing a; counterexample amplification; and the conditional implication from upper-density-one convergence to universal convergence. The density-one premise is not proved.

Preceding paper: Explicit Positive-Density Collatz Convergence in Logarithmic Time gives the target-one logarithmic-time result. This short companion uses the pinned slim supporting source without replacing that paper or extending its time bound to general targets.

What this formalization does not 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
Download companion source supplement (ZIP)Download pinned supporting source (ZIP)Verification and Reproduction

Verification and Reproduction

Supplement to Lech Mazur, Positive Lower Density of Collatz Predecessors, version 1.0, September 6, 2026.

Verification status: the adapted extension passed fresh compilation and its three-root statement/axiom audit on September 7, 2026. Supporting compiled dependencies were reused. Website review and publication remain separate.

Mathematical statements and formal counterparts

The ordinary Collatz map sends an even integer n to n/2 and an odd integer n to 3n+1. Reaching a target allows zero or more iterations. All counts below are of distinct positive integers strictly smaller than an integer cutoff X.

The source interface is CollatzPredecessorDensity.lean. The three theorem names below belong to the namespace CollatzPredecessorDensity.

Manuscript statement Formal theorem
For each fixed positive a not divisible by 3, there exist c > 0 and X0 such that at least cX starting integers below X reach a, for every X >= X0. predecessors_positive_lower_density
If any positive starting integer never reaches 1, the set of all such integers has positive lower natural density. nonconvergence_positive_lower_density_of_counterexample
If the proportion of positive integers reaching 1 is arbitrarily close to one at arbitrarily large cutoffs, every positive integer reaches 1. universal_reaches_one_of_arbitrarily_dense_convergence

The last hypothesis is exactly: for every real epsilon > 0 and every nonnegative integer N, there is an integer X >= N with X > 0 such that at least (1 - epsilon)X positive integers below X reach 1. This is equivalent to upper natural density one. A natural-density-one limit is a sufficient special case; no unconditional statistical hypothesis of this kind is proved here.

The first theorem assumes neither convergence nor nonperiodicity of the target. Its constants may depend on the target. It asserts no density limit, uniform positive constant across targets, effective procedure for obtaining the constants, or time bound. The second theorem includes a hypothetical cycle other than the known cycle through 1, as well as an unbounded orbit.

What has been checked, and what remains to be checked

The underlying theorem development has Lean proofs and retained axiom-audit records. Those records report only the standard Lean principles propext, Classical.choice, and Quot.sound, or subsets thereof. They report no sorryAx, unproved project axiom, or generated native-evaluation axiom for the audited theorems. The checks reused compiled dependencies; they were not a fresh rebuild of every supporting source file.

The source supplement retains the required parts of that development, with adapted proofs and the three-statement interface above. These exact adapted sources have now passed their own verification against the slim version 2.1 supporting library. All ten implementation/support modules and the public interface were freshly compiled, followed by the separate three-statement and axiom audit. The run completed successfully on September 7, 2026, at 07:16:31 UTC (3:16:31 AM EDT). Every advertised theorem reported exactly propext, Classical.choice, and Quot.sound; no admitted, custom project or generated native-evaluation axiom appeared. The source package's evidence/verification.json and release-status.json record these results.

The completed check used existing compiled supporting dependencies. It is fresh extension-source checking with reused compiled dependencies, not a fresh build of the entire library or an independent LeanChecker run. A compiled-file hash identifies the bytes used; it does not by itself prove how those bytes were originally built. The checked extension/build inputs and the baseline checkout remained unchanged during the run; later release-status and documentation edits do not change the compiled Lean sources.

The supporting source revision had already passed a later owning-target Lake build with clean source before and after. That later build replaced the cache objects listed in the archive's older direct-build inventory. The companion check explicitly records this distinction, authenticates the later build receipt, and hashes the current reused objects. The later receipt contains no per-object inventory; it does not independently establish each object's historical construction. No stronger cache-verification claim is implied.

Formal checking verifies the actual Lean declarations, not this prose or its historical comparisons. The manuscript's combined analytic input is an expository consequence of earlier estimates, not a claim that there is one separately checked declaration with exactly that presentation. The map comparison and elementary converse of the statistical criterion are also explained in the manuscript without being additional advertised formal theorems.

Source dependency and reproduction

The supplement is a small extension of an already-public library, not a self-contained copy of that library. Its source manifest records the released file identities. The assembly script retrieves only the required supporting sources from the exact earlier archive and checks their hashes. No private research checkout is needed for the assembled source project.

The pinned supporting release is the source archive accompanying Explicit Positive-Density Collatz Convergence in Logarithmic Time, version 2.1. The package records the following pins in baseline.json, lean-toolchain, and lake-manifest.json:

Other external package revisions are fixed in lake-manifest.json. A newer archive at the same address is not an interchangeable input: a hash mismatch must stop assembly. Replacing the supporting library requires a new compatibility check and a new verification record.

The public version 2.1 archive was downloaded and its complete hash verified. The companion adds only the reachability, counting and explicit-estimate support needed for its three statements. The oversized predecessor archive is not required or restored. Source-package revision 1.1 accompanies the unchanged theorem scope of manuscript version 1.0.

Follow the source package's README.md and REPRODUCIBILITY.md to assemble the project in a fresh directory and choose a supported verification procedure. The scripts distinguish a source build from a local check using an existing dependency cache, impose resource limits, and retain their commands, outputs, and completion status. An absent, interrupted, or failed record is not a passing check. Final publication materials must identify the exact checked sources and procedure without omitting cache reuse.

Authorship and rights

Lech Mazur is the author responsible for the manuscript. The ProofAtlas.ai harness and OpenAI GPT models accessed through Codex contributed substantially to the mathematics, formalization, checking, and exposition. Anthropic Claude reviewed the preceding paper; no new Claude review of this companion is claimed. Automated reviews are not human peer review.

The new formalization code and its build and verification tools are licensed under Apache-2.0. That license does not cover the manuscript or its images. The supporting library and external packages retain their own applicable licenses and notices.

Publication review

Review record

Publication reviews accepted

Lean checks the exact proof. Accepted review records cover evidence completeness, statement alignment, scope, and public wording; the visual review covers explanation only.

01

Formal evidence

The formal-evidence review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

The public-wording review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The reviewed release plan binds the exact companion source ZIP and unchanged, hash-pinned supporting source release.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

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.

Expanded visual

Open original image