Non-vacuity of the MCSP lower bounds

The lower bounds in Complexitylib.Algebraic.LowerBound.MCSP.Symmetry assume that the MCSP predicate is non-constant, and those in Complexitylib.Algebraic.LowerBound.MCSP.SubcubeRepetition assume that some truth table has exact DeMorgan.binaryCost complexity s ≥ 1. This module discharges both hypotheses.

• card_sub_le_costComplexity_deMorgan: a target with k essential inputs and m outputs has DeMorgan.binaryCost complexity at least k - m (weighted frontier counting).
• costComplexity_andTarget: the conjunction x 0 && x 1 of two of n + 2 variables has DeMorgan.binaryCost complexity exactly 1, so exactCostSet DeMorgan.interpretation DeMorgan.binaryCost (n + 2) 1 is nonempty (exactCostSet_deMorgan_one_nonempty).
• mcspCostScalar_deMorgan_succ_ne_of_mem_exactCostSet: if tt has exact complexity s ≥ 1, then mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s is non-constant (pairTruthTable tt tt is a yes-instance; pairing the complement of tt with tt is not).
• Consequently the Symmetry bounds hold for n + 1 without the non-constancy hypothesis (..._of_mem_exactCostSet), and for s = 1 on 2 ^ (n + 3) truth-table inputs they hold with no hypothesis at all (mcspCostTarget_deMorgan_one_binaryCost_lower_bound, mcspCostTarget_deMorgan_one_size_lower_bound, mcsp_one_formula_leaves_lower_bound).

The Binary predicate mcspScalar Binary.interpretation n s is not treated here; its non-constancy remains a hypothesis of the Binary bounds in Symmetry.

Essential inputs lower-bound DeMorgan.binaryCost complexity

theorem Algebraic.MCSP.card_sub_le_costComplexity_deMorgan {N m : ℕ} {target : Target Bool N m} {selected : Finset (Fin N)} (hess : ∀ i ∈ selected, EssentialAt target i) : ↑(selected.card - m) ≤ Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost target

If every coordinate in selected is essential for target, then any De Morgan circuit computing target has binaryCost at least selected.card - m.

A truth table of exact DeMorgan.binaryCost complexity one

def Algebraic.MCSP.andTarget (n : ℕ) : Target Bool (n + 2) 1

The conjunction x 0 && x 1 of the first two of n + 2 input variables.

Equations

• Algebraic.MCSP.andTarget n x x✝ = (x 0 && x 1)

def Algebraic.MCSP.andCircuit (n : ℕ) : Circuit DeMorgan.signature (n + 2) 1

The one-gate De Morgan circuit computing andTarget n.

Equations

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

theorem Algebraic.MCSP.andCircuit_computes (n : ℕ) : (andCircuit n).ComputesWith DeMorgan.interpretation (andTarget n)

andCircuit n computes andTarget n.

@[simp]

theorem Algebraic.MCSP.cost_andCircuit (n : ℕ) : (andCircuit n).cost DeMorgan.binaryCost = 1

andCircuit n has DeMorgan.binaryCost exactly 1.

theorem Algebraic.MCSP.costComplexity_andTarget (n : ℕ) : Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost (andTarget n) = 1

The conjunction of two variables has DeMorgan.binaryCost complexity exactly 1: the one-gate andCircuit gives ≤ 1, and since both variables are essential, frontier counting (card_sub_le_costComplexity_deMorgan) gives ≥ 2 - 1.

theorem Algebraic.MCSP.andTruthTable_mem_exactCostSet (n : ℕ) : (truthTableTargetEquiv (n + 2)).symm (andTarget n) ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost (n + 2) 1

The truth table of andTarget n has exact DeMorgan.binaryCost complexity 1.

theorem Algebraic.MCSP.exactCostSet_deMorgan_one_nonempty (n : ℕ) : (exactCostSet DeMorgan.interpretation DeMorgan.binaryCost (n + 2) 1).Nonempty

For every n, some 2 ^ (n + 2)-bit truth table has exact DeMorgan.binaryCost complexity 1.

Non-constancy of MCSP from an exact-complexity truth table

theorem Algebraic.MCSP.mcspCostScalar_deMorgan_succ_ne_of_mem_exactCostSet {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (pairTruthTable tt tt) ≠ mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s (pairTruthTable (fun (i : Fin (2 ^ n)) => !tt i) tt)

If tt has exact DeMorgan.binaryCost complexity s ≥ 1, then mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s is non-constant: it accepts pairTruthTable tt tt and rejects pairTruthTable (fun i => !tt i) tt.

theorem Algebraic.MCSP.mcspCostScalar_deMorgan_essentialAt_of_mem_exactCostSet {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) (i : Fin (2 ^ (n + 1))) : EssentialAt (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s) i

Hypothesis-free form of mcspCostScalar_deMorgan_essentialAt for n + 1: if some truth table has exact DeMorgan.binaryCost complexity s ≥ 1, every coordinate of mcspCostScalar ... (n + 1) s is essential.

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_inputSupport_eq_univ_of_mem_exactCostSet {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) {c : Circuit σ (2 ^ (n + 1)) 1} (hcomp : c.ComputesWith interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s)) : c.inputSupport = Finset.univ

Hypothesis-free form of mcspCostTarget_deMorgan_inputSupport_eq_univ for n + 1: if some truth table has exact DeMorgan.binaryCost complexity s ≥ 1, every circuit (in any basis) computing mcspCostTarget ... (n + 1) s reads all 2 ^ (n + 1) inputs.

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_binaryCost_lower_bound_of_mem_exactCostSet {n s : ℕ} (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) (hcomp : c.ComputesWith DeMorgan.interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s)) : 2 ^ (n + 1) ≤ c.cost DeMorgan.binaryCost + 1

Hypothesis-free form of mcspCostTarget_deMorgan_binaryCost_lower_bound for n + 1: 2 ^ (n + 1) ≤ c.cost DeMorgan.binaryCost + 1 whenever some truth table has exact DeMorgan.binaryCost complexity s ≥ 1.

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_size_lower_bound_of_mem_exactCostSet {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} (hs : 1 ≤ s) {tt : Fin (2 ^ n) → Bool} (htt : tt ∈ exactCostSet DeMorgan.interpretation DeMorgan.binaryCost n s) (c : Circuit σ (2 ^ (n + 1)) 1) (hfan : c.FanInAtMost 2) (hcomp : c.ComputesWith interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s)) : 2 ^ (n + 1) ≤ c.size + 1

Hypothesis-free form of mcspCostTarget_deMorgan_size_lower_bound for n + 1: 2 ^ (n + 1) ≤ c.size + 1 for every fan-in-2 circuit (in any basis) computing mcspCostTarget ... (n + 1) s, whenever some truth table has exact DeMorgan.binaryCost complexity s ≥ 1.

Fully hypothesis-free bounds for s = 1

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_one_binaryCost_lower_bound (n : ℕ) (c : Circuit DeMorgan.signature (2 ^ (n + 3)) 1) (hcomp : c.ComputesWith DeMorgan.interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 3) 1)) : 2 ^ (n + 3) ≤ c.cost DeMorgan.binaryCost + 1

Every De Morgan circuit computing mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 3) 1 satisfies 2 ^ (n + 3) ≤ c.cost DeMorgan.binaryCost + 1.

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_one_size_lower_bound {σ : Signature} {interpretation : Interpretation σ Bool} (n : ℕ) (c : Circuit σ (2 ^ (n + 3)) 1) (hfan : c.FanInAtMost 2) (hcomp : c.ComputesWith interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 3) 1)) : 2 ^ (n + 3) ≤ c.size + 1

Every fan-in-2 circuit (in any basis) computing mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost (n + 3) 1 satisfies 2 ^ (n + 3) ≤ c.size + 1.

theorem Algebraic.MCSP.mcsp_one_formula_leaves_lower_bound (n : ℕ) {F : KW.Formula (2 ^ (n + 3))} (hF : F.Computes (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 3) 1)) : 2 ^ (n + 3) ≤ F.leaves

Every De Morgan formula computing mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 3) 1 has at least 2 ^ (n + 3) leaves.