Integer existence and dyadic parity for OEIS A397594

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\geq0}a(n)X^n\in\mathbb Z[[X]]$, with $a(0)=1$. Rational rescaling means coefficientwise mapping to $\mathbb 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\geq1$, indices $0,\ldots,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. |

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).

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.

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 $\mathbb 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 $\mathbb Z/2\mathbb 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.

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.

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\leq39$ and formula (2) for $1\leq n\leq100$, and gives odd indices $5,7,9,15,17,31,33,63,65$ in $4\leq n\leq100$. These are finite computed results, separate from the all-index theorem.

1. 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)^n4^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$.
2. 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.
3. Kernel-checked parity: result's second conjunct gives exactly $n=2^k\pm1$ 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.
4. 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.
5. 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)=\operatorname{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.

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.