Input-XOR symmetry and essential coordinates of MCSP

Flipping a subset of input variables via xorTranslate a (x ↦ fun i => x i ^^ a i) induces a permutation tableTranslate a of the 2 ^ n truth-table coordinates that acts transitively on Fin (2 ^ n).

1. Invariance of DeMorgan.binaryCost complexity: Because NOT gates have zero binaryCost, precomposing a target with xorTranslate a preserves Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost for every a : Fin n → Bool. Consequently, mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s is invariant under tableTranslate a for every s.
2. Invariance of Binary (B₂) gate complexity: Absorbing input negations into the 16 binary gate operations of Binary.signature preserves Program.size and Circuit.size whenever the output wire is a gate, and uses at most 1 gate when the output wire is an input. Consequently, mcspScalar Binary.interpretation n s is invariant under tableTranslate a for all s ≥ 1.
3. All coordinates are essential: Any non-constant function on Fin N → Bool that is invariant under a transitive family of coordinate permutations depends essentially on every coordinate i : Fin N. In particular, whenever mcspCostScalar or mcspScalar is non-constant (hypothesis hne), every truth-table bit is essential, forcing c.inputSupport = Finset.univ. The frontier bounds Circuit.card_inputSupport_le_size and Circuit.card_inputSupport_le_cost then give 2 ^ n ≤ c.size + 1 for fan-in-2 circuits and 2 ^ n ≤ c.cost DeMorgan.binaryCost + 1 for De Morgan circuits.

The non-constancy hypothesis is discharged for the De Morgan predicate in Complexitylib.Algebraic.LowerBound.MCSP.NonVacuity, which shows that mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost (n + 1) s is non-constant whenever some truth table has exact binaryCost complexity s ≥ 1, and exhibits such a table for s = 1. For the Binary predicate mcspScalar Binary.interpretation n s, non-constancy remains a hypothesis.

Input XOR translation and truth-table coordinate permutations

def Algebraic.MCSP.xorTranslate {n : ℕ} (a : Fin n → Bool) : (Fin n → Bool) ≃ (Fin n → Bool)

Translate an n-bit input vector by bitwise XOR with a : Fin n → Bool.

Equations

• Algebraic.MCSP.xorTranslate a = { toFun := fun (x : Fin n → Bool) (i : Fin n) => x i ^^ a i, invFun := fun (x : Fin n → Bool) (i : Fin n) => x i ^^ a i, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Algebraic.MCSP.xorTranslate_apply {n : ℕ} (a x : Fin n → Bool) (i : Fin n) : (xorTranslate a) x i = (x i ^^ a i)

Coordinate i of xorTranslate a x is xor (x i) (a i).

@[simp]

theorem Algebraic.MCSP.xorTranslate_symm {n : ℕ} (a : Fin n → Bool) : (xorTranslate a).symm = xorTranslate a

xorTranslate a is an involution.

@[simp]

theorem Algebraic.MCSP.xorTranslate_self {n : ℕ} (a x : Fin n → Bool) : (xorTranslate a) ((xorTranslate a) x) = x

Applying xorTranslate a twice is the identity.

def Algebraic.MCSP.tableTranslate {n : ℕ} (a : Fin n → Bool) : Equiv.Perm (Fin (2 ^ n))

Permutation of the 2 ^ n truth-table coordinates induced by xorTranslate a.

Equations

• Algebraic.MCSP.tableTranslate a = (Algebraic.MCSP.inputEquiv n).symm.trans ((Algebraic.MCSP.xorTranslate a).trans (Algebraic.MCSP.inputEquiv n))

@[simp]

theorem Algebraic.MCSP.tableTranslate_symm {n : ℕ} (a : Fin n → Bool) : Equiv.symm (tableTranslate a) = tableTranslate a

tableTranslate a is an involution.

@[simp]

theorem Algebraic.MCSP.tableTranslate_inputEquiv {n : ℕ} (a x : Fin n → Bool) : (tableTranslate a) ((inputEquiv n) x) = (inputEquiv n) ((xorTranslate a) x)

tableTranslate a maps the index of x to the index of xorTranslate a x.

@[simp]

theorem Algebraic.MCSP.inputEquiv_symm_tableTranslate {n : ℕ} (a : Fin n → Bool) (i : Fin (2 ^ n)) : (inputEquiv n).symm ((tableTranslate a) i) = (xorTranslate a) ((inputEquiv n).symm i)

Decoding a translated index translates the decoded input.

@[simp]

theorem Algebraic.MCSP.tableTranslate_self {n : ℕ} (a : Fin n → Bool) (i : Fin (2 ^ n)) : (tableTranslate a) ((tableTranslate a) i) = i

Applying tableTranslate a twice is the identity.

@[simp]

theorem Algebraic.MCSP.truthTableTargetEquiv_comp_tableTranslate {n : ℕ} (a : Fin n → Bool) (tt : Fin (2 ^ n) → Bool) : (truthTableTargetEquiv n) (tt ∘ ⇑(tableTranslate a)) = fun (x : Fin n → Bool) (o : Fin 1) => (truthTableTargetEquiv n) tt ((xorTranslate a) x) o

Precomposing a truth table with tableTranslate a corresponds to precomposing the associated target with xorTranslate a.

theorem Algebraic.MCSP.exists_tableTranslate_eq {n : ℕ} (i j : Fin (2 ^ n)) : ∃ (a : Fin n → Bool), (tableTranslate a) i = j

The family of permutations tableTranslate a acts transitively on Fin (2 ^ n).

De Morgan binaryCost invariance under xorTranslate

def Algebraic.MCSP.deMorganLiteralCircuit {n : ℕ} (i : Fin n) (neg : Bool) : Circuit DeMorgan.signature n 1

A single-output De Morgan circuit computing x ↦ xor (x i) neg with zero binaryCost.

Equations

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

@[simp]

theorem Algebraic.MCSP.eval_deMorganLiteralCircuit {n : ℕ} (i : Fin n) (neg : Bool) (x : Fin n → Bool) (o : Fin 1) : (deMorganLiteralCircuit i neg).eval DeMorgan.interpretation x o = (x i ^^ neg)

deMorganLiteralCircuit i neg computes x ↦ xor (x i) neg.

@[simp]

theorem Algebraic.MCSP.cost_deMorganLiteralCircuit {n : ℕ} (i : Fin n) (neg : Bool) : (deMorganLiteralCircuit i neg).cost DeMorgan.binaryCost = 0

deMorganLiteralCircuit i neg has zero binaryCost.

def Algebraic.MCSP.deMorganXorTranslateCircuit {n : ℕ} (a : Fin n → Bool) : Circuit DeMorgan.signature n n

An n-output De Morgan circuit computing xorTranslate a with zero binaryCost.

Equations

• Algebraic.MCSP.deMorganXorTranslateCircuit a = Cslib.Circuits.Circuit.parallelFin n fun (i : Fin n) => Algebraic.MCSP.deMorganLiteralCircuit i (a i)

@[simp]

theorem Algebraic.MCSP.eval_deMorganXorTranslateCircuit {n : ℕ} (a x : Fin n → Bool) : (deMorganXorTranslateCircuit a).eval DeMorgan.interpretation x = (xorTranslate a) x

deMorganXorTranslateCircuit a computes xorTranslate a.

@[simp]

theorem Algebraic.MCSP.cost_deMorganXorTranslateCircuit {n : ℕ} (a : Fin n → Bool) : (deMorganXorTranslateCircuit a).cost DeMorgan.binaryCost = 0

deMorganXorTranslateCircuit a has zero binaryCost.

theorem Algebraic.MCSP.costComplexity_deMorgan_xorTranslate {n m : ℕ} (a : Fin n → Bool) (target : Target Bool n m) : (Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost fun (x : Fin n → Bool) => target ((xorTranslate a) x)) = Circuit.costComplexity DeMorgan.interpretation DeMorgan.binaryCost target

Precomposing a target with xorTranslate a preserves DeMorgan.binaryCost complexity.

@[simp]

theorem Algebraic.MCSP.mcspCostScalar_deMorgan_comp_tableTranslate {n s : ℕ} (a : Fin n → Bool) (tt : Fin (2 ^ n) → Bool) : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s (tt ∘ ⇑(tableTranslate a)) = mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt

mcspCostScalar for DeMorgan.binaryCost is invariant under tableTranslate a.

Full binary basis (B₂) gate-complexity invariance under xorTranslate

def Algebraic.MCSP.wireXorMask {n g : ℕ} (a : Fin n → Bool) : Wire n g → Bool

Mask for a wire under input XOR translation: input i is masked by a i, while internal gate wires are unmasked.

Equations

• Algebraic.MCSP.wireXorMask a = Cslib.Circuits.Wire.elim a fun (x : Fin g) => false

@[simp]

theorem Algebraic.MCSP.wireXorMask_input {n g : ℕ} (a : Fin n → Bool) (i : Fin n) : wireXorMask a (Wire.input i) = a i

The mask of input wire i is a i.

@[simp]

theorem Algebraic.MCSP.wireXorMask_gate {n g : ℕ} (a : Fin n → Bool) (j : Fin g) : wireXorMask a (Wire.gate j) = false

Gate wires are unmasked.

def Algebraic.MCSP.negateInputsBinaryLine {n g : ℕ} (a : Fin n → Bool) (line : Line Binary.signature n g) : Line Binary.signature n g

Absorb input XOR masks into a single Binary.signature gate line.

Equations

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

def Algebraic.MCSP.negateInputsBinaryProgram {n : ℕ} (a : Fin n → Bool) {g : ℕ} : Program Binary.signature n g → Program Binary.signature n g

Absorb input XOR masks into every gate of a Binary.signature program without changing its gate count.

Equations

• Algebraic.MCSP.negateInputsBinaryProgram a Cslib.Circuits.Program.empty = Cslib.Circuits.Program.empty
• Algebraic.MCSP.negateInputsBinaryProgram a (p.gate line) = (Algebraic.MCSP.negateInputsBinaryProgram a p).gate (Algebraic.MCSP.negateInputsBinaryLine a line)

theorem Algebraic.MCSP.eval_negateInputsBinaryProgram {n g : ℕ} (a : Fin n → Bool) (p : Program Binary.signature n g) (x : Fin n → Bool) : (negateInputsBinaryProgram a p).eval Binary.interpretation x = p.eval Binary.interpretation ((xorTranslate a) x)

negateInputsBinaryProgram a p evaluates p on the translated input xorTranslate a x.

theorem Algebraic.MCSP.exists_binary_circuit_xorTranslate {n s : ℕ} (hs : 1 ≤ s) (a : Fin n → Bool) {target : Target Bool n 1} {c : Circuit Binary.signature n 1} (hsize : c.size ≤ s) (hcomp : c.ComputesWith Binary.interpretation target) : ∃ (c' : Circuit Binary.signature n 1), c'.size ≤ s ∧ c'.ComputesWith Binary.interpretation fun (x : Fin n → Bool) => target ((xorTranslate a) x)

For 1 ≤ s, transforming a Binary.signature circuit of size ≤ s produces a circuit of size ≤ s computing the xorTranslate a-shifted target.

theorem Algebraic.MCSP.mcspScalar_binary_comp_tableTranslate {n s : ℕ} (hs : 1 ≤ s) (a : Fin n → Bool) (tt : Fin (2 ^ n) → Bool) : mcspScalar Binary.interpretation n s (tt ∘ ⇑(tableTranslate a)) = mcspScalar Binary.interpretation n s tt

For 1 ≤ s, mcspScalar Binary.interpretation n s is invariant under tableTranslate a.

Essential coordinates of transitive non-constant Boolean functions

theorem Algebraic.MCSP.exists_essentialAt_of_ne {N : ℕ} {V : Type u_1} {F : (Fin N → Bool) → V} {x y : Fin N → Bool} (hne : F x ≠ F y) : ∃ (i : Fin N), EssentialAt F i

Any non-constant function on the Boolean cube has at least one essential coordinate.

theorem Algebraic.MCSP.EssentialAt.perm {N : ℕ} {V : Type u_1} {F : (Fin N → Bool) → V} {π : Equiv.Perm (Fin N)} (hinv : ∀ (x : Fin N → Bool), F (x ∘ ⇑π) = F x) {i : Fin N} (hess : EssentialAt F i) : EssentialAt F (π i)

If F is invariant under precomposition with π : Equiv.Perm (Fin N), then EssentialAt F i implies EssentialAt F (π i).

theorem Algebraic.MCSP.essentialAt_all_of_tableTranslate_invariant {n : ℕ} {V : Type u_1} {F : (Fin (2 ^ n) → Bool) → V} (hinv : ∀ (a : Fin n → Bool) (tt : Fin (2 ^ n) → Bool), F (tt ∘ ⇑(tableTranslate a)) = F tt) {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : F tt₀ ≠ F tt₁) (i : Fin (2 ^ n)) : EssentialAt F i

Any non-constant function on Fin (2 ^ n) → Bool that is invariant under tableTranslate a for all a : Fin n → Bool has every coordinate i : Fin (2 ^ n) essential.

theorem Algebraic.MCSP.inputSupport_eq_univ_of_forall_essentialAt {σ : Signature} {interpretation : Interpretation σ Bool} {N : ℕ} {F : (Fin N → Bool) → Bool} {T : Target Bool N 1} (hT : ∀ (x : Fin N → Bool), T x 0 = F x) (hess : ∀ (i : Fin N), EssentialAt F i) {c : Circuit σ N 1} (hcomp : c.ComputesWith interpretation T) : c.inputSupport = Finset.univ

If every coordinate is essential for a scalar function F, then every circuit (in any basis) computing a single-output target T with T x 0 = F x reads every input.

Input-support bounds for De Morgan circuits

theorem Algebraic.MCSP.deMorgan_arity_le_binaryCost_add_one (op : DeMorgan.signature.Op) : DeMorgan.signature.Arity op ≤ DeMorgan.binaryCost op + 1

Every De Morgan operation has arity at most its binaryCost plus one, so the weighted frontier bound Circuit.card_inputSupport_le_cost applies to DeMorgan.binaryCost.

theorem Algebraic.MCSP.card_inputSupport_le_binaryCost {N m : ℕ} (c : Circuit DeMorgan.signature N m) : c.inputSupport.card ≤ m + c.cost DeMorgan.binaryCost

A De Morgan circuit with m outputs reads at most m + c.cost DeMorgan.binaryCost inputs.

Essential coordinates and 2 ^ n - 1 circuit size / cost bounds for non-constant MCSP

theorem Algebraic.MCSP.mcspCostScalar_deMorgan_essentialAt {n s : ℕ} {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₀ ≠ mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₁) (i : Fin (2 ^ n)) : EssentialAt (mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s) i

Whenever mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s is non-constant, every truth-table coordinate i : Fin (2 ^ n) is essential.

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_inputSupport_eq_univ {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₀ ≠ mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₁) {c : Circuit σ (2 ^ n) 1} (hcomp : c.ComputesWith interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost n s)) : c.inputSupport = Finset.univ

Any circuit (in any basis) computing non-constant mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost n s must include every truth-table coordinate in its inputSupport.

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_binaryCost_lower_bound {n s : ℕ} {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₀ ≠ mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₁) (c : Circuit DeMorgan.signature (2 ^ n) 1) (hcomp : c.ComputesWith DeMorgan.interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost n s)) : 2 ^ n ≤ c.cost DeMorgan.binaryCost + 1

2 ^ n ≤ c.cost DeMorgan.binaryCost + 1 for any De Morgan circuit computing mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost n s, provided this predicate is non-constant (hne).

theorem Algebraic.MCSP.mcspCostTarget_deMorgan_size_lower_bound {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₀ ≠ mcspCostScalar DeMorgan.interpretation DeMorgan.binaryCost n s tt₁) (c : Circuit σ (2 ^ n) 1) (hfan : c.FanInAtMost 2) (hcomp : c.ComputesWith interpretation (mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost n s)) : 2 ^ n ≤ c.size + 1

2 ^ n ≤ c.size + 1 for any fan-in-2 circuit (in any basis) computing mcspCostTarget DeMorgan.interpretation DeMorgan.binaryCost n s, provided this predicate is non-constant (hne).

theorem Algebraic.MCSP.mcspScalar_binary_essentialAt {n s : ℕ} (hs : 1 ≤ s) {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspScalar Binary.interpretation n s tt₀ ≠ mcspScalar Binary.interpretation n s tt₁) (i : Fin (2 ^ n)) : EssentialAt (mcspScalar Binary.interpretation n s) i

Whenever 1 ≤ s and mcspScalar Binary.interpretation n s is non-constant, every truth-table coordinate i : Fin (2 ^ n) is essential.

theorem Algebraic.MCSP.mcspTarget_binary_inputSupport_eq_univ {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} (hs : 1 ≤ s) {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspScalar Binary.interpretation n s tt₀ ≠ mcspScalar Binary.interpretation n s tt₁) {c : Circuit σ (2 ^ n) 1} (hcomp : c.ComputesWith interpretation (mcspTarget Binary.interpretation n s)) : c.inputSupport = Finset.univ

Any circuit (in any basis) computing mcspTarget Binary.interpretation n s (1 ≤ s), provided this predicate is non-constant, must include every truth-table coordinate in its inputSupport.

theorem Algebraic.MCSP.mcspTarget_binary_size_lower_bound {σ : Signature} {interpretation : Interpretation σ Bool} {n s : ℕ} (hs : 1 ≤ s) {tt₀ tt₁ : Fin (2 ^ n) → Bool} (hne : mcspScalar Binary.interpretation n s tt₀ ≠ mcspScalar Binary.interpretation n s tt₁) (c : Circuit σ (2 ^ n) 1) (hfan : c.FanInAtMost 2) (hcomp : c.ComputesWith interpretation (mcspTarget Binary.interpretation n s)) : 2 ^ n ≤ c.size + 1

2 ^ n ≤ c.size + 1 for any fan-in-2 circuit (in any basis) computing mcspTarget Binary.interpretation n s (1 ≤ s), provided this predicate is non-constant (hne).