Strict positivity of the Dirichlet square root behind OEIS A317940

Abstract

Let g be the multiplicative arithmetic function determined on prime powers by g(pᵉ) = 2^A005187(e), where A005187(e) = Σₖ ⌊e/2ᵏ⌋. Let f be the unique arithmetic function with f(1)=1 and Dirichlet square f∗f = g (OEIS A046644). OEIS A317940 records the numerators of the rational values f(n) and asks whether they are nonnegative. We prove the stronger statement f(n) > 0 for every n ≥ 1. The argument reduces the problem to positivity of the coefficients of the formal square root of the binary Euler product ∏ᵣ (1 + z^{2ʳ}/2), which follows from a closed positive formula for the logarithmic coefficients. A Lean 4 formalization proves the exact upstream statement and is kernel-verified against Mathlib.

The theorem (exact upstream statement)

Using DeepMind's exact definitions of A005187, A046644 and A317940_f — byte-identical to the upstream file (see below). The formalization also establishes the stronger internal fact that the values are strictly positive.

Proof idea

1. Because g is multiplicative with g(1)=1, its Dirichlet square root f is multiplicative; it suffices to understand the local coefficients c_e = f(pᵉ), satisfying Σⱼ c_j c_{e−j} = 2^A005187(e).
2. Since A005187(e) = 2e − s₂(e) (s₂ = binary digit sum), the normalized coefficients b_e = 2^{−s₂(e)} have generating function B(z) = ∏ᵣ (1 + z^{2ʳ}/2).
3. Let A(z)² = B(z), A(0)=1. For n = 2ᵛ·m with m odd, [zⁿ] log A(z) = (1/2m)(2^{−m} − Σⱼ 2^{−j−2ʲm}) > 0, so every coefficient of A = exp(log A) is strictly positive.
4. Rescaling c_e = 4ᵉ a_e recovers the prime-power convolution; the multiplicative lift h with h(pᵉ)=c_e satisfies h∗h = g, and endpoint-divisor separation shows h obeys the exact well-founded recursion defining f. Hence f = h and f(n) > 0. ∎

Full write-up: HUMAN_PROOF.md · paper draft (PDF) · short note (PDF). The same argument generalizes to ∏ᵣ(1+q z^{2ʳ})^α for 0<q≤1, α>0 — DigitalEulerPositivity.lean.

Verification

The 659-line Lean proof was compiled against real Mathlib on GitHub Actions (it fetched 7,869 Mathlib .olean files), and the kernel's axiom audit is clean:

Re-confirmed at two independent commits. CI run: verify-lean (job lean-a317940) ↗. Artifacts: axiom_audit.log · AXLE_verification.json · spec_integrity.json · VERIFICATION_REPORT.md.

Independent numeric corroboration

A from-scratch exact-rational reimplementation of the definitions reproduces the OEIS anchors a(1..4)=1,1,1,7 and finds f(n) > 0 for all n ≤ 200,000. Try it live on the interactive page.

Open upstream → closed here (reproducible)

DeepMind's file states the theorem with := by sorry (Lean's marker for “unproved”). Ours discharges it. Run either command:

Hashes

Machine-readable: evidence/A317940.json · archived upstream copy.

All files

Provenance for every file: PROJECT_SHA256SUMS.txt.

Reproduce the verification

Or push to the repo and let .github/workflows/verify-lean.yml (job lean-a317940) run it on GitHub's runners.

Scope & novelty

What is established here is that the formal theorem is proved — kernel-checked, clean axioms, faithful to DeepMind's exact statement. Whether the result and its argument are new relative to the literature is a separate, human question; the honest boundary is documented in PRIOR_ART.md (the binary digit-sum product identity is classical; the positivity argument and its A317940 application appear to be new — pending independent literature review).

🔍 Prior-art check → a deep, reproducible search (live upstream status, GitHub code search, OEIS, arXiv) with an automated crawler that re-runs in CI. Current finding: no pre-existing formal proof found; the conjecture is still open upstream.