def Hex.recombinationSearch (f : ZPoly) (localFactors : List ZPoly) : Option (List ZPoly)

Search for an integer-factor recombination of the lifted local factors.

The search enumerates subsets containing the first remaining local factor, accepts a subset only when its product exactly divides the current target, and then recurses on the quotient and unused local factors.

Equations

• Hex.recombinationSearch f localFactors = Hex.recombinationSearchAux✝ f localFactors (localFactors.length + 1)

def Hex.recombinationSearchModAux (target : ZPoly) (modulus : Nat) (localFactors : List ZPoly) : Nat → Option (List ZPoly)

Fuelled auxiliary for recombinationSearchMod. Recurses through subsetSplitsWithFirst localFactors: at every level the head local factor is forced into the candidate, the centred-lift result is normalised and checked against shouldRecordPolynomialFactor, and a successful exactQuotient? divides the search down to the remaining local factors and quotient.

Equations

• One or more equations did not get rendered due to their size.
• Hex.recombinationSearchModAux target modulus localFactors 0 = none

def Hex.recombinationSearchMod (f : ZPoly) (modulus : Nat) (localFactors : List ZPoly) : Option (List ZPoly)

Exhaustive lifted-factor recombination search at a fixed modulus. Drives the slow path by iterating subsets of the lifted local factors through recombinationSearchModAux.

Equations

• Hex.recombinationSearchMod f modulus localFactors = Hex.recombinationSearchModAux f modulus localFactors (localFactors.length + 1)

def Hex.recombineExhaustive (f : ZPoly) (d : LiftData) : Array ZPoly

Exhaustive recombination of the lifted local factors stored in d, run at the Hensel modulus p^k = liftModulus d. Returns the recovered integer factors as an array on success and #[] when the search fails.

Equations

• Hex.recombineExhaustive f d = match Hex.recombinationSearchMod f (Hex.liftModulus d) d.liftedFactors.toList with | some factors => factors.toArray | none => #[]

def Hex.subsetsOfSizeWithComplement {α : Type} : List α → Nat → List (List α × List α)

Size-k sublists of xs, each paired with its complement, order preserved in both components. The size-class building block of the size-ordered classical recombination search.

Equations

• One or more equations did not get rendered due to their size.
• Hex.subsetsOfSizeWithComplement x✝ 0 = [([], x✝)]
• Hex.subsetsOfSizeWithComplement [] n.succ = []

def Hex.initialHenselPrecision (B : Nat) : Nat

Initial Hensel precision used by the fast BHKS doubling schedule.

Equations

• Hex.initialHenselPrecision B = if B ≤ 4 then B else 4

def Hex.nextHenselPrecision (k B : Nat) : Nat

Successor precision used by the fast BHKS doubling schedule.

Equations

• Hex.nextHenselPrecision k B = if 2 * k < B then 2 * k else B

def Hex.ZPoly.toMonicLiftData (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : LiftData

Build the fixed-precision Hensel lift data for the monic transform of an square-free part. The exhaustive slow path still recombines against the original primitive polynomial, but the lift stage sees the monic polynomial required by the Hensel computation.

Equations

• core.toMonicLiftData B primeData = Hex.henselLiftData core.toMonic.monic (Hex.precisionForCoeffBound B primeData.p) primeData

def Hex.ZPoly.leadingCoeffInverse (core : ZPoly) (p k : Nat) : Int

Multiplicative inverse of core's leading coefficient modulo p ^ k, read off the integer Bezout certificate s · ℓf + t · p^k = gcd(ℓf, p^k). When gcd(leadingCoeff core, p ^ k) = 1 (the good-prime condition p ∤ ℓf) this is a genuine inverse: leadingCoeffInverse core p k * leadingCoeff core ≡ 1 (mod p^k) (leadingCoeffInverse_mul_emod).

Equations

• core.leadingCoeffInverse p k = (HexArith.Int.extGcd (Hex.DensePoly.leadingCoeff core) (Int.ofNat (p ^ k))).snd.fst

def Hex.ZPoly.monicTarget (core : ZPoly) (p k : Nat) : ZPoly

BHKS leading-coefficient-faithful monic target for core: rescale core by the modular inverse of its leading coefficient, then reduce modulo p ^ k.

This is van Hoeij's M1 normalisation (factor out ℓf, BHKS §2: f = ℓf·f₁···fr with the fᵢ monic in Z_p), distinct from the toMonic x ↦ x/ℓf substitution (M2). Over (ℤ/p^k)[x] it equals core · ℓf⁻¹, so its monic local factors divide core directly with no dilation. It is monic over ℤ when gcd(leadingCoeff core, p ^ k) = 1 and core is nonconstant (monicTarget_monic).

Equations

• core.monicTarget p k = Hex.ZPoly.reduceModPow (Hex.DensePoly.scale (core.leadingCoeffInverse p k) core) p k

def Hex.ZPoly.directLiftData (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) : LiftData

Fixed-precision Hensel lift data over core's own coordinate (BHKS-faithful).

Mirrors toMonicLiftData, but lifts core's monic modular factors against the leading-coefficient-normalised monicTarget rather than the x ↦ x/ℓf dilation (toMonic core).monic. The lifted factors therefore divide core in (ℤ/p^a)[x] directly, and the CLD lattice runs over core's own coordinate.

Equations

• core.directLiftData B primeData = Hex.henselLiftData (core.monicTarget primeData.p (Hex.precisionForCoeffBound B primeData.p)) (Hex.precisionForCoeffBound B primeData.p) primeData

theorem Hex.ZPoly.leadingCoeffInverse_mul_emod (core : ZPoly) (p k : Nat) (hpk : 1 < p ^ k) (hgcd : (DensePoly.leadingCoeff core).gcd (Int.ofNat (p ^ k)) = 1) : core.leadingCoeffInverse p k * DensePoly.leadingCoeff core % Int.ofNat (p ^ k) = 1

The leadingCoeffInverse is a genuine inverse of core's leading coefficient modulo p ^ k when the leading coefficient is coprime to p ^ k (the good-prime condition p ∤ ℓf). This is the unit-residue fact the BHKS monic target rests on.

theorem Hex.ZPoly.reduceModPow_size_le (f : ZPoly) (p k : Nat) : DensePoly.size (f.reduceModPow p k) ≤ DensePoly.size f

Size of reduceModPow is bounded by the source size (trimming only drops trailing zeros).

theorem Hex.ZPoly.monicTarget_size_eq (core : ZPoly) (p k : Nat) (hpk : 1 < p ^ k) (hgcd : (DensePoly.leadingCoeff core).gcd (Int.ofNat (p ^ k)) = 1) (hcore : 0 < DensePoly.size core) : DensePoly.size (core.monicTarget p k) = DensePoly.size core

The direct-coordinate monic target has exactly the input polynomial's size. Reduction cannot add coefficients, while coprimality makes its top coefficient equal to one, so reduction cannot discard the input's top degree.

theorem Hex.ZPoly.monicTarget_monic (core : ZPoly) (p k : Nat) (hpk : 1 < p ^ k) (hgcd : (DensePoly.leadingCoeff core).gcd (Int.ofNat (p ^ k)) = 1) (hcore : 0 < DensePoly.size core) : DensePoly.Monic (core.monicTarget p k)

The BHKS leading-coefficient-faithful monic target is genuinely monic over ℤ when core's leading coefficient is coprime to p ^ k and core is nonconstant.

This is the load-bearing soundness fact for handling the existing monic Hensel lift against monicTarget (van Hoeij M1) instead of the toMonic x ↦ x/ℓf dilation (M2): the lift's producer lemma QuadraticMultifactorLiftInvariant_of_choosePrimeData requires its target monic, and monicTarget supplies that while keeping core's own coordinate.

def Hex.cldCoeffFloor (core : ZPoly) : Nat

CLD column-adequacy floor for the fast recovery acceptance condition.

A successful BHKS recovery at schedule coefficient bound k only certifies column adequacy (the BHKS Lemma 5.7 separation hsep) once the lift precision precisionForCoeffBound k primeData.p clears the per-coordinate CLD threshold. The lattice and its CLD columns are built directly over core, so the floor is twice the largest per-coordinate bound of core itself.

Equations

• Hex.cldCoeffFloor core = 2 * List.foldl (fun (acc j : Nat) => max acc (Hex.bhksCoeffBound core j)) 0 (List.range (Hex.DensePoly.natDegree core + 1))

def Hex.bhksRecoveryFloor (core : ZPoly) : Nat

Acceptance floor for the fast recovery loop: the CLD column-adequacy floor cldCoeffFloor joined with the direct Mignotte recovery bound of core.

Equations

• Hex.bhksRecoveryFloor core = max (Hex.cldCoeffFloor core) core.defaultFactorCoeffBound

theorem Hex.cldCoeffFloor_le_bhksRecoveryFloor (core : ZPoly) : cldCoeffFloor core ≤ bhksRecoveryFloor core

The recovery floor is at least the logarithmic-derivative coefficient floor.

theorem Hex.defaultFactorCoeffBound_le_bhksRecoveryFloor (core : ZPoly) : core.defaultFactorCoeffBound ≤ bhksRecoveryFloor core

The recovery floor is at least the direct coefficient-recovery bound.

@[irreducible]

def Hex.bhksRecoveryThreshold (core : ZPoly) : Nat

An irreducible copy of the acceptance floor used when reducing the fast loop.

Definitionally bhksRecoveryFloor, but marked irreducible so that whnf in downstream proofs that case-split on a bhksRecoveryCoreWithBound application does not eagerly expand the (symbolic, structurally large) floor computation while reducing the loop's head if. The loop's behavioural unfolding lemma bhksRecoveryCoreWithBound_unfold re-exposes the plain bhksRecoveryFloor comparison, so proofs reason about the genuine floor.

Equations

• Hex.bhksRecoveryThreshold core = Hex.bhksRecoveryFloor core

theorem Hex.bhksRecoveryThreshold_eq (core : ZPoly) : bhksRecoveryThreshold core = bhksRecoveryFloor core

The opaque recovery threshold equals its mathematical coefficient floor.

def Hex.bhksRecoveryCoreWithBound (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) (k fuel : Nat) : Option (Array ZPoly)

BHKS fast recovery recombination loop. Computes the CLD column-adequacy floor once (through the irreducible bhksRecoveryThreshold, so whnf in downstream proofs that case-split on this application does not eagerly expand the symbolic floor) and runs bhksRecoveryLoop.

Equations

• Hex.bhksRecoveryCoreWithBound core B primeData k fuel = Hex.bhksRecoveryLoop✝ core B (Hex.bhksRecoveryThreshold core) primeData k fuel

def Hex.henselPrecisionSchedule (B : Nat) : Nat → Nat → List Nat

Finite list of Hensel precisions inspected by the fast BHKS recovery loop.

Equations

• Hex.henselPrecisionSchedule B x✝ 0 = []
• Hex.henselPrecisionSchedule B x✝ fuel.succ = x✝ :: if x✝ ≥ B then [] else Hex.henselPrecisionSchedule B (Hex.nextHenselPrecision x✝ B) fuel

theorem Hex.cap_mem_henselPrecisionSchedule (B : Nat) : B ∈ henselPrecisionSchedule B (initialHenselPrecision B) (ZPoly.quadraticDoublingSteps B + 2)

The fast-path cap B is itself a member of the canonical Hensel precision schedule the executable loop walks: henselPrecisionSchedule B (initialHenselPrecision B) (quadraticDoublingSteps B + 2).

This is the connective schedule lemma used by the Mathlib-facing Group D forward-recovery wrapper: callers who supply ForwardRecoveryInputs at the canonical terminal precision no longer need to re-prove the executable doubling-schedule membership obligation.

theorem Hex.bhksRecoveryCoreWithBound_eq_some_of_recovery_on_schedule_of_no_prior_recovery (core : ZPoly) (B : Nat) (primeData : PrimeChoiceData) {start fuel target : Nat} {factors : Array ZPoly} (hfloor : bhksRecoveryFloor core ≤ target) (hmem : target ∈ henselPrecisionSchedule B start fuel) (hno : ∀ (k : Nat), k ∈ henselPrecisionSchedule B start fuel → k ≠ target → bhksRecover? core (core.directLiftData k primeData) = none) (hrecover : bhksRecover? core (core.directLiftData target primeData) = some factors) : bhksRecoveryCoreWithBound core B primeData start fuel = some factors

If a target precision is on the fast recovery schedule, recovery succeeds there, and no other scheduled precision before the target succeeds, then the first-success loop returns exactly the target recovery.

This is the executable-loop determinism skeleton. The BHKS precision theorem supplies the hno premise by ruling out successful recovery below the Mignotte/cap precision.