Metadata

slug: hanna397594
bibkey: hanna2026a397594
doi: null
url: https://oeis.org/A397594
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/LinearRows/QuadrupledLinearExponentDyadicSupport

Integer existence and dyadic parity for OEIS A397594

Problem

Paul D. Hanna’s OEIS A397594, revision 15, states:

G.f. A(x) such that the sum of the first n coefficients in A(x/n)^n equals 4^(n-1) for n >= 1.

Its FORMULA gives:

(1) 4^(n-1) = Sum_{k=0..n-1} [x^k] A(x/n)^n for n >= 1. (2) (4n)^(n-1) = [x^(n-1)] A(x)^n / (1 - nx) for n >= 1.

The conjecture is:

Conjecture: for n > 3, a(n) is odd iff n is of the form 2^k-1 or 2^k+1 (k > 1).

The series is $A (X) = \sum_{n \geq 0} a (n) X^{n} \in Z [[X]]$ , with $a (0) = 1$ . Rational rescaling means coefficientwise mapping to $Q [[X]]$ followed by $X \mapsto X / m$ . Powers are ordinary formal products. There is no analytic convergence assumption.

Statement echo

Source or binding convention	Lean counterpart	Scope
$a (0) = 1$ , integer coefficients, offset zero	`IsSourceSeries`, its constant-coefficient conjunct and `PowerSeries ℤ` argument	Literal normalization.
Formula (1), every $m \geq 1$ , indices $0, \dots, m - 1$	`IsSourceSeries`, rational rescaling and `Finset.range m`	The source’s $n, k$ are the binders $m, j$ .
Formula (2)	Local `hname_row` equivalence in `result`; the derivation below	The denominator is the constant-one formal inverse.
$n > 3$ , odd iff $n = 2^{k} - 1$ or $n = 2^{k} + 1$ , $k > 1$	Universal conjunct of `claim`, proved by `result`	Both directions and both strict bounds are retained.
Integer-source existence and quantification over every source	Existential and universal conjuncts of `claim`	Required by preregistration #22490; existence excludes vacuity.

Motivation

The settling declaration is D5/S1/Recurrence/LinearRows/QuadrupledLinearExponentDyadicSupport.result. It answers the external named problem preregistered in #22490. The source note is D5/L/RecurrenceComposition/hanna2026a397594. The admission basis is open-problem-resolution (#22490; Proved).

Gap

The homogeneous dyadic-support theorem and the doubled-row source concern different defining equations. The quadrupled-row source requires its own integer existence and comparison with the homogeneous solution. An observed parity pattern for finitely many coefficients does not provide either claim.

Route

Write $R_{n} (A) = [X^{n}] A^{n + 1} / (1 - (n + 1) X)$ and let $N_{n} (A)$ be the existing normalized row operator. Clearing formula (1)’s denominators gives $R_{n} (A) = (4 (n + 1))^{n}$ . The imported exact_normalization gives $R_{n} (A) = (n + 1) N_{n} (A)$ for $n > 0$ . Cancellation in $Z$ therefore gives $N_{n} (A) = t_{n} = 4^{n} (n + 1)^{n - 1}$ .

Add the series with zero constant term and positive coefficients $t_{n}$ to the imported correction map advance. The resulting map preserves constant coefficient one and improves coefficient agreement by one degree, using advance_zero and advance_agree. The imported PowerSeriesNormalizedContraction.exists_unique_fixed supplies a fixed integer series. Its fixed-point equation gives $N_{n} (A) = t_{n}$ ; the source equivalence then gives formula (1).

For $n > 0$ , $t_{n}$ maps to zero in $Z /2 Z$ . The imported normalized_map and normalized_unique identify the source modulo two with the imported homogeneous solution. The imported hanna_conjecture, applied to generatingSeries using generating_equation, gives the stated dyadic-neighbor parity criterion above degree three.

Falsifier

Nonexistence of an integer source would contradict the first conjunct. An integer source and an index $n > 3$ at which exactly one side of the parity equivalence holds would contradict the universal conjunct. A finite prefix cannot certify either all-index assertion.

Evidence

The sole public theorem is D5.S1.Recurrence.LinearRows.QuadrupledLinearExponentDyadicSupport.result. It proves the full claim, including existence and universal parity. Its proof shape is bind-only: it applies the existing contraction, normalization and homogeneous parity owners, with denominator clearing and algebraic normalization. Its escape witness is none; the external named problem supplies the admission basis. Utility is none: the result is an unbounded symbolic assertion, not a retained finite numerical certificate.

The four-slot escape audit for result is unfinished, with the template and missing-evidence boundary in #22657. No Reg registration is claimed validated. The pointwise equality/iff templates read pointwise predicates and the existential template reads only an existential. A faithful dependent-family reconstruction of this conjunction, with its variation and observational-dependence evidence, has not been compiled.

The finite experiment is quadrupled-row-dyadic-parity, at immutable commit b2b8f61f913caa4dbe8eace3d5ab8dae15cd5225. The verified check.py has SHA-256 665de37ae789c10df0fd0615fd2967a95ca76e3da0997563f2252547c03a51ba. Running its extracted bytes with python3 /tmp/op-hanna397594/check.py exits 0. It reproduces the source coefficients in degrees 0–24, checks formula (1) for $1 \leq n \leq 39$ and formula (2) for $1 \leq n \leq 100$ , and gives odd indices $5, 7, 9, 15, 17, 31, 33, 63, 65$ in $4 \leq n \leq 100$ . These are finite computed results, separate from the all-index theorem.

Triage

Proved in prose: denominator clearing and triangular normalization give $t_{n} = 4^{n} (n + 1)^{n - 1}$ for $n > 0$ . Indeed, the coefficient-rescaling formula turns the rational sum multiplied by $(n + 1)^{n}$ into $\sum_{j = 0}^{n} [X^{j}] A^{n + 1} (n + 1)^{n - j} = R_{n} (A)$ . Formula (1) makes this $(n + 1)^{n} 4^{n}$ . Dividing the integer identity $R_{n} (A) = (n + 1) N_{n} (A)$ by the nonzero integer $n + 1$ gives the asserted forcing. Reversing these equalities gives formula (1); the geometric convolution is formula (2). The row $m = 1$ is exactly $a (0) = 1$ .
Kernel-checked existence: result’s first conjunct constructs an integer source using exists_unique_fixed on the forced correction map. Proved in prose source equivalence: the reversible equalities in item 1 show that the normalized forcing and the two source equations coincide. This equivalence is also used locally as hnormalized in result.
Kernel-checked parity: result’s second conjunct gives exactly $n = 2^{k} \pm 1$ with $k > 1$ for every $n > 3$ and every integer source. Proved in prose mechanism: $4^{n} (n + 1)^{n - 1}$ is even for every positive $n$ , so normalization commutes with reduction and its forcing vanishes. Normalized uniqueness supplies the homogeneous comparison described in Route, before the parity endpoint is applied.
Computed: the pinned experiment in Evidence reproduces degrees 0–24, checks the two source identities through 39/100 respectively, and checks the odd indices through 100. The command exits 0 with the script SHA-256 stated there; no broader experimental range is asserted.
Open: arbitrary even parameters, full triangle integrality, positivity and asymptotics are outside claim and are not settled here.

What the settlement shows

Kernel-checked: an integer source exists and every integer source has the conjectured all-index parity support, by result. Proved in prose: the decisive mechanism is integral normalization before reduction modulo two; reducing the original equations before cancelling $n + 1$ would discard information in even rows. The uniqueness clause of PowerSeriesNormalizedContraction.exists_unique_fixed also shows uniqueness among integer sources. Every source $B$ has constant coefficient one and $N_{n} (B) = t_{n}$ for $n > 0$ . For the forced correction map $S (F) = advance (F) + T$ , with $[X^{0}] T = 0$ and $[X^{n}] T = t_{n}$ for $n > 0$ , the constant coefficient of $S (B)$ is one, and for $n > 0$ its coefficient is $[X^{n}] B - N_{n} (B) + t_{n} = [X^{n}] B$ . Thus $B = S (B)$ coefficientwise, and fixed-point uniqueness equates any two integer sources. This is a prose consequence, not an additional public Lean theorem.

Open: extension to arbitrary even parameters and a complete integral parameter triangle requires further statements. The source’s reversion formulas (3)–(4), positivity and asymptotics receive no settlement from this claim. The parity conjecture for parameter four is discharged; no unproved dependency of another source formula is assumed resolved.

ASSUMED-UNVERIFIED

Literature completeness is ASSUMED-UNVERIFIED. The bounded source and literature screen in #22490 found no earlier settlement: the OEIS revision retains the conjecture, and the inspected arXiv, Zenodo, MathOverflow and repository searches did not locate a proof. OpenAlex and Semantic Scholar returned HTTP 429, the broad Crossref search was non-specific, and the classical Heninger–Rains–Sloane and Gessel background works were not read in full. These gaps preclude an exhaustive absence or originality claim. The source has neither a DOI nor an arXiv identifier. Later OEIS revisions are outside the fixed source snapshot.

Keyboard shortcuts

trureturing — Discovering truth