Research proof index

This lemma proves the final algebraic step in the DG25 Theorem 3.1 proof. It shows that if R > e + 1, then e * (R / (R - 1)) < e + 1. The intuition is that the fraction R / (R - 1) is always greater than 1, but as R gets larger, it gets closer to 1. The hypothesis R > e + 1 provides a strong enough bound to ensure the product e * (fraction) do...

Lemma 3.3 (Part 2): Bound on agreeing cells inside D For any column j that is in the disagreement set D, there is at most one parameter r in R* such that the columns Uᵣ j and Vᵣ j agree. Therefore, the total number of agreeing cells (r, j) with j ∈ D is at most |D|.

Lemma 3.3 (Part 1): Bound on agreeing cells outside D The set of agreeing cells (r, j) where j ∉ D is exactly the Cartesian product of R* and Dᶜ (the columns not in D).

Helper Lemma relating row distance to interleaved distance (as derived from DG25): d((Uᵣ)ᵢ, C) ≤ d^m(Uᵣ, C^m)

This lemma proves the final algebraic step in the DG25 Theorem 3.1 proof. It shows that if R > e + 1, then e * (R / (R - 1)) < e + 1. The intuition is that the fraction R / (R - 1) is always greater than 1, but as R gets larger, it gets closer to 1. The hypothesis R > e + 1 provides a strong enough bound to ensure the product e * (fraction) do...

inductively to each such matrix, we conclude that, for each r_{ϑ-1} ∈ R*, d^{2^{ϑ-1}}((1-r_{ϑ-1}) · U₀ + r_{ϑ-1} · U₁, C^{2^{ϑ-1}}) ≤ e -/ lemma correlatedAgreement_of_mem_R_star_tensor {ϑ_pred : ℕ} (ih : δ_ε_multilinearCorrelatedAgreement_Nat (F := F) (A := A) (ι := ι) (C := MC) (ϑ := ϑ_pred) (e := e) (ε := ε)) (u : Fin (2 ^ (ϑ_pred + 1)) → (Word A ι...