Minimum Circuit Size Problem (MCSP) definitions

This module defines the Minimum Circuit Size Problem (MCSP) as a family of Boolean functions on truth tables of length 2 ^ n.

• inputEquiv n: canonical recursive bijection (Fin n → Bool) ≃ Fin (2 ^ n) splitting on the first coordinate 0 : Fin (n + 1).
• truthTableEquiv n and truthTableTargetEquiv n: equivalences between truth tables Fin (2 ^ n) → Bool, scalar Boolean functions ScalarFunction Bool n, and single-output targets Target Bool n 1.
• pairTruthTable tt₀ tt₁: concatenates two 2 ^ n-bit truth tables into a 2 ^ (n + 1)-bit truth table corresponding to the subcube multiplexer muxTarget.
• mcspScalar / mcspTarget: gate-complexity MCSP predicate for an arbitrary basis.
• mcspCostScalar / mcspCostTarget: operation-cost MCSP predicate (used in particular with DeMorgan.binaryCost where NOT gates are free).
• yesSet, costYesSet, and exactCostSet: finite sets of truth tables with complexity ≤ s or = s. For gate complexity, |yesSet| is bounded above by the ordered and sharp Shannon-style circuit-counting budgets (card_yesSet_le_orderedBudget, card_yesSet_le_sharpBudget); no counting bounds are given for costYesSet or exactCostSet.

Relation to Complexity.MCSP

Complexity.MCSP (Complexitylib/Metacomplexity/MCSP/Defs.lean) is the language-level problem: encoded instances carrying an arity, a truth table, and a threshold, decided with respect to Basis.andOr2 circuit size. The definitions here are the algebraic-circuit-model variant: for fixed n and s, MCSP is a Boolean function on 2 ^ n truth-table bits, parametrized by an arbitrary basis interpretation and operation cost. The truth-table indexing also differs: inputEquiv is big-endian (x 0 is the most significant bit, selecting the lower or upper half), whereas Complexity.MCSP.Instance.inputIndex is little-endian (variable j is bit j of the index).

def Algebraic.MCSP.inputEquiv (n : ℕ) : (Fin n → Bool) ≃ Fin (2 ^ n)

Canonical recursive bijection between n-bit inputs and truth-table indices Fin (2 ^ n). For n + 1, inputs with x 0 = false map to the lower half 0 .. 2 ^ n - 1 and inputs with x 0 = true map to the upper half 2 ^ n .. 2 ^ (n + 1) - 1.

Equations

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

@[simp]

theorem Algebraic.MCSP.inputEquiv_cons_false {n : ℕ} (y : Fin n → Bool) : ↑((inputEquiv (n + 1)) (Fin.cons false y)) = ↑((inputEquiv n) y)

Inputs with leading bit false index the lower half of the truth table.

@[simp]

theorem Algebraic.MCSP.inputEquiv_cons_true {n : ℕ} (y : Fin n → Bool) : ↑((inputEquiv (n + 1)) (Fin.cons true y)) = 2 ^ n + ↑((inputEquiv n) y)

Inputs with leading bit true index the upper half of the truth table.

theorem Algebraic.MCSP.inputEquiv_symm_lt {n : ℕ} {i : Fin (2 ^ (n + 1))} (h : ↑i < 2 ^ n) : (inputEquiv (n + 1)).symm i = Fin.cons false ((inputEquiv n).symm ⟨↑i, h⟩)

Lower-half indices decode to inputs with leading bit false.

theorem Algebraic.MCSP.inputEquiv_symm_ge {n : ℕ} {i : Fin (2 ^ (n + 1))} (h : ¬↑i < 2 ^ n) : (inputEquiv (n + 1)).symm i = Fin.cons true ((inputEquiv n).symm ⟨↑i - 2 ^ n, ⋯⟩)

Upper-half indices decode to inputs with leading bit true.

def Algebraic.MCSP.truthTableEquiv (n : ℕ) : (Fin (2 ^ n) → Bool) ≃ ScalarFunction Bool n

Equivalence between 2 ^ n-bit truth tables and n-variable scalar Boolean functions.

Equations

• Algebraic.MCSP.truthTableEquiv n = (Algebraic.MCSP.inputEquiv n).symm.arrowCongr (Equiv.refl Bool)

@[simp]

theorem Algebraic.MCSP.truthTableEquiv_apply {n : ℕ} (tt : Fin (2 ^ n) → Bool) (x : Fin n → Bool) : (truthTableEquiv n) tt x = tt ((inputEquiv n) x)

Evaluating the function of a truth table reads the entry at the input's index.

@[simp]

theorem Algebraic.MCSP.truthTableEquiv_symm_apply {n : ℕ} (f : ScalarFunction Bool n) (i : Fin (2 ^ n)) : (truthTableEquiv n).symm f i = f ((inputEquiv n).symm i)

The truth table of a function lists its value at each decoded index.

def Algebraic.MCSP.scalarTargetEquiv (n : ℕ) : ScalarFunction Bool n ≃ Target Bool n 1

Equivalence between scalar Boolean functions and single-output Targets.

Equations

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

def Algebraic.MCSP.truthTableTargetEquiv (n : ℕ) : (Fin (2 ^ n) → Bool) ≃ Target Bool n 1

Equivalence between 2 ^ n-bit truth tables and single-output n-variable Boolean targets.

Equations

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

@[simp]

theorem Algebraic.MCSP.truthTableTargetEquiv_apply {n : ℕ} (tt : Fin (2 ^ n) → Bool) (x : Fin n → Bool) (o : Fin 1) : (truthTableTargetEquiv n) tt x o = tt ((inputEquiv n) x)

Evaluating the target of a truth table reads the entry at the input's index.

@[simp]

theorem Algebraic.MCSP.truthTableTargetEquiv_symm_apply {n : ℕ} (target : Target Bool n 1) (i : Fin (2 ^ n)) : (truthTableTargetEquiv n).symm target i = target ((inputEquiv n).symm i) 0

The truth table of a target lists its value at each decoded index.

def Algebraic.MCSP.muxTarget {n : ℕ} (u₀ u₁ : Target Bool n 1) : Target Bool (n + 1) 1

Multiplex two n-variable targets along the leading input bit 0 : Fin (n + 1).

Equations

• Algebraic.MCSP.muxTarget u₀ u₁ x o = if x 0 = true then u₁ (Fin.tail x) o else u₀ (Fin.tail x) o

@[simp]

theorem Algebraic.MCSP.muxTarget_cons_false {n : ℕ} (u₀ u₁ : Target Bool n 1) (y : Fin n → Bool) (o : Fin 1) : muxTarget u₀ u₁ (Fin.cons false y) o = u₀ y o

On the x 0 = false subcube, muxTarget u₀ u₁ agrees with u₀.

@[simp]

theorem Algebraic.MCSP.muxTarget_cons_true {n : ℕ} (u₀ u₁ : Target Bool n 1) (y : Fin n → Bool) (o : Fin 1) : muxTarget u₀ u₁ (Fin.cons true y) o = u₁ y o

On the x 0 = true subcube, muxTarget u₀ u₁ agrees with u₁.

def Algebraic.MCSP.pairTruthTable {n : ℕ} (tt₀ tt₁ : Fin (2 ^ n) → Bool) : Fin (2 ^ (n + 1)) → Bool

Concatenate two 2 ^ n-bit truth tables into a 2 ^ (n + 1)-bit truth table.

Equations

• Algebraic.MCSP.pairTruthTable tt₀ tt₁ i = if h : ↑i < 2 ^ n then tt₀ ⟨↑i, h⟩ else tt₁ ⟨↑i - 2 ^ n, ⋯⟩

def Algebraic.MCSP.leftHalf {n : ℕ} (tt : Fin (2 ^ (n + 1)) → Bool) : Fin (2 ^ n) → Bool

Extract the lower half (x 0 = false subcube) of a 2 ^ (n + 1)-bit truth table.

Equations

• Algebraic.MCSP.leftHalf tt i = tt ⟨↑i, ⋯⟩

def Algebraic.MCSP.rightHalf {n : ℕ} (tt : Fin (2 ^ (n + 1)) → Bool) : Fin (2 ^ n) → Bool

Extract the upper half (x 0 = true subcube) of a 2 ^ (n + 1)-bit truth table.

Equations

• Algebraic.MCSP.rightHalf tt i = tt ⟨2 ^ n + ↑i, ⋯⟩

@[simp]

theorem Algebraic.MCSP.leftHalf_pairTruthTable {n : ℕ} (tt₀ tt₁ : Fin (2 ^ n) → Bool) : leftHalf (pairTruthTable tt₀ tt₁) = tt₀

The lower half of pairTruthTable tt₀ tt₁ is tt₀.

@[simp]

theorem Algebraic.MCSP.rightHalf_pairTruthTable {n : ℕ} (tt₀ tt₁ : Fin (2 ^ n) → Bool) : rightHalf (pairTruthTable tt₀ tt₁) = tt₁

The upper half of pairTruthTable tt₀ tt₁ is tt₁.

@[simp]

theorem Algebraic.MCSP.pairTruthTable_leftHalf_rightHalf {n : ℕ} (tt : Fin (2 ^ (n + 1)) → Bool) : pairTruthTable (leftHalf tt) (rightHalf tt) = tt

Every 2 ^ (n + 1)-bit truth table is the pairing of its two halves.

theorem Algebraic.MCSP.pairTruthTable_injective_left {n : ℕ} {tt₀ tt₀' tt₁ : Fin (2 ^ n) → Bool} (h : pairTruthTable tt₀ tt₁ = pairTruthTable tt₀' tt₁) : tt₀ = tt₀'

pairTruthTable is injective in its first (lower-half) argument.

theorem Algebraic.MCSP.pairTruthTable_injective_right {n : ℕ} {tt₀ tt₁ tt₁' : Fin (2 ^ n) → Bool} (h : pairTruthTable tt₀ tt₁ = pairTruthTable tt₀ tt₁') : tt₁ = tt₁'

pairTruthTable is injective in its second (upper-half) argument.

theorem Algebraic.MCSP.truthTableTargetEquiv_pairTruthTable {n : ℕ} (tt₀ tt₁ : Fin (2 ^ n) → Bool) : (truthTableTargetEquiv (n + 1)) (pairTruthTable tt₀ tt₁) = muxTarget ((truthTableTargetEquiv n) tt₀) ((truthTableTargetEquiv n) tt₁)

Pairing two truth tables corresponds under truthTableTargetEquiv to muxTarget.

noncomputable def Algebraic.MCSP.mcspScalar {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) : ScalarFunction Bool (2 ^ n)

Gate-complexity MCSP as a scalar Boolean function on 2 ^ n-bit truth tables.

Equations

• Algebraic.MCSP.mcspScalar interpretation n s tt = decide (Cslib.Circuits.Circuit.gateComplexity interpretation ((Algebraic.MCSP.truthTableTargetEquiv n) tt) ≤ ↑s)

noncomputable def Algebraic.MCSP.mcspTarget {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) : Target Bool (2 ^ n) 1

Gate-complexity MCSP as a single-output Target.

Equations

• Algebraic.MCSP.mcspTarget interpretation n s tt x✝ = Algebraic.MCSP.mcspScalar interpretation n s tt

@[simp]

theorem Algebraic.MCSP.mcspScalar_eq_true_iff {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : mcspScalar interpretation n s tt = true ↔ Circuit.gateComplexity interpretation ((truthTableTargetEquiv n) tt) ≤ ↑s

mcspScalar accepts exactly the truth tables of gate complexity at most s.

@[simp]

theorem Algebraic.MCSP.mcspScalar_eq_false_iff {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : mcspScalar interpretation n s tt = false ↔ ↑s < Circuit.gateComplexity interpretation ((truthTableTargetEquiv n) tt)

mcspScalar rejects exactly the truth tables of gate complexity above s.

noncomputable def Algebraic.MCSP.mcspCostScalar {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) : ScalarFunction Bool (2 ^ n)

Operation-cost MCSP as a scalar Boolean function on 2 ^ n-bit truth tables.

Equations

• Algebraic.MCSP.mcspCostScalar interpretation cost n s tt = decide (Cslib.Circuits.Circuit.costComplexity interpretation cost ((Algebraic.MCSP.truthTableTargetEquiv n) tt) ≤ ↑s)

noncomputable def Algebraic.MCSP.mcspCostTarget {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) : Target Bool (2 ^ n) 1

Operation-cost MCSP as a single-output Target.

Equations

• Algebraic.MCSP.mcspCostTarget interpretation cost n s tt x✝ = Algebraic.MCSP.mcspCostScalar interpretation cost n s tt

@[simp]

theorem Algebraic.MCSP.mcspCostScalar_eq_true_iff {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : mcspCostScalar interpretation cost n s tt = true ↔ Circuit.costComplexity interpretation cost ((truthTableTargetEquiv n) tt) ≤ ↑s

mcspCostScalar accepts exactly the truth tables of cost complexity at most s.

@[simp]

theorem Algebraic.MCSP.mcspCostScalar_eq_false_iff {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : mcspCostScalar interpretation cost n s tt = false ↔ ↑s < Circuit.costComplexity interpretation cost ((truthTableTargetEquiv n) tt)

mcspCostScalar rejects exactly the truth tables of cost complexity above s.

@[simp]

theorem Algebraic.MCSP.mcspCostScalar_unit {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) : mcspCostScalar interpretation OperationCost.unit n s = mcspScalar interpretation n s

With unit operation cost, mcspCostScalar is gate-complexity mcspScalar.

noncomputable def Algebraic.MCSP.yesSet {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) : Finset (Fin (2 ^ n) → Bool)

The finite set of 2 ^ n-bit truth tables with gate complexity at most s.

Equations

• Algebraic.MCSP.yesSet interpretation n s = {tt : Fin (2 ^ n) → Bool | Algebraic.MCSP.mcspScalar interpretation n s tt = true}

@[simp]

theorem Algebraic.MCSP.mem_yesSet_iff {σ : Signature} (interpretation : Interpretation σ Bool) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : tt ∈ yesSet interpretation n s ↔ Circuit.gateComplexity interpretation ((truthTableTargetEquiv n) tt) ≤ ↑s

Membership in yesSet is gate complexity at most s.

noncomputable def Algebraic.MCSP.costYesSet {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) : Finset (Fin (2 ^ n) → Bool)

The finite set of 2 ^ n-bit truth tables with operation-cost complexity at most s.

Equations

• Algebraic.MCSP.costYesSet interpretation cost n s = {tt : Fin (2 ^ n) → Bool | Algebraic.MCSP.mcspCostScalar interpretation cost n s tt = true}

@[simp]

theorem Algebraic.MCSP.mem_costYesSet_iff {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : tt ∈ costYesSet interpretation cost n s ↔ Circuit.costComplexity interpretation cost ((truthTableTargetEquiv n) tt) ≤ ↑s

Membership in costYesSet is cost complexity at most s.

noncomputable def Algebraic.MCSP.exactCostSet {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) : Finset (Fin (2 ^ n) → Bool)

The finite set of 2 ^ n-bit truth tables with operation-cost complexity exactly s.

Equations

• Algebraic.MCSP.exactCostSet interpretation cost n s = {tt : Fin (2 ^ n) → Bool | Cslib.Circuits.Circuit.costComplexity interpretation cost ((Algebraic.MCSP.truthTableTargetEquiv n) tt) = ↑s}

@[simp]

theorem Algebraic.MCSP.mem_exactCostSet_iff {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) (tt : Fin (2 ^ n) → Bool) : tt ∈ exactCostSet interpretation cost n s ↔ Circuit.costComplexity interpretation cost ((truthTableTargetEquiv n) tt) = ↑s

Membership in exactCostSet is cost complexity exactly s.

theorem Algebraic.MCSP.exactCostSet_subset_costYesSet {σ : Signature} (interpretation : Interpretation σ Bool) (cost : OperationCost σ) (n s : ℕ) : exactCostSet interpretation cost n s ⊆ costYesSet interpretation cost n s

Truth tables of cost complexity exactly s are yes instances at threshold s.

theorem Algebraic.MCSP.card_yesSet_eq_card_functionsAtMost {σ : Signature} [Fintype σ.Op] (interpretation : Interpretation σ Bool) (n s : ℕ) : (yesSet interpretation n s).card = (Circuit.functionsAtMost interpretation n 1 s).card

yesSet has the same cardinality as Circuit.functionsAtMost.

theorem Algebraic.MCSP.card_yesSet_le_orderedBudget {σ : Signature} [Fintype σ.Op] (interpretation : Interpretation σ Bool) (n s : ℕ) : (yesSet interpretation n s).card ≤ σ.orderedBudget n 1 s

Ordered-syntax Shannon upper bound on the number of yes truth tables of MCSP.

theorem Algebraic.MCSP.card_yesSet_le_sharpBudget {σ : Signature} [Fintype σ.Op] (interpretation : Interpretation σ Bool) (n s : ℕ) : (yesSet interpretation n s).card ≤ σ.sharpBudget n 1 s

Sharp (g!-reduced) Shannon upper bound on the number of yes truth tables of MCSP.