hanna-a174470 - trureturing — Discovering truth

Metadata

slug: hanna-a174470
bibkey: hanna2010a174470
doi: null
url: https://oeis.org/A174470
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/Algebraic/HannaThueRothExponentialIntegrality.result

Problem

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 (n \geq 1 \sum \frac{c ( n )}{n} x^{n}) \in Q [[x]] .$

The assertion includes existence of this rational formal series and integrality of each ordinary coefficient at every $N \in 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.

Motivation

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.

Gap

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.

Route

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

$p^{v_{p} (m) + 1} ∣ c (p m) - c (m) .$

At $p = 3$ , $v_{3} (m) + 1 \leq m \leq 3 m$ , so the required power divides both logarithmic weights. At $p \neq = 3$ , multiplication by $p$ preserves $v_{3} (m)$ and hence $b (p m) = b (m)$ . Write $m = p^{v_{p} (m)} u$ . Euler’s congruence modulo $p^{v_{p} (m) + 1}$ gives $3^{(p - 1) m} \equiv 1$ , and

$c (p m) - c (m) = b (m) 3^{m} (3^{(p - 1) m} - 1) .$

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.

Falsifier

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.

Evidence

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 \leq m \leq 300$ ); and bases $- 12 \leq B \leq 12$ through degree 45, with cubic coefficient $2 B^{3} /3$ . The coefficient-vector SHA-256 is 5a172eafce1a83260f2f6bc3d4dea7d0a15149c2e625ec861dcac53a22d35a42.

Triage

What the settlement shows

Proved, kernel-checked: c_dold_three proves the required prime-three divisibility. The valuation bound used in its proof is $v_{3} (m) + 1 \leq 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.
Proved, kernel-checked: b_mul_prime gives $b (p m) = b (m)$ for every prime $p \neq = 3$ and $m>0; c_dold_away_three` gives the weight congruence using Euler modulo $p^{v_p(m)+1}$. Its quantifiers include $p=2$.
Proved, kernel-checked: result gives existence and integrality at every natural index, including zero, by the existing Dold criterion.
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, \dots, 12$ through degree 45. Its command exits 0 and its script hash and exact scope are recorded above. These checks assert no uniform extension.
Open: the all-integer- $B$ equivalence “the coefficients of $exp (\sum_{n \geq 1} b (n) B^{n} x^{n} / n)$ are integral if and only if $3 ∣ B$ ” is not formalized here. Only the finite tested range is computed. This neighbouring prediction is separate from the settled source assertion.
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.

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.

Keyboard shortcuts

trureturing — Discovering truth