317940.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

17 declarations, 1 contain sorry, 0 declared as axioms

Nonnegativity of the Dirichlet square root of A046644

A317940 is the integer sequence whose value a n is the numerator of the rational sequence f n, where the Dirichlet convolution square of f is A046644. The auxiliary sequence A046644 is multiplicative and takes the value $2^{\operatorname{A005187}(e)}$ on a prime power $p^e$.

The conjecture asks whether f n is nonnegative for every positive n. The proof reduces the problem to prime powers and constructs positive rational coefficients $c(e)$ satisfying

$$\sum_{i=0}^e c(i)c(e-i)=2^{\operatorname{A005187}(e)}.$$

The coefficients are obtained from formal power series. A positive series $A$ is defined by the first-order differential equation $A' = \frac12 D A$. A second explicitly defined series $B$ satisfies $B' = D B$ and has the same constant term as $A^2$; uniqueness of the coefficient recurrence therefore gives $A^2=B$. After rescaling the coefficients by $4^e$, this becomes the displayed prime-power convolution identity.

Extending $c(e)$ multiplicatively over prime factorizations gives a positive arithmetic function root with root * root = a046644. Finally, the recursive definition of f is shown to be the unique Dirichlet square root with value one at $1$, so f = root and every positive-index value of f is positive.

This route was found by first exploiting the multiplicativity recorded in the OEIS entry, reducing the recurrence to the exponent of a single prime, and then recognizing the resulting coefficient identities as a formal-power-series differential equation.

References:

Imports (1)

FormalConjecturesUtil

def OeisA317940.a005187 A005187: the sum of $\lfloor e / 2^k \rfloor$ over $k \ge 0$ line 67 source
Source documentation
A005187: the sum of $\lfloor e / 2^k \rfloor$ over $k \ge 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Finset.sum, Finset.range, HAdd.hAdd, OfNat.ofNat, HDiv.hDiv, HPow.hPow
10 instances, coercions and auxiliary constants left out.
```
noncomputable def a005187 (e : ℕ) : ℕ :=
…
```
def OeisA317940.a046644 A046644: the multiplicative function whose value at each prime power $p^e$ is $2^{\operatorname{A005187}(e)}$ line 74 source
Source documentation
A046644: the multiplicative function whose value at each prime power $p^e$ is $2^{\operatorname{A005187}(e)}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: ite, Eq, OfNat.ofNat, Finsupp.prod, Nat.factorization, HPow.hPow, OeisA317940.a005187
8 instances, coercions and auxiliary constants left out.
```
noncomputable def a046644 (n : ℕ) : ℚ :=
…
```
def OeisA317940.f The rational sequence whose Dirichlet convolution square is A046644, written using the defining recurrence from the OEIS entry line 82 source
Source documentation
The rational sequence whose Dirichlet convolution square is A046644, written using the defining recurrence from the OEIS entry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Rat
Proof uses: WellFounded.fix, WellFoundedRelation.rel, measure, id, ite, Eq, OfNat.ofNat, OeisA317940.a046644, Finset.sum, Nat.divisors, dite, And, GT.gt, LT.lt, HDiv.hDiv, HMul.hMul, Not, HSub.hSub
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def f : ℕ → ℚ :=
…
```
def OeisA317940.a A317940: the numerator of f n line 100 source
Source documentation
A317940: the numerator of f n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int
Proof uses: Rat.num, OeisA317940.f
```
noncomputable def a (n : ℕ) : ℤ :=
…
```
lemma OeisA317940.f_eq The defining recurrence of f, with the recursive calls folded back to f line 105 source
Source documentation
The defining recurrence of f, with the recursive calls folded back to f.
```
private lemma f_eq (n : ℕ) :
    f n = if n = 0 then 0 else if n = 1 then 1 else
      (a046644 n -
        ∑ d ∈ n.divisors, if _h : 1 < d ∧ d < n then f d * f (n / d) else 0) / 2 := by
…
```
Mentions: OeisA317940.f, OeisA317940.a046644
lemma OeisA317940.f_one line 113 source
lemma OeisA317940.f_prime At a prime p every divisor is 1 or p, so the interior sum is empty line 118 source
Source documentation
At a prime p every divisor is 1 or p, so the interior sum is empty.
```
private lemma f_prime {p : ℕ} (hp : p.Prime) : f p = a046644 p / 2 := by
…
```
Mentions: OeisA317940.f, OeisA317940.a046644
lemma OeisA317940.f_two line 127 source
lemma OeisA317940.f_three line 131 source
lemma OeisA317940.f_five line 135 source
lemma OeisA317940.f_four 4 = 2 ^ 2 is the only case here with a nonempty interior sum, contributing f 2 * f 2 line 140 source
Source documentation
4 = 2 ^ 2 is the only case here with a nonempty interior sum, contributing f 2 * f 2.
```
private lemma f_four : f 4 = 7 / 2 := by
…
```
Mentions: OeisA317940.f
theorem OeisA317940.a_1 f 1 = 1 is the base case of the recurrence, so a 1 = 1 line 154 source
Source documentation
f 1 = 1 is the base case of the recurrence, so a 1 = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, OeisA317940.a, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Rat.num, OeisA317940.f, id, congrArg, OeisA317940.a.eq_1, Rat, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem a_1 : a 1 = 1 := by
…
```
Mentions: OeisA317940.a
theorem OeisA317940.a_2 2 is prime, so the interior sum is empty and f 2 = a046644 2 / 2 = 1 line 160 source
Source documentation
2 is prime, so the interior sum is empty and f 2 = a046644 2 / 2 = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, OeisA317940.a, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Rat.num, OeisA317940.f, id, congrArg, OeisA317940.a.eq_1, Rat, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem a_2 : a 2 = 1 := by
…
```
Mentions: OeisA317940.a
theorem OeisA317940.a_3 3 is prime, so the interior sum is empty and f 3 = a046644 3 / 2 = 1 line 166 source
Source documentation
3 is prime, so the interior sum is empty and f 3 = a046644 3 / 2 = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, OeisA317940.a, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Rat.num, OeisA317940.f, id, congrArg, OeisA317940.a.eq_1, Rat, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem a_3 : a 3 = 1 := by
…
```
Mentions: OeisA317940.a
theorem OeisA317940.a_4 4 is the first index with a nonempty interior sum, giving f 4 = 7 / 2 line 172 source
Source documentation
4 is the first index with a nonempty interior sum, giving f 4 = 7 / 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, OeisA317940.a, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Rat.num, OeisA317940.f, id, congrArg, OeisA317940.a.eq_1, HDiv.hDiv, Rat, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_ratNum, Int.ofNat, Mathlib.Meta.NormNum.IsNNRat.to_isRat, inferInstance, DivisionRing, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv and 7 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem a_4 : a 4 = 7 := by
…
```
Mentions: OeisA317940.a
theorem OeisA317940.a_5 5 is prime, so the interior sum is empty and f 5 = a046644 5 / 2 = 1 line 178 source
Source documentation
5 is prime, so the interior sum is empty and f 5 = a046644 5 / 2 = 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Int, OeisA317940.a, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Rat.num, OeisA317940.f, id, congrArg, OeisA317940.a.eq_1, Rat, Eq.refl
6 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem a_5 : a 5 = 1 := by
…
```
Mentions: OeisA317940.a
theorem OeisA317940.f_nonnegative sorry line 201 source
depends on sorry what this means
Statement uses: Nat, GT.gt, OfNat.ofNat, GE.ge, Rat, OeisA317940.f
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.