Opposite-Root Symmetry at Odd Order
Abstract
Odd-index plus-recurrence polynomials are even after complexification.
Theorem 1.1 (Odd-index parity).
Lean statement: D5/S3/Arith/Primes/FibonacciRecurrencePolynomialOddParity.odd_recurrence_polynomial_even
Proof. Machine-checked in Lean as D5/S3/Arith/Primes/FibonacciRecurrencePolynomialOddParity.odd_recurrence_polynomial_even (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural r and complex z, evaluating the complexification of the recurrence polynomial at index 2r+1 at -z gives the same value as evaluating it at z. Thus complex roots occur in opposite pairs.