Hardness Magnification for MCSP via Circuit-Min-Merge

Slightly superlinear circuit lower bounds for MCSP[s] (Cslib.GapMCSP.yesSet s) imply NP ⊄ P/poly and P ≠ NP McKay, Murray, and Williams, Lemma 3.1, Theorem 1.4 (third bullet), and Section 5.

Assuming NP ⊆ P/poly, the polynomial-hierarchy language CircuitMinMergeLanguage (Cslib.MCSP.CircuitMinMergeLanguage), adapted from Circuit-Min-Merge in [McKayMurrayWilliams2019, Section 2.1], has polynomial-size circuits: given two subcube circuit certificates w₀ and w₁ for the half-subcubes p ++ [false] and p ++ [true] of {0, 1} ^ n (rather than t intervals), it selects the Cslib.BitString.wordLt-least valid size-≤ s circuit certificate w of length certLength n s (rather than a minimum-size circuit) that agrees with w₀ on p ++ [false] and with w₁ on p ++ [true], together with a validity bit. Following the C = P/poly case of the proof of Theorem 1.4 (Section 5) combined with Lemma 3.1's merge-tree idea, composing this merge circuit across the 2 ^ n nodes of the full binary tree of subcubes of {0, 1} ^ n (rather than a d-ary tree with ℓ = s³) produces a circuit of size 2 ^ n · poly(n, s(n)) deciding the 2 ^ n-bit slice of GapMCSP.yesSet s (Cslib.MCSP.exists_complexity_yesSet_le_of_NP_subset_PPoly).

Taking the contrapositive magnifies 2 ^ n · poly(n, s(n)) circuit lower bounds for GapMCSP.yesSet s to NP ⊄ P/poly (Cslib.MCSP.not_NP_subset_PPoly_of_yesSet_hard) and, via P ⊆ P/poly, to P ≠ NP (Cslib.MCSP.P_ne_NP_of_yesSet_hard). Relative to [McKayMurrayWilliams2019, Theorem 1.4, third bullet], the NP ⊄ P/poly magnification statements incorporate four specializations:

1. decision GapMCSP.yesSet s (MCSP[s]) instead of search-MCSP^A[s];
2. no oracle (A = ∅);
3. fan-in-2 De Morgan circuits counting all gates (Cslib.Circuits.Circuit.size);
4. a size-only lower bound, whereas the paper assumes no circuits of simultaneous size N · poly(s) and depth poly(s). Specializations (1) and (4) strengthen the lower-bound hypothesis (a decision lower bound implies a search lower bound, and a size-only lower bound implies a combined size-and-depth lower bound), while (2) and (3) fix parameters allowed by the source (A ∈ PH), making the Lean theorem a special case.

Main definitions

• Cslib.MCSP.agreesOnPoint, Cslib.MCSP.AgreesWithChildren: child-agreement predicates on a subcube prefix p (tested via List.isPrefixOf).
• Cslib.MCSP.IsMergedCert, Cslib.MCSP.IsMinMergedCert: valid and lexicographically minimal merged certificates.
• Cslib.MCSP.CircuitMinMergeLanguage: the Circuit-Min-Merge decision problem, adapted to binary subcube merging of fixed-threshold certificates.

Main results

• Cslib.MCSP.circuitMinMergeLanguage_mem_PPolyOn: under NP ⊆ P/poly, CircuitMinMergeLanguage ∈ PPolyOn encMerge.
• Cslib.MCSP.exists_complexity_yesSet_le_of_NP_subset_PPoly: under NP ⊆ P/poly, GapMCSP.yesSet s has circuits of size 2 ^ n · c · (n + s n + 1) ^ c on 2 ^ n-bit truth tables ([McKayMurrayWilliams2019, Lemma 3.1 and Section 5 (proof of Theorem 1.4, C = P/poly case)]).
• Cslib.MCSP.exists_complexity_yesSet_pow_le_of_NP_subset_PPoly: specialization to polynomial schedules s(n) = n ^ k.
• Cslib.MCSP.not_NP_subset_PPoly_of_yesSet_hard, Cslib.MCSP.not_NP_subset_PPoly_of_yesSet_pow_hard: circuit lower bounds for GapMCSP.yesSet imply NP ⊄ P/poly ([McKayMurrayWilliams2019, Theorem 1.4, third bullet], specialized to decision MCSP[s] without oracle and size-only De Morgan circuit lower bounds).
• Cslib.MCSP.P_ne_NP_of_yesSet_hard, Cslib.MCSP.P_ne_NP_of_yesSet_pow_hard: immediate corollaries concluding P ≠ NP via P ⊆ P/poly.

References

• D. McKay, C. D. Murray, R. R. Williams, Weak Lower Bounds on Resource-Bounded Compression Imply Strong Separations of Complexity Classes

Lexicographic minimum on fixed-length bit lists

Subcubes and child-agreement predicates

def Cslib.MCSP.agreesOnPoint (n s : ℕ) (p w₀ w₁ w x : List Bool) : Bool

Whether the candidate circuit w agrees at point x in the subcube p (tested by p.isPrefixOf x) with the child certificate w₀ (if x[p.length] = false) or w₁ (if x[p.length] = true).

theorem Cslib.MCSP.computableInPolyTime_agreesOnPoint {γ : Type} {encIn : γ ↪ List Bool} {n s : γ → ℕ} {p w₀ w₁ w x : γ → List Bool} (hn : Turing.MultiTapeTM.ComputableInPolyTime n encIn Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s encIn Turing.MultiTapeTM.encUnary) (hp : Turing.MultiTapeTM.ComputableInPolyTime p encIn Turing.MultiTapeTM.encBits) (hw₀ : Turing.MultiTapeTM.ComputableInPolyTime w₀ encIn Turing.MultiTapeTM.encBits) (hw₁ : Turing.MultiTapeTM.ComputableInPolyTime w₁ encIn Turing.MultiTapeTM.encBits) (hw : Turing.MultiTapeTM.ComputableInPolyTime w encIn Turing.MultiTapeTM.encBits) (hx : Turing.MultiTapeTM.ComputableInPolyTime x encIn Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : γ) => agreesOnPoint (n a) (s a) (p a) (w₀ a) (w₁ a) (w a) (x a)) encIn Turing.MultiTapeTM.encBool

agreesOnPoint is computable in polynomial time when n and s are given in unary.

def Cslib.MCSP.AgreesWithChildren (n s : ℕ) (p w₀ w₁ w : List Bool) : Prop

Whether the candidate circuit w agrees on the subcube p with the child certificates w₀ (on p ++ [false]) and w₁ (on p ++ [true]) at every n-bit input.

def Cslib.MCSP.IsMergedCert (n s : ℕ) (p w₀ w₁ w : List Bool) : Prop

w is a canonical certificate of length certLength n s encoding a valid size-s circuit on n inputs that agrees with w₀ on p ++ [false] and with w₁ on p ++ [true].

def Cslib.MCSP.IsMinMergedCert (n s : ℕ) (p w₀ w₁ w : List Bool) : Prop

w is the lexicographically smallest (BitString.wordLt) certificate satisfying IsMergedCert n s p w₀ w₁.

CircuitMinMergeLanguage and nonuniform quantifier elimination

def Cslib.MCSP.stateWidth (n s : ℕ) : ℕ

The width certLength n s + 1 of a child state vector (ok, w), consisting of one validity bit followed by a certificate of length certLength n s.

@[reducible, inline]

abbrev Cslib.MCSP.MergeHeader : Type

The fixed parameters ((n, s), (p, j)) of a query to CircuitMinMergeLanguage: arity n and size bound s in unary, subcube prefix p, and output bit index j in unary.

def Cslib.MCSP.encHeader : MergeHeader ↪ List Bool

Encoding of MergeHeader with n, s, j in unary and p as raw bits.

@[reducible, inline]

abbrev Cslib.MCSP.MergeInput : Type

An input (((n, s), (p, j)), v) to CircuitMinMergeLanguage, where v concatenates the two child state vectors (ok₀, w₀) and (ok₁, w₁) of width stateWidth n s.

def Cslib.MCSP.encMerge : MergeInput ↪ List Bool

Encoding of MergeInput as encPair encHeader encBits, so encMerge (hdr, v) = frame (encHeader hdr) ++ v.

def Cslib.MCSP.mergeOk₀ (a : MergeInput) : Bool

Extract the left child validity bit ok₀ from a MergeInput.

def Cslib.MCSP.mergeCert₀ (a : MergeInput) : List Bool

Extract the left child certificate w₀ of length certLength n s from a MergeInput.

def Cslib.MCSP.mergeOk₁ (a : MergeInput) : Bool

Extract the right child validity bit ok₁ from a MergeInput.

def Cslib.MCSP.mergeCert₁ (a : MergeInput) : List Bool

Extract the right child certificate w₁ of length certLength n s from a MergeInput.

def Cslib.MCSP.CircuitMinMergeLanguage : Set MergeInput

The CircuitMinMergeLanguage decision problem, adapted from Circuit-Min-Merge in [McKayMurrayWilliams2019, Section 2.1]: given parameters ((n, s), (p, j)) and concatenated child states v representing (ok₀, w₀) and (ok₁, w₁) for the two half-subcubes p ++ [false] and p ++ [true] (rather than t intervals), accepts when ok₀ = true, ok₁ = true, and there is a BitString.wordLt-least valid size-≤ s merged certificate w (IsMinMergedCert n s p w₀ w₁ w, rather than a minimum-size circuit) whose j-th output bit (true at j = 0, and bit j - 1 of w at j > 0) is true.

theorem Cslib.MCSP.circuitMinMergeLanguage_mem_PPolyOn (hNP : Complexity.NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) : CircuitMinMergeLanguage ∈ Circuits.Boolean.PPolyOn encMerge

Under NP ⊆ P/poly, CircuitMinMergeLanguage has polynomial-size circuits. Since CircuitMinMergeLanguage is defined by bounded existential and universal quantifiers over polynomial-time predicates, nonuniform quantifier elimination puts it in PPolyOn encMerge [McKayMurrayWilliams2019, Section 2.1 and Section 5 (proof of Theorem 1.4)].

Subcube certificates and semantic tree synthesis

def Cslib.MCSP.IsSubcubeCert (n s : ℕ) (f : BooleanFunction n) (p w : List Bool) : Prop

w is a canonical certificate of length certLength n s encoding a valid size-s circuit on n inputs that computes f on every point in the subcube p (tested via p.isPrefixOf).

def Cslib.MCSP.IsMinSubcubeCert (n s : ℕ) (f : BooleanFunction n) (p w : List Bool) : Prop

w is the lexicographically smallest (BitString.wordLt) certificate satisfying IsSubcubeCert n s f p.

noncomputable def Cslib.MCSP.subcubeState (n s : ℕ) (f : BooleanFunction n) (p : List Bool) : BitString (stateWidth n s)

The stateWidth n s-bit state vector of subcube p for f: bit 0 records whether a size-s circuit certificate exists for f on p, and bits 1 .. certLength n s record the lexicographically smallest such certificate (or all false if none exists).

Main theorems: MMW19 circuit upper bound and hardness magnification

theorem Cslib.MCSP.exists_complexity_yesSet_le_of_NP_subset_PPoly (hNP : Complexity.NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) : ∃ c > 0, ∀ (s : ℕ → ℕ) (n : ℕ), Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((GapMCSP.yesSet s).slice (2 ^ n))) ≤ 2 ^ n * c * (n + s n + 1) ^ c

McKay–Murray–Williams circuit upper bound for MCSP[s] under NP ⊆ P/poly [McKayMurrayWilliams2019, Lemma 3.1 and Section 5 (proof of Theorem 1.4, C = P/poly case)]: if NP ⊆ P/poly, then there is a constant c > 0 such that for every size schedule s : ℕ → ℕ and every n, the 2 ^ n-bit slice of GapMCSP.yesSet s has circuit complexity at most 2 ^ n * c * (n + s n + 1) ^ c. The proof composes the P/poly circuit for CircuitMinMergeLanguage across a binary merge tree over the 2 ^ n subcubes of {0, 1} ^ n (rather than a d-ary tree with ℓ = s³).

theorem Cslib.MCSP.exists_complexity_yesSet_pow_le_of_NP_subset_PPoly (hNP : Complexity.NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits) (k : ℕ) : ∃ c > 0, ∀ (n : ℕ), Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((GapMCSP.yesSet fun (m : ℕ) => m ^ k).slice (2 ^ n))) ≤ 2 ^ n * c * (n + 1) ^ c

McKay–Murray–Williams circuit upper bound for MCSP[n ^ k] under NP ⊆ P/poly [McKayMurrayWilliams2019, Lemma 3.1 and Section 5 (proof of Theorem 1.4, C = P/poly case)]: if NP ⊆ P/poly, then for every degree k, there is c > 0 such that the 2 ^ n-bit slice of GapMCSP.yesSet (fun m => m ^ k) has circuit complexity at most 2 ^ n * c * (n + 1) ^ c.

theorem Cslib.MCSP.not_NP_subset_PPoly_of_yesSet_hard (h : ∀ c > 0, ∃ (s : ℕ → ℕ) (n : ℕ), 2 ^ n * c * (n + s n + 1) ^ c < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((GapMCSP.yesSet s).slice (2 ^ n)))) : ¬Complexity.NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits

Hardness magnification for MCSP[s] against NP ⊆ P/poly [McKayMurrayWilliams2019, Theorem 1.4, third bullet]: if for every c > 0 there exist a schedule s and input arity n such that the 2 ^ n-bit slice of GapMCSP.yesSet s requires more than 2 ^ n * c * (n + s n + 1) ^ c gates, then NP ⊄ P/poly.

Relative to the paper's statement, this specializes search-MCSP^A[s] to decision GapMCSP.yesSet s (MCSP[s]), sets A = ∅, uses fan-in-2 De Morgan circuits counting all gates, and assumes a size-only lower bound rather than a combined size-and-depth lower bound.

theorem Cslib.MCSP.P_ne_NP_of_yesSet_hard (h : ∀ c > 0, ∃ (s : ℕ → ℕ) (n : ℕ), 2 ^ n * c * (n + s n + 1) ^ c < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((GapMCSP.yesSet s).slice (2 ^ n)))) : Complexity.P Turing.MultiTapeTM.encBits ≠ Complexity.NP Turing.MultiTapeTM.encBits

Hardness magnification for MCSP[s] to P ≠ NP: if for every c > 0 there exist a schedule s and input arity n such that the 2 ^ n-bit slice of GapMCSP.yesSet s requires more than 2 ^ n * c * (n + s n + 1) ^ c gates, then P ≠ NP.

This follows immediately from not_NP_subset_PPoly_of_yesSet_hard ([McKayMurrayWilliams2019, Theorem 1.4, third bullet]) and P ⊆ P/poly (P_subset_PPolyOn).

theorem Cslib.MCSP.not_NP_subset_PPoly_of_yesSet_pow_hard (k : ℕ) (h : ∀ c > 0, ∃ (n : ℕ), 2 ^ n * c * (n + 1) ^ c < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((GapMCSP.yesSet fun (m : ℕ) => m ^ k).slice (2 ^ n)))) : ¬Complexity.NP Turing.MultiTapeTM.encBits ⊆ Circuits.Boolean.PPolyOn Turing.MultiTapeTM.encBits

Hardness magnification for MCSP[n ^ k] against NP ⊆ P/poly [McKayMurrayWilliams2019, Theorem 1.4, third bullet]: if for some k and every c > 0, there is n such that the 2 ^ n-bit slice of GapMCSP.yesSet (fun m => m ^ k) requires more than 2 ^ n * c * (n + 1) ^ c gates, then NP ⊄ P/poly.

Relative to the paper's statement, this specializes search-MCSP^A[s] to decision GapMCSP.yesSet (MCSP[n ^ k]), sets A = ∅, uses fan-in-2 De Morgan circuits counting all gates, and assumes a size-only lower bound rather than a combined size-and-depth lower bound.

theorem Cslib.MCSP.P_ne_NP_of_yesSet_pow_hard (k : ℕ) (h : ∀ c > 0, ∃ (n : ℕ), 2 ^ n * c * (n + 1) ^ c < Circuits.complexity Circuits.Boolean.interpretation (Circuits.single ((GapMCSP.yesSet fun (m : ℕ) => m ^ k).slice (2 ^ n)))) : Complexity.P Turing.MultiTapeTM.encBits ≠ Complexity.NP Turing.MultiTapeTM.encBits

Hardness magnification for MCSP[n ^ k] to P ≠ NP: if for some k and every c > 0, there is n such that the 2 ^ n-bit slice of GapMCSP.yesSet (fun m => m ^ k) requires more than 2 ^ n * c * (n + 1) ^ c gates, then P ≠ NP.

This follows immediately from not_NP_subset_PPoly_of_yesSet_pow_hard ([McKayMurrayWilliams2019, Theorem 1.4, third bullet]) and P ⊆ P/poly (P_subset_PPolyOn).