inductive Hex.Matrix.DetWitness : Type

A kernel-checkable determinant certificate. See the module docstring.

• triangular (swaps : List (Nat × Nat)) (transform : List (List Int)) (value : Int) : DetWitness

  A triangularization: the row swaps in application order, the rows of the lower triangular transform (row i holds its i + 1 leading entries), and the value.

• singular (vec : List Int) : DetWitness

  A nonzero left kernel vector: the value is 0.

@[instance_reducible]

instance Hex.Matrix.instReprDetWitness : Repr DetWitness

Equations

• Hex.Matrix.instReprDetWitness = { reprPrec := Hex.Matrix.instReprDetWitness.repr }

def Hex.Matrix.instReprDetWitness.repr : DetWitness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.instInhabitedDetWitness : Inhabited DetWitness

Equations

• Hex.Matrix.instInhabitedDetWitness = { default := Hex.Matrix.instInhabitedDetWitness.default }

@[instance_reducible]

instance Hex.Matrix.instDecidableEqDetWitness : DecidableEq DetWitness

Equations

• Hex.Matrix.instDecidableEqDetWitness = Hex.Matrix.instDecidableEqDetWitness.decEq

def Hex.Matrix.instDecidableEqDetWitness.decEq (x✝ x✝¹ : DetWitness) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.instDecidableEqDetWitness.decEq (Hex.Matrix.DetWitness.triangular swaps transform value) (Hex.Matrix.DetWitness.singular vec) = isFalse ⋯
• Hex.Matrix.instDecidableEqDetWitness.decEq (Hex.Matrix.DetWitness.singular vec) (Hex.Matrix.DetWitness.triangular swaps transform value) = isFalse ⋯
• Hex.Matrix.instDecidableEqDetWitness.decEq (Hex.Matrix.DetWitness.singular a) (Hex.Matrix.DetWitness.singular b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Hex.Matrix.DetWitness.value : DetWitness → Int

The certified value.

Equations

• (Hex.Matrix.DetWitness.triangular swaps transform d).value = d
• (Hex.Matrix.DetWitness.singular vec).value = 0

def Hex.Matrix.DetWitness.nthRow : List (List Int) → Nat → List Int

Row i of a row list, [] past the end.

Equations

• Hex.Matrix.DetWitness.nthRow [] x✝ = []
• Hex.Matrix.DetWitness.nthRow (a :: tail) 0 = a
• Hex.Matrix.DetWitness.nthRow (head :: as) i.succ = Hex.Matrix.DetWitness.nthRow as i

def Hex.Matrix.DetWitness.nthInt : List Int → Nat → Int

Entry j of a row, 0 past the end.

Equations

• Hex.Matrix.DetWitness.nthInt [] x✝ = 0
• Hex.Matrix.DetWitness.nthInt (a :: tail) 0 = a
• Hex.Matrix.DetWitness.nthInt (head :: as) j.succ = Hex.Matrix.DetWitness.nthInt as j

def Hex.Matrix.DetWitness.replaceRow : List (List Int) → Nat → List Int → List (List Int)

Row i replaced by r; unchanged past the end.

Equations

• Hex.Matrix.DetWitness.replaceRow [] x✝¹ x✝ = []
• Hex.Matrix.DetWitness.replaceRow (head :: as) 0 x✝ = x✝ :: as
• Hex.Matrix.DetWitness.replaceRow (a :: as) i.succ x✝ = a :: Hex.Matrix.DetWitness.replaceRow as i x✝

def Hex.Matrix.DetWitness.swapRows (a b : Nat) (A : List (List Int)) : List (List Int)

Rows a and b exchanged.

Equations

• Hex.Matrix.DetWitness.swapRows a b A = Hex.Matrix.DetWitness.replaceRow (Hex.Matrix.DetWitness.replaceRow A a (Hex.Matrix.DetWitness.nthRow A b)) b (Hex.Matrix.DetWitness.nthRow A a)

def Hex.Matrix.DetWitness.applySwaps : List (Nat × Nat) → List (List Int) → List (List Int)

The swaps applied in order.

Equations

• Hex.Matrix.DetWitness.applySwaps [] x✝ = x✝
• Hex.Matrix.DetWitness.applySwaps ((a, b) :: s) x✝ = Hex.Matrix.DetWitness.applySwaps s (Hex.Matrix.DetWitness.swapRows a b x✝)

def Hex.Matrix.DetWitness.swapsOk (n : Nat) : List (Nat × Nat) → Bool

Every swap exchanges two distinct rows below n.

Equations

• Hex.Matrix.DetWitness.swapsOk n [] = true
• Hex.Matrix.DetWitness.swapsOk n ((a, b) :: s) = (a.blt n && b.blt n && !a.beq b && Hex.Matrix.DetWitness.swapsOk n s)

def Hex.Matrix.DetWitness.signOf : List (Nat × Nat) → Int

The sign of the arrangement: (-1)^(number of swaps).

Equations

• Hex.Matrix.DetWitness.signOf [] = 1
• Hex.Matrix.DetWitness.signOf (head :: s) = (Hex.Matrix.DetWitness.signOf s).neg

def Hex.Matrix.DetWitness.rowsLen (m : Nat) : List (List Int) → Bool

Every row has length m.

Equations

• Hex.Matrix.DetWitness.rowsLen m [] = true
• Hex.Matrix.DetWitness.rowsLen m (r :: rs) = (r.length.beq m && Hex.Matrix.DetWitness.rowsLen m rs)

def Hex.Matrix.DetWitness.dotInt : List Int → List Int → Int

The dot product of two integer lists, stopping at the shorter.

Equations

• Hex.Matrix.DetWitness.dotInt (a :: as) (b :: bs) = (a.mul b).add (Hex.Matrix.DetWitness.dotInt as bs)
• Hex.Matrix.DetWitness.dotInt x✝¹ x✝ = 0

def Hex.Matrix.DetWitness.column (j : Nat) : List (List Int) → List Int

Column j of a row list.

Equations

• Hex.Matrix.DetWitness.column j [] = []
• Hex.Matrix.DetWitness.column j (r :: rs) = Hex.Matrix.DetWitness.nthInt r j :: Hex.Matrix.DetWitness.column j rs

def Hex.Matrix.DetWitness.columnsFrom (A : List (List Int)) (j : Nat) : Nat → List (List Int)

Columns j, …, j + k - 1 of a row list.

Equations

• Hex.Matrix.DetWitness.columnsFrom A j 0 = []
• Hex.Matrix.DetWitness.columnsFrom A j k.succ = Hex.Matrix.DetWitness.column j A :: Hex.Matrix.DetWitness.columnsFrom A (j + 1) k

def Hex.Matrix.DetWitness.columns (m : Nat) (A : List (List Int)) : List (List Int)

The m columns of a row list.

Equations

• Hex.Matrix.DetWitness.columns m A = Hex.Matrix.DetWitness.columnsFrom A 0 m

def Hex.Matrix.DetWitness.zeroDots (t : List Int) : List (List Int) → Bool

The row is orthogonal to every column in the list.

Equations

• Hex.Matrix.DetWitness.zeroDots t [] = true
• Hex.Matrix.DetWitness.zeroDots t (r :: rs) = (decide (Hex.Matrix.DetWitness.dotInt t r = 0) && Hex.Matrix.DetWitness.zeroDots t rs)

def Hex.Matrix.DetWitness.anyNonzero : List Int → Bool

Some entry is nonzero.

Equations

• Hex.Matrix.DetWitness.anyNonzero [] = false
• Hex.Matrix.DetWitness.anyNonzero (a :: as) = (!decide (a = 0) || Hex.Matrix.DetWitness.anyNonzero as)

def Hex.Matrix.DetWitness.triangularCheck (d : Int) : List (List Int) → Nat → List (List Int) → List (List Int) → Int → Int → Bool

Walk the transform rows against the columns of the arranged matrix. Row i (with done the i columns already passed, in any order) must have length i + 1, a nonzero last entry lᵢ, and zero products with the earlier columns; its product with column i is the diagonal entry uᵢ of the triangular product. pl and pu accumulate ∏ lᵢ and sign · ∏ uᵢ, and at the end pl · d = pu is required.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.DetWitness.triangularCheck d x✝³ x✝² [] [] x✝¹ x✝ = decide (x✝¹.mul d = x✝)
• Hex.Matrix.DetWitness.triangularCheck d x✝⁵ x✝⁴ x✝³ x✝² x✝¹ x✝ = false

def Hex.Matrix.DetWitness.scaledRow (k : Nat) : List Rat → List Int → Bool

k • q = b entrywise.

Equations

• Hex.Matrix.DetWitness.scaledRow k [] [] = true
• Hex.Matrix.DetWitness.scaledRow k (q :: qs) (b :: bs) = (decide ((Rat.ofInt (Int.ofNat k)).mul q = Rat.ofInt b) && Hex.Matrix.DetWitness.scaledRow k qs bs)
• Hex.Matrix.DetWitness.scaledRow k x✝¹ x✝ = false

def Hex.Matrix.DetWitness.scaledRows : List Nat → List (List Rat) → List (List Int) → Bool

Every row of A scaled by its positive scale is the row of B.

Equations

• Hex.Matrix.DetWitness.scaledRows [] [] [] = true
• Hex.Matrix.DetWitness.scaledRows (k :: ks) (q :: qs) (b :: bs) = (Nat.blt 0 k && Hex.Matrix.DetWitness.scaledRow k q b && Hex.Matrix.DetWitness.scaledRows ks qs bs)
• Hex.Matrix.DetWitness.scaledRows x✝² x✝¹ x✝ = false

def Hex.Matrix.DetWitness.prodNat : List Nat → Nat

The product of the scales.

Equations

• Hex.Matrix.DetWitness.prodNat [] = 1
• Hex.Matrix.DetWitness.prodNat (k :: ks) = k.mul (Hex.Matrix.DetWitness.prodNat ks)

def Hex.Matrix.checkDetList (n : Nat) (A : List (List Int)) : DetWitness → Bool

The kernel checker. A is the matrix as a list of n rows of length n. Checks the shape, and then either the triangularization or the left kernel vector; see the module docstring.

Equations

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

def Hex.Matrix.checkDetRat (n : Nat) (A : List (List Rat)) (s : List Nat) (B : List (List Int)) (c : DetWitness) (v : Rat) : Bool

The kernel checker for a rational matrix A given as n rows: the scales s take the rows of A to the rows of the integer matrix B, which c certifies, and the value v satisfies v · ∏ s = value c.

Equations

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

def Hex.Matrix.rowLists {n : Nat} (A : Matrix Int n n) : List (List Int)

The rows of a square matrix as lists.

Equations

• A.rowLists = List.map (fun (x : Vector Int n) => x.toList) A.rows.toList

def Hex.Matrix.detWitnessOfLists (n : Nat) (A : List (List Int)) : Except String DetWitness

The kernel witness of a square integer matrix given as n rows of length n, by fraction-free elimination on [A | I], or the reason its own check fails.

Equations

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

def Hex.Matrix.detWitness {n : Nat} (A : Matrix Int n n) : Except String DetWitness

The kernel witness of a square integer matrix.

Equations

• A.detWitness = Hex.Matrix.detWitnessOfLists n A.rowLists