def HexBerlekampZassenhausMathlib.FactorTactic.intPolyInput? (ty : Lean.Expr) : Lean.MetaM Bool

Match a (whnfR-normalized) type against Polynomial ℤ.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.zpolyTy : Lean.Expr

The type Hex.ZPoly as an expression.

Equations

• HexBerlekampZassenhausMathlib.FactorTactic.zpolyTy = Lean.mkConst `Hex.ZPoly

def HexBerlekampZassenhausMathlib.FactorTactic.tomlFn : Lean.Expr

The transport HexPolyZMathlib.toPolynomial as an expression.

Equations

• HexBerlekampZassenhausMathlib.FactorTactic.tomlFn = Lean.mkConst `HexPolyZMathlib.toPolynomial

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

Certify a scalar equality (k : ℤ) = c by decide, checking at elaboration time that the Boolean actually reduces to true.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.combineBinary (eOrig : Lean.Expr) (v : Hex.ZPoly) (vaE vbE pa pb : Lean.Expr) (lem op : Lean.Name) : Lean.MetaM (Hex.ZPoly × Lean.Expr × Lean.Expr)

Combine two parsed children through a binary transport lemma: given child results (va, vaE, pa)/(vb, vbE, pb) with pa : toPolynomial vaE = a (and likewise pb), produce the node value v, the executable expression vaE ⋄ vbE, and the chained proof toPolynomial (vaE ⋄ vbE) = a ⋄ b.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.constLeaf (tactic : String) (k : ℤ) (cRhsE : Lean.Expr) (hTail? : Option Lean.Expr) : Lean.MetaM (Hex.ZPoly × Lean.Expr × Lean.Expr)

Build a constant leaf from the evaluated coefficient k: value DensePoly.C k, its literal expression, and the transport proof against the Mathlib scalar cRhsE (certified by decide), chained through hTail : Polynomial.C cRhsE = e when the leaf is not literally a C application.

Equations

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

partial def HexBerlekampZassenhausMathlib.FactorTactic.parsePolynomial (tactic : String) (fuel : ℕ) (e : Lean.Expr) : Lean.MetaM (Hex.ZPoly × Lean.Expr × Lean.Expr)

The parser-with-proof over Polynomial ℤ expressions: interpret X / C / numerals / + / - / * / neg / ^ (Nat literal) (with named defs unfolded one delta step at a time under a fuel guard), returning the executable value v : Hex.ZPoly, an executable expression vE denoting it (built from reified literals and executable operations), and a proof toPolynomial vE = e (up to definitional equality on the right). Structural heads are matched on the raw term: whnf would unfold Polynomial.C/X/numerals into their Finsupp normal form and defeat the match.

def HexBerlekampZassenhausMathlib.FactorTactic.parseInput (tactic : String) (e : Lean.Expr) : Lean.MetaM (Hex.ZPoly × Lean.Expr × Lean.Expr)

Parse the full input with parsePolynomial, then recombine the parsed expression with the flat reified literal of its value through one eq_of_beqCoeffs kernel check, yielding (f, fLit, hP) with hP : toPolynomial fLit = e.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.coverDecline (tactic : String) (q : Hex.ZPoly) : Lean.MetaM Lean.MessageData

The decline diagnostic for factors outside both certificate languages.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.searchCover (tactic : String) (factors : List Hex.ZPoly) : Lean.MetaM (Except Lean.MessageData (List (Hex.ZPoly × Hex.ZPoly.IrredWitness) × List (Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate)))

Search a mixed certificate cover for a factor list: a free-layer IrredWitness per distinct factor where one exists, a multi-prime degree-obstruction certificate otherwise. Returns the decline diagnostic when some factor has neither.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.reifyCertifiedList (certified : List (Hex.ZPoly × Hex.ZPoly.IrredWitness)) : Lean.MetaM Lean.Expr

Reify a (factor, IrredWitness) list as a literal Expr.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.reifyMultiList (multiPrime : List (Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate)) : Lean.MetaM Lean.Expr

Reify a (factor, multi-prime certificate) list as a literal Expr.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.factorSearch (tactic : String) (f : Hex.ZPoly) : Lean.MetaM (ℤ × List Hex.ZPoly)

The untrusted factor search shared by both factor_poly arms: factors with repetition in nondecreasing size order, plus the scalar, self-checked against the input.

Equations

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

inductive HexBerlekampZassenhausMathlib.FactorTactic.OneWitness : Type

One irreducibility witness of either kind for a single polynomial.

• free (w : Hex.ZPoly.IrredWitness) : OneWitness
• multi (cert : Hex.ZPolyIrreducibilityCertificate) : OneWitness

def HexBerlekampZassenhausMathlib.FactorTactic.searchOne (tactic : String) (fE : Lean.Expr) (f : Hex.ZPoly) : Lean.MetaM (Except Lean.MessageData OneWitness)

Search a single-polynomial witness: free-layer first, multi-prime fallback; decline diagnostic for balanced inputs outside both languages, targeted errors for zero/unit/reducible inputs.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.emitIrreducibleOfZ (tactic : String) (P fLit hP : Lean.Expr) (f : Hex.ZPoly) (w : OneWitness) : Lean.MetaM Lean.Expr

Emit irreducible_ofZ P fLit certified multiPrime (Eq.refl true) hP for a single-polynomial witness of either kind.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.zpolyIrredProof (fE : Lean.Expr) (w : OneWitness) : Lean.MetaM Lean.Expr

Emit the free-layer proof Hex.ZPoly.Irreducible fE for a witness of either kind.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.elabFactorInt (tactic : String) (e : Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

The factor_poly arm for Polynomial ℤ: parse with proof, factorize as untrusted search, certify the cover, and emit a reified Hex.FactoredPoly.ofZ application.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.elabIrredInt (tactic : String) (e : Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

The irreducibility arm for Polynomial ℤ.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.factorZPolyStrong (fE : Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

The strong Hex.ZPoly factor_poly arm: checked after the free extension, so it certifies covers the free layer declines (balanced factors) through the multi-prime certificates, emitting a Hex.ZPoly.Factored whose factors_irred is one irreducible_of_checkMultiPrimeCover check.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.irredZPolyStrong (fE : Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

The strong Hex.ZPoly irreducibility arm: free-layer conclusion Hex.ZPoly.Irreducible fE, certified through the multi-prime checker when the free extension declined.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.matchToPolynomial? (arg : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Match HexPolyZMathlib.toPolynomial f (or the unfolded HexPolyMathlib.toPolynomial at R = ℤ) and return f.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.closeGoal (tgt proof : Lean.Expr) : Lean.MetaM Hex.FactorTactic.ExtensionResult

Certify proof against the goal up to definitional equality and report success.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.goalIrredInt (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Hex.FactorTactic.ExtensionResult

Goal mode: close Hex.ZPoly.Irreducible e (free-layer statement), Irreducible (toPolynomial f), and Irreducible P for parseable P : Polynomial ℤ.

Equations

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

def HexBerlekampZassenhausMathlib.FactorTactic.extension : Hex.FactorTactic.Extension

The Polynomial ℤ / strong Hex.ZPoly extension, checked by name from Hex.FactorTactic.extensionNames; the integration tests fail if a rename makes the extension undiscoverable. Checked after the free Hex.ZPoly extension, so its ZPoly arms only see inputs the free layer declined.

Equations

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