def Hex.directCandidate (coreLc : Int) (modulus : Nat) (selected : List ZPoly) : ZPoly

Reconstruct an original-coordinate candidate from selected monic Hensel factors.

Equations

• Hex.directCandidate coreLc modulus selected = Hex.normalizeFactorSign (Hex.centeredLiftPoly (Hex.DensePoly.scale coreLc selected.toArray.polyProduct) modulus).primitivePart

def Hex.intDivides (multiple divisor : Int) : Bool

Exact integer divisibility with a magnitude rejection before remainder calculation. The arguments are the prospective multiple and divisor.

Equations

• Hex.intDivides multiple divisor = if multiple.natAbs < divisor.natAbs ∧ multiple ≠ 0 then false else multiple % divisor == 0

@[simp]

theorem Hex.intDivides_eq (multiple divisor : Int) : intDivides multiple divisor = (multiple % divisor == 0)

The guarded integer divisibility test agrees with a zero-remainder test.

def Hex.directDegreePrefilter (coreLc : Int) (target : ZPoly) (degreeSum : Nat) : Bool

Cached degree prefilter for a direct candidate.

Equations

• Hex.directDegreePrefilter coreLc target degreeSum = (coreLc == 0 || decide (target = 0) || decide (degreeSum ≤ Hex.DensePoly.natDegree target))

def Hex.directTrailingPrefilter (coreLc : Int) (target : ZPoly) (modulus : LiftModulus) (trailingResidue : Int) : Bool

Cached trailing-coefficient prefilter for a direct candidate.

The modulus arrives prepared, so the leaf reduces against the integer value the traversal already holds rather than rebuilding it.

Equations

• Hex.directTrailingPrefilter coreLc target modulus trailingResidue = Hex.intDivides (coreLc * Hex.DensePoly.coeff target 0) (modulus.centered (coreLc * trailingResidue))

@[simp]

theorem Hex.directTrailingPrefilter_eq (coreLc : Int) (target : ZPoly) (modulus : LiftModulus) (trailingResidue : Int) : directTrailingPrefilter coreLc target modulus trailingResidue = intDivides (coreLc * DensePoly.coeff target 0) (centeredModNat (coreLc * trailingResidue) modulus.nat)

The prepared prefilter tests divisibility by the centred representative.

def Hex.directCandidatePrefilter (coreLc : Int) (target : ZPoly) (modulus : LiftModulus) (degreeSum : Nat) (trailingResidue : Int) : Bool

Cached degree/trailing-coefficient prefilter for a direct candidate.

The selected Hensel factors are monic. At recovery precision the centered leading coefficient is coreLc, so the selected product has the supplied degree. If its primitive part divides target, its centered constant coefficient divides coreLc * target(0). Both checks happen before the polynomial product is formed. Conservative zero cases are retained for the standalone executable surface.

Equations

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

def Hex.directCandidateAfterPrefilter (coreLc : Int) (target : ZPoly) (modulus : Nat) (selected : List ZPoly) : Option (ZPoly × ZPoly)

The candidate computation itself, for a selection the cached prefilters have already accepted. The streaming traversal runs the prefilter itself, so that it can decide whether to build selected at all, and then calls this rather than paying for the prefilter twice.

Equations

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

def Hex.directCandidateAfterObstruction (coreLc : Int) (target : ZPoly) (cached : TargetImage target) (modulus : Nat) (selected : List ZPoly) : Option (ZPoly × ZPoly)

The candidate computation for a selection the cached prefilters accepted, with the word-prime divisibility obstruction ahead of exact integer division.

obstructs fires only on candidates that provably do not divide the target, so the value returned is directCandidateAfterPrefilter's. What changes is that a candidate the obstruction rejects is never put to multi-limb integer long division.

Equations

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

theorem Hex.directCandidateAfterObstruction_eq (coreLc : Int) (target : ZPoly) (cached : TargetImage target) (modulus : Nat) (selected : List ZPoly) : directCandidateAfterObstruction coreLc target cached modulus selected = directCandidateAfterPrefilter coreLc target modulus selected

Skipping an obstructed candidate's exact division changes nothing: exact division would have returned none on it.

def Hex.tryDirectCandidate (coreLc : Int) (target : ZPoly) (modulus : LiftModulus) (selected : List ZPoly) (degreeSum : Nat) (trailingResidue : Int) : Option (ZPoly × ZPoly)

Evaluate the candidate computation after the cached prefilters.

Equations

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