def HexBerlekampMathlib.FactorTactic.zmodInput? (ty : Lean.Expr) : Lean.MetaM (Option (ℕ × Lean.Expr))

Match a (whnfR-normalized) type against Polynomial (ZMod q) for a literal q, returning the modulus and its literal expression.

Equations

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

def HexBerlekampMathlib.FactorTactic.getNatLit (tactic : String) (e : Lean.Expr) : Lean.MetaM ℕ

Extract a Nat literal from an exponent expression (numerals and raw literals).

Equations

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

def HexBerlekampMathlib.FactorTactic.evalZModVal (tactic : String) (pE cE : Lean.Expr) : Lean.MetaM ℕ

Evaluate a closed ZMod q coefficient expression to its canonical Nat representative by whnf-reducing ZMod.val c.

Equations

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

def HexBerlekampMathlib.FactorTactic.scalarDecideProof (tactic : String) (prop : Lean.Expr) : Lean.MetaM Lean.Expr

Certify a scalar equality toZMod (ofNat q 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 HexBerlekampMathlib.FactorTactic.tomlFn (pE boundsE : Lean.Expr) : Lean.Expr

The partial application toMathlibPolynomial (p := q) as an expression.

Equations

• HexBerlekampMathlib.FactorTactic.tomlFn pE boundsE = Lean.mkApp2 (Lean.mkConst `HexPolyFpMathlib.toMathlibPolynomial) pE boundsE

def HexBerlekampMathlib.FactorTactic.combineBinary {q : ℕ} [Hex.ZMod64.Bounds q] (pE boundsE eOrig : Lean.Expr) (v : Hex.FpPoly q) (vaE vbE pa pb : Lean.Expr) (lem op : Lean.Name) : Lean.MetaM (Hex.FpPoly q × Lean.Expr × Lean.Expr)

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

Equations

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

def HexBerlekampMathlib.FactorTactic.constLeaf {q : ℕ} [Hex.ZMod64.Bounds q] (tactic : String) (pE boundsE : Lean.Expr) (k : ℕ) (cRhsE : Lean.Expr) (hTail? : Option Lean.Expr) : Lean.MetaM (Hex.FpPoly q × Lean.Expr × Lean.Expr)

Build a constant leaf from the canonical residue k: value DensePoly.C (ofNat q 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 HexBerlekampMathlib.FactorTactic.parsePolynomial (tactic : String) (q : ℕ) [Hex.ZMod64.Bounds q] (pE boundsE : Lean.Expr) (fuel : ℕ) (e : Lean.Expr) : Lean.MetaM (Hex.FpPoly q × Lean.Expr × Lean.Expr)

The parser-with-proof over Polynomial (ZMod q) 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 : FpPoly q, an executable expression vE denoting it (built from reified literals and executable operations), and a proof toMathlibPolynomial 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 HexBerlekampMathlib.FactorTactic.parseInput (tactic : String) (q : ℕ) [Hex.ZMod64.Bounds q] (pE boundsE e : Lean.Expr) : Lean.MetaM (Hex.FpPoly q × 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 : toMathlibPolynomial fLit = e.

Equations

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

def HexBerlekampMathlib.FactorTactic.elabFactorZMod (tactic : String) (q : ℕ) [Hex.ZMod64.Bounds q] (hpt : Hex.Nat.isPrimeTrial q = true) (pE e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

The factor_poly arm: parse with proof, run the shared FpPoly factor search as untrusted search, self-check, and emit a reified Hex.FactoredPoly.ofFp application.

Equations

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

def HexBerlekampMathlib.FactorTactic.elabIrredZMod (tactic : String) (q : ℕ) [Hex.ZMod64.Bounds q] (hpt : Hex.Nat.isPrimeTrial q = true) (pE e : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

The irreducibility arm: parse with proof, build the Rabin certificate as untrusted search, self-check, and emit a reified HexBerlekampMathlib.irreducible_ofFp application.

Equations

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

def HexBerlekampMathlib.FactorTactic.withZModInput (tactic : String) (ty : Lean.Expr) (k : (q : ℕ) → Hex.ZMod64.Bounds q → Hex.Nat.isPrimeTrial q = true → Lean.Expr → Lean.Elab.TermElabM Lean.Expr) : Lean.Elab.TermElabM Hex.FactorTactic.ExtensionResult

Match the input type, check primality and the ZMod64 bounds, and run the continuation with the Bounds instance in scope. Non-Polynomial (ZMod q) types are notApplicable; composite or oversized moduli are declined with a diagnostic.

Equations

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

def HexBerlekampMathlib.FactorTactic.goalIrredZMod (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Hex.FactorTactic.ExtensionResult

Goal mode: close Irreducible P for P : Polynomial (ZMod q).

Equations

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

def HexBerlekampMathlib.FactorTactic.extension : Hex.FactorTactic.Extension

The Polynomial (ZMod q) extension, checked by name from Hex.FactorTactic.extensionNames; the registration tests fail if a rename makes the extension undiscoverable.

Equations

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