inductive Hex.Matrix.DetWitness (R : Type := Int) : Type

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

• triangular {R : optParam Type Int} (swaps : List (Nat × Nat)) (transform : List (List R)) (value : R) : DetWitness R

  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 {R : optParam Type Int} (vec : List R) : DetWitness R

  A nonzero left kernel vector: the value is 0.

def Hex.Matrix.instReprDetWitness.repr {R✝ : Type} [Repr R✝] : DetWitness R✝ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.instReprDetWitness {R✝ : Type} [Repr R✝] : Repr (DetWitness R✝)

Equations

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

@[instance_reducible]

instance Hex.Matrix.instInhabitedDetWitness {a✝ : Type} : Inhabited (DetWitness a✝)

Equations

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

@[instance_reducible]

instance Hex.Matrix.instDecidableEqDetWitness {R✝ : Type} [DecidableEq R✝] : DecidableEq (DetWitness R✝)

Equations

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

def Hex.Matrix.instDecidableEqDetWitness.decEq {R✝ : Type} [DecidableEq R✝] (x✝ x✝¹ : DetWitness R✝) : 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 {R : Type} [Zero R] : DetWitness R → R

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.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.Packed.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.zeroDotsPacked (W r : Nat) (t : Nat × Nat) : List (Nat × Nat) → Bool

zeroDots on packed pairs.

Equations

• Hex.Matrix.DetWitness.zeroDotsPacked W r t [] = true
• Hex.Matrix.DetWitness.zeroDotsPacked W r t (head :: s) = (decide (Hex.Matrix.Packed.dotIntPacked W r t head = 0) && Hex.Matrix.DetWitness.zeroDotsPacked W r t s)

def Hex.Matrix.DetWitness.triangularCheckPacked (W r : Nat) (d : Int) : List (Nat × Nat) → Nat → List (List Int) → List (Nat × Nat) → List (Nat × Nat) → Int → Int → Bool

triangularCheck with the dot products on packed pairs: tps the packed rows of the transform alongside its rows ts, done and cs the packed columns.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.DetWitness.triangularCheckPacked W r d x✝³ x✝² [] [] [] x✝¹ x✝ = decide (x✝¹.mul d = x✝)
• Hex.Matrix.DetWitness.triangularCheckPacked W r d x✝⁶ 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.checkDetListPacked (W k n : Nat) (A : List (List Int)) : DetWitness → Bool

The kernel checker with the triangularization on packed rows, slot width W and entry bound k: checkDetList with triangularCheck replaced by triangularCheckPacked, plus the bounds that make the packed dot products exact: every entry of the matrix and of the transform below k in absolute value, k > 0, and n · k² < 2^W. The singular branch is unchanged. A passing packed check implies a passing checkDetList; see the companion's checkDetList_of_packed.

Equations

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

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

checkDetRat with the packed integer check.

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.

structure Hex.Matrix.DetWitness.Budget : Type

Independent limits on current elimination blocks and the emitted witness.

• maxIntermediate : Nat
• maxCertificate : Nat

def Hex.Matrix.DetWitness.instReprBudget.repr : Budget → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.DetWitness.instReprBudget : Repr Budget

Equations

• Hex.Matrix.DetWitness.instReprBudget = { reprPrec := Hex.Matrix.DetWitness.instReprBudget.repr }

@[instance_reducible]

instance Hex.Matrix.DetWitness.instBEqBudget : BEq Budget

Equations

• Hex.Matrix.DetWitness.instBEqBudget = { beq := Hex.Matrix.DetWitness.instBEqBudget.beq }

def Hex.Matrix.DetWitness.instBEqBudget.beq : Budget → Budget → Bool

Equations

• Hex.Matrix.DetWitness.instBEqBudget.beq { maxIntermediate := a, maxCertificate := a_1 } { maxIntermediate := b, maxCertificate := b_1 } = (a == b && a_1 == b_1)
• Hex.Matrix.DetWitness.instBEqBudget.beq x✝¹ x✝ = false

inductive Hex.Matrix.DetWitness.Limit : Type

• intermediate : Limit
• certificate : Limit

def Hex.Matrix.DetWitness.instReprLimit.repr : Limit → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.DetWitness.instReprLimit : Repr Limit

Equations

• Hex.Matrix.DetWitness.instReprLimit = { reprPrec := Hex.Matrix.DetWitness.instReprLimit.repr }

@[instance_reducible]

instance Hex.Matrix.DetWitness.instBEqLimit : BEq Limit

Equations

• Hex.Matrix.DetWitness.instBEqLimit = { beq := Hex.Matrix.DetWitness.instBEqLimit.beq }

def Hex.Matrix.DetWitness.instBEqLimit.beq : Limit → Limit → Bool

Equations

• Hex.Matrix.DetWitness.instBEqLimit.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Hex.Matrix.DetWitness.Error : Type

Resource declines remain distinct from malformed input or a rejected witness.

• exhausted (budget : Limit) (count limit : Nat) : Error
• malformed (dimension : Nat) : Error
• rejected : Error

def Hex.Matrix.DetWitness.instReprError.repr : Error → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.DetWitness.instReprError : Repr Error

Equations

• Hex.Matrix.DetWitness.instReprError = { reprPrec := Hex.Matrix.DetWitness.instReprError.repr }

@[instance_reducible]

instance Hex.Matrix.DetWitness.instBEqError : BEq Error

Equations

• Hex.Matrix.DetWitness.instBEqError = { beq := Hex.Matrix.DetWitness.instBEqError.beq }

def Hex.Matrix.DetWitness.instBEqError.beq : Error → Error → Bool

Equations

• Hex.Matrix.DetWitness.instBEqError.beq (Hex.Matrix.DetWitness.Error.exhausted a a_1 a_2) (Hex.Matrix.DetWitness.Error.exhausted b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• Hex.Matrix.DetWitness.instBEqError.beq (Hex.Matrix.DetWitness.Error.malformed a) (Hex.Matrix.DetWitness.Error.malformed b) = (a == b)
• Hex.Matrix.DetWitness.instBEqError.beq Hex.Matrix.DetWitness.Error.rejected Hex.Matrix.DetWitness.Error.rejected = true
• Hex.Matrix.DetWitness.instBEqError.beq x✝¹ x✝ = false

def Hex.Matrix.DetWitness.Error.message : Error → String

Equations

• One or more equations did not get rendered due to their size.
• (Hex.Matrix.DetWitness.Error.malformed a).message = toString "the matrix is not " ++ toString a ++ toString " × " ++ toString a
• Hex.Matrix.DetWitness.Error.rejected.message = "the witness fails its own check"

def Hex.Matrix.DetWitness.measure {R : Type} (size : R → Nat) : DetWitness R → Nat

Total serialized support, including the value in the triangular case.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.DetWitness.measure size (Hex.Matrix.DetWitness.singular a) = List.foldl (fun (total : Nat) (x : R) => total + size x) 0 a

def Hex.Matrix.detWitnessBudgeted {R : Type} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [Inhabited R] [DecidableEq R] (quot : R → R → R) (n : Nat) (size : R → Nat) (budget : DetWitness.Budget) (check : List (List R) → DetWitness R → Bool) (A : List (List R)) : Except DetWitness.Error (DetWitness R)

Fraction-free production with operand admission, block support and witness limits. The final self-check runs only after the witness fits its budget.

Equations

• Hex.Matrix.detWitnessBudgeted quot n size budget check A = Hex.Matrix.DetWitness.validate✝ (check A) (Hex.Matrix.DetWitness.produce✝ quot n size (some budget) A)

theorem Hex.Matrix.detWitnessBudgeted_check {R : Type} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [Inhabited R] [DecidableEq R] (quot : R → R → R) (n : Nat) (size : R → Nat) (budget : DetWitness.Budget) (check : List (List R) → DetWitness R → Bool) (A : List (List R)) (w : DetWitness R) (h : detWitnessBudgeted quot n size budget check A = Except.ok w) : check A w = true

def Hex.Matrix.detWitnessWith {R : Type} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [Inhabited R] [DecidableEq R] (quot : R → R → R) (n : Nat) (check : List (List R) → DetWitness R → Bool) (A : List (List R)) : Except String (DetWitness R)

The unlimited instance of the same producer, retaining the integer API.

Equations

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

theorem Hex.Matrix.detWitnessWith_check {R : Type} [Zero R] [One R] [Neg R] [Sub R] [Mul R] [Inhabited R] [DecidableEq R] (quot : R → R → R) (n : Nat) (check : List (List R) → DetWitness R → Bool) (A : List (List R)) (w : DetWitness R) (h : detWitnessWith quot n check A = Except.ok w) : check A w = true

Every successful producer return has passed its supplied checker. This does not assume the quotient implementation is correct: a rejected witness is returned as an error.

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

The integer instance of the generic witness producer.

Equations

• Hex.Matrix.detWitnessOfLists n A = Hex.Matrix.detWitnessWith HexArith.Int.exactDiv n (Hex.Matrix.checkDetList n) A

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