The first moment of Dinur's powering step

Counting, for a fixed faulty dart of R and a fixed crossing position, the killed-power constraints that the dart breaks — those whose walk crosses it and whose two ends both hold the decoded opinion about the dart's endpoints.

WalkSplit.card_label_crossing already counts such labels as (prefix count) * (suffix count) * (fibre weight), for arbitrary conditions on the two pieces. Here the conditions are the ones the powered constraint actually reads, and then each count is by definition a truthCount — the quantity KilledPlurality.card_le_mul_sum_truthCount bounds from below.

That is the whole point of the killed walk law: the prefix and suffix conditions concern different vertices and independent lengths, so summing over both positions multiplies two plurality bounds instead of entangling them.

Main results

• RegCSP.opinionOf_eq_startIdx, RegCSP.opinionOf_eq_endIdx — the counted conditions are the constraint's own two terms
• RegCSP.card_good_crossing — the count, as a product of two truthCounts and the fibre weight
• RegCSP.not_satisfies_of_good_crossing — every counted crossing breaks its constraint
• weight_factor — the crossing weight is the product of the two plurality weights, up to a fixed normaliser
• sum_crossing_factor, sum_goodCount_factor — hence the double sum over positions is a product of two weighted sums
• geom_tail_le, RegCSP.truthCount_le — the discarded positions carry geometrically little weight
• RegCSP.card_le_mul_sum_truthCount_half — plurality survives the restriction to half the range
• RegCSP.card_good_crossing_sq — the count indexed by the two lengths
• RegCSP.halfSum, pluralityLoss, RegCSP.per_dart_lower — the first moment for a single dart of R
• RegCSP.sum_dart_lower — summed over all the failed darts
• RegCSP.goodCrossings, RegCSP.mem_unsatDarts_of_goodCrossings_nonempty — the count the second-moment method uses, and its support condition
• RegCSP.sum_sq_goodCrossings — its second moment, as a sum over pairs
• RegCSP.goodPos, RegCSP.card_pairs_goodPos — the same positions indexed by naturals, so summation order can be exchanged
• RegCSP.sum_card_pairs_eq — that exchange, carried out
• RegCSP.card_both_good_le — two good crossings imply two failed crossings of the underlying walk
• RegCSP.sum_pairs_bound — the second moment's pair term, bounded
• RegCSP.sum_sq_goodCrossings_le — the second moment of the crossing count
• RegCSP.sum_card_goodPos_eq — the first moment, with counting exchanged
• RegCSP.sum_over_len_le — summing over effective lengths stays within the constraints good at a position
• RegCSP.mem_goodPos_of_crossing — a counted crossing of a failed dart is a good position
• RegCSP.crossingSet, RegCSP.sum_crossingSet_le — the counted sets, and that different darts contribute disjointly
• RegCSP.sum_len_pos_le, RegCSP.sum_Cd_le_sum_goodCrossings — the first moment is bounded by the total crossing count
• RegCSP.crossCount, RegCSP.sum_goodCrossings_ge — the first moment in closed form
• RegCSP.card_unsatDarts_ge — the second-moment bound on unsatisfied constraints
• RegCSP.powering_soundness — soundness of the killed powering step
• RegCSP.unsatFrac_killedPow_ge, RegCSP.le_unsatVal_killedPow — the same bound on the unsatisfied fraction, and on the value

theorem Complexity.weight_factor (deg q : ℕ) {T i j : ℕ} (h : i + j + 1 < T) : deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)) * (deg ^ (T + 1) * q ^ T) = deg ^ (T - i) * ((q - 1) ^ i * q ^ (T - i - 1)) * (deg ^ (T - j) * ((q - 1) ^ j * q ^ (T - j - 1))) * (q - 1)

The weights factorise. The fibre weight of a walk of length i + j + 1 is, up to the fixed normaliser deg ^ (T+1) * q ^ T, the product of the weights of lengths i and j times q - 1.

This identity is why the first moment splits: summing a product truthCount a i * truthCount b j against the crossing weight is the same as multiplying two sums each weighted exactly as the plurality bound weights them. Geometric weights are what make this work, and geometric weights are what the killed walk law produces.

theorem Complexity.sum_crossing_factor (deg q T H : ℕ) (hH : 2 * H + 1 < T) (f g : ℕ → ℕ) : (∑ i ∈ Finset.range (H + 1), ∑ j ∈ Finset.range (H + 1), f i * g j * (deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))) * (deg ^ (T + 1) * q ^ T) = (q - 1) * ((∑ i ∈ Finset.range (H + 1), f i * (deg ^ (T - i) * ((q - 1) ^ i * q ^ (T - i - 1)))) * ∑ j ∈ Finset.range (H + 1), g j * (deg ^ (T - j) * ((q - 1) ^ j * q ^ (T - j - 1))))

The double sum factorises. Over a square of positions small enough that i + j + 1 never reaches the truncation T, the crossing sum is — up to the normaliser — (q-1) times the product of the two weighted sums that the plurality bound controls.

Restricting to a square rather than the full triangle i + j + 1 < T is what makes this an identity: the triangle is not a product region. The tail thrown away is geometrically small.

theorem Complexity.geom_tail_le {q : ℕ} (hq : 0 < q) (T n k : ℕ) : T - k = n → k ≤ T → ∑ m ∈ Finset.Ico k T, (q - 1) ^ m * q ^ (T - 1 - m) ≤ (q - 1) ^ k * q ^ (T - k)

The geometric tail. The weights decay geometrically, so the positions beyond k carry at most (q-1)^k * q^(T-k) — a ((q-1)/q)^k fraction of the total. This is what makes both the truncation term and the restriction to a square of positions harmless.

theorem Complexity.sum_goodCount_factor (deg q T H : ℕ) (hH : 2 * H + 1 < T) (f g : ℕ → ℕ) (C : ℕ → ℕ → ℕ) (hC : ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), C i j = f i * g j * (deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))) : (∑ i ∈ Finset.range (H + 1), ∑ j ∈ Finset.range (H + 1), C i j) * (deg ^ (T + 1) * q ^ T) = (q - 1) * ((∑ i ∈ Finset.range (H + 1), f i * (deg ^ (T - i) * ((q - 1) ^ i * q ^ (T - i - 1)))) * ∑ j ∈ Finset.range (H + 1), g j * (deg ^ (T - j) * ((q - 1) ^ j * q ^ (T - j - 1))))

sum_crossing_factor in the form callers can use: the counts are supplied as an abstract function C, since the concrete count at position (i, j) is a Finset.card whose very statement needs i + j + 1 < T, a fact only available pointwise inside the sum.

theorem Complexity.RegCSP.opinionOf_eq_startIdx {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {ℓ : ℕ} (hℓ : ℓ ≤ T) (v : R.graph.V) (W : Fin ℓ → R.graph.D) (i : Fin ℓ) (hiT : ↑i ≤ T) : R.opinionOf q T hq A (R.graph.walkAt ℓ v W ↑i) hiT (R.graph.revWalk v (R.graph.segPre W ⋯)) = A v (R.graph.startIdx hℓ W i)

The prefix condition counted above is exactly the constraint's own startIdx term: the opinion v holds about the walk's i-th vertex.

theorem Complexity.RegCSP.opinionOf_eq_endIdx {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {ℓ : ℕ} (hℓ : ℓ ≤ T) (v : R.graph.V) (W : Fin ℓ → R.graph.D) (i : Fin ℓ) (hjT : ℓ - (↑i + 1) ≤ T) : R.opinionOf q T hq A (R.graph.walkAt ℓ v W (↑i + 1)) hjT (R.graph.segSuf W ↑i) = A (R.graph.walkEnd ℓ v W) (R.graph.endIdx hℓ v W i)

The suffix condition counted above is exactly the constraint's own endIdx term: the opinion the walk's far end holds about the (i+1)-st vertex.

theorem Complexity.RegCSP.card_good_crossing {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (a : R.graph.V) (d : R.graph.D) {ℓ i : ℕ} (hℓ : ℓ < T) (hi : i < ℓ) (hiT : i ≤ T) (hjT : ℓ - (i + 1) ≤ T) : {z : R.graph.V × (Fin T → R.graph.D) × (Fin T → Fin q) | stopAt z.2.2 = ℓ ∧ R.graph.walkAt ℓ z.1 (R.graph.preWalk z.2.1 ⋯) i = a ∧ R.graph.preWalk z.2.1 ⋯ ⟨i, hi⟩ = d ∧ R.opinionOf q T hq A a hiT (R.graph.revWalk z.1 (R.graph.segPre (R.graph.preWalk z.2.1 ⋯) ⋯)) = R.kPlurality q T hq A a ∧ R.opinionOf q T hq A (R.graph.nbr a d) hjT (R.graph.segSuf (R.graph.preWalk z.2.1 ⋯) i) = R.kPlurality q T hq A (R.graph.nbr a d)}.card = R.truthCount q T hq A a i * R.truthCount q T hq A (R.graph.nbr a d) (ℓ - (i + 1)) * (R.graph.deg ^ (T - ℓ) * ((q - 1) ^ ℓ * q ^ (T - ℓ - 1)))

The crossing count with the constraint's own conditions. For a dart (a, d) of R and a crossing position i inside an effective length ℓ, the killed-power constraints crossing (a, d) at i with truthful opinions at both ends number truthCount a i * truthCount (nbr a d) (ℓ - (i+1)) times the fibre weight.

Every counted crossing breaks its constraint

theorem Complexity.RegCSP.not_satisfies_of_good_crossing {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (z : R.graph.V × R.KLabels q T) (i : Fin (R.graph.kLen z.2)) (hiT : ↑i ≤ T) (hjT : R.graph.kLen z.2 - (↑i + 1) ≤ T) (hfault : ¬R.Satisfies (R.kDecode q T hq A) (R.graph.walkAt (R.graph.kLen z.2) z.1 (R.graph.kWalk z.2) ↑i, R.graph.kWalk z.2 i)) (hpre : R.opinionOf q T hq A (R.graph.walkAt (R.graph.kLen z.2) z.1 (R.graph.kWalk z.2) ↑i) hiT (R.graph.revWalk z.1 (R.graph.segPre (R.graph.kWalk z.2) ⋯)) = R.kDecode q T hq A (R.graph.walkAt (R.graph.kLen z.2) z.1 (R.graph.kWalk z.2) ↑i)) (hsuf : R.opinionOf q T hq A (R.graph.walkAt (R.graph.kLen z.2) z.1 (R.graph.kWalk z.2) (↑i + 1)) hjT (R.graph.segSuf (R.graph.kWalk z.2) ↑i) = R.kDecode q T hq A (R.graph.walkAt (R.graph.kLen z.2) z.1 (R.graph.kWalk z.2) (↑i + 1))) : ¬(R.killedPow q T hq).Satisfies A z

The counted darts really are unsatisfied. A killed walk crossing a dart that the decoded assignment fails, with both ends holding the decoded opinion about that dart's two vertices, breaks its own constraint. The two hypotheses are exactly the conditions card_good_crossing counts, turned into the constraint's startIdx / endIdx terms by the two identification lemmas.

theorem Complexity.RegCSP.truthCount_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (m : ℕ) : R.truthCount q T hq A v m ≤ R.graph.deg ^ m

A walk count never exceeds the number of walks.

theorem Complexity.RegCSP.card_le_mul_sum_truthCount_half {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) {H : ℕ} (hH : H + 1 ≤ T) : R.graph.deg ^ T * q ^ T ≤ Fintype.card α * (∑ m ∈ Finset.range (H + 1), R.truthCount q T hq A v m * (R.graph.deg ^ (T - m) * ((q - 1) ^ m * q ^ (T - m - 1))) + R.graph.deg ^ T * (q - 1) ^ T + R.graph.deg ^ T * ((q - 1) ^ (H + 1) * q ^ (T - (H + 1))))

Plurality on half the range. Restricting the weighted sum to positions at most H costs only the geometric tail, so the plurality bound survives the restriction to a square of positions that sum_crossing_factor needs.

theorem Complexity.RegCSP.card_good_crossing_sq {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (a : R.graph.V) (d : R.graph.D) {i j : ℕ} (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T) : {z : R.graph.V × (Fin T → R.graph.D) × (Fin T → Fin q) | stopAt z.2.2 = i + j + 1 ∧ R.graph.walkAt (i + j + 1) z.1 (R.graph.preWalk z.2.1 ⋯) i = a ∧ R.graph.preWalk z.2.1 ⋯ ⟨i, ⋯⟩ = d ∧ R.opinionOf q T hq A a hiT (R.graph.revWalk z.1 (R.graph.segPre (R.graph.preWalk z.2.1 ⋯) ⋯)) = R.kPlurality q T hq A a ∧ R.opinionOf q T hq A (R.graph.nbr a d) hjT (R.graph.segSuf (R.graph.preWalk z.2.1 ⋯) i) = R.kPlurality q T hq A (R.graph.nbr a d)}.card = R.truthCount q T hq A a i * R.truthCount q T hq A (R.graph.nbr a d) j * (R.graph.deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))

The crossing count indexed by the two lengths rather than by length and position — the form sum_goodCount_factor consumes.

The per-dart bound

noncomputable def Complexity.RegCSP.halfSum {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) (H : ℕ) : ℕ

The weighted count of truthful walks out of v, over positions at most H.

Equations

• R.halfSum q T hq A v H = ∑ m ∈ Finset.range (H + 1), R.truthCount q T hq A v m * (R.graph.deg ^ (T - m) * ((q - 1) ^ m * q ^ (T - m - 1)))

def Complexity.RegCSP.pluralityLoss (deg q T H : ℕ) : ℕ

What plurality pays for truncation: the walks that never stop, and those that stop after position H. Both are geometrically small next to deg ^ T * q ^ T.

Equations

• Complexity.RegCSP.pluralityLoss deg q T H = deg ^ T * (q - 1) ^ T + deg ^ T * ((q - 1) ^ (H + 1) * q ^ (T - (H + 1)))

theorem Complexity.RegCSP.card_le_mul_halfSum_add_loss {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (v : R.graph.V) {H : ℕ} (hH : H + 1 ≤ T) : R.graph.deg ^ T * q ^ T ≤ Fintype.card α * R.halfSum q T hq A v H + Fintype.card α * pluralityLoss R.graph.deg q T H

theorem Complexity.RegCSP.per_dart_lower {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (a : R.graph.V) (d : R.graph.D) {H : ℕ} (hH : 2 * H + 1 < T) (hHT : H + 1 ≤ T) (C : ℕ → ℕ → ℕ) (hC : ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), C i j = R.truthCount q T hq A a i * R.truthCount q T hq A (R.graph.nbr a d) j * (R.graph.deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))) : (q - 1) * ((R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H) * (R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H)) ≤ Fintype.card α ^ 2 * ((∑ i ∈ Finset.range (H + 1), ∑ j ∈ Finset.range (H + 1), C i j) * (R.graph.deg ^ (T + 1) * q ^ T))

The per-dart first moment. For one dart of R, the killed-power constraints crossing it with truthful opinions at both ends number at least

(q-1) · (X - |α|·loss)² / (|α|² · normaliser),

with X = deg^T · q^T. The two plurality bounds multiply because the crossing sum factorises — the payoff of the killed walk law.

theorem Complexity.RegCSP.sum_dart_lower {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (F : Finset R.Dart) {H : ℕ} (hH : 2 * H + 1 < T) (hHT : H + 1 ≤ T) (Cd : R.Dart → ℕ → ℕ → ℕ) (hCd : ∀ p ∈ F, ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), Cd p i j = R.truthCount q T hq A p.1 i * R.truthCount q T hq A (R.graph.nbr p.1 p.2) j * (R.graph.deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))) : F.card * ((q - 1) * ((R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H) * (R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H))) ≤ Fintype.card α ^ 2 * ((∑ p ∈ F, ∑ i ∈ Finset.range (H + 1), ∑ j ∈ Finset.range (H + 1), Cd p i j) * (R.graph.deg ^ (T + 1) * q ^ T))

The first moment, summed over the failed darts. Every dart of R that the decoded assignment fails contributes its own crossings, and for a given killed walk and position the dart crossed there is determined, so the contributions never overlap.

The crossing count of a single constraint

noncomputable def Complexity.RegCSP.goodCrossings {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (z : R.graph.V × R.KLabels q T) : Finset (Fin (R.graph.kLen z.2))

The steps at which a killed walk crosses a dart the decoded assignment fails, with truthful opinions at both ends. Its cardinality is the count the second-moment method is applied to.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RegCSP.mem_unsatDarts_of_goodCrossings_nonempty {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (z : R.graph.V × R.KLabels q T) (h : (R.goodCrossings q T hq A z).Nonempty) : z ∈ (R.killedPow q T hq).unsatDarts A

The support condition. A constraint with any good crossing is unsatisfied, so the second-moment method's support sits inside the unsatisfied darts.

theorem Complexity.RegCSP.sum_sq_goodCrossings {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) : ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card ^ 2 = ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card + 2 * ∑ z : R.graph.V × R.KLabels q T, ↑{p ∈ R.goodCrossings q T hq A z ×ˢ R.goodCrossings q T hq A z | p.1 < p.2}.card

The second moment, in terms of pairs of crossings. Squaring the count of good crossings and summing turns into the count itself plus twice the ordered pairs — and pairs of crossings are what the correlation bound estimates.

Positions as naturals

noncomputable def Complexity.RegCSP.goodPos {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (z : R.graph.V × R.KLabels q T) : Finset ℕ

The good crossing positions of a constraint, as naturals. The Fin version carries the constraint's own length in its type, which blocks the exchange of summation order the second moment needs; this one does not.

Equations

• R.goodPos q T hq A z = Finset.image Fin.val (R.goodCrossings q T hq A z)

theorem Complexity.RegCSP.card_goodPos {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (z : R.graph.V × R.KLabels q T) : (R.goodPos q T hq A z).card = (R.goodCrossings q T hq A z).card

theorem Complexity.RegCSP.mem_goodPos {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) {A : (R.killedPow q T hq).Assignment} {z : R.graph.V × R.KLabels q T} {k : ℕ} : k ∈ R.goodPos q T hq A z ↔ ∃ (h : k < R.graph.kLen z.2), ⟨k, h⟩ ∈ R.goodCrossings q T hq A z

theorem Complexity.RegCSP.card_pairs_goodPos {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (z : R.graph.V × R.KLabels q T) : {p ∈ R.goodPos q T hq A z ×ˢ R.goodPos q T hq A z | p.1 < p.2}.card = {p ∈ R.goodCrossings q T hq A z ×ˢ R.goodCrossings q T hq A z | p.1 < p.2}.card

Counting ordered pairs of positions is the same in either indexing.

theorem Complexity.RegCSP.lt_T_of_mem_goodPos {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) {A : (R.killedPow q T hq).Assignment} {z : R.graph.V × R.KLabels q T} {k : ℕ} (h : k ∈ R.goodPos q T hq A z) : k < T

theorem Complexity.RegCSP.sum_card_pairs_eq {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) : ∑ z : R.graph.V × R.KLabels q T, {p ∈ R.goodPos q T hq A z ×ˢ R.goodPos q T hq A z | p.1 < p.2}.card = ∑ p ∈ Finset.range T ×ˢ Finset.range T with p.1 < p.2, {z : R.graph.V × R.KLabels q T | p.1 ∈ R.goodPos q T hq A z ∧ p.2 ∈ R.goodPos q T hq A z}.card

Exchanging the order of counting. The pairs of good crossings, summed over the constraints, are the same as the constraints with two good crossings, summed over the pairs of positions. The right-hand side is the form the correlation bound estimates.

theorem Complexity.RegCSP.card_both_good_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {k l : ℕ} (hk : k < T) (hl : l < T) : {z : R.graph.V × R.KLabels q T | k ∈ R.goodPos q T hq A z ∧ l ∈ R.goodPos q T hq A z}.card ≤ q ^ T * {w : R.graph.V × (Fin T → R.graph.D) | (R.graph.walkAt T w.1 w.2 k, w.2 ⟨k, hk⟩) ∈ R.unsatDarts (R.kDecode q T hq A) ∧ (R.graph.walkAt T w.1 w.2 l, w.2 ⟨l, hl⟩) ∈ R.unsatDarts (R.kDecode q T hq A)}.card

Dropping to the underlying walk. Constraints with good crossings at two positions are, after forgetting the truthfulness conditions and the stopping signals, walks that cross a failed dart at both positions. Forgetting the signals costs the factor q ^ T; both omissions only weaken an upper bound.

theorem Complexity.RegCSP.sum_pairs_bound {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) (hspec : R.graph.SpectralBound lam) (hn : 0 < R.graph.order) : ∑ p ∈ Finset.range T ×ˢ Finset.range T with p.1 < p.2, ↑{z : R.graph.V × R.KLabels q T | p.1 ∈ R.goodPos q T hq A z ∧ p.2 ∈ R.goodPos q T hq A z}.card ≤ ↑q ^ T * (↑R.graph.deg ^ (T - 2) * (↑T * ↑T * (↑(R.unsatDarts (R.kDecode q T hq A)).card * ↑(R.unsatDarts (R.kDecode q T hq A)).card / ↑R.graph.order) + ↑T * (1 / (1 - lam)) * (↑R.graph.deg * ↑(R.unsatDarts (R.kDecode q T hq A)).card)))

The second moment's pair term, bounded. Chaining the drop to underlying walks, the two-crossing identity and the correlation bound.

theorem Complexity.RegCSP.sum_sq_goodCrossings_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) (hspec : R.graph.SpectralBound lam) (hn : 0 < R.graph.order) : ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card ^ 2 ≤ ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card + 2 * (↑q ^ T * (↑R.graph.deg ^ (T - 2) * (↑T * ↑T * (↑(R.unsatDarts (R.kDecode q T hq A)).card * ↑(R.unsatDarts (R.kDecode q T hq A)).card / ↑R.graph.order) + ↑T * (1 / (1 - lam)) * (↑R.graph.deg * ↑(R.unsatDarts (R.kDecode q T hq A)).card))))

The second moment of the crossing count. Everything above, assembled: the sum of squares is the sum plus twice a pair term, and the pair term is controlled by the spectral gap.

theorem Complexity.RegCSP.sum_card_goodPos_eq {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) : ∑ z : R.graph.V × R.KLabels q T, (R.goodPos q T hq A z).card = ∑ k ∈ Finset.range T, {z : R.graph.V × R.KLabels q T | k ∈ R.goodPos q T hq A z}.card

The first moment, with the order of counting exchanged: summing the good crossings over the constraints is the same as counting, for each position, the constraints good there.

theorem Complexity.RegCSP.sum_over_len_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (i H : ℕ) : ∑ j ∈ Finset.range (H + 1), {z : R.graph.V × R.KLabels q T | stopAt z.2.2 = i + j + 1 ∧ i ∈ R.goodPos q T hq A z}.card ≤ {z : R.graph.V × R.KLabels q T | i ∈ R.goodPos q T hq A z}.card

Constraints of different effective lengths are different constraints, so summing over the suffix length j at a fixed crossing position stays within the constraints good at that position.

theorem Complexity.RegCSP.mem_goodPos_of_crossing {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (a : R.graph.V) (d : R.graph.D) {i j : ℕ} (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T) (hfault : ¬R.Satisfies (R.kDecode q T hq A) (a, d)) (z : R.graph.V × R.KLabels q T) (hlen : stopAt z.2.2 = i + j + 1) (hwalk : R.graph.walkAt (i + j + 1) z.1 (R.graph.preWalk z.2.1 ⋯) i = a) (hlab : R.graph.preWalk z.2.1 ⋯ ⟨i, ⋯⟩ = d) (hpre : R.opinionOf q T hq A a hiT (R.graph.revWalk z.1 (R.graph.segPre (R.graph.preWalk z.2.1 ⋯) ⋯)) = R.kPlurality q T hq A a) (hsuf : R.opinionOf q T hq A (R.graph.nbr a d) hjT (R.graph.segSuf (R.graph.preWalk z.2.1 ⋯) i) = R.kPlurality q T hq A (R.graph.nbr a d)) : i ∈ R.goodPos q T hq A z

From a counted crossing to a good position. A constraint counted by card_good_crossing_sq, whose crossed dart the decoded assignment fails, is good at that position. The two descriptions differ only in how the walk's length is named — i + j + 1 on one side, kLen on the other — which walkAt_preWalk and opinionOf_congr reconcile without any transport.

noncomputable def Complexity.RegCSP.crossingSet {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (a : R.graph.V) (d : R.graph.D) {i j : ℕ} (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T) : Finset (R.graph.V × R.KLabels q T)

The constraints counted by card_good_crossing_sq, packaged.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RegCSP.card_crossingSet {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (a : R.graph.V) (d : R.graph.D) {i j : ℕ} (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T) : (R.crossingSet q T hq A a d hij hiT hjT).card = R.truthCount q T hq A a i * R.truthCount q T hq A (R.graph.nbr a d) j * (R.graph.deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))

theorem Complexity.RegCSP.sum_crossingSet_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {i j : ℕ} (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T) : ∑ p ∈ R.unsatDarts (R.kDecode q T hq A), (R.crossingSet q T hq A p.1 p.2 hij hiT hjT).card ≤ {z : R.graph.V × R.KLabels q T | stopAt z.2.2 = i + j + 1 ∧ i ∈ R.goodPos q T hq A z}.card

The crossings of different darts do not overlap. At a fixed position the dart a walk crosses is determined, so summing over the failed darts stays within the constraints good at that position.

theorem Complexity.RegCSP.sum_len_pos_le {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {H : ℕ} (hHT : H + 1 ≤ T) : ∑ i ∈ Finset.range (H + 1), ∑ j ∈ Finset.range (H + 1), {z : R.graph.V × R.KLabels q T | stopAt z.2.2 = i + j + 1 ∧ i ∈ R.goodPos q T hq A z}.card ≤ ∑ z : R.graph.V × R.KLabels q T, (R.goodCrossings q T hq A z).card

Summed over both lengths, the constraints good at a position never exceed the total crossing count.

theorem Complexity.RegCSP.sum_Cd_le_sum_goodCrossings {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {H : ℕ} (hHT : H + 1 ≤ T) (Cd : R.Dart → ℕ → ℕ → ℕ) (hCd : ∀ p ∈ R.unsatDarts (R.kDecode q T hq A), ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), ∀ (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T), Cd p i j = (R.crossingSet q T hq A p.1 p.2 hij hiT hjT).card) (hsq : ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), i + j + 1 < T) : ∑ p ∈ R.unsatDarts (R.kDecode q T hq A), ∑ i ∈ Finset.range (H + 1), ∑ j ∈ Finset.range (H + 1), Cd p i j ≤ ∑ z : R.graph.V × R.KLabels q T, (R.goodCrossings q T hq A z).card

The first moment, bounded by the crossing count. The counts summed by sum_dart_lower never exceed the total number of good crossings.

Powering soundness

theorem Complexity.RegCSP.card_unsatDarts_ge {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {Alb Bub : ℝ} (hA0 : 0 ≤ Alb) (hA : Alb ≤ ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card) (hB : ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card ^ 2 ≤ Bub) (hB0 : 0 < Bub) : Alb ^ 2 / Bub ≤ ↑((R.killedPow q T hq).unsatDarts A).card

The second-moment bound on unsatisfied constraints. Given a lower bound on the first moment of the crossing count and an upper bound on its second moment, at least Alb ^ 2 / Bub of the powered constraints are unsatisfied.

noncomputable def Complexity.RegCSP.crossCount {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (p : R.Dart) (i j : ℕ) : ℕ

The crossing count as a total function of the two lengths, so that it can be summed without carrying the side conditions.

Equations

• R.crossCount q T hq A p i j = if h : i + j + 1 < T then (R.crossingSet q T hq A p.1 p.2 h ⋯ ⋯).card else 0

theorem Complexity.RegCSP.crossCount_eq_card {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (p : R.Dart) {i j : ℕ} (hij : i + j + 1 < T) (hiT : i ≤ T) (hjT : i + j + 1 - (i + 1) ≤ T) : R.crossCount q T hq A p i j = (R.crossingSet q T hq A p.1 p.2 hij hiT hjT).card

theorem Complexity.RegCSP.crossCount_eq_prod {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) (p : R.Dart) {i j : ℕ} (hij : i + j + 1 < T) : R.crossCount q T hq A p i j = R.truthCount q T hq A p.1 i * R.truthCount q T hq A (R.graph.nbr p.1 p.2) j * (R.graph.deg ^ (T - (i + j + 1)) * ((q - 1) ^ (i + j + 1) * q ^ (T - (i + j + 1) - 1)))

theorem Complexity.RegCSP.sum_goodCrossings_ge {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {H : ℕ} (hH : 2 * H + 1 < T) (hHT : H + 1 ≤ T) (hsq : ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), i + j + 1 < T) : ↑((R.unsatDarts (R.kDecode q T hq A)).card * ((q - 1) * ((R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H) * (R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H)))) ≤ ↑(Fintype.card α ^ 2 * (R.graph.deg ^ (T + 1) * q ^ T)) * ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card

The first moment, in closed form. Combining the per-dart bound with the fact that the counted crossings are good crossings.

theorem Complexity.RegCSP.powering_soundness {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {H : ℕ} (hH : 2 * H + 1 < T) (hHT : H + 1 ≤ T) (hsq : ∀ i ∈ Finset.range (H + 1), ∀ j ∈ Finset.range (H + 1), i + j + 1 < T) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) (hspec : R.graph.SpectralBound lam) (hn : 0 < R.graph.order) (hBub : 0 < ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card + 2 * (↑q ^ T * (↑R.graph.deg ^ (T - 2) * (↑T * ↑T * (↑(R.unsatDarts (R.kDecode q T hq A)).card * ↑(R.unsatDarts (R.kDecode q T hq A)).card / ↑R.graph.order) + ↑T * (1 / (1 - lam)) * (↑R.graph.deg * ↑(R.unsatDarts (R.kDecode q T hq A)).card))))) : (↑((R.unsatDarts (R.kDecode q T hq A)).card * ((q - 1) * ((R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H) * (R.graph.deg ^ T * q ^ T - Fintype.card α * pluralityLoss R.graph.deg q T H)))) / ↑(Fintype.card α ^ 2 * (R.graph.deg ^ (T + 1) * q ^ T))) ^ 2 / (∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card + 2 * (↑q ^ T * (↑R.graph.deg ^ (T - 2) * (↑T * ↑T * (↑(R.unsatDarts (R.kDecode q T hq A)).card * ↑(R.unsatDarts (R.kDecode q T hq A)).card / ↑R.graph.order) + ↑T * (1 / (1 - lam)) * (↑R.graph.deg * ↑(R.unsatDarts (R.kDecode q T hq A)).card))))) ≤ ↑((R.killedPow q T hq).unsatDarts A).card

Soundness of the killed powering step. Combining the first moment (sum_goodCrossings_ge) with the second (sum_sq_goodCrossings_le) through Paley–Zygmund: a constant fraction of the powered constraints fail, the constant being the ratio of the squared first moment to the second.

The first moment is proportional to the number of darts the decoded assignment fails, so this is the amplification: the powered system's value is bounded below in terms of the original's.

theorem Complexity.RegCSP.card_dart_killedPow {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) : (R.killedPow q T hq).graph.order * (R.killedPow q T hq).graph.deg = R.graph.order * (R.graph.deg ^ T * q ^ T)

The powered system's constraint count.

theorem Complexity.RegCSP.unsatFrac_killedPow_ge {α : Type} (R : RegCSP α) (q T : ℕ) (hq : 0 < q) (A : (R.killedPow q T hq).Assignment) {LB : ℝ} (hLB : LB ≤ ↑((R.killedPow q T hq).unsatDarts A).card) (hn : 0 < R.graph.order) : LB / ↑(R.graph.order * (R.graph.deg ^ T * q ^ T)) ≤ ↑((R.killedPow q T hq).unsatFrac A)

A lower bound on the unsatisfied constraints becomes one on the unsatisfied fraction, which is what unsatVal and the amplification bookkeeping use.

theorem Complexity.RegCSP.le_unsatVal_killedPow {α : Type} [Fintype α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) {LB : ℝ} (h : ∀ (A : (R.killedPow q T hq).Assignment), LB ≤ ↑((R.killedPow q T hq).unsatFrac A)) : LB ≤ ↑(R.killedPow q T hq).unsatVal

A bound holding for every assignment holds for the value.