hanna a174470

Paul D. Hanna's OEIS A174470 states: “G.F.: exp( Sum_{n>=1} A014578(n)*(3x)^n/n ), where A014578 is the binary expansion of Thue constant.” Its COMMENT field says: “Conjectured to consist entirely of integers.” The source is revision 2; A014578 is revision 68. The source has no DOI or primary arXiv version.

Write $b(0)=0$ and, for $n>0$, let $b(n)=1$ when $v_3(n)$ is even and $b(n)=0$ otherwise. Set $c(n)=b(n)3^n$ and

$$ F(x)=\exp\left(\sum_{n\ge1}\frac{c(n)}n x^n\right)\in\mathbb Q[[x]]. $$

The assertion includes existence of this rational formal series and integrality of each ordinary coefficient at every $N\in\mathbb N$, including $N=0$.

Statement echo

| Source clause | Formal counterpart | Scope | | --- | --- | --- | | A014578's zero case and valuation-parity implementation | b | Integer-valued bits with explicit zero case. | | Weight A014578(n) times $3^n$ | c | Literal weight, with natural exponent. | | Formal exponential of the logarithmic sum | IsSourceSeries | Equality to PowerSeries.subst (logInput c) (PowerSeries.exp ℚ); logInput is reused from DoldExponentialIntegrality. | | “Conjectured to consist entirely of integers” | claim, proved by result | Existence and all-series/all-degree coefficient integrality; no additional hypotheses. |

The declarations are in D5.S1.Recurrence.Algebraic.HannaThueRothExponentialIntegrality. The claim spells out coefficient integrality and defines no second IntegralSeries predicate.

The all-index assertion is a named external open problem preregistered in #23128. Its settling GID is D5/S1/Recurrence/Algebraic/HannaThueRothExponentialIntegrality.result. The existing Dold exponential-integrality criterion supplies the final implication once the logarithmic weights satisfy its prime-power congruences.

The infinite integrality assertion is proved by result. Its proof shape is bind-only after expansion of the private helpers; its admission basis is open-problem-resolution (#23128; Proved). The escape audit for the sole public theorem remains unfinished under #23176. No faithful compiled four-slot registration is supplied: source-family reconstruction, the realization bridge, whole-family variation and sensitivity, and actual observational dependence remain missing.

For a prime $p$ and $m>0$, prove

$$ p^{v_p(m)+1}\mid c(pm)-c(m). $$

At $p=3$, $v_3(m)+1\le m\le3m$, so the required power divides both logarithmic weights. At $p\ne3$, multiplication by $p$ preserves $v_3(m)$ and hence $b(pm)=b(m)$. Write $m=p^{v_p(m)}u$. Euler's congruence modulo $p^{v_p(m)+1}$ gives $3^{(p-1)m}\equiv1$, and

$$ c(pm)-c(m)=b(m)3^m\bigl(3^{(p-1)m}-1\bigr). $$

The proof uses padicValNat.mul, padicValNat.eq_zero_of_not_dvd, Nat.padicValNat_lt_self, Nat.ModEq.pow_totient, and Nat.totient_prime_pow_succ. The private helpers combine the two prime cases into Dold c. DoldExponentialIntegrality.integral_exp_of_dold gives every integral coefficient. The formal exponential itself witnesses existence.

A nonintegral rational coefficient of the specified formal series would refute the source assertion. A failure of a Dold congruence would refute this route's sufficient premise, without by itself refuting integrality. Neither finite computations nor a negative literature search replace the kernel-checked all-index theorem.

Kernel evidence: D5/S1/Recurrence/Algebraic/HannaThueRothExponentialIntegrality.lean, theorem result : claim, with private helpers b_mul_prime, c_dold_three, c_dold_away_three, and c_dold. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}.

The source note is hanna2010a174470.

Experiment: hanna-a174470-integrality at revision 7b47971a07a821f567d4926081810ef189766d13. Command: python3 /tmp/op-hanna174470/stage-b-experiment/check.py, run on the unmodified check.py extracted from that revision, exit 0. Script SHA-256: 4f68da48ab26f1355bbca604d0674f662dea1c564c36ef0054b5520cd91bd8d7. Its readings cover the 27 displayed coefficients at indices 0–26; A014578 morphism indices 1–2187 and recurrence/floor formula indices 1–10000; integral coefficients at indices 0–120; five fractional Euler factors through degree 120; 7,800 Dold cases (26 primes at most 101 and $1\le m\le300$); and bases $-12\le B\le12$ through degree 45, with cubic coefficient $2B^3/3$. The coefficient-vector SHA-256 is 5a172eafce1a83260f2f6bc3d4dea7d0a15149c2e625ec861dcac53a22d35a42.

What the settlement shows

1. Proved, kernel-checked: c_dold_three proves the required prime-three divisibility. The valuation bound used in its proof is $v_3(m)+1\le m$ for $m>0$, supplied by Nat.padicValNat_lt_self; both logarithmic weights contain a sufficiently large power of 3. Multiplicativity of the bits at 3 is unnecessary.
2. Proved, kernel-checked: b_mul_prime gives $b(pm)=b(m)$ for every prime $p\ne3$ and $m>0; c_dold_away_three` gives the weight congruence using Euler modulo $p^{v_p(m)+1}$. Its quantifiers include $p=2$.
3. Proved, kernel-checked: result gives existence and integrality at every natural index, including zero, by the existing Dold criterion.
4. Computed: the experiment entry verifies all 27 source coefficients, integrality through degree 120, 7,800 Dold cases, and the base-$B$ extension test for $B=-12,\ldots,12$ through degree 45. Its command exits 0 and its script hash and exact scope are recorded above. These checks assert no uniform extension.
5. Open: the all-integer-$B$ equivalence “the coefficients of $\exp(\sum_{n\ge1}b(n)B^nx^n/n)$ are integral if and only if $3\mid B$” is not formalized here. Only the finite tested range is computed. This neighbouring prediction is separate from the settled source assertion.
6. Open: a generic theorem with an arbitrary integer function invariant under prime multiplication away from 3 is not formalized here. The bounded literature screen in #23128 identified no other source conjecture depending on A174470; completeness of that screen is ASSUMED-UNVERIFIED.

The source-specific settlement is suspected-novel within the literature screen recorded in #23128. That screen covers the primary OEIS entries, arXiv texts and metadata, Zenodo, public Lean collections, repository dossiers and preregistrations, and the cited classical integrality literature. Literature completeness is ASSUMED-UNVERIFIED; the screen includes unavailable or rate-limited MathDB, OpenAlex and Stack Exchange endpoints and is not a proof that no unindexed settlement exists. Dold, valuation and Euler results are existing ingredients. The unfinished escape audit is tracked by #23176 and is not a validated registration.