def Hex.Modular.CrtPlan.checkPairwise : List Nat → Bool

Executable pairwise-coprimality check.

Equations

• Hex.Modular.CrtPlan.checkPairwise [] = true
• Hex.Modular.CrtPlan.checkPairwise (modulus :: moduli) = ((moduli.all fun (other : Nat) => decide (modulus.gcd other = 1)) && Hex.Modular.CrtPlan.checkPairwise moduli)

def Hex.Modular.CrtPlan.check (moduli : Array Nat) : Bool

Executable validation check for a batch CRT plan.

Equations

• Hex.Modular.CrtPlan.check moduli = ((moduli.toList.all fun (modulus : Nat) => decide (1 < modulus)) && Hex.Modular.CrtPlan.checkPairwise moduli.toList)

def Hex.Modular.CrtPlan.Valid (moduli : Array Nat) : Prop

The validation condition for a batch CRT plan.

Equations

• Hex.Modular.CrtPlan.Valid moduli = (Hex.Modular.CrtPlan.check moduli = true)

@[instance_reducible]

instance Hex.Modular.CrtPlan.instDecidableValid (moduli : Array Nat) : Decidable (Valid moduli)

Equations

• Hex.Modular.CrtPlan.instDecidableValid moduli = Hex.Modular.CrtPlan.instDecidableValid._aux_1 moduli

theorem Hex.Modular.CrtPlan.valid_iff {moduli : Array Nat} : Valid moduli ↔ (∀ (m : Nat), m ∈ moduli.toList → 1 < m) ∧ List.Pairwise (fun (left right : Nat) => left.gcd right = 1) moduli.toList

Validation means precisely that every modulus is greater than one and that the moduli are pairwise coprime.

inductive Hex.Modular.CrtPlan.Tree : Type

A balanced modulus-product tree. A branch stores the inverse of the left product modulo the right product.

• empty : Tree
• leaf (modulus : Nat) : Tree
• branch (left right : Tree) (inverse : Int) : Tree

@[instance_reducible]

instance Hex.Modular.CrtPlan.instInhabitedTree : Inhabited Tree

Equations

• Hex.Modular.CrtPlan.instInhabitedTree = { default := Hex.Modular.CrtPlan.instInhabitedTree.default }

def Hex.Modular.CrtPlan.Tree.product : Tree → Nat

Product of all leaf moduli below a CRT tree.

Equations

• Hex.Modular.CrtPlan.Tree.empty.product = 1
• (Hex.Modular.CrtPlan.Tree.leaf modulus).product = modulus
• (left.branch right inverse).product = left.product * right.product

def Hex.Modular.CrtPlan.Tree.merge (left right : Tree) : Tree

Join two adjacent product trees, computing their sibling inverse once.

Equations

• left.merge right = left.branch right (HexArith.Int.extGcd (Int.ofNat (left.product % right.product)) (Int.ofNat right.product)).snd.fst

def Hex.Modular.CrtPlan.Tree.mergeLevel : List Tree → List Tree

Merge adjacent nodes of one product-tree level.

Equations

• Hex.Modular.CrtPlan.Tree.mergeLevel [] = []
• Hex.Modular.CrtPlan.Tree.mergeLevel [tree] = [tree]
• Hex.Modular.CrtPlan.Tree.mergeLevel (left :: right :: rest) = left.merge right :: Hex.Modular.CrtPlan.Tree.mergeLevel rest

def Hex.Modular.CrtPlan.Tree.finish : Nat → List Tree → Tree

Repeatedly merge levels. The initial leaf count is sufficient fuel: every nontrivial level strictly decreases the number of nodes.

Equations

• Hex.Modular.CrtPlan.Tree.finish 0 [] = Hex.Modular.CrtPlan.Tree.empty
• Hex.Modular.CrtPlan.Tree.finish 0 (tree :: tail) = tree
• Hex.Modular.CrtPlan.Tree.finish n.succ [] = Hex.Modular.CrtPlan.Tree.empty
• Hex.Modular.CrtPlan.Tree.finish n.succ [tree] = tree
• Hex.Modular.CrtPlan.Tree.finish fuel.succ x✝ = Hex.Modular.CrtPlan.Tree.finish fuel (Hex.Modular.CrtPlan.Tree.mergeLevel x✝)

def Hex.Modular.CrtPlan.Tree.ofList (moduli : List Nat) : Tree

Build the balanced tree for a list of moduli.

Equations

• Hex.Modular.CrtPlan.Tree.ofList moduli = Hex.Modular.CrtPlan.Tree.finish moduli.length (List.map Hex.Modular.CrtPlan.Tree.leaf moduli)

def Hex.Modular.CrtPlan.Tree.combine (left right inverse : Int) (leftModulus rightModulus : Nat) : Int

Combine two symmetric representatives using a precomputed sibling inverse.

Equations

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

def Hex.Modular.CrtPlan.Tree.eval : Tree → List Int → Int × List Int

Evaluate a scalar reconstruction tree, consuming one residue per leaf.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Modular.CrtPlan.Tree.empty.eval x✝ = (0, x✝)
• (Hex.Modular.CrtPlan.Tree.leaf modulus).eval [] = (0, [])
• (Hex.Modular.CrtPlan.Tree.leaf modulus).eval (residue :: residues) = (Hex.Modular.symMod residue modulus, residues)

def Hex.Modular.CrtPlan.Tree.evalVec (k : Nat) : Tree → List (Vector Int k) → Vector Int k × List (Vector Int k)

Evaluate all lanes of a reconstruction tree together. Every branch uses its stored inverse once for the whole vector.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Modular.CrtPlan.Tree.evalVec k Hex.Modular.CrtPlan.Tree.empty x✝ = (Vector.replicate k 0, x✝)
• Hex.Modular.CrtPlan.Tree.evalVec k (Hex.Modular.CrtPlan.Tree.leaf modulus) [] = (Vector.replicate k 0, [])
• Hex.Modular.CrtPlan.Tree.evalVec k (Hex.Modular.CrtPlan.Tree.leaf modulus) (residue :: residues) = (Vector.map (fun (value : Int) => Hex.Modular.symMod value modulus) residue, residues)

structure Hex.Modular.CrtPlan : Type

A validated balanced product tree of pairwise-coprime moduli greater than one. The tree contains all extended-GCD work needed by reconstruction.

• moduli : Array Nat

  Moduli in residue input order.

• tree : Tree

  Balanced product tree with precomputed sibling inverses.

• valid : Valid self.moduli

  All moduli are greater than one and pairwise coprime.

def Hex.Modular.CrtPlan.modulus (plan : CrtPlan) : Nat

Product of every modulus in a CRT plan.

Equations

• plan.modulus = plan.moduli.toList.prod

theorem Hex.Modular.CrtPlan.modulus_eq_prod (plan : CrtPlan) : plan.modulus = plan.moduli.toList.prod

theorem Hex.Modular.CrtPlan.modulus_pos (plan : CrtPlan) : 0 < plan.modulus

The root modulus of a validated plan is positive.

def Hex.Modular.CrtPlan.build? (moduli : Array Nat) : Option CrtPlan

Validate moduli and precompute a balanced product tree.

Equations

• Hex.Modular.CrtPlan.build? moduli = if h : Hex.Modular.CrtPlan.Valid moduli then some { moduli := moduli, tree := Hex.Modular.CrtPlan.Tree.ofList moduli.toList, valid := h } else none

theorem Hex.Modular.CrtPlan.build?_isSome (moduli : Array Nat) : (build? moduli).isSome = decide (Valid moduli)

Plan construction succeeds exactly for moduli greater than one that are pairwise coprime.

theorem Hex.Modular.CrtPlan.build?_moduli {moduli : Array Nat} {plan : CrtPlan} (h : build? moduli = some plan) : plan.moduli = moduli

A successful build records the requested modulus array unchanged.

def Hex.Modular.CrtPlan.reconstruct? (plan : CrtPlan) (residues : Array Int) : Option Int

Reconstruct one residue for every modulus. A count mismatch is rejected; the final linear congruence check makes the public result self-validating.

Equations

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

def Hex.Modular.CrtPlan.reconstructVec? {k : Nat} (plan : CrtPlan) (residues : Array (Vector Int k)) : Option (Vector Int k)

Reconstruct k lanes sharing one plan. Tree inverses are reused across every lane; reconstruction does not invoke extended GCD.

Equations

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

theorem Hex.Modular.CrtPlan.reconstruct?_eq_none_of_size_ne (plan : CrtPlan) (residues : Array Int) (h : residues.size ≠ plan.moduli.size) : plan.reconstruct? residues = none

Scalar reconstruction rejects a residue-count mismatch.

theorem Hex.Modular.CrtPlan.reconstructVec?_eq_none_of_size_ne {k : Nat} (plan : CrtPlan) (residues : Array (Vector Int k)) (h : residues.size ≠ plan.moduli.size) : plan.reconstructVec? residues = none

Vector reconstruction rejects a residue-count mismatch.

theorem Hex.Modular.CrtPlan.reconstruct?_congr {plan : CrtPlan} {residues : Array Int} {value : Int} (h : plan.reconstruct? residues = some value) : residues.size = plan.moduli.size ∧ ∀ (i : Fin plan.moduli.size), value % ↑plan.moduli[i] = residues.getD (↑i) 0 % ↑plan.moduli[i]

A successful scalar reconstruction is congruent to every input residue.

theorem Hex.Modular.CrtPlan.reconstructVec?_congr {k : Nat} {plan : CrtPlan} {residues : Array (Vector Int k)} {value : Vector Int k} (h : plan.reconstructVec? residues = some value) : residues.size = plan.moduli.size ∧ ∀ (i : Fin plan.moduli.size) (j : Fin k), value[j] % ↑plan.moduli[i] = (residues.getD (↑i) (Vector.replicate k 0))[j] % ↑plan.moduli[i]

Every lane of a successful vector reconstruction is congruent to its input residue at every modulus.

theorem Hex.Modular.CrtPlan.reconstruct?_le {plan : CrtPlan} {residues : Array Int} {value : Int} (h : plan.reconstruct? residues = some value) : 2 * value.natAbs ≤ plan.modulus

A scalar result lies in the symmetric interval of the root product.

theorem Hex.Modular.CrtPlan.reconstructVec?_le {k : Nat} {plan : CrtPlan} {residues : Array (Vector Int k)} {value : Vector Int k} (h : plan.reconstructVec? residues = some value) (j : Fin k) : 2 * value[j].natAbs ≤ plan.modulus

Every vector result lies in the symmetric interval of the root product.

theorem Hex.Modular.CrtPlan.emod_eq_modulus (plan : CrtPlan) {left right : Int} (h : ∀ (i : Fin plan.moduli.size), left % ↑plan.moduli[i] = right % ↑plan.moduli[i]) : left % ↑plan.modulus = right % ↑plan.modulus

Congruence at every leaf modulus implies congruence at the complete pairwise-coprime product recorded by the plan.

theorem Hex.Modular.CrtPlan.reconstruct?_symMod {plan : CrtPlan} {residues : Array Int} {value : Int} (h : plan.reconstruct? residues = some value) : symMod value plan.modulus = value

Every successful scalar reconstruction is already reduced to the symmetric interval of the complete modulus.

theorem Hex.Modular.CrtPlan.reconstructVec?_symMod {k : Nat} {plan : CrtPlan} {residues : Array (Vector Int k)} {value : Vector Int k} (h : plan.reconstructVec? residues = some value) (j : Fin k) : symMod value[j] plan.modulus = value[j]

Every lane of a successful vector reconstruction is already reduced to the symmetric interval of the complete modulus.

theorem Hex.Modular.CrtPlan.reconstruct?_eq_candidate {plan : CrtPlan} {residues : Array Int} {value candidate : Int} (hresult : plan.reconstruct? residues = some value) (hbound : 2 * candidate.natAbs < plan.modulus) (hcongr : ∀ (i : Fin plan.moduli.size), candidate % ↑plan.moduli[i] = residues.getD (↑i) 0 % ↑plan.moduli[i]) : value = candidate

Strictly half-bounded candidates that match every input residue are recovered exactly by scalar reconstruction.

theorem Hex.Modular.CrtPlan.reconstructVec?_eq_candidate {k : Nat} {plan : CrtPlan} {residues : Array (Vector Int k)} {value candidate : Vector Int k} (hresult : plan.reconstructVec? residues = some value) (hbound : ∀ (j : Fin k), 2 * candidate[j].natAbs < plan.modulus) (hcongr : ∀ (i : Fin plan.moduli.size) (j : Fin k), candidate[j] % ↑plan.moduli[i] = (residues.getD (↑i) (Vector.replicate k 0))[j] % ↑plan.moduli[i]) : value = candidate

Strictly half-bounded candidate lanes that match every input residue are recovered exactly by batch reconstruction.