Rational hitting lists: matrix computation

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

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

def Complexity.RationalHitting.StackLanguage.flattenStep {A : Type} (a : List (List A) × List A) : List (List A) × List A

Consume one inner list and append it to the flattening accumulator.

Equations

• Complexity.RationalHitting.StackLanguage.flattenStep a = (a.1.tail, a.2 ++ a.1.headD [])

theorem Complexity.RationalHitting.StackLanguage.flattenStep_code_le {A : Type} [Coding A] (a : List (List A) × List A) : (code (flattenStep a)).length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.flattenStep_iterate_code {A : Type} [Coding A] (a : List (List A) × List A) (k : ℕ) : (code (flattenStep^[k] a)).length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.flattenStep_iterate {A : Type} (l : List (List A)) (r : List A) : flattenStep^[l.length] (l, r) = ([], r ++ l.flatten)

theorem Complexity.RationalHitting.StackLanguage.Poly.listFlatten {A : Type} [Coding A] : Poly List.flatten

theorem Complexity.RationalHitting.StackLanguage.Poly.listFlatMap {A : Type} [Coding A] {B C : Type} [Coding B] [Coding C] [Inhabited B] {f : C × B → List A} (hf : Poly f) : Poly fun (a : C × List B) => List.flatMap (fun (b : B) => f (a.1, b)) a.2

@[instance_reducible]

instance Complexity.RationalHitting.StackLanguage.instInhabitedBitWord : Inhabited BitWord

Equations

• Complexity.RationalHitting.StackLanguage.instInhabitedBitWord = { default := { val := [] } }

def Complexity.RationalHitting.StackLanguage.concatStep (a : List BitWord × BitWord) : List BitWord × BitWord

Consume one word and append it to a concatenation accumulator.

Equations

• Complexity.RationalHitting.StackLanguage.concatStep a = (a.1.tail, { val := a.2.val ++ (a.1.headD { val := [] }).val })

theorem Complexity.RationalHitting.StackLanguage.concatStep_code_le (a : List BitWord × BitWord) : (code (concatStep a)).length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.concatStep_iterate_code (a : List BitWord × BitWord) (k : ℕ) : (code (concatStep^[k] a)).length ≤ (code a).length

theorem Complexity.RationalHitting.StackLanguage.concatStep_iterate (l : List BitWord) (r : List Bool) : concatStep^[l.length] (l, { val := r }) = ([], { val := r ++ List.flatMap BitWord.val l })

def Complexity.RationalHitting.StackLanguage.Procedure.encodeWord : Procedure (fun (x : List Bool) => x) (fun (x : List Bool) => x) encodedWord

Return the raw self-delimiting encoding of a binary natural word.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Poly.wordConcat : Poly fun (l : List BitWord) => { val := List.flatMap BitWord.val l }

theorem Complexity.RationalHitting.StackLanguage.Poly.encodeNat : Poly fun (a : ℕ) => { val := RationalHitting.encodeNat a }

theorem Complexity.RationalHitting.StackLanguage.Poly.encodeUnary : Poly fun (a : Unary) => { val := RationalHitting.encodeNat a.val }

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.Runtime.GridPoint : Type

Three unary coordinates of an integer specialization point.

Equations

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

def Complexity.RationalHitting.StackLanguage.Runtime.gridFn (x : GridPoint) : Fin 3 → ℕ

Read a grid-point record as a function on three coordinates.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.gridFn x = ![x.1.val, x.2.1.val, x.2.2.val]

def Complexity.RationalHitting.StackLanguage.Runtime.matrix (p : Params) (x : GridPoint) (a : Unary) : DenseSquare

Compute the dense integral matrix at the given grid point and variable index.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.matrix_poly : Poly fun (a : Params × GridPoint × Unary) => matrix a.1 a.2.1 a.2.2

theorem Complexity.RationalHitting.StackLanguage.Runtime.matrix_eq (n s : ℕ) (x : GridPoint) (a : Fin (n + 1)) : matrix (Params.of n s) x { val := ↑a } = DenseSquare.of (Generator.integralLift n (Parameters.truncation n s) (Parameters.exponent n s) (gridFn x) a)

def Complexity.RationalHitting.StackLanguage.Runtime.cramer (A B : DenseSquare) (i j : ℕ) : DenseSquare

Compute a Cramer numerator by replacing one matrix column.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.cramer A B i j = { dim := A.dim, val := fun (r c : Fin A.dim) => if ↑c = i then B.get (↑r) j else A.val r c }

theorem Complexity.RationalHitting.StackLanguage.Runtime.cramer_poly : Poly fun (a : (DenseSquare × DenseSquare) × Unary × Unary) => cramer a.1.1 a.1.2 a.2.1.val a.2.2.val

theorem Complexity.RationalHitting.StackLanguage.Runtime.cramer_of {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℤ) (i j : Fin d) : cramer (DenseSquare.of A) (DenseSquare.of B) ↑i ↑j = DenseSquare.of (A.updateCol i fun (r : Fin d) => B r j)

theorem Complexity.RationalHitting.StackLanguage.Runtime.cramer_det_of {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℤ) (i j : Fin d) : (cramer (DenseSquare.of A) (DenseSquare.of B) ↑i ↑j).val.det = (A.updateCol i fun (r : Fin d) => B r j).det

theorem Complexity.RationalHitting.StackLanguage.Runtime.cramer_encode_of {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℤ) (den : ℤ) (i j : Fin d) : encodeRat (Rat.divInt (cramer (DenseSquare.of A) (DenseSquare.of B) ↑i ↑j).val.det den) = encodeRat (Rat.divInt (A.updateCol i fun (r : Fin d) => B r j).det den)