Replacement designs and algebraic assembly for the shared-summary counting routine

Section 3 of OpenAI, The Exponential Time Hypothesis is False evaluates a finite sum of products of polynomial factors on the Boolean cube, $$Z = \sum_{x \in \{0, 1\}^n} \prod_{f \in F} \Phi_f((x_v)_{v \in I_f}),$$ over any commutative ℚ-algebra A by embedding Z as H(0) for a low-degree univariate polynomial H(T) ∈ A[T] built from polynomial replacement rows P⃗_{f,v}(T).

This module provides the algebraic design interface, domain cardinality bounds, and assembly identities from §§3.1–3.3 and §3.5 (Definition 3.1, Lemma 3.2, Proposition 3.4, and equations (3.1)–(3.6), (3.11)–(3.15), pp. 21–26), leaving the §3.4 affine/Taylor expansion (equations (3.7)–(3.10)) to AffineTaylor, the fixed-denominator coefficient bit-length condition (Definition 3.1(5)) to staged jet arithmetic, and Turing-machine time/space bounds to the runtime layer.

Main definitions

• Cslib.ReplacementCounting.intMeasurementBox: integer summary box [-D, D]^c of size (2D+1)^c.
• Cslib.ReplacementCounting.piGroupEquiv: decomposition (∀ g, {i // group i = g} → α) ≃ (ι → α).
• Cslib.ReplacementCounting.Design: algebraic (r, τ, D)-replacement design (Def. 3.1(1)–(4)).
• Cslib.ReplacementCounting.targetSum, Cslib.ReplacementCounting.liftedFactorProduct, Cslib.ReplacementCounting.targetPolynomial: Z (eq. (3.1)), disjoint-incidence product (eq. (3.2)), and H(T) (eq. (3.3)).
• Cslib.ReplacementCounting.jetOrder: confluent Taylor jet order J = ⌊d_H / Q⌋ + 1 (eq. (3.5)).

Main results

• Cslib.ReplacementCounting.pow_mul_subsetPairCount_le, Cslib.ReplacementCounting.subsetPairCount_le_one_div_pow_mul, Cslib.ReplacementCounting.subsetPairCount_le_ratio_pow: weighted Cslib.subsetPairCount bounds (eq. (3.15)).
• Cslib.ReplacementCounting.boolean_mulVec_mem_intMeasurementBox, Cslib.ReplacementCounting.card_intMeasurementBox: Boolean measurement inclusion and box size.
• Cslib.ReplacementCounting.Design.evalRow_eq_of_same_measurements: kernel shifts imply fiber locality via Cslib.SharedSummaries.fiber_locality_of_kernel_shifts.
• Cslib.ReplacementCounting.eval_zero_targetPolynomial, Cslib.ReplacementCounting.natDegree_targetPolynomial_le_of_liftedTotalDegree_le: H(0) = Z and degree bound ≤ d * d₀.
• Cslib.ReplacementCounting.Design.sum_restricted_prod_eq_sum_measurement_fibers: restricted-slice factorization via Cslib.SharedSummaries.sum_prod_eq_sum_measurement_fibers (Lemma 3.2 and equations (3.11), (3.13)).
• Cslib.ReplacementCounting.targetSum_eq_of_taylorJet, Cslib.ReplacementCounting.Design.targetSum_eq_of_taylorJet: exact recovery of Z from confluent Taylor jets via Polynomial.eval_zero_eq_of_taylorJet.
• Cslib.ReplacementCounting.Design.domainExaminationBound_real: 2 Q r C_q (2D+1)^{2τn} 2^{2n/r} bound across nodes, subset pairs, and measurement boxes (eq. (3.12) and Proposition 3.4).

References

• OpenAI, The Exponential Time Hypothesis is False, §§3.1–3.3 and §3.5, Definition 3.1, Lemma 3.2, Proposition 3.4, pp. 21–26.

1. Subset-pair count and weighted binomial bound (equations (3.14)–(3.15))

theorem Cslib.ReplacementCounting.pow_mul_subsetPairCount_le {η : ℝ} (hη₀ : 0 ≤ η) (hη₁ : η ≤ 1) (n q : ℕ) : η ^ q * ↑(subsetPairCount n q) ≤ (1 + 2 * η) ^ n

Weighted binomial bound for subset pairs ([OAI26c], equation (3.15), p. 25): for 0 ≤ η ≤ 1, η ^ q * C_q ≤ (1 + 2 * η) ^ n.

theorem Cslib.ReplacementCounting.subsetPairCount_le_one_div_pow_mul {η : ℝ} (hη₀ : 0 < η) (hη₁ : η ≤ 1) (n q : ℕ) : ↑(subsetPairCount n q) ≤ (1 / η) ^ q * (1 + 2 * η) ^ n

Divided form of the weighted binomial bound ([OAI26c], equation (3.15), p. 25): for 0 < η ≤ 1, C_q ≤ (1 / η) ^ q * (1 + 2 * η) ^ n.

theorem Cslib.ReplacementCounting.subsetPairCount_le_ratio_pow {R Q : ℕ} (hR : 1 ≤ R) (hRQ : R ≤ Q) (n q : ℕ) : ↑(subsetPairCount n q) ≤ (↑Q / ↑R) ^ q * (1 + 2 * (↑R / ↑Q)) ^ n

Specialization of subsetPairCount_le_one_div_pow_mul to η = R / Q for 1 ≤ R ≤ Q ([OAI26c], p. 26): C_q ≤ (Q / R) ^ q * (1 + 2 * (R / Q)) ^ n.

2. Integer measurement boxes and group decompositions

def Cslib.ReplacementCounting.intMeasurementBox (D c : ℕ) : Finset (Fin c → ℤ)

The integer interval box [-D, D]^c bounding c integer linear measurements of {0, 1} assignments when each row has ℓ₁-norm at most D ([OAI26c], pp. 22–23).

theorem Cslib.ReplacementCounting.card_Icc_neg_natCast (D : ℕ) : (Finset.Icc (-↑D) ↑D).card = 2 * D + 1

[-D, D] ∩ ℤ has cardinality 2 * D + 1.

@[simp]

theorem Cslib.ReplacementCounting.card_intMeasurementBox (D c : ℕ) : (intMeasurementBox D c).card = (2 * D + 1) ^ c

intMeasurementBox D c has cardinality (2 * D + 1) ^ c.

theorem Cslib.ReplacementCounting.boolean_dot_mem_Icc {α : Type u_1} [Fintype α] {w : α → ℤ} {D : ℕ} (hw : ∑ i : α, (w i).natAbs ≤ D) (x : α → Bool) : ∑ i : α, w i * BitString.bitVal ℤ (x i) ∈ Finset.Icc (-↑D) ↑D

Any {0, 1} inner product against an integer row of ℓ₁-norm at most D lies in [-D, D] ∩ ℤ.

theorem Cslib.ReplacementCounting.boolean_mulVec_mem_intMeasurementBox {α : Type u_1} [Fintype α] {c D : ℕ} {C : Fin c → α → ℤ} (hC : ∀ (k : Fin c), ∑ i : α, (C k i).natAbs ≤ D) (x : α → Bool) : (fun (k : Fin c) => ∑ i : α, C k i * BitString.bitVal ℤ (x i)) ∈ intMeasurementBox D c

Applying a c-row integer matrix whose rows have ℓ₁-norm at most D to a Boolean vector lands inside intMeasurementBox D c.

theorem Cslib.ReplacementCounting.card_image_boolean_mulVec_le {α : Type u_1} [Fintype α] [DecidableEq α] {c D : ℕ} {C : Fin c → α → ℤ} (hC : ∀ (k : Fin c), ∑ i : α, (C k i).natAbs ≤ D) : (Finset.image (fun (x : α → Bool) (k : Fin c) => ∑ i : α, C k i * BitString.bitVal ℤ (x i)) Finset.univ).card ≤ (2 * D + 1) ^ c

The image of the Boolean cube α → Bool under a c-row integer matrix of row ℓ₁-norm at most D is contained in intMeasurementBox D c and has cardinality at most (2 * D + 1) ^ c.

def Cslib.ReplacementCounting.piGroupEquiv {ι : Type u_1} {G : Type u_2} {α : Type u_3} (group : ι → G) : ((g : G) → { i : ι // group i = g } → α) ≃ (ι → α)

Canonical decomposition of functions on ι into functions on the fibers of group : ι → G, specializing (Equiv.piCongrFiberwise fun _ => Equiv.refl _).symm.

@[simp]

theorem Cslib.ReplacementCounting.piGroupEquiv_apply_of_eq {ι : Type u_1} {G : Type u_2} {α : Type u_3} (group : ι → G) (u : (g : G) → { i : ι // group i = g } → α) {i : ι} {g : G} (hi : group i = g) : (piGroupEquiv group) u i = u g ⟨i, hi⟩

Evaluating piGroupEquiv at i when group i = g selects u g ⟨i, hi⟩.

3. Definition 3.1 (r, τ, D)-replacement design interface

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

Algebraic (r, τ, D)-replacement design at Q distinct nonzero integer evaluation nodes for a finite family of factors s : Finset F with variable scopes scope : ∀ f, κ f → ι ([OAI26c], Definition 3.1(1)–(4), pp. 21–22).

Condition (5) of Definition 3.1 (the integer bit-length bound after clearing (R - 1)! Q!) is a staging property for exact fixed-denominator arithmetic in Appendix B and is kept separate from this algebraic interface.

• two_le_r : 2 ≤ r

  Number of variable groups satisfies 2 ≤ r.

• one_le_D : 1 ≤ D

  Row ℓ₁-bound satisfies 1 ≤ D.

• one_le_R : 1 ≤ R

  Replacement degree bound satisfies 1 ≤ R.

• R_lt_Q : R < Q

  Number of evaluation nodes satisfies R < Q.

• τ_pos : 0 < τ

  Total measurement-row density parameter satisfies 0 < τ.

• τ_le_half : τ ≤ 1 / 2

  Total measurement-row density parameter satisfies τ ≤ 1 / 2.

• nodes : Fin Q → ℤ

  Evaluation nodes in ℤ (in the paper 1, …, Q), pairwise distinct and nonzero.

• nodes_injective : Function.Injective self.nodes
• nodes_ne_zero (t : Fin Q) : self.nodes t ≠ 0
• varGroup : Fin Q → ι → Fin r

  Partition [n] = S_{t,1} ⊔ ⋯ ⊔ S_{t,r} at node t, encoded by i ↦ g.

• card_varGroup_le (t : Fin Q) (g : Fin r) : {i : ι | self.varGroup t i = g}.card * r ≤ 2 * Fintype.card ι

  Group size bound |S_{t,g}| ≤ 2n / r, stated multiplicatively as |S_{t,g}| * r ≤ 2 * n.

• factorGroup : F → Fin Q → Fin r

  Assigned group σ_f(t) ∈ [r] of factor f at node t.

• numRows : Fin Q → Fin r → ℕ

  Number of integer measurement rows c_{t,g} on group g at node t.

• sum_numRows_le (t : Fin Q) : ↑(∑ g : Fin r, self.numRows t g) ≤ 2 * τ * ↑(Fintype.card ι)

  Total measurement row bound ∑_g c_{t,g} ≤ 2 τ n.

• matrix (t : Fin Q) (g : Fin r) : Fin (self.numRows t g) → ι → ℤ

  Integer measurement matrices C_{t,g}, indexed on ι and supported on S_{t,g}.

• matrix_support (t : Fin Q) (g : Fin r) (k : Fin (self.numRows t g)) (i : ι) : self.varGroup t i ≠ g → self.matrix t g k i = 0
• row_l1_le (t : Fin Q) (g : Fin r) (k : Fin (self.numRows t g)) : ∑ i : ι, (self.matrix t g k i).natAbs ≤ D

  Every row of C_{t,g} has sum of absolute values at most D.

• row (f : F) : κ f → ι → Polynomial ℚ

  Polynomial replacement rows P⃗_{f,v}(T) ∈ ℚ[T]^{1 × n}.

• row_eval_zero (f : F) : f ∈ s → ∀ (v : κ f) (i : ι), Polynomial.eval 0 (self.row f v i) = if i = scope f v then 1 else 0

  At T = 0, P⃗_{f,v}(0) = δ_{scope f v}.

• row_natDegree_le (f : F) : f ∈ s → ∀ (v : κ f) (i : ι), (self.row f v i).natDegree ≤ R

  Each replacement entry has univariate degree at most R.

• kernel_zero (t : Fin Q) (f : F) : f ∈ s → ∀ (v : κ f) (g : Fin r), g ≠ self.factorGroup f t → ∀ (ξ : ι → ℚ), (∀ (i : ι), self.varGroup t i ≠ g → ξ i = 0) → (∀ (k : Fin (self.numRows t g)), ∑ i : ι, ↑(self.matrix t g k i) * ξ i = 0) → ∑ i : ι, Polynomial.eval (↑(self.nodes t)) (self.row f v i) * ξ i = 0

  Kernel condition (Definition 3.1(4)): for g ≠ σ_f(t) and ξ supported on S_{t,g}, C_{t,g} ξ = 0 implies ⟨P⃗_{f,v}(nodes t), ξ⟩ = 0.

theorem Cslib.ReplacementCounting.Design.Q_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 < Q

Q is strictly positive because 1 ≤ R < Q.

theorem Cslib.ReplacementCounting.Design.r_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 < r

r is strictly positive because 2 ≤ r.

def Cslib.ReplacementCounting.Design.groupSet {ι : 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 τ) (t : Fin Q) (g : Fin r) : Finset ι

Variables belonging to group g at node t (S_{t,g}).

theorem Cslib.ReplacementCounting.Design.biUnion_groupSet {ι : 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 τ) (t : Fin Q) : Finset.univ.biUnion (M.groupSet t) = Finset.univ

The group sets S_{t,g} partition Finset.univ.

theorem Cslib.ReplacementCounting.Design.disjoint_groupSet {ι : 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 τ) (t : Fin Q) {g₁ g₂ : Fin r} (hne : g₁ ≠ g₂) : Disjoint (M.groupSet t g₁) (M.groupSet t g₂)

Distinct groups at node t are disjoint.

theorem Cslib.ReplacementCounting.Design.card_groupSet_le_div {ι : 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 τ) (t : Fin Q) (g : Fin r) : (M.groupSet t g).card ≤ 2 * Fintype.card ι / r

Natural-division form of the group size bound: #S_{t,g} ≤ (2 * n) / r.

theorem Cslib.ReplacementCounting.Design.card_groupSet_le_real {ι : 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 τ) (t : Fin Q) (g : Fin r) : ↑(M.groupSet t g).card ≤ 2 * ↑(Fintype.card ι) / ↑r

Real-division form of the group size bound: (#S_{t,g} : ℝ) ≤ 2 * n / r.

@[reducible, inline]

abbrev Cslib.ReplacementCounting.Design.LocalCube {ι : 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 τ) (t : Fin Q) (g : Fin r) : Type u_1

Type of local Boolean assignments on group g at node t ({0, 1}^{S_{t,g}}).

theorem Cslib.ReplacementCounting.Design.card_localCube {ι : 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 τ) (t : Fin Q) (g : Fin r) : Fintype.card (M.LocalCube t g) = 2 ^ (M.groupSet t g).card

Cardinality of the local Boolean cube on group g at node t is 2 ^ #S_{t,g}.

def Cslib.ReplacementCounting.Design.localMeasure {ι : 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 τ) (t : Fin Q) (g : Fin r) (u : M.LocalCube t g) : Fin (M.numRows t g) → ℤ

Local integer measurement of u ∈ {0, 1}^{S_{t,g}} under C_{t,g}.

def Cslib.ReplacementCounting.Design.globalMeasure {ι : 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 τ) (t : Fin Q) (g : Fin r) (x : ι → Bool) : Fin (M.numRows t g) → ℤ

Global integer measurement of x : ι → Bool on group g at node t.

theorem Cslib.ReplacementCounting.Design.globalMeasure_piGroupEquiv {ι : 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 τ) (t : Fin Q) (g : Fin r) (u : (h : Fin r) → M.LocalCube t h) : M.globalMeasure t g ((piGroupEquiv (M.varGroup t)) u) = M.localMeasure t g (u g)

Because C_{t,g} is supported on S_{t,g}, the global measurement of a glued assignment agrees with the local measurement on group g.

def Cslib.ReplacementCounting.Design.groupBox {ι : 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 τ) (t : Fin Q) (g : Fin r) : Finset (Fin (M.numRows t g) → ℤ)

Per-group measurement box [-D, D]^{c_{t,g}} at node t.

def Cslib.ReplacementCounting.Design.measurementBox {ι : 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 τ) (t : Fin Q) : Finset ((g : Fin r) → Fin (M.numRows t g) → ℤ)

Full measurement tuple box ∏_g [-D, D]^{c_{t,g}} at node t.

theorem Cslib.ReplacementCounting.Design.localMeasure_mem_groupBox {ι : 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 τ) (t : Fin Q) (g : Fin r) (u : M.LocalCube t g) : M.localMeasure t g u ∈ M.groupBox t g

Every local Boolean assignment on group g has its measurement in M.groupBox t g.

theorem Cslib.ReplacementCounting.Design.card_measurementBox {ι : 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 τ) (t : Fin Q) : (M.measurementBox t).card = (2 * D + 1) ^ ∑ g : Fin r, M.numRows t g

Exact cardinality (2 * D + 1) ^ (∑_g c_{t,g}) of M.measurementBox t ([OAI26c], p. 23).

theorem Cslib.ReplacementCounting.Design.card_measurementBox_le_rpow {ι : 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 τ) (t : Fin Q) : ↑(M.measurementBox t).card ≤ (2 * ↑D + 1) ^ (2 * τ * ↑(Fintype.card ι))

Real-exponent bound (#(M.measurementBox t) : ℝ) ≤ (2D + 1) ^ (2 τ n) from ∑_g c_{t,g} ≤ 2 τ n ([OAI26c], equation (3.12), p. 25).

noncomputable def Cslib.ReplacementCounting.Design.evalRowRat {ι : 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 τ) (t : Fin Q) (f : F) (v : κ f) (x : ι → ℚ) : ℚ

Evaluation of the rational replacement linear form ⟨P⃗_{f,v}(nodes t), x⟩ on x : ι → ℚ.

noncomputable def Cslib.ReplacementCounting.Design.evalRow {ι : 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 τ) (t : Fin Q) (f : F) (v : κ f) (x : ι → Bool) : ℚ

Evaluation of the rational replacement linear form ⟨P⃗_{f,v}(nodes t), x⟩ on a Boolean assignment x : ι → Bool.

theorem Cslib.ReplacementCounting.Design.evalRowRat_eq_of_eq_outside_group {ι : 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 τ) {t : Fin Q} {f : F} (hf : f ∈ s) (v : κ f) {h : Fin r} (hh : h ≠ M.factorGroup f t) {x x' : ι → ℚ} (hout : ∀ (i : ι), M.varGroup t i ≠ h → x i = x' i) (hmeas : ∀ (k : Fin (M.numRows t h)), ∑ i : ι, ↑(M.matrix t h k i) * x i = ∑ i : ι, ↑(M.matrix t h k i) * x' i) : M.evalRowRat t f v x = M.evalRowRat t f v x'

Single-group invariance ([OAI26c], p. 22): if x, x' : ι → ℚ agree outside S_{t,h} for some h ≠ σ_f(t) and have equal C_{t,h} measurements, then ⟨P⃗_{f,v}(nodes t), x⟩ = ⟨P⃗_{f,v}(nodes t), x'⟩.

theorem Cslib.ReplacementCounting.Design.evalRowRat_eq_of_eq_on_assigned_group {ι : 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 τ) {t : Fin Q} {f : F} (hf : f ∈ s) (v : κ f) {x x' : ι → ℚ} (hassigned : ∀ (i : ι), M.varGroup t i = M.factorGroup f t → x i = x' i) (hmeas : ∀ (h : Fin r), h ≠ M.factorGroup f t → ∀ (k : Fin (M.numRows t h)), ∑ i : ι, ↑(M.matrix t h k i) * x i = ∑ i : ι, ↑(M.matrix t h k i) * x' i) : M.evalRowRat t f v x = M.evalRowRat t f v x'

All-groups rational invariance ([OAI26c], p. 22), derived via Cslib.SharedSummaries.fiber_locality_of_kernel_shifts: if x, x' : ι → ℚ agree on the assigned group S_{t,σ_f(t)} and have equal C_{t,h} measurements on all other groups h ≠ σ_f(t), then ⟨P⃗_{f,v}(nodes t), x⟩ = ⟨P⃗_{f,v}(nodes t), x'⟩.

theorem Cslib.ReplacementCounting.Design.evalRow_eq_of_same_measurements {ι : 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 τ) {t : Fin Q} {f : F} (hf : f ∈ s) (v : κ f) {u u' : (h : Fin r) → M.LocalCube t h} (hmeas : ∀ (h : Fin r), M.localMeasure t h (u h) = M.localMeasure t h (u' h)) (hsame : u (M.factorGroup f t) = u' (M.factorGroup f t)) : M.evalRow t f v ((piGroupEquiv (M.varGroup t)) u) = M.evalRow t f v ((piGroupEquiv (M.varGroup t)) u')

Boolean fiber-locality of evalRow: if two grouped Boolean assignments u, u' have the same integer measurements on every group and agree on σ_f(t), then evalRow agrees on their glued Boolean assignments.

noncomputable def Cslib.ReplacementCounting.Design.rowIn {ι : 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 τ) (A : Type u_4) [CommRing A] [Algebra ℚ A] (f : F) (v : κ f) (i : ι) : Polynomial A

Replacement rows mapped into any commutative ℚ-algebra A.

4. Target sum Z, univariate polynomial H(T), and degree bounds (§3.1, eqs. 3.1–3.3)

noncomputable def Cslib.ReplacementCounting.targetSum {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (scope : (f : F) → κ f → ι) (Φ : (f : F) → MvPolynomial (κ f) A) : A

The target Boolean-cube sum Z = ∑_{x ∈ {0, 1}^n} ∏_{f ∈ s} Φ_f((x_v)_{v ∈ I_f}) ([OAI26c], equation (3.1), p. 21).

noncomputable def Cslib.ReplacementCounting.liftedFactorProduct {F : Type u_1} {A : Type u_2} [CommSemiring A] {κ : F → Type u_3} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) : MvPolynomial ((f : F) × κ f) A

Disjoint-incidence product polynomial ∏_{f ∈ s} Φ_f((Y_{f,v})_{v ∈ κ f}) in MvPolynomial (Σ f, κ f) A, whose totalDegree is bounded by d in equation (3.2) of [OAI26c] (p. 21).

theorem Cslib.ReplacementCounting.totalDegree_liftedFactorProduct_le {F : Type u_1} {A : Type u_2} [CommSemiring A] {κ : F → Type u_3} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) : (liftedFactorProduct s Φ).totalDegree ≤ ∑ f ∈ s, (Φ f).totalDegree

The disjoint-incidence product has total degree at most ∑_{f ∈ s} (Φ f).totalDegree.

noncomputable def Cslib.ReplacementCounting.replacementEval {ι : Type u_1} {A : Type u_2} [Fintype ι] [CommRing A] (row : ι → Polynomial A) (x : ι → Bool) : Polynomial A

Linear replacement form ⟨P⃗_{f,v}(T), x⟩ = ∑_i P_{f,v,i}(T) x_i in Polynomial A.

noncomputable def Cslib.ReplacementCounting.targetPolynomial {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) : Polynomial A

Target univariate polynomial H(T) = ∑_{x ∈ {0,1}^n} ∏_{f ∈ s} Φ_f(⟨P⃗_{f,v}(T), x⟩) in Polynomial A ([OAI26c], equation (3.3), p. 21).

theorem Cslib.ReplacementCounting.eval_targetPolynomial {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (t : A) : Polynomial.eval t (targetPolynomial s Φ P) = ∑ x : ι → Bool, ∏ f ∈ s, (MvPolynomial.eval fun (v : κ f) => ∑ i : ι, Polynomial.eval t (P f v i) * BitString.bitVal A (x i)) (Φ f)

Evaluating targetPolynomial at a scalar t : A evaluates every replacement row at t.

theorem Cslib.ReplacementCounting.eval_zero_targetPolynomial {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (scope : (f : F) → κ f → ι) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (hzero : ∀ f ∈ s, ∀ (v : κ f) (i : ι), Polynomial.eval 0 (P f v i) = if i = scope f v then 1 else 0) : Polynomial.eval 0 (targetPolynomial s Φ P) = targetSum s scope Φ

At T = 0, H(0) = Z ([OAI26c], equations (3.1) and (3.3), p. 21): when every replacement row restores δ_{scope f v} at T = 0, (targetPolynomial s Φ P).eval 0 equals targetSum s scope Φ.

theorem Cslib.ReplacementCounting.natDegree_eval₂_polynomial_le {σ : Type u_1} {A : Type u_2} [CommSemiring A] (p : MvPolynomial σ A) (q : σ → Polynomial A) {d₀ : ℕ} (hq : ∀ (v : σ), (q v).natDegree ≤ d₀) : (MvPolynomial.eval₂ Polynomial.C q p).natDegree ≤ p.totalDegree * d₀

Substituting univariate polynomials of degree at most d₀ into a multivariate polynomial p gives a univariate polynomial of natDegree at most p.totalDegree * d₀.

theorem Cslib.ReplacementCounting.natDegree_targetPolynomial_le_of_liftedTotalDegree_le {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) {d d₀ : ℕ} (hd : (liftedFactorProduct s Φ).totalDegree ≤ d) (hP : ∀ f ∈ s, ∀ (v : κ f) (i : ι), (P f v i).natDegree ≤ d₀) : (targetPolynomial s Φ P).natDegree ≤ d * d₀

Degree bound for H(T) from the lifted product degree ([OAI26c], equations (3.2)–(3.3), p. 21): if liftedFactorProduct s Φ has total degree at most d and active replacement rows have natDegree at most d₀, then (targetPolynomial s Φ P).natDegree ≤ d * d₀.

theorem Cslib.ReplacementCounting.natDegree_targetPolynomial_le {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) {d₀ : ℕ} (hP : ∀ f ∈ s, ∀ (v : κ f) (i : ι), (P f v i).natDegree ≤ d₀) : (targetPolynomial s Φ P).natDegree ≤ (∑ f ∈ s, (Φ f).totalDegree) * d₀

Sum-of-degrees bound for H(T): if active replacement rows have natDegree at most d₀, then (targetPolynomial s Φ P).natDegree ≤ (∑_{f ∈ s} (Φ f).totalDegree) * d₀.

theorem Cslib.ReplacementCounting.natDegree_targetPolynomial_le_mul_pred {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [CommRing A] {κ : F → Type u_4} (s : Finset F) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) {d R : ℕ} (hd : ∑ f ∈ s, (Φ f).totalDegree ≤ d) (hP : ∀ f ∈ s, ∀ (v : κ f) (i : ι), (P f v i).natDegree ≤ R - 1) : (targetPolynomial s Φ P).natDegree ≤ d * (R - 1) ∧ (targetPolynomial s Φ P).natDegree ≤ d * R

Specialization to degree-≤ R - 1 replacement rows (as constructed in Section 4 of [OAI26c]): (targetPolynomial s Φ P).natDegree ≤ d * (R - 1) and ≤ d * R.

5. Jet order and generic Hermite recovery of Z = H(0) (equations (3.5)–(3.6))

def Cslib.ReplacementCounting.jetOrder (dH Q : ℕ) : ℕ

Confluent Taylor jet order J = ⌊d_H / Q⌋ + 1 ([OAI26c], equation (3.5), p. 24).

theorem Cslib.ReplacementCounting.jetOrder_pos (dH Q : ℕ) : 0 < jetOrder dH Q

jetOrder is always positive.

theorem Cslib.ReplacementCounting.add_div_eq_jetOrder (dH : ℕ) {Q : ℕ} (hQ : 0 < Q) : (dH + Q) / Q = jetOrder dH Q

Ceiling form ⌈(d_H + 1) / Q⌉ = (d_H + Q) / Q coincides with jetOrder d_H Q for 0 < Q.

theorem Cslib.ReplacementCounting.lt_mul_jetOrder (dH : ℕ) {Q : ℕ} (hQ : 0 < Q) : dH < Q * jetOrder dH Q

When 0 < Q, Q * jetOrder d_H Q strictly exceeds d_H ([OAI26c], eq. (3.5), p. 24).

theorem Cslib.ReplacementCounting.targetSum_eq_of_taylorJet {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] (A : Type u_3) [CommRing A] [Algebra ℚ A] {κ : F → Type u_4} (s : Finset F) (scope : (f : F) → κ f → ι) (Φ : (f : F) → MvPolynomial (κ f) A) (P : (f : F) → κ f → ι → Polynomial A) (hzero : ∀ f ∈ s, ∀ (v : κ f) (i : ι), Polynomial.eval 0 (P f v i) = if i = scope f v then 1 else 0) {N J : ℕ} {nodes : Fin N → ℤ} (hnodes : Function.Injective nodes) (hN : 0 < N) (hJ : 0 < J) (hdeg : (targetPolynomial s Φ P).natDegree < N * J) : targetSum s scope Φ = (↑(Polynomial.hermiteMatrix nodes J).det)⁻¹ • (((Polynomial.hermiteMatrix nodes J).map Int.cast).updateCol (⟨0, hN⟩, ⟨0, hJ⟩) ((Polynomial.taylorJet (fun (i : Fin N) => ↑(nodes i)) J) (targetPolynomial s Φ P))).det

Exact Z = H(0) recovery from confluent Taylor jets ([OAI26c], §3.4, p. 24): given N injective integer nodes (0 < N), jet order 0 < J, and replacement rows over a commutative ℚ-algebra A restoring scope at T = 0 such that (targetPolynomial s Φ P).natDegree < N * J, targetSum s scope Φ is recovered directly from Polynomial.taylorJet via Polynomial.eval_zero_eq_of_taylorJet.

6. Restricted-slice fiber sums and Proposition 3.4 bounds on a Design

def Cslib.ReplacementCounting.Design.restrictedLocalCube {ι : 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 τ) (t : Fin Q) (E : Finset ι) (g : Fin r) : Finset (M.LocalCube t g)

Restricted local Boolean cube X_{g, E} on group g at node t, fixing u_i = true for i ∈ E ∩ S_{t,g} ([OAI26c], Lemma 3.2 proof, p. 23).

noncomputable def Cslib.ReplacementCounting.Design.groupedFactor {ι : 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 τ) {B : Type u_4} [CommRing B] (evalFactor : (f : F) → (κ f → ℚ) → B) (t : Fin Q) (g : Fin r) (u : (h : Fin r) → M.LocalCube t h) : B

Product of factors assigned to group g at node t when each factor f is evaluated on its baseline vector v ↦ M.evalRow t f v x ([OAI26c], equation (3.11), p. 25).

theorem Cslib.ReplacementCounting.Design.prod_groupedFactor_eq {ι : 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 τ) {B : Type u_4} [CommRing B] (evalFactor : (f : F) → (κ f → ℚ) → B) (t : Fin Q) (u : (h : Fin r) → M.LocalCube t h) : ∏ g : Fin r, M.groupedFactor evalFactor t g u = ∏ f ∈ s, evalFactor f fun (v : κ f) => M.evalRow t f v ((piGroupEquiv (M.varGroup t)) u)

Grouping factors by σ_f(t) preserves the full product over s ([OAI26c], equation (3.11), p. 25).

theorem Cslib.ReplacementCounting.Design.groupedFactor_locality {ι : 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 τ) {B : Type u_4} [CommRing B] (evalFactor : (f : F) → (κ f → ℚ) → B) (t : Fin Q) (g : Fin r) (u u' : (h : Fin r) → M.LocalCube t h) (hmeas : ∀ (h : Fin r), M.localMeasure t h (u h) = M.localMeasure t h (u' h)) (hsame : u g = u' g) : M.groupedFactor evalFactor t g u = M.groupedFactor evalFactor t g u'

groupedFactor depends on u only through u g and the integer measurements of all groups.

theorem Cslib.ReplacementCounting.Design.sum_restricted_prod_eq_sum_measurement_fibers {ι : 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 τ) {B : Type u_4} [CommRing B] (evalFactor : (f : F) → (κ f → ℚ) → B) (t : Fin Q) (E : Finset ι) (representative : (y : (g : Fin r) → Fin (M.numRows t g) → ℤ) → (∀ (g : Fin r), ∃ (u : M.LocalCube t g), M.localMeasure t g u = y g) → (g : Fin r) → M.LocalCube t g) (valid : ∀ (y : (g : Fin r) → Fin (M.numRows t g) → ℤ) (hy : ∀ (g : Fin r), ∃ (u : M.LocalCube t g), M.localMeasure t g u = y g) (g : Fin r), M.localMeasure t g (representative y hy g) = y g) : (∑ x : ι → Bool with ∀ i ∈ E, x i = true, ∏ f ∈ s, evalFactor f fun (v : κ f) => M.evalRow t f v x) = ∑ y ∈ M.measurementBox t, SharedSummaries.fiberContribution (M.localMeasure t) (M.restrictedLocalCube t E) (M.groupedFactor evalFactor t) representative y

Restricted-slice measurement-fiber factorization ([OAI26c], Lemma 3.2 and equations (3.11), (3.13), pp. 22–25): for any subset E ⊆ ι, ring B, evaluator evalFactor, and valid unrestricted fiber representative selector, the sum over {x : ι → Bool | ∀ i ∈ E, x i = true} factors into per-group sums over M.measurementBox t via Cslib.SharedSummaries.sum_prod_eq_sum_measurement_fibers.

noncomputable def Cslib.ReplacementCounting.Design.targetPoly {ι : 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 τ) {A : Type u_4} [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) : Polynomial A

Target polynomial H(T) ∈ A[T] instantiated with M.rowIn A.

theorem Cslib.ReplacementCounting.Design.eval_zero_targetPoly {ι : 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 τ) {A : Type u_4} [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) : Polynomial.eval 0 (M.targetPoly Φ) = targetSum s scope Φ

At T = 0, (M.targetPoly Φ).eval 0 = targetSum s scope Φ.

theorem Cslib.ReplacementCounting.Design.natDegree_targetPoly_le {ι : 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 τ) {A : Type u_4} [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) {d : ℕ} (hd : (liftedFactorProduct s Φ).totalDegree ≤ d) : (M.targetPoly Φ).natDegree ≤ d * R

Degree bound (M.targetPoly Φ).natDegree ≤ d * R when (liftedFactorProduct s Φ).totalDegree ≤ d ([OAI26c], equations (3.2)–(3.3), p. 21).

theorem Cslib.ReplacementCounting.Design.eval_nodes_targetPoly_eq_sum_measurement_fibers {ι : 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 τ) {A : Type u_4} [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) (t : Fin Q) (representative : (y : (g : Fin r) → Fin (M.numRows t g) → ℤ) → (∀ (g : Fin r), ∃ (u : M.LocalCube t g), M.localMeasure t g u = y g) → (g : Fin r) → M.LocalCube t g) (valid : ∀ (y : (g : Fin r) → Fin (M.numRows t g) → ℤ) (hy : ∀ (g : Fin r), ∃ (u : M.LocalCube t g), M.localMeasure t g u = y g) (g : Fin r), M.localMeasure t g (representative y hy g) = y g) : Polynomial.eval (↑(M.nodes t)) (M.targetPoly Φ) = ∑ y ∈ M.measurementBox t, SharedSummaries.fiberContribution (M.localMeasure t) (M.restrictedLocalCube t ∅) (M.groupedFactor (fun (f : F) (q : κ f → ℚ) => (MvPolynomial.eval (⇑(algebraMap ℚ A) ∘ q)) (Φ f)) t) representative y

Unrestricted node evaluation H(nodes t) via measurement fibers ([OAI26c], §3.3, p. 23): evaluating M.targetPoly Φ at M.nodes t equals the E = ∅ measurement-fiber sum over M.measurementBox t.

noncomputable def Cslib.ReplacementCounting.Design.shiftedFactorEval {ι : 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 τ) {A : Type u_4} [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) (t : Fin Q) (U : Finset ι) (f : F) (qBaseline : κ f → ℚ) : Polynomial A

Factor Φ_{f, U}(x; z) ∈ Polynomial A at node t after fixing X⃗ = 1_U in the Taylor correction ([OAI26c], equations (3.8) and (3.11), pp. 24–25).

theorem Cslib.ReplacementCounting.Design.sum_restricted_shiftedFactor_eq_sum_measurement_fibers {ι : 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 τ) {A : Type u_4} [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) (t : Fin Q) (E U : Finset ι) (representative : (y : (g : Fin r) → Fin (M.numRows t g) → ℤ) → (∀ (g : Fin r), ∃ (u : M.LocalCube t g), M.localMeasure t g u = y g) → (g : Fin r) → M.LocalCube t g) (valid : ∀ (y : (g : Fin r) → Fin (M.numRows t g) → ℤ) (hy : ∀ (g : Fin r), ∃ (u : M.LocalCube t g), M.localMeasure t g u = y g) (g : Fin r), M.localMeasure t g (representative y hy g) = y g) : (∑ x : ι → Bool with ∀ i ∈ E, x i = true, ∏ f ∈ s, M.shiftedFactorEval Φ t U f fun (v : κ f) => M.evalRow t f v x) = ∑ y ∈ M.measurementBox t, SharedSummaries.fiberContribution (M.localMeasure t) (M.restrictedLocalCube t E) (M.groupedFactor (M.shiftedFactorEval Φ t U) t) representative y

Specialization of sum_restricted_prod_eq_sum_measurement_fibers to the Taylor-shifted factors Φ_{f, U}(x; z) in Polynomial A ([OAI26c], equations (3.11) and (3.13), p. 25).

theorem Cslib.ReplacementCounting.Design.targetSum_eq_of_taylorJet {ι : 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 τ) (A : Type u_4) [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) {d J : ℕ} (hd : (liftedFactorProduct s Φ).totalDegree ≤ d) (hJ : 0 < J) (hQJ : d * R < Q * J) : targetSum s scope Φ = (↑(Polynomial.hermiteMatrix M.nodes J).det)⁻¹ • (((Polynomial.hermiteMatrix M.nodes J).map Int.cast).updateCol (⟨0, ⋯⟩, ⟨0, hJ⟩) ((Polynomial.taylorJet (fun (i : Fin Q) => ↑(M.nodes i)) J) (M.targetPoly Φ))).det

Hermite jet recovery of Z for a Design ([OAI26c], equations (3.5)–(3.6) and Proposition 3.4, pp. 24–25): whenever (liftedFactorProduct s Φ).totalDegree ≤ d and d * R < Q * J (in particular for J = jetOrder (d * R) Q), targetSum s scope Φ equals the Hermite determinant expression in the order-J Taylor jets of M.targetPoly Φ at M.nodes.

theorem Cslib.ReplacementCounting.Design.targetSum_eq_of_taylorJet_jetOrder {ι : 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 τ) (A : Type u_4) [CommRing A] [Algebra ℚ A] (Φ : (f : F) → MvPolynomial (κ f) A) {d : ℕ} (hd : (liftedFactorProduct s Φ).totalDegree ≤ d) : targetSum s scope Φ = (↑(Polynomial.hermiteMatrix M.nodes (jetOrder (d * R) Q)).det)⁻¹ • (((Polynomial.hermiteMatrix M.nodes (jetOrder (d * R) Q)).map Int.cast).updateCol (⟨0, ⋯⟩, ⟨0, ⋯⟩) ((Polynomial.taylorJet (fun (i : Fin Q) => ↑(M.nodes i)) (jetOrder (d * R) Q)) (M.targetPoly Φ))).det

Specialization of Design.targetSum_eq_of_taylorJet at the canonical jet order J = jetOrder (d * R) Q = ⌊d * R / Q⌋ + 1 ([OAI26c], equation (3.5), p. 24).

theorem Cslib.ReplacementCounting.Design.two_mul_card_measurementBox_mul_sum_card_localCube {ι : 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 τ) (t : Fin Q) : 2 * (M.measurementBox t).card * ∑ g : Fin r, Fintype.card (M.LocalCube t g) = (2 * (2 * D + 1) ^ ∑ g : Fin r, M.numRows t g) * ∑ g : Fin r, 2 ^ (M.groupSet t g).card

Exact natural-number two-pass local-cube scan count 2 (2D + 1) ^ (∑_g c_{t,g}) ∑_g 2 ^ |S_{t,g}| at node t ([OAI26c], Lemma 3.2, p. 22).

theorem Cslib.ReplacementCounting.Design.sum_card_localCube_le {ι : 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 τ) (t : Fin Q) : ∑ g : Fin r, Fintype.card (M.LocalCube t g) ≤ r * 2 ^ (2 * Fintype.card ι / r)

Sum of local Boolean cube cardinalities across all r groups at node t is at most r * 2 ^ ((2 * n) / r).

theorem Cslib.ReplacementCounting.Design.singlePairScanBound_real {ι : 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 τ) (t : Fin Q) : 2 * ↑(M.measurementBox t).card * ∑ g : Fin r, ↑(Fintype.card (M.LocalCube t g)) ≤ 2 * ↑r * (2 * ↑D + 1) ^ (2 * τ * ↑(Fintype.card ι)) * 2 ^ (2 * ↑(Fintype.card ι) / ↑r)

Per-pair Boolean-vector scan bound at node t ([OAI26c], equation (3.12), p. 25): two scans of all r local cubes across every tuple in M.measurementBox t inspect at most 2 * r * (2D + 1) ^ (2 τ n) * 2 ^ (2 n / r) local assignments.

theorem Cslib.ReplacementCounting.Design.domainExaminationBound_real {ι : 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 : ℕ) : ∑ 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 * ↑(subsetPairCount (Fintype.card ι) q) * (2 * ↑D + 1) ^ (2 * τ * ↑(Fintype.card ι)) * 2 ^ (2 * ↑(Fintype.card ι) / ↑r)

Total finite-domain examination bound across all Q nodes and C_q subset pairs ([OAI26c], Proposition 3.4, p. 25): summing the two-pass local-cube scan count over all t : Fin Q and all subset pairs (E, U) with #E ≤ q and U ⊆ E yields at most 2 Q r C_q (2D + 1) ^ (2 τ n) 2 ^ (2 n / r).