structure Hex.Modular.Crt : Type

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

• 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 : Crt

The empty scalar CRT accumulation, modulo one.

Equations

• Hex.Modular.Crt.init = { modulus := 1, value := 0, pos := Hex.Modular.Crt.init._proof_1, le := Hex.Modular.Crt.init._proof_2 }

def Hex.Modular.Crt.push (c : Crt) (r : Int) (m : Nat) : Option 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.

Equations

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

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

GMP-backed compiled implementation of Crt.push.

Equations

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

@[csimp]

theorem Hex.Modular.Crt.push_eq_impl : push = pushImpl

The compiled CRT step agrees with its kernel-reducible reference.

theorem Hex.Modular.Crt.push_modulus {c c' : 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' : 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' : 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.push_le {c c' : Crt} {r : Int} {m : Nat} (_h : c.push r m = some c') : 2 * c'.value.natAbs ≤ c'.modulus

A successful scalar push preserves the symmetric-size invariant.

structure Hex.Modular.CrtVec (k : Nat) : Type

Several accumulated residues sharing one positive product modulus.

• modulus : Nat

  Product of the moduli already folded into the state.

• value : Vector Int k

  Symmetric representatives of the accumulated residues.

• pos : 0 < self.modulus

  The accumulated modulus is positive.

• le (i : Fin k) : 2 * self.value[i].natAbs ≤ self.modulus

  Every representative lies in the symmetric interval.

def Hex.Modular.CrtVec.init (k : Nat) : CrtVec k

The empty vector CRT accumulation, modulo one.

Equations

• Hex.Modular.CrtVec.init k = { modulus := 1, value := Vector.replicate k 0, pos := Hex.Modular.Crt.init._proof_1, le := ⋯ }

def Hex.Modular.CrtVec.push {k : Nat} (c : CrtVec k) (r : Vector Int k) (m : Nat) : Option (CrtVec k)

Fold k residues sharing modulus m into a vector CRT accumulation. The extended GCD and modular inverse are computed once and reused for every coordinate.

Equations

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

def Hex.Modular.CrtVec.pushImpl {k : Nat} (c : CrtVec k) (r : Vector Int k) (m : Nat) : Option (CrtVec k)

GMP-backed compiled implementation of CrtVec.push.

Equations

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

@[csimp]

theorem Hex.Modular.CrtVec.push_eq_impl : @push = @pushImpl

The compiled vector CRT step agrees with its kernel-reducible reference.

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

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

theorem Hex.Modular.CrtVec.push_congr_new {k : Nat} {c c' : CrtVec k} {r : Vector Int k} {m : Nat} (h : c.push r m = some c') (i : Fin k) : c'.value[i] % ↑m = r[i] % ↑m

A successful vector push records every requested new residue.

theorem Hex.Modular.CrtVec.push_congr_old {k : Nat} {c c' : CrtVec k} {r : Vector Int k} {m d : Nat} (hd : d ∣ c.modulus) (h : c.push r m = some c') (i : Fin k) : c'.value[i] % ↑d = c.value[i] % ↑d

A successful vector push preserves every old accumulated residue modulo every divisor of the old modulus.

theorem Hex.Modular.CrtVec.push_le {k : Nat} {c c' : CrtVec k} {r : Vector Int k} {m : Nat} (_h : c.push r m = some c') (i : Fin k) : 2 * c'.value[i].natAbs ≤ c'.modulus

A successful vector push preserves every symmetric-size invariant.

theorem Hex.Modular.CrtVec.push_coprime {k : Nat} {c c' : CrtVec k} {r : Vector Int k} {m : Nat} (h : c.push r m = some c') : c.modulus.Coprime m

A successful push uses a modulus coprime to the accumulated modulus.

theorem Hex.Modular.CrtVec.push_congr {k : Nat} {c c' : CrtVec k} {r : Vector Int k} {m : Nat} (h : c.push r m = some c') (i : Fin k) (x : Int) (hold : c.value[i] % ↑c.modulus = x % ↑c.modulus) (hnew : r[i] % ↑m = x % ↑m) : c'.value[i] % ↑c'.modulus = x % ↑c'.modulus

Congruence with both the old state and the new image gives congruence modulo the entire accumulated product after a successful push.

theorem Hex.Modular.CrtVec.eq_of_congr {k : Nat} (c : CrtVec k) (i : Fin k) {x : Int} (hx : 2 * x.natAbs < c.modulus) (h : c.value[i] % ↑c.modulus = x % ↑c.modulus) : c.value[i] = x

A strictly half-bounded integer congruent to a state's coordinate equals that coordinate; the stored coordinate only needs its non-strict bound.

theorem Hex.Modular.crt_unique {c : 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.