The deterministic core of Theorem 3.2

Proof of Theorem 3.2 of Becchetti et al. (arXiv:1511.03927), inequality (3), with the explicit number of rounds T(n, δ) = ⌈log (4n³) / log (1 + δ)⌉ + 1. By Lemma C.1, x⁽ᵗ⁻¹⁾(u) - x⁽ᵗ⁾(u) = α₂ λ₂ᵗ⁻¹ (1 - λ₂) χ(u) + (e⁽ᵗ⁻¹⁾(u) - e⁽ᵗ⁾(u)). The main term has absolute value at least 2b λ₂ᵗ⁻¹ / (nd) because ⟨x, χ⟩ is a nonzero even integer, while the error is at most 2 λᵗ⁻¹ √(2n). Since λ₂ ≥ (1 + δ) λ, (1 + δ)ᵗ⁻¹ ≥ 4n³, b ≥ 1 (connectivity) and d < 2n, the main term wins and fixes the sign.

theorem Averaging.one_le_cross {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hconn : G.Connected) (hn : 0 < n) : 1 ≤ b

On a connected clustered graph, some edge crosses the cut, so b ≥ 1.

theorem Averaging.cross_le_degree {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hn : 0 < n) : b ≤ d

theorem Averaging.degree_lt_two_mul {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (v : V) : d < 2 * n

theorem Averaging.dotProduct_clusterIndicator_eq {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (hP : IsBalancedPartition V₁ V₂ n) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) : x ⬝ᵥ clusterIndicator V₁ V₂ = 2 * (↑{v : V | x v = clusterIndicator V₁ V₂ v}.card - ↑n)

For a sign vector x, ⟨x, χ⟩ = 2 (k - n) where k counts the nodes with x v = χ v.

theorem Averaging.two_le_abs_dotProduct {V : Type u_1} [Fintype V] [DecidableEq V] {V₁ V₂ : Finset V} {n : ℕ} (hP : IsBalancedPartition V₁ V₂ n) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) (h : x ⬝ᵥ clusterIndicator V₁ V₂ ≠ 0) : 2 ≤ |x ⬝ᵥ clusterIndicator V₁ V₂|

⟨x, χ⟩ is a sum of 2n signs, hence even: if nonzero, it is at least 2 in absolute value.

theorem Averaging.one_le_reconstructionTime (n : ℕ) (δ : ℝ) : 1 ≤ reconstructionTime n δ

theorem Averaging.four_mul_cube_le_one_add_pow {n : ℕ} (hn : 0 < n) {δ : ℝ} (hδ : 0 < δ) {t : ℕ} (ht : reconstructionTime n δ ≤ t) : 4 * ↑n ^ 3 ≤ (1 + δ) ^ (t - 1)

After T(n, δ) rounds, (1 + δ)ᵗ⁻¹ ≥ 4n³.

theorem Averaging.sign_add_eq_of_abs_lt {M E : ℝ} (h : |E| < |M|) : SignType.sign (M + E) = SignType.sign M

A perturbation smaller than the main term does not change the sign.

theorem Averaging.sign_sub_eq_of_bounds {y₀ y₁ α₁ S c μ lam K N : ℝ} {s : ℕ} (h₀ : |y₀ - (α₁ + S / N * μ ^ s * c)| ≤ lam ^ s * K) (h₁ : |y₁ - (α₁ + S / N * μ ^ (s + 1) * c)| ≤ lam ^ (s + 1) * K) (hc : |c| = 1) (hN : 0 < N) (hμ : 0 < μ) (hμ1 : μ < 1) (hlam0 : 0 ≤ lam) (hlam1 : lam ≤ 1) (hK : 0 ≤ K) (hdom : 2 * lam ^ s * K < |S| * (μ ^ s * (1 - μ) / N)) : SignType.sign (y₀ - y₁) = SignType.sign (S * c)

Real-arithmetic core of inequality (3): if two consecutive values are within λˢ K and λˢ⁺¹ K of α₁ + (S/N) μˢ c and α₁ + (S/N) μˢ⁺¹ c, and the error bound 2 λˢ K is below the main term |S| μˢ (1 - μ) / N, then sgn (y₀ - y₁) = sgn (S c).

theorem Averaging.sign_avgIter_sub_eq_aux {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hconn : G.Connected) {δ : ℝ} (hδ : 0 < δ) (hgap : (1 + δ) * maxAbsOtherEigenvalue G d < 1 - 2 * ↑b / ↑d) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) (hχ : x ⬝ᵥ clusterIndicator V₁ V₂ ≠ 0) {t : ℕ} (ht : reconstructionTime n δ ≤ t) (u : V) : SignType.sign (avgIter G (t - 1) x u - avgIter G t x u) = SignType.sign (x ⬝ᵥ clusterIndicator V₁ V₂ * clusterIndicator V₁ V₂ u)

Theorem 3.2, deterministic core (inequality (3) of its proof).

theorem Averaging.exists_sign_avgIter_sub_clusters_aux {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hconn : G.Connected) {δ : ℝ} (hδ : 0 < δ) (hgap : (1 + δ) * maxAbsOtherEigenvalue G d < 1 - 2 * ↑b / ↑d) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) (hχ : x ⬝ᵥ clusterIndicator V₁ V₂ ≠ 0) : ∃ (s : SignType), s ≠ 0 ∧ ∀ (t : ℕ), reconstructionTime n δ ≤ t → (∀ u ∈ V₁, SignType.sign (avgIter G (t - 1) x u - avgIter G t x u) = s) ∧ ∀ u ∈ V₂, SignType.sign (avgIter G (t - 1) x u - avgIter G t x u) = -s

Theorem 3.2, deterministic core, cluster form: from round T(n, δ) on, the sign of x⁽ᵗ⁻¹⁾(u) - x⁽ᵗ⁾(u) is sgn ⟨x, χ⟩ on V₁ and -sgn ⟨x, χ⟩ on V₂.

theorem Averaging.color_eq_true_iff {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (x : V → ℝ) (t : ℕ) (u : V) : color G x t u = true ↔ SignType.sign (avgIter G (t - 1) x u - avgIter G t x u) ≠ 1

The protocol's coloring: blue (true) exactly when x⁽ᵗ⁻¹⁾(u) - x⁽ᵗ⁾(u) is not positive.

theorem Averaging.isStrongReconstruction_color_aux {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {V₁ V₂ : Finset V} {n d b : ℕ} (hG : IsClusteredRegular G V₁ V₂ n d b) (hconn : G.Connected) {δ : ℝ} (hδ : 0 < δ) (hgap : (1 + δ) * maxAbsOtherEigenvalue G d < 1 - 2 * ↑b / ↑d) {x : V → ℝ} (hx : ∀ (v : V), x v = 1 ∨ x v = -1) (hχ : x ⬝ᵥ clusterIndicator V₁ V₂ ≠ 0) {t : ℕ} (ht : reconstructionTime n δ ≤ t) : IsStrongReconstruction V₁ V₂ (color G x t)

Theorem 3.2, deterministic core, coloring form.