NullstellensatzReduction

The conditional weak-Nullstellensatz reduction; residue surjectivity remains a hypothesis

Open in Workbench View on GitHub

1-- The conditional weak-Nullstellensatz reduction; residue surjectivity remains a hypothesis.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module NullstellensatzReduction8import Grace.Cumulus.Algebra.Polynomial.NullstellensatzReduction910section Residues11variable (I A add zero neg mul one G : Set)12notation ring R := (A, add, zero, neg, mul, one)13notation ring P := R[I]14hypothesis field : IsField(R)15hypothesis generators : G ⊆ P16-- This is the remaining obligation. It is not asserted as an axiom or hidden in a definition.17hypothesis residues : ∀ J, IsMaximalIdeal(P, J) → SurjectiveBetween(polynomialResidueCoefficients(I, R, J), R, (P ⧸ idealRelation(P, J)))1819theorem unit_certificate_iff_unsatisfiable_given_residue_surjectivity20  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, A, add, zero, neg, mul, one, G, v))21proof22  exact polynomialIdeal.unit_iff_no_common_zero_of_residue_surjectivity with field, residues, generators2324end Residues25