Exact-complexity subcube repetition and MCSP lower bounds

This module proves Foundational Lemma B (Exact-Complexity Subcube Repetition) for DeMorgan.binaryCost and derives three families of circuit and formula lower bounds for MCSP:

1. Exact-complexity subcube repetition:
   • For any n-variable target u, repeating u on both halves of the (n + 1)-cube via muxTarget u u preserves DeMorgan.binaryCost complexity: costComplexity (muxTarget u u) = costComplexity u.
   • For any distinct n-variable targets u₀ ≠ u₁ where at least one has positive DeMorgan.binaryCost complexity, any De Morgan circuit computing muxTarget u₀ u₁ must have a charged gate reading coordinate 0 : Fin (n + 1) (via differingPath_of_gate_ne and DifferingPath.exists_first), so restricting 0 to either false or true deletes at least one charged gate (restrictProgram_deleted_of_readsInput). Consequently both costComplexity u₀ + 1 ≤ costComplexity (muxTarget u₀ u₁) and costComplexity u₁ + 1 ≤ costComplexity (muxTarget u₀ u₁).
   • Specializing to a truth table tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s with 1 ≤ s, for every tt' : Fin (2 ^ n) → Bool: mcspCostScalar ... (n + 1) s (pairTruthTable tt' tt) = true ↔ tt' = tt and mcspCostScalar ... (n + 1) s (pairTruthTable tt tt') = true ↔ tt' = tt.
2. Single-cut communication / cutwidth lower bound: Across any wire cut S separating the left-half truth-table inputs (j.val < 2 ^ n) from the right-half truth-table inputs, the diagonal truth tables pairTruthTable tt tt for tt ∈ exactCostSet ... n s must have pairwise distinct boundary keys, yielding (exactCostSet ... n s).card ≤ 2 ^ ((forward c.program S).card + (backward c.program S).card).
3. Khrapchenko formula and bounded-sharing De Morgan circuit lower bounds: Every diagonal truth table pairTruthTable tt tt (tt ∈ exactCostSet ... n s, 1 ≤ s) is a true-input of mcspCostScalar ... (n + 1) s with full sensitivity 2 ^ (n + 1), so every Khrapchenko measure bound M satisfies 2 ^ (n + 1) ≤ M. This yields 2 ^ (n + 1) ≤ F.leaves for De Morgan formulas and 2 ^ (n + 1) ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1) for De Morgan circuits with at most k shared gates.
4. Nechiporuk subfunction and formula lower bounds: For any Y₀ : Finset (Fin (2 ^ n)), embedded into the left half of Fin (2 ^ (n + 1)) as leftBlock Y₀, distinct restrictions restrictTo Y₀ tt of truth tables tt ∈ exactCostSet ... n s induce distinct subfunctions of mcspCostScalar ... (n + 1) s on leftBlock Y₀: ((exactCostSet ... n s).image (restrictTo Y₀)).card ≤ (Nechiporuk.subfunctions ... (leftBlock Y₀)).card. Taking Y₀ = Finset.univ gives (exactCostSet ... n s).card ≤ (Nechiporuk.subfunctions ... (leftBlock Finset.univ)).card. Combined with Nechiporuk.card_subfunctions_le, these give the corresponding Binary.Formula leaf lower bounds ... ≤ 2 * 16 ^ F.leavesIn (leftBlock Y₀).

All results above hold for every s ≥ 1 such that some truth table has exact DeMorgan.binaryCost complexity s (hypothesis htt or a nonempty exactCostSet); Complexitylib.Algebraic.LowerBound.MCSP.NonVacuity exhibits such a table for s = 1.

The resulting lower bounds are modest: writing N = 2 ^ (n + 1) for the number of MCSP inputs, the Khrapchenko consequences give N ≤ F.leaves (and the analogous linear bound with sharing), since the sensitivity argument uses a single true-input. The Nechiporuk consequences are also at most linear in N, because (exactCostSet ... n s).card ≤ 2 ^ (2 ^ n) = 2 ^ (N / 2), so the bound on F.leavesIn (leftBlock Finset.univ) is at most about N / 8.

Subcube repetition and DeMorgan.binaryCost gate elimination

@[simp]

theorem Algebraic.MCSP.fix_zero_apply {n : ℕ} (b : Bool) (y : Fin n → Bool) : (InputSubstitution.fix 0 b).apply y = Fin.cons b y

Fixing coordinate 0 : Fin (n + 1) to b sends y : Fin n → Bool to Fin.cons b y.

@[simp]

theorem Algebraic.MCSP.muxTarget_substitute_fix_false {n : ℕ} (u₀ u₁ : Target Bool n 1) : (muxTarget u₀ u₁).substitute (InputSubstitution.fix 0 false) = u₀

Fixing the leading bit of muxTarget u₀ u₁ to false recovers u₀.

@[simp]

theorem Algebraic.MCSP.muxTarget_substitute_fix_true {n : ℕ} (u₀ u₁ : Target Bool n 1) : (muxTarget u₀ u₁).substitute (InputSubstitution.fix 0 true) = u₁

Fixing the leading bit of muxTarget u₀ u₁ to true recovers u₁.

theorem Algebraic.MCSP.costComplexity_muxTarget_self_le {n : ℕ} (u : Target Bool n 1) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u u) ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u

Repeating a target on both halves of the (n + 1)-cube does not increase its DeMorgan.binaryCost complexity.

theorem Algebraic.MCSP.restrictCircuit_computes_muxTarget {n : ℕ} {u₀ u₁ : Target Bool n 1} {c : Circuit DeMorgan.signature (n + 1) 1} (hc : c.ComputesWith DeMorgan.interpretation (muxTarget u₀ u₁)) (b : Bool) : (DeMorgan.restrictCircuit c 0 b).result.ComputesWith DeMorgan.interpretation (bif b then u₁ else u₀)

Restricting coordinate 0 of a De Morgan circuit computing muxTarget u₀ u₁ to b yields a circuit computing the corresponding branch cond b u₁ u₀.

theorem Algebraic.MCSP.costComplexity_le_muxTarget {n : ℕ} (u₀ u₁ : Target Bool n 1) (b : Bool) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (bif b then u₁ else u₀) ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u₀ u₁)

Restricting coordinate 0 to b shows costComplexity (cond b u₁ u₀) ≤ costComplexity (muxTarget u₀ u₁).

theorem Algebraic.MCSP.costComplexity_le_muxTarget_left {n : ℕ} (u₀ u₁ : Target Bool n 1) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₀ ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u₀ u₁)

Restricting coordinate 0 to false shows costComplexity u₀ ≤ costComplexity (muxTarget u₀ u₁).

theorem Algebraic.MCSP.costComplexity_le_muxTarget_right {n : ℕ} (u₀ u₁ : Target Bool n 1) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₁ ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u₀ u₁)

Restricting coordinate 0 to true shows costComplexity u₁ ≤ costComplexity (muxTarget u₀ u₁).

@[simp]

theorem Algebraic.MCSP.costComplexity_muxTarget_self {n : ℕ} (u : Target Bool n 1) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u u) = Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u

Subcube repetition: repeating a target on both halves of the (n + 1)-cube preserves its DeMorgan.binaryCost complexity exactly.

@[simp]

theorem Algebraic.MCSP.costComplexity_constant_eq_zero {n : ℕ} (b : Bool) : (Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost fun (x : Fin n → Bool) (x_1 : Fin 1) => b) = 0

Constant targets have zero DeMorgan.binaryCost complexity.

theorem Algebraic.MCSP.costComplexity_add_one_le_cost_of_computes_muxTarget {n : ℕ} {u₀ u₁ : Target Bool n 1} (hne : u₀ ≠ u₁) (hpos : 1 ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₀ ∨ 1 ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₁) (c : Circuit DeMorgan.signature (n + 1) 1) (hc : c.ComputesWith DeMorgan.interpretation (muxTarget u₀ u₁)) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₀ + 1 ≤ ↑(c.cost DeMorgan.binaryCost) ∧ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₁ + 1 ≤ ↑(c.cost DeMorgan.binaryCost)

If u₀ ≠ u₁ and at least one of u₀, u₁ has positive DeMorgan.binaryCost complexity, then any circuit computing muxTarget u₀ u₁ has binaryCost strictly larger than both costComplexity u₀ and costComplexity u₁.

theorem Algebraic.MCSP.costComplexity_muxTarget_ge_add_one {n : ℕ} {u₀ u₁ : Target Bool n 1} (hne : u₀ ≠ u₁) (hpos : 1 ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₀ ∨ 1 ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₁) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₀ + 1 ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u₀ u₁) ∧ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost u₁ + 1 ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (muxTarget u₀ u₁)

If u₀ ≠ u₁ and at least one has positive DeMorgan.binaryCost complexity, then muxTarget u₀ u₁ has DeMorgan.binaryCost complexity strictly greater than both u₀ and u₁.

theorem Algebraic.MCSP.mcspCostScalar_pairTruthTable_left_eq_true_iff {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) (tt' : Fin (2 ^ n) → Bool) : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (pairTruthTable tt' tt) = true ↔ tt' = tt

Foundational Lemma B (left half): For 1 ≤ s and any truth table tt of exact DeMorgan.binaryCost complexity s, pairing tt' with tt yields complexity ≤ s if and only if tt' = tt.

theorem Algebraic.MCSP.mcspCostScalar_pairTruthTable_right_eq_true_iff {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) (tt' : Fin (2 ^ n) → Bool) : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (pairTruthTable tt tt') = true ↔ tt' = tt

Foundational Lemma B (right half): For 1 ≤ s and any truth table tt of exact DeMorgan.binaryCost complexity s, pairing tt with tt' yields complexity ≤ s if and only if tt' = tt.

Single-cut communication and cutwidth lower bound for MCSP

theorem Algebraic.MCSP.mix_pairTruthTable_of_halfCut {n g : ℕ} {S : Finset (Wire (2 ^ (n + 1)) g)} (hS : ∀ (j : Fin (2 ^ (n + 1))), Wire.input j ∈ S ↔ ↑j < 2 ^ n) (tt₁ tt₂ : Fin (2 ^ n) → Bool) : Cutwidth.SingleCut.mix S (pairTruthTable tt₁ tt₁) (pairTruthTable tt₂ tt₂) = pairTruthTable tt₁ tt₂

If a wire cut S contains the left-half input wires (j.val < 2 ^ n) and excludes the right-half input wires, mixing two diagonal truth tables pairTruthTable tt₁ tt₁ and pairTruthTable tt₂ tt₂ across S produces pairTruthTable tt₁ tt₂.

theorem Algebraic.MCSP.mcsp_singleCut_card_exactCostSet_le {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} (hs : 1 ≤ s) (c : Circuit σ (2 ^ (n + 1)) 1) (hc : c.ComputesWith interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s)) (S : Finset (Wire (2 ^ (n + 1)) c.size)) (hS : ∀ (j : Fin (2 ^ (n + 1))), Wire.input j ∈ S ↔ ↑j < 2 ^ n) : (exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s).card ≤ 2 ^ ((Cutwidth.SingleCut.forward c.program S).card + (Cutwidth.SingleCut.backward c.program S).card)

Single-cut communication lower bound for MCSP: For any circuit c computing mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (1 ≤ s) and any wire cut S separating the left-half truth-table inputs (j.val < 2 ^ n) from the right-half truth-table inputs, the boundary keys of pairTruthTable tt tt for tt ∈ exactCostSet ... n s are pairwise distinct, so (exactCostSet ... n s).card ≤ 2 ^ ((forward c.program S).card + (backward c.program S).card).

Khrapchenko sensitivity, formula, and bounded-sharing circuit lower bounds for MCSP

theorem Algebraic.MCSP.flip_pairTruthTable_lt {n : ℕ} (tt₀ tt₁ : Fin (2 ^ n) → Bool) {j : Fin (2 ^ (n + 1))} (hj : ↑j < 2 ^ n) : KW.flip (pairTruthTable tt₀ tt₁) j = pairTruthTable (KW.flip tt₀ ⟨↑j, hj⟩) tt₁

Flipping coordinate j (j.val < 2 ^ n) of pairTruthTable tt₀ tt₁ flips coordinate ⟨j.val, ...⟩ of the left half tt₀.

theorem Algebraic.MCSP.flip_pairTruthTable_ge {n : ℕ} (tt₀ tt₁ : Fin (2 ^ n) → Bool) {j : Fin (2 ^ (n + 1))} (hj : ¬↑j < 2 ^ n) : KW.flip (pairTruthTable tt₀ tt₁) j = pairTruthTable tt₀ (KW.flip tt₁ ⟨↑j - 2 ^ n, ⋯⟩)

Flipping coordinate j (¬ j.val < 2 ^ n) of pairTruthTable tt₀ tt₁ flips coordinate ⟨j.val - 2 ^ n, ...⟩ of the right half tt₁.

theorem Algebraic.MCSP.sensitiveCoordinates_mcsp_pairTruthTable_eq_univ {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) : KW.sensitiveCoordinates (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) (pairTruthTable tt tt) = Finset.univ

Every diagonal truth table pairTruthTable tt tt (tt ∈ exactCostSet ... n s, 1 ≤ s) has full sensitivity Finset.univ (all 2 ^ (n + 1) coordinates) for mcspCostScalar.

theorem Algebraic.MCSP.khrapchenkoBound_mcsp_lower_bound {n s M : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) (hM : KW.KhrapchenkoBound (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) M) : 2 ^ (n + 1) ≤ M

Khrapchenko bound for MCSP: Whenever 1 ≤ s and some truth table tt has exact DeMorgan.binaryCost complexity s, any Khrapchenko measure bound M for mcspCostScalar ... (n + 1) s satisfies 2 ^ (n + 1) ≤ M. The proof applies the Khrapchenko inequality to the single true-input pairTruthTable tt tt and its 2 ^ (n + 1) one-bit flips, so the bound is linear in the number 2 ^ (n + 1) of inputs.

theorem Algebraic.MCSP.mcsp_formula_leaves_lower_bound {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) {F : KW.Formula (2 ^ (n + 1))} (hF : F.Computes (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s)) : 2 ^ (n + 1) ≤ F.leaves

Any De Morgan formula computing mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (1 ≤ s, exactCostSet ... n s nonempty) has at least 2 ^ (n + 1) leaves.

theorem Algebraic.MCSP.mcsp_sharedGateCount_cost_lower_bound {n s k : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) (c : Circuit DeMorgan.signature (2 ^ (n + 1)) 1) (hc : c.ComputesWith DeMorgan.interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s)) (hk : KW.sharedGateCount c ≤ k) : 2 ^ (n + 1) ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1)

Any De Morgan circuit computing mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (1 ≤ s, exactCostSet ... n s nonempty) with sharedGateCount c ≤ k satisfies 2 ^ (n + 1) ≤ (k + 1) * (c.cost DeMorgan.binaryCost + k + 1).

Nechiporuk subfunction and Binary.Formula lower bounds for MCSP

def Algebraic.MCSP.leftHalfEmbed (n : ℕ) : Fin (2 ^ n) ↪ Fin (2 ^ (n + 1))

Embedding of Fin (2 ^ n) into the left half (j.val < 2 ^ n) of Fin (2 ^ (n + 1)).

Equations

• Algebraic.MCSP.leftHalfEmbed n = { toFun := fun (i : Fin (2 ^ n)) => ⟨↑i, ⋯⟩, inj' := ⋯ }

def Algebraic.MCSP.leftBlock {n : ℕ} (Y₀ : Finset (Fin (2 ^ n))) : Finset (Fin (2 ^ (n + 1)))

Given a subset Y₀ : Finset (Fin (2 ^ n)) of coordinates in the n-bit truth table, its embedded block in the left half of Fin (2 ^ (n + 1)) is Y₀.map (leftHalfEmbed n).

Equations

• Algebraic.MCSP.leftBlock Y₀ = Finset.map (Algebraic.MCSP.leftHalfEmbed n) Y₀

@[simp]

theorem Algebraic.MCSP.card_leftBlock {n : ℕ} (Y₀ : Finset (Fin (2 ^ n))) : (leftBlock Y₀).card = Y₀.card

@[simp]

theorem Algebraic.MCSP.mem_leftBlock_iff {n : ℕ} {Y₀ : Finset (Fin (2 ^ n))} {j : Fin (2 ^ (n + 1))} : j ∈ leftBlock Y₀ ↔ ∃ (h : ↑j < 2 ^ n), ⟨↑j, h⟩ ∈ Y₀

def Algebraic.MCSP.restrictTo {n : ℕ} (Y₀ : Finset (Fin (2 ^ n))) (tt : Fin (2 ^ n) → Bool) : ↥Y₀ → Bool

Restriction of a truth table tt : Fin (2 ^ n) → Bool to a subset of coordinates Y₀ : Finset (Fin (2 ^ n)).

Equations

• Algebraic.MCSP.restrictTo Y₀ tt i = tt ↑i

theorem Algebraic.MCSP.mcsp_card_image_restrictTo_le_subfunctions_leftBlock {n s : ℕ} (hs : 1 ≤ s) (Y₀ : Finset (Fin (2 ^ n))) : (Finset.image (restrictTo Y₀) (exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s)).card ≤ (Nechiporuk.subfunctions (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) (leftBlock Y₀)).card

Nechiporuk subfunction lower bound for MCSP on arbitrary left-half blocks: For 1 ≤ s and any subset Y₀ : Finset (Fin (2 ^ n)), distinct restrictions restrictTo Y₀ tt of truth tables tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s induce distinct subfunctions of mcspCostScalar ... (n + 1) s on leftBlock Y₀.

theorem Algebraic.MCSP.mcsp_card_exactCostSet_le_subfunctions_leftHalf {n s : ℕ} (hs : 1 ≤ s) : (exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s).card ≤ (Nechiporuk.subfunctions (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) (leftBlock Finset.univ)).card

Full-left-half Nechiporuk subfunction lower bound for MCSP: For 1 ≤ s, every truth table tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s induces a distinct subfunction of mcspCostScalar ... (n + 1) s on the left-half coordinate block leftBlock Finset.univ.

theorem Algebraic.MCSP.mcsp_binaryFormula_leavesIn_leftBlock_lower_bound {n s : ℕ} (hs : 1 ≤ s) (Y₀ : Finset (Fin (2 ^ n))) {F : Binary.Formula (2 ^ (n + 1))} (hF : F.eval = mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) : (Finset.image (restrictTo Y₀) (exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s)).card ≤ 2 * 16 ^ Binary.Formula.leavesIn (leftBlock Y₀) F

Nechiporuk Binary.Formula leaf lower bound for MCSP: For 1 ≤ s, any binary formula F : Binary.Formula (2 ^ (n + 1)) computing mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s satisfies ((exactCostSet ... n s).image (restrictTo Y₀)).card ≤ 2 * 16 ^ F.leavesIn (leftBlock Y₀) for every coordinate subset Y₀ : Finset (Fin (2 ^ n)).

theorem Algebraic.MCSP.mcsp_binaryFormula_leavesIn_leftHalf_lower_bound {n s : ℕ} (hs : 1 ≤ s) {F : Binary.Formula (2 ^ (n + 1))} (hF : F.eval = mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) : (exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s).card ≤ 2 * 16 ^ Binary.Formula.leavesIn (leftBlock Finset.univ) F

Full-left-half Binary.Formula leaf lower bound for MCSP: For 1 ≤ s, any binary formula F : Binary.Formula (2 ^ (n + 1)) computing mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s satisfies (exactCostSet ... n s).card ≤ 2 * 16 ^ F.leavesIn (leftBlock Finset.univ).