x2_plus_1_no_real_root
plain-language theorem explainer
The real polynomial x² + 1 never vanishes. Anyone arguing that the 8-tick shift forces complexification cites this algebraic obstruction. The proof is a one-line term wrapper: strict positivity of x² + 1 yields non-equality to zero.
Claim. For every real number $x$, one has $x^{2} + 1 \neq 0$.
background
The module Complex Structure Forcing shows that the 8-tick cyclic shift on the ledger state space cannot be diagonalized over the reals, so passage to ℂ is algebraically forced rather than optional. The shift T satisfies T⁸ = I; its eigenvalues are the eighth roots of unity, among them ω² = i.
The immediate upstream fact is the strict inequality: for every real x, x² + 1 > 0 (equivalently, −1 has no real square root). That positivity is the obstruction. The present statement is the non-vanishing corollary used when one only needs “no real root,” not the sign.
Local setting (module doc): T7 forces the period-8 shift; the eigenvalue i has no real representative; therefore full diagonalization requires ℂ, with DFT-8 as the canonical unitary form.
proof idea
One-line term proof. For arbitrary real x, apply the upstream positivity lemma (x² + 1 > 0), then convert strict inequality to inequality-to-zero via ne_of_gt. No case split and no further algebra.
why it matters
This is the non-vanishing half of the core forcing step “the 8-tick forces ℂ.” Downstream, complexification_forced packages existence of the imaginary eigenvalue (at mode k=2) together with this universal real non-root statement. The complex_structure_certificate records it as imaginary_not_real alongside shift period-8, DFT-8 unitarity, and J-cost phase invariance.
In the forcing chain it supports the T7-to-canonical-carrier bridge: once the eight-tick equation is in hand, the carrier must admit the complex eigenstructure that real scalars cannot supply. Landmark link: T7 (eight-tick octave) plus the algebraic fact that x² + 1 has no real root closes the “complex Hilbert space from cost” gap named in the module registry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.