The powering bound, in closed form

powering_soundness states the second-moment argument exactly as it falls out of the two moment estimates: a ratio of a first-moment lower bound squared to a second-moment upper bound, with every count left explicit. This module turns it into the statement the amplifier needs — a lower bound on the powered system's value as a rational function of the original value, with all the constants isolated:

c² u / (c + 2 T² u + 2 T / (1 - λ)) ≤ unsatFrac (killedPow)

where u is the decoded assignment's violated fraction and c = (q - 1) / (4 |α|²). For small u this is linear in u with slope of order (q - 1)² (1 - λ) / (|α|⁴ T), and since T need only be linear in q |α|, the slope grows with q: that is the amplification. For large u it is bounded below by a constant.

Two technical points are handled here. The first moment appears in the denominator of the second-moment bound, so the ratio has to be made monotone before the first-moment lower bound can be substituted in both places. And the plurality loss must be at most half the total, which requires T large enough relative to q and |α| — Bernoulli's inequality shows H + 1 = 4 |α| (q - 1) suffices.

Main results

• Complexity.RegCSP.unsatFrac_killedPow_clean — the closed-form bound
• Complexity.RegCSP.le_unsatVal_killedPow_min — the min form
• Complexity.exists_powering_params — a choice of T and H meeting every side condition

Monotonicity of the Paley–Zygmund ratio

theorem Complexity.sq_div_add_mono {m M P : ℝ} (hm : 0 ≤ m) (hmM : m ≤ M) (hP : 0 < P) : m ^ 2 / (m + P) ≤ M ^ 2 / (M + P)

m ↦ m² / (m + P) is increasing on m ≥ 0 for P > 0.

The algebra of the bound

theorem Complexity.powering_algebra {U N d K q lam C : ℝ} (T' : ℕ) (hN : 0 < N) (hd : 0 < d) (hK : 0 < K) (hq : 1 ≤ q) (hlam : lam < 1) (hU : 0 < U) (hcount : (U * ((q - 1) * (d ^ (T' + 2) * q ^ (T' + 2) / 2 * (d ^ (T' + 2) * q ^ (T' + 2) / 2))) / (K ^ 2 * (d ^ (T' + 2 + 1) * q ^ (T' + 2)))) ^ 2 / (U * ((q - 1) * (d ^ (T' + 2) * q ^ (T' + 2) / 2 * (d ^ (T' + 2) * q ^ (T' + 2) / 2))) / (K ^ 2 * (d ^ (T' + 2 + 1) * q ^ (T' + 2))) + 2 * (q ^ (T' + 2) * (d ^ T' * (↑(T' + 2) * ↑(T' + 2) * (U * U / N) + ↑(T' + 2) * (1 / (1 - lam)) * (d * U))))) ≤ C) : ((q - 1) / (4 * K ^ 2)) ^ 2 * (U / (N * d)) / ((q - 1) / (4 * K ^ 2) + 2 * ↑(T' + 2) ^ 2 * (U / (N * d)) + 2 * ↑(T' + 2) / (1 - lam)) ≤ C / (N * (d ^ (T' + 2) * q ^ (T' + 2)))

The powering bound's algebra, over opaque real quantities: U violated darts among N · d, first moment at least U (q - 1) (d^T q^T / 2)² / (K² d^(T+1) q^T), second moment as in sum_sq_goodCrossings_le.

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 P : ℝ} (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 ≤ ∑ z : R.graph.V × R.KLabels q T, ↑(R.goodCrossings q T hq A z).card + P) (hP : 0 < P) : Alb ^ 2 / (Alb + P) ≤ ↑((R.killedPow q T hq).unsatDarts A).card

The second-moment count, with the first-moment lower bound on both sides.

noncomputable def Complexity.RegCSP.powConst (q : ℕ) (α : Type) [Fintype α] : ℝ

The slope constant of the powering bound.

Equations

• Complexity.RegCSP.powConst q α = (↑q - 1) / (4 * ↑(Fintype.card α) ^ 2)

theorem Complexity.RegCSP.unsatFrac_killedPow_clean {α : 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) (hq1 : 1 ≤ q) (hloss : 2 * (Fintype.card α * pluralityLoss R.graph.deg q T H) ≤ R.graph.deg ^ T * q ^ T) : powConst q α ^ 2 * ↑(R.unsatFrac (R.kDecode q T hq A)) / (powConst q α + 2 * ↑T ^ 2 * ↑(R.unsatFrac (R.kDecode q T hq A)) + 2 * ↑T / (1 - lam)) ≤ ↑((R.killedPow q T hq).unsatFrac A)

The powering bound in closed form. Under the side conditions of powering_soundness and with the plurality loss at most half the total, the powered system's violated fraction is at least c² u / (c + 2 T² u + 2 T / (1 - λ)), u the decoded assignment's violated fraction.

The min form

noncomputable def Complexity.RegCSP.powSlope (c T lam : ℝ) : ℝ

The slope of the powering bound for small values.

Equations

• Complexity.RegCSP.powSlope c T lam = c ^ 2 / (c + 2 + 2 * T / (1 - lam))

noncomputable def Complexity.RegCSP.powFloor (c T lam : ℝ) : ℝ

The floor of the powering bound for large values.

Equations

• Complexity.RegCSP.powFloor c T lam = c ^ 2 / T ^ 2 / (c + 2 * T ^ 2 + 2 * T / (1 - lam))

theorem Complexity.RegCSP.min_le_powBound {c T lam u : ℝ} (hc : 0 ≤ c) (hT : 1 ≤ T) (hlam : lam < 1) (hu0 : 0 ≤ u) (hu1 : u ≤ 1) : min (powSlope c T lam * u) (powFloor c T lam) ≤ c ^ 2 * u / (c + 2 * T ^ 2 * u + 2 * T / (1 - lam))

The rational bound dominates a min. For values up to 1 / T² the bound is linear with slope powSlope; beyond that it is at least powFloor.

theorem Complexity.RegCSP.le_unsatVal_killedPow_min {α : Type} [Fintype α] [DecidableEq α] [Nonempty α] (R : RegCSP α) (q T : ℕ) (hq : 0 < q) {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) (hq1 : 1 ≤ q) (hloss : 2 * (Fintype.card α * pluralityLoss R.graph.deg q T H) ≤ R.graph.deg ^ T * q ^ T) : min (powSlope (powConst q α) (↑T) lam * ↑R.unsatVal) (powFloor (powConst q α) (↑T) lam) ≤ ↑(R.killedPow q T hq).unsatVal

The powered value, in min form.

Choosing the parameters

theorem Complexity.four_mul_pow_le {K q : ℕ} (hK : 1 ≤ K) (hq : 2 ≤ q) : 4 * K * (q - 1) ^ (4 * K * (q - 1)) ≤ q ^ (4 * K * (q - 1))

Bernoulli, for the plurality loss. With m = 4 K (q - 1), 4 K (q - 1)^m ≤ q^m.

def Complexity.powT (K q : ℕ) : ℕ

The truncation length used for powering: 8 K (q - 1).

Equations

• Complexity.powT K q = 2 * (4 * K * (q - 1))

def Complexity.powH (K q : ℕ) : ℕ

The plurality threshold used for powering: 4 K (q - 1) - 1.

Equations

• Complexity.powH K q = 4 * K * (q - 1) - 1

theorem Complexity.powering_params_spec {K q : ℕ} (hK : 1 ≤ K) (hq : 2 ≤ q) (d : ℕ) : 2 * powH K q + 1 < powT K q ∧ powH K q + 1 ≤ powT K q ∧ (∀ i ∈ Finset.range (powH K q + 1), ∀ j ∈ Finset.range (powH K q + 1), i + j + 1 < powT K q) ∧ 2 * (K * RegCSP.pluralityLoss d q (powT K q) (powH K q)) ≤ d ^ powT K q * q ^ powT K q

Parameters for powering. For q ≥ 2 and alphabet size K ≥ 1, the choices powT and powH meet every side condition of the powering bound, for any degree.

noncomputable def Complexity.slopeUnit (K lam : ℝ) : ℝ

The per-unit slope: powSlope grows at least linearly in q - 1, with this coefficient.

Equations

• Complexity.slopeUnit K lam = 1 / (16 * K ^ 4 * (1 / (4 * K ^ 2) + 2 + 16 * K / (1 - lam)))

theorem Complexity.slopeUnit_mul_le_powSlope {K q : ℕ} (hK : 1 ≤ K) (hq : 2 ≤ q) {lam : ℝ} (hlam1 : lam < 1) : slopeUnit (↑K) lam * (↑q - 1) ≤ RegCSP.powSlope ((↑q - 1) / (4 * ↑K ^ 2)) (↑(powT K q)) lam

The slope grows linearly in q.