Documentation

Complexitylib.Algebraic.LowerBound.GateElimination.DeMorganXor

The De Morgan XOR lower bound #

This file proves the lower bound 3 * (n - 1) as an instance of the generic gate-elimination framework. Its basis-specific core constructs a local, proof-carrying simplification of a De Morgan parity circuit which saves three AND/OR gates after fixing one input.

source
noncomputable def Algebraic.DeMorgan.XorElimination.eliminate (n : ℕ) (positive : 0 < n) (phase : Bool) (circuit : Circuit signature (n + 1) 1) (computes : circuit.ComputesWith interpretation (GateElimination.Xor.target { inputCount := n + 1, phase := phase })) :
GateElimination.Xor.ThreeGateStep binaryCost interpretation n phase circuit

Concrete three-gate elimination for a De Morgan parity circuit.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.DeMorgan.xorThreeGateEliminator :
    GateElimination.Xor.ThreeGateEliminator binaryCost interpretation

    De Morgan circuits admit the local three-gate elimination required by XOR. Witness selection is classical, so this is a proof certificate rather than an executable elimination procedure.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.DeMorgan.xor_lowerBound {n : ℕ} (circuit : Circuit signature n 1) (computes : circuit.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) :
      3 * (n - 1) ≤ circuit.cost binaryCost

      Every De Morgan circuit computing n-input XOR has at least 3 * (n - 1) AND/OR gates. Constants and NOT gates are free in this cost model.