The Bessel constant behind the sharp Khinchin inequality for Steinhaus sums at negative moments: sup_(3 ≤ t ≤ 12) 3J₀(t)² |J₁(t)|<tfrac110, proved from the power series
Abstract
Rapaport, Tkocz and Wu (arXiv:2512.09077) determine the sharp constant Aₚ in the Khinchin-type inequality Aₚ|S|₂ ≤ |S|ₚ for Steinhaus sums S=Σⱼ zⱼξⱼ in the last open range -1<p<0. The technical core of their proof, their Lemma 10, bounds ∫₀^∞|J₀(t)|³tᵖ⁻¹ d t for the Bessel function J₀ by splitting the integral at t=1,3,12, and two steps of that bound are asserted rather than proved: the constant L=sup_(3 ≤ t ≤ 12)|(d)/(dt)|J₀(t)|³|=sup_(3 ≤ t ≤ 12)3J₀(t)²|J₁(t)| is stated to be less than 0.1 on the strength of a numerical check, and on [1,3] the supremum of |J₀| over a subinterval is stated to be attained at an endpoint on the strength of the shape of |J₀|. We prove both statements from the power series of J₀ and J₁ in exact rational arithmetic. The obstacle is that on [3,12] the series cancels catastrophically, so neither interval evaluation of the truncated series nor a grid with a Lipschitz constant obtained from a bound on |J₀|,|J₁| (which is what one is trying to prove) is available. The classical monotonicity of the energy J₀²+J₁², whose derivative is -2J₁²/t, removes the circularity: one exact enclosure at the single point t=3 bounds |J₀| and |J₁| by 0.428 on all of [3,12], hence |(3J₀²J₁)'| ≤ 0.79 there, and a 289-point dyadic grid of step 1/32 closes the argument with sup_([3,12])3J₀²|J₁| ≤ 0.0805+0.79/64<0.093. The same certificate shows that 0.08 is not an upper bound and that the bound fails at t=1, so the interval [3,12] cannot be widened to [1,12]. Every statement is checked by the kernel of the Lean 4 proof assistant over Mathlib, which contains no Bessel function; the numerical part is discharged by kernel evaluation over ℚ with the three standard axioms only. The third numerical step of the same proof, a six-node tangent-line table, is not treated here: it requires rigorous enclosures of Γ and its logarithmic derivative, which we price.
Open review
This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.
Archived files
- Version 1 · current (opens in a new tab)
Source snapshot 2026-09-07 03:53 UTC
File fingerprint
86e3daa768e64deec3a3a685d36629ee017db3803653473fd63b777f39c414b2
Claim ledger
Stated results
SN1candidate2026-09-03
sup_(t in [3,12]) 3 J₀(t)² |J₁(t)| < 1/10 – the constant L of arXiv:2512.09077v2 Lemma 10, proved (not merely computed) from the power series of J₀ and J₁ in exact rational arithmetic, kernel-clean
SN2known2026-09-03
J₁(t) > 0 for 1 <= t <= 3, hence J₀ is antitone on [1,3] (J₀' = -J₁)
SN3routine2026-09-03
For every 1 <= a <= b <= 3 and t in [a,b], |J₀(t)| <= max|J₀(a)|, |J₀(b)| – the endpoint-maximum step behind the bound on A₂ in arXiv:2512.09077v2 Lemma 10
SN4routine2026-09-03
Negative controls: 3 J₀² |J₁| exceeds 8/100 somewhere in [3,12] (so 0.08 is too small a constant), exceeds 1/10 at t = 1 (so [3,12] cannot be widened to [1,12]), and exceeds 6/100 at t = 3 (so the bounded quantity is not identically zero)
SN5routine2026-09-03
Two-sided enclosure of the source's constant: 8/100 < sup_([3,12]) 3 J₀² |J₁| <= 93/1000, sharper than the source's 0.1
SN6known2026-09-03
The Bessel layer: J₀ and J₁ defined by their power series as tsums, summable for every real t; J₀' = -J₁ and J₁' = J₀ - J₁/t by term-by-term differentiation; J₀² + J₁² antitone on [1,12] (derivative -2J₁²/t); and the 24-term truncations within 2*6⁴8/(24!)² = 1.1665e-10 of J₀, J₁ uniformly on |t| <= 12
SN7measurement2026-09-03
Cost and route measurement: the whole certificate is kernel-clean under decide +kernel over Q (289-point grid: 59 s CPU, 8.2 GB peak, marginal 1.7 GB over the import baseline), contradicting the standing runbook rule that kernel decide is stuck on rational arithmetic
This ledger entry is reported in prose and is not bound to a Lean theorem.SN9known data2026-09-03
The two numerical cells of arXiv:2512.09077v2 Lemma 9, certified: l₀(0) - L(0) in [0.40001, 0.40002] and l₀(1) - L(1) in [0.30440, 0.30441], hence the source's '> 0.4' and '> 0.3'; both printed constants HOLD, the p = 0 one with only 1.65e-5 of slack
SN10routine2026-09-03
Negative controls for the Lemma 9 cells: 0.4 cannot be raised to 0.41 and 0.3 cannot be raised to 0.31; and both certificate intervals are nonempty with the psi finite-difference hypotheses satisfied
SN11measurement2026-09-03
Price of the source's Table 1 (the six-node tangent table, d₊-(j), j = 1..5): about 15-20 min of kernel time per cell and about 3 CPU-h for the whole table, because each cell needs 1100 rational log+exp enclosures for the 200-term B₂ and 900-term B₃ sums; the Bessel side is only about 110 s. Parked – under the 4 CPU-h cap but far beyond this window's 1 CPU-h
This ledger entry is reported in prose and is not bound to a Lean theorem.Provenance
- Generated by
- Machina Mathematica
- Released by
- Korea Superintelligence Labs
- Source context
- Rapaport, Tkocz and Wu, *Negative Moments of Steinhaus Sums* (arXiv:2512.09077v2, math.PR / math.FA; v1 2025-12-09, v2 2025-12-30, empty comment line, no journal reference, zero citers as of 2026-09-03) determine the sharp constant Aₚ in the Khinchin-type inequality Aₚ ‖S‖₂ ≤ ‖S‖ₚ for Steinhaus sums S = Σ zⱼ ξⱼ (the ξⱼ independent and uniform on the complex unit circle) in the last open range -1 < p < 0, closing a line that runs König–Kwapień (2001), Baernstein II–Culverhouse (2002) and König (2014). Their Theorem 1 is Aₚ = ‖(ξ₁+ξ₂)/
- Snapshot
- 2026-09-07 03:53 UTC
- Ledger commit
801848d7