Rational hitting lists: dense determinant

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/DenseDeterminant.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

@[simp]

theorem Complexity.RationalHitting.StackLanguage.list_code_length_nil {A : Type} [Coding A] : (code []).length = 0

@[simp]

theorem Complexity.RationalHitting.StackLanguage.list_code_cons {A : Type} [Coding A] (a : A) (l : List A) : (code (a :: l)).length = 2 * (code a).length + 1 + (code l).length

theorem Complexity.RationalHitting.StackLanguage.code_le_of_mem {A : Type} [Coding A] {a : A} {l : List A} (h : a ∈ l) : (code a).length ≤ (code l).length

theorem Complexity.RationalHitting.StackLanguage.list_code_length_le {A : Type} [Coding A] (l : List A) (B : ℕ) (h : ∀ a ∈ l, (code a).length ≤ B) : (code l).length ≤ l.length * (2 * B + 1)

theorem Complexity.RationalHitting.StackLanguage.drop_headD_getElem {A : Type} (l : List A) (z : A) (i : ℕ) (hi : i < l.length) : (List.drop i l).headD z = l[i]

theorem Complexity.RationalHitting.StackLanguage.finRows_access {A : Type} (z : A) {n : ℕ} (f : Fin n → A) (i : Fin n) : (List.drop (↑i) (List.map f (List.finRange n))).headD z = f i

theorem Complexity.RationalHitting.StackLanguage.finRange_map_val (n : ℕ) : List.map Fin.val (List.finRange n) = List.range n

theorem Complexity.RationalHitting.StackLanguage.range_map_to_finRange {A : Type} (n : ℕ) (f : ℕ → A) : List.map f (List.range n) = List.map (fun (i : Fin n) => f ↑i) (List.finRange n)

structure Complexity.RationalHitting.StackLanguage.DenseSquare : Type

A square integer matrix carrying its dimension.

• dim : ℕ

  Number of rows and columns.

• val : Matrix (Fin self.dim) (Fin self.dim) ℤ

  Integer matrix entries.

def Complexity.RationalHitting.StackLanguage.DenseSquare.rows (a : DenseSquare) : List (List ℤ)

Enumerate the matrix entries as a list of rows.

Equations

• a.rows = List.map (fun (i : Fin a.dim) => List.map (fun (j : Fin a.dim) => a.val i j) (List.finRange a.dim)) (List.finRange a.dim)

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instCodingDenseSquare : Coding DenseSquare

Equations

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

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instInhabitedDenseSquare : Inhabited DenseSquare

Equations

• Complexity.RationalHitting.StackLanguage.instInhabitedDenseSquare = { default := { dim := 0, val := 0 } }

def Complexity.RationalHitting.StackLanguage.DenseSquare.get (a : DenseSquare) (i j : ℕ) : ℤ

Read a matrix entry, returning zero outside the stored dimension.

Equations

• a.get i j = if hi : i < a.dim then if hj : j < a.dim then a.val ⟨i, hi⟩ ⟨j, hj⟩ else 0 else 0

@[simp]

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.get_fin (a : DenseSquare) (i j : Fin a.dim) : a.get ↑i ↑j = a.val i j

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.rows_get (a : DenseSquare) (i j : ℕ) : (List.drop j ((List.drop i a.rows).headD [])).headD 0 = a.get i j

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.dim_le_code (a : DenseSquare) : a.dim ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.entry_bits_le_code (a : DenseSquare) (i j : Fin a.dim) : (a.val i j).natAbs.bits.length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.get_bits_le_code (a : DenseSquare) (i j : ℕ) : (a.get i j).natAbs.bits.length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.code_length_le (a : DenseSquare) (b : ℕ) (h : ∀ (i j : Fin a.dim), (a.val i j).natAbs.bits.length ≤ b) : (code a).length ≤ 4 * a.dim ^ 2 * b + 14 * a.dim ^ 2 + 3 * a.dim + 1

theorem Complexity.RationalHitting.StackLanguage.Poly.denseDim : Poly fun (a : DenseSquare) => { val := a.dim }

theorem Complexity.RationalHitting.StackLanguage.Poly.denseRows : Poly DenseSquare.rows

theorem Complexity.RationalHitting.StackLanguage.Poly.denseGet : Poly fun (a : DenseSquare × Unary × Unary) => a.1.get a.2.1.val a.2.2.val

theorem Complexity.RationalHitting.StackLanguage.Poly.denseBuild {A : Type} [Coding A] {n : A → Unary} {f : A × Unary × Unary → ℤ} (hn : Poly n) (hf : Poly f) : Poly fun (a : A) => { dim := (n a).val, val := fun (i j : Fin (n a).val) => f (a, { val := ↑i }, { val := ↑j }) }

theorem Complexity.RationalHitting.StackLanguage.Poly.sumRange {A : Type} [Coding A] {f : A × Unary → ℤ} (hf : Poly f) : Poly fun (a : Unary × A) => (List.map (fun (i : ℕ) => f (a.2, { val := i })) (List.range a.1.val)).sum

def Complexity.RationalHitting.StackLanguage.DenseSquare.of {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : DenseSquare

Package an indexed matrix with its dimension.

Equations

• Complexity.RationalHitting.StackLanguage.DenseSquare.of A = { dim := n, val := A }

def Complexity.RationalHitting.StackLanguage.DenseSquare.step (A F : DenseSquare) : DenseSquare

One Bird determinant stage on dimension-carrying matrices.

Equations

• A.step F = { dim := A.dim, val := BirdDet.Spec.stepEntry A.val fun (i j : Fin A.dim) => F.get ↑i ↑j }

@[simp]

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.step_dim (A F : DenseSquare) : (A.step F).dim = A.dim

@[simp]

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.step_of {n : ℕ} (A F : Matrix (Fin n) (Fin n) ℤ) : (of A).step (of F) = of (BirdDet.Spec.stepEntry A F)

theorem Complexity.RationalHitting.StackLanguage.sum_diag_range (A F : DenseSquare) (i : Fin A.dim) : (List.map (fun (k : ℕ) => if ↑i < k then F.get k k else 0) (List.range A.dim)).sum = ∑ k > i, F.get ↑k ↑k

theorem Complexity.RationalHitting.StackLanguage.sum_product_range (A F : DenseSquare) (i j : Fin A.dim) : (List.map (fun (k : ℕ) => if ↑i < k then F.get (↑i) k * A.get k ↑j else 0) (List.range A.dim)).sum = ∑ k > i, F.get ↑i ↑k * A.val k j

theorem Complexity.RationalHitting.StackLanguage.Poly.denseStep : Poly fun (a : DenseSquare × DenseSquare) => a.1.step a.2

theorem Complexity.RationalHitting.StackLanguage.abs_le_pow_of_bits_le (z : ℤ) (b : ℕ) (h : z.natAbs.bits.length ≤ b) : |z| ≤ 2 ^ b

theorem Complexity.RationalHitting.StackLanguage.bits_le_of_abs_le_pow (z : ℤ) (b : ℕ) (h : |z| ≤ 2 ^ b) : z.natAbs.bits.length ≤ b + 1

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.get_abs_le (A : DenseSquare) (i j : ℕ) : |A.get i j| ≤ 2 ^ (code A).length

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.step_get_bound (A F : DenseSquare) (B C : ℕ) (hA : ∀ (i j : ℕ), |A.get i j| ≤ ↑B) (hF : ∀ (i j : ℕ), |F.get i j| ≤ ↑C) (i j : ℕ) : |(A.step F).get i j| ≤ ↑(2 * A.dim * B * C)

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.iterate_get_bound (A F : DenseSquare) (b : ℕ) (hA : ∀ (i j : ℕ), |A.get i j| ≤ 2 ^ b) (hF : ∀ (i j : ℕ), |F.get i j| ≤ 2 ^ b) (k i j : ℕ) : |(A.step^[k] F).get i j| ≤ 2 ^ (b + k * (1 + A.dim + b))

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.iterate_dim (A F : DenseSquare) (k : ℕ) : (A.step^[k + 1] F).dim = A.dim

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.iterate_code_bound (A F : DenseSquare) (b k : ℕ) (hA : (code A).length ≤ b) (hF : (code F).length ≤ b) : (code (A.step^[k + 1] F)).length ≤ 4 * A.dim ^ 2 * (b + (k + 1) * (1 + A.dim + b) + 1) + 14 * A.dim ^ 2 + 3 * A.dim + 1

def Complexity.RationalHitting.StackLanguage.birdState (a : DenseSquare × DenseSquare) : DenseSquare × DenseSquare

Advance the Bird stage while preserving the original matrix.

Equations

• Complexity.RationalHitting.StackLanguage.birdState a = (a.1, a.1.step a.2)

theorem Complexity.RationalHitting.StackLanguage.birdState_iterate (a : DenseSquare × DenseSquare) (k : ℕ) : birdState^[k] a = (a.1, a.1.step^[k] a.2)

theorem Complexity.RationalHitting.StackLanguage.birdState_iterate_size (n : ℕ) (a : DenseSquare × DenseSquare) (i : ℕ) (hi : i ≤ n) : (code (birdState^[i] a)).length ≤ (64 * (TimeBound.variable + 1) ^ 4).eval ((pairCode unaryCode code (n, a)).length + 1)

theorem Complexity.RationalHitting.StackLanguage.Poly.birdState_poly : Poly birdState

theorem Complexity.RationalHitting.StackLanguage.Poly.birdStages : Poly fun (a : Unary × DenseSquare) => a.2.step^[a.1.val] a.2

def Complexity.RationalHitting.StackLanguage.DenseSquare.detAlgorithm (A : DenseSquare) : ℤ

The executable determinant obtained from bounded Bird iteration.

Equations

• A.detAlgorithm = if A.dim = 0 then 1 else (-1) ^ (A.dim - 1) * (A.step^[A.dim - 1] A).get 0 0

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.iterate_of {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (k : ℕ) : (of A).step^[k] (of A) = of ((BirdDet.Spec.stepEntry A)^[k] A)

theorem Complexity.RationalHitting.StackLanguage.DenseSquare.detAlgorithm_eq (A : DenseSquare) : A.detAlgorithm = A.val.det

theorem Complexity.RationalHitting.StackLanguage.Poly.denseDet : Poly fun (A : DenseSquare) => A.val.det