HexPolyZGcd computes greatest common divisors in ℤ[x] together with
exact cofactors and replayable coprimality evidence. Its fast routes use
modular images, heuristic reconstruction, and subresultant chains. Every
route passes through the same small checker before its answer becomes public.
The executable library is Mathlib-free. It builds on HexPolyZ,
HexModular, and HexResultant, and it supplies the square-free
decomposition used by integer-polynomial factorization.
Evidence that the two cofactors have no common nonunit factor.
Constructors
Hex.ZPoly.CoprimeWitness.modular (p : Hex.ZMod64.Prime) (alpha beta : Hex.FpPoly p.m) : Hex.ZPoly.CoprimeWitness
A degree-preserving reduction and a Bezout identity over a prime field.
Hex.ZPoly.CoprimeWitness.constant (u v : Hex.ZPoly) (k : ℤ) : Hex.ZPoly.CoprimeWitness
An integral polynomial combination equal to a nonzero constant.
A gcd candidate, its two exact cofactors, and checked coprimality data.
Constructor
Hex.ZPoly.GcdCert.mk
Fields
gcd : Hex.ZPoly
The proposed normalized greatest common divisor.
cofL : Hex.ZPoly
The exact cofactor of the left input.
cofR : Hex.ZPoly
The exact cofactor of the right input.
coprime : Hex.ZPoly.CoprimeWitness
Replayable evidence that the two cofactors have no common nonunit.
Check a gcd certificate. Every producer, including deterministic fallbacks, must pass through this function before its candidate is exposed.
A successful checker establishes both exact cofactor identities and coprimality of the cofactors.
The checker verifies two exact product identities, the normalization convention, coprime cofactor contents, and one modular or integral Bezout witness. Candidate production is separate from certificate replay.
The exact quotient f / g, or none when g = 0 or the executable
integer-polynomial division does not reconstruct f exactly.
A successful exact division carries the checked multiplication witness.
Produce a checked gcd certificate. Mandatory zero and constant
certificates run before content or x extraction. Remaining route-0
reduction runs next; rejected fast candidates and failed restoration fall
through to total, data-only extended-subresultant route 4.
Canonically normalized gcd of two integer polynomials. Exposure is
limited to the projection equation gcd_eq_cert; gcdCert and its route
search remain opaque to kernel replay.
Exact cofactors belonging to the checked gcd.
Fold gcd over a list; the empty-list convention is zero.
Canonically normalized least common multiple.
The usual divisibility laws hold for the checked result, including the greatestness direction that downstream factorization algorithms need.
The canonical gcd divides the left input.
The canonical gcd divides the right input.
Every common divisor divides the canonical gcd.
open Hex
namespace HexPolyZGcdChapter
def x1 : ZPoly := DensePoly.ofList [1, 1]
def x2 : ZPoly := DensePoly.ofList [2, 1]
def left : ZPoly := x1 * x1 * x2
def right : ZPoly := x1 * x2 * x2
#guard ZPoly.gcd left right == x1 * x2
end HexPolyZGcdChapter
Integer-gcd replacement for primitiveSquareFreeDecomposition's rational
Euclidean bottleneck. The return type and normalization convention are shared
with the existing reference implementation.
Hex.ZPoly.sqfDecomp_reassembly_signed (f : Hex.ZPoly) : have d := f.sqfDecomp; ∃ ε, (ε = 1 ∨ ε = -1) ∧ Hex.DensePoly.scale ε (d.squareFreeCore * d.repeatedPart) = d.primitiveHex.ZPoly.sqfDecomp_reassembly_signed (f : Hex.ZPoly) : have d := f.sqfDecomp; ∃ ε, (ε = 1 ∨ ε = -1) ∧ Hex.DensePoly.scale ε (d.squareFreeCore * d.repeatedPart) = d.primitive
The fast square-free core and repeated part reassemble the primitive input up to the normalization sign.
Hex.ZPoly.sqfDecomp_squareFreeCore (f : Hex.ZPoly) (hcore : f.sqfDecomp.squareFreeCore ≠ 0) : f.sqfDecomp.squareFreeCore.SquareFreeRatHex.ZPoly.sqfDecomp_squareFreeCore (f : Hex.ZPoly) (hcore : f.sqfDecomp.squareFreeCore ≠ 0) : f.sqfDecomp.squareFreeCore.SquareFreeRat
Every nonzero fast square-free core is square-free over Rat[x].
The implementation uses the checked integer gcd of a primitive polynomial and its derivative. Its proof compares the repeated factor with the rational reference decomposition, then cancels that factor from their signed reassembly laws.
HexPolyZGcdMathlib transports the divisibility and maximality results
through the ring equivalence from ZPoly to Mathlib's Polynomial ℤ.
HexPolyZGcdMathlib.gcd_dvd_left (f h : Hex.ZPoly) : HexPolyZMathlib.equiv (f.gcd h) ∣ HexPolyZMathlib.equiv fHexPolyZGcdMathlib.gcd_dvd_left (f h : Hex.ZPoly) : HexPolyZMathlib.equiv (f.gcd h) ∣ HexPolyZMathlib.equiv f
The transported checked gcd divides the left input.
HexPolyZGcdMathlib.dvd_gcd (d f h : Hex.ZPoly) (hdf : HexPolyZMathlib.equiv d ∣ HexPolyZMathlib.equiv f) (hdh : HexPolyZMathlib.equiv d ∣ HexPolyZMathlib.equiv h) : HexPolyZMathlib.equiv d ∣ HexPolyZMathlib.equiv (f.gcd h)HexPolyZGcdMathlib.dvd_gcd (d f h : Hex.ZPoly) (hdf : HexPolyZMathlib.equiv d ∣ HexPolyZMathlib.equiv f) (hdh : HexPolyZMathlib.equiv d ∣ HexPolyZMathlib.equiv h) : HexPolyZMathlib.equiv d ∣ HexPolyZMathlib.equiv (f.gcd h)
Every common executable divisor divides the transported checked gcd.
HexPolyZGcdMathlib.divExact?_eq_dvd (f g : Hex.ZPoly) : (f.divExact? g).isSome = true ↔ g ≠ 0 ∧ HexPolyZMathlib.equiv g ∣ HexPolyZMathlib.equiv fHexPolyZGcdMathlib.divExact?_eq_dvd (f g : Hex.ZPoly) : (f.divExact? g).isSome = true ↔ g ≠ 0 ∧ HexPolyZMathlib.equiv g ∣ HexPolyZMathlib.equiv f
Checked exact division succeeds precisely for a nonzero divisor that divides after transport to Mathlib polynomials.
The exact-division correspondence records a nonzero-divisor condition.
This distinguishes the executable operation, which rejects division by zero,
from the proposition 0 ∣ 0, which is true.