structure 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.

• r : Int

  The current Euclidean remainder.

• t : Int

  The coefficient of the second input a.

def Hex.Modular.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

• Hex.Modular.instDecidableEqRow.decEq { r := a, t := a_1 } { r := b, t := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.Modular.instDecidableEqRow : DecidableEq Row

Equations

• Hex.Modular.instDecidableEqRow = Hex.Modular.instDecidableEqRow.decEq

def Hex.Modular.euclidUntil (m a P : Int) : 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.

Equations

• Hex.Modular.euclidUntil m a P = if _hm : m.natAbs = 0 then { r := 0, t := 0 } else have residue := (a % Int.ofNat m.natAbs).natAbs; Hex.Modular.euclidUntil.go✝ P m.natAbs residue 0 1

theorem Hex.Modular.euclidUntil_spec {modulus : Nat} {a P : Int} (hmodulus : 0 < modulus) (hP : 0 ≤ P) (hcut : P < ↑modulus) : have row := euclidUntil (Int.ofNat modulus) a P; 0 ≤ row.r ∧ row.r ≤ P ∧ row.t ≠ 0 ∧ ↑modulus ∣ row.t * a - row.r ∧ ∀ (p q : Int), ↑p.natAbs ≤ P → 0 < q → ↑modulus ∣ q * a - p → ↑row.t.natAbs ≤ q

The truncated Euclidean row is a nonzero modular-lattice vector whose second coordinate is no larger than that of any bounded lattice vector.