Binomial measurement row counts and algebraic replacement design assembly (Lemmas 4.1 and 4.7)

This module assembles the algebraic replacement design construction of Section 4 of the manuscript The Exponential Time Hypothesis is False ([OpenAI2026ETH], printed pp. 28, 32–34) by proving the exact binomial fiber count of Lemma 4.1 (p. 28, equation 4.8), the total measurement row bound of equation (4.16) (p. 32), and a generalized algebraic Lemma 4.7 existence theorem (pp. 33–34) establishing conditions (1)–(4) of Definition 3.1 (pp. 21–22) together with the explicit cleared-denominator and ℓ₁-coefficient norm bounds of Lemma 4.6 underlying condition (5) (formal O(Q log Q + log D) bit-length and native runtime-cost integration remain separate):

1. Slot-level antisymmetric and symmetric pair counts (Lemma 4.1 proof, p. 28):

   • For each evaluation slot s : Fin Q, the r × r pair basis splits into antisymPairs r = {p : Fin r × Fin r | p.2 < p.1} of cardinality r * (r - 1) / 2 (card_antisymPairs, eigenvalue -1) and symPairs r = {p : Fin r × Fin r | ¬ p.2 < p.1} of cardinality r * (r + 1) / 2 (card_symPairs, eigenvalue +1).

2. Exact binomial fiber count and Lemma 4.1 tail bound (p. 28, eq. 4.8):

   • For every subset S : Finset (Fin Q), the set of auxiliary basis labels β : AuxLabel Q r whose antisymmetric slot set antisymSlots β = {s | β.2 s < β.1 s} equals S has cardinality (r * (r - 1) / 2) ^ #S * (r * (r + 1) / 2) ^ (Q - #S) (card_filter_antisymSlots_eq).
   • Summing over S ∈ powersetCard j univ gives the exact fiber count #({β : AuxLabel Q r | antisymCount β = j}) = Q.choose j * (r * (r - 1) / 2) ^ j * (r * (r + 1) / 2) ^ (Q - j) (card_filter_antisymCount_eq) and the exact measurement row count #(measurementIndices Q r A₀ R) (card_measurementIndices_eq).
   • Over ℚ, for 0 < r, (#(measurementIndices Q r A₀ R) : ℚ) = (r ^ (2 * Q) : ℚ) * binomTailProb Q r A₀ R (card_measurementIndices_cast_eq), so binomTailProb Q r A₀ R ≤ ε (eq. 4.8) implies (#(measurementIndices Q r A₀ R) : ℚ) ≤ ε * (r ^ (2 * Q) : ℚ) (card_measurementIndices_le_of_binomTailProb_le).

3. Total group measurement row bound (Section 4.5, eq. 4.16, p. 32):

   • When h * r ^ (2 * Q) ≤ 2 * M, M ≤ b * n, and binomTailProb Q r A₀ R ≤ τ / (r * b), the total number of measurement rows across all r variable groups satisfies ((r * (h * #(measurementIndices Q r A₀ R)) : ℕ) : ℚ) ≤ 2 * τ * (n : ℚ) (card_allGroupMeasurementRows_le_two_mul_tau_mul_n).

4. Algebraic replacement design assembly (Definition 3.1, pp. 21–22, and Lemma 4.7, pp. 33–34):

   • ReplacementDesign bundles the variable partition varAssign, factor group schedule factorAssign, copy count h, and injective copy placement place together with the group-size, measurement-row count, measurement ℓ₁-norm, degree, evaluation-at-zero, and kernel-invariance properties of Definition 3.1 (1)–(4), plus the explicit cleared-denominator identity and ℓ₁ coefficient norm bound of Lemma 4.6 (commonDenom Q R = (R - 1)! * Q!) underlying Definition 3.1 (5) (formal O(Q log Q + log D) bit-length and native runtime-cost endpoints remain separate follow-up).
   • exists_replacementDesign proves an algebraic generalization of Lemma 4.7 (printed pp. 33–34) by combining Lemma 4.1, Lemma 4.3, Lemma 4.5 (exists_balanced_schedules_of_scopes), Section 4.5 (fiberRankCopy, varReplacementRow, varMeasurementMatrix), and Lemma 4.6: it requires only 0 ≤ τ, M ≤ b * n (omitting n ≤ M and τ ≤ 1 / 2), and the weaker node-range condition hI : ∀ a < R - 1, A₀ + a ≤ Q (vacuous at R = 1) rather than full interval containment I ⊆ [0, Q].

Main definitions

• Cslib.LinearAlgebra.antisymPairs, Cslib.LinearAlgebra.symPairs: antisymmetric (p.2 < p.1) and symmetric/diagonal (¬ p.2 < p.1) pairs in Fin r × Fin r.
• Cslib.LinearAlgebra.antisymSlots: the subset of evaluation slots where β.2 s < β.1 s.
• Cslib.LinearAlgebra.binomTailProb: the binomial tail probability Pr[W ∉ {A₀, ..., A₀ + R - 1}] for W ∼ Bin(Q, (r - 1) / (2 * r)) (eq. 4.8).
• Cslib.LinearAlgebra.ReplacementDesign: bundled Section 4 replacement design satisfying Definition 3.1 (1)–(4) and the explicit denominator/coefficient-norm bounds of Lemma 4.6.

Main results

• Cslib.LinearAlgebra.card_antisymPairs, Cslib.LinearAlgebra.card_symPairs: #(antisymPairs r) = r * (r - 1) / 2 and #(symPairs r) = r * (r + 1) / 2.
• Cslib.LinearAlgebra.card_filter_antisymCount_eq, Cslib.LinearAlgebra.card_measurementIndices_eq, Cslib.LinearAlgebra.card_measurementIndices_cast_eq, Cslib.LinearAlgebra.card_measurementIndices_le_of_binomTailProb_le: Lemma 4.1 exact binomial fiber count and equation (4.8) tail bound.
• Cslib.LinearAlgebra.card_allGroupMeasurementRows_le_two_mul_tau_mul_n: equation (4.16) total measurement row bound ≤ 2 * τ * n.
• Cslib.LinearAlgebra.exists_replacementDesign: Lemma 4.7 algebraic existence of a Section 4 replacement design.

References

• OpenAI, The Exponential Time Hypothesis is False (Definition 3.1, Lemmas 4.1, 4.3, 4.5, 4.6, and 4.7, pp. 21–22, 28, 30–34)

Part 1: Slot-level antisymmetric and symmetric pair counts (Lemma 4.1, p. 28)

def Cslib.LinearAlgebra.antisymPairs (r : ℕ) : Finset (Fin r × Fin r)

Ordered pairs (a, d) : Fin r × Fin r with d < a, indexing the antisymmetric pair-basis functions e_{a,d} - e_{d,a} of eigenvalue -1 under coordinate swap.

def Cslib.LinearAlgebra.symPairs (r : ℕ) : Finset (Fin r × Fin r)

Ordered pairs (a, d) : Fin r × Fin r with ¬ (d < a), indexing the diagonal and symmetric pair-basis functions of eigenvalue +1 under coordinate swap.

def Cslib.LinearAlgebra.diagPairs (r : ℕ) : Finset (Fin r × Fin r)

Diagonal ordered pairs (a, d) : Fin r × Fin r with a = d.

@[simp]

theorem Cslib.LinearAlgebra.mem_antisymPairs {r : ℕ} {p : Fin r × Fin r} : p ∈ antisymPairs r ↔ p.2 < p.1

@[simp]

theorem Cslib.LinearAlgebra.mem_symPairs {r : ℕ} {p : Fin r × Fin r} : p ∈ symPairs r ↔ ¬p.2 < p.1

@[simp]

theorem Cslib.LinearAlgebra.mem_diagPairs {r : ℕ} {p : Fin r × Fin r} : p ∈ diagPairs r ↔ p.1 = p.2

theorem Cslib.LinearAlgebra.card_antisymPairs_add_card_symPairs (r : ℕ) : (antisymPairs r).card + (symPairs r).card = r * r

antisymPairs r and symPairs r partition Fin r × Fin r.

theorem Cslib.LinearAlgebra.card_diagPairs (r : ℕ) : (diagPairs r).card = r

There are r diagonal pairs (a, a) in Fin r × Fin r.

theorem Cslib.LinearAlgebra.map_swap_antisymPairs (r : ℕ) : Finset.map (Equiv.prodComm (Fin r) (Fin r)).toEmbedding (antisymPairs r) = {p : Fin r × Fin r | p.1 < p.2}

Swapping coordinates maps antisymPairs r (p.2 < p.1) bijectively onto {p | p.1 < p.2}.

theorem Cslib.LinearAlgebra.two_mul_card_antisymPairs_add (r : ℕ) : 2 * (antisymPairs r).card + r = r * r

Partitioning Fin r × Fin r into p.2 < p.1, p.1 < p.2, and p.1 = p.2 gives 2 * #(antisymPairs r) + r = r * r.

theorem Cslib.LinearAlgebra.two_mul_card_antisymPairs (r : ℕ) : 2 * (antisymPairs r).card = r * (r - 1)

Twice the number of antisymmetric pairs in Fin r × Fin r is r * (r - 1).

theorem Cslib.LinearAlgebra.two_mul_card_symPairs (r : ℕ) : 2 * (symPairs r).card = r * (r + 1)

Twice the number of symmetric/diagonal pairs in Fin r × Fin r is r * (r + 1).

theorem Cslib.LinearAlgebra.card_antisymPairs (r : ℕ) : (antisymPairs r).card = r * (r - 1) / 2

There are r * (r - 1) / 2 antisymmetric pairs in Fin r × Fin r (Lemma 4.1, p. 28).

theorem Cslib.LinearAlgebra.card_symPairs (r : ℕ) : (symPairs r).card = r * (r + 1) / 2

There are r * (r + 1) / 2 symmetric and diagonal pairs in Fin r × Fin r (Lemma 4.1, p. 28).

Part 2: Exact binomial fiber count and Lemma 4.1 tail bound (p. 28, eq. 4.8)

def Cslib.LinearAlgebra.antisymSlots {Q r : ℕ} (β : AuxLabel Q r) : Finset (Fin Q)

The subset of evaluation slots s : Fin Q at which β.2 s < β.1 s.

theorem Cslib.LinearAlgebra.antisymCount_eq_card_antisymSlots {Q r : ℕ} (β : AuxLabel Q r) : antisymCount β = (antisymSlots β).card

antisymCount β is the cardinality of antisymSlots β.

theorem Cslib.LinearAlgebra.antisymCount_le {Q r : ℕ} (β : AuxLabel Q r) : antisymCount β ≤ Q

antisymCount β is at most Q.

def Cslib.LinearAlgebra.auxLabelEquivSlotPairs (Q r : ℕ) : AuxLabel Q r ≃ (Fin Q → Fin r × Fin r)

Equivalence between AuxLabel Q r = (Fin Q → Fin r) × (Fin Q → Fin r) and slotwise pairs Fin Q → Fin r × Fin r.

theorem Cslib.LinearAlgebra.card_filter_antisymSlots_eq (Q r : ℕ) (S : Finset (Fin Q)) : {β : AuxLabel Q r | antisymSlots β = S}.card = (antisymPairs r).card ^ S.card * (symPairs r).card ^ (Q - S.card)

For any fixed subset S : Finset (Fin Q) of evaluation slots, the auxiliary labels β : AuxLabel Q r with antisymSlots β = S are in bijection with Fintype.piFinset (fun s => if s ∈ S then antisymPairs r else symPairs r) and therefore have cardinality #(antisymPairs r) ^ #S * #(symPairs r) ^ (Q - #S).

theorem Cslib.LinearAlgebra.card_filter_antisymCount_eq (Q r j : ℕ) : {β : AuxLabel Q r | antisymCount β = j}.card = Q.choose j * (r * (r - 1) / 2) ^ j * (r * (r + 1) / 2) ^ (Q - j)

Lemma 4.1 exact binomial fiber count (p. 28): The number of auxiliary basis labels β : AuxLabel Q r with antisymCount β = j is Q.choose j * (r * (r - 1) / 2) ^ j * (r * (r + 1) / 2) ^ (Q - j).

theorem Cslib.LinearAlgebra.card_measurementIndices_eq (Q r A₀ R : ℕ) : (measurementIndices Q r A₀ R).card = ∑ j ∈ Finset.range (Q + 1) with j < A₀ ∨ A₀ + R ≤ j, Q.choose j * (r * (r - 1) / 2) ^ j * (r * (r + 1) / 2) ^ (Q - j)

Lemma 4.1 exact measurement row count (p. 28): The number of measurement indices in measurementIndices Q r A₀ R is the sum over j ∈ range (Q + 1) outside [A₀, A₀ + R) of Q.choose j * (r * (r - 1) / 2) ^ j * (r * (r + 1) / 2) ^ (Q - j).

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

The binomial tail probability Pr[W ∉ {A₀, ..., A₀ + R - 1}] for W ∼ Bin(Q, (r - 1) / (2 * r)) from Lemma 4.1 and equation (4.8) (p. 28).

theorem Cslib.LinearAlgebra.cast_antisymPairs_eq (r : ℕ) : ↑(r * (r - 1) / 2) = ↑r ^ 2 * ((↑r - 1) / (2 * ↑r))

Rational cast of #(antisymPairs r) = r * (r - 1) / 2.

theorem Cslib.LinearAlgebra.cast_symPairs_eq (r : ℕ) (hr : 0 < r) : ↑(r * (r + 1) / 2) = ↑r ^ 2 * ((↑r + 1) / (2 * ↑r))

Rational cast of #(symPairs r) = r * (r + 1) / 2.

theorem Cslib.LinearAlgebra.card_measurementIndices_cast_eq (Q r A₀ R : ℕ) (hr : 0 < r) : ↑(measurementIndices Q r A₀ R).card = ↑(r ^ (2 * Q)) * binomTailProb Q r A₀ R

Lemma 4.1 rational identity (p. 28): For 0 < r, the number of rows #(measurementIndices Q r A₀ R) of measurementMatrix equals D * Pr[W ∉ I] = r ^ (2 * Q) * binomTailProb Q r A₀ R.

theorem Cslib.LinearAlgebra.card_measurementIndices_le_of_binomTailProb_le {Q r A₀ R : ℕ} {ε : ℚ} (hr : 0 < r) (hε : binomTailProb Q r A₀ R ≤ ε) : ↑(measurementIndices Q r A₀ R).card ≤ ε * ↑(r ^ (2 * Q))

Lemma 4.1 and equation (4.8) row bound (p. 28): If binomTailProb Q r A₀ R ≤ ε, then #(measurementIndices Q r A₀ R) ≤ ε * r ^ (2 * Q).

theorem Cslib.LinearAlgebra.binomTailProb_eq_div (Q r A₀ R : ℕ) (hr : 0 < r) : binomTailProb Q r A₀ R = ↑(measurementIndices Q r A₀ R).card / ↑(r ^ (2 * Q))

For 0 < r, binomTailProb Q r A₀ R equals the fraction #(measurementIndices Q r A₀ R) / r ^ (2 * Q) of auxiliary basis labels outside [A₀, A₀ + R).

theorem Cslib.LinearAlgebra.binomTailProb_nonneg {Q r A₀ R : ℕ} (hr : 1 ≤ r) : 0 ≤ binomTailProb Q r A₀ R

binomTailProb Q r A₀ R is nonnegative for 1 ≤ r.

theorem Cslib.LinearAlgebra.binomTailProb_zero_right (Q r A₀ : ℕ) (hr : 0 < r) : binomTailProb Q r A₀ 0 = 1

When R = 0, the interval [A₀, A₀ + R) is empty and binomTailProb Q r A₀ 0 = 1 (the full binomial distribution sums to 1).

theorem Cslib.LinearAlgebra.binomTailProb_le_one (Q r A₀ R : ℕ) (hr : 0 < r) : binomTailProb Q r A₀ R ≤ 1

binomTailProb Q r A₀ R ≤ 1 for 0 < r.

Part 3: Total group measurement row bound (Section 4.5, eq. 4.16, p. 32)

theorem Cslib.LinearAlgebra.card_allGroupMeasurementRows_le_two_mul_tau_mul_n {Q r A₀ R h M b n : ℕ} {τ : ℚ} (hr : 0 < r) (hb : 0 < b) (hτ : 0 ≤ τ) (hhD : h * r ^ (2 * Q) ≤ 2 * M) (hM : M ≤ b * n) (htail : binomTailProb Q r A₀ R ≤ τ / (↑r * ↑b)) : ↑(r * (h * (measurementIndices Q r A₀ R).card)) ≤ 2 * τ * ↑n

Equation (4.16) total group measurement row bound (p. 32): When h * r ^ (2 * Q) ≤ 2 * M, M ≤ b * n, 0 ≤ τ, and binomTailProb Q r A₀ R ≤ τ / (r * b), the total number of measurement rows r * (h * #(measurementIndices Q r A₀ R)) across all r variable groups is at most 2 * τ * n.

Part 4: Algebraic Section 4 replacement design (Definition 3.1 & Lemma 4.7, pp. 32–34)

structure Cslib.LinearAlgebra.ReplacementDesign {n : ℕ} {F : Type u_1} [Fintype F] (scope : F → Finset (Fin n)) (Q r A₀ R : ℕ) (τ : ℚ) : Type u_1

A bundled Section 4 replacement design for a factor scope family scope : F → Finset (Fin n), recording Definition 3.1 (1)–(4) (pp. 21–22) together with the explicit cleared-denominator identity and ℓ₁ coefficient norm bound of Lemma 4.6 (p. 33) that underlie Definition 3.1 (5) (formal O(Q log Q + log D) bit-length and native runtime endpoints are separate follow-up).

• varAssign : Fin n → Fin Q → Fin r

  Variable group schedule a_v : Fin Q → Fin r for each v : Fin n (determining varGroup varAssign t g = {v | varAssign v t = g}).

• factorAssign : F → Fin Q → Fin r

  Factor group schedule σ_f = d_f : Fin Q → Fin r for each f : F.

• h : ℕ

  Number of auxiliary array copies h.

• place : BalancedSchedules.ScopeIncidence scope → Fin self.h × AuxLabel Q r

  Placement of each factor–variable incidence into Fin h × AuxLabel Q r.

• card_varGroup_le (t : Fin Q) (g : Fin r) : (varGroup self.varAssign t g).card ≤ 2 * n / r

  Definition 3.1 (1): every variable group S_{t,g} has size at most 2 * n / r.

• factorAssign_of_empty (f : F) : scope f = ∅ → ∀ (t : Fin Q), ↑(self.factorAssign f t) = 0

  Section 4.1 / Lemma 4.5: factors with empty scope are assigned to group 0 at every point.

• injective_place : Function.Injective self.place

  Section 4.5: all occupied positions (c(f,v), u_{f,v}) in [h] × B are distinct.

• place_snd (e : BalancedSchedules.ScopeIncidence scope) : (self.place e).2 = (self.varAssign (BalancedSchedules.scopeVarOf scope e), self.factorAssign (BalancedSchedules.scopeFactorOf scope e))

  Section 4.4–4.5: the auxiliary label of incidence e = (f, v) is (a_v, d_f).

• h_mul_D_le : self.h * r ^ (2 * Q) ≤ 2 * ∑ f : F, (scope f).card

  Section 4.5: the copy count satisfies h * D ≤ 2 * M.

• total_measurement_rows_le : ↑(r * (self.h * (measurementIndices Q r A₀ R).card)) ≤ 2 * τ * ↑n

  Definition 3.1 (3) and equation (4.16): the total number of measurement rows across all r groups at each evaluation point t is at most 2 * τ * n.

• sum_abs_measurement_row_le (p : Fin self.h × ↥(measurementIndices Q r A₀ R)) : ∑ v : Fin n, |varMeasurementMatrix Q r A₀ R ℤ self.place (BalancedSchedules.scopeVarOf scope) p v| ≤ ↑r ^ (2 * Q)

  Definition 3.1 (3): every row of the integer measurement matrix has ℓ₁-norm at most D = r ^ (2 * Q).

• natDegree_replacementRow_le (e : BalancedSchedules.ScopeIncidence scope) (v : Fin n) : (varReplacementRow Q r A₀ R self.place (BalancedSchedules.scopeVarOf scope) e v).natDegree ≤ R - 1

  Definition 3.1 (4): every replacement polynomial entry has degree at most R - 1 (≤ R).

• eval_replacementRow_zero (e : BalancedSchedules.ScopeIncidence scope) (v : Fin n) : Polynomial.eval 0 (varReplacementRow Q r A₀ R self.place (BalancedSchedules.scopeVarOf scope) e v) = if BalancedSchedules.scopeVarOf scope e = v then 1 else 0

  Definition 3.1 (4): at T = 0, the replacement row for incidence e evaluates to δ_{scopeVarOf scope e}.

• evalReplacementRow_nodePoint_eq_zero_of_kernel (e : BalancedSchedules.ScopeIncidence scope) (t : Fin Q) (g : Fin r) : g ≠ self.factorAssign (BalancedSchedules.scopeFactorOf scope e) t → ∀ (ξ : Fin n → ℚ), (∀ v ∉ varGroup self.varAssign t g, ξ v = 0) → (varMeasurementMatrix Q r A₀ R ℚ self.place (BalancedSchedules.scopeVarOf scope)).mulVec ξ = 0 → evalVarReplacementRow Q r A₀ R self.place (BalancedSchedules.scopeVarOf scope) e (nodePoint t) ξ = 0

  Definition 3.1 (4): for every t : Fin Q, off-group g ≠ factorAssign f t, and vector ξ : Fin n → ℚ supported on varGroup varAssign t g in the kernel of the measurement matrix, the replacement form at nodePoint t annihilates ξ.

• map_replacementRowScaledInt (e : BalancedSchedules.ScopeIncidence scope) (v : Fin n) : Polynomial.map (Int.castRingHom ℚ) (varReplacementRowScaledInt Q r A₀ R self.place (BalancedSchedules.scopeVarOf scope) e v) = ↑(commonDenom Q R) • varReplacementRow Q r A₀ R self.place (BalancedSchedules.scopeVarOf scope) e v

  Definition 3.1 (5) and Lemma 4.6: multiplying by commonDenom Q R = (R - 1)! * Q! clears all denominators to the integer polynomial row varReplacementRowScaledInt.

• sum_coeffNorm1_replacementRowScaledInt_le (e : BalancedSchedules.ScopeIncidence scope) : ∑ v : Fin n, ↑(varReplacementRowScaledInt Q r A₀ R self.place (BalancedSchedules.scopeVarOf scope) e v).coeffNorm1 ≤ ↑(commonDenom Q R) * (1 + (1 + 2 ^ Q) * ↑R * (4 * ↑Q) ^ (R - 1))

  Definition 3.1 (5) and Lemma 4.6: the sum of the ℓ₁ coefficient norms across all n entries of each cleared row varReplacementRowScaledInt is bounded by commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)).

theorem Cslib.LinearAlgebra.ReplacementDesign.evalReplacementRow_zero {n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {Q r A₀ R : ℕ} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (x : Fin n → ℚ) : evalVarReplacementRow Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) e 0 x = x (BalancedSchedules.scopeVarOf scope e)

Evaluating the replacement form at T = 0 on any vector x : Fin n → ℚ extracts x (scopeVarOf scope e).

theorem Cslib.LinearAlgebra.ReplacementDesign.evalReplacementRow_nodePoint_eq_of_eq_on_varGroup {n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {Q r A₀ R : ℕ} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (e : BalancedSchedules.ScopeIncidence scope) (t : Fin Q) (x x' : Fin n → ℚ) (hgrp : ∀ v ∈ varGroup D.varAssign t (D.factorAssign (BalancedSchedules.scopeFactorOf scope e) t), x v = x' v) (hmeas : (varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec x = (varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec x') : evalVarReplacementRow Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) e (nodePoint t) x = evalVarReplacementRow Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) e (nodePoint t) x'

In any ReplacementDesign, the value of evalVarReplacementRow at nodePoint t for incidence e = (f, v) depends only on x restricted to the assigned variable group varGroup D.varAssign t (D.factorAssign f t) and the measurements (varMeasurementMatrix Q r A₀ R ℚ D.place (scopeVarOf scope)).mulVec x.

theorem Cslib.LinearAlgebra.exists_replacementDesign {n : ℕ} {F : Type u_1} [Fintype F] (scope : F → Finset (Fin n)) {Q r A₀ R b w : ℕ} {τ : ℚ} (hn : 1 ≤ n) (hb_pos : 1 ≤ b) (hw_pos : 1 ≤ w) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ : 0 ≤ τ) (hI : ∀ a < R - 1, A₀ + a ≤ Q) (hb : ∀ (v : Fin n), {f : F | v ∈ scope f}.card ≤ b) (hw : ∀ (f : F), (scope f).card ≤ w) (hM_le : ∑ f : F, (scope f).card ≤ b * n) (hincidenceSize : 2 * (b + w) * (r ^ (2 * Q)) ^ 2 ≤ ∑ f : F, (scope f).card) (hgroupSize : 2 * Q * r ^ 2 ≤ n) (htail : binomTailProb Q r A₀ R ≤ τ / (↑r * ↑b)) : Nonempty (ReplacementDesign scope Q r A₀ R τ)

Lemma 4.7 (Algebraic existence of a Section 4 replacement design, pp. 33–34): Suppose 1 ≤ n, 1 ≤ b, 1 ≤ w, 2 ≤ r, 1 ≤ R, R < Q, 0 ≤ τ, every factor scope scope f has size at most w, every variable belongs to at most b scopes, M = ∑ f, #(scope f) ≤ b * n, the balance inequalities 2 * (b + w) * (r ^ (2 * Q)) ^ 2 ≤ M and 2 * Q * r ^ 2 ≤ n hold (eq. 4.13), the mismatch-annihilator node-range condition hI : ∀ a < R - 1, A₀ + a ≤ Q holds (vacuous at R = 1 and implied by [A₀, A₀ + R) ⊆ [0, Q]), and the binomial tail bound binomTailProb Q r A₀ R ≤ τ / (r * b) holds (eq. 4.8). Then there exists a ReplacementDesign satisfying Definition 3.1 (1)–(4) and the explicit cleared-denominator and ℓ₁-coefficient norm bounds of Lemma 4.6 (omitting the paper's n ≤ M and 0 < τ ≤ 1 / 2 regime assumptions and leaving the O(Q log Q + log D) bit-length / native runtime endpoint as separate follow-up).