Grace/Cumulus/Complex/Nullstellensatz.g17

Open in Workbench Download source

Imports

FundamentalTheorem · Algebra.Polynomial.Nullstellensatz

Declarations

• complexes.weak_nullstellensatz theorem derivation
• complexes.unsatisfiable_iff_certificate theorem derivation

Source

1-- Weak Nullstellensatz over the concrete Dedekind-real complex field.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Complex.Nullstellensatz8import FundamentalTheorem9import Algebra.Polynomial.Nullstellensatz1011section ComplexPolynomials12notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)13variable (I G : Set)14notation ring P := ℂ[I]15hypothesis finite : Finite(I)16hypothesis generators : G ⊆ P1718theorem complexes.weak_nullstellensatz19  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, ℂ, G, v))20proof21  have closed := complexes.algebraically_closed22  exact polynomialIdeal.unit_iff_no_common_zero with *2324theorem complexes.unsatisfiable_iff_certificate25  shows (∃ terms, List(idealProducts(P, G), terms) ∧ P[1] = ringSum{idealProducts(P, G)}(polynomialAdd(I, ℂ), P[0], terms)) ↔ ¬(∃ v, PolynomialCommonZero(I, ℂ, G, v))26proof27  have closed := complexes.algebraically_closed28  exact polynomialIdeal.finite_certificate_iff_no_common_zero with *2930end ComplexPolynomials31