ExpandingRecurrence
Abstract
A homogeneous positive-degree expanding recurrence has only the zero formal power series solution over any commutative ring.
A homogeneous positive-degree expanding recurrence has only the zero formal power series solution over any commutative ring.
Theorem 1.1 (eq_zero_of_mul_eq_X_expand).
Lean statement: D5/S3/Combinatorics/PowerSeries/ExpandingRecurrence.eq_zero_of_mul_eq_X_expand
Proof. Machine-checked in Lean as D5/S3/Combinatorics/PowerSeries/ExpandingRecurrence.eq_zero_of_mul_eq_X_expand (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every coefficient of a homogeneous expanding recurrence vanishes over any commutative ring.
Statements and proof dependencies come from the exact scoped Lean report. This generic coefficient argument uses the pinned Mathlib power-series APIs and has no assumed analytic convergence or cubic theta identity. No literature priority, worldwide absence, journal-typeset inspection, CI or original-problem acceptance is certified by this document.