Rational hitting lists: grid computation

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

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

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

theorem Complexity.RationalHitting.StackLanguage.Poly.tabulateUp {A B : Type} [Coding A] [Coding B] {n : A → ℕ} {f : A × Unary → B} (hn : Poly fun (a : A) => { val := n a }) (hf : Poly f) : Poly fun (a : A) => List.map (fun (i : ℕ) => f (a, { val := i })) (List.range (n a))

theorem Complexity.RationalHitting.StackLanguage.Poly.flatMapUp {A B : Type} [Coding A] [Coding B] {n : A → ℕ} {f : A × Unary → List B} (hn : Poly fun (a : A) => { val := n a }) (hf : Poly f) : Poly fun (a : A) => List.flatMap (fun (i : ℕ) => f (a, { val := i })) (List.range (n a))

theorem Complexity.RationalHitting.StackLanguage.Poly.wordRange {A : Type} [Coding A] {n : A → ℕ} {f : A × Unary → BitWord} (hn : Poly fun (a : A) => { val := n a }) (hf : Poly f) : Poly fun (a : A) => { val := List.flatMap (fun (i : ℕ) => (f (a, { val := i })).val) (List.range (n a)) }

@[reducible, inline]

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

Two integer matrices and a denominator for rational output encoding.

Equations

• Complexity.RationalHitting.StackLanguage.Runtime.MatrixWordArgs = ((Complexity.RationalHitting.StackLanguage.DenseSquare × Complexity.RationalHitting.StackLanguage.DenseSquare) × ℤ)

def Complexity.RationalHitting.StackLanguage.Runtime.matrixWord (A B : DenseSquare) (den : ℤ) : BitWord

Encode all entries of a normalized rational matrix in row order.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.matrixWord_poly : Poly fun (a : MatrixWordArgs) => matrixWord a.1.1 a.1.2 a.2

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

@[reducible, inline]

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

Generator parameters, grid point, normalization matrix, and denominator.

Equations

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

def Complexity.RationalHitting.StackLanguage.Runtime.tupleWord (p : Params) (x : GridPoint) (A : DenseSquare) (den : ℤ) : BitWord

Encode every variable matrix of one normalized tuple.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.tupleWord_poly : Poly fun (a : TupleWordArgs) => tupleWord a.1.1 a.1.2 a.2.1 a.2.2

theorem Complexity.RationalHitting.StackLanguage.Runtime.tupleWord_eq (n s : ℕ) (x : GridPoint) (den : ℤ) : (tupleWord (Params.of n s) x (matrix (Params.of n s) x 0) den).val = encodeTuple (ExecutableGenerator.tuple (ExecutableGenerator.normalized (ExecutableGenerator.inputTables n (Parameters.truncation n s) (Parameters.exponent n s) (gridFn x)) den))

def Complexity.RationalHitting.StackLanguage.Runtime.point (p : Params) (x : GridPoint) : List BitWord

Emit the tuple encoding at a grid point only when normalization is defined.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.point_poly : Poly fun (a : Params × GridPoint) => point a.1 a.2

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.point_eq (n s : ℕ) (x : GridPoint) : point (Params.of n s) x = List.map (fun (X : Tuple n (Generator.matrixDimension (Parameters.exponent n s))) => { val := encodeTuple X }) (ExecutableGenerator.atPoint n (Parameters.truncation n s) (Parameters.exponent n s) (gridFn x)).toList

theorem Complexity.RationalHitting.StackLanguage.map_filterMap_toList {A B C : Type} (l : List A) (f : A → Option B) (g : B → C) : List.map g (List.filterMap f l) = List.flatMap (fun (a : A) => List.map g (f a).toList) l

def Complexity.RationalHitting.StackLanguage.Runtime.words (p : Params) : List BitWord

Concatenate the tuple encodings emitted throughout the three-dimensional grid.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Runtime.words_poly : Poly words

theorem Complexity.RationalHitting.StackLanguage.Runtime.gridFn_fin {H : ℕ} (t p r : Fin H) : gridFn ({ val := ↑t + 1 }, { val := ↑p + 1 }, { val := ↑r + 1 }) = fun (i : Fin (Nat.succ 0).succ.succ) => ↑(![t, p, r] i) + 1

theorem Complexity.RationalHitting.StackLanguage.Runtime.words_eq (n s : ℕ) : words (Params.of n s) = List.map (fun (X : Tuple n (ExecutableGenerator.list n s).dimension) => { val := encodeTuple X }) (ExecutableGenerator.list n s).tuples