Internal: Schnorr's 3(N - 1) bound via De Morgan gate elimination

This module translates a straight-line Basis.andOr2 program into a straight-line De Morgan program (Algebraic.DeMorgan.signature) with the same wire values and whose charged binary-gate cost equals the source gate count. Composing with the three-gate elimination theorem Algebraic.GateElimination.Xor.lowerBound for Algebraic.DeMorgan.xorThreeGateEliminator gives parity_size_ge_three_mul_internal, the proof of the public theorem parity_size_ge_three_mul in Complexitylib.Circuits.Schnorr.

structure Complexity.SchnorrDeMorgan.Translation {N s : ℕ} (p : Cslib.Circuits.Program Basis.andOr2.signature N s) : Type

A De Morgan program simulating a straight-line Basis.andOr2 program p: every source wire is mapped to a target wire with the same value, and the target's charged binary-gate cost equals the number of source gates.

• gateCount : ℕ

  Number of gates in the translated program.

• result : Cslib.Circuits.Program Algebraic.DeMorgan.signature N self.gateCount

  The translated De Morgan program.

• wireMap : Cslib.Circuits.Wire N s → Cslib.Circuits.Wire N self.gateCount

  Where each source wire lives in the translated program.

• trace_eq (x : BitString N) (w : Cslib.Circuits.Wire N s) : self.result.trace Algebraic.DeMorgan.interpretation x (self.wireMap w) = p.trace Basis.andOr2.interpretation x w

  Wire values are preserved.

• cost_eq : Cslib.Circuits.Program.cost Algebraic.DeMorgan.binaryCost self.result = s

  Binary-gate cost equals the source gate count.

def Complexity.SchnorrDeMorgan.toBinaryOp : AndOrOp → Algebraic.DeMorgan.BinaryOp

The De Morgan binary operation corresponding to an AND/OR operation.

Equations

• Complexity.SchnorrDeMorgan.toBinaryOp Complexity.AndOrOp.and = Algebraic.DeMorgan.BinaryOp.and
• Complexity.SchnorrDeMorgan.toBinaryOp Complexity.AndOrOp.or = Algebraic.DeMorgan.BinaryOp.or

theorem Complexity.SchnorrDeMorgan.toBinaryOp_eval (op : AndOrOp) (inputs : BitString 2) : (toBinaryOp op).eval (inputs 0) (inputs 1) = op.eval 2 inputs

A fan-in-two AND/OR gate and its De Morgan counterpart agree on every pair of input values.

def Complexity.SchnorrDeMorgan.translate {N s : ℕ} (p : Cslib.Circuits.Program Basis.andOr2.signature N s) : Translation p

Translate a straight-line Basis.andOr2 program gate by gate into a De Morgan program, absorbing input negations into residual wire values.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.SchnorrDeMorgan.translate Cslib.Circuits.Program.empty = { gateCount := 0, result := Cslib.Circuits.Program.empty, wireMap := id, trace_eq := ⋯, cost_eq := ⋯ }

theorem Complexity.SchnorrDeMorgan.xorBool_eq_parity (N : ℕ) (x : BitString N) : Schnorr.xorBool N x = Algebraic.GateElimination.Xor.parity x

Schnorr.xorBool agrees with the algebraic library's parity.

theorem Complexity.parity_size_ge_three_mul_internal (N G : ℕ) [NeZero N] (c : Circuit Basis.andOr2 N 1 G) (comp : Bool) (heval : ∀ (x : BitString N), c.eval x 0 = (comp ^^ Schnorr.xorBool N x)) : 3 * (N - 1) ≤ c.size

Internal proof of parity_size_ge_three_mul.