Metadata

slug: ab2410
bibkey: acostababb2024partial
doi: 10.48550/arXiv.2410.17681
url: https://arxiv.org/abs/2410.17681v1
triage: theorem
motivation_gids:
  - D5/S3/Analytic/BesselRedheffer/AcostaBabbKernelRefutation

Acosta Babb’s weighted Bessel-kernel positivity conjecture

Problem

Ryan L. Acosta Babb, A partial converse to the Riemann–Lebesgue lemma for Bessel–Fourier series of order zero, arXiv:2410.17681v1, Section 4, Conjecture 1, states:

For all, $0 \leq α \leq \frac{1}{2}$ , $M \in N$ and $x \in [0, 1]$ , $K_{M}^{α} (x) \geq 0$ .

The selected definition is the source’s explicit weighted display

$K_{M}^{α} (x) = m = 1 \sum M (1 - \frac{m}{M + 1}) j_{m}^{α} J_{0} (j_{m} x) (M > 0), K_{0}^{α} (x) = 1.$

Here $j_{m}$ is the $m$ th positive zero of $J_{0}$ . The printed partial sum is $S_{m}^{α} (x) = \sum_{k = 1}^{m} j_{m}^{α} J_{0} (j_{k} x)$ . Its factor has index $m$ , so the printed Cesàro equality does not follow. The explicit weighted display, rather than that equality, is the target fixed by #22175.

Statement echo

Source clause or convention	Lean counterpart	Fidelity
Standard real $J_{0}$	Existing `BesselRedheffer.Defs.nbessel 0`	Reused directly; no new Bessel definition.
Positive zeros indexed from one	`j 1 = firstZero 0`; later `j` are infima of positive zeros strictly above the preceding entry	Literal binding recursive convention; first two infima identified with actual zeros in the proof of `root_brackets`. Index zero is unused.
Printed $S_{m}^{α}$	`S`	The printed index $m$ in the weight is preserved; this definition is separate from `K`.
Weighted formula and exceptional $M = 0$	`K`	Natural indices $1$ through $M$ , real weights and real powers; zero branch equals one.
Every real $0 \leq α \leq 1/2$	First quantifier and two hypotheses of `claim`	Both endpoints included.
Every natural $M$ and real $0 \leq x \leq 1$	Remaining quantifiers and hypotheses of `claim`	Includes zero modes and both interval endpoints.
$K_{M}^{α} (x) \geq 0$	Conclusion of `claim`	No extra hypothesis.
Refutation	`result : Not claim`	Exact negation; witness $(α, M, x) = (1/2, 2, 999/1000)$ .

Motivation

The conjecture supplies a proposed positivity premise for a stronger Bessel–Fourier coefficient construction. A negative value at two modes decides that premise without a classification for arbitrary mode counts. The source, binding conventions, Tier 1 assessment and partial literature screen are preregistered in #22175. The corresponding source note is acostababb2024partial.

Gap

No settlement was found in the successful literature screen recorded in #22175. The journal version, On the rate of growth of Bessel–Fourier coefficients for integrable functions, J. Math. Anal. Appl. 559 (2026), 130440, DOI 10.1016/j.jmaa.2026.130440, retains Conjecture 1 on p. 11. The unambiguous order-zero arXiv v1 assertion is the formal target. Literature completeness is ASSUMED-UNVERIFIED.

Independent later settlement. PrincipiaMathOrg/math-solutions independently settles this question in site-backup/mathdb-365454/mathdb-365454-solution.tex, at commit 47371706c400c79d06e3fb62190fcf6f7a725c85 (47371706), whose first public appearance was 2026-10-27. MJ Kang’s solution to MathDB problem 365454 was posted 2026-10-28. Both public appearances followed preregistration #22175, filed 2026-10-26T07:13:12Z. The open-problem-resolution admission precondition is checked at preregistration; these later public settlements do not invalidate that eligibility or the Lean refutation.

Route

All declaration names below belong to D5.S3.Analytic.BesselRedheffer.AcostaBabbKernelRefutation unless an owner is explicitly named. The existing normalized real Bessel series, coefficient, convergence and derivative facts supply the analytic inputs. Alternating-series remainder bounds enclose the function by finite rational polynomials. Derivative signs, the intermediate value theorem and a negative polynomial certificate between the two root intervals identify the first two positive zeros. The private two_mode identity then reduces the weighted sum to two terms, and point_negative compares them at the exact witness.

The source-specific admission basis is open-problem-resolution (#22175; Refuted). The theorem steps are classified bind-only; no independent escape-witness admission is asserted. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

Falsifier

The source assertion would require $K_{2}^{1/2} (999/1000) \geq 0$ . The module proves the strict opposite. A different interpretation based on repairing the printed $S$ formula is outside the bound target. Identifying the first two zeros is proved without adding zero-existence or zero-ordering hypotheses to claim.

Evidence

The settling declaration is D5.S3.Analytic.BesselRedheffer.AcostaBabbKernelRefutation.result. Its private proof dependencies include root_brackets, scaled_a_value, scaled_b_value and point_negative. The canonical frozen state record is Golden/Frozen/state/D5/S3/Analytic/BesselRedheffer/AcostaBabbKernelRefutation.lean.json; the Scribe records one OpenProblemResolutionClaim with resolution Refuted on result.

Exact rational experiment

Experiment directory at commit b01beb85ba641ba44f5d5711499d06a46af0ddef.

Command, from that repository root: python3 docs/reports/acosta-babb-bessel-kernel/check.py; exit code 0. Script SHA-256: ce3c873f27837df0248c09ec4c25d95d6a159658aeaed7ef0457db174a8acef1.

The script checks forty rational coefficient identities, root-endpoint signs and transferred derivative intervals, integer-power comparisons, and rational margins. It computes $27843/500000$ for the endpoint derivative lower comparison and $895734319/60000000 < 15$ for the curvature upper comparison. Its power comparisons correspond to $17/50 < α_{*} < 7/20$ . These finite comparisons do not prove the uniform-family or sharp-threshold analytic bridges. At the single point $(α, M, x) = (1/2, 2, 999/1000)$ , it computes the exact interval

$- \frac{182022699}{1 0 ^{12}} \leq K_{2}^{1/2} (999/1000) \leq - \frac{89362407}{500000000000} < 0.$

The interval computation is separate from the Lean proof, which uses the weaker sufficient rational bounds below. No uniform analytic conclusion is attributed to the computation.

Triage

Proved in the module (kernel-checked): the explicit weighted positivity conjecture is false at $α = 1/2$ , $M = 2$ , $x = 999/1000$ . Evidence: private point_negative and public result.
Proved in the module (kernel-checked): private root_brackets gives $24048255/1 0^{7} \leq j_{1} \leq 24048256/1 0^{7}$ and $55200781/1 0^{7} \leq j_{2} \leq 55200782/1 0^{7}$ . Its proof identifies the infima with actual zeros. order_one_positive, order_one_negative, first_decreasing, second_increasing and middle_negative exclude earlier or intervening zeros; the intermediate value theorem supplies the two zeros.
Proved in the module (kernel-checked): the private scaled_a_value and scaled_b_value estimates give $J_{0} (a x) \leq 1/800$ and $J_{0} (b x) \leq - 187/100000$ for the isolated $a = j_{1}$ , $b = j_{2}$ and $x = 999/1000$ . The proof of point_negative also establishes $a \leq 1551/1000$ and $b \geq 2349/1000$ , and uses these to make the negative second weighted mode exceed twice the first in magnitude.
Computed: the experiment entry above checks the endpoint-flux comparison $27843/500000$ , curvature comparison $895734319/60000000$ , and integer-power comparisons associated with $17/50 < α_{*} < 7/20$ . Evidence: the pinned check.py, command, exit code and SHA-256 above. The uniform-family and sharp-threshold analytic bridges are not Lean theorems of this delivery.
Open: formal sharp $M = 2$ sign classification and the uniform $α \in [2/5, 1/2]$ endpoint rectangle. The finite experiment checks their rational inputs, not those analytic bridges.
Open: positivity in other parameter ranges or for other $M$ ; the downstream existence assertions in Theorem 5.1 and Corollary 5.2; and Conjecture 2. Refuting the positivity premise removes the proposed conditional route, not those downstream conclusions themselves.

What the settlement shows

Proved in the module: at the single point the larger negative contribution of the second mode defeats the conjectured nonnegativity. This is the mechanism established by point_negative; a uniform endpoint-flux argument is not part of that theorem.

Explanation by rational arithmetic: the mode estimates in point_negative give the sufficient upper comparison

$\frac{2 ( 1551/1000 ) ( 1/800 ) - ( 2349/1000 ) ( 187/100000 )}{3} = - \frac{17171}{100000000} < 0.$

Proved in prose from the definition: the exceptional zero-mode kernel remains $K_{0}^{α} (x) = 1$ , since this is the zero branch of K. This surviving statement requires no assertion about other mode counts or exponents. Literature-attested: the journal’s weaker uniform lower bound in Lemma 3.3 is compatible with a negative interval and is not refuted by the point witness. It is not on this module’s dependency path.

Open: the sharp transition, the proposed uniform rectangle, and other positivity ranges require further analytic work. Theorem 5.1, Corollary 5.2 and the conditional Proposition 5.3 discussion lose the proposed positivity-based route; their existence conclusions and Conjecture 2 remain undecided here.

ASSUMED-UNVERIFIED

Literature completeness and originality are unverified. The successful source and citation screen is recorded in #22175; MathOverflow, rate-limited citation queries, unread final journal texts, uncapped broader arXiv results and full classical treatises are outside that screen. The result is repository-derived; no originality claim is made. No sharp sign classification or uniform counterexample family is claimed as kernel-checked.

Keyboard shortcuts

trureturing — Discovering truth