inductive Hex.DeclineReason : Type

Why the bounded direct classical engine declined.

• noGoodPrime : DeclineReason

  No admissible modular factorization was found.

• subsetBudget : DeclineReason

  The next complete subset-cardinality level exceeds the remaining budget.

• liftFailure : DeclineReason

  The modular factors could not be lifted to the required precision.

• largeSupport : DeclineReason

  The lifted support is routed to incremental partition replay.

• cardinalityCap : DeclineReason

  Every configured unforced cardinality was exhausted without a split.

• invalidCandidate : DeclineReason

  The search exhausted all allowed candidates without a valid split.

@[instance_reducible]

instance Hex.instDecidableEqDeclineReason : DecidableEq DeclineReason

Equations

• Hex.instDecidableEqDeclineReason x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hex.DeclineReason.name : DeclineReason → String

A short diagnostic name for a direct-search resource limit.

Equations

• Hex.DeclineReason.noGoodPrime.name = "noGoodPrime"
• Hex.DeclineReason.subsetBudget.name = "subsetBudget"
• Hex.DeclineReason.liftFailure.name = "liftFailure"
• Hex.DeclineReason.largeSupport.name = "largeSupport"
• Hex.DeclineReason.cardinalityCap.name = "cardinalityCap"
• Hex.DeclineReason.invalidCandidate.name = "invalidCandidate"

structure Hex.ClassicalStats : Type

Statistics from a direct classical attempt. completedLevels records the fully exhausted head-forced subset cardinalities, in execution order.

• prime : Nat

  The prime selected for the successful modular factorization, or zero.

• primeProbes : Nat

  The number of prime candidates examined.

• liftedFactorCount : Nat

  The number of lifted modular factors.

• henselLifts : Nat

  The number of quadratic Hensel lifts performed.

• candidatesTried : Nat

  The number of recombination candidates tested by exact division.

• completedLevels : Array Nat

  Subset cardinalities exhausted completely, in execution order.

• unforced : DirectCandidateStats

  Stage counters from the unforced low-cardinality sweep.

• unforcedCompletedLevels : Array Nat

  Unforced cardinalities exhausted completely, in execution order.

• peeledFactorDegrees : Array Nat

  Degrees peeled by the unforced sweep, in discovery order.

• peeledSupportSizes : Array Nat

  Selected lifted-support sizes of peeled factors.

• peeledComplementSizes : Array Nat

  Complementary support sizes after each successful peel.

• residualLiftedFactorCount : Nat

  Lifted factors left in the retained residual support.

• remainingSubsetBudget : Nat

  Candidate budget retained for the residual problem.

• unforcedDecline : Option DeclineReason

  Why the unforced sweep stopped, if it left a residual problem.

def Hex.instDecidableEqClassicalStats.decEq (x✝ x✝¹ : ClassicalStats) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.instDecidableEqClassicalStats : DecidableEq ClassicalStats

Equations

• Hex.instDecidableEqClassicalStats = Hex.instDecidableEqClassicalStats.decEq

inductive Hex.DirectHeadResult (basis : LiftData) : Type

Internal result of a head search.

• found {basis : LiftData} (split : DirectSplit basis) (budget candidates : Nat) (completed : Array Nat) : DirectHeadResult basis

  A factor and exact quotient were found.

• declined {basis : LiftData} (reason : DeclineReason) (budget candidates : Nat) (completed : Array Nat) : DirectHeadResult basis

  The bounded search stopped for the recorded reason.

def Hex.findDirectHead (coreLc : Int) (target : ZPoly) (basis : LiftData) (head : DirectLiftedIndex basis) (tail : List (DirectLiftedIndex basis)) (levels : List Nat) (budget candidates : Nat) (completed : Array Nat) : DirectHeadResult basis

Search complete cardinality levels only. If the next level does not fit, decline before evaluating any member of it.

Equations

• One or more equations did not get rendered due to their size.
• Hex.findDirectHead coreLc target basis head tail [] x✝² x✝¹ x✝ = Hex.DirectHeadResult.declined Hex.DeclineReason.invalidCandidate x✝² x✝¹ x✝

inductive Hex.DirectSearchResult : Type

Internal recursive result.

• factored (factors : List ZPoly) (budget : Nat) (stats : ClassicalStats) : DirectSearchResult

  The recursive search produced a complete factor list.

• declined (reason : DeclineReason) (budget : Nat) (stats : ClassicalStats) : DirectSearchResult

  The recursive search stopped for the recorded reason.

def Hex.searchDirectAux (coreLc : Int) (basis : LiftData) : Nat → ZPoly → List (DirectLiftedIndex basis) → Nat → ClassicalStats → DirectSearchResult

Search recursively for direct-coordinate factors within the remaining budget.

Equations

• One or more equations did not get rendered due to their size.
• Hex.searchDirectAux coreLc basis 0 x✝³ x✝² x✝¹ x✝ = Hex.DirectSearchResult.declined Hex.DeclineReason.liftFailure x✝¹ x✝
• Hex.searchDirectAux coreLc basis fuel.succ x✝² [] x✝¹ x✝ = if x✝² = 1 then Hex.DirectSearchResult.factored [] x✝¹ x✝ else Hex.DirectSearchResult.declined Hex.DeclineReason.liftFailure x✝¹ x✝

def Hex.searchDirect (coreLc : Int) (target : ZPoly) (basis : LiftData) (budget : Nat := defaultSubsetBudget) (stats : ClassicalStats := { }) : DirectSearchResult

Run the direct search with one shared top-level candidate budget.

Equations

• Hex.searchDirect coreLc target basis budget stats = Hex.searchDirectAux coreLc basis (basis.liftedFactors.size + 1) target (List.finRange basis.liftedFactors.size) budget stats

inductive Hex.DirectSweepResult (basis : LiftData) : Type

Result of one sequence of complete unforced cardinality sweeps.

• found {basis : LiftData} (split : DirectSplit basis) (budget : Nat) (stats : DirectCandidateStats) (completed : Array Nat) : DirectSweepResult basis

  A factor and exact quotient were found.

• stopped {basis : LiftData} (reason : DeclineReason) (budget : Nat) (stats : DirectCandidateStats) (completed : Array Nat) : DirectSweepResult basis

  No factor was found, or the next complete level exceeded the budget.

def Hex.findDirectSubset (coreLc : Int) (target : ZPoly) (basis : LiftData) (lift : LiftSupport basis) (image : TargetImage target) (support : List (DirectLiftedIndex basis)) (levels : List Nat) (budget : Nat) (stats : DirectCandidateStats) (completed : Array Nat) : DirectSweepResult basis

Search complete unforced cardinality levels without materializing subsets.

The whole cardinality schedule runs against one residual, so the one reduction of that residual is reused by every level.

Equations

• One or more equations did not get rendered due to their size.
• Hex.findDirectSubset coreLc target basis lift image support [] x✝² x✝¹ x✝ = Hex.DirectSweepResult.stopped Hex.DeclineReason.cardinalityCap x✝² x✝¹ x✝

structure Hex.DirectPartialFactorization (basis : LiftData) : Type

An exact partial factorization together with its indexed lifted support.

This is computational proposal state, not an irreducibility certificate. The public factorizer only consumes it after exact reconstruction and proved classical replay.

• factors : Array ZPoly

  Exact factors already peeled from the original target.

• residual : ZPoly

  Exact quotient remaining after the peeled factors.

• support : List (DirectLiftedIndex basis)

  Complementary lifted support for residual.

• budget : Nat

  Candidate budget not consumed by complete sweeps.

• stats : ClassicalStats

  Measurements accumulated by the partial search.

def Hex.peelDirectAux (coreLc : Int) (basis : LiftData) (lift : LiftSupport basis) (repeatLevels : List Nat) : Nat → ZPoly → List (DirectLiftedIndex basis) → Array ZPoly → Nat → ClassicalStats → List Nat → DirectPartialFactorization basis

Repeatedly peel exact factors from one lifted basis. levels controls the first sweep; after every split, the smaller repeatLevels schedule is restarted on the exact quotient and complementary support.

lift is the traversal data of the basis, which every sweep shares. The residual's image in F_q[X] is rebuilt here, once per nonunit residual reaching findDirectSubset: an exact split replaces the residual, so the previous reduction describes a polynomial the search has left behind. The reduction is built before that call rather than inside it, so a residual whose schedule is empty or whose first level does not fit the budget still pays for one.

Equations

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

def Hex.peelDirect (coreLc : Int) (target : ZPoly) (basis : LiftData) (maxCardinality : Nat := 3) (repeatCardinality : Nat := 2) (budget : Nat := defaultSubsetBudget) (stats : ClassicalStats := { }) : DirectPartialFactorization basis

Retain every cheap exact factor exposed by one Hensel lift. The first sweep admits support sizes up to maxCardinality; subsequent sweeps use the smaller repeatCardinality cap so progress is reused without repeatedly paying for the widest combinatorial level. The basis is lifted once, so its traversal data is prepared once here and shared by every sweep.

Equations

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