bibkey: hanna2026a393856
authors: Paul D. Hanna
year: 2026
title: OEIS A393856, G.f. satisfies A(x - x*A(4*x)/4) = x
doi: null
url: https://oeis.org/A393856
claim: "G.f. A(x) satisfies: A( x - x*A(4*x)/4 ) = x. Conjecture: a(n) == 1 (mod 5) for n >= 1."
strata_touched:
  - D5/S1/Recurrence/Invariants/ScaledReversionCongruence
license: citation-only
triage: anchor

OEIS A393856

Paul D. Hanna’s entry of March 11, 2026 defines the generating function by A( x - x*A(4*x)/4 ) = x and conjectures a(n) == 1 (mod 5) for n >= 1. The Lean module constructs the unique integer solution, proves the functional equation, and proves the congruence as the case q = 4 of a parametric theorem. The entry’s separate conjecture about odd coefficients is not stated as a theorem anywhere, and it does not need to be: it already follows from frozen content filed under a different entry. Reducing the defining equation modulo two, the scaling factor four vanishes and every term with j >= 2 drops, leaving B(X + X^2) = X, hence B + B^2 = X. The frozen D5/S3/Arith/ArtinSchreierTracePowersOfTwo proves S^2 + S = X for its own series S; the two constant coefficients are zero and one, so in characteristic two B + 1 and S are roots of the same equation with equal constant coefficient, and eq_of_square_add_eq_square_add identifies them. Adding one changes no positive coefficient, so reducedSeries_eq_artinSeries together with a396808_first_conjecture gives the odd-coefficient classification directly.

The same reduced object closes two neighbouring entries, so they are recorded here rather than in notes of their own. OEIS A195194, the nested reversion Inv(x - x*Inv(x - 2*x*Inv(x - 3*x*...))), conjectures the same power-of-two parity support; modulo two its multipliers alternate, the layer with multiplier two reduces to X, the tower collapses, and B + B^2 = X appears again. The frozen D5/S3/Arith/SelfReferentialInverseSeriesParity.unit_constant_support classifies that object, and ZMod.intCast_eq_one_iff_odd converts the coefficient statement into the oddness predicate. Its first terms are 1, 1, 4, 29, 312, 4528, with odd indices through fifty exactly 1, 2, 4, 8, 16, 32.

More generally the whole even-scaling branch of this reversion family shares the one reduced object: modulo two, A(x - x*A(k*x)/k) = x loses every term with j >= 2 whenever k is even, so k = 4 and k = 6 give the same equation. The integer sequences differ at once — a(5) is 8466 for k = 4 and 71744 for k = 6 — while the reductions modulo two agree at every index through forty. A distinct A-number in that branch is therefore not a distinct target.

Writing that chain out as a new Lean declaration would be a second source for a truth the graph already carries, so it is recorded here instead.

Verified locator

• URL: https://oeis.org/A393856