OEIS A392208: Parity Has Period Three

Abstract

The implicit exponential generating function of OEIS A392208 has coefficient parity of period three.

OEIS A392208 (entry dated 2026-01-24) supplies the defining equation A’(x) = exp(A(x) A’(x)^3) and the conjecture that a(n) is even if and only if 3 divides n for n >= 1. The entry supplies context rather than the repository’s strengthened integer recurrence, ODE uniqueness theorem, period-three proof, or theorem quantified over every integer sequence satisfying the equation.

Definition 1.1 (Binomial convolution).

$$\forall R:Type,(\mathrm{CommSemiring}\left(R\right)),f:(\mathbb{N}\to R),g:(\mathbb{N}\to R),n:\mathbb{N},\mathrm{egfMul}\left(f,g,n\right)=\sum _{k\in \mathrm{range}\left(n+1\right)}(\mathrm{choose}\left(n,k\right)\cdot f\left(k\right)\cdot g\left(n-k\right))$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfMul (✓ std3).

Source. Repository-derived.

Commentary.

OEIS A392208 (2026-01-24) uses exponential generating functions. This definition is the binomial convolution whose nth value is the displayed finite sum; range(n+1) contains exactly 0 through n, and natural subtraction in n-k is truncated at zero.

Definition 1.2 (Iterated binomial convolution).

$$\forall R:Type,(\mathrm{CommSemiring}\left(R\right)),f:(\mathbb{N}\to R),n:\mathbb{N},(\mathrm{egfPow}\left(f,0,n\right)=\mathrm{ite}\left(n=0,1,0\right))\wedge (\forall m:\mathbb{N},\mathrm{egfPow}\left(f,m+1,n\right)=\mathrm{egfMul}\left(f,\mathrm{egfPow}\left(f,m\right),n\right))$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfPow (✓ std3).

Source. Repository-derived.

Commentary.

OEIS A392208 (2026-01-24) contains the third and fifth powers of the derivative. The zero convolution power is the sequence that is one at zero and zero elsewhere; the successor clause is left binomial convolution by f.

Definition 1.3 (Recursive next-coefficient expression).

$$\forall s:(\mathbb{N}\to \mathbb{Z}),n:\mathbb{N},\mathrm{recurrenceRhs}\left(s,n\right)=\mathrm{egfPow}\left((j\mapsto s\left(j+1\right)),5,n\right)+3\cdot \mathrm{egfMul}\left(\mathrm{egfMul}\left(s,\mathrm{egfPow}\left((j\mapsto s\left(j+1\right)),3\right)\right),(j\mapsto \mathrm{ite}\left(j<n,s\left(j+2\right),0\right)),n\right)$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.recurrenceRhs (✓ std3).

Source. Repository-derived.

Commentary.

The repository defines this integer expression to append the next triangular recurrence coefficient. OEIS A392208 (2026-01-24) supplies context through its defining equation; this explicit integer recurrence expression is a repository strengthening beyond the OEIS wording.

Definition 1.4 (Finite recursive coefficient table).

$$\begin{array}{r}table:(\mathbb{N}\to \mathrm{List}\left(\mathbb{Z}\right))\\ \mathrm{table}\left(0\right)=[0,1]\\ \forall n:\mathbb{N},\mathrm{table}\left(n+1\right)=\mathrm{append}\left(\mathrm{table}\left(n\right),[\mathrm{recurrenceRhs}\left((k\mapsto \mathrm{getD}\left(\mathrm{table}\left(n\right),k,0\right)),n\right)]\right)\end{array}$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.table (✓ std3).

Source. Repository-derived.

Commentary.

The public table starts with the exact list [0,1]. At the successor step it appends exactly one value of recurrenceRhs, evaluated on getD of the preceding table with default zero. This repository object makes the definition of a self-contained.

Definition 1.5 (The recurrence-defined integer sequence).

$$\begin{array}{r}a:\mathbb{N}\to \mathbb{Z}\\ a\left(0\right)=0\\ a\left(1\right)=1\\ \forall n:\mathbb{N},a\left(n+2\right)=\mathrm{getD}\left(\mathrm{table}\left(n+1\right),n+2,0\right)\end{array}$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a (✓ std3).

Source. Repository-derived.

Commentary.

OEIS A392208 (2026-01-24) supplies the initial coefficients 0,1 for A itself. The public finite table starts at [0,1], appends the triangular recurrence value at every step, and getD returns zero only outside that table; the displayed clauses are the literal definition of a. The next theorem exports its recurrence without the auxiliary table.

Theorem 1.6 (Initial residues modulo two).

$$(\mathrm{cast}\left(a\left(0\right),\mathrm{ZMod}\left(2\right)\right)=0)\wedge \left((\mathrm{cast}\left(a\left(1\right),\mathrm{ZMod}\left(2\right)\right)=1)\wedge (\mathrm{cast}\left(a\left(2\right),\mathrm{ZMod}\left(2\right)\right)=1)\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.initial_residues_mod_two (✓ std3). ∎

Source. Repository-derived.

Commentary.

The recurrence-defined sequence has the right-associated initial residue triple (0,1,1) in ZMod(2), exactly as named in the candidate theorem atom.

Theorem 1.7 (Triangular integer recurrence).

$$\forall n:\mathbb{N},a\left(n+2\right)=\mathrm{egfPow}\left((j\mapsto a\left(j+1\right)),5,n\right)+3\cdot \mathrm{egfMul}\left(\mathrm{egfMul}\left(a,\mathrm{egfPow}\left((j\mapsto a\left(j+1\right)),3\right)\right),(j\mapsto a\left(j+2\right)),n\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a_recurrence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The ODE obtained from OEIS A392208 (2026-01-24) gives this integer recurrence. The apparent top second-derivative coefficient in the second summand vanishes because a(0)=0, so the recurrence is triangular with leading coefficient one.

Theorem 1.8 (Period three modulo two).

$$\forall n:\mathbb{N},\mathrm{ModEqZ}\left(2,a\left(n+3\right),a\left(n\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.recurrence_coefficient_period_three (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the recurrence-defined sequence attached to OEIS A392208 (2026-01-24), every coefficient three places later is congruent modulo two. ModEqZ denotes integer congruence, not a cast or rational equality.

Definition 1.9 (Implicit exponential power-series equation).

$$\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{ExpDefines}\left(A\right)=\left((\mathrm{constantCoeff}\left(A\right)=0)\wedge (\mathrm{DQ}\left(A\right)=\mathrm{subst}\left(\mathrm{expQ}\left(\right),A\cdot (\mathrm{DQ}\left(A\right){)}^3\right))\right)$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.ExpDefines (✓ std3).

Source. Repository-derived.

Commentary.

This is the exact formal power-series equation from OEIS A392208 (2026-01-24), together with A(0)=0. DQ is formal differentiation over the rationals, expQ is the rational formal exponential series, and subst is formal substitution.

Theorem 1.10 (The implicit equation implies the ODE).

$$\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{ExpDefines}\left(A\right))\Rightarrow \left(1-3\cdot A\cdot (\mathrm{DQ}\left(A\right){)}^3\right)\cdot \mathrm{DQ}\left(\mathrm{DQ}\left(A\right)\right)=(\mathrm{DQ}\left(A\right){)}^5$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.exp_definition_implies_ode (✓ std3). ∎

Source. Repository-derived.

Commentary.

Differentiating the equation in OEIS A392208 (2026-01-24) with the formal substitution chain rule yields the displayed denominator-free ODE. No analytic convergence is assumed.

Definition 1.11 (Rational exponential generating series).

$$\forall s:(\mathbb{N}\to \mathbb{Q}),\mathrm{egfSeries}\left(s\right)=\mathrm{mk}\left((n\mapsto \frac{s\left(n\right)}{(n)!})\right)$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfSeries (✓ std3).

Source. Repository-derived.

Commentary.

For OEIS A392208 (2026-01-24), the ordinary coefficient of x^n is s(n)/n!. The displayed fraction is rational division; no natural-number or integer division is used.

Theorem 1.12 (The first derivative has constant coefficient one).

$$\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{ExpDefines}\left(A\right))\Rightarrow \mathrm{constantCoeff}\left(\mathrm{DQ}\left(A\right)\right)=1$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.exp_definition_derivative_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

Evaluating the defining equation at constant coefficient zero yields A’(0)=1, which the identification of the OEIS-defined sequence with the recurrence uses.

Definition 1.13 (Coefficient form of the ODE).

$$\forall s:(\mathbb{N}\to \mathbb{Q}),\mathrm{EgfOde}\left(s\right)=\forall n:\mathbb{N},s\left(n+2\right)=\mathrm{egfPow}\left((j\mapsto s\left(j+1\right)),5,n\right)+3\cdot \mathrm{egfMul}\left(\mathrm{egfMul}\left(s,\mathrm{egfPow}\left((j\mapsto s\left(j+1\right)),3\right)\right),(j\mapsto s\left(j+2\right)),n\right)$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.EgfOde (✓ std3).

Source. Repository-derived.

Commentary.

This is the coefficient recurrence for the ODE derived from OEIS A392208 (2026-01-24), written over rational sequences using the public binomial convolution operations.

Theorem 1.14 (Uniqueness of the coefficient ODE).

$$\forall s:(\mathbb{N}\to \mathbb{Q}),t:(\mathbb{N}\to \mathbb{Q}),((s\left(0\right)=0)\wedge \left((s\left(1\right)=1)\wedge \left((t\left(0\right)=0)\wedge \left((t\left(1\right)=1)\wedge \left((\mathrm{EgfOde}\left(s\right))\wedge (\mathrm{EgfOde}\left(t\right))\right)\right)\right)\right))\Rightarrow s=t$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfOde_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

For OEIS A392208 (2026-01-24), two rational coefficient sequences satisfying the same triangular ODE recurrence and initial coefficients 0,1 agree everywhere. Strong induction uses the vanished top coefficient in the nonlinear term.

Definition 1.15 (Exact OEIS integer-sequence predicate).

$$\forall s:(\mathbb{N}\to \mathbb{Z}),\mathrm{OEISDefines}\left(s\right)=\left((\mathrm{constantCoeff}\left(\mathrm{egfSeries}\left((n\mapsto \mathrm{castQ}\left(s\left(n\right)\right))\right)\right)=0)\wedge (\mathrm{DQ}\left(\mathrm{egfSeries}\left((n\mapsto \mathrm{castQ}\left(s\left(n\right)\right))\right)\right)=\mathrm{subst}\left(\mathrm{expQ}\left(\right),\mathrm{egfSeries}\left((n\mapsto \mathrm{castQ}\left(s\left(n\right)\right))\right)\cdot (\mathrm{DQ}\left(\mathrm{egfSeries}\left((n\mapsto \mathrm{castQ}\left(s\left(n\right)\right))\right)\right){)}^3\right))\right)$$

Formalization. D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.OEISDefines (✓ std3).

Source. Repository-derived.

Commentary.

This expands the defining expression from OEIS A392208 (2026-01-24): castQ maps every integer coefficient to the rationals before forming its EGF, whose constant coefficient is zero and whose derivative is the substituted exponential shown here.

Theorem 1.16 (The recurrence sequence satisfies the OEIS equation).

$$\mathrm{OEISDefines}\left(a\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a_oeisDefines (✓ std3). ∎

Source. Repository-derived.

Commentary.

The named witness connects the repository sequence a to the exact generating-function predicate from OEIS A392208 (2026-01-24). Its proof follows the integer recurrence through the rational coefficient ODE and reconstructs the implicit exponential equation.

Theorem 1.17 (The OEIS equation determines the recurrence sequence).

$$\forall s:(\mathbb{N}\to \mathbb{Z}),(\mathrm{OEISDefines}\left(s\right))\Rightarrow s=a$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.oeis_defined_eq_recurrence (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every integer sequence satisfying the exact equation of OEIS A392208 (2026-01-24) equals a. The proof derives the ODE and A’(0)=1, applies triangular uniqueness over the rationals, and then recovers equality of the integer coefficients.

Theorem 1.18 (Every OEIS-defined sequence has period three modulo two).

$$\forall s:(\mathbb{N}\to \mathbb{Z}),(\mathrm{OEISDefines}\left(s\right))\Rightarrow \forall n:\mathbb{N},\mathrm{ModEqZ}\left(2,s\left(n+3\right),s\left(n\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.oeis_coefficient_period_three (✓ std3). ∎

Source. Repository-derived.

Commentary.

Identification with a transfers the kernel-verified period-three congruence to every integer sequence satisfying OEIS A392208 (2026-01-24).

Theorem 1.19 (Every OEIS-defined sequence satisfies the parity law).

$$\forall s:(\mathbb{N}\to \mathbb{Z}),(\mathrm{OEISDefines}\left(s\right))\Rightarrow \forall n:\mathbb{N},(1\le n)\Rightarrow (\mathrm{Even}\left(s\left(n\right)\right))\iff (3\mid n)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.parity_conjecture_of_oeisDefines (✓ std3). ∎

Source. Repository-derived.

Commentary.

This public companion transfers the parity theorem for a to every integer sequence satisfying the exact OEIS A392208 (2026-01-24) equation. It remains conditional on that defining predicate and is distinct from the unconditional atom anchor.

Theorem 1.20 (The A392208 parity conjecture).

$$\forall n:\mathbb{N},(1\le n)\Rightarrow (\mathrm{Even}\left(a\left(n\right)\right))\iff (3\mid n)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a392208_parity_conjecture (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the unconditional atom clause for the repository sequence a: at every positive index, a(n) is even if and only if three divides n. Its live proof specializes the general OEIS-defined parity theorem with the named witness a_oeisDefines.

References

• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.EgfOde
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.ExpDefines
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.OEISDefines
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a392208_parity_conjecture
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a_oeisDefines
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.a_recurrence
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfMul
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfOde_unique
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfPow
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.egfSeries
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.exp_definition_derivative_zero
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.exp_definition_implies_ode
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.initial_residues_mod_two
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.oeis_coefficient_period_three
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.oeis_defined_eq_recurrence
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.parity_conjecture_of_oeisDefines
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.recurrenceRhs
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.recurrence_coefficient_period_three
• Truth anchor: D5/S1/Recurrence/Parity/ExponentialImplicitParityPeriodThree.table