Hanna's derivative-substitution congruences for A232696

Paul D. Hanna's OEIS A232696 COMMENTS conjectures concern integer exponential coefficients $a_n=n![x^n]A$ of rational formal power series with $A(0)=1$. The source equation and its nominated congruences are:

%N A232696 E.g.f. A(x) satisfies: A'(x) = A(x/A'(x)) with A(0)=1. %C A232696 CONJECTURES. %C A232696 a(n) == 0 (mod 2) for n>=4. %C A232696 a(n) == 0 (mod 2^2) for n>=10.

| Record | Formal equation | Nominated congruences | Settling declaration | | --- | --- | --- | --- | | A232696 | $A'(x)=A(x/A'(x))$ | $2\mid a_n$ for $n\ge4$; $4\mid a_n$ for $n\ge10$ | HannaA232696Congruences.result |

The settling declaration belongs to D5.S1.Recurrence.Residue. It universally quantifies over rational formal solutions and concludes all-index integrality as well as the two displayed congruences. The source note records the OEIS record and its literal source text.

Statement echo

| Source clause | Lean counterpart | Fidelity | | --- | --- | --- | | $A'(x)=A(x/A'(x))$ and $A(0)=1$ | IsSolution in HannaA232696Congruences | The formal derivative, substitution and constant coefficient are literal. | | $a_n=n![x^n]A$ is integral | The existential a : ℕ → ℤ with eCoeff A n = (a n : ℚ) | Integrality is a conclusion at every index. | | $2\mid a_n$ for $n\ge4$ | The first divisibility conjunct in claim | The threshold and modulus are literal. | | $4\mid a_n$ for $n\ge10$ | The second divisibility conjunct in claim | The threshold and modulus are literal. |

The preregistration #21487 supplies the source conventions and literature screen for A232696. The corresponding result uses admission_basis: open-problem-resolution with resolution Proved. The source is recorded in Library/RecurrenceComposition/hanna2013derivativesubstitutioncongruences.md. The supporting machinery is D5/S1/Recurrence/Residue/HannaEGFMachinery; ExponentialImplicitParityPeriodThree supplies convolution and coefficient identities through its private declarations.

The OEIS record labels the two residue assertions as conjectures. The proof requires an integral triangular recurrence for derivative-substitution equations, coefficientwise residual transfer, and finite polynomial residuals. The literature screen found no settlement in its searched scope; completeness remains ASSUMED-UNVERIFIED.

The shared machinery constructs the unique integral coefficient recurrence, transports coefficient congruences from an integral approximate solution, and cancels integral unit powers. A232696 uses $[1,1,1,-1]$ modulo $2$ and $[1,1,1,-1,2,6,-264,5370,-93750,1315706]$ modulo $4$; integral-unit cancellation transfers residual divisibility.

A counterexample would be a rational formal solution with constant coefficient one whose factorial-normalized coefficient fails either nominated divisibility condition. A failure of the integral recurrence, residual divisibility or unit-cancellation hypotheses would also block the proof. Passing finite coefficient checks does not establish the assertions at every index.

The settling declaration in the Problem table proves its complete claim proposition. The axiom closure of every public declaration is contained in {propext, Classical.choice, Quot.sound}. The result's Scribe node carries OpenProblemResolutionClaim(hefg-a232696, Proved) on this dossier: A232696 resolves #21487. The finite exact experiment is external evidence and does not replace the kernel proofs.

Experiment

Experiment directory at commit e2566e824df32e3f308cd1b801ef82dd17fa64cf, script check.py. The pinned script exists at that commit and has SHA-256 14fa66db49524fd5b8ccbf45b2245d0a4813980bff076b1b0a855d869393f259. Command python3 ../trureturing-experiments/docs/reports/hanna-efg-congruences/check.py; exit 0. It recomputes exact terms for indices $0$ through $300$ for A232696, checks the nominated congruences, and compares the literal rational-series iteration through degree 12. The output ends with ALL_CHECKS_OK.

The same pinned experiment prints the exact terms A232696 $a_3=-1$ and $a_9=1315706$. Each predecessor fails the respective divisibility cutoff lowered by one.

What the settlement shows

Lists of approximate-solution coefficients in the table are factorial-normalized coefficients.

| Item | Status and evidence kind | Evidence and boundary | | --- | --- | --- | | Shared integer triangular recurrence, uniqueness and modular approximate-solution transfer for every natural $k,p$ and the normalized reciprocal branch; no analytic convergence claim | Proved; kernel-checked | HannaEGFMachinery.residual_transfer, sequence_unique and the supporting recurrence declarations. Formal power-series reasoning is coefficientwise. | | Both nominated congruences for indices $0$ through $300$, with independent rational-series agreement through degree 12 | Computed; external exact computation | check.py at the pinned experiment commit, command and exit 0 above. Scope is exactly A232696, indices $0\ldots300$, and iteration degree 12. Uniform extension beyond that finite range is supplied by the kernel-checked result, not by this computation. | | Cutoff predecessors A232696 $a_3=-1$ and $a_9=1315706$ | Computed; external exact computation | check.py at the pinned experiment commit, command, exit code and SHA-256 above. These values refute lowering the respective nominated cutoffs by one. | | A232696 uses $[1,1,1,-1]$ modulo $2$ and $[1,1,1,-1,2,6,-264,5370,-93750,1315706]$ modulo $4$; integral-unit cancellation transfers residual divisibility | Proved; kernel-checked | HannaA232696Congruences.result, clear_inverse_power and the finite residual declarations. |

Literature status

The source and revision history for A232696 were read. Searches of the exact identifier in arXiv, Crossref, Math StackExchange, repository issues and the bounded author/sequence screen found no settlement in the inspected scope. The primary sources are OEIS records without DOI or arXiv identifiers. Literature completeness and absence of an unlocated prior solution are ASSUMED-UNVERIFIED.

Literature completeness is ASSUMED-UNVERIFIED. The experiment is finite exact evidence only. The escape audit for newly public declarations is unfinished under #21758; no Reg source is delivered and no target is claimed declared_validated.