complex_is_unique
plain-language theorem explainer
The theorem asserts algebraic closure of the complex numbers, so every non-constant polynomial over ℂ has a root in ℂ. Researchers deriving quantum wavefunctions or Fourier transforms from discrete cyclic ledgers would cite it to justify the appearance of ℂ. The proof is a direct term reference to Mathlib's established result on the Fundamental Theorem of Algebra.
Claim. The field of complex numbers is algebraically closed: every non-constant polynomial with coefficients in ℂ has at least one root in ℂ.
background
Module MATH-004 derives the necessity of complex numbers from the 8-tick phase structure of the Recognition Science ledger. The 8-tick phase space is given by Phase := Fin 8, the set of phases 0 through 7. Upstream results include the Phase abbrev in ChurchTuringPhysicsStructure, which states 'The 8-tick phase space: phases 0 through 7', and the corresponding definition in EightTick.Hypotheses.
proof idea
The proof is a one-line term wrapper that applies Complex.isAlgClosed from Mathlib.
why it matters
This supplies the algebraic closure property required for the 8-tick phases e^{iπk/4} in the module's derivation of complex necessity (T7 eight-tick octave). It grounds the claim that rotations in the plane force ℂ for interference and composition in the ledger. No downstream results are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.