def HexBerlekampZassenhausMathlib.modPIndexOfLiftedIndex (data : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = data.factorsModP.size) (i : LiftedFactorIndex d) : ModPFactorIndex data

Inverse index transport for a lift whose factor count is preserved.

Equations

• HexBerlekampZassenhausMathlib.modPIndexOfLiftedIndex data d hsize i = Fin.cast hsize i

def HexBerlekampZassenhausMathlib.liftedIndexToModPEmbedding (data : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = data.factorsModP.size) : LiftedFactorIndex d ↪ ModPFactorIndex data

Embedding form of the inverse index transport.

Equations

• HexBerlekampZassenhausMathlib.liftedIndexToModPEmbedding data d hsize = { toFun := HexBerlekampZassenhausMathlib.modPIndexOfLiftedIndex data d hsize, inj' := ⋯ }

def HexBerlekampZassenhausMathlib.modPSubsetOfLiftedSubset (data : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = data.factorsModP.size) (S : LiftedFactorSubset d) : ModPFactorSubset data

Transport a lifted support back to the unique modular support.

Equations

• HexBerlekampZassenhausMathlib.modPSubsetOfLiftedSubset data d hsize S = Finset.map (HexBerlekampZassenhausMathlib.liftedIndexToModPEmbedding data d hsize) S

theorem HexBerlekampZassenhausMathlib.liftedSubset_modPSubset (data : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = data.factorsModP.size) (S : LiftedFactorSubset d) : liftedSubsetOfModPSubset data d hsize (modPSubsetOfLiftedSubset data d hsize S) = S

The two support transports are inverse in the lifted coordinate.

theorem HexBerlekampZassenhausMathlib.modPSubset_liftedSubset (data : Hex.PrimeChoiceData) (d : Hex.LiftData) (hsize : d.liftedFactors.size = data.factorsModP.size) (S : ModPFactorSubset data) : modPSubsetOfLiftedSubset data d hsize (liftedSubsetOfModPSubset data d hsize S) = S

The two support transports are inverse in the modular coordinate.

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

Semantic facts attached to the one direct-coordinate lift.

• targetMonic : Hex.DensePoly.Monic (core.monicTarget data.p (Hex.precisionForCoeffBound B data.p))

  The polynomial lifted in the direct coordinates is monic.

• invariant : Hex.ZPoly.QuadraticMultifactorLiftInvariant data.p (Hex.precisionForCoeffBound B data.p) (core.monicTarget data.p (Hex.precisionForCoeffBound B data.p)) (Array.map Hex.FpPoly.liftToZ data.factorsModP).toList

  The lifted factors satisfy the multifactor Hensel invariant.

• productModP : (Array.map Hex.FpPoly.liftToZ data.factorsModP).polyProduct.congr (core.monicTarget data.p (Hex.precisionForCoeffBound B data.p)) data.p

  The initial lifted product agrees with the direct target modulo p.

• liftedMonic (i : LiftedFactorIndex (core.directLiftData B data)) : Hex.DensePoly.Monic (liftedFactor (core.directLiftData B data) i)

  Every resulting lifted factor is monic.

• liftedModP (i : ModPFactorIndex data) : Hex.ZPoly.modP data.p (liftedFactor (core.directLiftData B data) (liftedIndexOfModPIndex data (core.directLiftData B data) ⋯ i)) = modPFactor data i

  Each lifted factor reduces to its corresponding modular factor.

• subsetProductMap (S : ModPFactorSubset data) : let d := core.directLiftData B data; let hsize := ⋯; Polynomial.map (Int.castRingHom (ZMod data.p)) (HexPolyZMathlib.toPolynomial (liftedFactorProduct d (liftedSubsetOfModPSubset data d hsize S))) = HexPolyFpMathlib.toMathlibPolynomial (modPFactorProduct data S)

  Reduction maps every selected lifted product to the same modular product.

theorem HexBerlekampZassenhausMathlib.directLiftFacts (core : Hex.ZPoly) (B : ℕ) (data : Hex.PrimeChoiceData) (hval : ModPFactorization core data) (hcore_size : 0 < Hex.DensePoly.size core) (hprecision : 1 ≤ Hex.precisionForCoeffBound B data.p) (hgcd : (Hex.DensePoly.leadingCoeff core).gcd (Int.ofNat (data.p ^ Hex.precisionForCoeffBound B data.p)) = 1) : DirectLiftFacts core B data

Construct the semantic bundle from the selected direct modular factorization and validated lift precision.