Collatz

Formal exploration of the Collatz conjecture in Lean, with verified partial results, computational experiments, and literature notes. The conjecture remains unproved.

The main library uses Lean core. A separate Mathlib extension contains additional analytic results and verification instructions.

Build

Install elan, then run:

lake build Collatz

The Lean version is pinned in lean-toolchain. Run the integrity checks (requires Bash and Python 3):

bash scripts/check_integrity.sh

CI also checks generated certificates and the exact interval and coefficient-descent developments. The Mathlib extension has its own verification instructions.

Research entry points

• Anchored barriers and finite cycle extraction — exact window splitting, the greatest invariant barrier kernel, an executable interval checker, exact one- and two-step capacities, and smaller verified budgets for cycle extraction. A sharp eight-step excursion theorem forces a hypothetical orbit floor to exceed five times its starting value. Every arbitrary-start orbit exits [b,5b] within twelve steps for b>1; the clock is sharp and yields conditional high-visit witnesses.

• Sharp wider-band clock — the ratio-21/4 band has a sharp seventeen-step exit clock, with reusable finite witness transfer for lower-surviving prefixes.

• Sharp thirty-step plateau — a universal clock at ratio 11/2, an infinite family of sharp witnesses, and a whole rational-width interval with the same optimal duration.

• Fixed-width clock lower bound — an infinite class survives in width 5.995 through 9,385 ordinary steps, using a kernel-checked finite coefficient profile and a reusable rational-band transfer theorem.

• Clock obstruction below six — compact witnesses survive in horizon-dependent widths 6-2/2^K, giving a necessary inequality between width deficit and ordinary exit-clock duration.

• Smaller six-band witnesses — balanced additive-error control reduces the sufficient witness-size bound from 10*8^K to (6K+4)*2^K, with the same expanded ordinary-time duration.

• Arbitrarily long six-band prefixes — for every finite horizon, an entire sufficiently large residue class stays in [n,6n]. This rules out every uniform finite exit clock at ratio six or above, with explicit witness size and expanded ordinary-time duration bounds.

• Rational band obstruction — a denominator-aware cycle certificate, exact closure classification, and why the integer floor bound does not extend to rational floors.

• First passage through 2,592 steps — a stronger conditional descent theorem, an exact residual condition equivalent to Collatz, and 32,768 new depth-fifteen class certificates.

• Stopping atlas and first crossing through 1,538 steps — 15,360 infinite-class certificates, finite counting conservation, a tighter discrepancy bound, and explicit remaining universal-descent obligations.

• Research status — results, open questions, and limitations.

• Proof index — guide to the Lean library.

• First coefficient crossing through 1,024 steps — a conditional descent theorem for unbounded inputs, retained from the universal-descent development; it does not assert a crossing by 1,024 for every input.

• Coefficient crossing and interval shape — effective finite-exception transfer, a separately certified 256-step theorem, and the exact interval-shape consequences.

• Exact first-descent intervals — complete classifier, refinement conservation, and the remaining coverage obligation.

• Natural stopping density, Korec density bounds, and inverse interval decisions.

• Research notes and argument summaries — experiments and verification records.

• Literature — sources and references.

Conditional theorems keep their hypotheses explicit. Finite computations and almost-everywhere results do not prove convergence for every positive input.

Sharp finite-floor affine error budget

FloorAffineError.lean proves that if accelerated states before time j stay above b, then their exact affine offset B satisfies w B ≤ a (3^a n + B) and (w-a) B ≤ a 3^a n, where a is the number of odd steps and w = 3 times the least odd integer at least b, plus 1. Natural subtraction is used in the second inequality. The endpoint need not stay above b. The first odd step at that least odd integer proves w is the largest valid uniform weight; this classification is formalized in Lean.

AffineBandExit.lean eliminates a common source between two affine endpoints. A positive coefficient gap g, finite lower survival, and upper-band assumptions imply g (w-a) ≤ P H a L (L and H are the two powers of 3). A strict violation therefore rules out those joint survival assumptions. This is conditional: no universal coverage of coefficient gaps or Collatz convergence is established. Mathematical priority has not been assessed.

Validation: python3 scripts/audit_floor_affine_error.py checks 11 theorem axiom footprints, 576,960 floor budgets, 25,699 endpoint exits, 2,001 sharpness controls, 84,817 source-elimination cases, and rejects three false statements.

The coefficient-gap criterion now formally produces a band exit within twice the accelerated horizon in the ordinary orbit (standard_exit). Universal coverage remains unproved. The audit includes both exit theorems (13 total).

Multiplicative floor-error budget

FloorProductError.lean proves v^a (3^a n+B) ≤ w^a 3^a n and consequently v^a B ≤ (w^a-v^a)3^a n, with v = 3 times the least odd integer at least the finite prefix floor b, and w = v+1. This follows by multiplying the one-step odd factors. Unlike the linear paid bound, it remains informative when a reaches or exceeds w. It assumes finite lower survival and proves neither universal descent nor convergence. This elementary product method has not been assessed for priority. The independent audit checks 278,684 products, including 192,568 cases beyond the linear budget, 1,001 sharp factor controls, three Lean theorem footprints, and two false statements rejected by the kernel.

product_band_budget additionally removes the source from two endpoints: finite lower survival through a and an upper band constraint at c imply Q H 2^a v^k ≤ P 2^c L w^k, where k counts odd steps through a. No initial source upper bound is required. Four theorem footprints are audited.

Priority note: products of step-error factors bounded using a minimum are established in Simons and de Weger's cycle analysis, §3.2, Lemma 4 and Corollary 5 (author-hosted version 1.44). Our finite-prefix core-Lean formulations are not evidence that this method, or their exact corollaries, constitute new mathematics.

The product criterion now formally produces accelerated and standard band exits (product_accelerated_exit, product_standard_exit) within twice the accelerated horizon. No initial source upper-band assumption is needed. The bounded sample n=1..300, the three specified floor choices, and horizons below 30 produced 98,910 product exit certificates versus 55,137 linear certificates, with 44,824 product certificates absent from the linear set. These sets need not be nested; these are sampled certificates, not distinct orbits or a density theorem. All certified conclusions were checked directly. The kernel audit now covers six theorem footprints.

Product-spread obstruction

ProductSpreadObstruction.lean proves that if Q H D ≤ P E L, the product correction cannot yield strict spread: Q H D v^k ≤ P E L w^k. Consequently a coefficient corridor [1,R] prevents width-R product-spread certificates for all floor choices and odd counts. This is a limitation of the sufficient exit test, not a proof of actual survival or a counterexample to Collatz. Balanced parity prefixes at lengths 16,64,256,1024 are independently checked using exact integer comparisons. Three general Lean lemmas are audited.

Comparison of floor-error budgets

FloorBudgetComparison.lean proves a classical cleared-denominator Bernoulli inequality and deduces (w-k)w^k ≤ w v^k and (w-k)(w^k-v^k) ≤ k v^k for k≤w, where w=v+1 is the floor weight. Thus the multiplicative paid-offset ratio is no worse than the linear ratio where the linear denominator is positive. This compares bounds, not exit certificate sets (the sets use different additional assumptions). Audit: 20,301 exact integer comparisons including v=0, three theorem footprints, and two false controls rejected. This is classical mathematics, not frontier novelty.

Exact trace-product descent test

ExactTraceProduct.lean retains A = product of 3x and Z = product of 3x+1 at the odd states of a finite accelerated trace. It proves A 2^j T_j(n) = Z 3^a n, positivity of A for n>0, and the exact test T_j(n)<n iff Z 3^a < A 2^j. This is a trace-dependent telescoping identity, not a prediction independent of the orbit, and establishes no universal descent. The product method is classical; no novelty claim is made. Audit: 61,061 exact identities including n=0; 61,000 positive-source descent equivalences; three theorem footprints; two false controls rejected.

Descent from source floor and odd count

FloorProductDescent.lean proves that 3^a w(n)^a < 2^j v(n)^a forces some accelerated descent by j and ordinary descent by 2j. Here a is the actual prefix odd count and v(n),w(n) are the floor bases. The criterion requires no individual odd-state product, but still uses the actual prefix odd count. No universal eventual certificate is proved. Audit: 202,000 horizons, 179,921 valid certificates, two theorem footprints, and two false controls. For sources 2..2000 through horizon 200, 1995 first certificates matched actual first descent, four lagged, none was missing; the largest lag was six accelerated steps (n=27, descent 59, certificate 65). These finite measurements are not density or completeness results.

Exact first-event delay certificates

ProductDelayCertificates.lean proves first accelerated descent and first source-floor product certificate at (59,65), (56,61), (54,55), (54,56) for sources 27,31,47,63 respectively. Bounded quantification checks every earlier horizon in Lean. The general soundness theorem applies to any first certificate. Independent exact exploration of sources 2..1,000,000 through horizon 1000 found precisely those four delays and 999,995 matches. This finite observation does not establish that those are the only exceptions globally. The reusable script explore_product_descent_delay.py supports arbitrary bounds. Audit: five theorem footprints and two false first-event controls rejected.

Exact coefficient-specific floor thresholds

ProductThresholds.lean proves floor-factor and certificate monotonicity. Two adjacent boundary checks then classify all natural floors. For coefficient pair (j,a)=(65,41), the test passes exactly for b≥1192; for (59,37), exactly for b≥50. The least admissible odd states are 1193 and 51 respectively. The descent corollaries apply to any source above the stated threshold whose actual prefix has that odd count. These are sufficient conditional results; the thresholds are exact for this test, not optimal for actual descent. Audit: eight theorem footprints, 12,006 threshold checks, 1,893 matching odd-count descent cases, two false controls rejected. The method remains a specialization of known product bounds, with no established frontier novelty.

Scalar gap criterion and improved finite first-light cutoff

CoefficientGapThreshold.lean proves that a D < (D-C) w(n) suffices for descent by j when C=3^a≤D=2^j. The scalar margin implies the full product test by the classical Bernoulli comparison. A separate corollary uses the existing first-light accumulator bound to improve the coarse repository cutoff n>H3^H to 3n>H*2^H: if a first coefficient crossing occurs by H, descent occurs at that crossing. It proves no existence of a crossing and no universal convergence. No frontier novelty has been established for this elementary improvement. Audit: four theorem footprints, 53,361 scalar cases, 16,043 valid scalar certificates, 179,303 descent cases, 2,924 first-light cutoff cases, and two false controls rejected.

Survival classification at the sharper cutoff

SharpFirstLightEventual.lean propagates 3n>H2^H to exact finite-horizon no-descent/heavy-prefix equivalence, first-descent/first-light equivalence, and first-stopping-time agreement for equal residues modulo 2^H above the cutoff. It reuses existing residue and accumulator theory and improves the sufficient source interval; it proves no eventual crossing for every source. Audit: four theorem footprints, 2,050 paired residue checks through horizon 40, and two false controls rejected. Frontier novelty is not established.

Smaller finite survival-count exceptional interval

SharpSurvivalCounts.lean uses natural cutoff H*2^H/3-1 (truncated at zero), accounting for shifted sources n+2. Actual survival equals the periodic coefficient test above this cutoff. Both directions of count comparison have this additive error, and the actual count is at most this error plus (N/2^H+1)*heavyCount H. This improves the finite exceptional interval from H*3^H; it neither strengthens the asymptotic density conclusion nor proves universal crossing. Audit: four theorem footprints, 39,013 count cutoffs through H=12 and N=3000, and two false rounding controls rejected. Frontier novelty remains unestablished.

One-dimensional endpoint certificate through horizon 10000

GapEndpointCertificates.lean proves scalar gap monotonicity in the odd count and a computable upper cap for light prefixes. GapEndpointScan.lean carries powers of 3 and 2 forward, verifies a power bracket and gap at each endpoint, and proves sequential-checker soundness. GapTenThousand.lean evaluates the full scan in the Lean kernel: any n≥3,330,950 descends at a first coefficient crossing if that crossing occurs by horizon 10000. No crossing existence is asserted by this scan alone; the smaller-source obligation is closed below. No frontier novelty or universal convergence claim is made. The cutoff is minimal for this scalar scan (the audit rejects 3,330,949), not claimed optimal for actual descent. Independent integer computation locates its record at (j,a)=(9971,6291). The scan is one-dimensional rather than enumerating all odd counts at every horizon. Audit: ten theorem footprints; 10000 independently reproduced endpoints; 5272 lower-odd-count checks; two false scan certificates rejected.

Finite-prefix Beatty accumulator barriers

FiniteBeattyBarrier.lean localizes the inherited RealizableBound argument. Its time cap assumes non-descent only at the current index; its accumulator cap assumes it only through a finite horizon. Neither requires an explicit positivity premise. A first coefficient crossing inside the certified odd-count reach must descend, and a power bracket converts that reach to a time horizon. These results do not prove that every source has a crossing. They adapt existing Beatty arguments; frontier novelty is not established.

BalancedFirstLightScan.lean independently proves soundness of a balanced interval checker whose leaves reuse the existing orbit scan. Audit: four Beatty theorem footprints, 344,004 exact non-descent prefixes for reach 64 and cutoff 868, and two false cap/time controls rejected. The balanced checker has one audited theorem footprint and two false controls rejected.

Certified first-crossing descent through horizon 14186

AllSourceTenThousand.lean closes the exceptional-source obligation in the endpoint scan by reusing AssetA.drops_within_224. Its inherited range covers every source below 3,998,720. CertifiedFirstCrossing.lean then combines that range with the localized Beatty barrier and the banked 8951-odd-step certificate. For every n>1, a first coefficient crossing by 14186 is the first actual descent. Any discrepancy must occur later. The theorem does not prove crossing existence for every source; it adapts existing accumulator arguments without a priority claim. The inherited stopping record at 1,126,015 is also proved to be a first coefficient crossing at step 224.

Both CI runs passed complete Lean compilation and the audit: 12 theorem footprints, 3,998,718 independently checked sources, and three false controls rejected. An additional independent census found that step 224 is attained by both 1,126,015 and 2,252,031 in this range; the second observation is computational, not separately a Lean theorem in this addition.