XOR as an instance of gate elimination

This module specializes the basis-independent gate-elimination framework to Boolean parity. It deliberately isolates the one basis-specific obligation: after fixing one input of an at-least-two-input parity circuit, construct a certified reduction saving at least three charged gates.

Any signature, interpretation, and operation cost satisfying that local obligation inherits the lower bound 3 * (n - 1). In particular, the De Morgan theorem can use the cost which charges AND and OR but makes constants and NOT free. A matching upper bound is outside this module.

def Algebraic.GateElimination.Xor.parity {n : ℕ} (input : Fin n → Bool) : Bool

XOR of all coordinates, using the Boolean-ring addition on Bool.

Equations

• Algebraic.GateElimination.Xor.parity input = ∑ coordinate : Fin n, input coordinate

def Algebraic.GateElimination.Xor.parityTarget (n : ℕ) : Target Bool n 1

Unflipped parity as a one-output target.

Equations

• Algebraic.GateElimination.Xor.parityTarget n input x✝ = Algebraic.GateElimination.Xor.parity input

structure Algebraic.GateElimination.Xor.State : Type

A parity problem records its number of inputs and an optional output flip.

• inputCount : ℕ

  Number of inputs.

• phase : Bool

  Whether the parity output is flipped.

@[instance_reducible]

instance Algebraic.GateElimination.Xor.instDecidableEqState : DecidableEq State

Equations

• Algebraic.GateElimination.Xor.instDecidableEqState = Algebraic.GateElimination.Xor.instDecidableEqState.decEq

def Algebraic.GateElimination.Xor.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

Equations

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

def Algebraic.GateElimination.Xor.target (state : State) : Target Bool state.inputCount 1

Parity, optionally flipped by state.phase, as a one-output target.

Equations

• Algebraic.GateElimination.Xor.target state input x✝ = Algebraic.GateElimination.Xor.parity input + state.phase

theorem Algebraic.GateElimination.Xor.target_essentialAt (state : State) (selected : Fin state.inputCount) : EssentialAt (fun (input : Fin state.inputCount → Bool) => target state input 0) selected

Every coordinate is essential to phased parity.

theorem Algebraic.GateElimination.Xor.target_ne_of_selected_ne (state : State) (selected : Fin state.inputCount) (left right : Fin state.inputCount → Bool) (agree : ∀ (input : Fin state.inputCount), input ≠ selected → left input = right input) (different : left selected ≠ right selected) : target state left 0 ≠ target state right 0

Flipping one coordinate flips phased parity, regardless of the other inputs.

@[simp]

theorem Algebraic.GateElimination.Xor.target_false (n : ℕ) : target { inputCount := n, phase := false } = parityTarget n

def Algebraic.GateElimination.Xor.problem (state : State) : Problem Bool 1

Package a parity state as a gate-elimination problem.

Equations

• Algebraic.GateElimination.Xor.problem state = { inputCount := state.inputCount, target := Algebraic.GateElimination.Xor.target state }

def Algebraic.GateElimination.Xor.restriction (n : ℕ) (phase value : Bool) (selected : Fin (n + 1)) : (problem { inputCount := n + 1, phase := phase }).Restriction (problem { inputCount := n, phase := value + phase })

Fixing one parity input removes that input and adds its value to the phase.

Equations

• Algebraic.GateElimination.Xor.restriction n phase value selected = { substitution := Algebraic.InputSubstitution.fix selected value, target_eq := ⋯ }

def Algebraic.GateElimination.Xor.rank (state : State) : ℕ

The well-founded rank of a parity problem.

Equations

• Algebraic.GateElimination.Xor.rank state = state.inputCount

def Algebraic.GateElimination.Xor.bound (state : State) : ℕ

The Schnorr-style lower-bound expression proved by the framework.

Equations

• Algebraic.GateElimination.Xor.bound state = 3 * (state.inputCount - 1)

structure Algebraic.GateElimination.Xor.ThreeGateStep {σ : Signature} (operationCost : OperationCost σ) (interpretation : Interpretation σ Bool) (n : ℕ) (phase : Bool) (circuit : Circuit σ (n + 1) 1) : Type u_1

The data produced by one basis-specific XOR elimination.

The residual circuit must agree with the original circuit after fixing selected to value; the cost certificate must save at least three.

• selected : Fin (n + 1)

  Input fixed by this elimination.

• value : Bool

  Boolean value assigned to the selected input.

• reduction : Circuit.Reduction operationCost circuit interpretation (InputSubstitution.fix self.selected self.value)

  Semantics- and cost-certified residual circuit.

• saves_three : 3 ≤ self.reduction.saving

  The reduction removes at least three units of charged cost.

structure Algebraic.GateElimination.Xor.ThreeGateEliminator {σ : Signature} (operationCost : OperationCost σ) (interpretation : Interpretation σ Bool) : Type u_1

The sole basis-specific hypothesis needed for the XOR lower bound.

It is stated for an arbitrary circuit signature and arbitrary weighted cost. The positivity premise says that the residual parity problem still has at least one input, so the source has at least two inputs.

• eliminate (n : ℕ) : 0 < n → (phase : Bool) → (circuit : Circuit σ (n + 1) 1) → circuit.ComputesWith interpretation (target { inputCount := n + 1, phase := phase }) → Circuit.CostSizeMinimal operationCost circuit interpretation (target { inputCount := n + 1, phase := phase }) → ThreeGateStep operationCost interpretation n phase circuit

  Produce a three-unit reduction for every minimum-cost non-base circuit.

def Algebraic.GateElimination.Xor.framework {σ : Signature} {operationCost : OperationCost σ} {interpretation : Interpretation σ Bool} (eliminator : ThreeGateEliminator operationCost interpretation) : OptimalFramework operationCost interpretation 1

Turn a local three-gate XOR eliminator into the generic framework.

Equations

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

theorem Algebraic.GateElimination.Xor.lowerBound {σ : Signature} {operationCost : OperationCost σ} {interpretation : Interpretation σ Bool} (eliminator : ThreeGateEliminator operationCost interpretation) (state : State) (circuit : Circuit σ state.inputCount 1) (computes : circuit.ComputesWith interpretation (target state)) : 3 * (state.inputCount - 1) ≤ circuit.cost operationCost

Every basis admitting the local three-gate elimination has XOR cost at least 3 * (n - 1).

theorem Algebraic.GateElimination.Xor.parity_lowerBound {σ : Signature} {operationCost : OperationCost σ} {interpretation : Interpretation σ Bool} (eliminator : ThreeGateEliminator operationCost interpretation) {n : ℕ} (circuit : Circuit σ n 1) (computes : circuit.ComputesWith interpretation (parityTarget n)) : 3 * (n - 1) ≤ circuit.cost operationCost

Unflipped XOR specialization of lowerBound.