theorem HexBerlekampZassenhausMathlib.bhksLatticeBasis_basis_lowerZero (f : Hex.ZPoly) (p a : ℕ) (lifted : Array Hex.ZPoly) (i j : Fin (lifted.size + Hex.DensePoly.natDegree f)) (hji : ↑j < ↑i) : (Hex.bhksLatticeBasis f p a lifted).basis[i][j] = 0

The BHKS knapsack lattice basis is upper-triangular: below-diagonal entries vanish. Follows from the block structure [I_r | Ã; 0 | diag].

theorem HexBerlekampZassenhausMathlib.bhksLatticeBasis_basis_diagPos (f : Hex.ZPoly) (p a : ℕ) (hp : 0 < p) (lifted : Array Hex.ZPoly) (i : Fin (lifted.size + Hex.DensePoly.natDegree f)) : 0 < (Hex.bhksLatticeBasis f p a lifted).basis[i][i]

The BHKS knapsack lattice basis has strictly positive diagonal (needs 0 < p): 1 in the I_r block, p^(a-l_j) > 0 in the D block.

theorem HexBerlekampZassenhausMathlib.bhksLatticeBasis_basis_independent (f : Hex.ZPoly) (p a : ℕ) (hp : 0 < p) (lifted : Array Hex.ZPoly) : (Hex.bhksLatticeBasis f p a lifted).basis.independent

The BHKS knapsack lattice basis is LLL-independent (Hex.Matrix.independent), so the proven LLL short-vector bound applies to it.

theorem HexBerlekampZassenhausMathlib.two_mul_bhksCoeffBound_le_cldCoeffFloor (core : Hex.ZPoly) (j : ℕ) : 2 * Hex.bhksCoeffBound core j ≤ Hex.cldCoeffFloor core

Every direct CLD column bound is dominated by the CLD floor.

theorem HexBerlekampZassenhausMathlib.liftedFactorProduct_singleton (d : Hex.LiftData) (i : LiftedFactorIndex d) : liftedFactorProduct d {i} = liftedFactor d i

The lifted-factor product over a singleton subset is the lifted factor.

theorem HexBerlekampZassenhausMathlib.directLiftedFactor_degree_pos (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (i : LiftedFactorIndex (core.directLiftData B data)) : 0 < Hex.DensePoly.natDegree (liftedFactor (core.directLiftData B data) i)

Each direct Hensel factor has positive degree.

theorem HexBerlekampZassenhausMathlib.directLiftedFactor_core_congr (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (i : LiftedFactorIndex (core.directLiftData B data)) : core.congr (liftedFactor (core.directLiftData B data) i * Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff core) (liftedFactorProduct (core.directLiftData B data) (Finset.univ \ {i}))) ((core.directLiftData B data).p ^ (core.directLiftData B data).k)

The full direct lift, scaled once by the input leading coefficient, factors through each local factor modulo the lift modulus.

theorem HexBerlekampZassenhausMathlib.directLiftedFactors_isCoprime (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (i j : LiftedFactorIndex (core.directLiftData B data)) (hji : j ≠ i) : IsCoprime (Polynomial.map (Int.castRingHom (ZMod ((core.directLiftData B data).p ^ (core.directLiftData B data).k))) (HexPolyZMathlib.toPolynomial (liftedFactor (core.directLiftData B data) i))) (Polynomial.map (Int.castRingHom (ZMod ((core.directLiftData B data).p ^ (core.directLiftData B data).k))) (HexPolyZMathlib.toPolynomial (liftedFactor (core.directLiftData B data) j)))

Distinct factors in the direct Hensel basis remain coprime modulo the full lift modulus.

theorem HexBerlekampZassenhausMathlib.directLiftedFactor_map_irreducible (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (i : LiftedFactorIndex (core.directLiftData B data)) : Irreducible (Polynomial.map (Int.castRingHom (ZMod data.p)) (HexPolyZMathlib.toPolynomial (liftedFactor (core.directLiftData B data) i)))

A direct Hensel factor remains irreducible after reduction at its selected prime.

theorem HexBerlekampZassenhausMathlib.directLiftedFactor_map_irreducible_at_liftPrime (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (i : LiftedFactorIndex (core.directLiftData B data)) : Irreducible (Polynomial.map (Int.castRingHom (ZMod (core.directLiftData B data).p)) (HexPolyZMathlib.toPolynomial (liftedFactor (core.directLiftData B data) i)))

A direct Hensel factor remains irreducible after reduction at the prime stored in the canonical lift data.

theorem HexBerlekampZassenhausMathlib.directLiftedFactor_natDegree_le_core (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (i : LiftedFactorIndex (core.directLiftData B data)) : (HexPolyZMathlib.toPolynomial ((core.directLiftData B data).liftedFactors.getD (↑i) 1)).natDegree ≤ (HexPolyZMathlib.toPolynomial core).natDegree

Every direct Hensel factor has degree at most the input polynomial. Reduction at the selected prime preserves both degrees, and the direct factor congruence makes the local factor divide the reduced square-free part.

theorem HexBerlekampZassenhausMathlib.directLiftedFactor_isCoprime_cldQuotient (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (facts : DirectLiftFacts core B data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (i : LiftedFactorIndex (core.directLiftData B data)) : IsCoprime (Polynomial.map (Int.castRingHom (ZMod ((core.directLiftData B data).p ^ (core.directLiftData B data).k))) (HexPolyZMathlib.toPolynomial (liftedFactor (core.directLiftData B data) i))) (Polynomial.map (Int.castRingHom (ZMod ((core.directLiftData B data).p ^ (core.directLiftData B data).k))) (HexPolyZMathlib.toPolynomial (Hex.cldQuotientMod core (liftedFactor (core.directLiftData B data) i) (core.directLiftData B data).p (core.directLiftData B data).k)))

A direct Hensel factor is coprime modulo the lift modulus to its own CLD quotient.

theorem HexBerlekampZassenhausMathlib.bhksProjectedRowSpanInt_le_trueSupportSpanInt (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) (hrows : 1 ≤ liftedFactors.size + Hex.DensePoly.natDegree f) (hind : (Hex.bhksLatticeBasis f p a liftedFactors).basis.independent) (hcover : ∀ (i : Fin liftedFactors.size), ∃ S ∈ trueSupports, i ∈ S) (hdisjoint : ∀ S ∈ trueSupports, ∀ T ∈ trueSupports, ∀ i ∈ S, i ∈ T → S = T) (hne : ∀ S ∈ trueSupports, S.Nonempty) (data : (S : ↑trueSupports) → BHKS.SupportShortVectorData (Hex.bhksLatticeBasis f p a liftedFactors) ↑S) (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) : BHKS.projectedRowSpanInt (Hex.bhksProjectedRows (Hex.bhksLatticeBasis f p a liftedFactors) hrows) ≤ BHKS.trueSupportSpanInt trueSupports

Production-bounded BHKS reverse containment from the algebraic lift facts.

This is the assembly point between the LLL geometry and the resultant contradiction. The deliberately coarse R, V, and E used by Hex.bhksBound dominate, respectively, support-vector coordinates, retained row coordinates, and the adjusted full vector.

structure HexBerlekampZassenhausMathlib.DirectAdequacy (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) : Prop

The direct lift and its genuine-support partition at an ordinary recombination-adequate precision. This is the shared algebraic context for both the inexpensive forward cut theorem and the full resultant argument.

• precision : 1 ≤ Hex.precisionForCoeffBound B data.p

  The Hensel precision contains at least one prime-power digit.

• inputScale_coprime : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1

  The input leading coefficient is invertible modulo the lift modulus.

• recovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p

  The modulus is large enough for unique centred coefficient recovery.

• lift : DirectLiftFacts core B data

  The semantic properties of the direct-coordinate Hensel lift.

• partition : DirectSupportPartition core B data Finset.univ core

  The genuine-factor supports partition all modular factors.

theorem HexBerlekampZassenhausMathlib.directAdequacy (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hval : ModPFactorization core data) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (_hB_ne : B ≠ 0) : DirectAdequacy core B data

Build the unique direct adequacy context from the semantic prime plan and the executable recovery floor.

theorem HexBerlekampZassenhausMathlib.DirectAdequacy.cover {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (A : DirectAdequacy core B data) (hcore_prim : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hval : ModPFactorization core data) (i : LiftedFactorIndex (core.directLiftData B data)) : ∃ U ∈ directTrueSupports core B data, i ∈ U

Every lifted-factor index belongs to a genuine support.

theorem HexBerlekampZassenhausMathlib.DirectAdequacy.disjoint {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (A : DirectAdequacy core B data) (U : Set (LiftedFactorIndex (core.directLiftData B data))) : U ∈ directTrueSupports core B data → ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V

Two genuine supports sharing an index are equal.

theorem HexBerlekampZassenhausMathlib.DirectAdequacy.factorCount {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (A : DirectAdequacy core B data) (hcore_prim : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hval : ModPFactorization core data) (hcore_ne : core ≠ 0) : (directTrueSupports core B data).ncard = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card

The number of genuine supports equals the number of normalized irreducible factors.

theorem HexBerlekampZassenhausMathlib.DirectAdequacy.localFactor {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (A : DirectAdequacy core B data) (hval : ModPFactorization core data) (i : LiftedFactorIndex (core.directLiftData B data)) : ∃ (h : Hex.ZPoly), Hex.DensePoly.Monic ((core.directLiftData B data).liftedFactors.getD (↑i) 1) ∧ 0 < Hex.DensePoly.natDegree ((core.directLiftData B data).liftedFactors.getD (↑i) 1) ∧ core.congr ((core.directLiftData B data).liftedFactors.getD (↑i) 1 * h) ((core.directLiftData B data).p ^ (core.directLiftData B data).k)

Every local factor divides the input modulo the full direct lift modulus.

noncomputable def HexBerlekampZassenhausMathlib.DirectAdequacy.shortVector {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (A : DirectAdequacy core B data) (hval : ModPFactorization core data) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (U : ↑(directTrueSupports core B data)) : BHKS.SupportShortVectorData (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) ↑U

The CLD vector of every genuine direct support is short at the ordinary recombination floor.

Equations

• One or more equations did not get rendered due to their size.

theorem HexBerlekampZassenhausMathlib.directCutProjection (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hval : ModPFactorization core data) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (hB_ne : B ≠ 0) (hrows : 1 ≤ (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).factorCount + (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).coeffWidth) : BHKS.CutProjectionHypotheses (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows) (directTrueSupports core B data)

At the ordinary recovery floor, every genuine direct support survives the Gram--Schmidt cut. This is the forward half W ≤ L'; unlike exact span it does not require the larger resultant bound.

theorem HexBerlekampZassenhausMathlib.directFactorCount_le_classCount (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hval : ModPFactorization core data) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (hB_ne : B ≠ 0) (hrows : 1 ≤ (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).factorCount + (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).coeffWidth) : (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card ≤ (Hex.bhksEquivalenceClassIndicators (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows)).size

At the ordinary recovery floor, the executable CLD partition has at least one class for every irreducible integer factor.

theorem HexBerlekampZassenhausMathlib.directProjectedSpan_eq (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hcore_pos : 0 < Hex.DensePoly.natDegree core) (hcore_prim : core.Primitive) (hcore_sqfree : Squarefree (HexPolyZMathlib.toPolynomial core)) (hval : ModPFactorization core data) (hp500 : data.p ≤ 500) (hB_floor : Hex.bhksRecoveryFloor core ≤ B) (hB_ne : B ≠ 0) (hadequate : 2 * Hex.bhksBound core < (core.directLiftData B data).p ^ (core.directLiftData B data).k) (hrows : 1 ≤ (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).factorCount + (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors).coeffWidth) : BHKS.projectedRowSpanInt (Hex.bhksProjectedRows (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) hrows) = BHKS.trueSupportSpanInt (directTrueSupports core B data)

At an adequate precision, the projected CLD lattice is exactly the span of the direct modular supports of the normalized irreducible integer factors. All algebraic inputs use directLiftData; no dilation-coordinate lift appears in the statement or proof.