inductive Hex.ClassicalOutcome : Type

Result of direct classical factorization.

• factored (factors : Array ZPoly) (stats : ClassicalStats) : ClassicalOutcome

  Direct recombination produced a complete factor array.

• declined (reason : DeclineReason) (stats : ClassicalStats) : ClassicalOutcome

  Direct recombination stopped for the recorded resource reason.

def Hex.instDecidableEqClassicalOutcome.decEq (x✝ x✝¹ : ClassicalOutcome) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Hex.instDecidableEqClassicalOutcome.decEq (Hex.ClassicalOutcome.factored factors stats) (Hex.ClassicalOutcome.declined reason stats_1) = isFalse ⋯
• Hex.instDecidableEqClassicalOutcome.decEq (Hex.ClassicalOutcome.declined reason stats) (Hex.ClassicalOutcome.factored factors stats_1) = isFalse ⋯

@[instance_reducible]

instance Hex.instDecidableEqClassicalOutcome : DecidableEq ClassicalOutcome

Equations

• Hex.instDecidableEqClassicalOutcome = Hex.instDecidableEqClassicalOutcome.decEq

def Hex.validDirectFactors (core : ZPoly) (factors : List ZPoly) : Bool

Directly checkable output invariants at the executable boundary. The Mathlib theorem proves these facts and irreducibility; this guard also keeps a malformed low-level result from escaping in non-proof consumers.

Equations

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

def Hex.factorDirectCoreOfPlan (core : SquareFreeInput) (modular : DirectPrimePlan core) (budget : Nat := defaultSubsetBudget) : ClassicalOutcome

One lift and one greedy direct recombination search from an existing prime plan. Keeping planning outside this function lets the total selector reuse the plan if the bounded search declines.

Equations

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

def Hex.factorDirectCore (core : SquareFreeInput) (budget : Nat := defaultSubsetBudget) : ClassicalOutcome

Plan once, then run the direct classical engine.

Equations

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