[yuiyuiui]

Submission type and scope

Mathematical publication/reference update for scope review. This PR does not claim a complete finite-n solution, Lean formalization, an award, or first priority for the constant or node construction. The catalog remains Open, Lean proof: No, Eligible to claim: No.

Problem

• Problem: JSP-000938, corresponding to Erdős Problem 1131, ordinary integral of the squared Lagrange cardinal functions over arbitrary distinct real nodes in [-1,1].
• Current entry and proposed change: add the paper reference to Publication details only. No status, solver-credit, Lean, eligibility, candidate or award change is proposed.
• Related issue: None.
• Paper: Sharp first-order asymptotics for the squared Lagrange interpolation integral, Kaiwen Jin, version 1, 24 October 2026. See Theorem 1.1 on p. 2; the complete proof is in Sections 2–7, pp. 3–44. The matching Jacobi construction is in Section 6, pp. 38–43. The complete paper has 45 pages.

For the original unit-cardinal ordinary-dx functional, let m_n be its infimum over every n distinct real nodes in [-1,1]. The paper gives

m_n = 2-c*/n+o(1/n),
c* = Gamma(1/4)^2/[8 Gamma(3/4)^2] = 1.0942198076... .

It proves the corresponding arbitrary-node asymptotic lower bound and a matching sequence given by the actual roots of the Jacobi polynomial P_n^(-3/4,-3/4). It does not determine the exact minimum for every fixed finite n or classify finite-n minimizing configurations. Scope and statement correspondence are explicitly presented in the paper. Maintainer assessment of the appropriate catalog treatment is requested.

Prior work and related contribution

The coefficient-1 conjecture had already been publicly disproved. Formal Conjectures PR 4585 and its immutable public proof establish an eventual defect at least 106/105, while leaving the exact minimum and sharp limiting coefficient unresolved. This paper does not claim that disproof as a new contribution.

Brutman and Toledano's 1997 article, DOI 10.1016/S0898-1221(97)00232-0, numerically predicted the same leading digits 1.094219... by finite optimization and Richardson extrapolation (journal pp. 43–45, Eq. (28), Tables 1–2). The paper explicitly credits that prediction. The earlier article also introduced an explicit Average node set and conjectured its asymptotic optimality (pp. 46–47, Eqs. (33), (35)–(36)); that separate construction conjecture is not asserted here. Its general cardinal-square identity (Theorem 2.1, Eq. (7), pp. 39–40) is acknowledged at the related Hermite reduction.

The submitted paper supplies a rigorous sharp arbitrary-node asymptotic argument, an exact gamma expression and a matching actual Jacobi construction. The 1997 argument for the limiting coefficient is numerical/extrapolative; no sharp arbitrary-node proof or this Jacobi construction appears in its full body. No absolute first-priority claim is made for the present theorem, constant or node family.

Attribution and verification

• Paper author and stated contribution: Kaiwen Jin, the sharp-asymptotic argument presented in the linked paper; submitting account yuiyuiui. The byline and contact appear on the paper.
• Previous disproof: credited to its actual public sources above; no reassignment of that work is proposed.
• Lean contribution: None submitted.
• Independent human verifier: None reported. The paper is submitted for mathematical and scope review; no official acceptance is asserted.
• AI assistance is disclosed at the end of the paper.

Checks

• Only the relevant catalog publication reference is changed; third-party credit and all status/eligibility fields are retained.
• The single external file deliverable is the complete paper PDF, linked at a fixed commit in the submitting account's fork; no source archive, code, private proof/audit records or identity/payment material is published.
• The paper's contribution is stated at its actual sharp-asymptotic scope.
• A full exact finite-n solution of the original extremal problem is not claimed. This is a publication-reference/scope-review update, not a request to mark the whole problem solved or award-eligible.