FiniteIdealCertificate

Arbitrary finite Nullstellensatz certificate soundness (ZF groundwork)

Open in Workbench View on GitHub

1-- Arbitrary finite Nullstellensatz certificate soundness (ZF groundwork).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 FiniteIdealCertificate8import Grace.Cumulus.Algebra.Ring910section Rings11variable (A add zero neg mul one G : Set)12hypothesis source : IsCommRing(A, add, zero, neg, mul, one)13hypothesis bounded : G ⊆ A14notation ring R := (A, add, zero, neg, mul, one)1516theorem finite_witness (x : Set)17  requires member : x ∈ idealSpan(A, add, zero, neg, mul, G)18  shows ∃ terms, List(idealProducts(A, mul, G), terms) ∧ x = ringSum{idealProducts(A, mul, G)}(add, zero, terms)19proof20  exact idealSpan.finite_certificate.forward with source, bounded, member2122section Evaluations23variable (f B plus z minus times unit : Set)24hypothesis target : IsCommRing(B, plus, z, minus, times, unit)25hypothesis hom : IsRingHom(f, A, add, zero, neg, mul, one, B, plus, z, minus, times, unit)26hypothesis nontrivial : Nontrivial(B, z, unit)27notation ring S := (B, plus, z, minus, times, unit)2829theorem no_common_zero (terms : List(idealProducts(A, mul, G)))30  requires identity : R[1] = ringSum{idealProducts(A, mul, G)}(add, zero, terms)31  shows ¬(∀ p ∈ G, f(p) = S[0])32proof33  exact idealSpan.finite_certificate_obstructs_vanishing at A, add, zero, neg, mul, one, G, f, B, plus, z, minus, times, unit, terms with *3435end Evaluations36end Rings37