Bridge from Section 4 replacement designs to the Section 3 counting design interface

Section 3 of [OpenAI2026ETH] (Definition 3.1, Lemma 3.2, and Proposition 3.4, pp. 21–26) formulates the shared-summary Boolean-cube counting routine around an abstract (r, τ, D)-replacement design (Cslib.ReplacementCounting.Design), while Section 4 (Lemmas 4.1–4.7, pp. 26–34) constructs the concrete auxiliary exchange-operator rows, balanced variable/factor schedules, injective copy placements, measurement matrices, and cleared-denominator integer polynomials bundled in Cslib.LinearAlgebra.ReplacementDesign.

This module bridges the two layers without introducing a third intermediate interface:

1. Concrete-to-abstract design conversion (ReplacementDesign.toCountingDesign): Every D : Cslib.LinearAlgebra.ReplacementDesign scope Q r A₀ R τ (with 2 ≤ r, 1 ≤ R < Q, and 0 < τ ≤ 1 / 2) canonically induces a Cslib.ReplacementCounting.Design (Fin n) s (fun f => {v : Fin n // v ∈ scope f}) (fun _ v => v.1) r Q R (r ^ (2 * Q)) (τ : ℝ) for any finite subset of active factors s : Finset F:

   • Evaluation nodes nodeInt t = (t.1 : ℤ) + 1 ∈ {1, …, Q} lift to nodePoint t : ℚ.
   • Variable groups varGroup t v = D.varAssign v t have group sets varGroup D.varAssign t g of cardinality at most 2 * n / r.
   • Each group (t, g) has D.h * #(measurementIndices Q r A₀ R) integer measurement rows formed by restricting the columns of varMeasurementMatrix Q r A₀ R ℤ D.place (scopeVarOf scope) to varGroup D.varAssign t g, preserving the row ℓ₁-bound ≤ r ^ (2 * Q), total row bound ≤ 2 * τ * n, and off-group kernel annihilation at nodePoint t.
   • Replacement polynomial rows (f, v) ↦ varReplacementRow Q r A₀ R D.place (scopeVarOf scope) ⟨f, v⟩ have degree at most R - 1 ≤ R, evaluate to δ_{v.1} at T = 0, and retain the explicit cleared-denominator identity and ℓ₁ coefficient norm bound of Lemma 4.6 (commonDenom Q R = (R - 1)! * Q!).

2. Three-term exponential domain-examination bound (Section 3.5, eq. (3.16), p. 26): Cslib.ReplacementCounting.threeTermExponent r Q R D τ defines the three-term counting-cost rate (R / Q) log (2 Q / R) + τ log (2 D + 1) + 1 / r, and Design.domainExaminationBound_le_mul_exp_threeTermExponent bounds Proposition 3.4's finite-domain examination count by 2 Q r exp ((c + 4) n ((R / Q) log (2 Q / R) + τ log (2 D + 1) + 1 / r)) whenever q ≤ c n R / Q.

3. Combined Lemma 4.7 → Proposition 3.4 existence theorem (exists_countingDesign_of_scopes): Under the algebraic Lemma 4.7 hypotheses on scope : F → Finset (Fin n) with 0 < τ ≤ 1 / 2, there exists a concrete D : Cslib.LinearAlgebra.ReplacementDesign scope Q r A₀ R τ whose induced D.toCountingDesign satisfies Proposition 3.4's Hermite jet recovery, restricted-slice measurement-fiber factorization, and exponential domain-examination bounds while preserving all Lemma 4.5–4.7 incidence, copy, denominator, and coefficient-norm bounds. Formal bit-length and native runtime-cost bounds remain separate.

Main definitions

• Cslib.LinearAlgebra.nodeInt: 1-based integer evaluation node (t.1 : ℤ) + 1.
• Cslib.LinearAlgebra.measurementRowEquiv: canonical equivalence Fin (h * #(measurementIndices Q r A₀ R)) ≃ Fin h × measurementIndices Q r A₀ R.
• Cslib.LinearAlgebra.ReplacementDesign.groupMeasurementRow: group-restricted integer measurement rows C_{t,g} supported on varGroup D.varAssign t g.
• Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign: canonical conversion from Cslib.LinearAlgebra.ReplacementDesign to Cslib.ReplacementCounting.Design.
• Cslib.ReplacementCounting.threeTermExponent: the three-term counting-cost rate (R / Q) log (2 Q / R) + τ log (2 D + 1) + 1 / r (eq. (3.16), p. 26; eq. (4.18), p. 34).

Main results

• Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_row_natDegree_le_pred, Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_natDegree_targetPoly_le_mul_pred: sharpened R - 1 degree bounds for Section 4 replacement designs.
• Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_map_replacementRowScaledInt, Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_sum_coeffNorm1_le: Lemma 4.6 denominator-clearing and ℓ₁ coefficient norm bounds on the counting design's rows.
• Cslib.ReplacementCounting.Design.domainExaminationBound_le_mul_exp_threeTermExponent, Cslib.ReplacementCounting.Design.domainExaminationBound_div_le_mul_exp_threeTermExponent: equation (3.16) exponential bound on Proposition 3.4's finite-domain examination count.
• Cslib.LinearAlgebra.exists_countingDesign_of_scopes: Lemma 4.7 existence of a concrete ReplacementDesign together with its induced Cslib.ReplacementCounting.Design.

References

• OpenAI, The Exponential Time Hypothesis is False, Sections 3.1–3.5 and 4.1–4.6, Definition 3.1, Lemma 3.2, Proposition 3.4, Lemmas 4.1–4.7, pp. 21–34.

1. Integer evaluation nodes and group-restricted measurement matrices

def Cslib.LinearAlgebra.nodeInt {Q : ℕ} (t : Fin Q) : ℤ

The 1-based integer evaluation node t.1 + 1 ∈ {1, …, Q} associated to t : Fin Q ([OAI26c], Definition 3.1 and Section 4.3, pp. 21, 29).

@[simp]

theorem Cslib.LinearAlgebra.cast_nodeInt_rat {Q : ℕ} (t : Fin Q) : ↑(nodeInt t) = nodePoint t

Casting nodeInt t to ℚ recovers nodePoint t.

theorem Cslib.LinearAlgebra.nodeInt_pos {Q : ℕ} (t : Fin Q) : 0 < nodeInt t

nodeInt is strictly positive at every t : Fin Q.

theorem Cslib.LinearAlgebra.nodeInt_ne_zero {Q : ℕ} (t : Fin Q) : nodeInt t ≠ 0

nodeInt is nonzero at every t : Fin Q.

theorem Cslib.LinearAlgebra.nodeInt_injective (Q : ℕ) : Function.Injective nodeInt

nodeInt : Fin Q → ℤ is injective.

noncomputable def Cslib.LinearAlgebra.measurementRowEquiv (Q r A₀ R h : ℕ) : Fin (h * (measurementIndices Q r A₀ R).card) ≃ Fin h × ↥(measurementIndices Q r A₀ R)

Canonical equivalence indexing the h * #(measurementIndices Q r A₀ R) rows of the pulled-back measurement matrix varMeasurementMatrix by Fin (h * #(measurementIndices Q r A₀ R)).

theorem Cslib.LinearAlgebra.cast_varMeasurementMatrix_int_eq_rat {A : Type u_1} [Fintype A] (Q r A₀ R : ℕ) {n h : ℕ} (place : A → Fin h × AuxLabel Q r) (varOf : A → Fin n) (p : Fin h × ↥(measurementIndices Q r A₀ R)) (v : Fin n) : ↑(varMeasurementMatrix Q r A₀ R ℤ place varOf p v) = varMeasurementMatrix Q r A₀ R ℚ place varOf p v

Casting an integer entry of varMeasurementMatrix to ℚ agrees with the rational entry of varMeasurementMatrix.

noncomputable def Cslib.LinearAlgebra.ReplacementDesign.groupMeasurementRow {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (t : Fin Q) (g : Fin r) (k : Fin (D.h * (measurementIndices Q r A₀ R).card)) (v : Fin n) : ℤ

The integer measurement matrix C_{t,g} on group g at node t, obtained by restricting varMeasurementMatrix Q r A₀ R ℤ D.place (scopeVarOf scope) to columns v with D.varAssign v t = g and extending by 0 outside varGroup D.varAssign t g ([OAI26c], Definition 3.1(3) and equation (4.15), pp. 22, 32).

theorem Cslib.LinearAlgebra.ReplacementDesign.groupMeasurementRow_of_ne {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (t : Fin Q) (g : Fin r) (k : Fin (D.h * (measurementIndices Q r A₀ R).card)) {v : Fin n} (hv : D.varAssign v t ≠ g) : D.groupMeasurementRow t g k v = 0

D.groupMeasurementRow t g k vanishes outside {v : Fin n | D.varAssign v t = g}.

theorem Cslib.LinearAlgebra.ReplacementDesign.groupMeasurementRow_of_eq {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (t : Fin Q) (g : Fin r) (k : Fin (D.h * (measurementIndices Q r A₀ R).card)) {v : Fin n} (hv : D.varAssign v t = g) : D.groupMeasurementRow t g k v = varMeasurementMatrix Q r A₀ R ℤ D.place (BalancedSchedules.scopeVarOf scope) ((measurementRowEquiv Q r A₀ R D.h) k) v

On {v : Fin n | D.varAssign v t = g}, D.groupMeasurementRow t g k agrees with varMeasurementMatrix.

theorem Cslib.LinearAlgebra.ReplacementDesign.sum_natAbs_groupMeasurementRow_le {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (t : Fin Q) (g : Fin r) (k : Fin (D.h * (measurementIndices Q r A₀ R).card)) : ∑ v : Fin n, (D.groupMeasurementRow t g k v).natAbs ≤ r ^ (2 * Q)

Every row of D.groupMeasurementRow t g has ℓ₁-norm at most r ^ (2 * Q).

theorem Cslib.LinearAlgebra.ReplacementDesign.sum_groupMeasurementRow_mul_eq_mulVec {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (t : Fin Q) (g : Fin r) (k : Fin (D.h * (measurementIndices Q r A₀ R).card)) {ξ : Fin n → ℚ} (hsupp : ∀ (v : Fin n), D.varAssign v t ≠ g → ξ v = 0) : ∑ v : Fin n, ↑(D.groupMeasurementRow t g k v) * ξ v = (varMeasurementMatrix Q r A₀ R ℚ D.place (BalancedSchedules.scopeVarOf scope)).mulVec ξ ((measurementRowEquiv Q r A₀ R D.h) k)

When ξ : Fin n → ℚ vanishes outside varGroup D.varAssign t g, pairing ξ with row k of D.groupMeasurementRow t g equals row measurementRowEquiv Q r A₀ R D.h k of (varMeasurementMatrix Q r A₀ R ℚ D.place (scopeVarOf scope)).mulVec ξ.

2. Canonical conversion ReplacementDesign → Cslib.ReplacementCounting.Design

noncomputable def Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) : ReplacementCounting.Design (Fin n) s (fun (f : F) => ↥(scope f)) (fun (x : F) (v : ↥(scope x)) => ↑v) r Q R (r ^ (2 * Q)) ↑τ

Canonical conversion of a concrete Section 4 ReplacementDesign into a Section 3 Cslib.ReplacementCounting.Design over any active factor subset s : Finset F ([OAI26c], Definition 3.1 and Lemma 4.7, pp. 21–22, 33–34).

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_nodes {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).nodes = nodeInt

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_varGroup {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (t : Fin Q) (v : Fin n) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).varGroup t v = D.varAssign v t

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_groupSet {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (t : Fin Q) (g : Fin r) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).groupSet t g = varGroup D.varAssign t g

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_factorGroup {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).factorGroup = D.factorAssign

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_numRows {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (t : Fin Q) (g : Fin r) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).numRows t g = D.h * (measurementIndices Q r A₀ R).card

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_sum_numRows {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (t : Fin Q) : ∑ g : Fin r, (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).numRows t g = r * (D.h * (measurementIndices Q r A₀ R).card)

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_matrix {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).matrix = D.groupMeasurementRow

@[simp]

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_row {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (f : F) (v : ↥(scope f)) (i : Fin n) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).row f v i = varReplacementRow Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) ⟨f, v⟩ i

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_evalRowRat {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (t : Fin Q) (f : F) (v : ↥(scope f)) (x : Fin n → ℚ) : (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).evalRowRat t f v x = evalVarReplacementRow Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) ⟨f, v⟩ (nodePoint t) x

Evaluating (D.toCountingDesign ...).evalRowRat t f v x agrees with evalVarReplacementRow at nodePoint t.

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_row_natDegree_le_pred {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (f : F) (v : ↥(scope f)) (i : Fin n) : ((D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).row f v i).natDegree ≤ R - 1

Section 4 replacement rows in D.toCountingDesign satisfy the sharper degree bound natDegree ≤ R - 1 (Lemma 4.3 and Section 4.5, pp. 29, 32).

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_natDegree_targetPoly_le_mul_pred {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) {A : Type u_2} [CommRing A] [Algebra ℚ A] (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (Φ : (f : F) → MvPolynomial (↥(scope f)) A) {d : ℕ} (hd : (ReplacementCounting.liftedFactorProduct s Φ).totalDegree ≤ d) : ((D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).targetPoly Φ).natDegree ≤ d * (R - 1)

Consequently, ((D.toCountingDesign ...).targetPoly Φ).natDegree ≤ d * (R - 1) whenever (liftedFactorProduct s Φ).totalDegree ≤ d.

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_map_replacementRowScaledInt {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (s : Finset F) (hr : 2 ≤ r) (hR : 1 ≤ R) (hRQ : R < Q) (hτ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (f : F) (v : ↥(scope f)) (i : Fin n) : Polynomial.map (Int.castRingHom ℚ) (varReplacementRowScaledInt Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) ⟨f, v⟩ i) = ↑(commonDenom Q R) • (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).row f v i

Lemma 4.6 common-denominator clearing on D.toCountingDesign (p. 33): multiplying (D.toCountingDesign ...).row f v i by commonDenom Q R = (R - 1)! * Q! yields the integer polynomial varReplacementRowScaledInt Q r A₀ R D.place (scopeVarOf scope) ⟨f, v⟩ i.

theorem Cslib.LinearAlgebra.ReplacementDesign.toCountingDesign_sum_coeffNorm1_le {Q r A₀ R n : ℕ} {F : Type u_1} [Fintype F] {scope : F → Finset (Fin n)} {τ : ℚ} (D : ReplacementDesign scope Q r A₀ R τ) (f : F) (v : ↥(scope f)) : ∑ i : Fin n, ↑(varReplacementRowScaledInt Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) ⟨f, v⟩ i).coeffNorm1 ≤ ↑(commonDenom Q R) * (1 + (1 + 2 ^ Q) * ↑R * (4 * ↑Q) ^ (R - 1))

Lemma 4.6 cleared-row ℓ₁ coefficient norm bound on D.toCountingDesign (p. 33): the sum of coeffNorm1 across all n entries of the cleared integer row for (f, v) is at most commonDenom Q R * (1 + (1 + 2 ^ Q) * R * (4 * Q) ^ (R - 1)).

3. Three-term exponential domain-examination bound (Section 3.5, eq. (3.16), p. 26)

noncomputable def Cslib.ReplacementCounting.threeTermExponent (r Q R D : ℕ) (τ : ℝ) : ℝ

The three-term counting-cost rate (R / Q) log (2 Q / R) + τ log (2 D + 1) + 1 / r governing the finite-domain examination bound of Proposition 3.4 and equation (3.16) ([OAI26c], Section 3.5, p. 26 and Section 4.7, equation (4.18), p. 34).

theorem Cslib.ReplacementCounting.one_le_two_mul_log_two_mul_div {R Q : ℕ} (hR : 1 ≤ R) (hRQ : R ≤ Q) : 1 ≤ 2 * Real.log (2 * ↑Q / ↑R)

When 1 ≤ R ≤ Q, 1 ≤ 2 * log (2 * Q / R) because 1 - 1 / 2 ≤ log 2 ≤ log (2 * Q / R).

theorem Cslib.ReplacementCounting.subsetPairCount_le_exp_mul_log_ratio {R Q n q : ℕ} {c : ℝ} (hR : 1 ≤ R) (hRQ : R ≤ Q) (hq : ↑q ≤ c * ↑n * (↑R / ↑Q)) : ↑(subsetPairCount n q) ≤ Real.exp ((c + 4) * ↑n * (↑R / ↑Q * Real.log (2 * ↑Q / ↑R)))

For 1 ≤ R ≤ Q and (q : ℝ) ≤ c * n * (R / Q), subsetPairCount n q is bounded by exp ((c + 4) * n * ((R / Q) * log (2 Q / R))) ([OAI26c], Section 3.5, p. 26).

theorem Cslib.ReplacementCounting.Design.threeTermExponent_pos {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] {s : Finset F} {κ : F → Type u_3} {scope : (f : F) → κ f → ι} {r Q R D : ℕ} {τ : ℝ} (M : Design ι s κ scope r Q R D τ) : 0 < threeTermExponent r Q R D τ

threeTermExponent r Q R D τ is strictly positive for any Design.

theorem Cslib.ReplacementCounting.Design.domainExaminationBound_le_mul_exp_threeTermExponent {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] {s : Finset F} {κ : F → Type u_3} {scope : (f : F) → κ f → ι} {r Q R D : ℕ} {τ : ℝ} (M : Design ι s κ scope r Q R D τ) {q : ℕ} {c : ℝ} (hc : 0 ≤ c) (hq : ↑q ≤ c * ↑(Fintype.card ι) * (↑R / ↑Q)) : ∑ t : Fin Q, ↑{p : Finset ι × Finset ι | p.1.card ≤ q ∧ p.2 ⊆ p.1}.card * (2 * ↑(M.measurementBox t).card * ∑ g : Fin r, ↑(Fintype.card (M.LocalCube t g))) ≤ 2 * ↑Q * ↑r * Real.exp ((c + 4) * ↑(Fintype.card ι) * threeTermExponent r Q R D τ)

Equation (3.16) exponential bound on Proposition 3.4's domain examination count ([OAI26c], Section 3.5, p. 26): whenever 0 ≤ c and (q : ℝ) ≤ c * Fintype.card ι * (R / Q), the total number of local Boolean assignments examined across all Q nodes and all subset pairs (E, U) with #E ≤ q and U ⊆ E is at most 2 * Q * r * exp ((c + 4) * Fintype.card ι * threeTermExponent r Q R D τ).

theorem Cslib.ReplacementCounting.Design.domainExaminationBound_div_le_mul_exp_threeTermExponent {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] {s : Finset F} {κ : F → Type u_3} {scope : (f : F) → κ f → ι} {r Q R D : ℕ} {τ : ℝ} (M : Design ι s κ scope r Q R D τ) {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (hd : ↑d ≤ c * ↑(Fintype.card ι)) : ∑ t : Fin Q, ↑{p : Finset ι × Finset ι | p.1.card ≤ d * R / Q ∧ p.2 ⊆ p.1}.card * (2 * ↑(M.measurementBox t).card * ∑ g : Fin r, ↑(Fintype.card (M.LocalCube t g))) ≤ 2 * ↑Q * ↑r * Real.exp ((c + 4) * ↑(Fintype.card ι) * threeTermExponent r Q R D τ)

Specialization of domainExaminationBound_le_mul_exp_threeTermExponent to the canonical truncation order q = (d * R) / Q = jetOrder (d * R) Q - 1 (equation (3.5), p. 24) when (d : ℝ) ≤ c * Fintype.card ι.

4. Combined Lemma 4.7 → Definition 3.1 / Proposition 3.4 existence bridge

theorem Cslib.LinearAlgebra.exists_countingDesign_of_scopes {n : ℕ} {F : Type u_1} [Fintype F] (scope : F → Finset (Fin n)) (s : Finset F) {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τ_pos : 0 < τ) (hτ_le : τ ≤ 1 / 2) (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)) : ∃ (D : ReplacementDesign scope Q r A₀ R τ), Nonempty (ReplacementCounting.Design (Fin n) s (fun (f : F) => ↥(scope f)) (fun (x : F) (v : ↥(scope x)) => ↑v) r Q R (r ^ (2 * Q)) ↑τ) ∧ D.h * r ^ (2 * Q) ≤ 2 * ∑ f : F, (scope f).card ∧ (∀ (f : F), scope f = ∅ → ∀ (t : Fin Q), ↑(D.factorAssign f t) = 0) ∧ (∀ (f : F) (v : ↥(scope f)) (i : Fin n), Polynomial.map (Int.castRingHom ℚ) (varReplacementRowScaledInt Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) ⟨f, v⟩ i) = ↑(commonDenom Q R) • (D.toCountingDesign s hr hR hRQ hτ_pos hτ_le).row f v i) ∧ ∀ (f : F) (v : ↥(scope f)), ∑ i : Fin n, ↑(varReplacementRowScaledInt Q r A₀ R D.place (BalancedSchedules.scopeVarOf scope) ⟨f, v⟩ i).coeffNorm1 ≤ ↑(commonDenom Q R) * (1 + (1 + 2 ^ Q) * ↑R * (4 * ↑Q) ^ (R - 1))

Lemma 4.7 → Definition 3.1 / Proposition 3.4 existence bridge ([OAI26c], Definition 3.1, Proposition 3.4, and Lemma 4.7, pp. 21–25, 33–34): Under the algebraic Lemma 4.7 hypotheses on scope : F → Finset (Fin n) with 0 < τ ≤ 1 / 2, there exists a concrete D : ReplacementDesign scope Q r A₀ R τ whose canonical D.toCountingDesign s hr hR hRQ hτ_pos hτ_le is a valid Cslib.ReplacementCounting.Design for every s : Finset F (automatically inheriting Design.targetSum_eq_of_taylorJet_jetOrder, Design.sum_restricted_shiftedFactor_eq_sum_measurement_fibers, and Design.domainExaminationBound_le_mul_exp_threeTermExponent while preserving all Lemma 4.5–4.7 incidence, copy, denominator, and ℓ₁ coefficient norm bounds on D).