Strictness of the conditional chain bound

In CSLib's Boolean basis (AND, OR, NOT, and constants, each of cost one), let f(x,y) = x ∧ y and g(x,y) = ¬(x ∧ y). Then C(f,g) = C(g) = 2, whereas C(f | g) = 1. The two-gate NAND circuit already contains the AND output. Supplying only NAND as a free input loses access to that intermediate wire.

All equalities are kernel-checked. The tiny one-gate lower bound enumerates the finite operation, wiring, output, and input choices using decide.

def Algebraic.ConditionalComplexity.andTarget : Target Bool 2 1

The two-input conjunction as a single-output target.

Equations

• Algebraic.ConditionalComplexity.andTarget input x✝ = (input 0 && input 1)

def Algebraic.ConditionalComplexity.nandTarget : Target Bool 2 1

The negation of two-input conjunction as a single-output target.

Equations

• Algebraic.ConditionalComplexity.nandTarget input x✝ = !(input 0 && input 1)

def Algebraic.ConditionalComplexity.andNandCircuit : Circuit Cslib.Circuits.Boolean.signature 2 (1 + 1)

Two gates with both the intermediate AND and final NAND exposed.

Equations

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

@[simp]

theorem Algebraic.ConditionalComplexity.andNandCircuit_size : andNandCircuit.size = 2

The shared circuit has exactly two gates: the AND and the NOT that turns it into the NAND.

theorem Algebraic.ConditionalComplexity.andNandCircuit_computes : andNandCircuit.ComputesWith Cslib.Circuits.Boolean.interpretation fun (input : Fin 2 → Bool) => Fin.append (andTarget input) (nandTarget input)

The shared circuit computes the pair of functions.

theorem Algebraic.ConditionalComplexity.gateComplexity_nand : Circuit.gateComplexity Cslib.Circuits.Boolean.interpretation nandTarget = 2

NAND requires exactly two gates in the AND/OR/NOT basis.

theorem Algebraic.ConditionalComplexity.gateComplexity_and_nand : (Circuit.gateComplexity Cslib.Circuits.Boolean.interpretation fun (input : Fin 2 → Bool) => Fin.append (andTarget input) (nandTarget input)) = 2

Exposing the intermediate conjunction in the NAND circuit is free.

theorem Algebraic.ConditionalComplexity.conditionalGateComplexity_and_given_nand : Circuit.conditionalGateComplexity Cslib.Circuits.Boolean.interpretation andTarget nandTarget = 1

Given NAND as a supplied value, one NOT gate recovers AND.

theorem Algebraic.ConditionalComplexity.gateComplexity_pair_lt_conditional_add : (Circuit.gateComplexity Cslib.Circuits.Boolean.interpretation fun (input : Fin 2 → Bool) => Fin.append (andTarget input) (nandTarget input)) < Circuit.conditionalGateComplexity Cslib.Circuits.Boolean.interpretation andTarget nandTarget + Circuit.gateComplexity Cslib.Circuits.Boolean.interpretation nandTarget

The chain upper bound can be strict: its two sides here are 2 and 3.