structure Hex.DirectLiftPlan (core : SquareFreeInput) (modular : DirectPrimePlan core) : Type

Validated recovery precision for one direct modular plan. There is no B = 0 meaning: construction fixes the ordinary Mignotte recovery bound and the corresponding positive Hensel exponent.

@[instance_reducible]

instance Hex.instDecidableEqDirectLiftPlan {core✝ : SquareFreeInput} {modular✝ : DirectPrimePlan core✝} : DecidableEq (DirectLiftPlan core✝ modular✝)

Equations

• Hex.instDecidableEqDirectLiftPlan = Hex.instDecidableEqDirectLiftPlan.decEq

def Hex.instDecidableEqDirectLiftPlan.decEq {core✝ : SquareFreeInput} {modular✝ : DirectPrimePlan core✝} (x✝ x✝¹ : DirectLiftPlan core✝ modular✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.instDecidableEqDirectLiftPlan.decEq { } { } = isTrue ⋯

def Hex.DirectLiftPlan.canonical (core : SquareFreeInput) (modular : DirectPrimePlan core) : DirectLiftPlan core modular

The unique recovery plan indexed by a square-free part and its selected modular factorization.

Equations

• Hex.DirectLiftPlan.canonical core modular = { }

def Hex.DirectLiftPlan.coeffBound {core : SquareFreeInput} {modular : DirectPrimePlan core} (_plan : DirectLiftPlan core modular) : Nat

Ordinary direct Mignotte coefficient bound.

Equations

• _plan.coeffBound = core.poly.defaultFactorCoeffBound

def Hex.DirectLiftPlan.precision {core : SquareFreeInput} {modular : DirectPrimePlan core} (plan : DirectLiftPlan core modular) : Nat

Recovery precision derived from the indexed polynomial, bound, and prime.

Equations

• plan.precision = Hex.precisionForCoeffBound plan.coeffBound modular.data.p

structure Hex.DirectLiftedBasis {core : SquareFreeInput} {modular : DirectPrimePlan core} (plan : DirectLiftPlan core modular) : Type

Token for the one direct-coordinate Hensel lift owned by a lift plan. The lifted data is derived from the indices rather than stored, so a basis from another square-free part or precision cannot be inserted.

def Hex.DirectLiftedBasis.canonical {core : SquareFreeInput} {modular : DirectPrimePlan core} (plan : DirectLiftPlan core modular) : DirectLiftedBasis plan

Construct the unique basis token for a recovery plan.

Equations

• Hex.DirectLiftedBasis.canonical plan = { }

def Hex.DirectLiftedBasis.data {core : SquareFreeInput} {modular : DirectPrimePlan core} {plan : DirectLiftPlan core modular} (_basis : DirectLiftedBasis plan) : LiftData

Execute the lift determined by the indexed recovery plan.

Equations

• _basis.data = core.poly.directLiftData plan.coeffBound modular.data

@[reducible, inline]

abbrev Hex.DirectLiftedIndex (basis : LiftData) : Type

Stable identity of a factor in the one direct lifted basis.

Equations

• Hex.DirectLiftedIndex basis = Fin basis.liftedFactors.size

def Hex.directLiftedFactor (basis : LiftData) (i : DirectLiftedIndex basis) : ZPoly

Fetch a lifted factor by its stable basis index.

Equations

• Hex.directLiftedFactor basis i = basis.liftedFactors[i]

def Hex.directLiftPlan (core : SquareFreeInput) (modular : DirectPrimePlan core) : DirectLiftPlan core modular

Recovery plan at the ordinary direct Mignotte bound.

Equations

• Hex.directLiftPlan core modular = Hex.DirectLiftPlan.canonical core modular

def Hex.directLiftedBasis (core : SquareFreeInput) (modular : DirectPrimePlan core) (plan : DirectLiftPlan core modular) : DirectLiftedBasis plan

Execute the unique Hensel lift owned by a direct recovery plan.

Equations

• Hex.directLiftedBasis core modular plan = Hex.DirectLiftedBasis.canonical plan