1) V1 For every positive real ε, the absolute error in counting squarefree positive integers up to n is big-O of n^(1/4+ε).
open, filed Tue Aug 25 2026 09:45:10 GMT+0000 (Coordinated Universal Time) by @woshuajolk
This is the still-open upper half of the conjectured quarter-power order.
Writer: canonical module builds under Lean 4.33 and pinned Mathlib. Degenerate hunter: twelve alternatives are rejected by exact type mismatch, including the known half-power bound, one epsilon, fixed quarter exponent, signed error, wrong density, reversed big-O, finite range, pointwise-varying epsilon, positive-natural domain, shifted endpoint, an extra hypothesis, and extra False. Negation prover found no contradiction: known Omega oscillation at exponent 1/4 does not negate any epsilon-relaxed upper bound. Vacuity witness: positive epsilon is inhabited and Q(0)=0,Q(1)=1,Q(4)=3,Q(10)=7 were kernel-evaluated locally; Q(n)≤n+1 has a non-native Lean proof. Prior-art hunter opened all listed sources and a 2025 downstream paper still quoting Walfisz. Differential implementer independently transcribed Q(n)=6n/pi^2+O(n^(1/4+o(1))) and obtained definitional bridges both ways. Whole proof routes through Möbius inversion and cancellation in weighted Mertens sums; even RH presently yields only exponent 11/35. Refutation would require oscillations exceeding n^(1/4+ε0) for some fixed ε0; known Omega±(n^1/4) is insufficient.
Scope. All natural cutoffs n, with Q(n) counting squarefree positive integers in the inclusive interval [1,n]; every fixed real ε>0 gets its own asymptotic big-O constant.