def HexBerlekampZassenhaus.FactorTactic.evalZPoly (tactic : String) (e : Lean.Expr) : Lean.MetaM Hex.ZPoly

Evaluate a closed Hex.ZPoly expression to its runtime value at elaboration time.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.witnessPrimes : List Nat

Candidate primes for the single-prime witness search.

Equations

• HexBerlekampZassenhaus.FactorTactic.witnessPrimes = List.filter Hex.Nat.isPrimeTrial (List.range 512)

def HexBerlekampZassenhaus.FactorTactic.searchModPWitness (q : Hex.ZPoly) : Option Hex.ZPoly.ModPWitness

Search for a single-prime modular witness for q (already known non-constant, non-linear). Returns none when no candidate prime works; either q is reducible, or it is balanced at every candidate prime.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.eisensteinShifts : List Int

The shifts tried by the Eisenstein-after-shift search, in order.

Equations

• HexBerlekampZassenhaus.FactorTactic.eisensteinShifts = [0, 1, -1, 2, -2, 3, -3]

def HexBerlekampZassenhaus.FactorTactic.eisensteinPrimeCap : Nat

Fixed breadth limit for the auxiliary Eisenstein witness search. Raising it expands coefficient-divisor enumeration and should be benchmarked as a separate tactic-coverage change; the current boundary witness checkIrredWitness (X² − 127) (.eisenstein 127 0) is locked by a test.

Equations

• HexBerlekampZassenhaus.FactorTactic.eisensteinPrimeCap = 128

def HexBerlekampZassenhaus.FactorTactic.smallPrimeDivisors (n : Nat) : List Nat

Prime divisors of n up to eisensteinPrimeCap, by trial division. Any cofactor above the cap is dropped because the Eisenstein witness search is deliberately bounded.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.searchEisenstein (f : Hex.ZPoly) : Option Hex.ZPoly.IrredWitness

Search for an Eisenstein-after-shift witness for f: for each candidate shift s, the candidate primes are the small prime divisors of the constant term of translate s f, and each candidate is validated by running the full checkIrredWitness Boolean check. First hit wins.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.searchWitness (q : Hex.ZPoly) : Option Hex.ZPoly.IrredWitness

Search for an irreducibility witness for q.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.reifyModPWitness (w : Hex.ZPoly.ModPWitness) : Lean.Expr

Reify a ModPWitness as a constructor application over reified pieces.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.reifyWitness : Hex.ZPoly.IrredWitness → Lean.Expr

Reify an IrredWitness.

Equations

• HexBerlekampZassenhaus.FactorTactic.reifyWitness Hex.ZPoly.IrredWitness.primeConst = Lean.mkConst `Hex.ZPoly.IrredWitness.primeConst
• HexBerlekampZassenhaus.FactorTactic.reifyWitness Hex.ZPoly.IrredWitness.linear = Lean.mkConst `Hex.ZPoly.IrredWitness.linear
• HexBerlekampZassenhaus.FactorTactic.reifyWitness (Hex.ZPoly.IrredWitness.modP w) = Lean.mkApp (Lean.mkConst `Hex.ZPoly.IrredWitness.modP) (HexBerlekampZassenhaus.FactorTactic.reifyModPWitness w)
• HexBerlekampZassenhaus.FactorTactic.reifyWitness (Hex.ZPoly.IrredWitness.eisenstein q shift) = Lean.mkApp2 (Lean.mkConst `Hex.ZPoly.IrredWitness.eisenstein) (Lean.mkNatLit q) (Lean.toExpr shift)

def HexBerlekampZassenhaus.FactorTactic.listLit (ty : Lean.Expr) (xs : List Lean.Expr) : Lean.Expr

Literal List expression (shared shape with the FpPoly elaborator).

Equations

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

def HexBerlekampZassenhaus.FactorTactic.dedupZPolys (l : List Hex.ZPoly) : List Hex.ZPoly

Deduplicate a ZPoly list by coefficient equality (order-preserving).

Equations

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

def HexBerlekampZassenhaus.FactorTactic.balancedDecline (tactic : String) (q : Hex.ZPoly) : Lean.MetaM Lean.MessageData

The balanced-factor decline diagnostic.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.checkTransparent (tactic : String) (f : Hex.ZPoly) (fE : Lean.Expr) : Lean.MetaM Lean.Expr

Checks that the user's term is definitionally transparent down to its evaluated literal.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.factorPolyZPoly (zeroE decE fE : Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

The factor_poly arm: factorize, certify each distinct factor by an IrredWitness, and emit a reified Hex.ZPoly.Factored. Declines when some factor has no free-layer witness.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.irredProof (fE : Lean.Expr) (f : Hex.ZPoly) : Lean.MetaM (Except Lean.MessageData Lean.Expr)

The irreducibility proof for a runtime ZPoly and its expression: shared by the term arm and goal mode.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.irreducibilityZPoly (fE : Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

The irreducibility term arm.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.goalIrredZPoly (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Hex.FactorTactic.ExtensionResult

Goal mode: close Hex.ZPoly.Irreducible e.

Equations

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

def HexBerlekampZassenhaus.FactorTactic.extension : Hex.FactorTactic.Extension

The Hex.ZPoly extension, checked by name from Hex.FactorTactic.extensionNames; the free and integration regression tests fail if a rename makes the extension undiscoverable.

Equations

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