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

Literal List expression [x₁, …, xₙ] : List ty.

Equations

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

def Hex.FactorTactic.coverEntryType (pE boundsE : Lean.Expr) : Lean.Expr

The type FpPoly p × ZMod64 p × Berlekamp.IrreducibilityCertificate of a certified-cover entry, at a reified prime and bounds instance.

Equations

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

def Hex.FactorTactic.reifyCoverEntry (pE boundsE : Lean.Expr) {p : Nat} [ZMod64.Bounds p] (m : FpPoly p) (c : ZMod64 p) (cert : Berlekamp.IrreducibilityCertificate) : Lean.Expr

Reify one certified-cover entry (m, c, cert).

Equations

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

def Hex.FactorTactic.fpFactorSearch (p : Nat) [ZMod64.Bounds p] (hp : Nat.Prime p) (f : FpPoly p) : ZMod64 p × List (FpPoly p)

The untrusted factor search for f : FpPoly p: leading unit plus monic irreducible factors with repetition, in nondecreasing size order. Correctness is carried entirely by the emitted kernel checks.

Equations

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

def Hex.FactorTactic.dedupFactors {p : Nat} [ZMod64.Bounds p] (l : List (FpPoly p)) : List (FpPoly p)

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

Equations

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

def Hex.FactorTactic.fpCoverEntries (tactic : String) (p : Nat) [ZMod64.Bounds p] (factors : List (FpPoly p)) : Lean.MetaM (List (FpPoly p × ZMod64 p × Berlekamp.IrreducibilityCertificate))

Build the certified-cover entries for the distinct factors: each factor is monic by construction, so the entry is (q, 1, cert). Errors if a Rabin certificate cannot be produced (the factors come from Berlekamp on square-free parts, so this indicates an internal error) or if a replay is over budget.

Equations

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

def Hex.FactorTactic.mkFpFactored (tactic : String) (p : Nat) [ZMod64.Bounds p] (hpt : Nat.isPrimeTrial p = true) (pE boundsE RE zeroE decE fE : Lean.Expr) : Lean.MetaM Lean.Expr

Constructs the value emitted by factor_poly for f : FpPoly p: returns the Hex.FpPoly.Factored f value as a raw Expr over reified literal data.

Equations

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

def Hex.FactorTactic.elabFactorPolyFp (tactic : String) (p : Nat) (pE boundsE RE zeroE decE fE : Lean.Expr) : Lean.MetaM Lean.Expr

Elaborate factor_poly f for f : FpPoly p: check primality and bounds for the literal modulus, then run the instance-carrying implementation.

Equations

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

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

Elaborate a factor_poly argument and produce the structure value, trying registered extensions for non-FpPoly input types.

Equations

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

def Hex.FactorTactic.factorPolyTerm : Lean.ParserDescr

factor_poly f elaborates to a certified irreducible factorization of f (a Hex.FpPoly.Factored f for f : FpPoly p; extensions add further input types), usable as obtain ⟨scalar, factors, factors_mul, factors_irred⟩ := factor_poly f.

Equations

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

def Hex.FactorTactic.elabFactorPoly : Lean.Elab.Term.TermElab

Term elaborator for factor_poly f: runs the search in compiled code and returns the checked certificate term.

Equations

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

def Hex.FactorTactic.introFactored (e : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Introduce the four fields of a recognized factorization result as scalar/factors let bindings plus factors_mul/factors_irred hypotheses. Inspecting the result type rather than the emitted constructor lets extension assemblers return opaque Hex.FactoredPoly terms while exposing the same tactic interface as the executable FpPoly and ZPoly extensions. Unrecognized extension result types land as a single factored hypothesis. Shared by the factor_poly and factor_poly! tactic forms.

Equations

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

def Hex.FactorTactic.factorPolyTac : Lean.ParserDescr

The tactic form of factor_poly: introduces scalar and factors as let bindings holding the literal factorization data, plus factors_mul and factors_irred hypotheses stated over them.

Equations

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

def Hex.FactorTactic.evalFactorPolyTac : Lean.Elab.Tactic.Tactic

Tactic elaborator for factor_poly f: elaborates the certificate and introduces its four fields into the local context.

Equations

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