inductive Hex.Modular.CrtTrace {k : Nat} (image : Nat → Option (Vector Int k)) (supply : Array Nat) : Nat → CrtVec k → Prop

Reachability through an exact prefix of the modulus supply. Rejected images and failed CRT pushes advance the prefix without changing the state; successful pushes retain the equality consumed by the CRT congruence lemmas.

• init {k : Nat} {image : Nat → Option (Vector Int k)} {supply : Array Nat} : CrtTrace image supply 0 (CrtVec.init k)
• skip {k : Nat} {image : Nat → Option (Vector Int k)} {supply : Array Nat} {index : Nat} {state : CrtVec k} (trace : CrtTrace image supply index state) (hi : index < supply.size) (himage : image supply[index] = none) : CrtTrace image supply (index + 1) state
• reject {k : Nat} {image : Nat → Option (Vector Int k)} {supply : Array Nat} {index : Nat} {state : CrtVec k} (trace : CrtTrace image supply index state) (hi : index < supply.size) {residues : Vector Int k} (himage : image supply[index] = some residues) (hpush : state.push residues supply[index] = none) : CrtTrace image supply (index + 1) state
• push {k : Nat} {image : Nat → Option (Vector Int k)} {supply : Array Nat} {index : Nat} {state next : CrtVec k} (trace : CrtTrace image supply index state) (hi : index < supply.size) {residues : Vector Int k} (himage : image supply[index] = some residues) (hpush : state.push residues supply[index] = some next) : CrtTrace image supply (index + 1) next

theorem Hex.Modular.CrtTrace.le_size {k : Nat} {image : Nat → Option (Vector Int k)} {supply : Array Nat} {consumed : Nat} {state : CrtVec k} (trace : CrtTrace image supply consumed state) : consumed ≤ supply.size

A traced state has consumed no more than the available supply.

theorem Hex.Modular.CrtTrace.congr {k : Nat} {image : Nat → Option (Vector Int k)} {supply : Array Nat} {consumed : Nat} {state : CrtVec k} (trace : CrtTrace image supply consumed state) (x : Vector Int k) (himage : ∀ (j : Nat) (hj : j < supply.size), j < consumed → ∀ (r : Vector Int k), image supply[j] = some r → ∀ (i : Fin k), r[i] % ↑supply[j] = x[i] % ↑supply[j]) (i : Fin k) : state.value[i] % ↑state.modulus = x[i] % ↑state.modulus

A traced state agrees modulo its accumulated modulus with every vector whose coordinates agree with all successful images in the consumed prefix.

def Hex.Modular.crtLoop {k : Nat} {α : Type u_1} (image : Nat → Option (Vector Int k)) (accept : 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.

Equations

• Hex.Modular.crtLoop image accept supply fuel = Hex.Modular.crtLoop.go✝ image accept supply fuel 0 (Hex.Modular.CrtVec.init k)

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