Grace/Cumulus/Complex/QuadraticRoots.g17

Imports

Declarations

complexPolynomial.quadratic_root theorem derivation
complex.square_root theorem derivation
Source

1-- Quadratic roots from minimum attainment and four explicit square directions.2-- No use of the fundamental theorem of algebra or general root extraction.3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Complex.QuadraticRoots9import FTAReduction10import SquareDirections1112section Complexes13notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1415theorem complexPolynomial.quadratic_root (c d : Set)16  requires constant : c ∈ ℂ17  requires linear : d ∈ ℂ18  shows ∃ a ∈ ℂ, complexPolynomial([c, d])(a) = ℂ[0]19proof20  obtain ⟨a, aIn, least⟩ := complexPolynomial.global_minimum at c, [d] with *21  have function := complexPolynomial.function at [c, d] with *22  have valueIn := FunctionBetween.apply_closed at complexPolynomial([c, d]), ℂ, ℂ, a with *23  have root : complexPolynomial([c, d])(a) = ℂ[0]24    by_contra nonzero25    obtain ⟨n, nIn, ds, dsList, residualNonzero, degree, pairing⟩ := complexPolynomial.minimum_power_pairing at c, a, [d] with *26    have nNat := nat.omega.backward at n with *27    have empty : List(ℂ, []) by typecheck28    rw [length.cons, length.nil] at degree29    have small : n ≤ (1:N) by arith30    have residualFunction := complexPolynomial.function at ds with *31    have zeroIn := complexZero.member32    have residualIn := FunctionBetween.apply_closed at complexPolynomial(ds), ℂ, ℂ, ℂ[0] with *33    obtain ⟨u, uIn, negative⟩ := complexDot.small_power_direction at complexPolynomial([c, d])(a), complexPolynomial(ds)(ℂ[0]), n with *34    have nonnegative := pairing with u, uIn35    have ring := complexes.comm_ring36    have ordinary := IsCommRing.ring with ring37    have monoid := IsRing.multiplicative with ordinary38    have power := monoidPow.closed at ℂ, complexMul, complexOne, u, succ(n) with *39    have product := IsRing.mul_closed with ordinary, power, residualIn40    have firstPoint := complex.point with valueIn41    have secondPoint := complex.point with product42    have impossible := realLe.transitive_less with *43    have irrefl := realLess.irreflexive_on44    exact irrefl with realZero, impossible45  refine ⟨a, aIn, root⟩4647theorem complex.square_root (b : Set)48  requires member : b ∈ ℂ49  shows ∃ a ∈ ℂ, ℂ[a * a] = b50proof51  have ring := complexes.comm_ring52  have ordinary := IsCommRing.ring with ring53  have negative := IsRing.neg_closed with ordinary, member54  have zeroIn := complexZero.member55  obtain ⟨a, aIn, root⟩ := complexPolynomial.quadratic_root at ℂ[-b], ℂ[0] with *56  have list : List(ℂ, [ℂ[-b], ℂ[0]]) by typecheck57  have empty : List(ℂ, []) by typecheck58  have tail : List(ℂ, [ℂ[0]]) by typecheck59  have identity : ℂ[a * a] = ℂ[complexPolynomial([ℂ[-b], ℂ[0]])(a) + b]60    rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.nil]61    ring62  rw root at identity63  have cancel : ℂ[0 + b] = b by ring64  rw cancel at identity65  refine ⟨a, aIn, identity⟩6667end Complexes68