Rosenzweig–Stanfill Open Problem 1.3

Rosenzweig and Stanfill state in Open Problem 1.3 (arXiv:2606.04225v1, page 2):

Show that $p_{2m,S_1}(\tfrac{1}{2}-m)\neq0$ for all $m\in\mathbb{N}$ where the sequence $S_1$ satisfies \eqref{Eq:S1}.

Their Definition 1.1 gives the Bell-polynomial expression

Given a sequence of numbers, $S$, indexed over a set $J\supseteq \mathbb{N}$, we define $p_{j,S}(t):=\sum_{k=0}^j \frac{(-1)^k}{k!} \widehat{B}{j,k}(s_1,\dots,s{j-k+1})t^k=\frac{(-1)^j}{j!}\det\mathcal{N}_{j,S}(t),\quad j\in\mathbb{N}_0,$

and equation (1.8) gives

$s_k^{(1)}=(1-2^{1-k})\frac{2 B_{k}}{k}=-\frac{2}{k}B_k(1/2),\quad k\in\mathbb{N}.$

The Lean encoding uses m : ℕ with 1 ≤ m for the source's positive naturals and uses the first Bell-polynomial expression.

The paper leaves this numbered problem open. The frozen declaration D5/S3/ArithSums/LogLaplacianBellNonvanishing.result proves its quantified nonvanishing statement for every positive natural index.

Issue #11490 preregistered the Tier 1 external open problem, the verbatim source statement, the literature check, and the 2-adic route before Lean implementation. The bounded search recorded not-found-in-searched-scope; the paper's v1 text explicitly presents Open Problem 1.3 as unproved.

The proof works over the 2-adic valuation on ℚ.

1. Odd-index sequence entries vanish, so only even Bell-profile indices contribute.
2. The von Staudt–Clausen formula gives the exact 2-adic valuation of each even Bernoulli number.
3. After scaling by 24^m m!, every nonprincipal profile has strictly positive valuation, while the unique profile with j₂ = m has valuation zero.
4. The ultrametric inequality makes the scaled sum nonzero, and hence the original Bell value is nonzero.

A counterexample would be a positive m for which the Bell-polynomial sum defining pBell (2*m) S1 ((1:ℚ)/2-m) is zero. The proof route would also fail if the valuation comparison did not separate the principal profile from every other nonzero profile.

The module compiles with the pinned Lean toolchain and standard axioms. Its public declarations are BellProfile, bellOrdinary, pBell, S1, claim, and result; result has type claim.

The source note is Library/ArithSums/rosenzweigstanfill2026loglaplacians.md, which records arXiv:2606.04225v1, the DOI locator, Open Problem 1.3's statement location, and the relevant definitions.

Tier 1 external named open problem, preregistered in issue #11490 before implementation. Resolution: proved. Admission basis: open-problem-resolution (#11490; Proved). Generality: I, following the imported frozen owner D5/S3/ArithSums/LogLaplacianEvenResidueVanishing, whose bellProfiles definition is used directly.

| declaration | proof_shape | escape witness | | --- | --- | --- | | result | bind-only | none |

The judgement form is the v4 preregistration in #11490. The valuation-domination statement and the scaled-sum identity are local have statements inside result. There are no private theorem or lemma declarations and no companion theorem. The literal Bell sum, coefficient valuations, factorial estimates and ultrametric facts remain on the proof's live path.

Information-escape registration is paused under CLAUDE.md §3.9.

What the settlement shows

Proved. The 2-adic valuation argument establishes nonvanishing uniformly for every positive m; the unique valuation-zero Bell profile is the one with j₂ = m, and all other nonzero profiles have positive valuation after scaling. The result therefore extends across the full quantified domain in Open Problem 1.3, with no numerical cutoff.

Formalization boundary. The Lean theorem is the exact rational Bell-polynomial statement encoded by claim; the displayed source determinant identity and the analytic fundamental-solution consequences are not part of this module's formal conclusion.

Open. The bridge from this result to the paper's separate Open Problem 1.6(i), and any analytic consequence requiring the paper's Theorem 1.2 and residue formula (1.7), remains open in this repository.

The two unidentified citing-work snippets in the preregistration remain ASSUMED-UNVERIFIED: their identities and whether they settle the problem have not been established. The bounded literature search does not establish exhaustive worldwide novelty or priority. The source has one arXiv version (v1, 2 June 2026); no claim is made about later unpublished work.