theorem HexBerlekampZassenhausMathlib.BHKS.adjustedCoordBound_lt_bhksBound (f : Hex.ZPoly) (hfdeg : 0 < Hex.DensePoly.natDegree f) : have n := Hex.DensePoly.natDegree f; have R := 4 * n + n * n * n; have V := 2 * n * 2 ^ (2 * n) * R; V + V * R + 2 ^ n * R < Hex.bhksBound f

The complete-vector coordinate envelope used by the BHKS adjustment is strictly below the executable resultant cap.

theorem HexBerlekampZassenhausMathlib.BHKS.cldFullAux_resultant_natAbs_lt_bhksBound (f : Hex.ZPoly) (p a : ℕ) (liftedFactors : Array Hex.ZPoly) (v : Vector ℤ ((Hex.bhksLatticeBasis f p a liftedFactors).factorCount + (Hex.bhksLatticeBasis f p a liftedFactors).coeffWidth)) (hf : f ≠ 0) (hfdeg : 0 < Hex.DensePoly.natDegree f) (hp2 : 2 ≤ p) (hp500 : p ≤ 500) (hr : liftedFactors.size ≤ Hex.DensePoly.natDegree f) (hv : ∀ (x : Fin (liftedFactors.size + Hex.DensePoly.natDegree f)), v[x].natAbs ≤ have n := Hex.DensePoly.natDegree f; have R := 4 * n + n * n * n; have V := 2 * n * 2 ^ (2 * n) * R; V + V * R + 2 ^ n * R) : ((HexPolyZMathlib.toPolynomial f).resultant (HexPolyZMathlib.toPolynomial (cldFullAux f p a liftedFactors v))).natAbs < Hex.bhksBound f

The explicit bhksBound strictly dominates the resultant of the input and any corrected full auxiliary whose complete lattice vector satisfies the E coordinate bound built into that cap.

theorem HexBerlekampZassenhausMathlib.BHKS.no_badVector (f : Hex.ZPoly) (p a : ℕ) (liftedFactors : Array Hex.ZPoly) (trueSupports : Set (Set (Fin liftedFactors.size))) (hf : f ≠ 0) (hfdeg : 0 < Hex.DensePoly.natDegree f) (hf_lc_coprime : IsCoprime (↑(p ^ a)) (HexPolyZMathlib.toPolynomial f).leadingCoeff) (hp2 : 2 ≤ p) (hp500 : p ≤ 500) (hr : liftedFactors.size ≤ Hex.DensePoly.natDegree f) (hk : 1 < p ^ a) (hprecision : 2 * Hex.bhksBound f < p ^ a) (hcut : ∀ (j : Fin (Hex.DensePoly.natDegree f)), Hex.bhksCoeffCutThreshold p f ↑j ≤ a) (hfac : ∀ (i : Fin liftedFactors.size), ∃ (h : Hex.ZPoly), Hex.DensePoly.Monic (liftedFactors.getD (↑i) 1) ∧ 0 < Hex.DensePoly.natDegree (liftedFactors.getD (↑i) 1) ∧ f.congr (liftedFactors.getD (↑i) 1 * h) (p ^ a)) (hdeg_le : ∀ (i : Fin liftedFactors.size), (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i) 1)).natDegree ≤ (HexPolyZMathlib.toPolynomial f).natDegree) (hcop : ∀ (i j : Fin liftedFactors.size), j ≠ i → IsCoprime (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i) 1))) (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑j) 1)))) (hown : ∀ (i : Fin liftedFactors.size), IsCoprime (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i) 1))) (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (Hex.cldQuotientMod f (liftedFactors.getD (↑i) 1) p a)))) (hsupport : ∀ (q : Polynomial ℤ), Irreducible q → q ∣ HexPolyZMathlib.toPolynomial f → ∃ S ∈ trueSupports, ∀ i ∈ S, Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i) 1)) ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ a))) q) (v : Vector ℤ ((Hex.bhksLatticeBasis f p a liftedFactors).factorCount + (Hex.bhksLatticeBasis f p a liftedFactors).coeffWidth)) (hv : (Hex.bhksLatticeBasis f p a liftedFactors).basis.memLattice v) (hzero : ∃ (i : Fin liftedFactors.size), v[Fin.castAdd (Hex.DensePoly.natDegree f) i] = 0) (hnonzero : ∀ S ∈ trueSupports, ∃ i ∈ S, v[Fin.castAdd (Hex.DensePoly.natDegree f) i] ≠ 0) (hvBound : ∀ (x : Fin (liftedFactors.size + Hex.DensePoly.natDegree f)), v[x].natAbs ≤ have n := Hex.DensePoly.natDegree f; have R := 4 * n + n * n * n; have V := 2 * n * 2 ^ (2 * n) * R; V + V * R + 2 ^ n * R) : False

Abstract algebraic BHKS bad-vector contradiction.

The hypotheses expose exactly the production facts later supplied by the Hensel lift: local monicity and positive degree, pairwise coprimality, own-CLD coprimality, and the fact that every monic irreducible factor of f is represented by one true support. The conclusion rules out a bounded lattice vector having one zero exponent while remaining nonzero on every true support.