Theorem 8: Expander Violated Checks

For a Tanner code on an expander graph, a vector x of small Hamming weight has |∂(x)| ≥ β|x|, where β = β' · β'' combines edge-to-vertex expansion (Lem_2) with vertex-to-edge-boundary expansion (Lem_3).

Main Results

• expanderViolatedChecks: The main bound |∂(x)| ≥ β' · β'' · |x|.

β parameters

noncomputable def ExpanderViolatedChecks.beta' (s lam2 alpha : ℝ) : ℝ

The edge-to-vertex expansion parameter β': β' = (sqrt(λ₂² + 4s(s-λ₂)α) - λ₂) / (s(s-λ₂)α).

Equations

• ExpanderViolatedChecks.beta' s lam2 alpha = EdgeToVertexExpansion.betaParam s lam2 alpha

noncomputable def ExpanderViolatedChecks.beta'' (s lam2 alpha dL : ℝ) : ℝ

The vertex-to-edge-boundary expansion parameter β'': β'' = ((dL - 1 - λ₂) - αs(s - λ₂)) / (dL - 1). This is obtained by applying Lem_3 with b = dL - 1 and α' = αs. Note: The paper's stated formula uses 4α/s and denominator dL, but the proof derivation yields αs (since |S| ≤ 2α|X₁| = αs|X₀|) and uses b = dL - 1 to ensure all high-expansion vertices have violated checks.

Equations

• ExpanderViolatedChecks.beta'' s lam2 alpha dL = (dL - 1 - lam2 - alpha * s * (s - lam2)) / (dL - 1)

Hamming weight of the differential image

noncomputable def ExpanderViolatedChecks.differentialWeight {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (x : ↑G.edgeSet → 𝔽₂) : ℕ

The Hamming weight of the differential output ∂(x), counting the number of vertices v where the local check parityCheck(localView_v(x)) is nonzero.

Equations

• ExpanderViolatedChecks.differentialWeight G Λ parityCheck x = {v : V | parityCheck ((localView Λ v) x) ≠ 0}.card

Helper: vertices in A have violated checks

theorem ExpanderViolatedChecks.violated_check_of_small_support {m s : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) (hdL_pos : 0 < dL) (x : Fin s → 𝔽₂) (hx_ne : x ≠ 0) (hx_wt : hammingWeight x ≤ dL - 1) : parityCheck x ≠ 0

For a vertex v ∈ A (high expansion), if v is incident to at most dL - 1 edges in the support of x, then the local check at v is violated.

Helper: counting edges within S incident to v

noncomputable def ExpanderViolatedChecks.supportEdgesAtVertex {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) (v : V) : ℕ

The number of edges in supportEdges incident to vertex v.

Equations

• ExpanderViolatedChecks.supportEdgesAtVertex G c v = {e ∈ SipserSpielman.supportEdges G c | v ∈ e}.card

Helper: edges in support are within S = incidentToSupport

theorem ExpanderViolatedChecks.supportEdges_both_endpoints_in_S {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) (e : Sym2 V) (he : e ∈ SipserSpielman.supportEdges G c) (w : V) (hw : w ∈ e) : w ∈ SipserSpielman.incidentToSupport G c

Every edge in the support has both endpoints in the incident vertex set S.

Helper: support edges are disjoint from edge boundary

theorem ExpanderViolatedChecks.supportEdge_not_in_edgeBoundary {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) (e : Sym2 V) (he : e ∈ SipserSpielman.supportEdges G c) : e ∉ CheegerConstant.edgeBoundary G (SipserSpielman.incidentToSupport G c)

Edges in the support are NOT in the edge boundary δS, since both endpoints are in S.

Helper: edges at v split into boundary and within-S

theorem ExpanderViolatedChecks.withinS_plus_boundary_eq_degree {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (S : Finset V) (v : V) (hv : v ∈ S) : have withinS := {e ∈ G.edgeFinset | v ∈ e ∧ ∀ w ∈ e, w ∈ S}.card; have boundary := (RelativeVertexToEdgeExpansion.edgeBoundaryAtVertex G S v).card; have otherS := {e ∈ G.edgeFinset | v ∈ e ∧ (∀ w ∈ e, w ∈ S) ∧ ¬∃ w ∈ e, w ∉ S}.card; boundary + withinS ≤ s

For v ∈ S, the number of within-S edges at v plus boundary edges at v equals the degree s.

Helper: Hamming weight of localView bounded by non-boundary edges

theorem ExpanderViolatedChecks.localView_weight_le_withinS {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) (c : ↑G.edgeSet → 𝔽₂) (S : Finset V) (hsupp : ∀ (e : ↑G.edgeSet), c e ≠ 0 → ∀ w ∈ ↑e, w ∈ S) (v : V) : hammingWeight ((localView Λ v) c) ≤ {e ∈ G.edgeFinset | v ∈ e ∧ ∀ w ∈ e, w ∈ S}.card

The Hamming weight of the local view at v is at most the number of within-S edges at v. Combined with withinS_plus_boundary_eq_degree, this gives hammingWeight(localView v c) ≤ s - |(δS)_v|.

theorem ExpanderViolatedChecks.localView_weight_add_boundary_le {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) (hreg : G.IsRegularOfDegree s) (c : ↑G.edgeSet → 𝔽₂) (S : Finset V) (v : V) (hv : v ∈ S) (hsupp : ∀ (e : ↑G.edgeSet), c e ≠ 0 → ∀ w ∈ ↑e, w ∈ S) : hammingWeight ((localView Λ v) c) + (RelativeVertexToEdgeExpansion.edgeBoundaryAtVertex G S v).card ≤ s

Combined: Hamming weight of localView + boundary edges ≤ s.

Connection lemmas

theorem ExpanderViolatedChecks.supportEdges_card_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : (SipserSpielman.supportEdges G c).card = SipserSpielman.edgeHammingWeight G c

The card of supportEdges equals edgeHammingWeight.

theorem ExpanderViolatedChecks.incidentToSupport_eq_incidentVertices {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : SipserSpielman.incidentToSupport G c = AlonChungContrapositive.incidentVertices (SipserSpielman.supportEdges G c)

incidentToSupport equals incidentVertices of supportEdges.

theorem ExpanderViolatedChecks.regular_handshaking {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) : 2 * G.edgeFinset.card = s * Fintype.card V

Handshaking lemma for regular graphs: 2 * |E| = s * |V|.

theorem ExpanderViolatedChecks.incidentToSupport_card_le_twice {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (c : ↑G.edgeSet → 𝔽₂) : (SipserSpielman.incidentToSupport G c).card ≤ 2 * SipserSpielman.edgeHammingWeight G c

|incidentToSupport G c| ≤ 2 * |support G c| (each edge contributes ≤ 2 vertices).

theorem ExpanderViolatedChecks.incidentToSupport_card_le_alphaS {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (s : ℕ) (hreg : G.IsRegularOfDegree s) (alpha : ℝ) (halpha_pos : 0 < alpha) (x : ↑G.edgeSet → 𝔽₂) (hx_le : ↑(SipserSpielman.edgeHammingWeight G x) ≤ alpha * ↑G.edgeFinset.card) : ↑(SipserSpielman.incidentToSupport G x).card ≤ alpha * ↑s * ↑(Fintype.card V)

|S| ≤ αs · |V| where S = incidentToSupport G x.

Violated checks at high-expansion vertices

theorem ExpanderViolatedChecks.localView_ne_zero_of_incidentToSupport {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) (c : ↑G.edgeSet → 𝔽₂) (v : V) (hv : v ∈ SipserSpielman.incidentToSupport G c) : (localView Λ v) c ≠ 0

For v ∈ incidentToSupport G c, the local view localView Λ v c is nonzero.

theorem ExpanderViolatedChecks.differentialWeight_ge_highExpansion {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] {s : ℕ} (Λ : Labeling G) (hreg : G.IsRegularOfDegree s) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (c : ↑G.edgeSet → 𝔽₂) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) (hdL_pos : 0 < dL) : have S := SipserSpielman.incidentToSupport G c; have A := RelativeVertexToEdgeExpansion.highExpansionVertices G S s (↑dL - 1); A.card ≤ differentialWeight G Λ parityCheck c

The differentialWeight is at least the number of high-expansion vertices (with parameter b = dL - 1). Each such vertex has a violated local check.

Main Theorem

theorem ExpanderViolatedChecks.beta'_pos (s : ℕ) (lam2 alpha : ℝ) (hs : 1 ≤ s) (hlam2_lt_s : lam2 < ↑s) (halpha_pos : 0 < alpha) : 0 < beta' (↑s) lam2 alpha

β' is positive when s ≥ 1, λ₂ < s, and α > 0. The discriminant λ₂² + 4s(s-λ₂)α > λ₂², so √(disc) > |λ₂| ≥ λ₂ (numerator > 0) and s(s-λ₂)α > 0 (denominator > 0).

theorem ExpanderViolatedChecks.expanderViolatedChecks {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hconn : G.Connected) (s : ℕ) (hs : 1 ≤ s) (hreg : G.IsRegularOfDegree s) (hcard : 2 ≤ Fintype.card V) {m : ℕ} (parityCheck : (Fin s → 𝔽₂) →ₗ[𝔽₂] Fin m → 𝔽₂) (Λ : Labeling G) (dL : ℕ) (hdL : dL = (ClassicalCode.ofParityCheck parityCheck).distance) (hdL_pos : 0 < dL) (hdL_le_s : dL ≤ s) (lam2 : ℝ) (hlam2 : lam2 = GraphExpansion.secondLargestEigenvalue G hcard) (hlam2_lt_s : lam2 < ↑s) (alpha : ℝ) (halpha_pos : 0 < alpha) (halpha_le : alpha ≤ 1) (x : ↑G.edgeSet → 𝔽₂) (hx_le : ↑(SipserSpielman.edgeHammingWeight G x) ≤ alpha * ↑G.edgeFinset.card) : ↑(differentialWeight G Λ parityCheck x) ≥ beta' (↑s) lam2 alpha * beta'' (↑s) lam2 alpha ↑dL * ↑(SipserSpielman.edgeHammingWeight G x)

Expander Violated Checks (Theorem 8). For a Tanner code on an s-regular expander graph with second-largest eigenvalue λ₂, local code distance dL ≤ s, and a vector x with |x| ≤ α|X₁|, we have |∂(x)| ≥ β' · β'' · |x| where β' = (√(λ₂² + 4s(s-λ₂)α) - λ₂) / (s(s-λ₂)α) and β'' = ((dL - 1 - λ₂) - αs(s - λ₂)) / (dL - 1).