complex_is_unique
The declaration asserts that the complex numbers are algebraically closed. Researchers deriving quantum wavefunctions or phasor representations from discrete phase cycles would cite it to justify the appearance of i. The proof is a one-line term wrapper that invokes Mathlib's implementation of the Fundamental Theorem of Algebra.
claimThe field of complex numbers is algebraically closed: every non-constant polynomial with coefficients in $ℂ$ possesses at least one root in $ℂ$.
background
Recognition Science obtains complex numbers from the eight-tick phase structure. The upstream definition Phase := Fin 8 encodes the discrete cycle whose elements represent 45° rotations. These phases must support additive composition and interference, which forces a two-dimensional representation equivalent to the complex plane. The module MATH-004 states that rotations cannot be realized in one dimension and therefore the ledger requires $ℂ$. Upstream results on collision-free structures and empirical programs supply the surrounding ledger constraints but do not alter the algebraic statement.
proof idea
The proof is a one-line wrapper that applies the Mathlib constant Complex.isAlgClosed, which encodes the Fundamental Theorem of Algebra.
why it matters in Recognition Science
The result supplies the algebraic closure property required by the 8-tick octave (T7) once phases are introduced. It feeds the necessity argument in MATH-004 that complex amplitudes appear in quantum mechanics and electromagnetism because the ledger cycle is cyclic. No downstream uses are recorded, leaving the physical interpretation of the imaginary unit as an open bridge to the forcing chain.
scope and limits
- Does not derive algebraic closure from the 8-tick axioms alone.
- Does not construct explicit roots for given polynomials.
- Does not address the physical meaning of the imaginary unit.
- Does not prove uniqueness of $ℂ$ up to isomorphism.
formal statement (Lean)
227theorem complex_is_unique :
228 -- ℂ is algebraically closed: every polynomial over ℂ has a root in ℂ
229 IsAlgClosed ℂ := Complex.isAlgClosed
proof body
Term-mode proof.
230
231/-! ## The RS Interpretation -/
232
233/-- In RS, complex numbers arise because:
234
235 1. The ledger has 8 ticks (discrete)
236 2. Ticks are phases (cyclic)
237 3. Phase differences matter (interference)
238 4. Phase is additive under composition
239 5. The unique structure satisfying these is ℂ
240
241 Complex numbers aren't a human invention - they're forced by nature! -/