inductive Hex.FactorTactic.ExtensionResult : Type

Outcome of offering an input to an extension. notApplicable means the extension does not handle this input type at all (try the next silently); declined means it handles the type but cannot certify this input (try the next, keep the diagnostic for the final error); fatal aborts selection.

• notApplicable : ExtensionResult
• declined (why : Lean.MessageData) : ExtensionResult
• success (e : Lean.Expr) : ExtensionResult
• fatal (msg : Lean.MessageData) : ExtensionResult

structure Hex.FactorTactic.Extension : Type

Capabilities a downstream library registers to extend factor_poly/irreducibility to further input types. The arguments of the term hooks are the original syntax, the elaborated polynomial, its whnfR-normalized type, and the expected type of the surrounding elaboration.

• factorPoly? : Lean.Syntax → Lean.Expr → Lean.Expr → Option Lean.Expr → Lean.Elab.TermElabM ExtensionResult

  Handle a factor_poly p term elaboration.

• irreducibility? : Lean.Syntax → Lean.Expr → Lean.Expr → Option Lean.Expr → Lean.Elab.TermElabM ExtensionResult

  Handle an irreducibility p term elaboration.

• goalIrred? : Lean.MVarId → Lean.Elab.Tactic.TacticM ExtensionResult

  Handle goal-closing irreducibility on the given goal.

def Hex.FactorTactic.extensionNames : List Lean.Name

Well-known extension constants, checked in order. Downstream libraries declare a public meta def of type Extension under one of these names; adding an entry requires a HexBerlekamp release.

Equations

• Hex.FactorTactic.extensionNames = [`HexBerlekampZassenhaus.FactorTactic.extension, `HexBerlekampMathlib.FactorTactic.extension, `HexBerlekampZassenhausMathlib.FactorTactic.extension]

def Hex.FactorTactic.extensions : Lean.MetaM (List Extension)

All extensions present in the current environment, in lookup order, with the declared type checked before use.

Equations

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

inductive Hex.FactorTactic.PolyInput : Type

Classification of a factor_poly/irreducibility input by its whnfR-normalized type.

• fp (p : Nat) (pE boundsE RE zeroE decE : Lean.Expr) : PolyInput

  Hex.FpPoly p for a literal prime p, with the instance and coefficient-type expressions extracted from the input's type.

• zpoly (RE zeroE decE : Lean.Expr) : PolyInput

  Hex.ZPoly, with the instance expressions from the input's type.

• other : PolyInput

  Anything else (offered to extensions).

def Hex.FactorTactic.classify (ty : Lean.Expr) : Lean.MetaM PolyInput

Classify an input's type: DensePoly (ZMod64 p) → .fp, DensePoly Int → .zpoly, anything else → .other. The FpPoly/ZPoly abbreviations are reducible, so whnfR exposes the DensePoly application; the instance expressions are taken from the type itself, never synthesized.

Equations

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

def Hex.FactorTactic.evalFpPoly (tactic : String) (p : Nat) [ZMod64.Bounds p] (pE boundsE e : Lean.Expr) : Lean.MetaM (FpPoly p)

Evaluate a closed Hex.FpPoly p expression to its runtime value at elaboration time (compiled/interpreted evaluation, not kernel reduction).

Equations

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

def Hex.FactorTactic.replayBudget : Nat

Ceiling on degree · p, the cost driver of one kernel Rabin-certificate replay. Inputs over budget fail at elaboration time with a clear message instead of emitting a proof the kernel cannot afford to check.

Equations

• Hex.FactorTactic.replayBudget = 1 <<< 26

def Hex.FactorTactic.primeReplayBudget : Nat

Ceiling on candidate remainder tests in one kernel primality replay. 2^16 covers the full ZMod64 modulus range, whose largest square-root scan tests fewer than 2^16 candidates.

Equations

• Hex.FactorTactic.primeReplayBudget = 1 <<< 16

def Hex.FactorTactic.primeReplayCost (n : Nat) : Nat

Worst-case number of remainder tests in Hex.Nat.isPrimeTrial n. This mirrors the checker's square stopping convention without performing any divisions, and is used only at elaboration time to budget the proof that the kernel will replay.

Equations

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

def Hex.FactorTactic.checkReplayBudget (tactic : String) (p deg : Nat) : Lean.MetaM Unit

Fail fast when a Rabin replay for a degree-deg factor at modulus p would exceed replayBudget.

Equations

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

def Hex.FactorTactic.checkClosed (tactic : String) (e : Lean.Expr) : Lean.MetaM Unit

Reject inputs the compiled evaluator cannot see: free variables and metavariables.

Equations

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

def Hex.FactorTactic.applyExtensions (run : Extension → Lean.Elab.TermElabM ExtensionResult) (whenNone : Array Lean.MessageData → Lean.Elab.TermElabM Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Try the registered extensions in order, retaining decline diagnostics. whenNone renders the final error when no extension succeeds.

Equations

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

def Hex.FactorTactic.unsupportedMessage (tactic : String) (ty : Lean.Expr) (declines : Array Lean.MessageData) : Lean.MessageData

The standard "unsupported input type" tail for selection failures, including any extension decline diagnostics.

Equations

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