Grace/Cumulus/Complex/Quartic.g17

Open in Workbench Download source

Imports

Cubic

Declarations

Source

1-- Ferrari's solution of the quartic over the complex numbers: a depressed2-- quartic y⁴ + py² + qy + r is a difference of two squares once m solves the3-- resolvent cubic, so its roots are roots of two quadratics, and a general4-- monic quartic is depressed by the shift x = y − a/45-- 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.Quartic11import Cubic1213section Complexes14notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)15notation ring R := (ℝ, realAdd, realZero, realNeg, realMul, realOne)1617theorem complex.two_nonzero18  shows ℂ[2] ≠ ℂ[0]19proof20  have positive : 0 < 2 by arith21  exact complexNumeral.nonzero with positive2223theorem complex.zero_of_square (s : Set)24  requires sIn : s ∈ ℂ25  requires square : ℂ[s * s] = ℂ[0]26  shows s = ℂ[0]27proof28  have alternatives : s = ℂ[0] ∨ s ≠ ℂ[0] by tauto29  cases alternatives with zero | nonzero30  . exact zero31  . exact complex.zero_of_mul with sIn, sIn, nonzero, square3233-- Ferrari's identity: with α² = 2m, αγ = q, and γ² = 4m² + 4pm + p² − 4r,34-- four times the depressed quartic is (2y² + p + 2m)² − (2αy − γ)².35theorem quartic.ferrari_identity (p q r m α γ y : Set)36  requires pIn : p ∈ ℂ37  requires qIn : q ∈ ℂ38  requires rIn : r ∈ ℂ39  requires mIn : m ∈ ℂ40  requires alphaIn : α ∈ ℂ41  requires gammaIn : γ ∈ ℂ42  requires yIn : y ∈ ℂ43  requires alphaSquare : ℂ[α * α] = ℂ[2 * m]44  requires gamma : ℂ[α * γ] = q45  requires gammaSquare : ℂ[γ * γ] = ℂ[2 * 2 * (m * m) + 2 * 2 * (p * m) + p * p + -(2 * 2 * r)]46  shows ℂ[2 * 2 * (y * y * y * y + p * (y * y) + q * y + r)] = ℂ[(2 * (y * y) + p + 2 * m) * (2 * (y * y) + p + 2 * m) + -((2 * (α * y) + -γ) * (2 * (α * y) + -γ))]47proof48  linear_combination (ℂ[2 * 2 * (y * y)]) * alphaSquare + (ℂ[-(2 * 2 * y)]) * gamma + gammaSquare4950-- A root of either Ferrari quadratic is a root of the depressed quartic.51theorem quartic.root_of_factor (p q r m α γ y : Set)52  requires pIn : p ∈ ℂ53  requires qIn : q ∈ ℂ54  requires rIn : r ∈ ℂ55  requires mIn : m ∈ ℂ56  requires alphaIn : α ∈ ℂ57  requires gammaIn : γ ∈ ℂ58  requires yIn : y ∈ ℂ59  requires alphaSquare : ℂ[α * α] = ℂ[2 * m]60  requires gamma : ℂ[α * γ] = q61  requires gammaSquare : ℂ[γ * γ] = ℂ[2 * 2 * (m * m) + 2 * 2 * (p * m) + p * p + -(2 * 2 * r)]62  requires factor : ℂ[2 * (y * y) + -(2 * (α * y)) + (p + 2 * m + γ)] = ℂ[0]63  shows ℂ[y * y * y * y + p * (y * y) + q * y + r] = ℂ[0]64proof65  have two := complex.two_nonzero66  have twoIn : ℂ[2] ∈ ℂ by typecheck67  have four := complex.mul_nonzero with two, two68  have fourIn : ℂ[2 * 2] ∈ ℂ by typecheck69  have quarticIn : ℂ[y * y * y * y + p * (y * y) + q * y + r] ∈ ℂ by typecheck70  have identity := quartic.ferrari_identity at p, q, r, m, α, γ, y with *71  have scaled : ℂ[2 * 2 * (y * y * y * y + p * (y * y) + q * y + r)] = ℂ[0]72    rw identity73    linear_combination (ℂ[2 * (y * y) + p + 2 * m + 2 * (α * y) + -γ]) * factor74  exact complex.zero_of_mul with four, scaled7576-- Every depressed quartic has a root given by Ferrari's method: m solves the77-- resolvent cubic, α² = 2m, γ = q/α (or γ² = p² − 4r when m = 0), and y78-- solves 2y² − 2αy + (p + 2m + γ) = 0.79theorem quartic.depressed_solution (p q r : Set)80  requires pIn : p ∈ ℂ81  requires qIn : q ∈ ℂ82  requires rIn : r ∈ ℂ83  shows ∃ y ∈ ℂ, ℂ[y * y * y * y + p * (y * y) + q * y + r] = ℂ[0] ∧ ∃ m ∈ ℂ, ∃ α ∈ ℂ, ∃ γ ∈ ℂ, ℂ[2 * 2 * 2 * (m * m * m) + 2 * 2 * 2 * (p * (m * m)) + 2 * (p * p * m) + -(2 * 2 * 2 * (r * m)) + -(q * q)] = ℂ[0] ∧ ℂ[α * α] = ℂ[2 * m] ∧ ℂ[α * γ] = q ∧ ℂ[2 * (y * y) + -(2 * (α * y)) + (p + 2 * m + γ)] = ℂ[0]84proof85  have zeroIn := complexZero.member86  have two := complex.two_nonzero87  have twoIn : ℂ[2] ∈ ℂ by typecheck88  have four := complex.mul_nonzero with two, two89  have fourIn : ℂ[2 * 2] ∈ ℂ by typecheck90  obtain ⟨h, hIn, half⟩ := complex.inverse_exists with two91  obtain ⟨e, eIn, quarter⟩ := complex.inverse_exists with four92  have linearIn : ℂ[p * p * e + -r] ∈ ℂ by typecheck93  have constantIn : ℂ[-(q * q * (e * h))] ∈ ℂ by typecheck94  obtain ⟨m, mIn, monic⟩ := cubic.root_exists at p, ℂ[p * p * e + -r], ℂ[-(q * q * (e * h))] with pIn, linearIn, constantIn95  have resolvent : ℂ[2 * 2 * 2 * (m * m * m) + 2 * 2 * 2 * (p * (m * m)) + 2 * (p * p * m) + -(2 * 2 * 2 * (r * m)) + -(q * q)] = ℂ[0]96    linear_combination (ℂ[2 * 2 * 2]) * monic + (ℂ[-(2 * (p * p * m)) + q * q * (2 * h)]) * quarter + (ℂ[q * q]) * half97  have data : ∃ α ∈ ℂ, ∃ γ ∈ ℂ, ℂ[α * α] = ℂ[2 * m] ∧ ℂ[α * γ] = q ∧ ℂ[γ * γ] = ℂ[2 * 2 * (m * m) + 2 * 2 * (p * m) + p * p + -(2 * 2 * r)]98    have alternatives : m = ℂ[0] ∨ m ≠ ℂ[0] by tauto99    cases alternatives with mZero | mNonzero100    . have squareZero : ℂ[q * q] = ℂ[0]101        rw mZero at resolvent102        linear_combination -resolvent103      have qZero := complex.zero_of_square with qIn, squareZero104      have discriminantIn : ℂ[p * p + -(2 * 2 * r)] ∈ ℂ by typecheck105      obtain ⟨γ, gammaIn, gammaRoot⟩ := complex.square_root with discriminantIn106      witness ℂ[0]107      constructor108      . exact zeroIn109      . witness γ110        constructor111        . exact gammaIn112        . constructor113          . rw mZero114            ring115          . constructor116            . rw qZero117              ring118            . rw mZero119              linear_combination gammaRoot120    . have twoMIn : ℂ[2 * m] ∈ ℂ by typecheck121      have twoMNonzero := complex.mul_nonzero with mIn, two, mNonzero122      obtain ⟨α, alphaIn, alphaSquare⟩ := complex.square_root with twoMIn123      have alphaNonzero : α ≠ ℂ[0]124        intro alphaZero125        rw alphaZero at alphaSquare126        apply twoMNonzero127        linear_combination -alphaSquare128      obtain ⟨w, wIn, unit⟩ := complex.inverse_exists with alphaIn, alphaNonzero129      have gammaIn : ℂ[q * w] ∈ ℂ by typecheck130      have scale : ℂ[2 * m * (w * w)] = ℂ[1]131        linear_combination (ℂ[-(w * w)]) * alphaSquare + (ℂ[α * w + 1]) * unit132      witness α133      constructor134      . exact alphaIn135      . witness ℂ[q * w]136        constructor137        . exact gammaIn138        . constructor139          . exact alphaSquare140          . constructor141            . linear_combination q * unit142            . linear_combination (ℂ[2 * 2 * (m * m) + 2 * 2 * (p * m) + p * p + -(2 * 2 * r)]) * scale + (ℂ[-(w * w)]) * resolvent143  obtain ⟨α, alphaIn, γ, gammaIn, alphaSquare, gamma, gammaSquare⟩ := data144  have quadraticConstantIn : ℂ[(p + 2 * m + γ) * h] ∈ ℂ by typecheck145  have quadraticLinearIn : ℂ[-α] ∈ ℂ by typecheck146  obtain ⟨y, yIn, yRoot⟩ := complexPolynomial.quadratic_root with quadraticConstantIn, quadraticLinearIn147  have list : List(ℂ, [ℂ[(p + 2 * m + γ) * h], ℂ[-α]]) by typecheck148  have tail : List(ℂ, [ℂ[-α]]) by typecheck149  have empty : List(ℂ, []) by typecheck150  rw [complexPolynomial.horner_value, hornerAt.cons, hornerAt.cons, hornerAt.nil] at yRoot151  have factor : ℂ[2 * (y * y) + -(2 * (α * y)) + (p + 2 * m + γ)] = ℂ[0]152    linear_combination (ℂ[2]) * yRoot + (ℂ[-(p + 2 * m + γ)]) * half153  have root := quartic.root_of_factor with *154  witness y155  constructor156  . exact yIn157  . constructor158    . exact root159    . witness m160      constructor161      . exact mIn162      . witness α163        constructor164        . exact alphaIn165        . witness γ166          constructor167          . exact gammaIn168          . exact ⟨resolvent, ⟨alphaSquare, ⟨gamma, factor⟩⟩⟩169170-- The shift x = y − a·e with 4e = 1 depresses a monic quartic.171theorem quartic.depress (a b c d e y : Set)172  requires aIn : a ∈ ℂ173  requires bIn : b ∈ ℂ174  requires cIn : c ∈ ℂ175  requires dIn : d ∈ ℂ176  requires eIn : e ∈ ℂ177  requires yIn : y ∈ ℂ178  requires quarter : ℂ[2 * 2 * e] = ℂ[1]179  shows ℂ[(y + -(a * e)) * (y + -(a * e)) * (y + -(a * e)) * (y + -(a * e)) + a * ((y + -(a * e)) * (y + -(a * e)) * (y + -(a * e))) + b * ((y + -(a * e)) * (y + -(a * e))) + c * (y + -(a * e)) + d] = ℂ[y * y * y * y + (b + -((3 + 3) * (a * a * (e * e)))) * (y * y) + (c + -(2 * (a * b * e)) + 2 * 2 * 2 * (a * a * a * (e * e * e))) * y + (d + -(a * c * e) + a * a * b * (e * e) + -(3 * (a * a * a * a * (e * e * e * e))))]180proof181  linear_combination (ℂ[-(a * ((y + -(a * e)) * (y + -(a * e)) * (y + -(a * e))))]) * quarter182183-- Ferrari's solution of the general monic quartic.184theorem quartic.solution (a b c d : Set)185  requires aIn : a ∈ ℂ186  requires bIn : b ∈ ℂ187  requires cIn : c ∈ ℂ188  requires dIn : d ∈ ℂ189  shows ∃ x ∈ ℂ, ℂ[x * x * x * x + a * (x * x * x) + b * (x * x) + c * x + d] = ℂ[0] ∧ ∃ e ∈ ℂ, ∃ y ∈ ℂ, ℂ[2 * 2 * e] = ℂ[1] ∧ x = ℂ[y + -(a * e)] ∧ ℂ[y * y * y * y + (b + -((3 + 3) * (a * a * (e * e)))) * (y * y) + (c + -(2 * (a * b * e)) + 2 * 2 * 2 * (a * a * a * (e * e * e))) * y + (d + -(a * c * e) + a * a * b * (e * e) + -(3 * (a * a * a * a * (e * e * e * e))))] = ℂ[0]190proof191  have two := complex.two_nonzero192  have four := complex.mul_nonzero with two, two193  obtain ⟨e, eIn, quarter⟩ := complex.inverse_exists with four194  have pIn : ℂ[b + -((3 + 3) * (a * a * (e * e)))] ∈ ℂ by typecheck195  have qIn : ℂ[c + -(2 * (a * b * e)) + 2 * 2 * 2 * (a * a * a * (e * e * e))] ∈ ℂ by typecheck196  have rIn : ℂ[d + -(a * c * e) + a * a * b * (e * e) + -(3 * (a * a * a * a * (e * e * e * e)))] ∈ ℂ by typecheck197  obtain ⟨y, yIn, root, rest⟩ := quartic.depressed_solution with pIn, qIn, rIn198  have identity := quartic.depress with aIn, bIn, cIn, dIn, eIn, yIn, quarter199  have xIn : ℂ[y + -(a * e)] ∈ ℂ by typecheck200  witness ℂ[y + -(a * e)]201  constructor202  . exact xIn203  . constructor204    . rw identity205      exact root206    . witness e207      constructor208      . exact eIn209      . witness y210        constructor211        . exact yIn212        . exact ⟨quarter, ⟨rfl, root⟩⟩213214end Complexes215