The same result, four ways. Pick the one that fits, then drive the thing itself — the slider below is not an illustration, it is the actual quantity the machine-checked theorem bounds.
The short version.
There is a famous unsolved puzzle about numbers — take a number, halve it if it's even, triple-and-add-one if it's odd, repeat. Nobody knows whether every number eventually falls to 1. This work does not solve that. It proves a smaller, precise statement that sits underneath it.
The tool is a smoothing filter. Imagine blurring a photo: you replace every pixel with a weighted average of its neighbours. The filter used here is very good at blurring — it barely reaches out at all, so it hardly moves anything far from where it started. The theorem puts a hard ceiling on how far it can reach: at most 3/(4n), where bigger n means a tighter filter.
So what does a ceiling on a blur have to do with 3n+1? Here is the actual chain.
One family of attacks on Collatz does not chase individual numbers at all. It asks whether the map spreads numbers out — whether, after enough steps, the values it produces are scattered evenly rather than clumping in patterns. If you can show the mixing is thorough enough, whole categories of bad behaviour become impossible: trajectories that settle into a loop, or drift off forever, need the arithmetic to conspire, and thorough mixing forbids the conspiracy.
Measuring that mixing comes down to bounding some very awkward sums, and the filter above is the instrument for doing it. What was proved here is that the instrument is sharp enough: a hard ceiling on its reach. Feed that ceiling into the surrounding argument and a quantity the program calls a transfer operator is forced to shrink at every scale — which is what upgrades one conjecture in the chain from assumed to proved.
Now the part that usually gets left out. That chain does not reach the Collatz conjecture. One further link in it is currently only measured — checked numerically, believed, not proved. Beyond that sits a step the program has explicitly labelled a wall these methods do not cross. And what a computer verified here is the technical base of the argument, not the whole chain and certainly not Collatz.
That accounting is the actual point. It is easy to write a paragraph that sounds like progress on a famous problem. It is harder, and more useful, to say exactly which link is proved, which is assumed, and where the road stops — and then to publish a machine-checkable artifact so nobody has to take your word for any of it.
For readers comfortable with graphs, averages and a little trigonometry.
The object is a kernel — a bump-shaped weighting function used to average a signal. Averaging with a kernel is the mathematical version of blurring: to get the new value at a point you take a weighted average of nearby values, and the kernel is that set of weights. Everything about the resulting blur is determined by the shape of the bump.
This particular bump is built out of waves. Add up the first n complex waves and you get a function that is large at the origin — where they all line up — and small elsewhere, where they interfere. Square its magnitude and you get the Fejér kernel, a classical object. Square it again and you get the fourth power used here.
Two reasons, both practical. First, a fourth power is automatically non-negative, so it is a legitimate set of weights — you cannot blur with something that goes negative without strange things happening. Second, and more importantly, the tails fall off much faster. Squaring once gives you decay like 1/t²; squaring twice gives 1/t⁴. That extra decay is exactly what makes the "reach" integral converge nicely, and it is why the sharper Jackson kernel is preferred over plain Fejér when you need quantitative control.
The awkward constant out front, 3/(n(2n²+1)), is just normalisation: it scales the bump so the weights sum to exactly 1. Blurring should not brighten or darken the picture. That constant is not chosen — it is forced, and computing it is precisely statement (i), the harder of the two results proved here.
Two properties matter, and they are in tension. The kernel is concentrated: as n grows, almost all its weight piles up near zero, so the blur becomes gentler and gentler. But concentration alone is not enough — a kernel can be tall in the middle and still have fat tails that quietly borrow from far away.
So you measure the reach: ∫J(t)·|t|dt, the average distance the weights actually borrow from. Weight sitting far out is penalised in proportion to how far out it sits, which means fat tails cannot hide. The theorem pins that reach below 3/(4n) for every n — so doubling the sharpness at least halves how far the blur can see.
Move the slider and watch both effects at once. The blue bump narrows and spikes. The green curve — the kernel multiplied by |t|, the thing actually being integrated — flattens and pulls in toward the origin. That flattening is the theorem.
Three numbers are worth watching. Total mass stays pinned at 1.0000 at every n; that is statement (i) holding, computed live by a completely different method than the proof uses. Reach falls roughly like 1/n, halving as n doubles. And headroom sits near 70% — the true reach is about 28% of the proved ceiling.
That gap is not sloppiness. A proof takes the bound it can defend cleanly across every n, not the tightest one a computer can measure at any particular n. Chasing the sharp constant would have meant a much harder argument for no benefit downstream, because the surrounding result only needs some bound of order 1/n. Knowing when a loose bound suffices is most of the craft.
The statements.
With Dn(t) = sin(nπt)/sin(πt) and Jn = (3/(n(2n²+1)))·Dn⁴, two results were formalised:
(i) ∫₀¹ Dn(t)⁴ dt = n(2n²+1)/3
(ii) ∫−1/21/2 Jn(t)·|t| dt ≤ 3/(4n)
(i) is the Fejér normalisation. Mathlib has no Fejér kernel, so it was built from scratch: write Dn⁴ = ‖∑j<n e(jt)‖⁴, expand over quadruples, integrate termwise by character orthogonality, and what survives is #{(i,j,k,l) ∈ [0,n)⁴ : i+j = k+l}. Fibre that count by d = i−k and it collapses to ∑|d|<n(n−|d|)² = n(2n²+1)/3.
(ii) follows from two pointwise bounds — J ≤ n⁴ near the origin, J ≤ 1/(16t⁴) away from it — split at |t| = 1/(2n). That constant is forced: it minimises c²/2 + 1/(32c²), and the four pieces then total exactly n²/2 − 1/4. The natural guess 1/n gives 1.0625n² − 0.25 and fails.
Worth spelling out, because the shape is reusable. The identity is proved by turning an integral into a cardinality and then evaluating the cardinality:
∫₀¹ ‖∑j<n e(jt)‖⁴ dt
= ∫₀¹ ∑i,k,j,l e(((i−k)+(j−l))t) dt — expand
= ∑i,k,j,l [ (i−k)+(j−l) = 0 ] — orthogonality, termwise
= ∑|d|<n r(d)·r(−d) = ∑|d|<n r(d)² — fibre by d = i−k
= ∑|d|<n (n−|d|)² = n(2n²+1)/3
The only analytic input is ∫₀¹e(kt)dt = [k=0]; everything after it is combinatorics. The fibre count r(d) = n−|d| comes from an explicit bijection k ↦ (k+d⁺, k+d⁻), where exactly one of d⁺ = max(d,0), d⁻ = max(−d,0) is zero — one map covering both signs with no case split.
Everything is phrased in ‖·‖², never ‖·‖. The Dirichlet ratio is signed and its norm is not, so working in squares throughout removes every absolute value and makes the fourth-power step (‖g‖²)² a single line instead of a sign analysis.
And the counting is done on ∑|i−k| rather than ∑(n−|i−k|). The second summand mentions n, so induction on n perturbs every term; the first does not, so D(n+1)−D(n) is just the new row and column. Since ∑(n−|i−k|) = n³ − D(n), you recover the target from 3D(n) = n³ − n.
These two results are the analytic base of a δ=1 certificate. The recorded chain is Tm < 1 for all m ≥ 2 ⇒ uniform δ=1 ⇒ (TM-ℓ²) sharp ⇒ K2 ⇒ (MS), which would make the Fourier-decay conjecture (MS) unconditional.
The boundary: a separate multiplicative-mass input, (MULT), is currently
measured numerically and not proved, and the conditional statement
(MS)+(MULT) ⇒ depth c₀ = 1/2−ε is a depth result, not the Collatz conjecture. The program
additionally flags a step it calls a Collatz-hard wall. What is machine-checked is this
analytic base — 79 declarations — not the reduction chain above it. The reduction skeleton
is phase 2 of the same ticket and is still open. Since this page was written, (MS) itself has
become a theorem modulo (MULT-mass) — which is now the single remaining link.
Worth recording because it is short and self-contained. Toumi (2025) proves a Gowers-norm bound for the Thue–Morse carry structure with an explicit η₀ ≈ 1.31×10⁻¹³ at k=3, decaying doubly exponentially in k. That carry-state matrix turns out to be the same operator this program solved exactly: its spectral radius is (1+√17)/8, giving
η₀ = 1 − log₂((1+√17)/4) = 0.6429813631… = 1 − β
— k-independent, and larger by a factor of about 5×10¹². Exact at k=2 (characteristic polynomial factor 4λ²−λ−1), numerically confirmed to 10⁻¹⁶ at k=3. A strong claim awaiting a written proof, not yet a formalised theorem; the distinction is deliberate.
Lean 4 + Mathlib, 79 declarations, no sorry.
The trust boundary is enforced by #print axioms on every build rather than by a
comment. Grepping for sorry is insufficient — a declaration can inherit
sorryAx through an import without the token appearing in its file.
'TXPOF59.dirichlet_pow4_integral' depends on axioms:
[propext, Classical.choice, Quot.sound]
'TXPOF59.jackson_weighted_bound' depends on axioms:
[propext, Classical.choice, Quot.sound]
Axiom audit clean - nothing depends on sorryAx.
L3_SchurCohn.lean 5 decls 96 L 2×2 stability
L1_Ramanujan.lean 11 decls 285 L unit character sums mod 3^m
L2_Orthogonality.lean 9 decls 104 L ∫₀¹ e(kt) = [k=0]
L2_FejerCore.lean 9 decls 113 L geometric-sum bridge
L2_Assembly.lean 6 decls 104 L quadruple expansion
L2_Counting.lean 3 decls 86 L fibre count r(d) = n−|d|
L2_CountEval.lean 6 decls 132 L 3D(n) = n³ − n
L2_JacksonBound.lean 18 decls 225 L pointwise bounds, evenness
L2_Jackson.lean 8 decls 310 L targets (i) and (ii)
Audit.lean — 133 L #print axioms, all 79
Mathlib has no Fejér or Jackson kernel and no Ramanujan sums, so L1 and the L2 chain are
from-scratch developments. What Mathlib does supply and this leans on:
integral_exp_mul_complex, exp_int_mul_two_pi_mul_I,
AddChar.sum_eq_zero_of_ne_one, geom_sum_mul,
integral_zpow, integral_mono_on, and
intervalIntegral.integral_congr_ae.
Squared norms everywhere. ‖·‖^2 rather than ‖·‖
throughout L2_FejerCore. The Dirichlet ratio is signed, its norm is not, and the
target is a fourth power — so squares eliminate every abs and the entire sign
case-split. That file is ~110 lines instead of several hundred.
Count the subtraction-free thing. sum_sq_range is stated as
6·∑r² + 3n² = 2n³ + n, not ∑r² = (n−1)n(2n−1)/6. Both the division
and the n−1 are hazards in ℕ: truncated subtraction breaks the
n = 0 base case and blocks ring. Clearing denominators gives an
identity true for every n with a clean induction.
Cast to ℤ before doing arithmetic. Same reason. Nearly all the
ℕ/ℤ bookkeeping in L2_Counting then falls to
omega, which understands natAbs and toNat natively.
set leaves a body. set a := 1/(2*n) makes
a a local definition, and ring unfolds it on one side of a goal but
not the other — producing residuals like (a^2)⁻¹ = a⁻¹^2 that look impossible
and are not. clear_value a fixes it in one line. Diagnosing the symptom instead
of the cause cost three rounds.
Removable singularities are not removed. fejer4 is a quotient,
so Lean's division-by-zero convention makes it 0 wherever
sin πt = 0, while ‖gₙ‖⁴ is continuous there. They agree only off a
null set, so both targets need integral_congr_ae. In (i) the bad point is
t = 1 and Ι 0 1 = Ioc 0 1 excludes t = 0 for free; in
(ii) the bad point is interior and there is no such luck.
Rewrite direction is syntactic, not semantic. Three separate rounds went to
rw firing the wrong way or on the wrong side —
← integral_ofReal when the goal held the left side,
sum_product matching the left-hand sum after
sum_mul_sum had put one there too. conv_rhs exists for this.
Lean v4.26.0 pinned in lean-toolchain, Mathlib at the matching tag.
build-quick.bat runs lake build then
lake env lean TXPOF59/Audit.lean, writing build.log and
audit.log. The audit is deliberately run directly rather than as a library
target so Lake cannot replay a cached result — and check the log's timestamp against the
sources before believing it. Three rounds here were wasted reading a log older than the file
it supposedly described.
This is the actual integrand from statement (ii). Nothing here is decorative — the numbers are computed live and compared against the proved bound.
The filled shape is Jn(t), the kernel. The lighter curve is Jn(t)·|t| — the quantity being integrated. As n rises the kernel spikes, the weighted curve flattens, and the reach falls away like 1/n. Total mass stays pinned at 1, which is statement (i) doing its job.
Nine files, each one a ticket. Click any step.