Trisection
Abstract
Exact coefficient extraction separates all three residue classes at every natural index over any commutative ring.
Exact coefficient extraction separates all three residue classes at every natural index over any commutative ring.
Theorem 1.1 (coeff_shift_expand_three).
Lean statement: D5/S3/Combinatorics/PowerSeries/Trisection.coeff_shift_expand_three
Proof. Machine-checked in Lean as D5/S3/Combinatorics/PowerSeries/Trisection.coeff_shift_expand_three (✓ std3). ∎
Source. Repository-derived.
Commentary.
Coeff shift expand three.
Theorem 1.2 (coeff_three_components).
Lean statement: D5/S3/Combinatorics/PowerSeries/Trisection.coeff_three_components
Proof. Machine-checked in Lean as D5/S3/Combinatorics/PowerSeries/Trisection.coeff_three_components (✓ std3). ∎
Source. Repository-derived.
Commentary.
A formal dissection determines each progression at every natural degree.
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.