Grace/Cumulus/Complex/Cubic.g17

Open in Workbench Download source

Imports

QuadraticRoots · FundamentalTheorem · Field

Declarations

Source

1-- Cardano's solution of the cubic over the complex numbers: a depressed2-- cubic x³ + px + q has the root s + t whenever s³ + t³ = −q and 3st = −p,3-- such a pair exists for every p and q, and a general monic cubic is4-- depressed by the shift x = y − a/35-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Complex.Cubic11import QuadraticRoots12import FundamentalTheorem13import Field1415section Complexes16notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)17notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1819-- Closure of the complex operations, in the shape typecheck can use.20theorem complexAdd.closed (x y : Set)21  requires xIn : x ∈ ℂ22  requires yIn : y ∈ ℂ23  shows ℂ[x + y] ∈ ℂ24proof25  have ring := complexes.comm_ring26  have ordinary := IsCommRing.ring with ring27  exact IsRing.add_closed with ordinary, xIn, yIn2829theorem complexMul.closed (x y : Set)30  requires xIn : x ∈ ℂ31  requires yIn : y ∈ ℂ32  shows ℂ[x * y] ∈ ℂ33proof34  have ring := complexes.comm_ring35  have ordinary := IsCommRing.ring with ring36  exact IsRing.mul_closed with ordinary, xIn, yIn3738theorem complexNeg.closed (x : Set)39  requires xIn : x ∈ ℂ40  shows ℂ[-x] ∈ ℂ41proof42  have ring := complexes.comm_ring43  have ordinary := IsCommRing.ring with ring44  exact IsRing.neg_closed with ordinary, xIn4546theorem complexList.cons_nonempty (c : Set) (cs : List(ℂ))47  requires cIn : c ∈ ℂ48  shows c :: cs ≠ []49proof50  intro same51  have lengths : length{ℂ}(c :: cs) = length{ℂ}([])52    rw same53    rfl54  rw [length.cons, length.nil] at lengths55  have reversed : (0 : Nat) = succ(length{ℂ}(cs)) by cc56  exact Naturals.disjoint.zero.succ at length{ℂ}(cs) with reversed5758-- Inverses, zero divisors, and the nonzero constant three.59theorem complex.inverse_exists (x : Set)60  requires xIn : x ∈ ℂ61  requires nonzero : x ≠ ℂ[0]62  shows ∃ y ∈ ℂ, ℂ[x * y] = ℂ[1]63proof64  have field := complexes.is_field65  obtain ⟨y, inverse⟩ := IsField.inverse_exists with field, xIn, nonzero66  have yIn := inverse.right.left67  have law := inverse.right.right.right68  witness y69  exact ⟨yIn, law⟩7071theorem complex.zero_of_mul (x y : Set)72  requires xIn : x ∈ ℂ73  requires yIn : y ∈ ℂ74  requires nonzero : x ≠ ℂ[0]75  requires product : ℂ[x * y] = ℂ[0]76  shows y = ℂ[0]77proof78  have field := complexes.is_field79  have noZero := IsField.no_zero_divisors with field80  have forX := noZero with xIn81  have forY := forX with yIn82  have alternatives := forY with product83  cases alternatives with xZero | yZero84  . exfalso85    exact nonzero with xZero86  . exact yZero8788theorem complex.mul_nonzero (x y : Set)89  requires xIn : x ∈ ℂ90  requires yIn : y ∈ ℂ91  requires xNonzero : x ≠ ℂ[0]92  requires yNonzero : y ≠ ℂ[0]93  shows ℂ[x * y] ≠ ℂ[0]94proof95  intro product96  have yZero := complex.zero_of_mul with xIn, yIn, xNonzero, product97  exact yNonzero with yZero9899theorem complex.zero_of_cube (s : Set)100  requires sIn : s ∈ ℂ101  requires cube : ℂ[s * s * s] = ℂ[0]102  shows s = ℂ[0]103proof104  have alternatives : s = ℂ[0] ∨ s ≠ ℂ[0] by tauto105  cases alternatives with zero | nonzero106  . exact zero107  . have squareIn : ℂ[s * s] ∈ ℂ by typecheck108    have squareNonzero := complex.mul_nonzero with sIn, sIn, nonzero, nonzero109    exact complex.zero_of_mul at ℂ[s * s], s with sIn, squareNonzero, cube110111theorem complex.three_nonzero112  shows ℂ[3] ≠ ℂ[0]113proof114  have positive : 0 < 3 by arith115  exact complexNumeral.nonzero with positive116117-- Cube roots and roots of monic cubics, from the fundamental theorem.118theorem complex.cube_root (w : Set)119  requires wIn : w ∈ ℂ120  shows ∃ s ∈ ℂ, ℂ[s * s * s] = w121proof122  have negIn : ℂ[-w] ∈ ℂ by typecheck123  have zeroIn := complexZero.member124  have nonempty := complexList.cons_nonempty at ℂ[-w], [ℂ[0], ℂ[0]] with negIn125  obtain ⟨s, sIn, root⟩ := complexPolynomial.has_root with nonempty126  have list : List(ℂ, [ℂ[-w], ℂ[0], ℂ[0]]) by typecheck127  have tail1 : List(ℂ, [ℂ[0], ℂ[0]]) by typecheck128  have tail2 : List(ℂ, [ℂ[0]]) by typecheck129  have empty : List(ℂ, []) by typecheck130  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.cons, hornerAt.nil] at root131  witness s132  constructor133  . exact sIn134  . linear_combination root135136theorem cubic.root_exists (a b c : Set)137  requires aIn : a ∈ ℂ138  requires bIn : b ∈ ℂ139  requires cIn : c ∈ ℂ140  shows ∃ x ∈ ℂ, ℂ[x * x * x + a * (x * x) + b * x + c] = ℂ[0]141proof142  have nonempty := complexList.cons_nonempty at c, [b, a] with cIn143  obtain ⟨x, xIn, root⟩ := complexPolynomial.has_root with nonempty144  have list : List(ℂ, [c, b, a]) by typecheck145  have tail1 : List(ℂ, [b, a]) by typecheck146  have tail2 : List(ℂ, [a]) by typecheck147  have empty : List(ℂ, []) by typecheck148  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.cons, hornerAt.nil] at root149  witness x150  constructor151  . exact xIn152  . linear_combination root153154-- Cardano: s + t is a root of the depressed cubic when s³ + t³ = −q and155-- 3st = −p.156theorem cubic.cardano_root (p q s t : Set)157  requires pIn : p ∈ ℂ158  requires qIn : q ∈ ℂ159  requires sIn : s ∈ ℂ160  requires tIn : t ∈ ℂ161  requires cubes : ℂ[s * s * s + t * t * t] = ℂ[-q]162  requires product : ℂ[3 * (s * t)] = ℂ[-p]163  shows ℂ[(s + t) * (s + t) * (s + t) + p * (s + t) + q] = ℂ[0]164proof165  linear_combination cubes + (s + t) * product166167-- Such a pair exists: s is a cube root of a root of the resolvent quadratic168-- and t = −p/(3s), or p = 0 and t is a cube root of −q.169theorem cubic.cardano_pair (p q : Set)170  requires pIn : p ∈ ℂ171  requires qIn : q ∈ ℂ172  shows ∃ s ∈ ℂ, ∃ t ∈ ℂ, ℂ[s * s * s + t * t * t] = ℂ[-q] ∧ ℂ[3 * (s * t)] = ℂ[-p]173proof174  have zeroIn := complexZero.member175  have three := complex.three_nonzero176  have threeIn : ℂ[3] ∈ ℂ by typecheck177  have nine := complex.mul_nonzero with threeIn, threeIn, three, three178  have nineIn : ℂ[3 * 3] ∈ ℂ by typecheck179  have twentySeven := complex.mul_nonzero with nineIn, threeIn, nine, three180  have twentySevenIn : ℂ[3 * 3 * 3] ∈ ℂ by typecheck181  have pCubeIn : ℂ[p * p * p] ∈ ℂ by typecheck182  have constantIn : ℂ[-(3 * 3 * 3 * (p * p * p))] ∈ ℂ by typecheck183  have linearIn : ℂ[3 * 3 * 3 * q] ∈ ℂ by typecheck184  obtain ⟨W, WIn, Wroot⟩ := complexPolynomial.quadratic_root at ℂ[-(3 * 3 * 3 * (p * p * p))], ℂ[3 * 3 * 3 * q] with constantIn, linearIn185  have list : List(ℂ, [ℂ[-(3 * 3 * 3 * (p * p * p))], ℂ[3 * 3 * 3 * q]]) by typecheck186  have tail : List(ℂ, [ℂ[3 * 3 * 3 * q]]) by typecheck187  have empty : List(ℂ, []) by typecheck188  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.nil] at Wroot189  have resolvent : ℂ[W * W + 3 * 3 * 3 * q * W + -(3 * 3 * 3 * (p * p * p))] = ℂ[0]190    linear_combination Wroot191  obtain ⟨S, SIn, Scube⟩ := complex.cube_root at W with WIn192  have alternatives : S = ℂ[0] ∨ S ≠ ℂ[0] by tauto193  cases alternatives with SZero | SNonzero194  . have WZero : W = ℂ[0]195      rw SZero at Scube196      have zeroCube : ℂ[0 * 0 * 0] = ℂ[0] by ring197      rw zeroCube at Scube198      symm at Scube199      exact Scube200    have scaled : ℂ[3 * 3 * 3 * (p * p * p)] = ℂ[0]201      rw WZero at resolvent202      linear_combination -resolvent203    have pCubeZero := complex.zero_of_mul at ℂ[3 * 3 * 3], ℂ[p * p * p] with twentySevenIn, pCubeIn, twentySeven, scaled204    have pZero := complex.zero_of_cube at p with pIn, pCubeZero205    have negQIn : ℂ[-q] ∈ ℂ by typecheck206    obtain ⟨T, TIn, Tcube⟩ := complex.cube_root at ℂ[-q] with negQIn207    witness ℂ[0]208    constructor209    . exact zeroIn210    . witness T211      constructor212      . exact TIn213      . constructor214        . linear_combination Tcube215        . rw pZero216          ring217  . obtain ⟨v, vIn, third⟩ := complex.inverse_exists at ℂ[3] with threeIn, three218    obtain ⟨u, uIn, unit⟩ := complex.inverse_exists at S with SIn, SNonzero219    have WNonzero : W ≠ ℂ[0]220      intro WZero221      rw WZero at Scube222      apply SNonzero223      exact complex.zero_of_cube with SIn, Scube224    have scaleNonzero := complex.mul_nonzero with twentySevenIn, WIn, twentySeven, WNonzero225    have scaleIn : ℂ[3 * 3 * 3 * W] ∈ ℂ by typecheck226    have sIn : ℂ[S * v] ∈ ℂ by typecheck227    have tIn : ℂ[-(p * u)] ∈ ℂ by typecheck228    have excessIn : ℂ[(S * v) * (S * v) * (S * v) + (-(p * u)) * (-(p * u)) * (-(p * u)) + q] ∈ ℂ by typecheck229    have key : ℂ[(3 * 3 * 3 * W) * ((S * v) * (S * v) * (S * v) + (-(p * u)) * (-(p * u)) * (-(p * u)) + q)] = ℂ[0]230      linear_combination resolvent + (ℂ[3 * 3 * 3 * W * (v * v * v) + 3 * 3 * 3 * (p * p * p) * (u * u * u)]) * Scube + (ℂ[W * W * ((3 * v) * (3 * v) + 3 * v + 1)]) * third + (ℂ[-(3 * 3 * 3 * (p * p * p)) * ((S * u) * (S * u) + S * u + 1)]) * unit231    have excessZero := complex.zero_of_mul at ℂ[3 * 3 * 3 * W], ℂ[(S * v) * (S * v) * (S * v) + (-(p * u)) * (-(p * u)) * (-(p * u)) + q] with scaleIn, excessIn, scaleNonzero, key232    witness ℂ[S * v]233    constructor234    . exact sIn235    . witness ℂ[-(p * u)]236      constructor237      . exact tIn238      . constructor239        . linear_combination excessZero240        . linear_combination (-(p * (S * u))) * third + (-p) * unit241242-- Every depressed cubic has a root of Cardano's form.243theorem cubic.depressed_solution (p q : Set)244  requires pIn : p ∈ ℂ245  requires qIn : q ∈ ℂ246  shows ∃ x ∈ ℂ, ℂ[x * x * x + p * x + q] = ℂ[0] ∧ ∃ s ∈ ℂ, ∃ t ∈ ℂ, x = ℂ[s + t] ∧ ℂ[s * s * s + t * t * t] = ℂ[-q] ∧ ℂ[3 * (s * t)] = ℂ[-p]247proof248  obtain ⟨s, sIn, t, tIn, cubes, product⟩ := cubic.cardano_pair with pIn, qIn249  have root := cubic.cardano_root with pIn, qIn, sIn, tIn, cubes, product250  have sumIn : ℂ[s + t] ∈ ℂ by typecheck251  witness ℂ[s + t]252  constructor253  . exact sumIn254  . constructor255    . exact root256    . witness s257      constructor258      . exact sIn259      . witness t260        constructor261        . exact tIn262        . exact ⟨rfl, ⟨cubes, product⟩⟩263264-- The shift x = y − a·v with 3v = 1 depresses a monic cubic.265theorem cubic.depress (a b c v y : Set)266  requires aIn : a ∈ ℂ267  requires bIn : b ∈ ℂ268  requires cIn : c ∈ ℂ269  requires vIn : v ∈ ℂ270  requires yIn : y ∈ ℂ271  requires third : ℂ[3 * v] = ℂ[1]272  shows ℂ[(y + -(a * v)) * (y + -(a * v)) * (y + -(a * v)) + a * ((y + -(a * v)) * (y + -(a * v))) + b * (y + -(a * v)) + c] = ℂ[y * y * y + (b + -(a * a * v)) * y + (c + -(a * b * v) + 2 * (a * a * a * (v * v * v)))]273proof274  linear_combination (-(a * y * y) + a * a * v * y + -(a * a * a * v * v)) * third275276-- Cardano's solution of the general monic cubic.277theorem cubic.solution (a b c : Set)278  requires aIn : a ∈ ℂ279  requires bIn : b ∈ ℂ280  requires cIn : c ∈ ℂ281  shows ∃ x ∈ ℂ, ℂ[x * x * x + a * (x * x) + b * x + c] = ℂ[0] ∧ ∃ v ∈ ℂ, ∃ y ∈ ℂ, ℂ[3 * v] = ℂ[1] ∧ x = ℂ[y + -(a * v)] ∧ ∃ s ∈ ℂ, ∃ t ∈ ℂ, y = ℂ[s + t] ∧ ℂ[s * s * s + t * t * t] = ℂ[-(c + -(a * b * v) + 2 * (a * a * a * (v * v * v)))] ∧ ℂ[3 * (s * t)] = ℂ[-(b + -(a * a * v))]282proof283  have three := complex.three_nonzero284  obtain ⟨v, vIn, third⟩ := complex.inverse_exists with three285  have linearIn : ℂ[b + -(a * a * v)] ∈ ℂ by typecheck286  have constantIn : ℂ[c + -(a * b * v) + 2 * (a * a * a * (v * v * v))] ∈ ℂ by typecheck287  obtain ⟨y, yIn, root, s, sIn, t, tIn, shape, cubes, product⟩ := cubic.depressed_solution with288    linearIn, constantIn289  have identity := cubic.depress with aIn, bIn, cIn, vIn, yIn, third290  have xIn : ℂ[y + -(a * v)] ∈ ℂ by typecheck291  witness ℂ[y + -(a * v)]292  constructor293  . exact xIn294  . constructor295    . rw identity296      exact root297    . witness v298      constructor299      . exact vIn300      . witness y301        constructor302        . exact yIn303        . constructor304          . exact third305          . constructor306            . rfl307            . witness s308              constructor309              . exact sIn310              . witness t311                constructor312                . exact tIn313                . exact ⟨shape, ⟨cubes, product⟩⟩314315end Complexes316