ProofAtlas

Number theory · dynamical systems · formal theorem

Power-Saving Bound for Logarithmic-Time Collatz Descent

For every N ≥ 15,552, the proportion of natural numbers n < N that do not fall below their starting value within k ≤ log n accelerated Collatz steps is at most 10,000,000 · N⁻¹ᐟ¹⁰⁰.

Scope: For every natural cutoff N ≥ 15,552, the checked theorem bounds the proportion of n < N with no accelerated Collatz iterate below n within k ≤ log n steps by 10,000,000 · N⁻¹ᐟ¹⁰⁰.

Lean checkedBuild passed
Unfinished proof stepsNone
PublicationAccepted formal theorem
Logarithmic-time stopping statement mapFor every cutoff N at least 15,552, the proportion of starts below N that do not descend below themselves within their logarithmic accelerated-Collatz clock is bounded by an explicit negative power of N.
Exact scope: For every natural cutoff N ≥ 15,552, the checked theorem bounds the proportion of n < N with no accelerated Collatz iterate below n within k ≤ log n steps by 10,000,000 · N⁻¹ᐟ¹⁰⁰.

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.

theorem natCountingRatio_finiteStoppingTime_log_failure_le_power {N : ℕ} (hN : 15552 ≤ N) : natCountingRatio {n : ℕ | ¬ ∃ k : ℕ, (k : ℝ) ≤ Real.log (n : ℝ) ∧ accelerated^[k] n < n} N ≤ 10000000 * (N : ℝ) ^ (-(1 / 100 : ℝ))
Definitions used in this proposition

accelerated

def accelerated (n : ℕ) : ℕ :=
  if Even n then n / 2 else (3 * n + 1) / 2

natCountingRatio

noncomputable def natCountingRatio (s : Set ℕ) (N : ℕ) : ℝ :=
  (natCount s N : ℝ) / (N : ℝ)
Open main Lean file

Proof route

From parity words to a power-saving stopping bound

6 proof stages

The checked route has six distinct movements: parity words encode accelerated iterates and residue classes; contracting words force descent after a finite threshold; a binomial tail counts the remaining words; a logarithmic clock isolates finite and combinatorial failures; five-step blocks turn those failures into three geometric errors; and a calibrated logarithmic depth converts their decay into the explicit N^(-1/100) exceptional-proportion bound.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

  1. Scientific figure illustrating: A length-k even/odd history determines the affine formula for the k-th accelerated iterate and one residue class modulo 2^k.
    A length-k even/odd history determines the affine formula for the k-th accelerated iterate and one residue class modulo 2^k.
    01

    Parity words encode iterates exactly

    A parity word of length k fixes accelerated^[k] n and one congruence class modulo 2^k

    The proof begins with deterministic coding, not a probabilistic Collatz model. Complete parity words and residue classes correspond exactly, so counting words later becomes a count of possible starts.

    Lean lemmas for this step
    • ParityWord
    • iterate_affine_of_parityPrefix
    • unique_residue_for_word
  2. Scientific figure illustrating: When a parity word contains few enough odd steps, its multiplicative factor is below one and its affine correction is absorbed beyond a finite start threshold.
    When a parity word contains few enough odd steps, its multiplicative factor is below one and its affine correction is absorbed beyond a finite start threshold.
    02

    Contracting words force descent

    3^s / 2^k < 1, together with a finite threshold, implies accelerated^[k] n < n

    The contracting-word argument is pointwise on each retained residue lane. It proves descent below the starting value after an explicit finite cutoff, while deliberately leaving a class of noncontracting words for the counting argument.

    Lean lemmas for this step
    • branch_descends_of_contracting
    • descends_of_contracting_of_branchThreshold_le
    • descends_of_mem_contractingResidues_ge
  3. Sixteen four-mark parity words are arranged in five groups of sizes one, four, six, four, and one; a gold enclosure surrounds the four words with three gold marks and the single all-gold word.
    All length-four parity words form exact binomial layers of sizes 1, 4, 6, 4, and 1; the final two layers are enclosed as a finite upper tail.
    03

    A finite parity-word upper tail

    #{noncontracting length-k words} / 2^k is bounded by a binomial upper tail

    Each capsule contains four positions, with hollow cobalt rings and filled gold disks distinguishing the two parity choices. Grouping by gold-mark count lists every binary word exactly once. The gold region contains exactly the five words with at least three gold marks. This is a concrete finite counting schematic only; it asserts no general threshold or analytic tail estimate.

    Lean lemmas for this step
    • card_noncontracting_words_le_high_odd_tail
    • noncontractingWordRatio_le_highOddTailRatio
    • highOddTailRatio_le_geometric_bound
  4. Scientific figure illustrating: At depth k ≤ log n, failure is covered by a finite initial range together with the residue classes belonging to noncontracting parity words.
    At depth k ≤ log n, failure is covered by a finite initial range together with the residue classes belonging to noncontracting parity words.
    04

    The logarithmic clock isolates two failures

    failure by logarithmic time ⊆ finite early range ∪ noncontracting residue classes

    The finite stopping argument combines the pointwise contraction threshold with the word count. It does not say every later start succeeds; it supplies an explicit cover whose two parts can be estimated uniformly below a cutoff N.

    Lean lemmas for this step
    • finiteStoppingTimeLogBudgetFailureSet
    • finiteStoppingTimeLogBudgetFailureSet_subset
    • natCount_finiteStoppingTimeLogBudgetFailureSet_le
  5. Scientific figure illustrating: Grouping logarithmic depth into five-step blocks bounds the finite-cutoff, residue-rounding, and word-tail contributions by three geometrically decaying terms.
    Grouping logarithmic depth into five-step blocks bounds the finite-cutoff, residue-rounding, and word-tail contributions by three geometrically decaying terms.
    05

    Five-step blocks control three errors

    exceptional ratio ≤ finite-cutoff term + residue-rounding term + noncontracting-word term

    The effective estimate keeps the three sources separate long enough to justify each decay rate, then adds them into one exceptional envelope. They are rigorous upper bounds rather than empirical errors and have not yet been rewritten as a power of N.

    Lean lemmas for this step
    • natCountingRatio_finiteStoppingTimeLogBudgetFailureSet_le_geometric
    • natCountingRatio_finiteStoppingTimeLogBudgetFailureSet_le_five_mul
    • natCountingRatio_finiteStoppingTime_log_failure_le_five_mul
  6. Scientific figure illustrating: Choosing the depth as a logarithmic function of N converts the geometric estimates into the explicit exceptional proportion 10,000,000 · N^(-1/100).
    Choosing the depth as a logarithmic function of N converts the geometric estimates into the explicit exceptional proportion 10,000,000 · N^(-1/100).
    06

    Geometric decay becomes a power of N

    N ≥ 15,552 ⇒ failureRatio(N) ≤ 10,000,000 · N^(-1/100)

    The final arithmetic comparison holds for every N ≥ 15,552. It gives a deliberately coarse power-saving bound for starts that have not descended within their accelerated logarithmic clock; the bound need not be below one near the threshold and does not make the exceptional set empty.

    Lean lemmas for this step
    • natCountingRatio_finiteStoppingTime_log_failure_le_five_mul
    • terras_geometric_log_depth_le_power
    • natCountingRatio_finiteStoppingTime_log_failure_le_power

The theorem at a glance

Power-saving logarithmic-time descent at a glance

Ivory editorial poster for the quantitative Terras-style stopping theorem, showing the exact exceptional-set ratio, accelerated-map definition, a logarithmic clock over descending traces, four proof movements, and a red exact-scope footer.
A parity-word count gives an explicit power-saving upper bound for starts that have not descended below themselves within logarithmic accelerated time.

Accessible transcript

N ≥ 15,552 ⇒ failureRatio(N) ≤ 10,000,000 · N^(-1/100)

Parity words encode accelerated iterates and residue classes exactly. Contracting words force descent beyond a finite threshold, a binomial tail bounds the remaining words, and a logarithmic depth turns the resulting geometric errors into the explicit N^(-1/100) exceptional-proportion bound.

Read the complete poster transcript

COLLATZ DYNAMICS · QUANTITATIVE STOPPING

POWER-SAVING LOGARITHMIC-TIME DESCENT

FOR EVERY N ≥ 15,552

E_N = {n < N | no k ≤ log n has T^k(n) < n}

|E_N| / N ≤ 10,000,000 · N^(-1/100)

T(n) = n/2 if n is even · (3n + 1)/2 if n is odd

MOST STARTS DESCEND BELOW THEMSELVES WITHIN A LOGARITHMIC CLOCK

HOW THE PROOF MOVES

1 · ENCODE PARITY WORDS

Each length-k history determines one residue class modulo 2^k.

2 · FORCE DESCENT

Contracting words put the accelerated iterate below its start.

3 · COUNT THE EXCEPTIONS

A binomial tail bounds the noncontracting parity words.

4 · CHOOSE LOGARITHMIC DEPTH

Three geometric errors collapse to the explicit power N^(-1/100).

EXACT SCOPE

Descent below the starting value, not arrival at 1. Accelerated steps, not raw Collatz steps. The exceptional set need not be empty. Constants are explicit but deliberately coarse.

Theorem schematic

Power-saving descent within a logarithmic clock

Scientific figure illustrating: For every N at least 15,552, only an explicitly power-saving proportion of starts below N can fail to descend within their accelerated logarithmic clock.
For every N at least 15,552, only an explicitly power-saving proportion of starts below N can fail to descend within their accelerated logarithmic clock.

N ≥ 15,552 ⇒ natCountingRatio {n | ¬ ∃ k ≤ log n, accelerated^[k] n < n} N ≤ 10,000,000 · N^(-1/100)

For n below a cutoff N, failure means that no accelerated iterate T^k(n) is smaller than n for any k with k at most log n. The checked theorem bounds the counting ratio of those failures by 10,000,000 · N^(-1/100). It concerns descent below the start, not arrival at one.

Result boundary

What this theorem does—and does not—establish

For every natural cutoff N ≥ 15,552, the checked theorem bounds the proportion of n < N with no accelerated Collatz iterate below n within k ≤ log n steps by 10,000,000 · N⁻¹ᐟ¹⁰⁰.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

Continue the mathematics

Open questions and extensions

The pinned theorem and its complete local import closure let people and AI agents inspect the proof, compare another route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks each proposed extension against its own exact statement.

What the source ZIP contains

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and continuation data. Mathlib and other third-party dependencies are not bundled.

Complete checked Lean source · 20 Lean files · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
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 first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

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

Expanded visual

Open original image