def Hex.Matrix.FieldLists.matrix (n m : Nat) (a : Lists.ScaledRows) : Bool

A positive scale and an exact rectangular block.

Equations

• Hex.Matrix.FieldLists.matrix n m a = (Nat.blt 0 a.denom && Hex.Matrix.Lists.shape n m a.nums)

def Hex.Matrix.FieldLists.vector (n : Nat) (a : Lists.Scaled) : Bool

A positive scale and an exact vector length.

Equations

• Hex.Matrix.FieldLists.vector n a = (Nat.blt 0 a.denom && a.nums.length.beq n)

def Hex.Matrix.FieldLists.product (n m : Nat) (a b c : Lists.ScaledRows) : Bool

Matrix multiplication with denominators cleared once per identity.

Equations

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

def Hex.Matrix.FieldLists.inverse (n : Nat) (a b : Lists.ScaledRows) : Bool

Inverse products need only the scaled identity, without materializing it.

Equations

• Hex.Matrix.FieldLists.inverse n a b = Hex.Matrix.Lists.product n n a.nums b.nums fun (i j : Nat) => (Int.ofNat (a.denom.mul b.denom)).mul (Hex.Matrix.Lists.identity i j)

def Hex.Matrix.FieldLists.columnBlock (a : Lists.Scaled) : Lists.ScaledRows

A vector represented as a single-column block.

Equations

• Hex.Matrix.FieldLists.columnBlock a = { denom := a.denom, nums := List.map (fun (z : Int) => [z]) a.nums }

def Hex.Matrix.FieldLists.rowBlock (a : Lists.Scaled) : Lists.ScaledRows

A vector represented as a single-row block.

Equations

• Hex.Matrix.FieldLists.rowBlock a = { denom := a.denom, nums := [a.nums] }

def Hex.Matrix.FieldLists.kernel (n : Nat) (a : Lists.ScaledRows) (v : Lists.Scaled) : Bool

Zero right product.

Equations

• Hex.Matrix.FieldLists.kernel n a v = Hex.Matrix.Lists.all (fun (i : Nat) => decide (Hex.Matrix.Lists.dot (Hex.Matrix.Lists.entry [] a.nums i) v.nums = 0)) n

def Hex.Matrix.FieldLists.separator (m : Nat) (a : Lists.ScaledRows) (b y : Lists.Scaled) : Bool

Zero left product and nonzero pairing with the right-hand side.

Equations

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

def Hex.Matrix.FieldLists.denominator (qs : List Rat) : Nat

Structural common denominator, without GCD or well-founded recursion.

Equations

• Hex.Matrix.FieldLists.denominator qs = List.foldl (fun (d : Nat) (q : Rat) => if (d.mod q.den).beq 0 = true then d else d.mul q.den) 1 qs

def Hex.Matrix.FieldLists.encode (qs : List Rat) : Lists.Scaled

A direct residual check chooses its scale by a structural list fold.

Equations

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

def Hex.Matrix.FieldLists.encodeRows (rows : List (List Rat)) : Lists.ScaledRows

Encode a matrix with the same structural scale fold as a direct residual check.

Equations

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

inductive Hex.Matrix.InverseWitness : Type

An arbitrary inverse or nonzero right-kernel witness.

• invertible (input value : Lists.ScaledRows) : InverseWitness
• singular (input : Lists.ScaledRows) (kernel : Lists.Scaled) (index : Nat) : InverseWitness

@[instance_reducible]

instance Hex.Matrix.instReprInverseWitness : Repr InverseWitness

Equations

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

def Hex.Matrix.instReprInverseWitness.repr : InverseWitness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.instInhabitedInverseWitness : Inhabited InverseWitness

Equations

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

def Hex.Matrix.instDecidableEqInverseWitness.decEq (x✝ x✝¹ : InverseWitness) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.instDecidableEqInverseWitness.decEq (Hex.Matrix.InverseWitness.invertible input value) (Hex.Matrix.InverseWitness.singular input_1 kernel index) = isFalse ⋯
• Hex.Matrix.instDecidableEqInverseWitness.decEq (Hex.Matrix.InverseWitness.singular input kernel index) (Hex.Matrix.InverseWitness.invertible input_1 value) = isFalse ⋯

@[instance_reducible]

instance Hex.Matrix.instDecidableEqInverseWitness : DecidableEq InverseWitness

Equations

• Hex.Matrix.instDecidableEqInverseWitness = Hex.Matrix.instDecidableEqInverseWitness.decEq

def Hex.Matrix.checkInverseList (n : Nat) (rows : List (List Rat)) (c : InverseWitness) : Bool

Check either mathematical outcome independently of row reduction.

Equations

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

structure Hex.Matrix.SolveBasis : Type

The list data needed to reconstruct a complete reduced-row-echelon witness.

• reduced : Lists.ScaledRows
• transform : Lists.ScaledRows
• inverse : Lists.ScaledRows
• rank : Nat
• pivots : List Nat
• free : List Nat
• value : Lists.Scaled
• nullity : Nat
• basis : Lists.ScaledRows

def Hex.Matrix.instReprSolveBasis.repr : SolveBasis → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.instReprSolveBasis : Repr SolveBasis

Equations

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

@[instance_reducible]

instance Hex.Matrix.instInhabitedSolveBasis : Inhabited SolveBasis

Equations

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

def Hex.Matrix.instDecidableEqSolveBasis.decEq (x✝ x✝¹ : SolveBasis) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hex.Matrix.instDecidableEqSolveBasis : DecidableEq SolveBasis

Equations

• Hex.Matrix.instDecidableEqSolveBasis = Hex.Matrix.instDecidableEqSolveBasis.decEq

inductive Hex.Matrix.SolveWitness : Type

Complete affine data or a separating row.

• consistent (input : Lists.ScaledRows) (rhs : Lists.Scaled) (data : SolveBasis) : SolveWitness
• inconsistent (input : Lists.ScaledRows) (rhs separator : Lists.Scaled) : SolveWitness

@[instance_reducible]

instance Hex.Matrix.instReprSolveWitness : Repr SolveWitness

Equations

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

def Hex.Matrix.instReprSolveWitness.repr : SolveWitness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.Matrix.instInhabitedSolveWitness : Inhabited SolveWitness

Equations

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

@[instance_reducible]

instance Hex.Matrix.instDecidableEqSolveWitness : DecidableEq SolveWitness

Equations

• Hex.Matrix.instDecidableEqSolveWitness = Hex.Matrix.instDecidableEqSolveWitness.decEq

def Hex.Matrix.instDecidableEqSolveWitness.decEq (x✝ x✝¹ : SolveWitness) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.instDecidableEqSolveWitness.decEq (Hex.Matrix.SolveWitness.consistent input rhs data) (Hex.Matrix.SolveWitness.inconsistent input_1 rhs_1 separator) = isFalse ⋯
• Hex.Matrix.instDecidableEqSolveWitness.decEq (Hex.Matrix.SolveWitness.inconsistent input rhs separator) (Hex.Matrix.SolveWitness.consistent input_1 rhs_1 data) = isFalse ⋯

def Hex.Matrix.FieldLists.echelon (n m : Nat) (d : SolveBasis) : Bool

A sorted in-range pivot list and the full reduced-row-echelon clauses.

Equations

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

def Hex.Matrix.FieldLists.freeData (m : Nat) (d : SolveBasis) : Bool

Free columns in increasing order, canonical particular solution and basis.

Equations

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

def Hex.Matrix.checkSolveList (n m : Nat) (rows : List (List Rat)) (rhs : List Rat) (c : SolveWitness) : Bool

Validate the entire affine space or the inconsistency witness.

Equations

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

def Hex.Matrix.checkSolutionList (n m : Nat) (rows : List (List Rat)) (rhs candidate : List Rat) : Bool

Check any supplied solution, with no canonical-solution restriction.

Equations

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