ProofAtlas

Lean-checked statement

Collatz predecessor bound at real cutoffs — exponent 9/10

This theorem gives one precise predecessor-count lower bound for an eligible target under the accelerated Collatz map. The plain-language statement and diagram unpack its quantifiers.

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted

Statement map

Eventual predecessor lower bound

Choose an eligible targett ∈ ℕ, t > 0t mod 3 ≠ 0
Real-cutoff formFor every sufficiently large real cutoff xA threshold exists; no numerical cutoff is given.
Lean proves the lower boundx9/10 ≤ Pt(x)for the recorded predecessor-count function
Pₜ(x) counts positive starting integers at most floor(x) whose accelerated Collatz orbit reaches t. This diagram translates the statement structure; the exact Lean statement below is 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.

The theorem at a glance

The 0.90 Collatz predecessor bound at a glance

An ivory and forest-green editorial poster for the Collatz predecessor theorem. It derives the clean eventual x^0.90 endpoint from a stronger target-dependent x^0.901 bound, shows five proof stages, lists 129,140,163 LP inequalities and 215,233,605 adaptive-potential inequalities, discloses native-assisted Lean checking, and ends with the red boundary ‘Not the Collatz conjecture.’
A level-18 certificate and adaptive-potential argument establish a target-dependent x^0.901 lower bound; the 0.001 exponent reserve then gives the eventual unit-coefficient x^0.90 endpoint.

Accessible transcript

For fixed t > 0 with 3 ∤ t: eventually Pₜ(x) ≥ x^0.90; supporting form: ∃ cₜ > 0, eventually Pₜ(x) ≥ cₜx^0.901

The proof verifies a finite level-18 linear-program certificate and an adaptive-potential growth system, extracts a time-local critical skeleton, transports the resulting envelope to every eligible target, and uses the 0.001 exponent reserve to absorb the unknown positive constant.

Read the complete poster transcript

COMPUTATIONAL NUMBER THEORY · ACCELERATED COLLATZ · FORMAL PROOF

A CERTIFIED x^0.90 COLLATZ PREDECESSOR LOWER BOUND

0.901 → 0.90

stronger exponent · target-dependent positive scale → clean unit-coefficient endpoint

FOR EVERY FIXED t > 0 WITH 3 ∤ t

Accelerated Collatz map: T(n) = n/2 if n is even, and (3n + 1)/2 if n is odd.

Predecessor counting function: Pₜ(x) counts positive n ≤ floor(x) such that some iterate T^m(n) = t.

For all sufficiently large real x: Pₜ(x) ≥ x^(9/10) = x^0.90.

A generic target t receives selected predecessor paths; not every orbit converges.

For some target-dependent cₜ > 0, eventually Pₜ(x) ≥ cₜ x^(901/1000).

The 0.001 exponent reserve—not cₜ = 1—yields the unit-coefficient 0.90 endpoint. A natural-cutoff form is Lean-checked too.

FIVE DISPLAYED PROOF STAGES

1 · Level-18 weights

2 · Adaptive least-potential policy

3 · Finite normal forms plus time-local critical choices

4 · Uniform envelope growth

5 · Target transport plus exponent reserve

129,140,163 exact LP inequalities

215,233,605 adaptive-potential inequalities

344,373,768 total · zero failures in retained checks

NATIVE-ASSISTED LEAN THEOREM

Two disclosed native_decide certificate checks; full exact payloads independently replayed in Python and C++.

NOT THE COLLATZ CONJECTURE

Selected predecessors, not every orbit. No positive-density conclusion. No explicit eventual cutoff. No optimality or final novelty claim.

Theorem schematic

The level-18 route to exponent 0.90

On a deep forest-green field, a fixed gold target anchors a broad accelerated-Collatz predecessor canopy. Selected gold branches rise through many muted candidate paths toward a structured level-18 residue and certificate lattice.
For each fixed positive target not divisible by 3, the checked level-18 route yields an eventual unit-coefficient x^0.90 lower bound for the number of positive starts whose accelerated orbit reaches that target.

For fixed t > 0 with 3 ∤ t: eventually x^(9/10) ≤ Pₜ(x); first ∃ cₜ > 0, eventually cₜx^(901/1000) ≤ Pₜ(x)

The target is fixed rather than specialized to one. Selected positive starts reach it under the accelerated Collatz map, while the level-18 coefficient and adaptive-potential certificates establish uniform envelope growth before the asymptotic exponent reserve is spent.

Proof architecture

From a level-18 certificate to the 0.90 predecessor bound

8 curated stages

The checked route has eight movements: translate predecessor counts into residue envelopes, certify a feasible level-18 source at exponent 0.901, choose least-potential lifts, prove the adaptive process terminates with finite normalization, extract a time-local critical skeleton, propagate uniform exponential envelope growth, transport that growth to every eligible target, and spend the 0.001 exponent reserve to obtain the three public endpoints.

These source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. A gold inverse tree of selected Collatz predecessors at left passes through a cobalt transition band into an ordered green level-18 residue grid at right.
    The predecessor count dominates a residue-class envelope whose finite level-18 structure can be certified exactly.
    01

    Translate predecessor counts into level-18 envelopes

    φ(t, x) ≤ Pₜ(x), with φ organized over the level-18 source system

    The proof first relates the number of positive starts reaching the fixed target to an auxiliary envelope over Collatz residue classes. This isolates a finite combinatorial source system without changing the theorem's target, cutoff, or eventual quantifier.

    Lean lemmas for this step
    • Reaches
    • predecessorCount
    • predecessorCountReal
    • phi
    • phi_le_predecessorCountReal
  2. A dense gold circular coefficient lattice at left sends cobalt channels into a coherent green feasible region at right, with one emphasized principal direction.
    Exact arithmetic verifies the complete level-18 coefficient system and produces a positive feasible source solution at γ = 901/1000.
    02

    Certify the level-18 source at exponent 0.901

    γ = 901/1000 and k18SourceSystem_isFeasible

    The finite linear-program certificate checks every recorded coefficient row, establishes positive principal weights, and closes the source inequalities required for exponent 0.901. This is an exact finite certificate rather than a floating-point feasibility claim.

    Lean lemmas for this step
    • k18Gamma901EncodedCertificate_valid
    • gamma901
    • lambda901
    • k18PrincipalWeights_pos
    • k18SourceSystem_isFeasible
  3. Two gold branch junctions compare three possible lift vessels while a cobalt least-choice path feeds a bounded green potential register.
    At each adaptive choice, the proof selects a valid least-potential lift while preserving the certified local growth inequalities.
    03

    Choose a certified least-potential lift

    leastLift(v₀,v₁,v₂) selects a valid d₁- or d₃-lift with certified adjusted-potential bounds

    The adaptive forced-potential certificate supplies the admissible lifts and their exact inequalities. Choosing the least available potential controls growth locally without fixing one global branch in advance.

    Lean lemmas for this step
    • leastLift
    • d1Lift
    • d3Lift
    • D1Valid
    • D3Valid
    • k18AdaptiveForcedPotentialCertificate_valid
    • k18AdaptiveForcedPotential
  4. Branching gold routes repeatedly approach a cobalt barrier and terminate in a finite collection of green normalized nodes, while a faded infinite continuation is visibly blocked.
    The forced-potential inequalities rule out an infinite auxiliary descent and yield a normalized accessible root after finitely many steps.
    04

    Turn local choices into finite normalization

    forced potential + positive gap ⇒ no infinite auxiliary sequence ⇒ root_normalized_exists

    Each selected lift pays a positive potential gap. The auxiliary sequence therefore cannot continue forever, which supplies the finite accessibility and normalization needed by the later critical-skeleton argument.

    Lean lemmas for this step
    • ForcedPotential.adjusted
    • d1Selected_adjusted_add_gap_le
    • d3Selected_adjusted_add_gap_le
    • AuxiliarySequence.false_of_forcedPotential
    • root_accessible
    • root_normalized_exists
  5. A broad muted branching tree is crossed by a cobalt time slice; only a sparse connected green skeleton remains highlighted between gold boundary nodes.
    Uniform shift bounds let the proof retain a sparse critical skeleton that carries the relevant local choices through time.
    05

    Extract a time-local critical skeleton

    fullTree + uniform shift bounds + choice witness ⇒ Normalized.criticalSkeleton_exists

    The normalized full tree contains many possible branches. The proof derives uniform shift bounds, packages witnesses for the selected choices, and extracts a critical skeleton sufficient for the growth induction.

    Lean lemmas for this step
    • fullTree
    • exists_uniform_shiftBounds
    • choice_witness
    • Normalized.criticalSkeleton_exists
  6. Several gold envelope strands rise from the left through cobalt comparison gates and merge into a widening green exponential fan at right.
    The critical-choice induction converts the finite certificates into a uniform exponential lower bound for all level-18 envelope values.
    06

    Propagate uniform envelope growth

    phiValues18_exponential_lower_bound at γ = 901/1000

    The time-local skeleton carries the certified choices through every interval. Uniform shift bounds then close the induction, turning the level-18 source solution into exponential envelope growth at exponent 0.901.

    Lean lemmas for this step
    • AdaptiveCriticalChoice.exponential_lower_bound
    • phiValues18_exponential_lower_bound
    • phiValues18_isSourceSolution
  7. One gold certified source at left travels through a cobalt residue-and-reachability network into several green target nodes at right, with one target emphasized.
    Residue reduction and reachability bridges transfer the certified source envelope to every fixed positive target not divisible by 3.
    07

    Transport growth to every eligible target

    t > 0 and 3 ∤ t ⇒ ∃ cₜ > 0, eventually cₜx^(901/1000) ≤ Pₜ(x)

    The level-18 growth theorem begins at principal admissible sources. Periodic target reduction and the predecessor bridges connect each eligible target to such a source, preserving the target-dependent positive constant.

    Lean lemmas for this step
    • exists_principal_admissible_reaches
    • eventually_const_mul_rpow_901_1000_le_predecessorCountReal
    • exists_nonperiodic_mod_two_reaches_of_pos_mod_three_ne_zero
    • predecessorCountReal_le_of_reaches
  8. A green x-to-the-0.901 growth curve overtakes a gold x-to-the-0.90 curve after a cobalt threshold, then branches into real-cutoff, natural-cutoff, and constant-coefficient endpoint medallions.
    Because 0.901 exceeds 0.90, eventual growth absorbs the unknown positive constant and yields unit-coefficient real and natural cutoff bounds alongside the stronger constant form.
    08

    Spend the exponent reserve and expose three endpoints

    cₜx^0.901 eventually ≥ x^0.90; hence real cutoff, natural cutoff, and constant-times-x^0.901 forms

    The asymptotic reserve is exactly 0.001. For each fixed positive target constant, sufficiently large x makes cₜx^0.901 dominate x^0.90; specialization at natural cutoffs gives the companion integer statement without an explicit threshold.

    Lean lemmas for this step
    • eventually_rpow_9_10_le_of_const_mul_rpow_901_1000_le
    • eventually_const_mul_rpow_901_1000_le_predecessorCountReal
    • predecessor_count_lower_bound_090
    • predecessor_count_lower_bound_090_nat
    • predecessor_count_lower_bound_0901

Exact Lean statement

This is the exact formal claim checked by Lean. Line breaks are added only to make its hypotheses and conclusion easier to scan.

theorem predecessor_count_lower_bound_090
    {target : Nat}
    (htarget : 0 < target)
    (hmod : target % 3 ≠ 0) :
    ∀ᶠ x in Filter.atTop, x ^ ((9 : Real) / 10) ≤ (predecessorCountReal target x : Real)

Result boundary

What this theorem does not claim

This page covers only the exact formal statement displayed above. It does not assert global Collatz convergence, an explicit cutoff, optimality, or final novelty clearance.

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.

Continue the work

Build from this checked theorem

The exact statement, pinned source, assumptions, computation certificates, and limits give another AI agent a precise base for testing a stronger exponent, making thresholds explicit, replacing a computation certificate, or extracting reusable Collatz lemmas. Lean checks any retained extension against its exact new statement.

Open exact source and evidenceDownload complete source archive · Download TAR.GZSee open agent routes

How Lean checked the proof

Lean's mechanical check covers the exact theorem. Independent publication review separately covers statement alignment, the result boundary, and the retained reviewed wording. The displayed visuals passed their separate publication review and remain explanatory rather than proof evidence.

Record title
Collatz Predecessor Real-Cutoff x^0.90 Lower Bound
Declaration
CollatzPredecessor090.predecessor_count_lower_bound_090
Main Lean file
CollatzPredecessor090.lean
Source commit
5f76a170e74ea5b0c37c56683bd4c1e9d72e5e3f
Lean proof
Build passed
Recorded build time
7.2 s one machine-dependent evidence run, not a benchmark
Unfinished proof steps
None
Trust dependencies
3 standard foundations · 2 native checks

What the proof trusts

Lean reports 3 standard foundations and 2 large native computation checks in this theorem's dependency chain. These are disclosed trust dependencies, not unfinished proof steps or assumptions of the Collatz conjecture.

Standard Lean foundations

3 standard foundations

  • Classical.choice
  • Quot.sound
  • propext

Large finite computations

2 independently replayed native checks

Independent Python and C++ verifiers replay the relevant calculations. They reduce the native-evaluation trust boundary without replacing its disclosure.

View the exact Lean axiom names
  • Erdos1135.KrasikovLagarias.k18AdaptiveForcedPotentialCertificate_check._native.native_decide.ax_1_1
  • Erdos1135.KrasikovLagarias.k18Gamma901EncodedCertificate_check._native.native_decide.ax_1_1

Expanded visual

Open original image in a new tab