Divisibility modulo three of the A373308 coefficients

OEIS A373308, Paul D. Hanna, Jun 20 2024, gives the following NAME and COMMENT, quoted verbatim from Library/Arith/hanna2024a373308.md.

NAME:

Expansion of Product_{n>=0} (1 - x^(2^n))^3.

COMMENT:

Conjecture: a(3n+1) and a(3n+2) are divisible by 3 for n >= 0.

The entry's separate Thue-Morse congruence for a(3n) and zero-index characterisation conjectures are context only; neither is claimed here.

This is a first-tier recent OEIS conjecture. The target is the divisibility assertion for every natural index, with KPI = open problems resolved.

The supplied search-seat record reports no proof found: the OEIS entry and revision history were read on 2026-09-09, followed by identifier searches on arXiv, MathOverflow, and GitHub. This Stage-B seat had no network access and did not independently repeat those searches. No exhaustive literature search or first-publication priority is asserted.

The infinite product in the NAME, Π_{n≥0}(1 − x^{2^n})³, is represented by its defining functional equation A = (1 - X)^3 * A.subst (X^2) with A(0) = 1. Mathlib has no infinite products of formal power series; the equation is the exact characterising property, obtained by removing the first factor and shifting the remaining factors. This is the honesty boundary: Lean proves existence and uniqueness for that equation, not an identity involving a formal infinite-product operator.

The integer sequence a is defined recursively with a(0) = 1 (multiplier 1). For positive n its recurrence is a(n) = Σ_{i=0}^{min(3,n)} C(3,i)(-1)^i [n-i even] a((n-i)/2). The implementation sums through n using the coefficients of (1 - X)^3; those beyond degree three vanish. Index subtraction and division are natural number operations. generatingSeries = PowerSeries.mk a is the integer formal power series A. generating_equation proves both A(0) = 1 and A = (1 - X)^3 * A.subst (X^2). generating_unique uses strong induction on coefficients to show that every B with constant coefficient 1 satisfying that equation equals A.

Over ZMod 3, Frobenius gives (1 - X)^3 = 1 - X^3, so the reduced series satisfies Ā = (1 - X^3) * Ā.subst (X^2). mod_three_support, via the private solution_support strong induction, proves (a n : ZMod 3) = 0 whenever 3 ∤ n: both contributing halved indices n/2 and (n-3)/2 remain outside the multiples of three and are smaller than n. The second contribution occurs only when n is at least three and n-3 is even; the first requires n even. hanna_conjecture then states 3 ∣ a (3*n+1) ∧ 3 ∣ a (3*n+2) for every n.

The separate Thue-Morse and zero-index conjectures are not claimed. The module has Mathlib-only imports, no D5 import, and generality G.

A natural index n for which either a(3*n+1) or a(3*n+2) is not divisible by three would contradict the assertion. The orchestrator's exact check is supporting evidence only; a finite check does not establish this universal statement and was not rerun by this seat.

• Lean module: D5/S1/Recurrence/Invariants/CubedBinaryProductModThree.lean.
• Main public theorem: hanna_conjecture.
• Companions: generating_equation, generating_unique, mod_three_support.
• Axioms: std3 (propext, Classical.choice, Quot.sound), as reported for each public theorem by the implementation seat's #print axioms checks.
• The orchestrator reported verification of make lean, make lean-report, and make emit before this Stage-B edit; these were not rerun by this seat.

theorem. The formal proof closes the quoted universal divisibility assertion for the unique normalized functional-equation solution representing the NAME.

The quotations, attribution, and date were supplied by the orchestrator and copied from the Library note. The OEIS revision history was read by the search seat on 2026-09-09, not by this network-disabled Stage-B seat. The reported literature scope was the OEIS entry and its revision history plus identifier searches on arXiv, MathOverflow, and GitHub; private MathSciNet and zbMATH indexes and the third-party Lean ecosystem were not exhaustively checked by this seat. First-publication priority and the external source's identification with the normalized functional equation are not kernel-checked facts.