Polynomial-time variable copy placement and replacement-row pullback

Given a bounded-occurrence incidence family with auxiliary block-label indices u_e < D and variable indices v_e < n, Section 4.5 (p. 32) and Lemma 4.7 (pp. 33–34) of OpenAI, The Exponential Time Hypothesis is False assign each incidence a copy index c_e < h so that all pairs (c_e, u_e) are distinct, partition the variables into schedule groups S_{t,g} at step t, and pull back the {0, 1, -1} block measurement rows and cleared-denominator block replacement rows along ι : K^n → K^{h × D}. Parameterized over any blockMeas : List (List ℤ) and blockRepl : List (List (List ℤ)), this module proves all combinatorial, linear-algebraic, and ℓ₁-norm invariants and bridges to Complexity.Foundations.LinearAlgebra.VariableCopyPlacement. Generic copyEmbedExec over arbitrary K and x : ℕ → K serves as an unencoded semantic helper for the linear-map pullback and refinement bridges (with no tape encoding or complexity certificate), while plain Turing.MultiTapeTM.ComputableInPolyTime certificates cover the seven concrete integer/list routines (fiberRanks, flatPlacement, varGroupList, pullbackMeasurementRow, pullbackMeasurementMatrix, restrictGroupColumns, and pullbackReplacementRow).

Main definitions

• Cslib.LinearAlgebra.CopyPlacement.fiberRanks, Cslib.LinearAlgebra.CopyPlacement.flatPlacement, Cslib.LinearAlgebra.CopyPlacement.varGroupList, Cslib.LinearAlgebra.CopyPlacement.copyEmbedExec, Cslib.LinearAlgebra.CopyPlacement.pullbackMeasurementRow, Cslib.LinearAlgebra.CopyPlacement.pullbackMeasurementMatrix, Cslib.LinearAlgebra.CopyPlacement.restrictGroupColumns, Cslib.LinearAlgebra.CopyPlacement.pullbackReplacementRow.

Main results

• Cslib.LinearAlgebra.CopyPlacement.nodup_zip_fiberRanks, Cslib.LinearAlgebra.CopyPlacement.lt_of_mem_fiberRanks, Cslib.LinearAlgebra.CopyPlacement.biUnion_toFinset_varGroupList, Cslib.LinearAlgebra.CopyPlacement.isTableShape_pullbackReplacementRow, Cslib.LinearAlgebra.CopyPlacement.zipWith_mul_sum_pullbackMeasurementRow, Cslib.LinearAlgebra.CopyPlacement.sum_evalCoeffList_pullbackReplacementRow, Cslib.LinearAlgebra.CopyPlacement.getD_zero_pullbackReplacementRow, Cslib.LinearAlgebra.CopyPlacement.abs_zipWith_mul_sum_pullbackMeasurementRow_le, Cslib.LinearAlgebra.CopyPlacement.jetL1Norm_pullbackReplacementRow_le, Cslib.LinearAlgebra.CopyPlacement.sum_evalCoeffList_pullbackReplacementRow_eq_zero_of_kernel, Cslib.LinearAlgebra.CopyPlacement.getElem_fiberRanks_eq_fiberRank, Cslib.LinearAlgebra.CopyPlacement.getD_pullbackMeasurementRow_ofFn_eq_varMeasurementMatrix.

References

• OpenAI, The Exponential Time Hypothesis is False

Deterministic copy-index assignment (fiberRanks and flatPlacement)

def Cslib.LinearAlgebra.CopyPlacement.fiberRanks (labels : List ℕ) : List ℕ

Assign each incidence e < labels.length the number of earlier incidences < e carrying the same auxiliary block label labels[e], deterministically realizing e ↦ (c_e, u_e) from Section 4.5 (p. 32) and Lemma 4.7 of [OAI26c].

def Cslib.LinearAlgebra.CopyPlacement.flatPlacement (D : ℕ) (labels : List ℕ) : List ℕ

Flat slot index c_e * D + u_e pairing each copy index from fiberRanks labels with its auxiliary block-label index < D.

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.length_fiberRanks (labels : List ℕ) : (fiberRanks labels).length = labels.length

fiberRanks preserves the number of incidences.

theorem Cslib.LinearAlgebra.CopyPlacement.getElem_fiberRanks (labels : List ℕ) {e : ℕ} (he : e < (fiberRanks labels).length) : (fiberRanks labels)[e] = List.count labels[e] (List.take e labels)

Entry e of fiberRanks labels counts occurrences of labels[e] in labels.take e.

theorem Cslib.LinearAlgebra.CopyPlacement.getD_fiberRanks (labels : List ℕ) {e : ℕ} (he : e < labels.length) (d : ℕ) : (fiberRanks labels).getD e d = List.count (labels.getD e 0) (List.take e labels)

Defaulted lookup of fiberRanks labels at a valid incidence index e.

theorem Cslib.LinearAlgebra.CopyPlacement.getElem_fiberRanks_eq_fiberRank (labels : List ℕ) (e : Fin labels.length) : (fiberRanks labels)[↑e] = fiberRank (fun (i : Fin labels.length) => labels[i]) e

Entry e of fiberRanks labels agrees with Cslib.LinearAlgebra.fiberRank on Fin labels.length.

theorem Cslib.LinearAlgebra.CopyPlacement.nodup_zip_fiberRanks (labels : List ℕ) : ((fiberRanks labels).zip labels).Nodup

Unconditional injectivity of (fiberRanks labels).zip labels. Distinct incidence positions always receive distinct (copyIdx, blockLabel) pairs.

theorem Cslib.LinearAlgebra.CopyPlacement.fiberRanks_pair_ne_of_ne {labels : List ℕ} {e₁ e₂ : ℕ} (he₁ : e₁ < labels.length) (he₂ : e₂ < labels.length) (hne : e₁ ≠ e₂) : ((fiberRanks labels).getD e₁ 0, labels.getD e₁ 0) ≠ ((fiberRanks labels).getD e₂ 0, labels.getD e₂ 0)

Distinct valid incidence indices receive distinct (copyIdx, blockLabel) pairs.

theorem Cslib.LinearAlgebra.CopyPlacement.lt_of_mem_fiberRanks {labels : List ℕ} {h : ℕ} (hbound : ∀ (y : ℕ), List.count y labels ≤ h) {c : ℕ} (hc : c ∈ fiberRanks labels) : c < h

Copy-multiplicity bound. If every block label occurs at most h times in labels, then every copy index produced by fiberRanks labels is strictly less than h.

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.length_flatPlacement (D : ℕ) (labels : List ℕ) : (flatPlacement D labels).length = labels.length

flatPlacement preserves the number of incidences.

theorem Cslib.LinearAlgebra.CopyPlacement.nodup_flatPlacement {D : ℕ} {labels : List ℕ} (hD : ∀ u ∈ labels, u < D) : (flatPlacement D labels).Nodup

When all labels in labels lie below D, flatPlacement D labels is duplicate-free.

theorem Cslib.LinearAlgebra.CopyPlacement.lt_mul_of_mem_flatPlacement {D h : ℕ} {labels : List ℕ} (hD : ∀ u ∈ labels, u < D) (hbound : ∀ (y : ℕ), List.count y labels ≤ h) {s : ℕ} (hs : s ∈ flatPlacement D labels) : s < h * D

When all labels lie below D and each occurs at most h times, flat slots lie below h * D.

Executable variable-group partition (varGroupList)

def Cslib.LinearAlgebra.CopyPlacement.varGroupList (varSchedules : List (List ℕ)) (t g : ℕ) : List ℕ

Sorted list of variable indices v < varSchedules.length whose group index at evaluation step t equals g (S_{t,g} = {v ∈ [n] : a_v(t) = g} in Section 4.5, p. 32 of [OAI26c]). Schedule lists shorter than t + 1 default to group 0 via List.getD.

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.mem_varGroupList {varSchedules : List (List ℕ)} {t g v : ℕ} : v ∈ varGroupList varSchedules t g ↔ v < varSchedules.length ∧ (varSchedules.getD v []).getD t 0 = g

Membership in varGroupList varSchedules t g.

theorem Cslib.LinearAlgebra.CopyPlacement.pairwise_lt_varGroupList (varSchedules : List (List ℕ)) (t g : ℕ) : List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (varGroupList varSchedules t g)

varGroupList is strictly increasing.

theorem Cslib.LinearAlgebra.CopyPlacement.nodup_varGroupList (varSchedules : List (List ℕ)) (t g : ℕ) : (varGroupList varSchedules t g).Nodup

varGroupList contains no duplicate variable indices.

theorem Cslib.LinearAlgebra.CopyPlacement.disjoint_toFinset_varGroupList (varSchedules : List (List ℕ)) (t : ℕ) {g₁ g₂ : ℕ} (hne : g₁ ≠ g₂) : Disjoint (varGroupList varSchedules t g₁).toFinset (varGroupList varSchedules t g₂).toFinset

Distinct groups g₁ ≠ g₂ at step t yield disjoint variable sets.

theorem Cslib.LinearAlgebra.CopyPlacement.biUnion_toFinset_varGroupList {varSchedules : List (List ℕ)} {t r : ℕ} (hsched : ∀ v < varSchedules.length, (varSchedules.getD v []).getD t 0 < r) : ((Finset.range r).biUnion fun (g : ℕ) => (varGroupList varSchedules t g).toFinset) = Finset.range varSchedules.length

When every variable's schedule value at step t lies in 0, …, r - 1, the groups varGroupList varSchedules t g for g < r partition Finset.range varSchedules.length.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_length_varGroupList {varSchedules : List (List ℕ)} {t r : ℕ} (hsched : ∀ v < varSchedules.length, (varSchedules.getD v []).getD t 0 < r) : ∑ g ∈ Finset.range r, (varGroupList varSchedules t g).length = varSchedules.length

Exact cardinality partition: the lengths of varGroupList varSchedules t g across g < r sum to varSchedules.length.

theorem Cslib.LinearAlgebra.CopyPlacement.mem_varGroupList_iff_mem_varGroup {n Q r : ℕ} {varSchedules : List (List ℕ)} {a : Fin n → Fin Q → Fin r} (hlen : varSchedules.length = n) (ha : ∀ (v : Fin n) (t : Fin Q), (varSchedules.getD ↑v []).getD (↑t) 0 = ↑(a v t)) (t : Fin Q) (g : Fin r) (v : Fin n) : ↑v ∈ varGroupList varSchedules ↑t ↑g ↔ v ∈ varGroup a t g

varGroupList agrees with Cslib.LinearAlgebra.varGroup whenever varSchedules encodes a : Fin n → Fin Q → Fin r.

Executable copy-embedding and pullback of measurement and replacement rows

def Cslib.LinearAlgebra.CopyPlacement.copyEmbedExec {K : Type u_1} [AddCommMonoid K] (placements : List (ℕ × ℕ)) (incVars : List ℕ) (x : ℕ → K) (copyIdx y : ℕ) : K

Executable copy-embedding coordinate (ι x)_{copyIdx, y} from Section 4.5 (p. 32) of [OAI26c], pairing placements with incVars via List.zip (truncating to min placements.length incVars.length) and summing x v over records ((c_e, u_e), v_e) with c_e = copyIdx and u_e = y.

def Cslib.LinearAlgebra.CopyPlacement.pullbackMeasurementRow (n : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (copyIdx : ℕ) (auxRow : List ℤ) : List ℤ

Pull back a single auxiliary measurement row auxRow : List ℤ in copy copyIdx to a length-n integer row over the original variables ((π_{copyIdx} ι)^⊤ auxRow), pairing placements with incVars via List.zip and defaulting out-of-range block indices u_e ≥ auxRow.length to 0.

def Cslib.LinearAlgebra.CopyPlacement.pullbackMeasurementMatrix (n h : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (blockMeas : List (List ℤ)) : List (List ℤ)

Pull back a block measurement matrix blockMeas : List (List ℤ) across h copies to form the (h * blockMeas.length) × n integer matrix Ĉ = C̃ ι of equation (4.15) in [OAI26c].

def Cslib.LinearAlgebra.CopyPlacement.restrictGroupColumns (groupVars : List ℕ) (mat : List (List ℤ)) : List (List ℤ)

Restrict each row of an integer matrix mat to the columns indexed by groupVars, forming the submatrix C_{t,g} = Ĉ|_{S_{t,g}} of equation (4.15) in [OAI26c]; out-of-range column indices v ≥ row.length default to 0.

def Cslib.LinearAlgebra.CopyPlacement.pullbackReplacementRow (n R : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (e : ℕ) (blockRepl : List (List (List ℤ))) : List (List ℤ)

Pull back the cleared-denominator replacement row of incidence e ((c_e, u_e) in placements) from a D × D × R integer polynomial table blockRepl to an n × R table via Cslib.tabulateTable computing d_den • P⃗_{f,v}(T) = d_den • P⃗_{u_{f,v}}(T) π_{c(f,v)} ι (equation (4.14), p. 32 and Lemmas 4.6–4.7, pp. 33–34 of [OAI26c]). Pairs placements with incVars via List.zip, defaulting missing e, u_e, or (y, k) lookups to (0, 0), [], and 0 (Cslib.rowEntry).

Dimensions, IsTableShape certificates, slices, and sum-over-zip helpers

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.length_pullbackMeasurementRow (n : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (copyIdx : ℕ) (auxRow : List ℤ) : (pullbackMeasurementRow n placements incVars copyIdx auxRow).length = n

pullbackMeasurementRow produces a row of length n.

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.length_pullbackMeasurementMatrix (n h : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (blockMeas : List (List ℤ)) : (pullbackMeasurementMatrix n h placements incVars blockMeas).length = h * blockMeas.length

pullbackMeasurementMatrix produces h * blockMeas.length rows.

theorem Cslib.LinearAlgebra.CopyPlacement.length_row_of_mem_pullbackMeasurementMatrix {n h : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {blockMeas : List (List ℤ)} {row : List ℤ} (hrow : row ∈ pullbackMeasurementMatrix n h placements incVars blockMeas) : row.length = n

Every row of pullbackMeasurementMatrix has length n.

theorem Cslib.LinearAlgebra.CopyPlacement.isTableShape_pullbackMeasurementMatrix (n h : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (blockMeas : List (List ℤ)) : IsTableShape (h * blockMeas.length) n (pullbackMeasurementMatrix n h placements incVars blockMeas)

pullbackMeasurementMatrix has rectangular table shape (h * blockMeas.length) × n.

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.length_restrictGroupColumns (groupVars : List ℕ) (mat : List (List ℤ)) : (restrictGroupColumns groupVars mat).length = mat.length

restrictGroupColumns preserves the number of rows.

theorem Cslib.LinearAlgebra.CopyPlacement.length_row_of_mem_restrictGroupColumns {groupVars : List ℕ} {mat : List (List ℤ)} {row : List ℤ} (hrow : row ∈ restrictGroupColumns groupVars mat) : row.length = groupVars.length

Every row of restrictGroupColumns groupVars mat has length groupVars.length.

theorem Cslib.LinearAlgebra.CopyPlacement.isTableShape_restrictGroupColumns (groupVars : List ℕ) (mat : List (List ℤ)) : IsTableShape mat.length groupVars.length (restrictGroupColumns groupVars mat)

restrictGroupColumns groupVars mat has rectangular table shape mat.length × groupVars.length.

@[simp]

theorem Cslib.LinearAlgebra.CopyPlacement.length_pullbackReplacementRow (n R : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (e : ℕ) (blockRepl : List (List (List ℤ))) : (pullbackReplacementRow n R placements incVars e blockRepl).length = n

pullbackReplacementRow produces n polynomial entries.

theorem Cslib.LinearAlgebra.CopyPlacement.length_coeff_of_mem_pullbackReplacementRow {n R : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {e : ℕ} {blockRepl : List (List (List ℤ))} {poly : List ℤ} (hpoly : poly ∈ pullbackReplacementRow n R placements incVars e blockRepl) : poly.length = R

Every polynomial entry in pullbackReplacementRow has length R.

theorem Cslib.LinearAlgebra.CopyPlacement.isTableShape_pullbackReplacementRow (n R : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (e : ℕ) (blockRepl : List (List (List ℤ))) : IsTableShape n R (pullbackReplacementRow n R placements incVars e blockRepl)

pullbackReplacementRow has rectangular table shape n × R.

theorem Cslib.LinearAlgebra.CopyPlacement.map_coeff_pullbackReplacementRow (n R : ℕ) (placements : List (ℕ × ℕ)) (incVars : List ℕ) (e : ℕ) (blockRepl : List (List (List ℤ))) {k : ℕ} (hk : k < R) : List.map (fun (poly : List ℤ) => poly.getD k 0) (pullbackReplacementRow n R placements incVars e blockRepl) = pullbackMeasurementRow n placements incVars (placements.getD e (0, 0)).1 (List.map (fun (poly : List ℤ) => poly.getD k 0) (blockRepl.getD (placements.getD e (0, 0)).2 []))

Extracting degree-k coefficients (k < R) across pullbackReplacementRow coincides with pullbackMeasurementRow applied to the degree-k coefficient slice of blockRepl[u_e].

theorem Cslib.LinearAlgebra.CopyPlacement.copyEmbedExec_eq_of_nodup {K : Type u_1} [AddCommMonoid K] {placements : List (ℕ × ℕ)} {incVars : List ℕ} (hnodup : placements.Nodup) (x : ℕ → K) {e : ℕ} (he : e < min placements.length incVars.length) : copyEmbedExec placements incVars x (placements.getD e (0, 0)).1 (placements.getD e (0, 0)).2 = x (incVars.getD e 0)

When placements.Nodup, the copy-embedding at an occupied slot placements[e] equals x (incVars[e]), matching the piecewise definition on p. 32 of [OAI26c].

theorem Cslib.LinearAlgebra.CopyPlacement.copyEmbedExec_eq_zero_of_forall_ne {K : Type u_1} [AddCommMonoid K] {placements : List (ℕ × ℕ)} {incVars : List ℕ} (x : ℕ → K) {copyIdx y : ℕ} (hunocc : ∀ p ∈ placements, p ≠ (copyIdx, y)) : copyEmbedExec placements incVars x copyIdx y = 0

At any unoccupied slot (copyIdx, y) ∉ placements, copyEmbedExec vanishes.

Exact linear-map pullback semantics

theorem Cslib.LinearAlgebra.CopyPlacement.sum_pullbackMeasurementRow_mul {K : Type u_1} [CommRing K] {n D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} (hvars : ∀ v ∈ incVars, v < n) (hD : ∀ p ∈ placements, p.2 < D) (copyIdx : ℕ) (auxRow : List ℤ) (x : ℕ → K) : ∑ v ∈ Finset.range n, ↑((pullbackMeasurementRow n placements incVars copyIdx auxRow).getD v 0) * x v = ∑ y ∈ Finset.range D, ↑(auxRow.getD y 0) * copyEmbedExec placements incVars x copyIdx y

Linear-map pullback semantics over any commutative ring. When all incidence variables lie below n (∀ v ∈ incVars, v < n) and all placed block labels lie below D (∀ p ∈ placements, p.2 < D), evaluating pullbackMeasurementRow against x : ℕ → K on 0, …, n - 1 equals evaluating auxRow against copyEmbedExec placements incVars x copyIdx on 0, …, D - 1.

theorem Cslib.LinearAlgebra.CopyPlacement.zipWith_mul_sum_pullbackMeasurementRow {n D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} (hvars : ∀ v ∈ incVars, v < n) (hD : ∀ p ∈ placements, p.2 < D) (copyIdx : ℕ) (auxRow : List ℤ) (x : ℕ → ℤ) : (List.zipWith (fun (x1 x2 : ℤ) => x1 * x2) (pullbackMeasurementRow n placements incVars copyIdx auxRow) (List.map x (List.range n))).sum = (List.zipWith (fun (x1 x2 : ℤ) => x1 * x2) auxRow (List.map (copyEmbedExec placements incVars x copyIdx) (List.range D))).sum

Integer dot-product pullback semantics. When ∀ v ∈ incVars, v < n and ∀ p ∈ placements, p.2 < D, for any x : ℕ → ℤ, the dot product of pullbackMeasurementRow with (List.range n).map x equals the dot product of auxRow with (List.range D).map (copyEmbedExec placements incVars x copyIdx).

theorem Cslib.LinearAlgebra.CopyPlacement.sum_evalCoeffList_pullbackReplacementRow {K : Type u_1} [CommRing K] {n R D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {e : ℕ} {blockRepl : List (List (List ℤ))} (hvars : ∀ v ∈ incVars, v < n) (hD : ∀ p ∈ placements, p.2 < D) (hdeg : ∀ poly ∈ blockRepl.getD (placements.getD e (0, 0)).2 [], poly.length ≤ R) (t : K) (x : ℕ → K) : ∑ v ∈ Finset.range n, Polynomial.evalCoeffList t (List.map Int.cast ((pullbackReplacementRow n R placements incVars e blockRepl).getD v [])) * x v = ∑ y ∈ Finset.range D, Polynomial.evalCoeffList t (List.map Int.cast ((blockRepl.getD (placements.getD e (0, 0)).2 []).getD y [])) * copyEmbedExec placements incVars x (placements.getD e (0, 0)).1 y

Replacement-row polynomial pullback semantics. When ∀ v ∈ incVars, v < n, ∀ p ∈ placements, p.2 < D, and every polynomial coefficient list in row u_e of blockRepl has length ≤ R, evaluating pullbackReplacementRow at t via Polynomial.evalCoeffList against x : ℕ → K equals evaluating row u_e of blockRepl at t against copyEmbedExec placements incVars x c_e.

Exact T = 0 variable-restoration theorem

theorem Cslib.LinearAlgebra.CopyPlacement.getD_zero_pullbackReplacementRow {n R : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {e : ℕ} {blockRepl : List (List (List ℤ))} {d_den : ℤ} (hR : 0 < R) (hnodup : placements.Nodup) (he : e < min placements.length incVars.length) (hzero : ∀ p ∈ placements, rowEntry (blockRepl.getD (placements.getD e (0, 0)).2 []) p.2 0 = if (placements.getD e (0, 0)).2 = p.2 then d_den else 0) {v : ℕ} (hv : v < n) : rowEntry (pullbackReplacementRow n R placements incVars e blockRepl) v 0 = if v = incVars.getD e 0 then d_den else 0

Constant-term (T = 0) variable restoration. When 0 < R, placements.Nodup, e < min placements.length incVars.length, and row u_e of blockRepl has constant coefficient (Cslib.rowEntry _ p.2 0) equal to d_den • δ_{u_e, p.2} at every placed label p ∈ placements, the constant coefficient Cslib.rowEntry (pullbackReplacementRow ...) v 0 at variable v < n equals d_den • δ_{v, incVars[e]}.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_evalCoeffList_pullbackReplacementRow_zero {K : Type u_1} [CommRing K] {n R : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {e : ℕ} {blockRepl : List (List (List ℤ))} {d_den : ℤ} (hR : 0 < R) (hnodup : placements.Nodup) (he : e < min placements.length incVars.length) (hvars : ∀ v ∈ incVars, v < n) (hzero : ∀ p ∈ placements, rowEntry (blockRepl.getD (placements.getD e (0, 0)).2 []) p.2 0 = if (placements.getD e (0, 0)).2 = p.2 then d_den else 0) (x : ℕ → K) : ∑ v ∈ Finset.range n, Polynomial.evalCoeffList 0 (List.map Int.cast ((pullbackReplacementRow n R placements incVars e blockRepl).getD v [])) * x v = ↑d_den * x (incVars.getD e 0)

When 0 < R, placements.Nodup, e < min placements.length incVars.length, ∀ v ∈ incVars, v < n, and hzero holds on placements, evaluating pullbackReplacementRow at T = 0 restores (d_den : K) * x (incVars.getD e 0).

Row ℓ₁-norm preservation and Boolean evaluation bounds

theorem Cslib.LinearAlgebra.CopyPlacement.sum_abs_pullbackMeasurementRow_le {n D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} (hnodup : placements.Nodup) (hD : ∀ p ∈ placements, p.2 < D) (copyIdx : ℕ) (auxRow : List ℤ) : ∑ v ∈ Finset.range n, |(pullbackMeasurementRow n placements incVars copyIdx auxRow).getD v 0| ≤ ∑ y ∈ Finset.range D, |auxRow.getD y 0|

Row ℓ₁-norm preservation (§4.5, eq. (4.15) and Lemma 4.6). When placements.Nodup and every placed block label lies below D, pulling back auxRow does not increase its ℓ₁-norm: ∑_{v < n} |row[v]| ≤ ∑_{y < D} |auxRow[y]|.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_natAbs_pullbackMeasurementRow_le {n : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {auxRow : List ℤ} (hnodup : placements.Nodup) (hD : ∀ p ∈ placements, p.2 < auxRow.length) (copyIdx : ℕ) : (List.map Int.natAbs (pullbackMeasurementRow n placements incVars copyIdx auxRow)).sum ≤ (List.map Int.natAbs auxRow).sum

Executable Int.natAbs-sum form of sum_abs_pullbackMeasurementRow_le when placements.Nodup and ∀ p ∈ placements, p.2 < auxRow.length.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_abs_pullbackMeasurementRow_le_of_abs_le_one {n D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} (hnodup : placements.Nodup) (hD : ∀ p ∈ placements, p.2 < D) {auxRow : List ℤ} (haux : ∀ z ∈ auxRow, |z| ≤ 1) (copyIdx : ℕ) : ∑ v ∈ Finset.range n, |(pullbackMeasurementRow n placements incVars copyIdx auxRow).getD v 0| ≤ ↑D

When placements.Nodup, ∀ p ∈ placements, p.2 < D, and every entry of auxRow lies in [-1, 1] (in particular {0, 1, -1}), the ℓ₁-norm of pullbackMeasurementRow is at most D.

theorem Cslib.LinearAlgebra.CopyPlacement.abs_zipWith_mul_sum_pullbackMeasurementRow_le {n D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} (hnodup : placements.Nodup) (hD : ∀ p ∈ placements, p.2 < D) {auxRow : List ℤ} (haux : ∀ z ∈ auxRow, |z| ≤ 1) (copyIdx : ℕ) {x : ℕ → ℤ} (hx : ∀ v < n, |x v| ≤ 1) : |(List.zipWith (fun (x1 x2 : ℤ) => x1 * x2) (pullbackMeasurementRow n placements incVars copyIdx auxRow) (List.map x (List.range n))).sum| ≤ ↑D

Boolean evaluation bound in [-D, D] (equation (4.15) of [OAI26c]). When placements.Nodup, ∀ p ∈ placements, p.2 < D, ∀ z ∈ auxRow, |z| ≤ 1, and ∀ v < n, |x v| ≤ 1 (in particular any Boolean vector x ∈ {0, 1}^n), the inner product of pullbackMeasurementRow with x lies in [-D, D].

theorem Cslib.LinearAlgebra.CopyPlacement.sum_natAbs_restrictGroupRow_le {groupVars : List ℕ} (hnodup : groupVars.Nodup) (row : List ℤ) : (List.map Int.natAbs (List.map (fun (v : ℕ) => row.getD v 0) groupVars)).sum ≤ (List.map Int.natAbs row).sum

Column restriction to a duplicate-free subset groupVars does not increase row ℓ₁-norm.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_abs_pullbackReplacementRow_le {n R D : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {e : ℕ} {blockRepl : List (List (List ℤ))} (hnodup : placements.Nodup) (hD : ∀ p ∈ placements, p.2 < D) : ∑ v ∈ Finset.range n, ∑ k ∈ Finset.range R, |rowEntry (pullbackReplacementRow n R placements incVars e blockRepl) v k| ≤ ∑ y ∈ Finset.range D, ∑ k ∈ Finset.range R, |rowEntry (blockRepl.getD (placements.getD e (0, 0)).2 []) y k|

Total polynomial ℓ₁ preservation for pullbackReplacementRow (Lemma 4.6 of [OAI26c]). When placements.Nodup and ∀ p ∈ placements, p.2 < D, the sum across all variables v < n and degrees k < R of |Cslib.rowEntry (pullbackReplacementRow ...) v k| is at most the corresponding sum across y < D of row u_e in blockRepl.

theorem Cslib.LinearAlgebra.CopyPlacement.jetL1Norm_pullbackReplacementRow_le {n R : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {e : ℕ} {blockRepl : List (List (List ℤ))} (hnodup : placements.Nodup) : jetL1Norm (pullbackReplacementRow n R placements incVars e blockRepl) ≤ jetL1Norm (blockRepl.getD (placements.getD e (0, 0)).2 [])

Cslib.jetL1Norm preservation for pullbackReplacementRow. When placements.Nodup, the executable ℓ₁ table norm Cslib.jetL1Norm of pullbackReplacementRow is at most that of row u_e in blockRepl.

Group-separation kernel transfer

theorem Cslib.LinearAlgebra.CopyPlacement.sum_restrictGroupRow_mul {K : Type u_1} [CommRing K] {groupVars : List ℕ} {row : List ℤ} {x : ℕ → K} (hnodup : groupVars.Nodup) (hvars : ∀ v ∈ groupVars, v < row.length) (hsupp : ∀ v < row.length, v ∉ groupVars → x v = 0) : ∑ j ∈ Finset.range groupVars.length, ↑((List.map (fun (v : ℕ) => row.getD v 0) groupVars).getD j 0) * x (groupVars.getD j 0) = ∑ v ∈ Finset.range row.length, ↑(row.getD v 0) * x v

When groupVars.Nodup, ∀ v ∈ groupVars, v < row.length, and x vanishes below row.length outside groupVars, evaluating the restricted row against x on groupVars agrees with evaluating row against x on 0, …, row.length - 1.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_copyEmbedExec_eq_zero_of_restrict_kernel {K : Type u_1} [CommRing K] {n h D : ℕ} {groupVars : List ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {blockMeas : List (List ℤ)} {x : ℕ → K} (hnodup : groupVars.Nodup) (hgroup : ∀ v ∈ groupVars, v < n) (hinc : ∀ v ∈ incVars, v < n) (hD : ∀ p ∈ placements, p.2 < D) (hsupp : ∀ v < n, v ∉ groupVars → x v = 0) (hker : ∀ r ∈ restrictGroupColumns groupVars (pullbackMeasurementMatrix n h placements incVars blockMeas), ∑ j ∈ Finset.range groupVars.length, ↑(r.getD j 0) * x (groupVars.getD j 0) = 0) {copyIdx : ℕ} (hcopy : copyIdx < h) {auxRow : List ℤ} (haux : auxRow ∈ blockMeas) : ∑ y ∈ Finset.range D, ↑(auxRow.getD y 0) * copyEmbedExec placements incVars x copyIdx y = 0

Kernel transfer from restrictGroupColumns to blockMeas (C^B (π_c ι ξ̃) = 0, p. 32 of [OAI26c]). When groupVars.Nodup, ∀ v ∈ groupVars, v < n, ∀ v ∈ incVars, v < n, ∀ p ∈ placements, p.2 < D, x vanishes below n outside groupVars, and its restriction lies in the kernel of restrictGroupColumns groupVars (pullbackMeasurementMatrix ...), every copyIdx < h and auxRow ∈ blockMeas annihilates copyEmbedExec placements incVars x copyIdx.

theorem Cslib.LinearAlgebra.CopyPlacement.copyEmbedExec_eq_zero_of_ne_group {K : Type u_1} [AddCommMonoid K] {varSchedules : List (List ℕ)} {t g : ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {x : ℕ → K} {copyIdx y labelGroup : ℕ} (hinc : ∀ v ∈ incVars, v < varSchedules.length) (hsupp : ∀ v < varSchedules.length, v ∉ varGroupList varSchedules t g → x v = 0) (hcompat : ∀ e < min placements.length incVars.length, placements.getD e (0, 0) = (copyIdx, y) → (varSchedules.getD (incVars.getD e 0) []).getD t 0 = labelGroup) (hne : labelGroup ≠ g) : copyEmbedExec placements incVars x copyIdx y = 0

Support separation under copy embedding. When ∀ v ∈ incVars, v < varSchedules.length, x vanishes below varSchedules.length outside varGroupList varSchedules t g, and every incidence e < min placements.length incVars.length placed at (copyIdx, y) has step-t schedule value labelGroup ≠ g, copyEmbedExec placements incVars x copyIdx y = 0.

theorem Cslib.LinearAlgebra.CopyPlacement.sum_evalCoeffList_pullbackReplacementRow_eq_zero_of_kernel {K : Type u_1} [CommRing K] {n h R D : ℕ} {groupVars : List ℕ} {placements : List (ℕ × ℕ)} {incVars : List ℕ} {blockMeas : List (List ℤ)} {blockRepl : List (List (List ℤ))} {e : ℕ} {t : K} {x : ℕ → K} {badY : ℕ → Prop} (hnodup : groupVars.Nodup) (hgroup : ∀ v ∈ groupVars, v < n) (hinc : ∀ v ∈ incVars, v < n) (hD : ∀ p ∈ placements, p.2 < D) (hcopy : (placements.getD e (0, 0)).1 < h) (hdeg : ∀ poly ∈ blockRepl.getD (placements.getD e (0, 0)).2 [], poly.length ≤ R) (hsupp : ∀ v < n, v ∉ groupVars → x v = 0) (hker : ∀ r ∈ restrictGroupColumns groupVars (pullbackMeasurementMatrix n h placements incVars blockMeas), ∑ j ∈ Finset.range groupVars.length, ↑(r.getD j 0) * x (groupVars.getD j 0) = 0) (havoid : ∀ y < D, badY y → copyEmbedExec placements incVars x (placements.getD e (0, 0)).1 y = 0) (hblockAnn : ∀ (η : ℕ → K), (∀ auxRow ∈ blockMeas, ∑ y ∈ Finset.range D, ↑(auxRow.getD y 0) * η y = 0) → (∀ y < D, badY y → η y = 0) → ∑ y ∈ Finset.range D, Polynomial.evalCoeffList t (List.map Int.cast ((blockRepl.getD (placements.getD e (0, 0)).2 []).getD y [])) * η y = 0) : ∑ v ∈ Finset.range n, Polynomial.evalCoeffList t (List.map Int.cast ((pullbackReplacementRow n R placements incVars e blockRepl).getD v [])) * x v = 0

End-to-end replacement-row kernel-orthogonality transfer (Section 4.5, p. 32 and Lemma 4.7, p. 34 of [OAI26c]). Under groupVars.Nodup, ∀ v ∈ groupVars, v < n, ∀ v ∈ incVars, v < n, ∀ p ∈ placements, p.2 < D, (placements.getD e (0, 0)).1 < h, and row u_e polynomial lengths ≤ R, if x : ℕ → K is supported on groupVars, lies in the restricted kernel of pullbackMeasurementMatrix, has copyEmbedExec ... c_e vanishing on badY below D, and row u_e annihilates at t every blockMeas-kernel vector avoiding badY, then evaluating pullbackReplacementRow at t against x yields 0.

Specification bridges to Foundations.LinearAlgebra.VariableCopyPlacement

theorem Cslib.LinearAlgebra.CopyPlacement.copyEmbedExec_ofFn_eq_copyProj_copyEmbed {M n h Q r : ℕ} {K : Type u_1} [AddCommMonoid K] (place : Fin M → Fin h × AuxLabel Q r) (varOf : Fin M → Fin n) {code : AuxLabel Q r → ℕ} (hcode : Function.Injective code) (x : Fin n → K) (xExec : ℕ → K) (hx : ∀ (v : Fin n), xExec ↑v = x v) (c : Fin h) (u : AuxLabel Q r) : copyEmbedExec (List.ofFn fun (e : Fin M) => (↑(place e).1, code (place e).2)) (List.ofFn fun (e : Fin M) => ↑(varOf e)) xExec (↑c) (code u) = copyProj c (copyEmbed place varOf x) u

copyEmbedExec agrees with Cslib.LinearAlgebra.copyProj ∘ Cslib.LinearAlgebra.copyEmbed under any injective integer encoding code of AuxLabel Q r.

theorem Cslib.LinearAlgebra.CopyPlacement.getD_pullbackMeasurementRow_ofFn_eq_varMeasurementMatrix {M n h Q r A₀ R : ℕ} (place : Fin M → Fin h × AuxLabel Q r) (varOf : Fin M → Fin n) (code : AuxLabel Q r → ℕ) (auxRow : List ℤ) (c : Fin h) (β : ↥(measurementIndices Q r A₀ R)) (hrow : ∀ (u : AuxLabel Q r), auxRow.getD (code u) 0 = measurementMatrix Q r A₀ R ℤ β u) (v : Fin n) : (pullbackMeasurementRow n (List.ofFn fun (e : Fin M) => (↑(place e).1, code (place e).2)) (List.ofFn fun (e : Fin M) => ↑(varOf e)) (↑c) auxRow).getD (↑v) 0 = varMeasurementMatrix Q r A₀ R ℤ place varOf (c, β) v

Entry v of pullbackMeasurementRow agrees with Cslib.LinearAlgebra.varMeasurementMatrix Q r A₀ R ℤ place varOf (c, β) v whenever auxRow encodes row β of Cslib.LinearAlgebra.measurementMatrix along code.

theorem Cslib.LinearAlgebra.CopyPlacement.getD_pullbackReplacementRow_ofFn_eq_coeffsBelow_varReplacementRowScaledInt {M n h Q r A₀ R : ℕ} (place : Fin M → Fin h × AuxLabel Q r) (varOf : Fin M → Fin n) (code : AuxLabel Q r → ℕ) (blockRepl : List (List (List ℤ))) (e : Fin M) (hrepl : ∀ (y : AuxLabel Q r) {k : ℕ}, k < R → rowEntry (blockRepl.getD (code (place e).2) []) (code y) k = (auxReplacementRowScaledInt Q r A₀ R (place e).2 y).coeff k) (v : Fin n) : (pullbackReplacementRow n R (List.ofFn fun (i : Fin M) => (↑(place i).1, code (place i).2)) (List.ofFn fun (i : Fin M) => ↑(varOf i)) (↑e) blockRepl).getD ↑v [] = (varReplacementRowScaledInt Q r A₀ R place varOf e v).coeffsBelow R

When Cslib.rowEntry (blockRepl.getD (code (place e).2) []) (code y) k agrees with the degree-k coefficient of Cslib.LinearAlgebra.auxReplacementRowScaledInt for all y and k < R, entry v of pullbackReplacementRow equals Polynomial.coeffsBelow _ R of Cslib.LinearAlgebra.varReplacementRowScaledInt.

theorem Cslib.LinearAlgebra.CopyPlacement.ofCoeffList_pullbackReplacementRow_ofFn_eq_varReplacementRowScaledInt {M n h Q r A₀ R : ℕ} (hR : 0 < R) (place : Fin M → Fin h × AuxLabel Q r) (varOf : Fin M → Fin n) (code : AuxLabel Q r → ℕ) (blockRepl : List (List (List ℤ))) (e : Fin M) (hrepl : ∀ (y : AuxLabel Q r) {k : ℕ}, k < R → rowEntry (blockRepl.getD (code (place e).2) []) (code y) k = (auxReplacementRowScaledInt Q r A₀ R (place e).2 y).coeff k) (v : Fin n) : Polynomial.ofCoeffList ((pullbackReplacementRow n R (List.ofFn fun (i : Fin M) => (↑(place i).1, code (place i).2)) (List.ofFn fun (i : Fin M) => ↑(varOf i)) (↑e) blockRepl).getD ↑v []) = varReplacementRowScaledInt Q r A₀ R place varOf e v

When 0 < R and Cslib.rowEntry (blockRepl.getD (code (place e).2) []) (code y) k agrees with the degree-k coefficient of Cslib.LinearAlgebra.auxReplacementRowScaledInt for all y and k < R, Polynomial.ofCoeffList of entry v of pullbackReplacementRow equals Cslib.LinearAlgebra.varReplacementRowScaledInt Q r A₀ R place varOf e v.

Plain polynomial-time certificates (ComputableInPolyTime)

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_fiberRanksWithInput {Input : Type} {encIn : Input ↪ List Bool} {labels : Input → List ℕ} (hlabels : Turing.MultiTapeTM.ComputableInPolyTime labels encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => fiberRanks (labels x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Compositional plain polynomial-time certificate for fiberRanks.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_fiberRanks : Turing.MultiTapeTM.ComputableInPolyTime fiberRanks (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

fiberRanks is computable in polynomial time on framed lists of binary naturals.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_flatPlacementWithInput {Input : Type} {encIn : Input ↪ List Bool} {D : Input → ℕ} {labels : Input → List ℕ} (hD : Turing.MultiTapeTM.ComputableInPolyTime D encIn Turing.MultiTapeTM.encNat) (hlabels : Turing.MultiTapeTM.ComputableInPolyTime labels encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => flatPlacement (D x) (labels x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Compositional plain polynomial-time certificate for flatPlacement.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_flatPlacement : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List ℕ) => flatPlacement p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

flatPlacement is computable in polynomial time from (D, labels).

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_varGroupListWithInput {Input : Type} {encIn : Input ↪ List Bool} {varSchedules : Input → List (List ℕ)} {t g : Input → ℕ} (hsched : Turing.MultiTapeTM.ComputableInPolyTime varSchedules encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat))) (ht : Turing.MultiTapeTM.ComputableInPolyTime t encIn Turing.MultiTapeTM.encNat) (hg : Turing.MultiTapeTM.ComputableInPolyTime g encIn Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => varGroupList (varSchedules x) (t x) (g x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

Compositional plain polynomial-time certificate for varGroupList.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_varGroupList : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List (List ℕ) × ℕ × ℕ) => varGroupList p.1 p.2.1 p.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)

varGroupList is computable in polynomial time on (varSchedules, (t, g)).

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_pullbackMeasurementRowWithInput {Input : Type} {encIn : Input ↪ List Bool} {n : Input → ℕ} {placements : Input → List (ℕ × ℕ)} {incVars : Input → List ℕ} {copyIdx : Input → ℕ} {auxRow : Input → List ℤ} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hpl : Turing.MultiTapeTM.ComputableInPolyTime placements encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) (hinc : Turing.MultiTapeTM.ComputableInPolyTime incVars encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hcopy : Turing.MultiTapeTM.ComputableInPolyTime copyIdx encIn Turing.MultiTapeTM.encNat) (haux : Turing.MultiTapeTM.ComputableInPolyTime auxRow encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => pullbackMeasurementRow (n x) (placements x) (incVars x) (copyIdx x) (auxRow x)) encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

Compositional plain polynomial-time certificate for pullbackMeasurementRow (n in unary).

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_pullbackMeasurementRow : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × List (ℕ × ℕ) × List ℕ × ℕ × List ℤ) => pullbackMeasurementRow p.1 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)

pullbackMeasurementRow is computable in polynomial time with n in encUnary.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_pullbackMeasurementMatrixWithInput {Input : Type} {encIn : Input ↪ List Bool} {n h : Input → ℕ} {placements : Input → List (ℕ × ℕ)} {incVars : Input → List ℕ} {blockMeas : Input → List (List ℤ)} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hh : Turing.MultiTapeTM.ComputableInPolyTime h encIn Turing.MultiTapeTM.encUnary) (hpl : Turing.MultiTapeTM.ComputableInPolyTime placements encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) (hinc : Turing.MultiTapeTM.ComputableInPolyTime incVars encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hmeas : Turing.MultiTapeTM.ComputableInPolyTime blockMeas encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => pullbackMeasurementMatrix (n x) (h x) (placements x) (incVars x) (blockMeas x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for pullbackMeasurementMatrix ((n, h) in unary).

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_pullbackMeasurementMatrix : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (ℕ × ℕ) × List ℕ × List (List ℤ)) => pullbackMeasurementMatrix p.1.1 p.1.2 p.2.1 p.2.2.1 p.2.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

pullbackMeasurementMatrix is computable in polynomial time with (n, h) in encUnary.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_restrictGroupColumnsWithInput {Input : Type} {encIn : Input ↪ List Bool} {groupVars : Input → List ℕ} {mat : Input → List (List ℤ)} (hgroup : Turing.MultiTapeTM.ComputableInPolyTime groupVars encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (hmat : Turing.MultiTapeTM.ComputableInPolyTime mat encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => restrictGroupColumns (groupVars x) (mat x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for restrictGroupColumns.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_restrictGroupColumns : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List ℕ × List (List ℤ)) => restrictGroupColumns p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

restrictGroupColumns is computable in polynomial time.

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_pullbackReplacementRowWithInput {Input : Type} {encIn : Input ↪ List Bool} {n R : Input → ℕ} {placements : Input → List (ℕ × ℕ)} {incVars : Input → List ℕ} {e : Input → ℕ} {blockRepl : Input → List (List (List ℤ))} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hR : Turing.MultiTapeTM.ComputableInPolyTime R encIn Turing.MultiTapeTM.encUnary) (hpl : Turing.MultiTapeTM.ComputableInPolyTime placements encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat))) (hinc : Turing.MultiTapeTM.ComputableInPolyTime incVars encIn (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) (he : Turing.MultiTapeTM.ComputableInPolyTime e encIn Turing.MultiTapeTM.encNat) (hrepl : Turing.MultiTapeTM.ComputableInPolyTime blockRepl encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin)))) : Turing.MultiTapeTM.ComputableInPolyTime (fun (x : Input) => pullbackReplacementRow (n x) (R x) (placements x) (incVars x) (e x) (blockRepl x)) encIn (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

Compositional plain polynomial-time certificate for pullbackReplacementRow ((n, R) in unary).

theorem Cslib.LinearAlgebra.CopyPlacement.computableInPolyTime_pullbackReplacementRow : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (ℕ × ℕ) × List (ℕ × ℕ) × List ℕ × ℕ × List (List (List ℤ))) => pullbackReplacementRow p.1.1 p.1.2 p.2.1 p.2.2.1 p.2.2.2.1 p.2.2.2.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat)) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))))))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encIntBin))

pullbackReplacementRow is computable in polynomial time with (n, R) in encUnary.