theorem HexBerlekampZassenhausMathlib.BHKS.cldQuotientMod_size_le_degree (f g : Hex.ZPoly) (p a : ℕ) (hf : 0 < Hex.DensePoly.natDegree f) (hg : 0 < Hex.DensePoly.natDegree g) : Hex.DensePoly.size (Hex.cldQuotientMod f g p a) ≤ Hex.DensePoly.natDegree f

A positive-degree CLD divisor leaves a quotient with strictly fewer coefficient slots than the input. Thus the production coeffWidth = deg(f) array stores the whole CLD quotient, not a truncation.

def HexBerlekampZassenhausMathlib.BHKS.polCoeff (L : Hex.BhksLatticeBasis) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) (j : Fin L.coeffWidth) : ℤ

The full centred CLD-residue combination attached to the first block of a BHKS vector.

Equations

• HexBerlekampZassenhausMathlib.BHKS.polCoeff L z v j = ∑ i : Fin L.factorCount, v[Fin.castAdd L.coeffWidth i] * Hex.centeredResiduePow L.p L.precision (z i j)

def HexBerlekampZassenhausMathlib.BHKS.fullAuxCoeff (L : Hex.BhksLatticeBasis) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) (j : Fin L.coeffWidth) : ℤ

Correct reconstruction of one coefficient of the truncated-lattice auxiliary polynomial from the full lattice vector.

Equations

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

def HexBerlekampZassenhausMathlib.BHKS.pol (L : Hex.BhksLatticeBasis) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) : Hex.ZPoly

Polynomial whose coefficients are the full centred CLD-residue combination POL(e).

Equations

• HexBerlekampZassenhausMathlib.BHKS.pol L z v = Hex.DensePoly.ofCoeffs (Array.ofFn fun (j : Fin L.coeffWidth) => HexBerlekampZassenhausMathlib.BHKS.polCoeff L z v j)

def HexBerlekampZassenhausMathlib.BHKS.fullAux (L : Hex.BhksLatticeBasis) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) : Hex.ZPoly

Polynomial reconstructed from all coordinates of a truncated BHKS lattice vector.

Equations

• HexBerlekampZassenhausMathlib.BHKS.fullAux L z v = Hex.DensePoly.ofCoeffs (Array.ofFn fun (j : Fin L.coeffWidth) => HexBerlekampZassenhausMathlib.BHKS.fullAuxCoeff L z v j)

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.pol_coeff (L : Hex.BhksLatticeBasis) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) (j : Fin L.coeffWidth) : Hex.DensePoly.coeff (pol L z v) ↑j = polCoeff L z v j

Coefficient rule for pol.

@[simp]

theorem HexBerlekampZassenhausMathlib.BHKS.fullAux_coeff (L : Hex.BhksLatticeBasis) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (v : Vector ℤ (L.factorCount + L.coeffWidth)) (j : Fin L.coeffWidth) : Hex.DensePoly.coeff (fullAux L z v) ↑j = fullAuxCoeff L z v j

Coefficient rule for fullAux.

theorem HexBerlekampZassenhausMathlib.BHKS.fullAuxCoeff_vecMul (L : Hex.BhksLatticeBasis) (hL : BhksBlockForm L) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (c : Vector ℤ (L.factorCount + L.coeffWidth)) (j : Fin L.coeffWidth) (hcut : L.cutThresholds.getD (↑j) 0 ≤ L.precision) (hp : 0 < L.p) (hcld : ∀ (i : Fin L.factorCount), (L.cldRows.getD ↑i #[]).getD (↑j) 0 = Hex.psiCut L.p L.precision (L.cutThresholds.getD (↑j) 0) (z i j)) : fullAuxCoeff L z (Hex.Matrix.vecMul c L.basis) j = polCoeff L z (Hex.Matrix.vecMul c L.basis) j + ↑(L.p ^ L.precision) * c[Fin.natAdd L.factorCount j]

The corrected coefficient reconstruction identity.

The top-right block contributes the cut coefficients, the bottom-right block contributes the period coefficient, and the low residues restore the discarded part of each centred CLD residue. The only term left over is the displayed multiple of p^precision.

theorem HexBerlekampZassenhausMathlib.BHKS.fullAux_congr_pol_vecMul (L : Hex.BhksLatticeBasis) (hL : BhksBlockForm L) (z : Fin L.factorCount → Fin L.coeffWidth → ℤ) (c : Vector ℤ (L.factorCount + L.coeffWidth)) (hcut : ∀ (j : Fin L.coeffWidth), L.cutThresholds.getD (↑j) 0 ≤ L.precision) (hp : 0 < L.p) (hcld : ∀ (i : Fin L.factorCount) (j : Fin L.coeffWidth), (L.cldRows.getD ↑i #[]).getD (↑j) 0 = Hex.psiCut L.p L.precision (L.cutThresholds.getD (↑j) 0) (z i j)) : (fullAux L z (Hex.Matrix.vecMul c L.basis)).congr (pol L z (Hex.Matrix.vecMul c L.basis)) (L.p ^ L.precision)

Polynomial form of fullAuxCoeff_vecMul: the full-vector auxiliary is coefficientwise congruent modulo p^precision to POL(e).

def HexBerlekampZassenhausMathlib.BHKS.cldResidue (f : Hex.ZPoly) (p a : ℕ) (liftedFactors : Array Hex.ZPoly) (i : Fin (Hex.bhksLatticeBasis f p a liftedFactors).factorCount) (j : Fin (Hex.bhksLatticeBasis f p a liftedFactors).coeffWidth) : ℤ

Raw quotient coefficient used by the production all-coefficients CLD lattice.

Equations

• HexBerlekampZassenhausMathlib.BHKS.cldResidue f p a liftedFactors i j = Hex.DensePoly.coeff (Hex.cldQuotientMod f (liftedFactors.getD (↑i) 1) p a) ↑j

def HexBerlekampZassenhausMathlib.BHKS.cldFullAux (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)) : Hex.ZPoly

Production specialization of the corrected full-vector auxiliary.

Equations

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

theorem HexBerlekampZassenhausMathlib.BHKS.cldFullAux_coeff_natAbs_le (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)) (E : ℕ) (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 ≤ E) (k : ℕ) : (Hex.DensePoly.coeff (cldFullAux f p a liftedFactors v) k).natAbs ≤ (Hex.DensePoly.natDegree f + 1) * E * (500 * (Hex.bhksColumnFloor f + 1))

Every coefficient of the corrected production auxiliary is bounded by the M component of Hex.bhksBound, provided all coordinates of the full lattice vector have magnitude at most E.

The period coordinate contributes one term bounded by E*C; each of the at most degree f first-block coordinates contributes another such term.

theorem HexBerlekampZassenhausMathlib.BHKS.cldFullAux_natDegree_le (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)) : (HexPolyZMathlib.toPolynomial (cldFullAux f p a liftedFactors v)).natDegree ≤ Hex.DensePoly.natDegree f

The corrected full auxiliary stores exactly degree f coefficient slots.

def HexBerlekampZassenhausMathlib.BHKS.cldPol (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)) : Hex.ZPoly

Production specialization of the full centred residue combination POL(e).

Equations

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

noncomputable def HexBerlekampZassenhausMathlib.BHKS.cldCombination (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)) : Polynomial ℤ

The same production CLD combination before coefficient centering.

Equations

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

theorem HexBerlekampZassenhausMathlib.BHKS.cldCombination_coeff (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)) (j : ℕ) : (cldCombination f p a liftedFactors v).coeff j = ∑ i : Fin liftedFactors.size, v[Fin.castAdd (Hex.DensePoly.natDegree f) i] * Hex.DensePoly.coeff (Hex.cldQuotientMod f (liftedFactors.getD (↑i) 1) p a) j

Coefficients of the uncentred CLD combination.

theorem HexBerlekampZassenhausMathlib.BHKS.cldPol_coeff_of_lt (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)) (k : ℕ) (hk : k < Hex.DensePoly.natDegree f) : Hex.DensePoly.coeff (cldPol f p a liftedFactors v) k = ∑ i : Fin liftedFactors.size, v[Fin.castAdd (Hex.DensePoly.natDegree f) i] * Hex.centeredResiduePow p a (Hex.DensePoly.coeff (Hex.cldQuotientMod f (liftedFactors.getD (↑i) 1) p a) k)

In-range coefficient formula for the centred production CLD combination.

theorem HexBerlekampZassenhausMathlib.BHKS.cldPol_map_eq_cldCombination (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 : 0 < Hex.DensePoly.natDegree f) (hdeg : ∀ (i : Fin liftedFactors.size), 0 < Hex.DensePoly.natDegree (liftedFactors.getD (↑i) 1)) : Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (cldPol f p a liftedFactors v)) = Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (cldCombination f p a liftedFactors v)

Modulo the lift modulus, centering the stored CLD coefficients does not change the polynomial combination.

theorem HexBerlekampZassenhausMathlib.BHKS.liftedFactor_dvd_cldCombination_of_coord_eq_zero (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)) (i₀ : Fin liftedFactors.size) (hk : 1 < p ^ 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)) (hcop : ∀ (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)))) (hzero : v[Fin.castAdd (Hex.DensePoly.natDegree f) i₀] = 0) : Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i₀) 1)) ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (cldCombination f p a liftedFactors v)

If one first-block exponent is zero, the corresponding lifted local factor divides the uncentred CLD combination modulo the lift modulus. Pairwise coprimality cancels every other lifted factor from its CLD syzygy.

theorem HexBerlekampZassenhausMathlib.BHKS.coord_cast_eq_zero_of_liftedFactor_dvd_cldCombination (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)) (i₀ : Fin liftedFactors.size) (hk : 1 < p ^ 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)) (hcop : ∀ (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 : 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)))) (hdvd : Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i₀) 1)) ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (cldCombination f p a liftedFactors v)) : ↑v[Fin.castAdd (Hex.DensePoly.natDegree f) i₀] = 0

Conversely, if a lifted factor divides the CLD combination and is coprime to its own CLD quotient modulo the lift modulus, then its first-block exponent vanishes modulo that modulus.

theorem HexBerlekampZassenhausMathlib.BHKS.isCoprime_cldQuotientMod (f q h : Hex.ZPoly) (p a : ℕ) (hk : 1 < p ^ a) (hqmonic : Hex.DensePoly.Monic q) (hqdeg : 0 < Hex.DensePoly.natDegree q) (hfac : f.congr (q * h) (p ^ a)) (hcop_h : IsCoprime (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial q)) (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial h))) (hcop_deriv : IsCoprime (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial q)) (Polynomial.derivative (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial q)))) : IsCoprime (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial q)) (Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (Hex.cldQuotientMod f q p a)))

The CLD quotient belonging to one lifted factor is coprime to that factor modulo the lift modulus. The two substantive inputs are exactly the familiar square-free factorisation properties: the factor is coprime to its complementary factor h, and it is coprime to its own derivative.

Indeed the CLD congruence and f ≡ q * h give q * cld = q * (h * q') after mapping modulo p^a. Monicity cancels q; the right-hand side is coprime to q.

theorem HexBerlekampZassenhausMathlib.BHKS.cldFullAux_congr_cldPol (f : Hex.ZPoly) (p a : ℕ) (liftedFactors : Array Hex.ZPoly) (c : Vector ℤ ((Hex.bhksLatticeBasis f p a liftedFactors).factorCount + (Hex.bhksLatticeBasis f p a liftedFactors).coeffWidth)) (hp : 0 < p) (hcut : ∀ (j : Fin (Hex.DensePoly.natDegree f)), Hex.bhksCoeffCutThreshold p f ↑j ≤ a) : (cldFullAux f p a liftedFactors (Hex.Matrix.vecMul c (Hex.bhksLatticeBasis f p a liftedFactors).basis)).congr (cldPol f p a liftedFactors (Hex.Matrix.vecMul c (Hex.bhksLatticeBasis f p a liftedFactors).basis)) (p ^ a)

The corrected auxiliary polynomial for the production BHKS basis is congruent to its full centred CLD-residue combination modulo p^a.

theorem HexBerlekampZassenhausMathlib.BHKS.liftedFactor_dvd_cldFullAux (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)) (i₀ : Fin liftedFactors.size) (hf : 0 < Hex.DensePoly.natDegree f) (hk : 1 < p ^ a) (hp : 0 < p) (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)) (hcop : ∀ (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)))) (hv : (Hex.bhksLatticeBasis f p a liftedFactors).basis.memLattice v) (hzero : v[Fin.castAdd (Hex.DensePoly.natDegree f) i₀] = 0) : Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i₀) 1)) ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (cldFullAux f p a liftedFactors v))

A zero first-block coordinate of an actual BHKS lattice vector makes the corresponding lifted factor divide the corrected full auxiliary modulo the lift modulus.

theorem HexBerlekampZassenhausMathlib.BHKS.coord_cast_eq_zero_of_liftedFactor_dvd_cldFullAux (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)) (i₀ : Fin liftedFactors.size) (hf : 0 < Hex.DensePoly.natDegree f) (hk : 1 < p ^ a) (hp : 0 < p) (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)) (hcop : ∀ (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 : 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)))) (hv : (Hex.bhksLatticeBasis f p a liftedFactors).basis.memLattice v) (hdvd : Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (liftedFactors.getD (↑i₀) 1)) ∣ Polynomial.map (Int.castRingHom (ZMod (p ^ a))) (HexPolyZMathlib.toPolynomial (cldFullAux f p a liftedFactors v))) : ↑v[Fin.castAdd (Hex.DensePoly.natDegree f) i₀] = 0

Divisibility of the corrected full auxiliary by a lifted factor forces the corresponding first-block coordinate to vanish modulo the lift modulus.