no_real_root_x2_plus_1
plain-language theorem explainer
For every real x, x² + 1 is strictly positive, so −1 has no real square root. Recognition Science cites this as the algebraic obstruction that forces the 8-tick shift operator off the reals into ℂ. The proof is a one-line linear-arithmetic appeal to nonnegativity of squares.
Claim. For every real number $x$, one has $x^2 + 1 > 0$. Equivalently, there is no $x \in \mathbb{R}$ with $x^2 = -1$.
background
The module Complex Structure Forcing argues that the eight-tick cyclic shift $T$ on the ledger state space (period $T^8 = I$, from T7) cannot be diagonalized over $\mathbb{R}$. Its eigenvalues are the 8th roots of unity; in particular $\omega^2 = e^{i\pi/2} = i$ satisfies $i^2 + 1 = 0$.
Over the reals the same polynomial never vanishes: squares are nonnegative, so $x^2 + 1 \ge 1 > 0$. That elementary fact is the algebraic obstruction named in the module argument (step 3): without a real representative of $i$, $T$ has no full eigenbasis in $\mathbb{R}^8$, and complexification is forced rather than postulated.
Sibling material in the module identifies the DFT-8 eigenvalues, including the explicit match of mode 2 to $i$ and mode 6 to $-i$, which is where this positivity statement is consumed.
proof idea
Term-mode proof by linarith on the single fact sq_nonneg x: $x^2 \ge 0$ implies $x^2 + 1 \ge 1 > 0$. No Recognition-specific lemmas are invoked; the argument is pure real arithmetic.
why it matters
This is the concrete positivity lemma that the module's forcing chain needs at step 3: the eigenvalue $\omega^2 = i$ of the eight-tick shift has no real representative. The immediate corollary x2_plus_1_no_real_root rephrases it as non-vanishing, and both feed the complex-structure story that closes the registry gap "Complex Hilbert space from cost".
Downstream, the same module builds UnitaryEvolution (admissible evolutions preserve the DFT-8 inner product and do not increase total mode J-cost) and records Hamiltonian emergence from the small-deviation expansion $J(1+\varepsilon)=\varepsilon^2/2+O(\varepsilon^3)$. Without the real obstruction proved here, the passage from the cost axioms plus T7 to a complex Hilbert space with genuine unitarity would remain a modeling choice rather than a forced extension.
Framework landmarks: T7 (eight-tick octave), T5 (J-uniqueness underlying mode cost), and the module's dependence on T8 ($D=3$) for the ambient ledger geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.