Number theory · dynamical systems · formal 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.
Scope: 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.
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.
Fix a natural target a > 0 with 3 ∤ a. There exist a real c > 0 and a natural X₀, which may depend on a, such that every natural X ≥ X₀ satisfies cX ≤ #{n ∈ ℕ : 0 < n < X and T^[k](n) = a for some k ∈ ℕ}. Here T sends even n to n/2 and odd n to 3n+1; zero or more ordinary steps are allowed. Each starting integer is counted once, not once per path. No assumption that a reaches 1 is needed.
theorem predecessors_positive_lower_density
{a : ℕ} (ha : 0 < a) (hthree : ¬ 3 ∣ a) :
HasPositiveLowerDensity (predecessors a)Definitions used in this proposition
CollatzPredecessorDensity.HasPositiveLowerDensity
def HasPositiveLowerDensity (s : Set ℕ) : Prop :=
∃ c : ℝ, 0 < c ∧ ∃ X0 : ℕ, ∀ X : ℕ, X0 ≤ X →
c * (X : ℝ) ≤ (countBelow s X : ℝ)CollatzPredecessorDensity.predecessors
abbrev predecessors (a : ℕ) : Set ℕ :=
Erdos1135.ND.PositiveDensity.ordinaryPredecessorSet aErdos1135.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 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
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.
- 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.
Companion research paper
Positive Lower Density of Collatz Predecessors
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.
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.
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
predecessors_positive_lower_density- Source commit
c290ac229b37
Mechanical evidence
Lean verification
These fields support the exact Lean declaration, not a broader informal claim.
- Artifact ID
artifact.collatz.predecessors_positive_lower_density.v001- Accepted-result title
- Accepted Result: Positive lower density of predecessors of a fixed target
- Accepted-result status
- Accepted formal 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.