def HexBerlekampZassenhausMathlib.FactorTactic.bangBudget : ℕ

Dense-size cap (degree + 1) for the kernel factorizer replay: degree 12 already costs tens of seconds of kernel time per input.

Equations

• HexBerlekampZassenhausMathlib.FactorTactic.bangBudget = 13

def HexBerlekampZassenhausMathlib.FactorTactic.checkBangBudget (tactic : String) (f : Hex.ZPoly) : Lean.MetaM Unit

Reject inputs whose kernel factorizer replay would be over budget.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.kernelDecideTrue (tactic : String) (prop : Lean.Expr) : Lean.MetaM Unit

Precheck that the kernel can reduce decide prop to true in the current environment, so a missing import all closure fails here with a clear message instead of a bare kernel type mismatch at declaration time.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangChecks (tactic : String) (fE : Lean.Expr) (f : Hex.ZPoly) : Lean.MetaM Unit

Shared degenerate-input and budget checks for the bang fallbacks.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangZPolyIrred (tactic : String) (fE : Lean.Expr) : Lean.MetaM Lean.Expr

The irreducibility! fallback for Hex.ZPoly inputs: free-layer conclusion via one kernel factorizer replay.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangIntIrred (tactic : String) (e : Lean.Expr) : Lean.MetaM Lean.Expr

The irreducibility! fallback for Polynomial ℤ inputs: parse with proof, then transport the kernel replay through the translation equality.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.forallIrredProp (factorsE : Lean.Expr) : Lean.MetaM Lean.Expr

The membership-bounded irreducibility proposition ∀ q ∈ factorsE, Hex.ZPoly.Irreducible q as an expression.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangFactorCommon (tactic : String) (f : Hex.ZPoly) : Lean.MetaM (Lean.Expr × Lean.Expr)

The factor_poly! fallback machinery shared by both input types: factorize, self-check, reify, and kernel-precheck the per-factor replay. Returns the scalar and factor-list expressions.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangZPolyFactor (fE : Lean.Expr) : Lean.MetaM Lean.Expr

The factor_poly! fallback for Hex.ZPoly inputs.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangIntFactor (e : Lean.Expr) : Lean.MetaM Lean.Expr

The factor_poly! fallback for Polynomial ℤ inputs.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.elabBangArg (tactic : String) (t : Lean.Syntax) (onZPoly onInt : Lean.Expr → Lean.MetaM Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Elaborate a bang-fallback argument and selection on its type.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.irreducibilityBangTerm : Lean.ParserDescr

irreducibility! f behaves as irreducibility f, then falls back to the kernel factorizer replay when the certificate computation declines (see the module docstring for the import all closure and cost caveats).

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.elabIrreducibilityBang : Lean.Elab.Term.TermElab

Elaborator for term-mode irreducibility!.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.bangGoalProof (tgt : Lean.Expr) : Lean.MetaM Lean.Expr

The bang goal-mode fallback: close Hex.ZPoly.Irreducible e, Irreducible (toPolynomial f), or Irreducible P for parseable P : Polynomial ℤ by the kernel factorizer replay.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.irreducibilityBangTac : Lean.ParserDescr

Tactic forms of irreducibility!, mirroring irreducibility: bare form closes an irreducibility goal, irreducibility! f adds this, and irreducibility! h : f names it h, each falling back to the kernel factorizer replay when the certificate computation declines.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.evalIrreducibilityBangTac : Lean.Elab.Tactic.Tactic

Elaborator for the irreducibility! tactic forms.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.elabFactorBangArgument (stx t : Lean.Syntax) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Shared plain-then-bang elaboration for factor_poly!.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.factorPolyBangTerm : Lean.ParserDescr

factor_poly! f behaves as factor_poly f, then falls back to per-factor kernel factorizer replays when the certificate computation declines (see the module docstring for the import all closure and cost caveats).

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.elabFactorPolyBang : Lean.Elab.Term.TermElab

Elaborator for term-mode factor_poly!.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.factorPolyBangTac : Lean.ParserDescr

The tactic form of factor_poly!: as the factor_poly tactic (scalar/factors bindings plus factors_mul/factors_irred), with the kernel-replay fallback.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.evalFactorPolyBangTac : Lean.Elab.Tactic.Tactic

Elaborator for the factor_poly! tactic form.

Equations

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