Metadata

slug: hefg-a232695
bibkey: hanna2013derivativesubstitutioncongruences
doi: null
url: https://oeis.org/A232695
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/Residue/HannaA232695Congruences.result

Hanna’s derivative-substitution congruences for A232695

Problem

Paul D. Hanna’s OEIS A232695 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 A232695 E.g.f. A(x) satisfies: A’(x) = A(x*A’(x)^5) with A(0)=1. %C A232695 CONJECTURES. %C A232695 a(n) == 1 (mod 5) for n>=0. %C A232695 a(n) == 0 (mod 2) for n>=4.

Record	Formal equation	Nominated congruences	Settling declaration
A232695	$A^{'} (x) = A (x (A^{'} (x))^{5})$	$5 ∣ a_{n} - 1$ for every $n \geq 0$ ; $2 ∣ a_{n}$ for $n \geq 4$	`HannaA232695Congruences.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))^{5})$ and $A (0) = 1$	`IsSolution` in `HannaA232695Congruences`	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.
$5 ∣ a_{n} - 1$ for all $n \geq 0$	The first divisibility conjunct in `claim`	The all-index residue is literal.
$2 ∣ a_{n}$ for $n \geq 4$	The second divisibility conjunct in `claim`	The threshold and modulus are literal.

Motivation

The preregistration #21486 supplies the source conventions and literature screen for A232695. 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.

Gap

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

Route

The shared machinery constructs the unique integral coefficient recurrence, transports coefficient congruences from an integral approximate solution, and cancels integral unit powers. A232695 uses $[1, 1, 1, 11]$ modulo $2$ and the exponential residual modulo $5$ ; the general divisor-of- $k$ exponential transfer is available.

Falsifier

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.

Evidence

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-a232695, Proved) on this dossier: A232695 resolves #21486. 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 A232695, 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 A232695 $a_{3} = 11$ . Each predecessor fails the respective divisibility cutoff lowered by one.

Triage

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 A232695, indices $0 \dots 300$ , and iteration degree 12. Uniform extension beyond that finite range is supplied by the kernel-checked result, not by this computation.
Cutoff predecessors A232695 $a_{3} = 11$	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.
Exponential residual sum is divisible by $m$ after subtracting $1$ whenever $m ∣ k$	Proved; kernel-checked	`HannaEGFMachinery.expSum_mod` and `exp_residual`. The statement is coefficientwise for formal series.
A232695 uses $[1, 1, 1, 11]$ modulo $2$ and the exponential residual modulo $5$ ; the general divisor-of- $k$ exponential transfer is available	Proved; kernel-checked	`HannaA232695Congruences.result` and the shared exponential residual declarations. The additional $2^{k}$ cutoff family is outside this module.

Literature status

The source and revision history for A232695 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.

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.

Keyboard shortcuts

trureturing — Discovering truth