Exponential worst-case hardness gives exponential average-case hardness

Let L be a language whose slices need De Morgan circuits of size 2 ^ (γ n) for all large n. This module encodes the slices of L with the reconstruction theorem of Sudan, Trevisan and Vadhan (Cslib.Circuits.Boolean.complexity_le_pow_of_agree_hardnessEncode) along a concrete schedule of parameters, and proves that the encoded language is average-case hard for circuits of size 2 ^ ⌊N / c⌋ at all large lengths N (Cslib.HardnessEncoding.eventually_isAverageCaseHard_encodedSlice).

The schedule. Let M = ⌈40 / γ⌉ + 1 (Cslib.HardnessEncoding.blockFactor). At length N, the block length is b = ⌊N / (4 (M + 1))⌋ (Cslib.HardnessEncoding.blockLength); the slice of L at length n = M b is encoded over the explicit binary field of degree w = 4 b (Cslib.BinaryField), with b-bit blocks embedded as polynomials of degree less than b. The encoding has (M + 1) w ≤ N input bits; the remaining input bits are ignored (Cslib.HardnessEncoding.encodedSlice), and the encoded slices form the encoded language (Cslib.HardnessEncoding.encodedLanguage). For the hardness s = 2 ^ σ, σ = ⌊N / c⌋ with c = 200 (M + 1) (Cslib.HardnessEncoding.hardnessDivisor), the parameters of the reconstruction are K = 2 σ + ⌊log₂ w⌋ + 2 masks, the Sudan parameter D = 2 ^ (3 b - ⌊b / 4⌋) and majority trees of depth L = ⌊log₂ (M b)⌋ + 1.

The argument. A circuit of size s agreeing with the slice at length N on a 1 / 2 + 1 / s fraction gives, after fixing the ignored bits (Cslib.Circuits.Boolean.exists_complexity_le_of_agree_prefix), a circuit of size s + 2 with the same agreement with the encoding, and the reconstruction theorem turns it into a circuit for the slice of L at length M b with at most 2 ^ 27 * M ^ 3 * b ^ 6 * 2 ^ (36 b + 5 σ) < 2 ^ (40 b) ≤ 2 ^ (γ M b) gates, for large b (Cslib.HardnessEncoding.isAverageCaseHard_encodedSlice_of): a contradiction.

The hardness is eventual: it holds at all large lengths N, from worst-case hardness at all large lengths n. The schedule only uses the hard lengths M b, multiples of M; with a suitable modification of the schedule, worst-case hardness at infinitely many lengths gives average-case hardness at infinitely many encoded lengths, which is not what Cslib.Complexity.P_eq_BPP_of_isAverageCaseHard assumes.

Main definitions

• Cslib.HardnessEncoding.blockFactor, Cslib.HardnessEncoding.hardnessDivisor, Cslib.HardnessEncoding.blockLength: the schedule.
• Cslib.HardnessEncoding.encodedSlice: the encoded slice at length N.
• Cslib.HardnessEncoding.encodedLanguage: the language of the encoded slices.

Main results

• Cslib.HardnessEncoding.isAverageCaseHard_encodedSlice_of: hardness at one length.
• Cslib.HardnessEncoding.eventually_isAverageCaseHard_encodedSlice: exponential worst-case hardness gives exponential average-case hardness.

References

• [M. Sudan, L. Trevisan, S. Vadhan, Pseudorandom generators without the XOR lemma] [STV01]
• R. Impagliazzo, A. Wigderson, P = BPP if E requires exponential circuits: Derandomizing the XOR lemma

The schedule

noncomputable def Cslib.HardnessEncoding.blockFactor (γ : ℝ) : ℕ

The block factor M = ⌈40 / γ⌉ + 1 for the hardness exponent γ.

noncomputable def Cslib.HardnessEncoding.hardnessDivisor (γ : ℝ) : ℕ

The divisor c = 200 (M + 1) of the average-case hardness exponent.

def Cslib.HardnessEncoding.blockLength (M N : ℕ) : ℕ

The block length b = ⌊N / (4 (M + 1))⌋ at input length N.

theorem Cslib.HardnessEncoding.encodedLength_le (M N : ℕ) : M * (4 * blockLength M N) + 4 * blockLength M N ≤ N

The encoding at length N reads at most N input bits: (M + 1) w ≤ N for w = 4 b.

noncomputable def Cslib.HardnessEncoding.encodedSlice (L : Language Bool) (M N : ℕ) : BooleanFunction N

The encoded slice at length N: the encoding of the slice of L at length M b over the explicit binary field of degree w = 4 b, read from the first (M + 1) w input bits, where b = blockLength M N; constant when b = 0.

noncomputable def Cslib.HardnessEncoding.encodedLanguage (L : Language Bool) (M : ℕ) : Language Bool

The encoded language: its slice at each length N is the encoded slice encodedSlice L M N.

@[simp]

theorem Cslib.HardnessEncoding.slice_encodedLanguage (L : Language Bool) (M N : ℕ) : (encodedLanguage L M).slice N = encodedSlice L M N

The slices of the encoded language are the encoded slices.

The numeric hypotheses of the reconstruction

Hardness at one length

theorem Cslib.HardnessEncoding.isAverageCaseHard_encodedSlice_of {L : Language Bool} {M N σ : ℕ} (hM : 1 ≤ M) (hb : 1 ≤ blockLength M N) (hev : (2 ^ 27 * M ^ 3 + 4608 * M + 128) * blockLength M N ^ 6 ≤ 2 ^ (blockLength M N / 4)) (hσ : 50 * σ ≤ blockLength M N + 1) (hhard : 2 ^ (40 * blockLength M N) ≤ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (L.slice (M * blockLength M N)))) : Circuits.Boolean.IsAverageCaseHard (encodedSlice L M N) (2 ^ σ)

Hardness at one length. Let M ≥ 1 and let the block length b at length N be positive with (2 ^ 27 * M ^ 3 + 4608 * M + 128) * b ^ 6 ≤ 2 ^ ⌊b / 4⌋. If 50 σ ≤ b + 1 and the slice of L at length M b needs 2 ^ (40 b) gates, then the encoded slice at length N is average-case hard for size 2 ^ σ.

Hardness at all large lengths

theorem Cslib.HardnessEncoding.eventually_isAverageCaseHard_encodedSlice {L : Language Bool} {γ : ℝ} (hγ : 0 < γ) (hard : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (γ * ↑n) ≤ ↑(Circuits.complexity Circuits.Boolean.interpretation (Circuits.single (L.slice n)))) : ∀ᶠ (N : ℕ) in Filter.atTop, Circuits.Boolean.IsAverageCaseHard (encodedSlice L (blockFactor γ) N) (2 ^ (N / hardnessDivisor γ))

Exponential worst-case hardness gives exponential average-case hardness [STV01], [IW97]. If the slices of L need De Morgan circuits of size 2 ^ (γ n) for all large n, for some γ > 0, then the encoded slices of L at all large lengths N are average-case hard for size 2 ^ ⌊N / c⌋, where c = hardnessDivisor γ.