Documentation

def Cslib.LinearAlgebra.decodeAuxDigits (Q r idx : ℕ) :

List ℕ × List ℕ

Decode idx in base r into two length-Q digit lists (u₁, u₂) via Cslib.Radix.digit. Total for all r, idx: extracts the low 2 * Q digits idx / r ^ i % r when idx ≥ r ^ (2 * Q) (0 digits at r = 1; at r = 0, slot 0 is idx when 0 < Q and higher slots are 0).

Instances For

def Cslib.LinearAlgebra.encodeAuxDigits (r : ℕ) (u : List ℕ × List ℕ) :

Pack a pair of base-r digit lists (u₁, u₂) into a natural number via Nat.ofDigits.

Instances For

def Cslib.LinearAlgebra.auxLabelToDigits {Q r : ℕ} (u : AuxLabel Q r) :

List ℕ × List ℕ

Convert u : AuxLabel Q r to its pair of length-Q natural-number digit lists.

Instances For

def Cslib.LinearAlgebra.encodeAuxLabel {Q r : ℕ} (u : AuxLabel Q r) :

Pack u : AuxLabel Q r into its mixed-radix index < r ^ (2 * Q).

Instances For

def Cslib.LinearAlgebra.decodeAuxLabel {Q r : ℕ} (hD : 0 < r ^ (2 * Q)) (idx : ℕ) :

AuxLabel Q r

Decode an index idx : ℕ into AuxLabel Q r whenever 0 < r ^ (2 * Q).

Instances For

@[simp]

theorem Cslib.LinearAlgebra.length_fst_decodeAuxDigits (Q r idx : ℕ) :

(decodeAuxDigits Q r idx).1.length = Q

First coordinate list of decodeAuxDigits Q r idx has length Q.

@[simp]

theorem Cslib.LinearAlgebra.length_snd_decodeAuxDigits (Q r idx : ℕ) :

(decodeAuxDigits Q r idx).2.length = Q

Second coordinate list of decodeAuxDigits Q r idx has length Q.

theorem Cslib.LinearAlgebra.mem_fst_decodeAuxDigits_lt {Q r idx a : ℕ} (hr : 1 ≤ r) (ha : a ∈ (decodeAuxDigits Q r idx).1) :

a < r

Every digit in (decodeAuxDigits Q r idx).1 is strictly less than r when 1 ≤ r.

theorem Cslib.LinearAlgebra.mem_snd_decodeAuxDigits_lt {Q r idx a : ℕ} (hr : 1 ≤ r) (ha : a ∈ (decodeAuxDigits Q r idx).2) :

a < r

Every digit in (decodeAuxDigits Q r idx).2 is strictly less than r when 1 ≤ r.

theorem Cslib.LinearAlgebra.encodeAuxDigits_lt {Q r : ℕ} {u : List ℕ × List ℕ} (hu₁ : u.1.length = Q) (hu₂ : u.2.length = Q) (hb₁ : ∀ a ∈ u.1, a < r) (hb₂ : ∀ a ∈ u.2, a < r) (hQr : Q = 0 ∨ 1 ≤ r) :

encodeAuxDigits r u < r ^ (2 * Q)

A pair of length-Q digit lists < r encodes below r ^ (2 * Q) when Q = 0 ∨ 1 ≤ r.

theorem Cslib.LinearAlgebra.decodeAuxDigits_encodeAuxDigits {Q r : ℕ} {u : List ℕ × List ℕ} (hu₁ : u.1.length = Q) (hu₂ : u.2.length = Q) (hb₁ : ∀ a ∈ u.1, a < r) (hb₂ : ∀ a ∈ u.2, a < r) :

decodeAuxDigits Q r (encodeAuxDigits r u) = u

Decoding encodeAuxDigits r u recovers u for every pair of length-Q digit lists < r.

theorem Cslib.LinearAlgebra.encodeAuxDigits_decodeAuxDigits {Q r idx : ℕ} (hidx : idx < r ^ (2 * Q)) :

encodeAuxDigits r (decodeAuxDigits Q r idx) = idx

Encoding decodeAuxDigits Q r idx recovers idx for every idx < r ^ (2 * Q).

@[simp]

theorem Cslib.LinearAlgebra.auxLabelToDigits_decodeAuxLabel {Q r : ℕ} (hD : 0 < r ^ (2 * Q)) (idx : ℕ) :

auxLabelToDigits (decodeAuxLabel hD idx) = decodeAuxDigits Q r idx

Converting decodeAuxLabel hD idx back to digits yields decodeAuxDigits Q r idx.

theorem Cslib.LinearAlgebra.encodeAuxLabel_lt {Q r : ℕ} (u : AuxLabel Q r) :

encodeAuxLabel u < r ^ (2 * Q)

Every u : AuxLabel Q r encodes to an index strictly less than r ^ (2 * Q).

@[simp]

theorem Cslib.LinearAlgebra.decodeAuxDigits_encodeAuxLabel {Q r : ℕ} (u : AuxLabel Q r) :

decodeAuxDigits Q r (encodeAuxLabel u) = auxLabelToDigits u

Decoding encodeAuxLabel u yields auxLabelToDigits u.

@[simp]

theorem Cslib.LinearAlgebra.decodeAuxLabel_encodeAuxLabel {Q r : ℕ} (hD : 0 < r ^ (2 * Q)) (u : AuxLabel Q r) :

decodeAuxLabel hD (encodeAuxLabel u) = u

Left-inverse identity for decodeAuxLabel and encodeAuxLabel.

@[simp]

theorem Cslib.LinearAlgebra.encodeAuxLabel_decodeAuxLabel {Q r idx : ℕ} (hD : 0 < r ^ (2 * Q)) (hidx : idx < r ^ (2 * Q)) :

encodeAuxLabel (decodeAuxLabel hD idx) = idx

Right-inverse identity for encodeAuxLabel and decodeAuxLabel on idx < r ^ (2 * Q).

def Cslib.LinearAlgebra.auxLabelEquivFin (Q r : ℕ) :

AuxLabel Q r ≃ Fin (r ^ (2 * Q))

Computable mixed-radix equivalence between AuxLabel Q r and Fin (r ^ (2 * Q)).

Instances For

2. Common denominator bit-length bounds (`commonDenom`) #

theorem Cslib.LinearAlgebra.size_commonDenom_le (Q R : ℕ) :

(commonDenom Q R).size ≤ (R - 1) * (R - 1).size + Q * Q.size + 2

Binary bit-length bound for commonDenom Q R = (R - 1)! * Q! (Lemma 4.6, p. 33).

theorem Cslib.LinearAlgebra.length_encIntBin_commonDenom_le (Q R : ℕ) :

(Turing.MultiTapeTM.encIntBin ↑(commonDenom Q R)).length ≤ (R - 1) * (R - 1).size + Q * Q.size + 3

Encoded encIntBin bit-length bound for (commonDenom Q R : ℤ).

3. Executable `{0, 1, -1}` measurement matrix `C^B` #

def Cslib.LinearAlgebra.pairBasisNat (α δ x y : ℕ) :

ℤ

Executable 1-slot {0, 1, -1} basis value on natural-number digits α δ x y : ℕ.

Instances For

def Cslib.LinearAlgebra.eigenvecDigits (Q : ℕ) (β u : List ℕ × List ℕ) :

ℤ

Executable {0, 1, -1} entry ψ_β(u) on digit lists β, u (missing digits read as 0).

Instances For

def Cslib.LinearAlgebra.antisymCountDigits (Q : ℕ) (β : List ℕ × List ℕ) :

Antisymmetric slot count #{s < Q | β.2[s] < β.1[s]} on digits β (missing digits 0).

Instances For

def Cslib.LinearAlgebra.auxMeasurementIndicesBounded (D_cap Q r A₀ R : ℕ) :

List ℕ

Measurement row indices outside Ico A₀ (A₀ + R), truncated to < min D_cap (r ^ (2 * Q)).

Instances For

def Cslib.LinearAlgebra.auxMeasurementIndices (Q r A₀ R : ℕ) :

List ℕ

Full list of measurement row indices < r ^ (2 * Q) outside Finset.Ico A₀ (A₀ + R).

Instances For

def Cslib.LinearAlgebra.auxMeasurementRowsBounded (D_cap Q r A₀ R : ℕ) :

List (List ℤ)

Executable {0, 1, -1} measurement matrix C^B truncated below min D_cap (r ^ (2 * Q)).

Instances For

def Cslib.LinearAlgebra.auxMeasurementRows (Q r A₀ R : ℕ) :

List (List ℤ)

Executable {0, 1, -1} measurement matrix C^B of Lemma 4.1 (p. 28).

Instances For

theorem Cslib.LinearAlgebra.pairBasisNat_mem (α δ x y : ℕ) :

pairBasisNat α δ x y = 0 ∨ pairBasisNat α δ x y = 1 ∨ pairBasisNat α δ x y = -1

Every value of pairBasisNat lies in {0, 1, -1}.

theorem Cslib.LinearAlgebra.eigenvecDigits_mem (Q : ℕ) (β u : List ℕ × List ℕ) :

eigenvecDigits Q β u = 0 ∨ eigenvecDigits Q β u = 1 ∨ eigenvecDigits Q β u = -1

Every entry of eigenvecDigits lies in {0, 1, -1}.

@[simp]

theorem Cslib.LinearAlgebra.eigenvecDigits_auxLabelToDigits {Q r : ℕ} (β u : AuxLabel Q r) :

eigenvecDigits Q (auxLabelToDigits β) (auxLabelToDigits u) = eigenvecInt β u

eigenvecDigits on auxLabelToDigits agrees identically with eigenvecInt.

@[simp]

theorem Cslib.LinearAlgebra.antisymCountDigits_auxLabelToDigits {Q r : ℕ} (β : AuxLabel Q r) :

antisymCountDigits Q (auxLabelToDigits β) = antisymCount β

antisymCountDigits on auxLabelToDigits agrees identically with antisymCount.

theorem Cslib.LinearAlgebra.auxMeasurementRowsBounded_eq_auxMeasurementRows {D_cap Q r A₀ R : ℕ} (h : r ^ (2 * Q) ≤ D_cap) :

auxMeasurementRowsBounded D_cap Q r A₀ R = auxMeasurementRows Q r A₀ R

When r ^ (2 * Q) ≤ D_cap, auxMeasurementRowsBounded equals auxMeasurementRows.

theorem Cslib.LinearAlgebra.decodeAuxLabel_mem_measurementIndices_iff {Q r A₀ R b_idx : ℕ} (hb : b_idx < r ^ (2 * Q)) :

decodeAuxLabel ⋯ b_idx ∈ measurementIndices Q r A₀ R ↔ b_idx ∈ auxMeasurementIndices Q r A₀ R

Characterization of membership in auxMeasurementIndices Q r A₀ R via measurementIndices.

theorem Cslib.LinearAlgebra.isTableShape_auxMeasurementRows (Q r A₀ R : ℕ) :

IsTableShape (measurementIndices Q r A₀ R).card (r ^ (2 * Q)) (auxMeasurementRows Q r A₀ R)

auxMeasurementRows Q r A₀ R is a #(measurementIndices Q r A₀ R) × r ^ (2 * Q) table.

theorem Cslib.LinearAlgebra.mem_auxMeasurementRowsBounded_mem {D_cap Q r A₀ R : ℕ} {row : List ℤ} {c : ℤ} (hrow : row ∈ auxMeasurementRowsBounded D_cap Q r A₀ R) (hc : c ∈ row) :

c = 0 ∨ c = 1 ∨ c = -1

Every entry of auxMeasurementRowsBounded D_cap Q r A₀ R belongs to {0, 1, -1}.

theorem Cslib.LinearAlgebra.abs_mem_auxMeasurementRowsBounded_le_one {D_cap Q r A₀ R : ℕ} {row : List ℤ} {c : ℤ} (hrow : row ∈ auxMeasurementRowsBounded D_cap Q r A₀ R) (hc : c ∈ row) :

|c| ≤ 1

Every entry of auxMeasurementRowsBounded D_cap Q r A₀ R has absolute value at most 1.

theorem Cslib.LinearAlgebra.rowEntry_auxMeasurementRows {Q r A₀ R i u_idx : ℕ} (hi : i < (auxMeasurementIndices Q r A₀ R).length) (hu : u_idx < r ^ (2 * Q)) :

rowEntry (auxMeasurementRows Q r A₀ R) i u_idx = eigenvecInt (decodeAuxLabel ⋯ (auxMeasurementIndices Q r A₀ R)[i]) (decodeAuxLabel ⋯ u_idx)

In-bounds entry correspondence (i < length, u_idx < r ^ (2 * Q)) between auxMeasurementRows and eigenvecInt via Cslib.rowEntry (0 out of bounds).

theorem Cslib.LinearAlgebra.measurementMatrix_mulVec_eq_zero_iff_auxMeasurementRows (Q r A₀ R : ℕ) (K : Type u_1) [CommRing K] (ξ : AuxLabel Q r → K) :

(measurementMatrix Q r A₀ R K).mulVec ξ = 0 ↔ ∀ row ∈ auxMeasurementRows Q r A₀ R, ∑ u : AuxLabel Q r, ↑(row.getD (encodeAuxLabel u) 0) * ξ u = 0

Kernel correspondence: ξ lies in ker (measurementMatrix Q r A₀ R K) iff its inner product with every row in auxMeasurementRows Q r A₀ R vanishes.

4. Executable cleared integer replacement rows (`auxReplacementRowCoeffs`) #

def Cslib.LinearAlgebra.isSwapOrbitDigits (Q : ℕ) (u y : List ℕ × List ℕ) :

Bool

Whether y lies in the swap orbit of (u.2, u.1) across slots < Q (missing digits 0).

Instances For

def Cslib.LinearAlgebra.offDiagCountDigits (Q : ℕ) (u : List ℕ × List ℕ) :

Number of off-diagonal slots s < Q where u.2[s] ≠ u.1[s] (missing digits read as 0).

Instances For

def Cslib.LinearAlgebra.mismatchCountDigits (Q : ℕ) (u y : List ℕ × List ℕ) :

Number of mismatch slots s < Q where y.1[s] ≠ u.2[s] (missing digits read as 0).

Instances For

def Cslib.LinearAlgebra.orbitWeightStep (m : ℕ) (c : ℤ) (f : List ℤ) :

One factor (2 W_0 - c I) on the (m + 1)-state Hamming-weight vector f of a swap orbit.

Instances For

def Cslib.LinearAlgebra.fallingOrbitWeights (m A₀ j : ℕ) :

Weight profile after multiplying ∏_{a < j} (2 W_0 - 2 (A₀ + a) I) on a swap orbit.

Instances For

def Cslib.LinearAlgebra.m0ScaledIntDigits (Q A₀ R : ℕ) (u y : List ℕ × List ℕ) :

ℤ

Executable (R - 1)! M_0[u, y] entry summing j < R runs of the (m + 1)-state 1D swap-orbit DP fallingOrbitWeights (0 at R = 0; missing digits read as 0).

Instances For

def Cslib.LinearAlgebra.mulLinearSub (p : List ℤ) (t : ℤ) :

Multiply a polynomial coefficient list p (constant term first) by (t - X).

Instances For

def Cslib.LinearAlgebra.mismatchAnnihilatorCoeffsDigits (Q : ℕ) (u y : List ℕ × List ℕ) :

Executable integer coefficient list of Q! φ_{u,y}(T) = mismatchAnnihilatorScaledInt u y (missing digits at slots s ≥ length read as 0).

Instances For

def Cslib.LinearAlgebra.eqAuxDigits (Q : ℕ) (u y : List ℕ × List ℕ) :

Bool

Whether two digit-list pairs agree on their first Q slots (missing digits read as 0).

Instances For

def Cslib.LinearAlgebra.auxReplacementRowCoeffsDigits (Q A₀ R : ℕ) (u y : List ℕ × List ℕ) :

Executable dense coefficient list (length max R 1) of d_den · P⃗_u(T)_y on digit lists, cleared by commonDenom Q R = (R - 1)! * Q! > 0 (at R = 0, (R - 1)! = 1 and length is 1; missing digits read as 0).

Instances For

def Cslib.LinearAlgebra.auxReplacementRowCoeffsIdx (Q r A₀ R u_idx y_idx : ℕ) :

Executable cleared integer replacement polynomial coefficients from mixed-radix indices.

Instances For

def Cslib.LinearAlgebra.auxReplacementRowCoeffs (Q r A₀ R : ℕ) (u y : AuxLabel Q r) :

Executable dense coefficient list (length max R 1) of auxReplacementRowScaledInt, cleared by commonDenom Q R = (R - 1)! * Q! > 0 (at R = 0, (R - 1)! = 1 and output length is 1).

Instances For

def Cslib.LinearAlgebra.auxReplacementTableBounded (D_cap Q r A₀ R : ℕ) :

List (List (List ℤ))

Executable D_len × D_len × max R 1 table of cleared replacement polynomials guarded by unary cap D_cap (truncating row and column indices to < D_len = min D_cap (r ^ (2 * Q))).

Instances For

def Cslib.LinearAlgebra.auxReplacementTable (Q r A₀ R : ℕ) :

List (List (List ℤ))

Full D × D × max R 1 table of cleared integer replacement polynomials.

Instances For

4.1 Correctness of the 1D swap-orbit DP for `M0ScaledInt` #

@[simp]

theorem Cslib.LinearAlgebra.m0ScaledIntDigits_auxLabelToDigits (Q r A₀ R : ℕ) (u y : AuxLabel Q r) :

m0ScaledIntDigits Q A₀ R (auxLabelToDigits u) (auxLabelToDigits y) = M0ScaledInt Q r A₀ R u y

m0ScaledIntDigits on auxLabelToDigits equals M0ScaledInt Q r A₀ R u y.

4.2 Correctness of `mismatchAnnihilatorCoeffsDigits` and `auxReplacementRowCoeffs` #

@[simp]

theorem Cslib.LinearAlgebra.ofCoeffList_mismatchAnnihilatorCoeffsDigits (Q r : ℕ) (u y : AuxLabel Q r) :

Polynomial.ofCoeffList (mismatchAnnihilatorCoeffsDigits Q (auxLabelToDigits u) (auxLabelToDigits y)) = mismatchAnnihilatorScaledInt u y

Reconstructing a polynomial from mismatchAnnihilatorCoeffsDigits yields mismatchAnnihilatorScaledInt u y.

@[simp]

theorem Cslib.LinearAlgebra.length_auxReplacementRowCoeffsDigits (Q A₀ R : ℕ) (u y : List ℕ × List ℕ) :

(auxReplacementRowCoeffsDigits Q A₀ R u y).length = max R 1

Length of auxReplacementRowCoeffsDigits is max R 1.

@[simp]

theorem Cslib.LinearAlgebra.length_auxReplacementRowCoeffs (Q r A₀ R : ℕ) (u y : AuxLabel Q r) :

(auxReplacementRowCoeffs Q r A₀ R u y).length = max R 1

Length of auxReplacementRowCoeffs is max R 1 (equal to R whenever 1 ≤ R).

theorem Cslib.LinearAlgebra.natDegree_mismatchAnnihilatorScaledInt_le {Q r : ℕ} (u y : AuxLabel Q r) :

(mismatchAnnihilatorScaledInt u y).natDegree ≤ (mismatchSet u y).card

Degree of mismatchAnnihilatorScaledInt u y is at most #(mismatchSet u y).

theorem Cslib.LinearAlgebra.getD_auxReplacementRowCoeffs (Q r A₀ R : ℕ) (u y : AuxLabel Q r) (k : ℕ) :

(auxReplacementRowCoeffs Q r A₀ R u y).getD k 0 = (auxReplacementRowScaledInt Q r A₀ R u y).coeff k

Exact coefficient equality between auxReplacementRowCoeffs and auxReplacementRowScaledInt.

@[simp]

theorem Cslib.LinearAlgebra.ofCoeffList_auxReplacementRowCoeffs (Q r A₀ R : ℕ) (u y : AuxLabel Q r) :

Polynomial.ofCoeffList (auxReplacementRowCoeffs Q r A₀ R u y) = auxReplacementRowScaledInt Q r A₀ R u y

Reconstructing a polynomial from auxReplacementRowCoeffs Q r A₀ R u y gives auxReplacementRowScaledInt Q r A₀ R u y unconditionally.

theorem Cslib.LinearAlgebra.auxReplacementTableBounded_eq_auxReplacementTable {D_cap Q r A₀ R : ℕ} (h : r ^ (2 * Q) ≤ D_cap) :

auxReplacementTableBounded D_cap Q r A₀ R = auxReplacementTable Q r A₀ R

When r ^ (2 * Q) ≤ D_cap, auxReplacementTableBounded equals auxReplacementTable.

theorem Cslib.LinearAlgebra.getD_auxReplacementTable {Q r A₀ R u_idx y_idx : ℕ} (hu : u_idx < r ^ (2 * Q)) (hy : y_idx < r ^ (2 * Q)) :

((auxReplacementTable Q r A₀ R).getD u_idx []).getD y_idx [] = auxReplacementRowCoeffs Q r A₀ R (decodeAuxLabel ⋯ u_idx) (decodeAuxLabel ⋯ y_idx)

Exact entry lookup in auxReplacementTable Q r A₀ R for u_idx, y_idx < r ^ (2 * Q).

4.3 Coefficient magnitude, `coeffNorm1` bridge, and bit-length bounds (Lemma 4.6) #

theorem Cslib.LinearAlgebra.natAbs_m0ScaledIntDigits_le (Q A₀ R : ℕ) (u y : List ℕ × List ℕ) :

(m0ScaledIntDigits Q A₀ R u y).natAbs ≤ (R - 1).factorial * R * (2 * (Q + A₀ + R)) ^ (R - 1)

Unconditional magnitude bound on m0ScaledIntDigits Q A₀ R u y.

theorem Cslib.LinearAlgebra.sum_natAbs_mismatchAnnihilatorCoeffsDigits_le (Q : ℕ) (u y : List ℕ × List ℕ) :

(List.map Int.natAbs (mismatchAnnihilatorCoeffsDigits Q u y)).sum ≤ 2 ^ Q * Q.factorial

Polynomial ℓ₁ bound ‖Q! φ_{u,y}‖₁ ≤ 2 ^ Q * Q! on mismatchAnnihilatorCoeffsDigits (Lemma 4.6, p. 33).

@[simp]

theorem Cslib.LinearAlgebra.sum_natAbs_auxReplacementRowCoeffs_eq_coeffNorm1 (Q r A₀ R : ℕ) (u y : AuxLabel Q r) :

(List.map Int.natAbs (auxReplacementRowCoeffs Q r A₀ R u y)).sum = (auxReplacementRowScaledInt Q r A₀ R u y).coeffNorm1

Exact equality between the list ℓ₁ sum of auxReplacementRowCoeffs and Polynomial.coeffNorm1 of auxReplacementRowScaledInt.

theorem Cslib.LinearAlgebra.natAbs_mem_auxReplacementRowCoeffsDigits_le {Q A₀ R : ℕ} {u y : List ℕ × List ℕ} {c : ℤ} (hc : c ∈ auxReplacementRowCoeffsDigits Q A₀ R u y) :

c.natAbs ≤ commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (2 * (Q + A₀ + R)) ^ (R - 1))

Unconditional magnitude bound on every coefficient of auxReplacementRowCoeffsDigits.

theorem Cslib.LinearAlgebra.length_encIntBin_mem_auxReplacementRowCoeffs_le {Q r A₀ R : ℕ} {u y : AuxLabel Q r} {c : ℤ} (hc : c ∈ auxReplacementRowCoeffs Q r A₀ R u y) :

(Turing.MultiTapeTM.encIntBin c).length ≤ (commonDenom Q R).size + Q + R.size + (R - 1) * (2 * (Q + A₀ + R)).size + 5

Explicit encIntBin bit-length bound for every coefficient of auxReplacementRowCoeffs (Lemma 4.6, p. 33).

theorem Cslib.LinearAlgebra.sum_row_natAbs_auxReplacementRowCoeffs_le {Q r A₀ R : ℕ} (hQ : 0 < Q) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (u : AuxLabel Q r) :

∑ y : AuxLabel Q r, (List.map Int.natAbs (auxReplacementRowCoeffs Q r A₀ R u y)).sum ≤ commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1))

Row-ℓ₁ coefficient bound (Lemma 4.6, p. 33): when 0 < Q and ∀ a < R - 1, A₀ + a ≤ Q, the sum of absolute values across row u of auxReplacementRowCoeffs is at most commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)).

5. Plain polynomial-time certificates (Lemma 4.7, p. 34) #

theorem Cslib.LinearAlgebra.computableInPolyTime_decodeAuxDigits {α : Type} {input : α ↪ List Bool} {Q r idx : α → ℕ} (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q input Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encNat) (hidx : Turing.MultiTapeTM.ComputableInPolyTime idx input Turing.MultiTapeTM.encNat) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => decodeAuxDigits (Q a) (r a) (idx a)) input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))

decodeAuxDigits is computable in polynomial time from unary Q and binary (r, idx).

theorem Cslib.LinearAlgebra.computableInPolyTime_encodeAuxDigits {α : Type} {input : α ↪ List Bool} {r : α → ℕ} {u : α → List ℕ × List ℕ} (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encNat) (hu : Turing.MultiTapeTM.ComputableInPolyTime u input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => encodeAuxDigits (r a) (u a)) input Turing.MultiTapeTM.encNat

encodeAuxDigits is computable in polynomial time from binary r and digit lists u.

theorem Cslib.LinearAlgebra.computableInPolyTime_commonDenom {α : Type} {input : α ↪ List Bool} {Q R : α → ℕ} (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q input Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R input Turing.MultiTapeTM.encUnary) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => commonDenom (Q a) (R a)) input Turing.MultiTapeTM.encNat

commonDenom Q R = (R - 1)! * Q! is computable in polynomial time from unary (Q, R).

theorem Cslib.LinearAlgebra.computableInPolyTime_commonDenom_int {α : Type} {input : α ↪ List Bool} {Q R : α → ℕ} (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q input Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R input Turing.MultiTapeTM.encUnary) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => ↑(commonDenom (Q a) (R a))) input Turing.MultiTapeTM.encIntBin

(commonDenom Q R : ℤ) is computable in polynomial time in encIntBin from unary (Q, R).

theorem Cslib.LinearAlgebra.computableInPolyTime_auxMeasurementRowsBounded {α : Type} {input : α ↪ List Bool} {D_cap Q r A₀ R : α → ℕ} (hD : Turing.MultiTapeTM.ComputableInPolyTime D_cap input Turing.MultiTapeTM.encUnary) (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q input Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encUnary) (hA₀ : Turing.MultiTapeTM.ComputableInPolyTime A₀ input Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R input Turing.MultiTapeTM.encUnary) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => auxMeasurementRowsBounded (D_cap a) (Q a) (r a) (A₀ a) (R a)) input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

auxMeasurementRowsBounded (C^B) is computable in polynomial time from unary (D_cap, Q, r, A₀, R).

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => auxReplacementRowCoeffsDigits (Q a) (A₀ a) (R a) (u a) (y a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

auxReplacementRowCoeffsDigits (d_den · P⃗_u(T)_y) is computable in polynomial time per (u, y) pair from unary (Q, A₀, R) and digit lists u, y.

theorem Cslib.LinearAlgebra.computableInPolyTime_auxReplacementRowCoeffsIdx {α : Type} {input : α ↪ List Bool} {Q r A₀ R u_idx y_idx : α → ℕ} (hQ : Turing.MultiTapeTM.ComputableInPolyTime Q input Turing.MultiTapeTM.encUnary) (hr : Turing.MultiTapeTM.ComputableInPolyTime r input Turing.MultiTapeTM.encNat) (hA₀ : Turing.MultiTapeTM.ComputableInPolyTime A₀ input Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R input Turing.MultiTapeTM.encUnary) (hu : Turing.MultiTapeTM.ComputableInPolyTime u_idx input Turing.MultiTapeTM.encNat) (hy : Turing.MultiTapeTM.ComputableInPolyTime y_idx input Turing.MultiTapeTM.encNat) :

Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => auxReplacementRowCoeffsIdx (Q a) (r a) (A₀ a) (R a) (u_idx a) (y_idx a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

auxReplacementRowCoeffsIdx is computable in polynomial time per (u_idx, y_idx) pair from unary (Q, A₀, R) and binary (r, u_idx, y_idx).