Variable copy placement and coefficient norm bounds for polynomial replacement rows

Given the auxiliary exchange matrix M0, measurement matrix measurementMatrix (C^B), and auxiliary replacement rows auxReplacementRow (P⃗_u(T)) from Complexity.Foundations.LinearAlgebra.ExchangeReplacement, this module formalizes Section 4.5 (p. 32, equations 4.14–4.16) and the explicit coefficient norm bounds of Lemma 4.6 (p. 33) of the manuscript The Exponential Time Hypothesis is False ([OpenAI2026ETH]):

1. Deterministic copy-index assignment from fiber multiplicity bounds (Section 4.5, p. 32):

   • For a linearly ordered incidence index type A and auxiliary label map u : A → β, if every fiber {e : A | u e = y} has cardinality at most h, fiberRankCopy u h_bound : A → Fin h assigns each incidence e its rank {e' : A | u e' = u e ∧ e' < e} within its fiber, making fun e => (fiberRankCopy u h_bound e, u e) injective (injective_fiberRankCopy_prod).

2. Variable copy placement into Fin h × AuxLabel Q r (Section 4.5, p. 32, eq. 4.14):

   • Given a placement place : A → Fin h × AuxLabel Q r and variable projection varOf : A → Fin n, the linear copy/fiber-sum map copyEmbed place varOf (ι : (Fin n → K) → (Fin h × AuxLabel Q r → K)) sums x (varOf e) over incidences e with place e = p (placing x (varOf e) at place e and 0 at unoccupied positions when place is injective), and copyProj c (π_c) projects onto copy c : Fin h.
   • varReplacementRow Q r A₀ R place varOf e : Fin n → ℚ[X] (P⃗_{f,v}(T) = P⃗_{u_{f,v}}(T) π_c ι) has degree at most R - 1 (natDegree_varReplacementRow_le), evaluates at T = 0 to δ_{varOf e} when place is injective (eval_varReplacementRow_zero, evalVarReplacementRow_zero), and clears denominators to varReplacementRowScaledInt upon multiplication by commonDenom Q R = (R - 1)! Q! (map_varReplacementRowScaledInt).

3. Variable measurement matrices and Definition 3.1 separation (Section 4.5, eqs. 4.15–4.16):

   • varGroup a t g = {v : Fin n | a v t = g} (S_{t,g}) partitions Fin n into r disjoint variable groups for each evaluation step t : Fin Q.
   • varMeasurementMatrix Q r A₀ R K place varOf (Ĉ = C̃ ι) and its group restrictions have h * #(measurementIndices Q r A₀ R) rows per group (r * h * #(measurementIndices Q r A₀ R) total rows across g : Fin r, eq. 4.16).
   • When place is injective, every row of varMeasurementMatrix Q r A₀ R ℤ place varOf has ℓ₁-norm at most r ^ (2 * Q) = D (sum_abs_varMeasurementMatrix_le), so on any {0, 1}-valued vector its evaluation lies in [-D, D].
   • When (place e').2.1 = a (varOf e') for all e' : A, Lemma 4.3 transfers directly to Fin n → ℚ: if g ≠ (place e).2.2 t and ξ is supported on varGroup a t g with (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec ξ = 0, then evalVarReplacementRow Q r A₀ R place varOf e (nodePoint t) ξ = 0 (evalVarReplacementRow_nodePoint_eq_zero_of_kernel), and evalVarReplacementRow at nodePoint t depends only on x restricted to varGroup a t ((place e).2.2 t) and (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec x (evalVarReplacementRow_nodePoint_eq_of_eq_on_varGroup).

4. Explicit ℓ₁-coefficient norm bounds (Lemma 4.6, p. 33):

   • Reusing the canonical Polynomial.coeffNorm1 from Complexity.Foundations.Data.Polynomial.CoeffNorm1 and defining rowNorm1 A u = ∑ y, |A u y|, prove coeffNorm1_mismatchAnnihilatorScaledInt_le : (mismatchAnnihilatorScaledInt u y).coeffNorm1 ≤ Q! * 2 ^ Q and, when 0 < Q and hI : ∀ a < R - 1, A₀ + a ≤ Q, prove rowNorm1_M0ScaledInt_le : rowNorm1 (M0ScaledInt Q r A₀ R) u ≤ (R - 1)! * R * (4 * Q) ^ (R - 1) together with the row coefficient ℓ₁-sum bound ≤ commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)) for both auxReplacementRowScaledInt (sum_coeffNorm1_auxReplacementRowScaledInt_le) and, under injective place, varReplacementRowScaledInt (sum_coeffNorm1_varReplacementRowScaledInt_le).

Main definitions

• Cslib.LinearAlgebra.fiberRank, Cslib.LinearAlgebra.fiberRankCopy: deterministic copy index in Fin h from fiber multiplicity bound ≤ h.
• Cslib.LinearAlgebra.copyEmbed, Cslib.LinearAlgebra.copyProj: the linear copy/fiber-sum map ι into Fin h × AuxLabel Q r and copy projection π_c.
• Cslib.LinearAlgebra.varReplacementRow, Cslib.LinearAlgebra.evalVarReplacementRow, Cslib.LinearAlgebra.varReplacementRowScaledInt: replacement polynomial rows P⃗_{f,v}(T) on the original n variables and their integer-cleared counterparts.
• Cslib.LinearAlgebra.varGroup, Cslib.LinearAlgebra.varGroupRestrict, Cslib.LinearAlgebra.varMeasurementMatrix: variable groups S_{t,g} and pulled-back measurement matrix Ĉ = C̃ ι.
• Cslib.LinearAlgebra.rowNorm1: matrix row ℓ₁ norm.

Main results

• Cslib.LinearAlgebra.injective_fiberRankCopy_prod: distinctness of (c(e), u(e)) when fiber multiplicities are at most h.
• Cslib.LinearAlgebra.natDegree_varReplacementRow_le, Cslib.LinearAlgebra.evalVarReplacementRow_zero, Cslib.LinearAlgebra.evalVarReplacementRow_nodePoint_eq_zero_of_kernel, Cslib.LinearAlgebra.evalVarReplacementRow_nodePoint_eq_of_eq_on_varGroup: Definition 3.1 replacement row properties on Fin n.
• Cslib.LinearAlgebra.sum_abs_varMeasurementMatrix_le, Cslib.LinearAlgebra.abs_varMeasurementMatrix_mulVec_le_of_zero_one: row ℓ₁-norm bound ≤ r ^ (2 * Q) and [-D, D] range on {0, 1} inputs.
• Cslib.LinearAlgebra.coeffNorm1_mismatchAnnihilatorScaledInt_le, Cslib.LinearAlgebra.sum_coeffNorm1_auxReplacementRowScaledInt_le, Cslib.LinearAlgebra.sum_coeffNorm1_varReplacementRowScaledInt_le: Lemma 4.6 explicit row coefficient ℓ₁-sum bounds under 0 < Q and ∀ a < R - 1, A₀ + a ≤ Q.

References

• [OAI26c]

1. Deterministic copy assignment from fiber multiplicity bounds (Section 4.5, p. 32)

def Cslib.LinearAlgebra.fiberRank {A : Type u_1} {β : Type u_2} [Fintype A] [LinearOrder A] [DecidableEq β] (u : A → β) (e : A) : ℕ

Rank of e : A within its label fiber {e' : A | u e' = u e}, counting strictly smaller elements e' < e.

theorem Cslib.LinearAlgebra.fiberRank_lt_card_fiber {A : Type u_1} {β : Type u_2} [Fintype A] [LinearOrder A] [DecidableEq β] (u : A → β) (e : A) : fiberRank u e < {e' : A | u e' = u e}.card

theorem Cslib.LinearAlgebra.injective_fiberRank_prod {A : Type u_1} {β : Type u_2} [Fintype A] [LinearOrder A] [DecidableEq β] (u : A → β) : Function.Injective fun (e : A) => (fiberRank u e, u e)

def Cslib.LinearAlgebra.fiberRankCopy {A : Type u_1} {β : Type u_2} [Fintype A] [LinearOrder A] [DecidableEq β] {h : ℕ} (u : A → β) (h_bound : ∀ (y : β), {e : A | u e = y}.card ≤ h) (e : A) : Fin h

Explicit copy index c(e) ∈ Fin h assigned to e : A when every label fiber of u : A → β has size at most h (Section 4.5, p. 32).

theorem Cslib.LinearAlgebra.injective_fiberRankCopy_prod {A : Type u_1} {β : Type u_2} [Fintype A] [LinearOrder A] [DecidableEq β] {h : ℕ} (u : A → β) (h_bound : ∀ (y : β), {e : A | u e = y}.card ≤ h) : Function.Injective fun (e : A) => (fiberRankCopy u h_bound e, u e)

All pairs (fiberRankCopy u h_bound e, u e) in Fin h × β are distinct (Section 4.5, p. 32).

2. Variable copy placement into Fin h × AuxLabel Q r (Section 4.5, p. 32, eq. 4.14)

def Cslib.LinearAlgebra.copyEmbed {A : Type u_1} [Fintype A] {n h Q r : ℕ} {K : Type u_2} [AddCommMonoid K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (x : Fin n → K) (p : Fin h × AuxLabel Q r) : K

The linear copy/fiber-sum map ι : (Fin n → K) → (Fin h × AuxLabel Q r → K) summing x (varOf e) over incidences e : A with place e = p (which places x (varOf e) at position place e and 0 at unoccupied positions when place is injective; Section 4.5, p. 32).

def Cslib.LinearAlgebra.copyProj {h Q r : ℕ} {K : Type u_1} (c : Fin h) (η : Fin h × AuxLabel Q r → K) (u : AuxLabel Q r) : K

The projection π_c : (Fin h × AuxLabel Q r → K) → (AuxLabel Q r → K) onto copy c : Fin h (Section 4.5, p. 32).

@[simp]

theorem Cslib.LinearAlgebra.copyEmbed_zero {A : Type u_1} [Fintype A] {n h Q r : ℕ} {K : Type u_2} [AddCommMonoid K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) : copyEmbed place varOf 0 = 0

theorem Cslib.LinearAlgebra.copyEmbed_add {A : Type u_1} [Fintype A] {n h Q r : ℕ} {K : Type u_2} [AddCommMonoid K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (x₁ x₂ : Fin n → K) : copyEmbed place varOf (x₁ + x₂) = copyEmbed place varOf x₁ + copyEmbed place varOf x₂

theorem Cslib.LinearAlgebra.copyEmbed_sub {A : Type u_1} [Fintype A] {n h Q r : ℕ} {K : Type u_2} [AddCommGroup K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (x₁ x₂ : Fin n → K) : copyEmbed place varOf (x₁ - x₂) = copyEmbed place varOf x₁ - copyEmbed place varOf x₂

@[simp]

theorem Cslib.LinearAlgebra.copyProj_zero {h Q r : ℕ} {K : Type u_1} [Zero K] (c : Fin h) : copyProj c 0 = 0

theorem Cslib.LinearAlgebra.copyProj_add {h Q r : ℕ} {K : Type u_1} [Add K] (c : Fin h) (η₁ η₂ : Fin h × AuxLabel Q r → K) : copyProj c (η₁ + η₂) = copyProj c η₁ + copyProj c η₂

theorem Cslib.LinearAlgebra.copyProj_sub {h Q r : ℕ} {K : Type u_1} [Sub K] (c : Fin h) (η₁ η₂ : Fin h × AuxLabel Q r → K) : copyProj c (η₁ - η₂) = copyProj c η₁ - copyProj c η₂

theorem Cslib.LinearAlgebra.copyEmbed_apply_place {A : Type u_1} [Fintype A] {n h Q r : ℕ} {K : Type u_2} [AddCommMonoid K] {place : A → Fin h × AuxLabel Q r} (hinj : Function.Injective place) (varOf : A → Fin n) (x : Fin n → K) (e : A) : copyEmbed place varOf x (place e) = x (varOf e)

When place is injective, copyEmbed place varOf x (place e) extracts x (varOf e).

noncomputable def Cslib.LinearAlgebra.varReplacementRow {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (e : A) (v : Fin n) : Polynomial ℚ

The replacement polynomial row P⃗_e(T) = P⃗_{u_e}(T) π_{c(e)} ι ∈ (Fin n → ℚ[X]) on the original variables Fin n (eq. 4.14, p. 32).

noncomputable def Cslib.LinearAlgebra.evalVarReplacementRow {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (e : A) (t : ℚ) (x : Fin n → ℚ) : ℚ

Pairing ⟨P⃗_e(t), x⟩ of varReplacementRow Q r A₀ R place varOf e with x : Fin n → ℚ at T = t (Section 4.5, p. 32).

noncomputable def Cslib.LinearAlgebra.varReplacementRowScaledInt {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (e : A) (v : Fin n) : Polynomial ℤ

The scaled integer replacement row d_den P⃗_e(T) ∈ (Fin n → ℤ[X]) on the original variables (Lemma 4.6, p. 33).

theorem Cslib.LinearAlgebra.evalVarReplacementRow_eq_evalAuxReplacementRow {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (e : A) (t : ℚ) (x : Fin n → ℚ) : evalVarReplacementRow Q r A₀ R place varOf e t x = evalAuxReplacementRow Q r A₀ R (place e).2 t (copyProj (place e).1 (copyEmbed place varOf x))

Equation (4.14) identity (p. 32): evaluating varReplacementRow on x : Fin n → ℚ equals evaluating auxReplacementRow at (place e).2 on π_{(place e).1} (ι x).

theorem Cslib.LinearAlgebra.natDegree_varReplacementRow_le {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (e : A) (v : Fin n) : (varReplacementRow Q r A₀ R place varOf e v).natDegree ≤ R - 1

Every entry of varReplacementRow Q r A₀ R place varOf e has degree at most R - 1 (Section 4.5, p. 32).

theorem Cslib.LinearAlgebra.eval_varReplacementRow_zero {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} {place : A → Fin h × AuxLabel Q r} (hinj : Function.Injective place) (varOf : A → Fin n) (e : A) (v : Fin n) : Polynomial.eval 0 (varReplacementRow Q r A₀ R place varOf e v) = if varOf e = v then 1 else 0

When place is injective, varReplacementRow evaluates at T = 0 to δ_{varOf e} (Section 4.5, p. 32).

theorem Cslib.LinearAlgebra.evalVarReplacementRow_zero {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} {place : A → Fin h × AuxLabel Q r} (hinj : Function.Injective place) (varOf : A → Fin n) (e : A) (x : Fin n → ℚ) : evalVarReplacementRow Q r A₀ R place varOf e 0 x = x (varOf e)

When place is injective, ⟨P⃗_e(0), x⟩ = x (varOf e) (Section 4.5, p. 32).

theorem Cslib.LinearAlgebra.map_varReplacementRowScaledInt {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (e : A) (v : Fin n) : Polynomial.map (Int.castRingHom ℚ) (varReplacementRowScaledInt Q r A₀ R place varOf e v) = ↑(commonDenom Q R) • varReplacementRow Q r A₀ R place varOf e v

Lemma 4.6 for varReplacementRow (p. 33): multiplying varReplacementRow by commonDenom Q R = (R - 1)! Q! gives the integer polynomial varReplacementRowScaledInt.

3. Variable measurement matrices and Definition 3.1 separation (Section 4.5, p. 32)

def Cslib.LinearAlgebra.varGroup {n Q r : ℕ} (a : Fin n → Fin Q → Fin r) (t : Fin Q) (g : Fin r) : Finset (Fin n)

The actual-variable group S_{t, g} = {v : Fin n | a v t = g} (eq. 4.14, p. 32).

@[simp]

theorem Cslib.LinearAlgebra.mem_varGroup {n Q r : ℕ} {a : Fin n → Fin Q → Fin r} {t : Fin Q} {g : Fin r} {v : Fin n} : v ∈ varGroup a t g ↔ a v t = g

theorem Cslib.LinearAlgebra.disjoint_varGroup {n Q r : ℕ} (a : Fin n → Fin Q → Fin r) (t : Fin Q) {g₁ g₂ : Fin r} (hne : g₁ ≠ g₂) : Disjoint (varGroup a t g₁) (varGroup a t g₂)

theorem Cslib.LinearAlgebra.biUnion_varGroup {n Q r : ℕ} (a : Fin n → Fin Q → Fin r) (t : Fin Q) : Finset.univ.biUnion (varGroup a t) = Finset.univ

def Cslib.LinearAlgebra.varGroupRestrict {n Q r : ℕ} {K : Type u_1} [Zero K] (a : Fin n → Fin Q → Fin r) (t : Fin Q) (g : Fin r) (x : Fin n → K) : Fin n → K

Restriction of x : Fin n → K to varGroup a t g, extended by zero outside varGroup a t g.

theorem Cslib.LinearAlgebra.sum_varGroupRestrict {n Q r : ℕ} {K : Type u_1} [AddCommMonoid K] (a : Fin n → Fin Q → Fin r) (t : Fin Q) (x : Fin n → K) : ∑ g : Fin r, varGroupRestrict a t g x = x

def Cslib.LinearAlgebra.varMeasurementMatrix {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (K : Type u_2) [CommRing K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) : Matrix (Fin h × ↥(measurementIndices Q r A₀ R)) (Fin n) K

The pulled-back measurement matrix Ĉ = C̃ ι on Fin n with rows indexed by Fin h × measurementIndices Q r A₀ R (eq. 4.15, p. 32).

def Cslib.LinearAlgebra.groupMeasurementMatrix {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (K : Type u_2) [CommRing K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (a : Fin n → Fin Q → Fin r) (t : Fin Q) (g : Fin r) : Matrix (Fin h × ↥(measurementIndices Q r A₀ R)) (↥(varGroup a t g)) K

The group-restricted measurement matrix C_{t,g} = Ĉ|_{S_{t,g}} keeping columns in varGroup a t g (eq. 4.15, p. 32).

theorem Cslib.LinearAlgebra.sum_card_rows_groupMeasurementMatrix (Q r A₀ R h : ℕ) : ∑ _g : Fin r, Fintype.card (Fin h × ↥(measurementIndices Q r A₀ R)) = r * h * (measurementIndices Q r A₀ R).card

Equation (4.16) row count identity (p. 32): each of the r matrices C_{t,g} has h * #(measurementIndices Q r A₀ R) rows, so their total row count across g : Fin r is r * h * #(measurementIndices Q r A₀ R).

theorem Cslib.LinearAlgebra.sum_card_rows_groupMeasurementMatrix_le (Q r A₀ R h h_bound c_bound : ℕ) (hh : h ≤ h_bound) (hc : (measurementIndices Q r A₀ R).card ≤ c_bound) : ∑ _g : Fin r, Fintype.card (Fin h × ↥(measurementIndices Q r A₀ R)) ≤ r * h_bound * c_bound

Equation (4.16) row count bound (p. 32): if h ≤ h_bound and #(measurementIndices Q r A₀ R) ≤ c_bound, then the total number of measurement rows across all r variable groups is at most r * h_bound * c_bound.

theorem Cslib.LinearAlgebra.varMeasurementMatrix_mulVec {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (K : Type u_2) [CommRing K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (x : Fin n → K) (c : Fin h) (β : ↥(measurementIndices Q r A₀ R)) : (varMeasurementMatrix Q r A₀ R K place varOf).mulVec x (c, β) = (measurementMatrix Q r A₀ R K).mulVec (copyProj c (copyEmbed place varOf x)) β

Equation (4.15) action identity (p. 32): the (c, β)-entry of (Ĉ x) equals the β-entry of C^B (π_c (ι x)).

theorem Cslib.LinearAlgebra.varMeasurementMatrix_mulVec_eq_zero_iff {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (K : Type u_2) [CommRing K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (x : Fin n → K) : (varMeasurementMatrix Q r A₀ R K place varOf).mulVec x = 0 ↔ ∀ (c : Fin h), (measurementMatrix Q r A₀ R K).mulVec (copyProj c (copyEmbed place varOf x)) = 0

Ĉ x = 0 iff C^B (π_c (ι x)) = 0 for every copy c : Fin h (p. 32).

theorem Cslib.LinearAlgebra.sum_varMeasurementMatrix_mulVec_varGroupRestrict {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (K : Type u_2) [CommRing K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (a : Fin n → Fin Q → Fin r) (t : Fin Q) (x : Fin n → K) : ∑ g : Fin r, (varMeasurementMatrix Q r A₀ R K place varOf).mulVec (varGroupRestrict a t g x) = (varMeasurementMatrix Q r A₀ R K place varOf).mulVec x

The full measurement vector Ĉ x is the sum over g : Fin r of the group measurements Ĉ (x|_{S_{t,g}}).

theorem Cslib.LinearAlgebra.copyProj_copyEmbed_eq_zero_of_not_mem_auxGroup {A : Type u_1} [Fintype A] {n h Q r : ℕ} {K : Type u_2} [AddCommMonoid K] (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (a : Fin n → Fin Q → Fin r) (hcompat : ∀ (e' : A), (place e').2.1 = a (varOf e')) (t : Fin Q) (g : Fin r) (ξ : Fin n → K) (hsupp : ∀ v ∉ varGroup a t g, ξ v = 0) (c : Fin h) {y : AuxLabel Q r} (hy : y ∉ auxGroup t g) : copyProj c (copyEmbed place varOf ξ) y = 0

If (place e').2.1 = a (varOf e') for all e' : A and ξ : Fin n → K vanishes outside varGroup a t g, then for every copy c : Fin h, copyProj c (copyEmbed place varOf ξ) vanishes outside auxGroup t g (Section 4.5, p. 32).

theorem Cslib.LinearAlgebra.evalVarReplacementRow_nodePoint_eq_zero_of_kernel {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (a : Fin n → Fin Q → Fin r) (hcompat : ∀ (e' : A), (place e').2.1 = a (varOf e')) (e : A) (t : Fin Q) (g : Fin r) (hg : g ≠ (place e).2.2 t) (ξ : Fin n → ℚ) (hsupp : ∀ v ∉ varGroup a t g, ξ v = 0) (hker : (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec ξ = 0) : evalVarReplacementRow Q r A₀ R place varOf e (nodePoint t) ξ = 0

Definition 3.1 kernel separation on Fin n (Section 4.5, p. 32): when (place e').2.1 = a (varOf e') for all e' : A, if g ≠ (place e).2.2 t, ξ : Fin n → ℚ is supported on varGroup a t g, and (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec ξ = 0, then evalVarReplacementRow Q r A₀ R place varOf e (nodePoint t) ξ = 0.

theorem Cslib.LinearAlgebra.evalVarReplacementRow_nodePoint_eq_of_eq_on_varGroup {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (a : Fin n → Fin Q → Fin r) (hcompat : ∀ (e' : A), (place e').2.1 = a (varOf e')) (e : A) (t : Fin Q) (x₁ x₂ : Fin n → ℚ) (hgroup : ∀ v ∈ varGroup a t ((place e).2.2 t), x₁ v = x₂ v) (hmeas : (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec x₁ = (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec x₂) : evalVarReplacementRow Q r A₀ R place varOf e (nodePoint t) x₁ = evalVarReplacementRow Q r A₀ R place varOf e (nodePoint t) x₂

Determination by assigned variable group and measurements (Section 4.5, p. 32): at T = nodePoint t, ⟨P⃗_e(nodePoint t), x⟩ depends only on x restricted to varGroup a t ((place e).2.2 t) and (varMeasurementMatrix Q r A₀ R ℚ place varOf).mulVec x.

theorem Cslib.LinearAlgebra.sum_abs_varMeasurementMatrix_le {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} {place : A → Fin h × AuxLabel Q r} (hinj : Function.Injective place) (varOf : A → Fin n) (p : Fin h × ↥(measurementIndices Q r A₀ R)) : ∑ v : Fin n, |varMeasurementMatrix Q r A₀ R ℤ place varOf p v| ≤ ↑r ^ (2 * Q)

When place is injective, every row of varMeasurementMatrix Q r A₀ R ℤ place varOf has absolute row sum at most r ^ (2 * Q) = D (Section 4.5, p. 32).

theorem Cslib.LinearAlgebra.abs_varMeasurementMatrix_mulVec_le_of_zero_one {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} {place : A → Fin h × AuxLabel Q r} (hinj : Function.Injective place) (varOf : A → Fin n) (x : Fin n → ℤ) (hx : ∀ (v : Fin n), x v = 0 ∨ x v = 1) (p : Fin h × ↥(measurementIndices Q r A₀ R)) : |(varMeasurementMatrix Q r A₀ R ℤ place varOf).mulVec x p| ≤ ↑r ^ (2 * Q)

On any {0, 1}-valued vector x : Fin n → ℤ, every coordinate of (varMeasurementMatrix Q r A₀ R ℤ place varOf).mulVec x has absolute value at most r ^ (2 * Q) = D (and thus lies in [-D, D] ∩ ℤ, Section 4.5, p. 32).

4. Explicit ℓ₁-coefficient norm bounds (Lemma 4.6, p. 33)

theorem Cslib.LinearAlgebra.coeffNorm1_mismatchAnnihilatorScaledInt_le {Q r : ℕ} (u y : AuxLabel Q r) : (mismatchAnnihilatorScaledInt u y).coeffNorm1 ≤ Q.factorial * 2 ^ Q

Lemma 4.6 annihilator norm bound (p. 33): ‖Q! φ_{u,y}‖₁ ≤ Q! * 2 ^ Q (i.e. ‖φ_{u,y}‖₁ ≤ 2 ^ Q).

theorem Cslib.LinearAlgebra.natCast_coeffNorm1_mismatchAnnihilatorScaledInt_le {Q r : ℕ} (u y : AuxLabel Q r) : ↑(mismatchAnnihilatorScaledInt u y).coeffNorm1 ≤ ↑Q.factorial * 2 ^ Q

Integer-cast form of coeffNorm1_mismatchAnnihilatorScaledInt_le.

def Cslib.LinearAlgebra.rowNorm1 {Q r : ℕ} (A : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (u : AuxLabel Q r) : ℤ

The row ℓ₁-norm ∑ y, |A u y| of a matrix A at row u (Lemma 4.6, p. 33).

theorem Cslib.LinearAlgebra.rowNorm1_nonneg {Q r : ℕ} (A : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (u : AuxLabel Q r) : 0 ≤ rowNorm1 A u

theorem Cslib.LinearAlgebra.rowNorm1_add_le {Q r : ℕ} (A B : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (u : AuxLabel Q r) : rowNorm1 (A + B) u ≤ rowNorm1 A u + rowNorm1 B u

theorem Cslib.LinearAlgebra.rowNorm1_sub_le {Q r : ℕ} (A B : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (u : AuxLabel Q r) : rowNorm1 (A - B) u ≤ rowNorm1 A u + rowNorm1 B u

theorem Cslib.LinearAlgebra.rowNorm1_sum_le {Q r : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (u : AuxLabel Q r) : rowNorm1 (∑ i ∈ s, f i) u ≤ ∑ i ∈ s, rowNorm1 (f i) u

theorem Cslib.LinearAlgebra.rowNorm1_smul {Q r : ℕ} (c : ℤ) (A : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (u : AuxLabel Q r) : rowNorm1 (c • A) u = |c| * rowNorm1 A u

@[simp]

theorem Cslib.LinearAlgebra.rowNorm1_one {Q r : ℕ} (u : AuxLabel Q r) : rowNorm1 1 u = 1

@[simp]

theorem Cslib.LinearAlgebra.rowNorm1_subsetSwapMatrix {Q r : ℕ} (J : Finset (Fin Q)) (u : AuxLabel Q r) : rowNorm1 (subsetSwapMatrix Q r ℤ J) u = 1

theorem Cslib.LinearAlgebra.rowNorm1_mul_le {Q r : ℕ} (A B : Matrix (AuxLabel Q r) (AuxLabel Q r) ℤ) (M : ℤ) (hB : ∀ (z : AuxLabel Q r), rowNorm1 B z ≤ M) (u : AuxLabel Q r) : rowNorm1 (A * B) u ≤ rowNorm1 A u * M

theorem Cslib.LinearAlgebra.rowNorm1_twoW0_le (Q r : ℕ) (u : AuxLabel Q r) : rowNorm1 (twoW0 Q r ℤ) u ≤ 2 * ↑Q

theorem Cslib.LinearAlgebra.rowNorm1_twoW0_sub_smul_le {Q r A₀ a : ℕ} (ha : A₀ + a ≤ Q) (u : AuxLabel Q r) : rowNorm1 (twoW0 Q r ℤ - (2 * (↑A₀ + ↑a)) • 1) u ≤ 4 * ↑Q

theorem Cslib.LinearAlgebra.rowNorm1_fallingProdMatrixInt_le {Q r A₀ j : ℕ} (hj : ∀ a < j, A₀ + a ≤ Q) (u : AuxLabel Q r) : rowNorm1 (fallingProdMatrixInt Q r A₀ j) u ≤ (4 * ↑Q) ^ j

theorem Cslib.LinearAlgebra.rowNorm1_fallingTermMatrixInt_le {Q r A₀ j : ℕ} (hj : ∀ a < j, A₀ + a ≤ Q) (u : AuxLabel Q r) : rowNorm1 (fallingTermMatrixInt Q r A₀ j) u ≤ (4 * ↑Q) ^ j

theorem Cslib.LinearAlgebra.rowNorm1_M0ScaledInt_le {Q r A₀ R : ℕ} (hQ : 0 < Q) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (u : AuxLabel Q r) : rowNorm1 (M0ScaledInt Q r A₀ R) u ≤ ↑(R - 1).factorial * ↑R * (4 * ↑Q) ^ (R - 1)

Lemma 4.6 matrix norm bound (p. 33): when 0 < Q and every interpolation node A₀ + a (a < R - 1) is at most Q, every row of M0ScaledInt Q r A₀ R has ℓ₁-norm at most (R - 1)! * R * (4 * Q) ^ (R - 1) (i.e. ‖M_0‖_∞ ≤ R (4 Q)^{R - 1}).

theorem Cslib.LinearAlgebra.sum_coeffNorm1_auxReplacementRowScaledInt_le {Q r A₀ R : ℕ} (hQ : 0 < Q) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (u : AuxLabel Q r) : ∑ y : AuxLabel Q r, ↑(auxReplacementRowScaledInt Q r A₀ R u y).coeffNorm1 ≤ ↑(commonDenom Q R) * (1 + (1 + 2 ^ Q) * ↑R * (4 * ↑Q) ^ (R - 1))

Lemma 4.6 auxiliary row coefficient bound (p. 33): when 0 < Q and every interpolation node A₀ + a (a < R - 1) is at most Q (hI : ∀ a < R - 1, A₀ + a ≤ Q), for every u : AuxLabel Q r, the sum of the absolute values of all coefficients in the cleared row auxReplacementRowScaledInt Q r A₀ R u is at most commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)).

theorem Cslib.LinearAlgebra.sum_coeffNorm1_varReplacementRowScaledInt_le {A : Type u_1} [Fintype A] {Q r A₀ R n h : ℕ} {place : A → Fin h × AuxLabel Q r} (hQ : 0 < Q) (hinj : Function.Injective place) (varOf : A → Fin n) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (e : A) : ∑ v : Fin n, ↑(varReplacementRowScaledInt Q r A₀ R place varOf e v).coeffNorm1 ≤ ↑(commonDenom Q R) * (1 + (1 + 2 ^ Q) * ↑R * (4 * ↑Q) ^ (R - 1))

Lemma 4.6 original-variable row coefficient bound (p. 33): when 0 < Q, place is injective, and hI : ∀ a < R - 1, A₀ + a ≤ Q, the sum of the absolute values of all coefficients in the cleared row varReplacementRowScaledInt Q r A₀ R place varOf e on Fin n is at most commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)).