Pointwise normalization and encoding in polynomial time

At each point (t, p, r) of the three-dimensional integer grid, the executable hitting-list generator materializes the n + 1 integer lift matrices [U₀, U₁, …, Uₙ], tests whether det U₀ = 0, and when det U₀ ≠ 0 computes every entry of each normalized matrix U₀⁻¹ * Uₐ as the reduced rational ratio of two integer determinants via Cramer's rule, before serializing the resulting tuple with encodeTuple.

This module expresses that per-point pipeline directly on the list-of-rows tables produced by liftRows and certifies that it runs in polynomial time on a multi-tape Turing machine:

• cramerRows A B colA colB replaces column colA of A by column colB of B;
• matrixEntryWord A B den i j encodes Rat.divInt (detRows (cramerRows A B i j)) den;
• matrixWord A B den and tupleWord tables den serialize one normalized matrix and the full tuple of n normalized matrices;
• pointWordOfTables, pointWordsOfTables, pointWord, and pointWords perform the singularity test on U₀ and emit the encoded tuple (or [] when singular).

Main definitions

• Cslib.Circuits.Rational.cramerRows: column replacement on lists of integer rows.
• Cslib.Circuits.Rational.matrixEntryWord, Cslib.Circuits.Rational.matrixWord, Cslib.Circuits.Rational.tupleWord: encoded entry, matrix, and tuple from integer row tables and a common denominator.
• Cslib.Circuits.Rational.pointWordOfTables, Cslib.Circuits.Rational.pointWordsOfTables, Cslib.Circuits.Rational.pointWord, Cslib.Circuits.Rational.pointWords: the singularity-tested encoded tuple at a grid point, as a bit word and as a singleton-or-empty list of bit words.

Main results

• Cslib.Circuits.Rational.cramerRows_eq: cramerRows agrees with Matrix.updateCol on rowsOf.
• Cslib.Circuits.Rational.matrixEntryWord_eq, Cslib.Circuits.Rational.matrixWord_eq, Cslib.Circuits.Rational.tupleWord_eq: agreement with ExecutableGenerator.normalizedEntry, ExecutableGenerator.normalized, and encodeTuple.
• Cslib.Circuits.Rational.pointWord_eq, Cslib.Circuits.Rational.pointWords_eq: pointWord and pointWords agree with ExecutableGenerator.atPoint composed with encodeTuple.
• Cslib.Circuits.Rational.computableInPolyTime_cramerRows, Cslib.Circuits.Rational.computableInPolyTime_matrixEntryWord, Cslib.Circuits.Rational.computableInPolyTime_matrixWord, Cslib.Circuits.Rational.computableInPolyTime_tupleWord, Cslib.Circuits.Rational.pointWordOfTables_polytime, Cslib.Circuits.Rational.pointWordsOfTables_polytime, Cslib.Circuits.Rational.computableInPolyTime_pointWord, Cslib.Circuits.Rational.computableInPolyTime_pointWords, Cslib.Circuits.Rational.pointWord_polytime: polynomial-time certificates for the per-point pipeline.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/PointComputation.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

List-level Cramer normalization and tuple encoding

def Cslib.Circuits.Rational.cramerRows (A B : List (List ℤ)) (colA colB : ℕ) : List (List ℤ)

Replace column colA of A with column colB of B, producing an A.length × A.length list of rows.

def Cslib.Circuits.Rational.matrixEntryWord (A B : List (List ℤ)) (den : ℤ) (i j : ℕ) : List Bool

Encoded reduced-rational (i, j)-entry of A⁻¹ * B given the common denominator den, computed by Cramer's rule and detRows.

def Cslib.Circuits.Rational.matrixWord (A B : List (List ℤ)) (den : ℤ) : List Bool

Encoded d × d rational matrix A⁻¹ * B in row-major order given the common denominator den, where d = A.length.

def Cslib.Circuits.Rational.tupleWord (tables : List (List (List ℤ))) (den : ℤ) : List Bool

Encoded tuple of n normalized rational matrices from a list tables of n + 1 integer tables [U₀, U₁, …, Uₙ] and the common denominator den.

def Cslib.Circuits.Rational.pointWordOfTables (tables : List (List (List ℤ))) : List Bool

Emit the encoded normalized tuple for a list of integer tables [U₀, U₁, …, Uₙ], or [] when detRows U₀ = 0.

def Cslib.Circuits.Rational.pointWordsOfTables (tables : List (List (List ℤ))) : List (List Bool)

Singleton list [tupleWord tables den] when detRows (tables.headD []) ≠ 0, and [] when singular; used to enumerate grid points by List.flatMap.

def Cslib.Circuits.Rational.pointWord (n N M Dg t p r : ℕ) : List Bool

Encoded normalized tuple at the grid coordinates (t, p, r), or [] if singular.

def Cslib.Circuits.Rational.pointWords (n N M Dg t p r : ℕ) : List (List Bool)

Singleton list containing the encoded normalized tuple at (t, p, r) when nonsingular, or [] when singular.

Agreement with the executable generator

theorem Cslib.Circuits.Rational.cramerRows_eq {d : ℕ} (A B : Matrix (Fin d) (Fin d) ℤ) (i j : Fin d) : cramerRows (rowsOf A) (rowsOf B) ↑i ↑j = rowsOf (A.updateCol i fun (r : Fin d) => B r j)

cramerRows on rowsOf computes the rows of Matrix.updateCol.

theorem Cslib.Circuits.Rational.matrixEntryWord_eq {d : ℕ} (A B : DeterminantAlgorithm.Table d) (den : ℤ) (i j : Fin d) : matrixEntryWord (rowsOf (DeterminantAlgorithm.denote A)) (rowsOf (DeterminantAlgorithm.denote B)) den ↑i ↑j = encodeRat (ExecutableGenerator.normalizedEntry A B den i j)

matrixEntryWord agrees with encodeRat (ExecutableGenerator.normalizedEntry A B den i j).

theorem Cslib.Circuits.Rational.matrixWord_eq {d : ℕ} (A B : DeterminantAlgorithm.Table d) (den : ℤ) : matrixWord (rowsOf (DeterminantAlgorithm.denote A)) (rowsOf (DeterminantAlgorithm.denote B)) den = List.flatMap (fun (i : Fin d) => List.flatMap (fun (j : Fin d) => encodeRat (ExecutableGenerator.normalizedEntry A B den i j)) (List.finRange d)) (List.finRange d)

matrixWord serializes all d × d entries of ExecutableGenerator.normalizedEntry A B den.

theorem Cslib.Circuits.Rational.tupleWord_eq {n d : ℕ} (A : Vector (DeterminantAlgorithm.Table d) (n + 1)) (den : ℤ) : tupleWord (List.map (fun (T : DeterminantAlgorithm.Table d) => rowsOf (DeterminantAlgorithm.denote T)) A.toList) den = encodeTuple (ExecutableGenerator.tuple (ExecutableGenerator.normalized A den))

tupleWord on the row lists of A equals encodeTuple on the normalized tuple.

theorem Cslib.Circuits.Rational.pointWordOfTables_eq {n d : ℕ} (A : Vector (DeterminantAlgorithm.Table d) (n + 1)) : pointWordOfTables (List.map (fun (T : DeterminantAlgorithm.Table d) => rowsOf (DeterminantAlgorithm.denote T)) A.toList) = have den := DeterminantAlgorithm.determinant (A.get 0); if den = 0 then [] else encodeTuple (ExecutableGenerator.tuple (ExecutableGenerator.normalized A den))

pointWordOfTables on the row lists of A tests determinant (A.get 0) = 0 and encodes the normalized tuple when nonsingular.

theorem Cslib.Circuits.Rational.pointWordsOfTables_eq {n d : ℕ} (A : Vector (DeterminantAlgorithm.Table d) (n + 1)) : pointWordsOfTables (List.map (fun (T : DeterminantAlgorithm.Table d) => rowsOf (DeterminantAlgorithm.denote T)) A.toList) = have den := DeterminantAlgorithm.determinant (A.get 0); if den = 0 then [] else [encodeTuple (ExecutableGenerator.tuple (ExecutableGenerator.normalized A den))]

pointWordsOfTables on the row lists of A produces [] when singular and the singleton encoded tuple when nonsingular.

theorem Cslib.Circuits.Rational.pointWord_eq (n N e : ℕ) (x : Fin 3 → ℕ) : pointWord n N (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (x 0) (x 1) (x 2) = (ExecutableGenerator.atPoint n N e x).elim [] encodeTuple

pointWord at (x 0, x 1, x 2) agrees with ExecutableGenerator.atPoint n N e x followed by encodeTuple.

theorem Cslib.Circuits.Rational.pointWords_eq (n N e : ℕ) (x : Fin 3 → ℕ) : pointWords n N (CyclotomicRing.dimension e) (CyclotomicRing.degree e) (x 0) (x 1) (x 2) = (Option.map encodeTuple (ExecutableGenerator.atPoint n N e x)).toList

pointWords at (x 0, x 1, x 2) agrees with ((ExecutableGenerator.atPoint n N e x).map encodeTuple).toList.

Polynomial-time certificates

theorem Cslib.Circuits.Rational.computableInPolyTime_cramerRows {α : Type} {encIn : α ↪ List Bool} {A B : α → List (List ℤ)} {colA colB : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hcolA : Turing.MultiTapeTM.ComputableInPolyTime colA encIn Turing.MultiTapeTM.encUnary) (hcolB : Turing.MultiTapeTM.ComputableInPolyTime colB encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => cramerRows (A x) (B x) (colA x) (colB x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Column replacement cramerRows is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_matrixEntryWord {α : Type} {encIn : α ↪ List Bool} {A B : α → List (List ℤ)} {den : α → ℤ} {i j : α → ℕ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hden : Turing.MultiTapeTM.ComputableInPolyTime den encIn Turing.MultiTapeTM.encIntBin) (hi : Turing.MultiTapeTM.ComputableInPolyTime i encIn Turing.MultiTapeTM.encUnary) (hj : Turing.MultiTapeTM.ComputableInPolyTime j encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => matrixEntryWord (A x) (B x) (den x) (i x) (j x)) encIn Turing.MultiTapeTM.encBits

Encoding one normalized rational entry via Cramer's rule and detRows is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_matrixWord {α : Type} {encIn : α ↪ List Bool} {A B : α → List (List ℤ)} {den : α → ℤ} (hA : Turing.MultiTapeTM.ComputableInPolyTime A encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hB : Turing.MultiTapeTM.ComputableInPolyTime B encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hden : Turing.MultiTapeTM.ComputableInPolyTime den encIn Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => matrixWord (A x) (B x) (den x)) encIn Turing.MultiTapeTM.encBits

Encoding a full normalized rational matrix is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_tupleWord {α : Type} {encIn : α ↪ List Bool} {tables : α → List (List (List ℤ))} {den : α → ℤ} (htables : Turing.MultiTapeTM.ComputableInPolyTime tables encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) (hden : Turing.MultiTapeTM.ComputableInPolyTime den encIn Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => tupleWord (tables x) (den x)) encIn Turing.MultiTapeTM.encBits

Encoding a tuple of normalized rational matrices from tables and den is polynomial-time.

theorem Cslib.Circuits.Rational.pointWordOfTables_polytime : Turing.MultiTapeTM.ComputableInPolyTime pointWordOfTables (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) Turing.MultiTapeTM.encBits

Singularity-tested tuple encoding on a list of integer tables is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_pointWordOfTables {α : Type} {encIn : α ↪ List Bool} {tables : α → List (List (List ℤ))} (htables : Turing.MultiTapeTM.ComputableInPolyTime tables encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => pointWordOfTables (tables x)) encIn Turing.MultiTapeTM.encBits

Compositional polynomial-time certificate for pointWordOfTables.

theorem Cslib.Circuits.Rational.pointWordsOfTables_polytime : Turing.MultiTapeTM.ComputableInPolyTime pointWordsOfTables (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Singularity-tested singleton-or-empty tuple encoding on a list of integer tables is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_pointWordsOfTables {α : Type} {encIn : α ↪ List Bool} {tables : α → List (List (List ℤ))} (htables : Turing.MultiTapeTM.ComputableInPolyTime tables encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => pointWordsOfTables (tables x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Compositional polynomial-time certificate for pointWordsOfTables.

theorem Cslib.Circuits.Rational.computableInPolyTime_pointWord {α : Type} {encIn : α ↪ List Bool} {n N M Dg t p r : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encUnary) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => pointWord (n x) (N x) (M x) (Dg x) (t x) (p x) (r x)) encIn Turing.MultiTapeTM.encBits

Computing the encoded normalized tuple at a grid point is polynomial-time.

theorem Cslib.Circuits.Rational.computableInPolyTime_pointWords {α : Type} {encIn : α ↪ List Bool} {n N M Dg t p r : α → ℕ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hN : Turing.MultiTapeTM.ComputableInPolyTime N encIn Turing.MultiTapeTM.encUnary) (hM : Turing.MultiTapeTM.ComputableInPolyTime M encIn Turing.MultiTapeTM.encUnary) (hDg : Turing.MultiTapeTM.ComputableInPolyTime Dg encIn Turing.MultiTapeTM.encUnary) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encUnary) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => pointWords (n x) (N x) (M x) (Dg x) (t x) (p x) (r x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Computing the singleton-or-empty list of encoded tuples at a grid point is polynomial-time.

theorem Cslib.Circuits.Rational.pointWord_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : ℕ × ℕ × ℕ × ℕ × ℕ × ℕ × ℕ) => pointWord q.1 q.2.1 q.2.2.1 q.2.2.2.1 q.2.2.2.2.1 q.2.2.2.2.2.1 q.2.2.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)))))) Turing.MultiTapeTM.encBits

Standalone polynomial-time certificate for pointWord on a 7-tuple of unary naturals.