theorem HexMatrixTheory.getD_eq_getElem' {α : Type u_1} (l : List α) (i : ℕ) (d : α) (h : i < l.length) : l.getD i d = l[i]

theorem HexMatrixTheory.getD_eq_default' {α : Type u_1} (l : List α) (i : ℕ) (d : α) (h : l.length ≤ i) : l.getD i d = d

def HexMatrixTheory.vecOfList {α : Type u_1} [Zero α] (k : ℕ) : List α → Fin k → α

A list as a vector, padded with zeros; vecOfList (k + 1) (a :: l) unfolds to vecCons a (vecOfList k l), so a ![…] literal is definitionally vecOfList of its entries.

Equations

• HexMatrixTheory.vecOfList 0 x✝ = ![]
• HexMatrixTheory.vecOfList k.succ (a :: l) = Matrix.vecCons a (HexMatrixTheory.vecOfList k l)
• HexMatrixTheory.vecOfList n.succ [] = fun (x : Fin (n + 1)) => 0

def HexMatrixTheory.ofLists {α : Type u_1} [Zero α] (n m : ℕ) (L : List (List α)) : Matrix (Fin n) (Fin m) α

The Mathlib matrix of a row list, padded with zeros.

Equations

• HexMatrixTheory.ofLists n m L = Matrix.of (HexMatrixTheory.vecOfList n (List.map (HexMatrixTheory.vecOfList m) L))

theorem HexMatrixTheory.vecOfList_apply {α : Type u_1} [Zero α] (k : ℕ) (l : List α) (i : Fin k) : vecOfList k l i = l.getD (↑i) 0

theorem HexMatrixTheory.ofLists_apply {α : Type u_1} [Zero α] (n m : ℕ) (L : List (List α)) (i : Fin n) (j : Fin m) : ofLists n m L i j = (L.getD ↑i []).getD (↑j) 0

def HexMatrixTheory.entriesEq {α : Type u_1} [Zero α] [DecidableEq α] (n m : ℕ) (A : Matrix (Fin n) (Fin m) α) (L : List (List α)) : Bool

The entrywise comparison of a matrix with its row list, as a Boolean the kernel evaluates by enumerating every index pair.

Equations

• HexMatrixTheory.entriesEq n m A L = (List.finRange n).all fun (i : Fin n) => (List.finRange m).all fun (j : Fin m) => decide (A i j = HexMatrixTheory.ofLists n m L i j)

theorem HexMatrixTheory.eq_ofLists_of_entriesEq {α : Type u_1} [Zero α] [DecidableEq α] (n m : ℕ) (A : Matrix (Fin n) (Fin m) α) (L : List (List α)) (h : entriesEq n m A L = true) : A = ofLists n m L

A passing entrywise comparison identifies the matrix with its row list.

def HexMatrixTheory.vectorEntriesEq {α : Type u_1} [Zero α] [DecidableEq α] (n : ℕ) (v : Fin n → α) (xs : List α) : Bool

Compare a closed vector with the list used by a certificate.

Equations

• HexMatrixTheory.vectorEntriesEq n v xs = (List.finRange n).all fun (i : Fin n) => decide (v i = HexMatrixTheory.vecOfList n xs i)

theorem HexMatrixTheory.eq_vecOfList_of_entriesEq {α : Type u_1} [Zero α] [DecidableEq α] (n : ℕ) (v : Fin n → α) (xs : List α) (h : vectorEntriesEq n v xs = true) : v = vecOfList n xs

The entrywise identification route for closed vector functions.

structure HexMatrixTheory.Certified {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : Type u_2

The record returned by the result-producing term forms (det% A): the value of f a and the proof.

• value : β

  The computed value.

• proof : f a = self.value

  The certificate that it is f a.

structure HexMatrixTheory.KernelConfig : Type

Configuration shared by the matrix tactics rank and det, in the style of decide +kernel: rank -packing, det -packing.

• packing : Bool

  Evaluate the certificate's dot products on Kronecker-packed rows (one multiplication, shift and mask per dot product in the kernel) instead of term by term. The certificate is the same; the packed checker is proven equal to the plain one under a bound the kernel verifies.

def HexMatrixTheory.Literal.elabKernelConfig (cfg : Lean.Syntax) (init : KernelConfig := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM KernelConfig

Elaborate the optConfig of a matrix tactic into a KernelConfig.

Equations

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

def HexMatrixTheory.Literal.integerBits (z : ℤ) : ℕ

Bit length of a signed certificate scalar, excluding its sign.

Equations

• HexMatrixTheory.Literal.integerBits z = if (z == 0) = true then 0 else z.natAbs.log2 + 1

def HexMatrixTheory.Literal.reportCertificate (tactic serialized : String) (integers : List ℤ) (denominators : List ℕ := []) (extra : List (String × Lean.Json) := []) : Lean.MetaM Unit

Optional certificate measurements for the external proof-probe runner. No clock is read here; kernel time comes from Lean's external profiler.

Equations

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

inductive HexMatrixTheory.Literal.Route : Type

How a recognized literal is identified with its row list.

• chain : Route

  A Matrix.of vector chain (!![…], Matrix.of ![…]): A = ofLists n m L is rfl.

• entrywise : Route

  A fun i j => … or Matrix.ofArray xs h literal: A = ofLists n m L by one kernel decide on entriesEq.

@[instance_reducible]

instance HexMatrixTheory.Literal.instReprRoute : Repr Route

Equations

• HexMatrixTheory.Literal.instReprRoute = { reprPrec := HexMatrixTheory.Literal.instReprRoute.repr }

def HexMatrixTheory.Literal.instReprRoute.repr : Route → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HexMatrixTheory.Literal.instDecidableEqRoute : DecidableEq Route

Equations

• HexMatrixTheory.Literal.instDecidableEqRoute x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure HexMatrixTheory.Literal.Recognized : Type

A recognized closed matrix literal.

• n : ℕ

  Rows.

• m : ℕ

  Columns.

• carrier : Lean.Expr

  The entry carrier.

• entries : Array (Array Lean.Expr)

  The entry expressions, row-major, as they appear in the literal (or, for the fun and ofArray forms, as instantiated at each index pair).

• route : Route

  The identification route.

def HexMatrixTheory.Literal.unfoldBudget : ℕ

How many definitions are unfolded when looking for a literal.

Equations

• HexMatrixTheory.Literal.unfoldBudget = 8

def HexMatrixTheory.Literal.shape? (ty : Lean.Expr) : Lean.MetaM (Option (ℕ × ℕ × Lean.Expr))

The shape of the type Matrix (Fin n) (Fin m) R with closed dimensions: (n, m, R), or of the function type Fin n → Fin m → R a bare lambda has. The dimensions may be any closed expressions that evaluate to numerals, as Matrix.of ![…] elaborates them as Nat.succ chains.

Equations

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

def HexMatrixTheory.Literal.matchChain? (n m : ℕ) (A : Lean.Expr) : Lean.MetaM (Option (Array (Array Lean.Expr)))

Match a Matrix.of ![…] chain (the !![…] notation included) of the given shape. Like Mathlib's matchMatrixLit?, but every vecCons chain must end in vecEmpty, so that the literal is definitionally the ofLists of its entries.

Equations

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

def HexMatrixTheory.Literal.finLit (n k : ℕ) : Lean.MetaM Lean.Expr

⟨k, _⟩ : Fin n.

Equations

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

def HexMatrixTheory.Literal.matchFn? (n m : ℕ) (A : Lean.Expr) : Lean.MetaM (Option (Array (Array Lean.Expr)))

Match a fun i j => … literal: the body instantiated at every index pair.

Equations

• One or more equations did not get rendered due to their size.
• HexMatrixTheory.Literal.matchFn? n m A = pure none

def HexMatrixTheory.Literal.matchOfArray? (n m : ℕ) (A : Lean.Expr) : Lean.MetaM (Option (Array (Array Lean.Expr)))

Match a Matrix.ofArray xs h literal whose array reduces to n * m entries.

Equations

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

partial def HexMatrixTheory.Literal.matchLiteral? (n m : ℕ) (R A : Lean.Expr) (budget : ℕ := unfoldBudget) (allowOpen : Bool := false) : Lean.MetaM (Option Recognized)

Find the literal behind A : Matrix (Fin n) (Fin m) R, unfolding definitions within unfoldBudget. Symbolic consumers may enable open entries.

def HexMatrixTheory.Literal.literal? (A : Lean.Expr) (allowOpen : Bool := false) : Lean.MetaM (Option Recognized)

Recognize a matrix literal, requiring closed entries unless explicitly enabled.

Equations

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

def HexMatrixTheory.Literal.evalEntry (e : Lean.Expr) : Lean.MetaM ℚ

Evaluate an entry to a rational with norm_num; an entry norm_num alone does not evaluate (the fun i j => … form instantiates its body at Fin literals, leaving Fin.val, casts and if i = j tests) is first simplified with the default simp set. An entry that is not a closed numeric expression is an error naming it.

Equations

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

def HexMatrixTheory.Literal.evalEntries (lit : Recognized) : Lean.MetaM (Array (Array ℚ))

Evaluate every entry to a rational.

Equations

• HexMatrixTheory.Literal.evalEntries lit = Array.mapM (fun (x : Array Lean.Expr) => Array.mapM HexMatrixTheory.Literal.evalEntry x) lit.entries

def HexMatrixTheory.Literal.rowList (type : Lean.Expr) (rows : Array (Array Lean.Expr)) : Lean.MetaM Lean.Expr

The row list of quoted entries, as a List (List type).

Equations

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

def HexMatrixTheory.Literal.decideProof (prop : Lean.Expr) : Lean.MetaM Lean.Expr

of_decide_eq_true on a closed decidable proposition, for the kernel to evaluate; no elaborator-side evaluation happens.

Equations

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

def HexMatrixTheory.Literal.addClosedProof (target proof : Lean.Expr) : Lean.MetaM Lean.Expr

Add the closed proof proof : target as an auxiliary lemma, checked by the kernel synchronously and exactly once, and return the constant. This is the declaration-checking path decide +kernel uses (mkAuxLemma), without reuse of an earlier lemma for the same statement, so every supplied proof is checked. mkAuxTheorem is not used: with its default zetaDelta := false its closure step type-checks the proof in the elaborator (Meta.check) before the kernel does, which evaluates the certificate a second time. The target and the proof must be closed, with no free variables and no expression or universe metavariables; the universe parameters are the level parameters they mention.

Equations

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

def HexMatrixTheory.Literal.identification (lit : Recognized) (A L : Lean.Expr) : Lean.MetaM Lean.Expr

The proof of A = ofLists n m L along the literal's route: rfl for a vector chain, one kernel decide on entriesEq otherwise.

Equations

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

def HexMatrixTheory.Literal.elabArgument (t : Lean.Syntax) (carrier : Lean.Expr := Lean.mkConst `Int) : Lean.Elab.TermElabM Lean.Expr

Elaborate a matrix argument with the frontend's carrier expectation. Integer frontends use the default; field frontends supply their field so unannotated numerals and fractions elaborate in that carrier.

Equations

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

structure HexMatrixTheory.Literal.VectorLiteral : Type

A closed vector literal, including a stated invariant-factor function.

• size : ℕ
• carrier : Lean.Expr
• entries : Array Lean.Expr
• route : Route

partial def HexMatrixTheory.Literal.matchVector? (n : ℕ) (carrier v : Lean.Expr) (budget : ℕ := unfoldBudget) : Lean.MetaM (Option VectorLiteral)

Recognize vector notation or a closed lambda behind bounded unfolding.

def HexMatrixTheory.Literal.vectorLiteral? (v : Lean.Expr) : Lean.MetaM (Option VectorLiteral)

Recognize a closed vector from its function type.

Equations

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

def HexMatrixTheory.Literal.vectorIdentification (lit : VectorLiteral) (v xs : Lean.Expr) : Lean.MetaM Lean.Expr

Identify a vector with its quoted list along the recognized route.

Equations

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