hex

35.11. HexMvFactor: checked multivariate factorization🔗

35.11.1. Introduction🔗

HexMvFactor factors sparse multivariate polynomials over Int. Its bounded driver combines structural answers, content and square-free decomposition, Kronecker splitting, evaluation-point search, leading-coefficient distribution, and checked extended EEZ lifting.

A stopped search is data, not an unchecked exception: the partial result retains its already verified decomposition, the exact failure reason, and the generator state. A complete answer additionally replays an irreducibility certificate for every distinct factor.

35.11.2. Checked decompositions🔗

🔗structure
Hex.MvFactor.Factor (n : Nat) (cmp : Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : Type
Hex.MvFactor.Factor (n : Nat)
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type

One nonconstant entry in a product decomposition.

Constructor

Hex.MvFactor.Factor.mk

Fields

factor : Hex.MvPoly n Int cmp

Primitive normalized nonconstant polynomial.

multiplicity : Nat

Positive exponent of the factor in the decomposition.

🔗structure
Hex.MvFactor.Decomp (n : Nat) (cmp : Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] : Type
Hex.MvFactor.Decomp (n : Nat)
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type

An integer scalar and a list of polynomial powers.

Constructor

Hex.MvFactor.Decomp.mk

Fields

content : Int

Integer scalar separated from the polynomial factors.

factors : List (Hex.MvFactor.Factor n cmp)

Pairwise-distinct polynomial factors with their multiplicities.

🔗def
Hex.MvFactor.checkDecomp {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) (D : Hex.MvFactor.Decomp n cmp) : Bool
Hex.MvFactor.checkDecomp {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp)
  (D : Hex.MvFactor.Decomp n cmp) : Bool

Replay all five decomposition conditions from the SPEC.

🔗def
Hex.MvFactor.IsDecompOf {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) (D : Hex.MvFactor.Decomp n cmp) : Prop
Hex.MvFactor.IsDecompOf {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp)
  (D : Hex.MvFactor.Decomp n cmp) : Prop

The semantic product and nonconstant-positive-multiplicity payload of a checked decomposition. Normalization and distinctness are checker-side canonicity conditions rather than part of this minimal witness.

🔗structure
Hex.MvFactor.CheckedDecomp {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) : Type
Hex.MvFactor.CheckedDecomp {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) : Type

Accepted decomposition data tied to the subject checked by its caller.

Constructor

Hex.MvFactor.CheckedDecomp.mk

Fields

raw : Hex.MvFactor.Decomp n cmp

Raw decomposition data accepted by the checker.

valid : Hex.MvFactor.checkDecomp f self.raw = true

Evidence that replay accepts the decomposition for f.

🔗theorem
Hex.MvFactor.checkDecomp_sound {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  {f : Hex.MvPoly n Int cmp} {D : Hex.MvFactor.Decomp n cmp}
  (h : Hex.MvFactor.checkDecomp f D = true) :
  Hex.MvFactor.IsDecompOf f D
Hex.MvFactor.checkDecomp_sound {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  {f : Hex.MvPoly n Int cmp}
  {D : Hex.MvFactor.Decomp n cmp}
  (h :
    Hex.MvFactor.checkDecomp f D = true) :
  Hex.MvFactor.IsDecompOf f D

Executable replay implies the semantic decomposition payload.

The decomposition stores integer content separately and gives each nonconstant, primitive, normalized factor a positive multiplicity. Replay also checks pairwise distinctness, making the result canonical enough for downstream comparison and tactic output.

35.11.3. Kronecker splitting🔗

🔗def
Hex.MvFactor.kron {n : Nat} {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp] (degrees : Fin n → Nat)
  (p : Hex.MvPoly n Int cmp) : Hex.ZPoly
Hex.MvFactor.kron {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (degrees : Fin n → Nat)
  (p : Hex.MvPoly n Int cmp) : Hex.ZPoly

Substitute x_j = z^(radixWeight degrees j).

🔗def
Hex.MvFactor.unKron? {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (degrees : Fin n → Nat) (P : Hex.ZPoly) :
  Option (Hex.MvPoly n Int cmp)
Hex.MvFactor.unKron? {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (degrees : Fin n → Nat)
  (P : Hex.ZPoly) :
  Option (Hex.MvPoly n Int cmp)

Partial inverse to kron, with an exact re-encoding check before any decoded polynomial is exposed.

🔗def
Hex.MvFactor.findSplit {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (degrees : Fin n → Nat) (g : Hex.MvPoly n Int cmp)
  (uni : List (Hex.ZPoly × Nat)) : Option (Hex.MvFactor.Split n cmp)
Hex.MvFactor.findSplit {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (degrees : Fin n → Nat)
  (g : Hex.MvPoly n Int cmp)
  (uni : List (Hex.ZPoly × Nat)) :
  Option (Hex.MvFactor.Split n cmp)

Search all proper exponent vectors for a genuine multivariate divisor.

🔗def
Hex.MvFactor.kronDecide {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (g : Hex.MvPoly n Int cmp) : Hex.MvFactor.Verdict n cmp
Hex.MvFactor.kronDecide {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (g : Hex.MvPoly n Int cmp) :
  Hex.MvFactor.Verdict n cmp

Total Kronecker decision procedure on the intended primitive, nonconstant domain. Outside that domain it still terminates, while the soundness theorem below deliberately requires the missing hypotheses.

🔗theorem
Hex.MvFactor.kronDecide_checks {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  {g : Hex.MvPoly n Int cmp} {cert : Hex.MvFactor.IrredCert n cmp}
  (hprim : g.content = 1) (hnonconst : ¬g.IsConst)
  (h :
    Hex.MvFactor.kronDecide g = Hex.MvFactor.Verdict.irreducible cert) :
  ∃ scalar uni,
    cert = Hex.MvFactor.IrredCert.kronecker scalar uni ∧
      Hex.MvFactor.checkKronecker g scalar uni = true
Hex.MvFactor.kronDecide_checks {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  {g : Hex.MvPoly n Int cmp}
  {cert : Hex.MvFactor.IrredCert n cmp}
  (hprim : g.content = 1)
  (hnonconst : ¬g.IsConst)
  (h :
    Hex.MvFactor.kronDecide g =
      Hex.MvFactor.Verdict.irreducible
        cert) :
  ∃ scalar uni,
    cert =
        Hex.MvFactor.IrredCert.kronecker
          scalar uni ∧
      Hex.MvFactor.checkKronecker g scalar
          uni =
        true

The producer's irreducible branch replays on its intended domain.

🔗theorem
Hex.MvFactor.kronDecide_split {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  {g : Hex.MvPoly n Int cmp} {split : Hex.MvFactor.Split n cmp}
  (h :
    Hex.MvFactor.kronDecide g = Hex.MvFactor.Verdict.reducible split) :
  Hex.MvFactor.checkSplitCore g split = true
Hex.MvFactor.kronDecide_split {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  {g : Hex.MvPoly n Int cmp}
  {split : Hex.MvFactor.Split n cmp}
  (h :
    Hex.MvFactor.kronDecide g =
      Hex.MvFactor.Verdict.reducible
        split) :
  Hex.MvFactor.checkSplitCore g split =
    true

Every reducible outcome has already passed cheap split replay.

Mixed-radix weights make the substitution injective on the polynomial's degree box. Decoding rejects exponent vectors outside that box, and every candidate split is multiplied back in the original multivariate ring before it is exposed.

35.11.4. Evaluation points and EEZ lifting🔗

🔗structure
Hex.MvFactor.Config : Type
Hex.MvFactor.Config : Type

Search budgets shared by the point layer and the downstream EEZ driver.

Constructor

Hex.MvFactor.Config.mk

Fields

rand : Hex.Rand

Initial deterministic random-generator state.

pointFuel : Nat

Maximum number of evaluation points examined.

pointScouts : Nat

Maximum number of admissible probes retained.

pointShell : Nat

Maximum infinity-norm shell enumerated for evaluation points.

primeFuel : Nat

Maximum number of candidate primes examined.

doublings : Nat

Maximum number of reconstruction-modulus doublings.

recombLevels : Nat

Number of grouped recombination levels attempted.

kronecker : Bool

Whether the Kronecker route may be used.

kroneckerDeg : Nat

Maximum encoded univariate degree accepted by Kronecker substitution.

🔗def
Hex.MvFactor.probe {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (_cfg : Hex.MvFactor.Config)
  (i : Fin (n + 1)) (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp'] (a : Fin n → Int)
  (s : Hex.MvPoly (n + 1) Int cmp) (lc : Hex.MvFactor.Decomp n cmp')
  (r : Hex.Rand) :
  Except Hex.MvFactor.PointReject
    (Hex.MvFactor.Probe n cmp cmp' × Hex.Rand)
Hex.MvFactor.probe {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (_cfg : Hex.MvFactor.Config)
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (a : Fin n → Int)
  (s : Hex.MvPoly (n + 1) Int cmp)
  (lc : Hex.MvFactor.Decomp n cmp')
  (r : Hex.Rand) :
  Except Hex.MvFactor.PointReject
    (Hex.MvFactor.Probe n cmp cmp' ×
      Hex.Rand)

Probe one caller-supplied point. Factorization is deterministic, so the random state is returned unchanged; only shell ordering advances it.

🔗def
Hex.MvFactor.scoutPoints {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (cfg : Hex.MvFactor.Config)
  (i : Fin (n + 1)) (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp'] (s : Hex.MvPoly (n + 1) Int cmp)
  (lc : Hex.MvFactor.Decomp n cmp') (r : Hex.Rand) :
  Hex.MvFactor.PointSearchResult n cmp cmp'
Hex.MvFactor.scoutPoints {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (cfg : Hex.MvFactor.Config)
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (s : Hex.MvPoly (n + 1) Int cmp)
  (lc : Hex.MvFactor.Decomp n cmp')
  (r : Hex.Rand) :
  Hex.MvFactor.PointSearchResult n cmp
    cmp'

Enumerate bounded evaluation-point shells and retain the best probes.

🔗def
Hex.MvFactor.distribute? {n : Nat} (_i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (a : Fin n → Int) (lc : Hex.MvFactor.Decomp n cmp')
  (uni : List Hex.ZPoly) (scalar : Int) :
  Option (List (Hex.MvPoly n Int cmp') × List Hex.ZPoly)
Hex.MvFactor.distribute? {n : Nat}
  (_i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (a : Fin n → Int)
  (lc : Hex.MvFactor.Decomp n cmp')
  (uni : List Hex.ZPoly) (scalar : Int) :
  Option
    (List (Hex.MvPoly n Int cmp') ×
      List Hex.ZPoly)

Public SPEC-shaped wrapper. The main-variable index records the ambient arity for callers even though all work here is already in the n remaining variables.

🔗def
Hex.MvFactor.factorSquarefree {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (lower : Hex.MvFactor.LowerFactor n)
  (cfg : Hex.MvFactor.Config) (s : Hex.MvPoly (n + 1) Int cmp)
  (r : Hex.Rand) :
  Except (Hex.MvFactor.EezProgress cmp) (Hex.MvFactor.EezResult cmp)
Hex.MvFactor.factorSquarefree {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (lower : Hex.MvFactor.LowerFactor n)
  (cfg : Hex.MvFactor.Config)
  (s : Hex.MvPoly (n + 1) Int cmp)
  (r : Hex.Rand) :
  Except (Hex.MvFactor.EezProgress cmp)
    (Hex.MvFactor.EezResult cmp)

Factor one squarefree component, recursively extracting its content in the selected main variable and then processing grouped factors with explicit same-arity fuel.

Point enumeration is deterministic for a fixed Rand state and explicitly bounded by shell and fuel limits. Probes reject degree drops and unsuitable images before building a Hensel input. Grouped recombination tests products of lifted image factors and retains only exact multivariate divisors.

35.11.5. Public factorization🔗

🔗inductive type
Hex.MvFactor.Failure (n : Nat)
  (cmp : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type
Hex.MvFactor.Failure (n : Nat)
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type

Public, stable failure distinctions for bounded factorization.

Constructors

Hex.MvFactor.Failure.zero {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] :
  Hex.MvFactor.Failure n cmp

The input is the zero polynomial.

Hex.MvFactor.Failure.point {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (attempts : Nat)
  (last : Option Hex.MvFactor.PointReject) :
  Hex.MvFactor.Failure n cmp

Evaluation-point search exhausted its budget.

Hex.MvFactor.Failure.lift {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (inner : Hex.MvHensel.Failure) :
  Hex.MvFactor.Failure n cmp

Multivariate Hensel lifting rejected the constructed input or stopped.

Hex.MvFactor.Failure.recombine {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] (levels : Nat) :
  Hex.MvFactor.Failure n cmp

Grouped recombination exhausted its level budget.

Hex.MvFactor.Failure.irreducible {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (factor : Hex.MvPoly n Int cmp) :
  Hex.MvFactor.Failure n cmp

No available certificate proved the reported factor irreducible.

Hex.MvFactor.Failure.random {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  (error : Hex.RandError) : Hex.MvFactor.Failure n cmp

Random-word generation failed.

🔗structure
Hex.MvFactor.Partial {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) : Type
Hex.MvFactor.Partial {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) : Type

A checked coarse answer together with the reason bounded search stopped and the generator state reached at that point.

Constructor

Hex.MvFactor.Partial.mk

Fields

found : Hex.MvFactor.CheckedDecomp f

Checked decomposition accumulated before the search stopped.

reason : Hex.MvFactor.Failure n cmp

Exact reason why the bounded search stopped.

rand : Hex.Rand

Random-generator state reached when the search stopped.

🔗def
Hex.MvFactor.factorWith {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (cfg : Hex.MvFactor.Config) (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f)
    (Hex.MvFactor.CheckedDecomp f × Hex.Rand)
Hex.MvFactor.factorWith {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (cfg : Hex.MvFactor.Config)
  (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f)
    (Hex.MvFactor.CheckedDecomp f ×
      Hex.Rand)

Bounded factorization with explicit configuration and generator state.

🔗def
Hex.MvFactor.factor? {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f) (Hex.MvFactor.CheckedDecomp f)
Hex.MvFactor.factor? {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f)
    (Hex.MvFactor.CheckedDecomp f)

Deterministic convenience entry point using Config.default.

🔗def
Hex.MvFactor.completeWith {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (cfg : Hex.MvFactor.Config) (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f)
    (Hex.MvFactor.CheckedComplete f × Hex.Rand)
Hex.MvFactor.completeWith {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (cfg : Hex.MvFactor.Config)
  (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f)
    (Hex.MvFactor.CheckedComplete f ×
      Hex.Rand)

Bounded factorization followed by checked certificate production for every returned factor. No complete result is exposed without final replay.

🔗def
Hex.MvFactor.complete? {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f) (Hex.MvFactor.CheckedComplete f)
Hex.MvFactor.complete? {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) :
  Except (Hex.MvFactor.Partial f)
    (Hex.MvFactor.CheckedComplete f)

Deterministic complete factorization at Config.default.

factor? returns a checked product decomposition or a checked partial decomposition with a stopping reason. complete? goes further: it requires the irreducibility producer to certify every factor and performs one final independent replay.

35.11.6. Irreducibility certificates🔗

🔗inductive type
Hex.MvFactor.IrredCert (n : Nat)
  (cmp : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type 1
Hex.MvFactor.IrredCert (n : Nat)
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type 1

A checkable irreducibility witness, modulo the univariate obligations reported by obligations.

Constructors

Hex.MvFactor.IrredCert.degreeOne {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [outerTrans : Std.TransCmp cmp]
  [outerEq : Std.LawfulEqCmp cmp] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [order : Hex.IsMonomialOrder cmp']
  (prim : Hex.MvPoly.ContentCert n Int cmp') :
  Hex.MvFactor.IrredCert (n + 1) cmp

Certify irreducibility from degree one in a selected variable.

Hex.MvFactor.IrredCert.image {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [outerTrans : Std.TransCmp cmp]
  [outerEq : Std.LawfulEqCmp cmp] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [order : Hex.IsMonomialOrder cmp'] (point : Fin n → Int)
  (prim : Hex.MvPoly.ContentCert n Int cmp') :
  Hex.MvFactor.IrredCert (n + 1) cmp

Certify irreducibility from an irreducible degree-preserving image.

Hex.MvFactor.IrredCert.embed {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [outerTrans : Std.TransCmp cmp]
  [outerEq : Std.LawfulEqCmp cmp] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [order : Hex.IsMonomialOrder cmp']
  (sub : Hex.MvPoly n Int cmp')
  (cert : Hex.MvFactor.IrredCert n cmp') :
  Hex.MvFactor.IrredCert (n + 1) cmp

Transport a lower-arity irreducibility certificate through embedding.

Hex.MvFactor.IrredCert.kronecker {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  [outerTrans : Std.TransCmp cmp]
  [outerEq : Std.LawfulEqCmp cmp] (scalar : Int)
  (uni : List (Hex.ZPoly × Nat)) :
  Hex.MvFactor.IrredCert n cmp

Certify irreducibility by complete bounded Kronecker factorization.

🔗def
Hex.MvFactor.checkIrred {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp] :
  Hex.MvPoly n Int cmp → Hex.MvFactor.IrredCert n cmp → Bool
Hex.MvFactor.checkIrred {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp] :
  Hex.MvPoly n Int cmp →
    Hex.MvFactor.IrredCert n cmp → Bool

Replay an irreducibility certificate. Successful image certificates leave the primitive univariate image as an explicit obligation.

🔗theorem
Hex.MvFactor.checkIrred_sound {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  {g : Hex.MvPoly n Int cmp} {cert : Hex.MvFactor.IrredCert n cmp}
  (h : Hex.MvFactor.checkIrred g cert = true)
  (ho :
    ∀ (F : Hex.ZPoly),
      F ∈ Hex.MvFactor.obligations g cert → Hex.MvHensel.Irred F) :
  Hex.MvHensel.Irred g
Hex.MvFactor.checkIrred_sound {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  {g : Hex.MvPoly n Int cmp}
  {cert : Hex.MvFactor.IrredCert n cmp}
  (h :
    Hex.MvFactor.checkIrred g cert = true)
  (ho :
    ∀ (F : Hex.ZPoly),
      F ∈
          Hex.MvFactor.obligations g
            cert →
        Hex.MvHensel.Irred F) :
  Hex.MvHensel.Irred g

Checked certificate replay, together with its declared univariate obligations, implies Mathlib-free irreducibility.

🔗structure
Hex.MvFactor.Complete (n : Nat)
  (cmp : Hex.Mono n → Hex.Mono n → Ordering) [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type 1
Hex.MvFactor.Complete (n : Nat)
  (cmp :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] : Type 1

A decomposition paired positionally with irreducibility certificates.

Constructor

Hex.MvFactor.Complete.mk

Fields

decomp : Hex.MvFactor.Decomp n cmp

Checked product decomposition whose factors are certified below.

certs : List (Hex.MvFactor.IrredCert n cmp)

Irreducibility certificates aligned with the decomposition factors.

🔗def
Hex.MvFactor.checkComplete {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp) (complete : Hex.MvFactor.Complete n cmp) :
  Bool
Hex.MvFactor.checkComplete {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  (f : Hex.MvPoly n Int cmp)
  (complete :
    Hex.MvFactor.Complete n cmp) :
  Bool

Reject zero, replay the decomposition, and pair every factor with exactly one irreducibility certificate.

🔗theorem
Hex.MvFactor.checkComplete_sound {n : Nat}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  {f : Hex.MvPoly n Int cmp} {complete : Hex.MvFactor.Complete n cmp}
  (h : Hex.MvFactor.checkComplete f complete = true)
  (ho :
    ∀ (pair : Hex.MvFactor.Factor n cmp × Hex.MvFactor.IrredCert n cmp),
      pair ∈ complete.decomp.factors.zip complete.certs →
        ∀ (F : Hex.ZPoly),
          F ∈ Hex.MvFactor.obligations pair.fst.factor pair.snd →
            Hex.MvHensel.Irred F) :
  Hex.MvFactor.IsFactorizationOf f complete.decomp
Hex.MvFactor.checkComplete_sound {n : Nat}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  {f : Hex.MvPoly n Int cmp}
  {complete : Hex.MvFactor.Complete n cmp}
  (h :
    Hex.MvFactor.checkComplete f
        complete =
      true)
  (ho :
    ∀
      (pair :
        Hex.MvFactor.Factor n cmp ×
          Hex.MvFactor.IrredCert n cmp),
      pair ∈
          complete.decomp.factors.zip
            complete.certs →
        ∀ (F : Hex.ZPoly),
          F ∈
              Hex.MvFactor.obligations
                pair.fst.factor pair.snd →
            Hex.MvHensel.Irred F) :
  Hex.MvFactor.IsFactorizationOf f
    complete.decomp

Complete checker replay plus the declared univariate obligations gives a factorization into irreducibles.

Certificates cover constants, selected-variable degree one, irreducible images with primitive leading data, embeddings from lower arity, and complete Kronecker decisions. The checker, not the producer, is the trusted boundary.

35.11.7. Cross-references🔗

  • HexMvGcd supplies exact division, content, and square-free decomposition.

  • HexMvHensel supplies checked reconstruction from suitable univariate image factorizations.

  • The Mathlib companion transports checked results to MvPolynomial and provides the factor_poly and irreducibility tactics.