Executable confluent Hermite Cramer recovery

Executable list-of-rows builders and plain Turing.MultiTapeTM.ComputableInPolyTime certificates for recovering the integer constant term H(0) = (H_zero : ℚ) of a rational polynomial H ∈ ℚ[X] with H.natDegree < N (N = nodes.length * J) from a nodes.length × J table jets (jets.length = nodes.length, each row of length J) of integer-scaled order-J Taylor jets Ω · [z ^ j] H(t_i + z) with nonzero scale Ω ≠ 0 at distinct integer nodes nodes = [t_0, …, t_{Q-1}] (nodes.Nodup).

Following Appendix B.3, equation (B.1), of [OAI26c], hermiteRows nodes J tabulates the N × N integer confluent Vandermonde matrix V (Polynomial.hermiteMatrix), cramerColZeroRows replaces column 0 with the flattened scaled jet vector b = Ω y to form V_{(0)}, and hermiteRecoverZero evaluates N_H = detRows V_{(0)} and D_H = detRows V via the division-free staged determinant of Complexity/Computability/Circuit/Rational/Runtime/Determinant.lean before performing the single total integer division N_H / (Ω · D_H) (Int.ediv, exact when nodes.Nodup and Ω ≠ 0, and returning 0 when Ω = 0 or D_H = 0). hermiteRecoverModPowTwo composes this recovery with Int.modPowTwo to extract bounded counts modulo 2 ^ ℓ.

Main definitions

• Cslib.Circuits.Rational.hermiteRows: executable (nodes.length * J) × (nodes.length * J) integer confluent Vandermonde matrix as List (List ℤ).
• Cslib.Circuits.Rational.cramerColZeroRows: replace column 0 of each row k with rhs[k].
• Cslib.Circuits.Rational.hermiteRecoverZero: recover integer H(0) = det V_{(0)} / (Ω · det V) for nonzero Ω ≠ 0 and distinct nodes via detRows and total Int.ediv (returning 0 when Ω = 0 or det V = 0).
• Cslib.Circuits.Rational.hermiteRecoverModPowTwo: recover the least nonnegative residue of integer H(0) modulo 2 ^ ℓ under the same Ω ≠ 0, nodes.Nodup, degree, and jet-shape hypotheses.

Main results

• Cslib.Circuits.Rational.length_hermiteRows, Cslib.Circuits.Rational.length_of_mem_hermiteRows, Cslib.Circuits.Rational.length_cramerColZeroRows, Cslib.Circuits.Rational.length_of_mem_cramerColZeroRows: shape well-formedness.
• Cslib.Circuits.Rational.ofRows_hermiteRows, Cslib.Circuits.Rational.detRows_hermiteRows, Cslib.Circuits.Rational.detRows_hermiteRows_ne_zero: ofRows and detRows agreement with Polynomial.hermiteMatrix and nonsingularity for nodes.Nodup.
• Cslib.Circuits.Rational.detRows_cramerColZeroRows_eq_mul_eval_zero, Cslib.Circuits.Rational.hermiteRecoverZero_eq_of_rowEntry, Cslib.Circuits.Rational.hermiteRecoverZero_eq, Cslib.Circuits.Rational.hermiteRecoverModPowTwo_eq, Cslib.Circuits.Rational.modPowTwo_sum_hermiteRecoverZero_eq: exact Cramer numerator identity and integer / modular recovery of H(0) and coordinate sums.
• Cslib.Circuits.Rational.intBits_tdiv_le, Cslib.Circuits.Rational.intBits_ediv_le, Cslib.Circuits.Rational.intBits_emod_le_of_ne_zero, Cslib.Circuits.Rational.intBits_emod_le_add_one_of_ne_zero, Cslib.Circuits.Rational.intBits_emod_le_max, Cslib.Circuits.Rational.intBits_modPowTwo_le, Cslib.Circuits.Rational.intBits_le_of_mem_hermiteRows, Cslib.Circuits.Rational.intBits_le_of_mem_cramerColZeroRows: sign-magnitude bit-length bounds for division, modular reduction, and Hermite/Cramer table entries.
• Cslib.Circuits.Rational.computableInPolyTime_hermiteRows, Cslib.Circuits.Rational.hermiteRows_polytime, Cslib.Circuits.Rational.computableInPolyTime_cramerColZeroRows, Cslib.Circuits.Rational.cramerColZeroRows_polytime, Cslib.Circuits.Rational.computableInPolyTime_hermiteRecoverZero, Cslib.Circuits.Rational.hermiteRecoverZero_polytime, Cslib.Circuits.Rational.computableInPolyTime_hermiteRecoverModPowTwo, Cslib.Circuits.Rational.hermiteRecoverModPowTwo_polytime, Cslib.Circuits.Rational.computableInPolyTime_modPowTwo_sum_hermiteRecoverZero: plain polynomial-time certificates.

References

• OpenAI, The Exponential Time Hypothesis is False

Executable list-of-rows builders

def Cslib.Circuits.Rational.hermiteRows (nodes : List ℤ) (J : ℕ) : List (List ℤ)

The (nodes.length * J) × (nodes.length * J) integer confluent Vandermonde (Hermite) matrix at nodes of uniform order J, stored in row-major (node, jet-order) order: row i * J + j and column m holds (m.choose j : ℤ) * nodes[i] ^ (m - j), which vanishes for m < j.

def Cslib.Circuits.Rational.cramerColZeroRows (mat : List (List ℤ)) (rhs : List ℤ) : List (List ℤ)

Replace column 0 of each row k of mat with rhs.getD k 0, keeping the tail of each row unchanged.

def Cslib.Circuits.Rational.hermiteRecoverZero (nodes : List ℤ) (J : ℕ) (Ω : ℤ) (jets : List (List ℤ)) : ℤ

Recover the integer value H(0) = (H_zero : ℚ) of H ∈ ℚ[X] with H.natDegree < nodes.length * J from a nodes.length × J table jets (jets.length = nodes.length, each row of length J) of its Ω-scaled order-J Taylor jets with nonzero scale Ω ≠ 0 at distinct integer nodes (nodes.Nodup), via Cramer's rule, detRows, and total Int.ediv (returning 0 when Ω = 0 or detRows (hermiteRows nodes J) = 0; see hermiteRecoverZero_eq).

def Cslib.Circuits.Rational.hermiteRecoverModPowTwo (nodes : List ℤ) (J ℓ : ℕ) (Ω : ℤ) (jets : List (List ℤ)) : ℤ

Recover the least nonnegative residue of integer H(0) modulo 2 ^ ℓ from Ω-scaled order-J Taylor jets jets under the hypotheses of hermiteRecoverZero_eq (nodes.Nodup, Ω ≠ 0, H.natDegree < nodes.length * J, integer H(0), and nodes.length × J jet shape; see hermiteRecoverModPowTwo_eq).

Shape and well-formedness

@[simp]

theorem Cslib.Circuits.Rational.length_hermiteRows (nodes : List ℤ) (J : ℕ) : (hermiteRows nodes J).length = nodes.length * J

hermiteRows nodes J has nodes.length * J rows.

theorem Cslib.Circuits.Rational.length_of_mem_hermiteRows {nodes : List ℤ} {J : ℕ} {row : List ℤ} (hrow : row ∈ hermiteRows nodes J) : row.length = nodes.length * J

Every row of hermiteRows nodes J has length nodes.length * J.

@[simp]

theorem Cslib.Circuits.Rational.length_cramerColZeroRows (mat : List (List ℤ)) (rhs : List ℤ) : (cramerColZeroRows mat rhs).length = mat.length

cramerColZeroRows mat rhs preserves the number of rows of mat.

theorem Cslib.Circuits.Rational.length_of_mem_cramerColZeroRows {mat : List (List ℤ)} {rhs : List ℤ} (hmat : ∀ r ∈ mat, r.length = mat.length) {row : List ℤ} (hrow : row ∈ cramerColZeroRows mat rhs) : row.length = mat.length

If every row of mat has length mat.length, then every row of cramerColZeroRows mat rhs has length mat.length.

theorem Cslib.Circuits.Rational.length_of_mem_cramerColZeroRows_hermiteRows {nodes : List ℤ} {J : ℕ} {rhs row : List ℤ} (hrow : row ∈ cramerColZeroRows (hermiteRows nodes J) rhs) : row.length = nodes.length * J

Every row of cramerColZeroRows (hermiteRows nodes J) rhs has length nodes.length * J.

Agreement with Polynomial.hermiteMatrix and Matrix.updateCol

theorem Cslib.Circuits.Rational.rowEntry_hermiteRows (nodes : List ℤ) (J : ℕ) (r c : Fin nodes.length × Fin J) : rowEntry (hermiteRows nodes J) ↑(finProdFinEquiv r) ↑(finProdFinEquiv c) = Polynomial.hermiteMatrix (fun (i : Fin nodes.length) => nodes[i]) J r c

Entry (finProdFinEquiv r, finProdFinEquiv c) of hermiteRows nodes J equals entry (r, c) of Polynomial.hermiteMatrix.

theorem Cslib.Circuits.Rational.ofRows_hermiteRows (nodes : List ℤ) (J : ℕ) : ofRows (hermiteRows nodes J) = (Matrix.reindex (finProdFinEquiv.trans (finCongr ⋯)) (finProdFinEquiv.trans (finCongr ⋯))) (Polynomial.hermiteMatrix (fun (i : Fin nodes.length) => nodes[i]) J)

ofRows (hermiteRows nodes J) is Polynomial.hermiteMatrix reindexed along finProdFinEquiv.

theorem Cslib.Circuits.Rational.detRows_hermiteRows (nodes : List ℤ) (J : ℕ) : detRows (hermiteRows nodes J) = (Polynomial.hermiteMatrix (fun (i : Fin nodes.length) => nodes[i]) J).det

detRows (hermiteRows nodes J) equals the determinant of Polynomial.hermiteMatrix.

theorem Cslib.Circuits.Rational.detRows_hermiteRows_ne_zero {nodes : List ℤ} (hnodup : nodes.Nodup) (J : ℕ) : detRows (hermiteRows nodes J) ≠ 0

At distinct integer nodes (nodes.Nodup), detRows (hermiteRows nodes J) is nonzero.

theorem Cslib.Circuits.Rational.rowEntry_cramerColZeroRows (mat : List (List ℤ)) (rhs : List ℤ) {i : ℕ} (hi : i < mat.length) (j : ℕ) : rowEntry (cramerColZeroRows mat rhs) i j = if j = 0 then rhs.getD i 0 else rowEntry mat i j

Looking up entry (i, j) of cramerColZeroRows mat rhs for i < mat.length returns rhs.getD i 0 in column 0 and rowEntry mat i j in columns j > 0.

theorem Cslib.Circuits.Rational.ofRows_cramerColZeroRows (mat : List (List ℤ)) (rhs : List ℤ) (h0 : 0 < mat.length) : ofRows (cramerColZeroRows mat rhs) = (Matrix.reindex (finCongr ⋯) (finCongr ⋯)) ((ofRows mat).updateCol ⟨0, h0⟩ fun (i : Fin mat.length) => rhs.getD (↑i) 0)

For nonempty mat, ofRows (cramerColZeroRows mat rhs) is (ofRows mat).updateCol 0 reindexed along length_cramerColZeroRows.

theorem Cslib.Circuits.Rational.detRows_cramerColZeroRows (mat : List (List ℤ)) (rhs : List ℤ) (h0 : 0 < mat.length) : detRows (cramerColZeroRows mat rhs) = ((ofRows mat).updateCol ⟨0, h0⟩ fun (i : Fin mat.length) => rhs.getD (↑i) 0).det

detRows (cramerColZeroRows mat rhs) is the determinant of ofRows mat with column 0 replaced by rhs.

theorem Cslib.Circuits.Rational.detRows_cramerColZeroRows_hermiteRows (nodes : List ℤ) (J : ℕ) (jets : List (List ℤ)) (hQ : 0 < nodes.length) (hJ : 0 < J) (hjets_len : jets.length = nodes.length) (hjets_row : ∀ row ∈ jets, row.length = J) : detRows (cramerColZeroRows (hermiteRows nodes J) jets.flatten) = ((Polynomial.hermiteMatrix (fun (i : Fin nodes.length) => nodes[i]) J).updateCol (⟨0, hQ⟩, ⟨0, hJ⟩) fun (r : Fin nodes.length × Fin J) => rowEntry jets ↑r.1 ↑r.2).det

detRows of cramerColZeroRows (hermiteRows nodes J) jets.flatten equals the determinant of Polynomial.hermiteMatrix with column (0, 0) replaced by (i, j) ↦ rowEntry jets i j.

Exact Cramer recovery of H(0)

theorem Cslib.Circuits.Rational.detRows_cramerColZeroRows_eq_mul_eval_zero {nodes : List ℤ} {J : ℕ} {Ω H_zero : ℤ} {jets : List (List ℤ)} {H : Polynomial ℚ} (hdeg : H.natDegree < nodes.length * J) (hH0 : Polynomial.eval 0 H = ↑H_zero) (hjets_len : jets.length = nodes.length) (hjets_row : ∀ row ∈ jets, row.length = J) (hjets : ∀ (i : Fin nodes.length) (j : Fin J), ↑(rowEntry jets ↑i ↑j) = ↑Ω * ((Polynomial.taylor ↑nodes[i]) H).coeff ↑j) : detRows (cramerColZeroRows (hermiteRows nodes J) jets.flatten) = Ω * detRows (hermiteRows nodes J) * H_zero

Exact integer Cramer identity for scaled Taylor jets: without any distinctness or nonzero-scale assumption, detRows (cramerColZeroRows (hermiteRows nodes J) jets.flatten) equals (Ω * detRows (hermiteRows nodes J)) * H_zero.

theorem Cslib.Circuits.Rational.hermiteRecoverZero_eq_of_rowEntry {nodes : List ℤ} {J : ℕ} {Ω H_zero : ℤ} {jets : List (List ℤ)} {H : Polynomial ℚ} (hnodup : nodes.Nodup) (hΩ : Ω ≠ 0) (hdeg : H.natDegree < nodes.length * J) (hH0 : Polynomial.eval 0 H = ↑H_zero) (hjets_len : jets.length = nodes.length) (hjets_row : ∀ row ∈ jets, row.length = J) (hjets : ∀ (i : Fin nodes.length) (j : Fin J), ↑(rowEntry jets ↑i ↑j) = ↑Ω * ((Polynomial.taylor ↑nodes[i]) H).coeff ↑j) : hermiteRecoverZero nodes J Ω jets = H_zero

Exact confluent Hermite Cramer recovery (rowEntry form). When nodes are distinct, Ω ≠ 0, H ∈ ℚ[X] has natDegree < nodes.length * J and integer value H(0) = H_zero, and jets holds the Ω-scaled order-J Taylor jets at nodes, hermiteRecoverZero returns H_zero.

theorem Cslib.Circuits.Rational.hermiteRecoverZero_eq {nodes : List ℤ} {J : ℕ} {Ω H_zero : ℤ} {jets : List (List ℤ)} {H : Polynomial ℚ} (hnodup : nodes.Nodup) (hΩ : Ω ≠ 0) (hdeg : H.natDegree < nodes.length * J) (hH0 : Polynomial.eval 0 H = ↑H_zero) (hjets_len : jets.length = nodes.length) (hjets_row : ∀ row ∈ jets, row.length = J) (hjets : ∀ (i : Fin nodes.length) (j : Fin J), have hi := ⋯; have hj := ⋯; ↑jets[↑i][↑j] = ↑Ω * ((Polynomial.taylor ↑nodes[i]) H).coeff ↑j) : hermiteRecoverZero nodes J Ω jets = H_zero

Exact confluent Hermite Cramer recovery (getElem form, [OAI26c] eq. (B.1)).

theorem Cslib.Circuits.Rational.hermiteRecoverModPowTwo_eq {nodes : List ℤ} {J ℓ : ℕ} {Ω H_zero count : ℤ} {jets : List (List ℤ)} {H : Polynomial ℚ} (hnodup : nodes.Nodup) (hΩ : Ω ≠ 0) (hdeg : H.natDegree < nodes.length * J) (hH0 : Polynomial.eval 0 H = ↑H_zero) (hjets_len : jets.length = nodes.length) (hjets_row : ∀ row ∈ jets, row.length = J) (hjets : ∀ (i : Fin nodes.length) (j : Fin J), ↑(rowEntry jets ↑i ↑j) = ↑Ω * ((Polynomial.taylor ↑nodes[i]) H).coeff ↑j) (hcount₀ : 0 ≤ count) (hcount₁ : count < 2 ^ ℓ) (hdvd : 2 ^ ℓ ∣ H_zero - count) : hermiteRecoverModPowTwo nodes J ℓ Ω jets = count

Modular recovery of a count count ∈ [0, 2 ^ ℓ) congruent to H(0) modulo 2 ^ ℓ.

theorem Cslib.Circuits.Rational.modPowTwo_sum_hermiteRecoverZero_eq {nodes : List ℤ} {J ℓ : ℕ} {Ω count : ℤ} {coordJets : List (List (List ℤ))} {Hs : List (Polynomial ℚ)} {H_zeros : List ℤ} (hnodup : nodes.Nodup) (hΩ : Ω ≠ 0) (hlen_H : Hs.length = coordJets.length) (hlen_Z : H_zeros.length = coordJets.length) (hcoord : ∀ (s : Fin coordJets.length), have hsH := ⋯; have hsZ := ⋯; Hs[↑s].natDegree < nodes.length * J ∧ Polynomial.eval 0 Hs[↑s] = ↑H_zeros[↑s] ∧ coordJets[s].length = nodes.length ∧ (∀ row ∈ coordJets[s], row.length = J) ∧ ∀ (i : Fin nodes.length) (j : Fin J), ↑(rowEntry coordJets[s] ↑i ↑j) = ↑Ω * ((Polynomial.taylor ↑nodes[i]) Hs[↑s]).coeff ↑j) (hcount₀ : 0 ≤ count) (hcount₁ : count < 2 ^ ℓ) (hdvd : 2 ^ ℓ ∣ H_zeros.sum - count) : (List.map (hermiteRecoverZero nodes J Ω) coordJets).sum.modPowTwo ℓ = count

Multi-coordinate count recovery modulo 2 ^ ℓ ([OAI26c], Appendix B.3): summing the recovered integer constant terms H_s(0) across coordinates and reducing modulo 2 ^ ℓ yields count whenever 0 ≤ count < 2 ^ ℓ and 2 ^ ℓ ∣ ∑_s H_s(0) - count.

Entry magnitude and bit-length bounds

theorem Cslib.Circuits.Rational.intBits_tdiv_le (a b : ℤ) : intBits (a.tdiv b) ≤ intBits a

Truncated integer division never increases the sign-magnitude bit length of the dividend.

theorem Cslib.Circuits.Rational.intBits_ediv_le (a b : ℤ) : intBits (a.ediv b) ≤ intBits a

Euclidean integer division never increases the sign-magnitude bit length of the dividend.

theorem Cslib.Circuits.Rational.intBits_emod_le_of_ne_zero (a : ℤ) {b : ℤ} (hb : b ≠ 0) : intBits (a.emod b) ≤ intBits b

For a nonzero divisor b, the Euclidean remainder a.emod b has sign-magnitude bit length at most intBits b.

theorem Cslib.Circuits.Rational.intBits_emod_le_add_one_of_ne_zero (a : ℤ) {b : ℤ} (hb : b ≠ 0) : intBits (a.emod b) ≤ intBits b + 1

For a nonzero divisor b, intBits (a.emod b) ≤ intBits b + 1.

theorem Cslib.Circuits.Rational.intBits_emod_le_max (a b : ℤ) : intBits (a.emod b) ≤ max (intBits a) (intBits b)

Unconditionally on b (including b = 0), intBits (a.emod b) ≤ max (intBits a) (intBits b).

theorem Cslib.Circuits.Rational.intBits_modPowTwo_le (x : ℤ) (ℓ : ℕ) : intBits (x.modPowTwo ℓ) ≤ ℓ + 1

Reducing modulo 2 ^ ℓ produces an integer of sign-magnitude bit length at most ℓ + 1.

theorem Cslib.Circuits.Rational.natAbs_lt_of_mem_hermiteRows {nodes : List ℤ} {J b : ℕ} (hnodes : ∀ t ∈ nodes, t.natAbs < 2 ^ b) {row : List ℤ} (hrow : row ∈ hermiteRows nodes J) {z : ℤ} (hz : z ∈ row) : z.natAbs < 2 ^ (nodes.length * J * (b + 1))

If every node in nodes has magnitude below 2 ^ b, then every entry of hermiteRows nodes J has magnitude strictly below 2 ^ ((nodes.length * J) * (b + 1)).

theorem Cslib.Circuits.Rational.intBits_le_of_mem_hermiteRows {nodes : List ℤ} {J b : ℕ} (hnodes : ∀ t ∈ nodes, intBits t ≤ b + 1) {row : List ℤ} (hrow : row ∈ hermiteRows nodes J) {z : ℤ} (hz : z ∈ row) : intBits z ≤ nodes.length * J * (b + 1) + 1

Entry bit-length bound for hermiteRows: if every node has intBits t ≤ b + 1, then every entry z of hermiteRows nodes J satisfies intBits z ≤ (nodes.length * J) * (b + 1) + 1.

theorem Cslib.Circuits.Rational.intBits_le_of_mem_cramerColZeroRows {mat : List (List ℤ)} {rhs : List ℤ} {B : ℕ} (hmat : ∀ row ∈ mat, ∀ z ∈ row, intBits z ≤ B + 1) (hrhs : ∀ w ∈ rhs, intBits w ≤ B + 1) {row : List ℤ} (hrow : row ∈ cramerColZeroRows mat rhs) {z : ℤ} (hz : z ∈ row) : intBits z ≤ B + 1

Entry bit-length bound for cramerColZeroRows: replacing column 0 with rhs preserves any common bit-length bound on mat and rhs.

Plain polynomial-time certificates

theorem Cslib.Circuits.Rational.computableInPolyTime_hermiteRows {α : Type} {encIn : α ↪ List Bool} {nodes : α → List ℤ} {J : α → ℕ} (hnodes : Turing.MultiTapeTM.ComputableInPolyTime nodes encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => hermiteRows (nodes x) (J x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Constructing hermiteRows (nodes x) (J x) from binary integer nodes and a unary order J is computable in polynomial time.

theorem Cslib.Circuits.Rational.hermiteRows_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℤ × ℕ) => hermiteRows p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

hermiteRows is computable in polynomial time on encPair (encList encIntBin) encUnary.

theorem Cslib.Circuits.Rational.computableInPolyTime_cramerColZeroRows {α : Type} {encIn : α ↪ List Bool} {mat : α → List (List ℤ)} {rhs : α → List ℤ} (hmat : Turing.MultiTapeTM.ComputableInPolyTime mat encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (hrhs : Turing.MultiTapeTM.ComputableInPolyTime rhs encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => cramerColZeroRows (mat x) (rhs x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Replacing column 0 via cramerColZeroRows is computable in polynomial time.

theorem Cslib.Circuits.Rational.cramerColZeroRows_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (List ℤ) × List ℤ) => cramerColZeroRows p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

cramerColZeroRows is computable in polynomial time on pairs of integer matrix and RHS.

theorem Cslib.Circuits.Rational.computableInPolyTime_hermiteRecoverZero {α : Type} {encIn : α ↪ List Bool} {nodes : α → List ℤ} {J : α → ℕ} {Ω : α → ℤ} {jets : α → List (List ℤ)} (hnodes : Turing.MultiTapeTM.ComputableInPolyTime nodes encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hΩ : Turing.MultiTapeTM.ComputableInPolyTime Ω encIn Turing.MultiTapeTM.encIntBin) (hjets : Turing.MultiTapeTM.ComputableInPolyTime jets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => hermiteRecoverZero (nodes x) (J x) (Ω x) (jets x)) encIn Turing.MultiTapeTM.encIntBin

Confluent Hermite Cramer recovery hermiteRecoverZero is computable in polynomial time.

theorem Cslib.Circuits.Rational.hermiteRecoverZero_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : ((List ℤ × ℕ) × ℤ) × List (List ℤ)) => hermiteRecoverZero q.1.1.1 q.1.1.2 q.1.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) Turing.MultiTapeTM.encIntBin

Direct tuple certificate for hermiteRecoverZero over binary integers and unary order J.

theorem Cslib.Circuits.Rational.computableInPolyTime_hermiteRecoverModPowTwo {α : Type} {encIn : α ↪ List Bool} {nodes : α → List ℤ} {J ℓ : α → ℕ} {Ω : α → ℤ} {jets : α → List (List ℤ)} (hnodes : Turing.MultiTapeTM.ComputableInPolyTime nodes encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hΩ : Turing.MultiTapeTM.ComputableInPolyTime Ω encIn Turing.MultiTapeTM.encIntBin) (hjets : Turing.MultiTapeTM.ComputableInPolyTime jets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => hermiteRecoverModPowTwo (nodes x) (J x) (ℓ x) (Ω x) (jets x)) encIn Turing.MultiTapeTM.encIntBin

Modular confluent Hermite Cramer recovery hermiteRecoverModPowTwo is computable in polynomial time when J and ℓ are given in unary.

theorem Cslib.Circuits.Rational.hermiteRecoverModPowTwo_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : (((List ℤ × ℕ) × ℕ) × ℤ) × List (List ℤ)) => hermiteRecoverModPowTwo q.1.1.1.1 q.1.1.1.2 q.1.1.2 q.1.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encIntBin) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) Turing.MultiTapeTM.encIntBin

Direct tuple certificate for hermiteRecoverModPowTwo.

theorem Cslib.Circuits.Rational.computableInPolyTime_modPowTwo_sum_hermiteRecoverZero {α : Type} {encIn : α ↪ List Bool} {nodes : α → List ℤ} {J ℓ : α → ℕ} {Ω : α → ℤ} {coordJets : α → List (List (List ℤ))} (hnodes : Turing.MultiTapeTM.ComputableInPolyTime nodes encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) (hJ : Turing.MultiTapeTM.ComputableInPolyTime J encIn Turing.MultiTapeTM.encUnary) (hℓ : Turing.MultiTapeTM.ComputableInPolyTime ℓ encIn Turing.MultiTapeTM.encUnary) (hΩ : Turing.MultiTapeTM.ComputableInPolyTime Ω encIn Turing.MultiTapeTM.encIntBin) (hcoordJets : Turing.MultiTapeTM.ComputableInPolyTime coordJets encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : α) => (List.map (hermiteRecoverZero (nodes x) (J x) (Ω x)) (coordJets x)).sum.modPowTwo (ℓ x)) encIn Turing.MultiTapeTM.encIntBin

Recovering a coordinate sum ∑_s H_s(0) mod 2 ^ ℓ across a list of scaled jet tables sharing nodes, J, and Ω ([OAI26c], Appendix B.3) is computable in polynomial time.