hex

35.10. HexMvHensel: checked multivariate lifting🔗

35.10.1. Introduction🔗

HexMvHensel reconstructs multivariate integer factors from a factorization of a univariate image. The extended EEZ pipeline translates an evaluation point to the origin, installs prescribed leading coefficients, introduces the remaining variables in order, and solves each correction equation in a bounded degree box.

Every partial operation returns Option or a structured failure. Successful public results cross an independent checker, so callers do not need to trust point selection, the diophantine solver, or the reconstruction loop.

35.10.2. Coordinates and images🔗

🔗def
Hex.MvHensel.shift {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (i : Fin (n + 1)) (a : Fin n → Int)
  (p : Hex.MvPoly (n + 1) Int cmp) : Hex.MvPoly (n + 1) Int cmp
Hex.MvHensel.shift {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (i : Fin (n + 1)) (a : Fin n → Int)
  (p : Hex.MvPoly (n + 1) Int cmp) :
  Hex.MvPoly (n + 1) Int cmp

Substitute x_(i.succAbove j) ↦ x_(i.succAbove j) + a j, fixing the main variable x_i.

🔗def
Hex.MvHensel.unshift {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (i : Fin (n + 1)) (a : Fin n → Int)
  (p : Hex.MvPoly (n + 1) Int cmp) : Hex.MvPoly (n + 1) Int cmp
Hex.MvHensel.unshift {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (i : Fin (n + 1)) (a : Fin n → Int)
  (p : Hex.MvPoly (n + 1) Int cmp) :
  Hex.MvPoly (n + 1) Int cmp

Undo shift i a.

🔗def
Hex.MvHensel.imageAt {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (a : Fin n → Int) (p : Hex.MvPoly (n + 1) Int cmp) : Hex.DensePoly Int
Hex.MvHensel.imageAt {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (a : Fin n → Int)
  (p : Hex.MvPoly (n + 1) Int cmp) :
  Hex.DensePoly Int

The univariate image at a, obtained by sparse Horner evaluation of every coefficient in the recursive view in the non-main variables.

🔗def
Hex.MvHensel.lcIn {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) Int cmp) : Hex.MvPoly n Int cmp'
Hex.MvHensel.lcIn {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (p : Hex.MvPoly (n + 1) Int cmp) :
  Hex.MvPoly n Int cmp'

Leading coefficient in the chosen main variable, as a polynomial in the remaining variables.

🔗def
Hex.MvHensel.truncate {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (i : Fin (n + 1)) (d : Fin n → Nat)
  (p : Hex.MvPoly (n + 1) Int cmp) : Hex.MvPoly (n + 1) Int cmp
Hex.MvHensel.truncate {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp]
  (i : Fin (n + 1)) (d : Fin n → Nat)
  (p : Hex.MvPoly (n + 1) Int cmp) :
  Hex.MvPoly (n + 1) Int cmp

Delete every term whose exponent in a non-main variable exceeds the corresponding component of d.

The chosen main variable is fixed by translation. imageAt evaluates every remaining-variable coefficient, while lcIn retains the top coefficient as a polynomial in those variables.

35.10.3. Univariate and multivariate corrections🔗

🔗structure
Hex.MvHensel.UniValid (q : Nat) (images witness : List Hex.ZPoly) : Prop
Hex.MvHensel.UniValid (q : Nat)
  (images witness : List Hex.ZPoly) : Prop

The direct hypotheses on the univariate data extracted from V1, V5 and V6 of a valid multivariate lift input.

Constructor

Hex.MvHensel.UniValid.mk

Fields

modulus : 1 < q

A working prime power is nontrivial.

lengths : witness.length = images.length

There is one witness component per image.

positiveDegree : ∀ (j : Nat), j < images.length → 0 < Hex.DensePoly.natDegree (images.getD j 0)

Constant images have already been removed as content.

unitLeading : ∀ (j : Nat), j < images.length → (Hex.DensePoly.leadingCoeff (images.getD j 0)).gcd ↑q = 1

Every image has unit leading coefficient modulo the prime power.

identity : Hex.MvHensel.UniCongr q (Hex.MvHensel.uniCombination witness (Hex.MvHensel.complements images)) 1

The supplied tuple is a partial-fraction identity.

witnessDegree : ∀ (j : Nat), j < images.length → Hex.DensePoly.natDegree (witness.getD j 0) < Hex.DensePoly.natDegree (images.getD j 0)

Witness components use their degree-bounded representatives.

🔗def
Hex.MvHensel.solveUni (q : Nat) (images witness : List Hex.ZPoly)
  (c : Hex.ZPoly) : List Hex.ZPoly
Hex.MvHensel.solveUni (q : Nat)
  (images witness : List Hex.ZPoly)
  (c : Hex.ZPoly) : List Hex.ZPoly

Given a partial-fraction witness, return the symmetric-canonical, degree-bounded solution of the univariate correction equation.

🔗theorem
Hex.MvHensel.solveUni_spec {q : Nat} {images witness : List Hex.ZPoly}
  {c : Hex.ZPoly} (h : Hex.MvHensel.UniValid q images witness)
  (hc :
    Hex.DensePoly.natDegree (Hex.MvHensel.reduceUni q c) <
      Hex.DensePoly.natDegree (Hex.MvHensel.uniProduct images)) :
  Hex.MvHensel.UniCongr q
    (Hex.MvHensel.uniCombination
      (Hex.MvHensel.solveUni q images witness c)
      (Hex.MvHensel.complements images))
    c
Hex.MvHensel.solveUni_spec {q : Nat}
  {images witness : List Hex.ZPoly}
  {c : Hex.ZPoly}
  (h :
    Hex.MvHensel.UniValid q images
      witness)
  (hc :
    Hex.DensePoly.natDegree
        (Hex.MvHensel.reduceUni q c) <
      Hex.DensePoly.natDegree
        (Hex.MvHensel.uniProduct
          images)) :
  Hex.MvHensel.UniCongr q
    (Hex.MvHensel.uniCombination
      (Hex.MvHensel.solveUni q images
        witness c)
      (Hex.MvHensel.complements images))
    c

solveUni reconstructs every right-hand side below the product degree.

🔗def
Hex.MvHensel.witnessOf? {n : Nat} (s : Hex.MvHensel.Setup n)
  (images : List Hex.ZPoly) : Option (List Hex.ZPoly)
Hex.MvHensel.witnessOf? {n : Nat}
  (s : Hex.MvHensel.Setup n)
  (images : List Hex.ZPoly) :
  Option (List Hex.ZPoly)

Produce the partial-fraction tuple modulo p ^ l, or none if an image loses degree modulo p, the images are not pairwise coprime there, or the requested exponent is zero.

🔗def
Hex.MvHensel.diophantine {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (q : Nat) (i : Fin (n + 1))
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp']
  (d : Fin n → Nat) (bs : List (Hex.MvPoly (n + 1) Int cmp))
  (images witness : List Hex.ZPoly) (c : Hex.MvPoly (n + 1) Int cmp) :
  Option (List (Hex.MvPoly (n + 1) Int cmp))
Hex.MvHensel.diophantine {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Hex.IsMonomialOrder cmp] (q : Nat)
  (i : Fin (n + 1))
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp']
  (d : Fin n → Nat)
  (bs : List (Hex.MvPoly (n + 1) Int cmp))
  (images witness : List Hex.ZPoly)
  (c : Hex.MvPoly (n + 1) Int cmp) :
  Option
    (List (Hex.MvPoly (n + 1) Int cmp))

Solve Σ_j Δ_j b_j ≡ c (mod q) inside the non-main degree box d, with deg_i Δ_j < deg images[j]. A malformed tuple, an out-of-range recursive right-hand side, or a failed final equation returns none.

🔗theorem
Hex.MvHensel.diophantine_spec {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {q : Nat} {i : Fin (n + 1)}
  {d : Fin n → Nat} {bs : List (Hex.MvPoly (n + 1) Int cmp)}
  {images witness : List Hex.ZPoly} {c : Hex.MvPoly (n + 1) Int cmp}
  (huni : Hex.MvHensel.UniValid q images witness)
  (hbs : bs.length = images.length)
  (hc :
    Hex.MvPoly.degreeOf i c <
      Hex.DensePoly.natDegree (Hex.MvHensel.uniProduct images))
  (hb :
    ∀ (j : Nat),
      j < bs.length →
        Hex.MvHensel.imageAt i cmp' (fun x => 0) (bs.getD j 0) =
          (Hex.MvHensel.complements images).getD j 0)
  (hbdeg :
    ∀ (j : Nat),
      j < bs.length →
        Hex.MvPoly.degreeOf i (bs.getD j 0) +
            Hex.DensePoly.natDegree (images.getD j 0) ≤
          Hex.DensePoly.natDegree (Hex.MvHensel.uniProduct images)) :
  ∃ answer sum,
    Hex.MvHensel.diophantine q i cmp' d bs images witness c =
        some answer ∧
      Hex.MvHensel.mvCombination? answer bs = some sum ∧
        Hex.MvHensel.BoxCongr i d q sum c ∧
          ∀ (j : Nat),
            j < images.length →
              Hex.MvPoly.degreeOf i (answer.getD j 0) <
                Hex.DensePoly.natDegree (images.getD j 0)
Hex.MvHensel.diophantine_spec {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {q : Nat}
  {i : Fin (n + 1)} {d : Fin n → Nat}
  {bs : List (Hex.MvPoly (n + 1) Int cmp)}
  {images witness : List Hex.ZPoly}
  {c : Hex.MvPoly (n + 1) Int cmp}
  (huni :
    Hex.MvHensel.UniValid q images
      witness)
  (hbs : bs.length = images.length)
  (hc :
    Hex.MvPoly.degreeOf i c <
      Hex.DensePoly.natDegree
        (Hex.MvHensel.uniProduct images))
  (hb :
    ∀ (j : Nat),
      j < bs.length →
        Hex.MvHensel.imageAt i cmp'
            (fun x => 0) (bs.getD j 0) =
          (Hex.MvHensel.complements
                images).getD
            j 0)
  (hbdeg :
    ∀ (j : Nat),
      j < bs.length →
        Hex.MvPoly.degreeOf i
              (bs.getD j 0) +
            Hex.DensePoly.natDegree
              (images.getD j 0) ≤
          Hex.DensePoly.natDegree
            (Hex.MvHensel.uniProduct
              images)) :
  ∃ answer sum,
    Hex.MvHensel.diophantine q i cmp' d bs
          images witness c =
        some answer ∧
      Hex.MvHensel.mvCombination? answer
            bs =
          some sum ∧
        Hex.MvHensel.BoxCongr i d q sum
            c ∧
          ∀ (j : Nat),
            j < images.length →
              Hex.MvPoly.degreeOf i
                  (answer.getD j 0) <
                Hex.DensePoly.natDegree
                  (images.getD j 0)

Under the partial-fraction hypotheses and the load-bearing degree bound on the multivariate bases, the recursive solve succeeds, satisfies the box equation, and preserves each factor's main-variable degree bound.

The univariate solver chooses degree-bounded symmetric representatives modulo the prime power. The recursive solver lifts this partial-fraction equation through the non-main variables and checks the final box congruence.

35.10.4. Inputs, certificates, and replay🔗

🔗structure
Hex.MvHensel.Input (n : Nat)
  (cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering)
  (cmp' : Hex.Mono n → Hex.Mono n → Ordering) [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] : Type
Hex.MvHensel.Input (n : Nat)
  (cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering)
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] : Type

The starting data for one multivariate lift.

Constructor

Hex.MvHensel.Input.mk

Fields

setup : Hex.MvHensel.Setup n

Selected main variable, evaluation point, prime, and exponent.

target : Hex.MvPoly (n + 1) Int cmp

Multivariate polynomial whose factors are to be lifted.

images : List Hex.ZPoly

Univariate factors of the target at the evaluation point.

leading : List (Hex.MvPoly n Int cmp')

Prescribed leading coefficients for the lifted factors.

witness : List Hex.ZPoly

Univariate partial-fraction witnesses for the image factors.

🔗inductive type
Hex.MvHensel.Failure : Type
Hex.MvHensel.Failure : Type

Failures retain the distinction between malformed input, an unsuitable point or prime, and failure to reconstruct at the available modulus.

Constructors

Hex.MvHensel.Failure.arity : Hex.MvHensel.Failure

Tuple arities, degrees, or setup parameters are malformed.

Hex.MvHensel.Failure.degreeDrop : Hex.MvHensel.Failure

Evaluation lowers the target's main-variable degree.

Hex.MvHensel.Failure.imageProduct : Hex.MvHensel.Failure

The univariate images do not multiply to the evaluated target.

Hex.MvHensel.Failure.leadingProduct : Hex.MvHensel.Failure

The prescribed leading coefficients do not multiply correctly.

Hex.MvHensel.Failure.leadingImage (j : Nat) :
  Hex.MvHensel.Failure

A leading coefficient has the wrong image at the selected point.

Hex.MvHensel.Failure.primeDividesLc (j : Nat) :
  Hex.MvHensel.Failure

The working prime divides an image leading coefficient.

Hex.MvHensel.Failure.notCoprime : Hex.MvHensel.Failure

The univariate images are not pairwise coprime modulo the prime.

Hex.MvHensel.Failure.witnessDegree (j : Nat) :
  Hex.MvHensel.Failure

A partial-fraction witness exceeds its permitted degree.

Hex.MvHensel.Failure.reconstruct (modulus : Nat) :
  Hex.MvHensel.Failure

Integer reconstruction failed at the reported modulus.

🔗def
Hex.MvHensel.valid {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] (inp : Hex.MvHensel.Input n cmp cmp') :
  Bool
Hex.MvHensel.valid {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  (inp : Hex.MvHensel.Input n cmp cmp') :
  Bool

Boolean form of the V1--V6 input contract.

🔗structure
Hex.MvHensel.Cert (n : Nat)
  (cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering)
  [Hex.IsMonomialOrder cmp] : Type
Hex.MvHensel.Cert (n : Nat)
  (cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering)
  [Hex.IsMonomialOrder cmp] : Type

The lifted factor tuple is the complete certificate payload.

Constructor

Hex.MvHensel.Cert.mk

Fields

factors : List (Hex.MvPoly (n + 1) Int cmp)

Reconstructed multivariate factors in image-factor order.

🔗def
Hex.MvHensel.check {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] (inp : Hex.MvHensel.Input n cmp cmp')
  (cert : Hex.MvHensel.Cert n cmp) : Bool
Hex.MvHensel.check {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  (inp : Hex.MvHensel.Input n cmp cmp')
  (cert : Hex.MvHensel.Cert n cmp) : Bool

Replay the exact product, image, and leading-coefficient conditions.

🔗theorem
Hex.MvHensel.check_sound {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {inp : Hex.MvHensel.Input n cmp cmp'}
  {cert : Hex.MvHensel.Cert n cmp}
  (h : Hex.MvHensel.check inp cert = true) :
  Hex.MvHensel.IsLiftOf inp cert.factors
Hex.MvHensel.check_sound {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  {inp : Hex.MvHensel.Input n cmp cmp'}
  {cert : Hex.MvHensel.Cert n cmp}
  (h :
    Hex.MvHensel.check inp cert = true) :
  Hex.MvHensel.IsLiftOf inp cert.factors

The executable checker implies the semantic certificate predicate.

Validation covers tuple arities, absence of degree drop, image and leading coefficient products, leading images, the working prime, coprimality, and witness degree. Replay then establishes exact reassembly and the frame of every returned factor.

35.10.5. Stagewise lifting and retries🔗

🔗def
Hex.MvHensel.IsStage {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] (inp : Hex.MvHensel.Input n cmp cmp')
  (count : Nat) (factors : List (Hex.MvPoly (n + 1) Int cmp)) : Prop
Hex.MvHensel.IsStage {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  (inp : Hex.MvHensel.Input n cmp cmp')
  (count : Nat)
  (factors :
    List (Hex.MvPoly (n + 1) Int cmp)) :
  Prop

The state carried between EEZ stages. It records exactly the facts used at the next diophantinePrefix call: fixed image and main degree, installed leading prefix, absence of future variables, and the product equation through the completed prefix.

🔗def
Hex.MvHensel.lift {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] (inp : Hex.MvHensel.Input n cmp cmp') :
  Except Hex.MvHensel.Failure (Hex.MvHensel.Cert n cmp)
Hex.MvHensel.lift {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  (inp : Hex.MvHensel.Input n cmp cmp') :
  Except Hex.MvHensel.Failure
    (Hex.MvHensel.Cert n cmp)

Perform one checked lift at the exponent stored in inp.setup.

🔗def
Hex.MvHensel.liftWith {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] (cfg : Hex.MvHensel.Config)
  (inp : Hex.MvHensel.Input n cmp cmp') :
  Except Hex.MvHensel.Failure (Hex.MvHensel.Cert n cmp)
Hex.MvHensel.liftWith {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  (cfg : Hex.MvHensel.Config)
  (inp : Hex.MvHensel.Input n cmp cmp') :
  Except Hex.MvHensel.Failure
    (Hex.MvHensel.Cert n cmp)

Lift with the configured number of exponent doublings.

🔗theorem
Hex.MvHensel.lift_checks {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {inp : Hex.MvHensel.Input n cmp cmp'}
  {cert : Hex.MvHensel.Cert n cmp}
  (h : Hex.MvHensel.lift inp = Except.ok cert) :
  Hex.MvHensel.check inp cert = true
Hex.MvHensel.lift_checks {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  {inp : Hex.MvHensel.Input n cmp cmp'}
  {cert : Hex.MvHensel.Cert n cmp}
  (h :
    Hex.MvHensel.lift inp =
      Except.ok cert) :
  Hex.MvHensel.check inp cert = true

Every certificate returned by lift passes the independent checker.

🔗theorem
Hex.MvHensel.lift_progress {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {inp : Hex.MvHensel.Input n cmp cmp'}
  (h : Hex.MvHensel.valid inp = true) :
  (∃ cert, Hex.MvHensel.lift inp = Except.ok cert) ∨
    ∃ modulus,
      Hex.MvHensel.lift inp =
        Except.error (Hex.MvHensel.Failure.reconstruct modulus)
Hex.MvHensel.lift_progress {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  {inp : Hex.MvHensel.Input n cmp cmp'}
  (h : Hex.MvHensel.valid inp = true) :
  (∃ cert,
      Hex.MvHensel.lift inp =
        Except.ok cert) ∨
    ∃ modulus,
      Hex.MvHensel.lift inp =
        Except.error
          (Hex.MvHensel.Failure.reconstruct
            modulus)

Once V1--V6 hold, reconstruction is the only possible failure.

Reconstruction failures retain the attempted modulus. liftWith can double the exponent and regenerate the partial-fraction witness a bounded number of times; malformed inputs are not retried.

35.10.6. Uniqueness and completeness🔗

🔗def
Hex.MvHensel.coeffBound {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] (inp : Hex.MvHensel.Input n cmp cmp') : Nat
Hex.MvHensel.coeffBound {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  (inp : Hex.MvHensel.Input n cmp cmp') :
  Nat

A uniform factor-coefficient bound obtained by translating the target, using the corrected mixed-radix Kronecker substitution, and applying the closed-form univariate Mignotte bound.

🔗theorem
Hex.MvHensel.lift_unique {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {inp : Hex.MvHensel.Input n cmp cmp'}
  {fs gs : List (Hex.MvPoly (n + 1) Int cmp)}
  (h : Hex.MvHensel.valid inp = true)
  (h1 : Hex.MvHensel.IsLiftOf inp fs)
  (h2 : Hex.MvHensel.IsLiftOf inp gs) : fs = gs
Hex.MvHensel.lift_unique {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  {inp : Hex.MvHensel.Input n cmp cmp'}
  {fs gs :
    List (Hex.MvPoly (n + 1) Int cmp)}
  (h : Hex.MvHensel.valid inp = true)
  (h1 : Hex.MvHensel.IsLiftOf inp fs)
  (h2 : Hex.MvHensel.IsLiftOf inp gs) :
  fs = gs

At most one exact factor tuple is compatible with a valid lift input.

🔗theorem
Hex.MvHensel.lift_complete {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {inp : Hex.MvHensel.Input n cmp cmp'}
  {bound : Nat} (h : Hex.MvHensel.valid inp = true)
  (hB : Hex.MvHensel.BoundsFactors inp bound)
  (hq : 2 * bound < inp.setup.modulus)
  (hex : ∃ fs, Hex.MvHensel.IsLiftOf inp fs) :
  ∃ cert, Hex.MvHensel.lift inp = Except.ok cert
Hex.MvHensel.lift_complete {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  {inp : Hex.MvHensel.Input n cmp cmp'}
  {bound : Nat}
  (h : Hex.MvHensel.valid inp = true)
  (hB :
    Hex.MvHensel.BoundsFactors inp bound)
  (hq : 2 * bound < inp.setup.modulus)
  (hex :
    ∃ fs, Hex.MvHensel.IsLiftOf inp fs) :
  ∃ cert,
    Hex.MvHensel.lift inp = Except.ok cert

Above twice a valid coefficient bound, every compatible factorization is found by the concrete lift.

🔗theorem
Hex.MvHensel.no_lift_of_reconstruct {n : Nat}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  {cmp' : Hex.Mono n → Hex.Mono n → Ordering} [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp'] {inp : Hex.MvHensel.Input n cmp cmp'}
  {bound modulus : Nat} (h : Hex.MvHensel.valid inp = true)
  (hB : Hex.MvHensel.BoundsFactors inp bound)
  (hq : 2 * bound < inp.setup.modulus)
  (hfail :
    Hex.MvHensel.lift inp =
      Except.error (Hex.MvHensel.Failure.reconstruct modulus)) :
  ¬∃ fs, Hex.MvHensel.IsLiftOf inp fs
Hex.MvHensel.no_lift_of_reconstruct
  {n : Nat}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  {cmp' :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Hex.IsMonomialOrder cmp]
  [Hex.IsMonomialOrder cmp']
  {inp : Hex.MvHensel.Input n cmp cmp'}
  {bound modulus : Nat}
  (h : Hex.MvHensel.valid inp = true)
  (hB :
    Hex.MvHensel.BoundsFactors inp bound)
  (hq : 2 * bound < inp.setup.modulus)
  (hfail :
    Hex.MvHensel.lift inp =
      Except.error
        (Hex.MvHensel.Failure.reconstruct
          modulus)) :
  ¬∃ fs, Hex.MvHensel.IsLiftOf inp fs

Past the coefficient bound, reconstruction failure proves that the point admits no compatible factorization.

The executable bound applies mixed-radix Kronecker substitution after the coordinate shift. Once the modulus exceeds twice a valid factor-coefficient bound, reconstruction is complete and a reconstruction failure proves that no compatible lift tuple exists.

35.10.7. Cross-references🔗

  • HexModular supplies arbitrary-precision symmetric residues and rational reconstruction infrastructure.

  • HexMvGcd supplies named-variable content and the gcd layer used by the completeness contracts.

  • HexMvFactor constructs valid lift inputs, distributes leading coefficients, and recombines the checked factors.