def HexBerlekampZassenhausMathlib.directLiftedSupport (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (S : ModPFactorSubset data) : LiftedFactorSubset (core.directLiftData B data)

Lift a modular support into the sole canonical Hensel basis.

Equations

• HexBerlekampZassenhausMathlib.directLiftedSupport core B data S = HexBerlekampZassenhausMathlib.liftedSubsetOfModPSubset data (core.directLiftData B data) ⋯ S

theorem HexBerlekampZassenhausMathlib.supportProduct_coe_eq_liftedFactorProduct (f : Hex.ZPoly) (d : Hex.LiftData) (p a : ℕ) (S : LiftedFactorSubset d) : BHKS.supportProduct (Hex.bhksLatticeBasis f p a d.liftedFactors) ↑S = liftedFactorProduct d S

BHKS.supportProduct and the canonical finite-support product select the same direct lifted factors.

structure HexBerlekampZassenhausMathlib.DirectFactorCertificate (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (S : ModPFactorSubset data) : Type

One normalized irreducible integer factor, indexed by its direct modular support and carrying the exact congruence used by the CLD column proof.

• factor : Hex.ZPoly

  The normalized integer factor represented by S.

• cofactor : Hex.ZPoly

  The complementary integer factor.

• irreducible : Irreducible (HexPolyZMathlib.toPolynomial self.factor)

  The represented integer factor is irreducible.

• factor_mul : self.factor * self.cofactor = core

  The factor and cofactor multiply to the input polynomial.

• represented : RepresentsIntegerFactorModP data self.factor S

  The modular subset represents the integer factor.

• normalized : Hex.normalizeFactorSign self.factor = self.factor

  The factor uses the chosen sign normalization.

• supportNonempty : Finset.Nonempty S

  The modular support is not empty.

• candidate_eq : directSupportCandidate core B data S = self.factor

  Direct coefficient recovery returns this factor.

• 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.

• scaledProduct_congr : (scaledLiftedFactorProduct core (core.directLiftData B data) (directLiftedSupport core B data S)).congr (Hex.DensePoly.scale (Hex.DensePoly.leadingCoeff self.cofactor) self.factor) ((core.directLiftData B data).p ^ (core.directLiftData B data).k)

  The scaled lifted product agrees with the scaled factor modulo the lift modulus.

noncomputable def HexBerlekampZassenhausMathlib.DirectFactorCertificate.recoveredLift {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) : BHKS.RecoveredLift (Hex.bhksLatticeBasis core (core.directLiftData B data).p (core.directLiftData B data).k (core.directLiftData B data).liftedFactors) ↑(directLiftedSupport core B data S)

View a direct factor certificate as the logarithmic-derivative recovery package used by the lattice geometry.

Equations

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

theorem HexBerlekampZassenhausMathlib.DirectFactorCertificate.factor_dvd {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) : C.factor ∣ core

A certified direct factor divides the input polynomial.

theorem HexBerlekampZassenhausMathlib.DirectFactorCertificate.factor_ne {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) : C.factor ≠ 0

A certified direct factor is nonzero.

theorem HexBerlekampZassenhausMathlib.DirectFactorCertificate.primitive {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) (hcore_primitive : core.Primitive) : C.factor.Primitive

A certified direct factor of a primitive input is primitive.

theorem HexBerlekampZassenhausMathlib.DirectFactorCertificate.leadingCoeff_pos {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) : 0 < Hex.DensePoly.leadingCoeff C.factor

A certified normalized direct factor has positive leading coefficient.

theorem HexBerlekampZassenhausMathlib.DirectFactorCertificate.degree_pos {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) (hcore_primitive : core.Primitive) : 0 < Hex.DensePoly.natDegree C.factor

A certified direct factor of a primitive input has positive degree.

theorem HexBerlekampZassenhausMathlib.DirectFactorCertificate.liftedFactor_map_dvd {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (C : DirectFactorCertificate core B data S) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (i : LiftedFactorIndex (core.directLiftData B data)) (hi : i ∈ directLiftedSupport core B data S) : 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 C.factor)

Every local Hensel factor in a certified direct support divides the represented integer factor modulo the full lift modulus. The only scalar cancelled here is the cofactor leading coefficient, which is a unit because it divides the input leading coefficient.

theorem HexBerlekampZassenhausMathlib.directSupport_nonempty_of_represents {core factor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (hcore_primitive : core.Primitive) (hval : ModPFactorization core data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) (hnorm : Hex.normalizeFactorSign factor = factor) (hrep : RepresentsIntegerFactorModP data factor S) : Finset.Nonempty S

The modular support representing a positive-degree irreducible integer divisor is nonempty.

noncomputable def HexBerlekampZassenhausMathlib.directFactorCertificate {core factor : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} {S : ModPFactorSubset data} (hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p) (hval : ModPFactorization core data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hirr : Irreducible (HexPolyZMathlib.toPolynomial factor)) (hdvd : factor ∣ core) (hnorm : Hex.normalizeFactorSign factor = factor) (hrep : RepresentsIntegerFactorModP data factor S) : DirectFactorCertificate core B data S

Package a normalized irreducible divisor and its direct modular support as the single certificate consumed by the CLD proof.

Equations

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

def HexBerlekampZassenhausMathlib.directTrueSupports (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) : Set (Set (LiftedFactorIndex (core.directLiftData B data)))

The direct-coordinate true supports seen by the CLD lattice. The carrier is the canonical lift of a modular support and the witness is the exact factor certificate for that same support.

Equations

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

theorem HexBerlekampZassenhausMathlib.directTrueSupports.cover {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p) (hval : ModPFactorization core data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hpartition : DirectSupportPartition core B data Finset.univ core) (i : LiftedFactorIndex (core.directLiftData B data)) : ∃ U ∈ directTrueSupports core B data, i ∈ U

The full direct support partition covers every lifted factor index.

theorem HexBerlekampZassenhausMathlib.directTrueSupports.eq_of_mem_inter {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hpartition : DirectSupportPartition core B data Finset.univ core) (U : Set (LiftedFactorIndex (core.directLiftData B data))) : U ∈ directTrueSupports core B data → ∀ V ∈ directTrueSupports core B data, ∀ i ∈ U, i ∈ V → U = V

Two direct true supports containing the same lifted index are equal.

theorem HexBerlekampZassenhausMathlib.directTrueSupports.nonempty {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (U : Set (LiftedFactorIndex (core.directLiftData B data))) : U ∈ directTrueSupports core B data → U.Nonempty

Every certified direct support is nonempty.

theorem HexBerlekampZassenhausMathlib.directTrueSupports.ncard_eq_normalizedFactors_card {core : Hex.ZPoly} {B : ℕ} {data : Hex.PrimeChoiceData} (hcore_primitive : core.Primitive) (hcore_lc_pos : 0 < Hex.DensePoly.leadingCoeff core) (hrecovery : 2 * core.defaultFactorCoeffBound < data.p ^ Hex.precisionForCoeffBound B data.p) (hval : ModPFactorization core data) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) (hpartition : DirectSupportPartition core B data Finset.univ core) (hcore_ne : core ≠ 0) : (directTrueSupports core B data).ncard = (UniqueFactorizationMonoid.normalizedFactors (HexPolyZMathlib.toPolynomial core)).card

Direct true supports are in bijection with the normalized irreducible factors of the primitive square-free part.