Proofs · exact certificates · compressed computation · partial Lean formalization

---

The problem

For a positive integer (m), define

[ b_1=m,\qquad b_{n+1}=b_n+(b_n\bmod n). ]

The Cloitre stabilization conjecture asks whether, for every start (m), the increments

[ b_{n+1}-b_n ]

are eventually constant. The problem appears in OEIS A073117, OEIS A117846, and MathOverflow 191518.

Important

The universal stabilization conjecture remains open. This repository contains internally audited partial theorems, certified finite results, and reproducible computational evidence—not a proof of universal stabilization.

Results at a glance

Finite-start theorem If the orbit from (m) has eventual increment (c), then [ \boxed{m<(c+3)(3c+5)}. ] This converts every fixed-increment question into a finite computation.	Certified nonsurjectivity The eventual increments are not surjective onto the positive integers. The smallest omitted values are [ \boxed{5\text{ and }7}. ] This is supported by an independent arbitrary-precision certificate covering the complete finite ranges supplied by the theorem.
Counterexample restrictions Every bounded-quotient orbit stabilizes. Hence any counterexample must satisfy [ q_n\to\infty, \qquad q_n=\Omega_m!\left(\frac{n}{\log n}\right), \qquad b_n=\Omega_m!\left(\frac{n^2}{\log n}\right). ]	Periodic behavior excluded No admissible nonzero eventually periodic quotient-change sequence exists. Therefore any counterexample must be genuinely aperiodic.

Structural coordinate

Write

[ b_n=q_n n+r_n,\qquad 0\le r_n<n,\qquad e_n=r_n-q_n. ]

Then the recurrence becomes

[ \boxed{e_{n+1}=2e_n-\Delta q_n(n+2)}, \qquad e_{n+1}\equiv2e_n\pmod{n+2}. ]

Stabilization is exactly the event (e_n=0). This exposes the dynamics as a doubling map with a moving modulus and supplies the main organizing coordinate for the project.

Claim status

Claim	Current status	Evidence boundary
Universal stabilization	Open	No proof claimed
(m<(c+3)(3c+5))	Internally proved	Complete proof; awaiting external mathematical review
Eventual increments 5 and 7 are omitted	Certified	Independent complete finite certificate
106 omissions among (1,\dots,1823)	Census result	Primary compressed census; full independent census pending
Counterexample growth bounds	Internally proved	Complete proof; awaiting external mathematical review
No eventually periodic quotient-change sequence	Internally proved	Complete proof; awaiting external mathematical review
Two-counter termination for every valid entry state	Open	Only the eventually-no-down branch is reduced
Safe-map instance at (N=10^6)	Certified finite result	Independent Rust/Python agreement

“Internally proved” means that a complete proof is present and passed a fresh-context internal audit. It does not mean that an external specialist has refereed it. See audit/release-readiness.md.

The aperiodic frontier

For an eventually-no-down tail, the project derives an exact future-digit identity and an exact two-counter safe map. A compressed certificate checks all (999{,}999) positive states at index (10^6) and empties the safe set after (9{,}019) additional steps.

Caution

The two-counter map covers the eventually-no-down branch only. A hypothetical counterexample with infinitely many quotient down-steps lies outside this reduction. The (N=10^6) certificate is rigorous but finite; it is not a uniform termination theorem.

Computational record

	Previous baseline	This project
Verified starting values	(m\le2\times10^5)	(m\le10^7)
Longest stabilization index	(9{,}363{,}863)	(327{,}695{,}231)
Smallest start attaining record	(31{,}873)	(1{,}320{,}111)
Eventual increment there	(2{,}341{,}202)	(81{,}923{,}126)
Distinct compressed orbits	—	9,911 from (10^7) starts

The primary sweep advances the set of live values in lockstep and checks the covering identity

merges + absorbed + live == starts

before reporting a completed range.

Verification stack

Layer	Role
search-framework/	Zero-dependency Rust dynamics, compressed sweep, census, periodic and safe-map tools
verification-framework/	Independent u128 raw-(b) verifier
verification-framework/verify.py	Third implementation using arbitrary-precision Python integers
independent/	Independent certificate regenerators
lean/Conjecture.lean	Mathlib-free Lean formalization of foundational identities
.github/workflows/ci.yml	Rust, Python, certificate, hash, OEIS, and Lean checks

The Lean development compiles without sorry, but it does not formalize the finite-start theorem, growth bounds, all-period exclusion, or two-counter reduction.

Recommended reading path

1. audit/evidence-manifest.md — audit release identity, canonical artifact hashes, and evidence boundaries
2. manuscript/README.md — compact statement-and-proof dossier
3. audit/theorem-dependency.md — theorem dependency graph and critical cuts
4. theorem-status.md — complete claim ledger
5. supplement/README.md — algorithms, certificates, and reproduction
6. audit/fresh-proof-review.md — fresh-context internal audit

Research notes and specialized analyses

File	Contents
partial-proofs.md	foundational proofs and finite-start theorem
bounded-quotient-analysis.md	entry ridge, rebound cascade, bounded quotient, growth bound
periodic-orbit-analysis.md	affine-phase obstruction and finite periodic search
periodic-denominator-families.md	denominator-family exclusions
periodic-boundary-reduction.md	universal boundary subset-equation reduction
aperiodic-tail-analysis.md	future-digit identity and monotone-tail safe map
symbolic-analysis.md	doubling model, heuristics, and failures
compressed-orbit-analysis.md	compression design and rejected approaches
invariant-search.md	negative invariant and potential searches
literature-review.md	prior work and attribution
research-log.md	exploratory chronology and corrections
research-log-aperiodic.md	continuation chronology
future-directions.md	ranked unresolved directions

Reproduction

Fast continuous-integration checks:

cargo test --release --manifest-path search-framework/Cargo.toml
cargo test --release --manifest-path verification-framework/Cargo.toml
cargo run --release --manifest-path verification-framework/Cargo.toml -- --selftest
python verification-framework/verify.py --oeis
python independent/verify_small_spectrum.py
python scripts/periodic_phase_blocks.py --max-denominator 501
lake build
lean lean/Conjecture.lean

The full (10^7) census and full (N=10^6) independent safe-map regeneration are intentionally not run on every push. Exact commands and expected digests are recorded in supplement/03-reproduction.md.

Frozen audit release

The exploratory snapshot is commit f19ffcd75d04a05529878ce0226088f2f3221c0b.

The complete immutable audit package is tagged:

v0.1.0-audit → 46e4780dc4955c1fd21110aebcbc6da688794668

Later README, metadata, and CI maintenance do not alter that frozen record.

Citation

Citation metadata are provided in CITATION.cff. The package is AI-assisted and maintainer-curated; that boundary is stated explicitly in the citation metadata and audit documents.

---

The central conjecture is open. The partial results, certificates, and exact scope boundaries are the contribution of this repository.