trureturing — Discovering truth

bibkey: hanna2010a174470
authors: Paul D. Hanna
year: 2010
title: "OEIS A174470: Thue/Roth weighted exponential integrality"
doi: null
url: https://oeis.org/A174470
claim: "Conjectured to consist entirely of integers."
strata_touched:
  - D5/S1/Recurrence/Algebraic/HannaThueRothExponentialIntegrality
license: citation-only
triage: anchor

Verified locator

Source: https://oeis.org/A174470

The primary source is OEIS A174470, revision 2, with the conjecture in its COMMENT field. It has no page number, DOI or primary arXiv version. The referenced bit sequence is OEIS A014578, revision 68: https://oeis.org/A014578/internal.

Source statement

The NAME and COMMENT fields of A174470 read verbatim:

%N G.F.: exp( Sum_{n>=1} A014578(n)*(3x)^n/n ), where A014578 is the binary expansion of Thue constant.
%C Conjectured to consist entirely of integers.

The NAME, substitution description and recurrence of A014578 read verbatim:

%N Binary expansion of Thue constant (or Roth's constant).
%C a(0) = 0; then fixed point of the morphism 1->110, 0->111, starting with a(1) = 1. - _Philippe Deléham_, Mar 21 2004
%F a(0)=0; a(3k)=1-a(k) for k>=1; a(3k+1)=a(3k+2)=1 for k>=0. - _Benoit Cloitre_, Mar 19 2004

The PARI implementation is also quoted verbatim:

%o (PARI) A014578(n) = if(!n,n,valuation(n, 3)%2==0); \\ _Ralf Stephan_, Sep 02 2013, edited for the term a(0)=0 - _Antti Karttunen_, May 28 2024

It sets the zero term to zero and otherwise tests whether the three-adic valuation is even. The Lean bit function takes values in ℤ; the series is in ℚ[[x]], and its ordinary coefficient indices range over all natural numbers, including zero. PowerSeries.subst takes the input series first and PowerSeries.exp ℚ second. The existing logInput supplies rational coefficient c(n)/n, with zero constant coefficient.

Arithmetic mechanism

For c(n)=b(n)·3^n, the prime-three Dold congruence follows from padicValNat 3 m + 1 ≤ m when m ≠ 0. At every other prime, multiplication by that prime preserves the three-adic valuation, and Euler’s prime-power congruence supplies divisibility of the power difference. The existing Dold exponential-integrality theorem then gives every integer coefficient.

Evidence boundary

Preregistration and the bounded literature screen: https://github.com/the-omega-institute/trureturing/issues/23128. The source-specific settlement is suspected-novel within that screen; literature completeness is ASSUMED-UNVERIFIED. The Dold criterion and Euler’s theorem are existing mathematical ingredients.

The experiment is in the-omega-institute/trureturing-experiments, commit 7b47971a07a821f567d4926081810ef189766d13, at docs/reports/hanna-a174470-integrality/check.py, SHA-256 4f68da48ab26f1355bbca604d0674f662dea1c564c36ef0054b5520cd91bd8d7. The preregistration records exit 0 for python3 docs/reports/hanna-a174470-integrality/check.py, with 27 source coefficients matched, integral coefficients through degree 120, 7,800 Dold cases, and the base-B test for −12 ≤ B ≤ 12 through degree 45. Those finite readings support the source identification; the infinite integrality statement is proved by the Dold argument.