The polynomial system x+y=3, xy=5, x^2+y^2=1 is inconsistent, witnessed by an explicit cofactor identity summing to the constant 1

Identifier: F:cas-groebner-cofactor-unit-ideal-witness
Proof route: cas-certificate
External status: proved
Axiom footprint: cas.exact-rational-multivariate-polynomial-arithmetic: MvPoly add/mul/sub run in axeyum-cas's own exact-rational representation, not through crate::Kernel::add_declaration., cas.recombination-is-order-independent-of-the-producing-walk: the cofactor SEARCH (unit_ideal_cofactors) is a Buchberger-style Groebner walk under a chosen monomial order (crate::groebner::MonomialOrder), and its correctness as a search is taken as read. What this fact checks is the WITNESS the walk emits, by a `recombine` re-derivation using only MvPoly::add/MvPoly::mul -- no leading-term selection, no monomial order, no S-polynomial reduction -- so a bug in the Groebner walk's search strategy can at worst cause a decline or a wrong non-witness, never manufacture a false 'unit ideal' verdict that survives recombination., cas.groebner-cert-no-kernel-carrier: this kernel has no Groebner/multivariate-polynomial development capable of hosting c1*g1+c2*g2+c3*g3=1 as a checked term; rat_prelude/polynomial.rs is univariate.

Recorded description

The three polynomials g1 = x+y-3, g2 = xy-5, g3 = x^2+y^2-1 generate the unit ideal in Q[x,y]: there exist cofactor polynomials c1,c2,c3 with c1*g1 + c2*g2 + c3*g3 = 1 identically. This means the system {x+y=3, xy=5, x^2+y^2=1} has NO common solution over any commutative ring extension -- (x+y)^2 = x^2+2xy+y^2 forces x^2+y^2 = 9-10 = -1 whenever the first two equations hold, contradicting the third. axeyum_cas::groebner_cert::unit_ideal_cofactors produces the cofactors by a monomial-order-dependent Groebner walk, but the WITNESS is order-independent: an independent re-derivation using nothing but polynomial addition and multiplication (no Groebner machinery, no monomial order, no S-polynomials) recombines c1*g1+c2*g2+c3*g3 and confirms it equals exactly the constant 1. As a companion, the system {x-1, y-2} -- consistent, with common zero (1,2) -- correctly produces a NONZERO remainder, so the checker is shown capable of the negative answer and not merely always returning 'unit ideal'. Cas-internal under ADR-0601 SS2: the kernel has rat_prelude/matrix.rs and polynomial.rs but no multivariate polynomial ring with exact division, so this identity is not currently bridgeable.

Formal statement

(groebner-cofactor-certificate
  (generators (- (+ x y) 3) (- (* x y) 5) (- (+ (pow x 2) (pow y 2)) 1))
  (assert (= (+ (* c1 g1) (* c2 g2) (* c3 g3)) 1))
  (conclude (unit-ideal generators))
  (conclude (forall (x y) (not (and (= (+ x y) 3) (= (* x y) 5) (= (+ (pow x 2) (pow y 2)) 1))))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

cas-groebner-unit-ideal-recombines-to-one

Kind: witness-replay
Status: checked

Supports: the cofactor identity c1*g1+c2*g2+c3*g3 = 1 for the three named generators, re-derived independently of the Groebner walk that produced the cofactors

Checker command

cargo test -p axeyum-cas --lib groebner_cert::tests::unit_ideal_certificate_recombines -- --exact 2>/dev/null | grep -cE '^test groebner_cert::tests::unit_ideal_certificate_recombines \.\.\. ok$'

Evidence notes

Verified both directions on this host: the real test path gives count=1, exit=0; the same command against a deliberately wrong test path (…_WRONG) gives count=0, exit=1. `grep -cE` consumes the pipe so it cannot SIGPIPE.

cas-groebner-consistent-system-is-not-refuted

Kind: witness-replay
Status: checked

Supports: the companion consistent system {x-1, y-2} -- which has the common zero (1,2) -- produces a nonzero remainder rather than a spurious unit-ideal claim, so the checker demonstrably distinguishes the two cases rather than always answering 'unit ideal'

Checker command

cargo test -p axeyum-cas --lib groebner_cert::tests::a_consistent_system_does_not_contain_the_unit -- --exact 2>/dev/null | grep -cE '^test groebner_cert::tests::a_consistent_system_does_not_contain_the_unit \.\.\. ok$'

Evidence notes

Verified both directions on this host: count=1 exit=0 for the real test path, count=0 exit=1 for a deliberately wrong test path. Without this row the first row alone would not show the module can report anything other than a unit-ideal verdict.

Provenance

{
  "date": "2026-09-01",
  "established_by": "lane cas-facts-round-two, following docs/research/11-design-review/2026-09-01-cas-certificate-reconstruction-audit.md, which listed groebner_cert.rs among the certificate-carrying modules with no naming fact even though its cofactor identity is reachable from the geometry bridge facts through certify_by_linear_elimination. This fact names groebner_cert.rs directly, via its own module tests, independent of the geometry-certificate family.",
  "source": "Groebner basis theory (Buchberger); the ideal-membership refutation technique -- a cofactor identity summing to a nonzero constant witnesses inconsistency of a polynomial system over any commutative ring -- is standard computational algebra, used throughout this crate's geometry-theorem certification (geometry_certify.rs).",
  "prior_art": [
    {
      "who": "Bruno Buchberger",
      "what": "Groebner bases and the algorithm for deciding ideal membership that this module's search is built on",
      "year": 1965,
      "where": "PhD thesis, University of Innsbruck; see also his 1970 Aequationes Mathematicae paper",
      "attribution": "standard attribution; this lane did not consult the primary source"
    }
  ]
}