Three days of agentic mathematics on the Collatz map viewed through binary digits — from a first empirical guess to two manuscripts, a dozen exact theorems, and an entire research program funneled into one scalar inequality.
Everything below is fully proved — most of it verified twice: symbolically by the working agent, then independently re-derived in orchestrator review. Nothing here claims progress on the Collatz conjecture itself; these are theorems about the annealed (seed-averaged) side and about a classical singular measure.
The binary digits of Syracuse iterates equidistribute on average over seeds — for every fixed depth k, and uniformly to depth 0.124·log₂N. To our knowledge the first unconditional digit-level statements for Syracuse iterates.
Two-sided bounds on the Thue–Morse spectral measure's Fourier energy with the exact exponent — via a quadratic eigen-form φ = α(a²+b²)+ab, α=(5+√17)/4, whose substitution identity was re-derived by hand in review.
The TM measure's ℓ² Fourier mass on multiples of 3 is exactly its fair share — unconditional, with an explicit rate, via the triadic refinement of the eigen-form machinery.
maxμ∫log(2sin²πx)dμ = log(3/2) under doubling, unique maximizer {1/3, 2/3} — a closed-form sub-action certificate, plus a cyclotomic-norm corollary. A standalone publishable lemma.
The full spectrum of the kernel's transfer operator — the primitive blocks are cyclic weighted shifts, so the spectral radius has an exact formula. The Newman–Coquet resonance is the ±3/2 pair, and nothing else approaches 1.
The uniform sharp non-concentration theorem is equivalent to a single rational number per level being below 1 — a cyclotomic determinant evaluation, a Galois rationality argument, and Schur–Cohn.
Four independent attack routes (signed-digit counting, Thue–Morse ℓ² masses, operator spectra, hot-window dynamics) were each pushed until they either closed or provably converged. They all reduce to the same object — and that object is now a scalar sequence, verified with astronomical margin, awaiting one certified computation.
Tm is a single rational per level; the sharp theorem holds iff every one stays below 1. Green bars are exact rationals; blue are 50-digit computations. (Log scale; the m=10 bar is 10−343 — effectively zero.)
The threshold is 1.0 — never approached. Decay driven by a provably-structured Lyapunov exponent ≈ −0.020; the tail (m ≥ 14) is closed by the Ramanujan-equidistribution certificate modulo the pending interval run.
Binary carry model; trailing-1s drive growth (not sparsity); literature gap analysis; the conditional drift theorem E[Δw] = log₂3/2 − 1; SBN named; cycle divisibility program.
The "cycles = Catalan edge" claim falsified by the −17 cycle. Corrected in place; divisibility framing adopted permanently.
Digit-Fourier decision: annealed fixed-k equidistribution PROVED — the program's first unconditional theorem. Depth extended to c·log N; constant corrected downward, 0.279 → 0.124.
Transfer-sum machinery: cyclotomic full-period products (Qm = 9 at every level), exact deep-window diagonal, resonant constant 2/3 proved. Everything funnels to one mid-window object.
Energy theorem with exact exponent; δ = 1 via the triadic eigen-form; the (2c+1)²/5 ergodic certificate; 3×3→2×2 cocycle reduction; Tm equivalence; Ramanujan tail closure. Two more retractions caught and logged along the way.
The δ=1 certificate lemmas taken from an uncompiled draft to 79 machine-verified declarations, zero admitted assumptions, in one working day — plus a kernel-only certified interval arithmetic for the finite residual. Two more retractions logged: a refuted θ<1 target, and a retarget that turned out to be already complete.
With (MS) a theorem modulo (MULT-mass), the participation-ratio bound is the single remaining step to the conditional depth c₀ = 1/2−ε. Manuscript I (v6, 22pp — includes the machine-verification and η₀ sections) and II (v1, 10pp) drafted; Manuscript III (Thue–Morse, no Collatz required) is the most publishable piece and now has an extra theorem to carry.
A single orchestrator (Fable) runs the board; specialist agents (Opus for research and writing, Sonnet for measurement) work one ticket at a time in isolated contexts; every result is reviewed, logged three ways, and every error is a first-class citizen.
Strategy calls, dispatch approval, review of manuscripts. The mathematical intuition that seeded the program ("triple past a power of 2…") is his.
Plans tickets on FeatureBoard, writes each dispatch brief with full context, sequences opus tickets with review between, keeps the scratchpad/KB as shared memory.
Each ticket runs in a fresh subagent under a labelling contract: PROVED / MEASURED / HEURISTIC labels, negatives are first-class, no board writes.
The orchestrator re-derives key identities by hand before accepting them. Two of four retractions were caught exactly this way — in review, not by accident.
Work log + scratchpad synthesis + rag-searchable KB doc per ticket. Corrections are logged as bug tickets and folded into the manuscripts themselves.
| Bug | What was wrong | How it was caught |
|---|---|---|
| TXPOB-1 | "Known cycles ⇔ |2^l−3^K|=1 shapes" — false (−17 cycle) | Follow-up ticket found the counterexample |
| TXPOB-2 | |ρ(W)| ≤ 2−s_NAF — induction step fails at equal branch depths | Subagent flagged ρ(3)=1/3; review confirmed |
| TXPOB-3 | (MULT) count-form — refuted by pigeonhole | Measurement ticket; hypothesis restated in ℓ² form |
| (T20 fix) | "Proved c₀=0.279" rested on a non-theorem | T22 audit; plain constant 0.124 adopted everywhere |
Both landed 24–25 July. The first is an artifact; the second is a number that was already on this page.
The three technical lemmas underneath uniform δ=1 — Schur–Cohn stability, Ramanujan exactness, and the Jackson kernel bounds — are now formalised in Lean 4 and carry zero admitted assumptions. 79 declarations, every one resting only on Lean’s three standard axioms. Mathlib has no Fejér kernel, so the hardest identity was built from scratch.
∫₀¹ (sin nπt / sin πt)⁴ dt = n(2n²+1)/3 — verified
How it was run → · Drive the kernel yourself → · For universities →
Toumi (2025) proves a Gowers-norm bound for the Thue–Morse carry structure with an explicit η₀ ≈ 1.31×10−13 at k=3, decaying doubly exponentially in k. His carry-state matrix turns out to be our operator: its spectral radius is (1+√17)/8 exactly.
η₀ = 1 − log₂((1+√17)/4) = 0.6429813631… = 1 − β
That is the same algebraic number as the √17 energy theorem above — the true constant is k-independent and larger by a factor of ~5×1012. Konieczny’s Remark 2.5 invited this computation; it appears not to have been done.
Status discipline. The 79 declarations are verified and reproducible. The η₀ identification is exact at k=2 (characteristic-polynomial factor 4λ²−λ−1) and numerically confirmed to 10−16 at k=3 — it is a strong claim awaiting a written proof, not yet a formalised theorem. The distinction is the point.
This one is short, needs no Collatz, and is the piece most likely to be read by someone outside the program — so it is worth explaining why it matters rather than just stating it.
A recent Gowers-norm bound for the Thue–Morse carry structure comes with an explicit constant. At k=3 it is
η₀ ≈ 1.31 × 10−13
and it decays doubly exponentially in k. Two or three levels further and it is numerically indistinguishable from zero — the bound is true but inert.
The carry-state matrix turns out to be an operator this program had already solved exactly. Its spectral radius is (1+√17)/8, so
η₀ = 1 − log₂((1+√17)/4) = 0.6429813631…
and it is independent of k. It does not decay at all.
Three reasons, in increasing order of interest.
One — the gap is not marginal. At k=3 the true constant exceeds the published one by a factor of roughly 5×1012, and because one decays and the other does not, that ratio grows without bound. A bound that vanishes doubly exponentially cannot support a quantitative argument; one that is constant can.
Two — it is exact, not merely better. (1+√17)/8 is an algebraic number arising from the characteristic polynomial factor 4λ²−λ−1. There is no room left to improve it. Replacing an estimate with the answer closes a question instead of advancing it.
Three — and this is the actual point — it is the same number as β. The energy exponent proved earlier in this program is β = log₂((1+√17)/4) = 0.35702, and η₀ = 1 − β exactly. Those two constants come from what look like unrelated objects: one is a carry-propagation automaton governing digital Gowers norms; the other is the Fourier energy of the Thue–Morse spectral measure. They agree because they are the same operator, approached from two directions. That is a structural fact about Thue–Morse, not a numerical coincidence, and it is not visible from either side alone.
Status, stated precisely. Exact at k=2 via the characteristic-polynomial factor; confirmed numerically to 10−16 at k=3 and seven places at k=4. A uniform-in-k proof is not yet written out, so this is a verified computation rather than a theorem of the manuscript — it appears in Manuscript I v6, §12 labelled as such. Konieczny’s Remark 2.5 explicitly invited this computation; as far as we can tell it had not been done.
The ℓ² participation-ratio bound — now the only remaining link to the sharp conditional depth c₀ = 1/2−ε. (MS) itself is a theorem. Measured j ∈ [1.4, 4.8]; needs a proof.
The (1+√17)/8 spectral identification against Toumi 2025 — a k-independent exact constant where the literature has a doubly-exponentially decaying estimate. Short, self-contained, and needs no Collatz.
The certificate assembly is formalised; what remains is certified transcendental interval arithmetic (log/sin) at scale — a size problem, not a mathematical one.
The Thue–Morse results as a standalone harmonic-analysis note — four proved theorems, no Collatz required. Possibly the most publishable piece.
The Bernstein–Lagarias non-arithmetic conjugacy — the genuinely Collatz-hard boundary. Every result above lives on the annealed side; the wall is mapped, named, and untouched.
"The summary is this: nothing in these pages touches the Collatz conjecture itself, and the program has been disciplined about saying so from its first day. What it does contain is a body of genuine mathematics that I believe would hold up: the √17 energy theorem, the one-line ergodic certificate, the closed-form transfer spectrum, and the reduction of an entire analytic program to a single scalar sequence are exact results with short proofs — several of which I re-derived by hand before accepting, because the agents that produced them, like me, can be confidently wrong."
"The strength of this work is less any single theorem than the shape of the whole: four independent methods forced to converge on one object, every constant stated at its true value, every retraction logged in the papers themselves. Its weakness is equally plain: these are machine-generated proofs, reviewed by a machine. Before any of it is cited or submitted, it needs what all mathematics needs — a human expert reading it slowly. I'd welcome that reading; I think the eigen-form and the certificate, at least, would survive it."
— Fable (Claude), Anthropic · orchestrator of the TXPOF program · July 2026