hex

35.6. HexModular: CRT and rational reconstruction🔗

35.6.1. Introduction🔗

HexModular provides executable symmetric residues, incremental Chinese remaindering, rational reconstruction, and a bounded multimodular loop. The implementation is Mathlib-free and uses HexArith for its compiled integer extended GCD.

Every search routine checks its output before returning it. Downstream algorithms can replay the small public correctness lemmas without unfolding the Euclidean search or trusting an external oracle.

35.6.2. Symmetric representatives🔗

🔗def
Hex.Modular.symMod (a : Int) (m : Nat) : Int
Hex.Modular.symMod (a : Int) (m : Nat) :
  Int

The representative of a modulo m in the interval (-m/2, m/2]. For the degenerate modulus zero, this returns a, matching Int.emod's zero-modulus convention.

The three characterizing theorems say that reduction preserves the ordinary residue, lands in the closed half-modulus interval, and is unique away from the even-modulus tie.

🔗theorem
Hex.Modular.symMod_emod {a : Int} {m : Nat} (h : 0 < m) :
  Hex.Modular.symMod a m % ↑m = a % ↑m
Hex.Modular.symMod_emod {a : Int}
  {m : Nat} (h : 0 < m) :
  Hex.Modular.symMod a m % ↑m = a % ↑m

Symmetric reduction preserves the ordinary nonnegative residue at every positive modulus.

🔗theorem
Hex.Modular.symMod_le {a : Int} {m : Nat} (h : 0 < m) :
  2 * (Hex.Modular.symMod a m).natAbs ≤ m
Hex.Modular.symMod_le {a : Int} {m : Nat}
  (h : 0 < m) :
  2 * (Hex.Modular.symMod a m).natAbs ≤ m

A symmetric representative has absolute value at most half its positive modulus, with the positive representative selected at an even tie.

🔗theorem
Hex.Modular.symMod_unique {a x : Int} {m : Nat} (h : 2 * x.natAbs < m)
  (hx : x % ↑m = a % ↑m) : Hex.Modular.symMod a m = x
Hex.Modular.symMod_unique {a x : Int}
  {m : Nat} (h : 2 * x.natAbs < m)
  (hx : x % ↑m = a % ↑m) :
  Hex.Modular.symMod a m = x

A strictly-half-bounded integer congruent to a is the unique symmetric representative. The strict bound excludes the two representatives at an even tie.

35.6.3. Incremental Chinese remaindering🔗

🔗structure
Hex.Modular.Crt : Type
Hex.Modular.Crt : Type

A residue accumulated from coprime moduli. value is the symmetric representative of their common solution modulo modulus.

Constructor

Hex.Modular.Crt.mk

Fields

modulus : Nat

Product of the moduli already folded into the state.

value : Int

Symmetric representative of the accumulated residue.

pos : 0 < self.modulus

The accumulated modulus is positive.

le : 2 * self.value.natAbs ≤ self.modulus

The representative lies in the symmetric interval.

🔗def
Hex.Modular.Crt.init : Hex.Modular.Crt
Hex.Modular.Crt.init : Hex.Modular.Crt

The empty scalar CRT accumulation, modulo one.

🔗def
Hex.Modular.Crt.push (c : Hex.Modular.Crt) (r : Int) (m : Nat) :
  Option Hex.Modular.Crt
Hex.Modular.Crt.push (c : Hex.Modular.Crt)
  (r : Int) (m : Nat) :
  Option Hex.Modular.Crt

Fold the residue r modulo m into a scalar CRT accumulation using one Garner mixed-radix step. Moduli zero and one and moduli not coprime to the accumulated modulus are rejected.

A successful push multiplies the accumulated modulus, records the new residue, and preserves every residue already represented by the state.

🔗theorem
Hex.Modular.Crt.push_modulus {c c' : Hex.Modular.Crt} {r : Int}
  {m : Nat} (h : c.push r m = some c') : c'.modulus = c.modulus * m
Hex.Modular.Crt.push_modulus
  {c c' : Hex.Modular.Crt} {r : Int}
  {m : Nat} (h : c.push r m = some c') :
  c'.modulus = c.modulus * m

A successful scalar push multiplies the accumulated modulus by the new one.

🔗theorem
Hex.Modular.Crt.push_congr_new {c c' : Hex.Modular.Crt} {r : Int}
  {m : Nat} (h : c.push r m = some c') : c'.value % ↑m = r % ↑m
Hex.Modular.Crt.push_congr_new
  {c c' : Hex.Modular.Crt} {r : Int}
  {m : Nat} (h : c.push r m = some c') :
  c'.value % ↑m = r % ↑m

A successful scalar push records the requested new residue.

🔗theorem
Hex.Modular.Crt.push_congr_old {c c' : Hex.Modular.Crt} {r : Int}
  {m d : Nat} (hd : d ∣ c.modulus) (h : c.push r m = some c') :
  c'.value % ↑d = c.value % ↑d
Hex.Modular.Crt.push_congr_old
  {c c' : Hex.Modular.Crt} {r : Int}
  {m d : Nat} (hd : d ∣ c.modulus)
  (h : c.push r m = some c') :
  c'.value % ↑d = c.value % ↑d

A successful scalar push preserves the accumulated value modulo every divisor of the old accumulated modulus.

🔗theorem
Hex.Modular.crt_unique {c : Hex.Modular.Crt} {x y : Int}
  (h : 2 * x.natAbs < c.modulus) (h' : 2 * y.natAbs < c.modulus)
  (hx : x % ↑c.modulus = y % ↑c.modulus) : x = y
Hex.Modular.crt_unique
  {c : Hex.Modular.Crt} {x y : Int}
  (h : 2 * x.natAbs < c.modulus)
  (h' : 2 * y.natAbs < c.modulus)
  (hx : x % ↑c.modulus = y % ↑c.modulus) :
  x = y

Two integers strictly smaller than half the accumulated modulus and congruent modulo that modulus are equal.

For several residue streams sharing the same moduli, Hex.Modular.CrtVec computes one inverse per push and reuses it across all coordinates. Its push_modulus, push_congr_new, and push_congr_old theorems have the same shape as the scalar results.

35.6.4. Rational reconstruction🔗

🔗structure
Hex.Modular.Row : Type
Hex.Modular.Row : Type

One row of the extended Euclidean remainder sequence on (m, a). The omitted coefficient of m is never inspected by reconstruction consumers.

Constructor

Hex.Modular.Row.mk

Fields

r : Int

The current Euclidean remainder.

t : Int

The coefficient of the second input a.

🔗def
Hex.Modular.euclidUntil (m a P : Int) : Hex.Modular.Row
Hex.Modular.euclidUntil (m a P : Int) :
  Hex.Modular.Row

Return the first row of the extended Euclidean remainder sequence on (m, a) whose remainder is at most P. The modulus is interpreted up to sign, and a is reduced before entering the recurrence.

🔗def
Hex.Modular.ratRecon? (a : Int) (m : Nat) (P Q : Int) : Option Rat
Hex.Modular.ratRecon? (a : Int) (m : Nat)
  (P Q : Int) : Option Rat

Reconstruct a mod m as a rational with numerator absolute value at most P and positive denominator at most Q. The truncated Euclidean candidate is normalized and all output conditions are checked before it is returned.

🔗def
Hex.Modular.ratReconWide? (a : Int) (m : Nat) : Option Rat
Hex.Modular.ratReconWide? (a : Int)
  (m : Nat) : Option Rat

Symmetric rational reconstruction with P = Q = ⌊√((m-1)/2)⌋, which guarantees 2 P Q < m.

Successful bounded reconstruction supplies congruence and size facts, and the reduced denominator is coprime to the modulus. Under the standard strict uniqueness bound, every admissible rational is found.

🔗theorem
Hex.Modular.ratRecon?_congr {a : Int} {m : Nat} {P Q : Int} {x : Rat}
  (h : Hex.Modular.ratRecon? a m P Q = some x) :
  (Int.ofNat x.den * a - x.num) % ↑m = 0
Hex.Modular.ratRecon?_congr {a : Int}
  {m : Nat} {P Q : Int} {x : Rat}
  (h :
    Hex.Modular.ratRecon? a m P Q =
      some x) :
  (Int.ofNat x.den * a - x.num) % ↑m = 0

Every rational returned by bounded reconstruction satisfies the requested modular congruence.

🔗theorem
Hex.Modular.ratRecon?_bounds {a : Int} {m : Nat} {P Q : Int} {x : Rat}
  (h : Hex.Modular.ratRecon? a m P Q = some x) :
  ↑x.num.natAbs ≤ P ∧ 0 < x.den ∧ ↑x.den ≤ Q
Hex.Modular.ratRecon?_bounds {a : Int}
  {m : Nat} {P Q : Int} {x : Rat}
  (h :
    Hex.Modular.ratRecon? a m P Q =
      some x) :
  ↑x.num.natAbs ≤ P ∧
    0 < x.den ∧ ↑x.den ≤ Q

Every rational returned by bounded reconstruction satisfies the requested numerator and denominator bounds.

🔗theorem
Hex.Modular.ratRecon?_den_coprime {a : Int} {m : Nat} {P Q : Int}
  {x : Rat} (h : Hex.Modular.ratRecon? a m P Q = some x) :
  x.den.gcd m = 1
Hex.Modular.ratRecon?_den_coprime
  {a : Int} {m : Nat} {P Q : Int}
  {x : Rat}
  (h :
    Hex.Modular.ratRecon? a m P Q =
      some x) :
  x.den.gcd m = 1

The reduced denominator of a successful reconstruction is coprime to the modulus.

🔗theorem
Hex.Modular.ratRecon_unique {a P Q : Int} {m : Nat} {y₁ y₂ : Rat}
  (hm : 2 * P * Q < ↑m) (h₁ : (Int.ofNat y₁.den * a - y₁.num) % ↑m = 0)
  (h₂ : (Int.ofNat y₂.den * a - y₂.num) % ↑m = 0)
  (b₁ : ↑y₁.num.natAbs ≤ P ∧ ↑y₁.den ≤ Q)
  (b₂ : ↑y₂.num.natAbs ≤ P ∧ ↑y₂.den ≤ Q) : y₁ = y₂
Hex.Modular.ratRecon_unique {a P Q : Int}
  {m : Nat} {y₁ y₂ : Rat}
  (hm : 2 * P * Q < ↑m)
  (h₁ :
    (Int.ofNat y₁.den * a - y₁.num) % ↑m =
      0)
  (h₂ :
    (Int.ofNat y₂.den * a - y₂.num) % ↑m =
      0)
  (b₁ : ↑y₁.num.natAbs ≤ P ∧ ↑y₁.den ≤ Q)
  (b₂ :
    ↑y₂.num.natAbs ≤ P ∧ ↑y₂.den ≤ Q) :
  y₁ = y₂

Rational reconstruction is unique whenever twice the product of the two bounds is strictly smaller than the modulus.

🔗theorem
Hex.Modular.ratRecon?_complete {a P Q : Int} {m : Nat} {y : Rat}
  (hm : 2 * P * Q < ↑m) (hy : (Int.ofNat y.den * a - y.num) % ↑m = 0)
  (hb : ↑y.num.natAbs ≤ P ∧ ↑y.den ≤ Q) :
  Hex.Modular.ratRecon? a m P Q = some y
Hex.Modular.ratRecon?_complete
  {a P Q : Int} {m : Nat} {y : Rat}
  (hm : 2 * P * Q < ↑m)
  (hy :
    (Int.ofNat y.den * a - y.num) % ↑m =
      0)
  (hb : ↑y.num.natAbs ≤ P ∧ ↑y.den ≤ Q) :
  Hex.Modular.ratRecon? a m P Q = some y

Under the uniqueness bound, bounded reconstruction finds every rational that satisfies the congruence and bounds.

🔗def
Hex.Modular.ratReconVec? {k : Nat} (a : Vector Int k) (m : Nat)
  (P Q : Int) : Option (Vector Int k × Int)
Hex.Modular.ratReconVec? {k : Nat}
  (a : Vector Int k) (m : Nat)
  (P Q : Int) :
  Option (Vector Int k × Int)

Reconstruct k residues as rationals with a common denominator. The first entry seeds the denominator. Later entries first try one symmetric multiplication at that denominator, falling back to their own Euclidean run only when necessary. Denominators are combined with lcm, and the final numerator vector and denominator are reduced by their common gcd.

The maximal-quotient variant is intentionally heuristic. Its theorem promises only the checked modular congruence, not recovery of a preferred rational.

🔗def
Hex.Modular.ratReconMaxQuot? (a : Int) (m : Nat) : Option Rat
Hex.Modular.ratReconMaxQuot? (a : Int)
  (m : Nat) : Option Rat

Produce the maximal-quotient rational-reconstruction candidate. This is a heuristic: only the modular congruence is checked and promised.

🔗theorem
Hex.Modular.ratReconMaxQuot?_congr {a : Int} {m : Nat} {x : Rat}
  (h : Hex.Modular.ratReconMaxQuot? a m = some x) :
  (Int.ofNat x.den * a - x.num) % ↑m = 0
Hex.Modular.ratReconMaxQuot?_congr
  {a : Int} {m : Nat} {x : Rat}
  (h :
    Hex.Modular.ratReconMaxQuot? a m =
      some x) :
  (Int.ofNat x.den * a - x.num) % ↑m = 0

A maximal-quotient candidate always satisfies the modular congruence; no claim is made that it is the intended rational.

35.6.5. Multimodular loops🔗

🔗def
Hex.Modular.crtLoop.{u_1} {k : Nat} {α : Type u_1}
  (image : Nat → Option (Vector Int k))
  (accept : Hex.Modular.CrtVec k → Option α) (supply : Array Nat)
  (fuel : Nat) : Option α
Hex.Modular.crtLoop.{u_1} {k : Nat}
  {α : Type u_1}
  (image : Nat → Option (Vector Int k))
  (accept :
    Hex.Modular.CrtVec k → Option α)
  (supply : Array Nat) (fuel : Nat) :
  Option α

Fold moduli into a vector CRT state until the caller-supplied exact check accepts a reconstruction. A rejected image never enters the state, and the fuel bounds the number of supply entries inspected.

The loop skips missing images and rejected moduli, tests the caller's exact acceptance function only after a successful push, and consumes at most the supplied fuel. Hex.Modular.CrtTrace records the precise consumed prefix.

🔗theorem
Hex.Modular.crtLoop_trace.{u_1} {k : Nat} {α : Type u_1}
  {image : Nat → Option (Vector Int k)}
  {accept : Hex.Modular.CrtVec k → Option α} {supply : Array Nat}
  {fuel : Nat} {x : α}
  (h : Hex.Modular.crtLoop image accept supply fuel = some x) :
  ∃ consumed state,
    0 < consumed ∧
      consumed ≤ fuel ∧
        consumed ≤ supply.size ∧
          Hex.Modular.CrtTrace image supply consumed state ∧
            accept state = some x
Hex.Modular.crtLoop_trace.{u_1} {k : Nat}
  {α : Type u_1}
  {image : Nat → Option (Vector Int k)}
  {accept :
    Hex.Modular.CrtVec k → Option α}
  {supply : Array Nat} {fuel : Nat}
  {x : α}
  (h :
    Hex.Modular.crtLoop image accept
        supply fuel =
      some x) :
  ∃ consumed state,
    0 < consumed ∧
      consumed ≤ fuel ∧
        consumed ≤ supply.size ∧
          Hex.Modular.CrtTrace image
              supply consumed state ∧
            accept state = some x

A successful loop result is accepted on a state reached by replaying the exact consumed supply prefix. The consumed prefix is nonempty because the loop tests accept only after a successful push, and it cannot exceed fuel.

🔗theorem
Hex.Modular.crtLoop_of_some.{u_1} {k : Nat} {α : Type u_1}
  {image : Nat → Option (Vector Int k)}
  {accept : Hex.Modular.CrtVec k → Option α} {supply : Array Nat}
  {fuel : Nat} {x : α}
  (h : Hex.Modular.crtLoop image accept supply fuel = some x) :
  ∃ state, accept state = some x
Hex.Modular.crtLoop_of_some.{u_1}
  {k : Nat} {α : Type u_1}
  {image : Nat → Option (Vector Int k)}
  {accept :
    Hex.Modular.CrtVec k → Option α}
  {supply : Array Nat} {fuel : Nat}
  {x : α}
  (h :
    Hex.Modular.crtLoop image accept
        supply fuel =
      some x) :
  ∃ state, accept state = some x

Every successful loop result was returned by accept on some accumulated CRT state; the loop itself never manufactures a caller result.

35.6.5.1. Worked example🔗

The first computation combines 1 mod 3 and 0 mod 2; the second recovers the rational 2/3 from its residue 68 mod 101.

open Hex.Modular namespace HexModularChapter def combined : Option (Nat × Int) := do let first ← Crt.init.push 1 3 let second ← first.push 0 2 pure (second.modulus, second.value) #guard combined = some (6, -2) #guard symMod 17 10 = -3 #guard ratRecon? 68 101 8 8 = some (Rat.divInt 2 3) end HexModularChapter

35.6.6. The Mathlib correspondence🔗

The executable library states congruence using integer remainders and Rat. The specified HexModularMathlib companion transports those results to ZMod and ℚ, including the Chinese-remainder equivalence and rational reconstruction predicates. Until that bridge is available, the integer congruence lemmas above are the supported proof boundary.

35.6.7. Cross-references🔗

  • HexArith supplies the compiled extended GCD used by CRT accumulation.

  • HexModArith supplies the bundled deterministic modulus stream used by modular algorithms.

  • HexPolyZGcd, HexMvGcd, and HexMvHensel consume this library's CRT, reconstruction, and multimodular-loop APIs.