Scaled Reversion and Coefficient Congruence

Abstract

Scaled reversion proves Hanna’s coefficient congruences in OEIS A393856 and A393857.

Paul D. Hanna’s entries hanna2026a393856 and hanna2026a393857 specify A(x-xA(qx)/q)=x for q=4 and q=5 and conjecture that every positive-index coefficient is one modulo q+1. The theorem below treats every positive natural q. The separate parity conjecture in A393856 is not addressed.

PowerSeries(R) denotes formal power series over R, X is the indeterminate, coeff(n,f) extracts coefficient n, and mk builds a series from its coefficient function. The notation subst(f,g) means f composed with g. The constant-series embedding is C; rescale(r,f) multiplies coefficient n by r to the power n. All indices and q are natural numbers. Sequence values and the final remainders are integers. In the formulas G(q) denotes generatingSeries(q), and P denotes the auxiliary iteration specified with the definition of a.

Definition 1.1 (Stabilized integer coefficients).

$$\begin{array}{r}\forall q:\mathbb{N},\forall n:\mathbb{N},a\left(q,n\right)=\mathrm{coeff}\left(n,P\left(q,n+1\right)\right)\\ \forall q:\mathbb{N},P\left(q,0\right)=0\\ \forall q:\mathbb{N},\forall k:\mathbb{N},P\left(q,k+1\right)=P\left(q,k\right)+X-\mathrm{subst}\left(P\left(q,k\right),\mathrm{inner}\left(q,P\left(q,k\right)\right)\right)\end{array}$$

Formalization. D5/S1/Recurrence/Invariants/ScaledReversionCongruence.a (✓ std3).

Source. Repository-derived.

Commentary.

Starting with the zero series, the correction P+X-subst(P,inner(q,P)) gains one degree of agreement at each iteration. Coefficient n is read at iteration n+1, where it has stabilized.

Definition 1.2 (The integer generating series).

$$\forall q:\mathbb{N},G\left(q\right)=\mathrm{mk}\left(a\left(q\right)\right)$$

Formalization. D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generatingSeries (✓ std3).

Source. Repository-derived.

Commentary.

The coefficient function a(q) defines G(q) over the integers.

Definition 1.3 (The integral inner argument).

$$\forall q:\mathbb{N},\forall f:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\mathrm{inner}\left(q,f\right)=X-(X{)}^2\cdot \mathrm{mk}\left((n:\mathbb{N}\mapsto (\mathrm{cast}\left(q,\mathbb{Z}\right){)}^n\cdot \mathrm{coeff}\left(n+1,f\right))\right)$$

Formalization. D5/S1/Recurrence/Invariants/ScaledReversionCongruence.inner (✓ std3).

Source. Repository-derived.

Commentary.

The coefficient of degree n+2 subtracted from X is q to the power n times coefficient n+1 of f. This expression is integral and its constant and linear coefficients are zero and one, respectively.

Theorem 1.4 (Existence and the rescaling identity).

$$\begin{array}{r}\forall q:\mathbb{N},\\ (\mathrm{subst}\left(G\left(q\right),\mathrm{inner}\left(q,G\left(q\right)\right)\right)=X)\wedge ((\mathrm{constantCoeff}\left(G\left(q\right)\right)=0)\wedge ((\mathrm{coeff}\left(1,G\left(q\right)\right)=1)\wedge (C\left(\mathrm{cast}\left(q,\mathbb{Z}\right)\right)\cdot (X-\mathrm{inner}\left(q,G\left(q\right)\right))=X\cdot \mathrm{rescale}\left(\mathrm{cast}\left(q,\mathbb{Z}\right),G\left(q\right)\right))))\end{array}$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generating_equation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Agreement with arbitrarily late approximations proves the substitution equation. The first two coefficients follow from the initial iterations. The last conjunct identifies the inner argument by clearing the scalar denominator q; all four identities hold even at q=0.

Theorem 1.5 (Uniqueness by first difference).

$$\forall q:\mathbb{N},\forall f:\mathrm{PowerSeries}\left(\mathbb{Z}\right),(\mathrm{subst}\left(f,\mathrm{inner}\left(q,f\right)\right)=X)⟹f=G\left(q\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generating_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

If two series agree below degree d, their inner arguments agree below d+1. Substitution into a series beginning with X preserves the first nonzero coefficient of their difference. The correction therefore improves agreement by one degree. Induction proves uniqueness; no constant-coefficient assumption on f is needed.

Theorem 1.6 (The functional equation with division by q).

$$\forall q:\mathbb{N},(1\le q)⟹\mathrm{let}A=\mathrm{map}\left(\mathrm{intCastRingHom}\left(\mathbb{Q}\right),G\left(q\right)\right),\mathrm{subst}\left(A,X-C\left((\mathrm{cast}\left(q,\mathbb{Q}\right){)}^{-1}\right)\cdot X\cdot \mathrm{rescale}\left(\mathrm{cast}\left(q,\mathbb{Q}\right),A\right)\right)=X$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generating_equation_rational (✓ std3). ∎

Source. Repository-derived.

Commentary.

Map the integer equation to rational coefficients. For positive q, multiplication by its reciprocal converts the rescaling identity into the displayed inner argument. Thus the constructed series satisfies exactly A(x-xA(qx)/q)=x.

Theorem 1.7 (The parametric congruence).

$$\forall q:\mathbb{N},(1\le q)⟹\forall n:\mathbb{N},(1\le n)⟹a\left(q,n\right)\mathrm{mod}(q+1)=1$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/ScaledReversionCongruence.coeff_congruence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reduce the proved integer equation to ZMod(q+1), where q=-1. The series E=X/(1-X) has inner argument X/(1+X), and substituting this into E gives X. These identities follow by multiplying by unit denominators. The first-difference uniqueness proof works over every commutative ring, including ZMod(q+1), so the reduced generating series equals E. Its positive-degree coefficients are one. Since q+1 is at least two, one is the integer remainder.

Theorem 1.8 (The A393856 conjecture).

$$\forall n:\mathbb{N},(1\le n)⟹a\left(4,n\right)\mathrm{mod}5=1$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/ScaledReversionCongruence.hanna_a393856 (✓ std3). ∎

Resolves. Problems/oeis-a393856-scaled-reversion-mod-five (proved) by D5/S1/Recurrence/Invariants/ScaledReversionCongruence.hanna_a393856.

Citation. Paul D. Hanna (2026). OEIS A393856, G.f. satisfies A(x - xA(4x)/4) = x. URL: https://oeis.org/A393856.

Commentary.

Specializing the parametric theorem to q=4 proves the mod-five conjecture in hanna2026a393856 for every positive index.

Theorem 1.9 (The A393857 conjecture).

$$\forall n:\mathbb{N},(1\le n)⟹a\left(5,n\right)\mathrm{mod}6=1$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Invariants/ScaledReversionCongruence.hanna_a393857 (✓ std3). ∎

Resolves. Problems/oeis-a393857-scaled-reversion-mod-six (proved) by D5/S1/Recurrence/Invariants/ScaledReversionCongruence.hanna_a393857.

Citation. Paul D. Hanna (2026). OEIS A393857, G.f. satisfies A(x - xA(5x)/5) = x. URL: https://oeis.org/A393857.

Commentary.

Specializing the parametric theorem to q=5 proves the mod-six conjecture in hanna2026a393857 for every positive index.

References

• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.a
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.coeff_congruence
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generatingSeries
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generating_equation
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generating_equation_rational
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.generating_unique
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.hanna_a393856
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.hanna_a393857
• Truth anchor: D5/S1/Recurrence/Invariants/ScaledReversionCongruence.inner