Dual-rail normalization for AC0 circuits

This module implements the local compiler underlying input-negation normal form. Every Boolean value is represented by two wires carrying the value and its complement. A source NOT swaps the two rails without adding a gate. A source AND or OR produces both its ordinary output and its De Morgan dual, using exactly two target gates.

The construction is semantic rather than syntactic: the same block translation simulates both Boolean evaluation and the logical-depth interpretation. Thus compilation preserves logical depth exactly and doubles the charged AND/OR cost, including at fan-in zero.

def Algebraic.AC0.DualRail.encode (value : Bool) : Fin 2 → Bool

Encode a Boolean together with its complement.

Equations

• Algebraic.AC0.DualRail.encode value = ![value, !value]

def Algebraic.AC0.DualRail.duplicateDepth (depth : ℕ) : Fin 2 → ℕ

Duplicate a logical depth across both rails.

Equations

• Algebraic.AC0.DualRail.duplicateDepth depth = ![depth, depth]

def Algebraic.AC0.DualRail.notCircuit : Circuit signature (1 * 2) 2

A NOT gate swaps the two rails without adding a gate.

Equations

• Algebraic.AC0.DualRail.notCircuit = { size := 0, program := Cslib.Circuits.Program.empty, outputs := ![Algebraic.Block.inputWire 0 1, Algebraic.Block.inputWire 0 0] }

@[simp]

theorem Algebraic.AC0.DualRail.notCircuit_size : notCircuit.size = 0

The dual-rail NOT only swaps the rails: it has no gates.

def Algebraic.AC0.DualRail.andPositiveLine (inputCount : ℕ) : Line signature (inputCount * 2) 0

The positive AND output of a dual-rail AND gadget.

Equations

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

def Algebraic.AC0.DualRail.andNegativeLine (inputCount : ℕ) : Line signature (inputCount * 2) 1

The complemented output of a dual-rail AND gadget, computed by OR.

Equations

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

@[simp]

theorem Algebraic.AC0.DualRail.andPositiveLine_eval {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) (gates : Fin 0 → U) : (andPositiveLine inputCount).eval target input gates = target (Op.and inputCount) fun (argument : Fin (signature.Arity (Op.and inputCount))) => input (finProdFinEquiv (argument, 0))

@[simp]

theorem Algebraic.AC0.DualRail.andNegativeLine_eval {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) (gates : Fin 1 → U) : (andNegativeLine inputCount).eval target input gates = target (Op.or inputCount) fun (argument : Fin (signature.Arity (Op.or inputCount))) => input (finProdFinEquiv (argument, 1))

def Algebraic.AC0.DualRail.andCircuit (inputCount : ℕ) : Circuit signature (inputCount * 2) 2

The two-output gadget implementing AND and its complement.

Equations

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

@[simp]

theorem Algebraic.AC0.DualRail.andCircuit_size (inputCount : ℕ) : (andCircuit inputCount).size = 2

The dual-rail AND gadget has exactly two gates: an AND for the positive rail and an OR for its complement.

def Algebraic.AC0.DualRail.orPositiveLine (inputCount : ℕ) : Line signature (inputCount * 2) 0

The positive OR output of a dual-rail OR gadget.

Equations

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

def Algebraic.AC0.DualRail.orNegativeLine (inputCount : ℕ) : Line signature (inputCount * 2) 1

The complemented output of a dual-rail OR gadget, computed by AND.

Equations

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

@[simp]

theorem Algebraic.AC0.DualRail.orPositiveLine_eval {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) (gates : Fin 0 → U) : (orPositiveLine inputCount).eval target input gates = target (Op.or inputCount) fun (argument : Fin (signature.Arity (Op.or inputCount))) => input (finProdFinEquiv (argument, 0))

@[simp]

theorem Algebraic.AC0.DualRail.orNegativeLine_eval {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) (gates : Fin 1 → U) : (orNegativeLine inputCount).eval target input gates = target (Op.and inputCount) fun (argument : Fin (signature.Arity (Op.and inputCount))) => input (finProdFinEquiv (argument, 1))

def Algebraic.AC0.DualRail.orCircuit (inputCount : ℕ) : Circuit signature (inputCount * 2) 2

The two-output gadget implementing OR and its complement.

Equations

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

@[simp]

theorem Algebraic.AC0.DualRail.orCircuit_size (inputCount : ℕ) : (orCircuit inputCount).size = 2

The dual-rail OR gadget has exactly two gates: an OR for the positive rail and an AND for its complement.

def Algebraic.AC0.DualRail.gateCount : Op → ℕ

Number of gates in a dual-rail operation gadget.

Equations

• Algebraic.AC0.DualRail.gateCount Algebraic.AC0.Op.not = 0
• Algebraic.AC0.DualRail.gateCount (Algebraic.AC0.Op.and arity) = 2
• Algebraic.AC0.DualRail.gateCount (Algebraic.AC0.Op.or arity) = 2

def Algebraic.AC0.DualRail.translation : BlockTranslation signature signature 2

Dual-rail compilation of arbitrary AC0 gates.

Equations

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

@[simp]

theorem Algebraic.AC0.DualRail.translation_gateCount (op : Op) : translation.gateCount op = gateCount op

Each dual-rail gadget has gateCount gates.

@[simp]

theorem Algebraic.AC0.DualRail.notCircuit_eval_zero {U : Type u_1} (target : Interpretation signature U) (input : Fin (1 * 2) → U) : notCircuit.eval target input 0 = input 1

@[simp]

theorem Algebraic.AC0.DualRail.notCircuit_eval_one {U : Type u_1} (target : Interpretation signature U) (input : Fin (1 * 2) → U) : notCircuit.eval target input 1 = input 0

@[simp]

theorem Algebraic.AC0.DualRail.andCircuit_eval_zero {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) : (andCircuit inputCount).eval target input 0 = target (Op.and inputCount) fun (argument : Fin (signature.Arity (Op.and inputCount))) => input (finProdFinEquiv (argument, 0))

@[simp]

theorem Algebraic.AC0.DualRail.andCircuit_eval_one {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) : (andCircuit inputCount).eval target input 1 = target (Op.or inputCount) fun (argument : Fin (signature.Arity (Op.or inputCount))) => input (finProdFinEquiv (argument, 1))

@[simp]

theorem Algebraic.AC0.DualRail.orCircuit_eval_zero {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) : (orCircuit inputCount).eval target input 0 = target (Op.or inputCount) fun (argument : Fin (signature.Arity (Op.or inputCount))) => input (finProdFinEquiv (argument, 0))

@[simp]

theorem Algebraic.AC0.DualRail.orCircuit_eval_one {U : Type u_1} (inputCount : ℕ) (target : Interpretation signature U) (input : Fin (inputCount * 2) → U) : (orCircuit inputCount).eval target input 1 = target (Op.and inputCount) fun (argument : Fin (signature.Arity (Op.and inputCount))) => input (finProdFinEquiv (argument, 1))

@[simp]

theorem Algebraic.AC0.DualRail.encode_zero (value : Bool) : encode value 0 = value

@[simp]

theorem Algebraic.AC0.DualRail.encode_one (value : Bool) : encode value 1 = !value

@[simp]

theorem Algebraic.AC0.DualRail.duplicateDepth_apply (depth : ℕ) (rail : Fin 2) : duplicateDepth depth rail = depth

theorem Algebraic.AC0.DualRail.operation_encode (op : Op) (input : Fin (arity op) → Bool) : encode (interpretation op input) = (translation.operation op).eval interpretation (Block.flatten (encode ∘ input))

def Algebraic.AC0.DualRail.booleanSimulation : BlockSimulation translation interpretation interpretation

Boolean dual-rail simulation.

Equations

• Algebraic.AC0.DualRail.booleanSimulation = Algebraic.BlockSimulation.ofPreserves Algebraic.AC0.DualRail.encode Algebraic.AC0.DualRail.operation_encode

theorem Algebraic.AC0.DualRail.operation_duplicateDepth (op : Op) (input : Fin (arity op) → ℕ) : duplicateDepth (logicalDepthInterpretation op input) = (translation.operation op).eval logicalDepthInterpretation (Block.flatten (duplicateDepth ∘ input))

def Algebraic.AC0.DualRail.depthSimulation : BlockSimulation translation logicalDepthInterpretation logicalDepthInterpretation

Logical-depth dual-rail simulation.

Equations

• Algebraic.AC0.DualRail.depthSimulation = Algebraic.BlockSimulation.ofPreserves Algebraic.AC0.DualRail.duplicateDepth Algebraic.AC0.DualRail.operation_duplicateDepth

theorem Algebraic.AC0.DualRail.pullCost_andOrCost (op : Op) : translation.pullCost andOrCost op = 2 * andOrCost op

Whole-circuit normalization

def Algebraic.AC0.DualRail.inputNegationProgram (n g : ℕ) : g ≤ n → Program signature n g

The first g input-negation gates over an n-input namespace.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.AC0.DualRail.inputNegationProgram n 0 x_2 = Cslib.Circuits.Program.empty

def Algebraic.AC0.DualRail.inputEncoder (n : ℕ) : Circuit signature n (n * 2)

Generate the positive and negative literal rails for every input. The encoder has one NOT gate per input, and each such gate reads that input directly.

Equations

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

@[simp]

theorem Algebraic.AC0.DualRail.inputEncoder_eval {n : ℕ} (input : Fin n → Bool) : (inputEncoder n).eval interpretation input = Block.flatten (encode ∘ input)

The input encoder computes each input together with its complement.

@[simp]

theorem Algebraic.AC0.DualRail.inputEncoder_depth_eval {n : ℕ} (input : Fin n → ℕ) : (inputEncoder n).eval logicalDepthInterpretation input = Block.flatten (duplicateDepth ∘ input)

Input encoding adds no logical depth: both rails inherit their input's arrival time.

@[simp]

theorem Algebraic.AC0.DualRail.inputEncoder_andOrCost (n : ℕ) : (inputEncoder n).cost andOrCost = 0

Input encoding has zero charged AND/OR cost.

theorem Algebraic.AC0.DualRail.inputEncoder_negationsAtInputs (n : ℕ) : Program.NegationsAtInputs (inputEncoder n).program

Every NOT in the input encoder reads an original input.

def Algebraic.AC0.DualRail.positiveOutputs {n m : ℕ} (circuit : Circuit signature n (m * 2)) : Circuit signature n m

Project the positive rail of every compiled output.

Equations

• Algebraic.AC0.DualRail.positiveOutputs circuit = circuit.mapOutputs fun (output : Fin m) => finProdFinEquiv (output, 0)

@[simp]

theorem Algebraic.AC0.DualRail.positiveOutputs_size {n m : ℕ} (circuit : Circuit signature n (m * 2)) : (positiveOutputs circuit).size = circuit.size

Keeping only the positive rails adds no gates.

def Algebraic.AC0.DualRail.normalize {n m : ℕ} (circuit : Circuit signature n m) : Circuit signature n m

Eliminate every internal negation by dual-rail compilation. The resulting circuit contains n input-literal NOT gates followed by a negation-free compiled program.

Equations

• Algebraic.AC0.DualRail.normalize circuit = (Algebraic.AC0.DualRail.positiveOutputs (Algebraic.AC0.DualRail.translation.compile circuit)).comp (Algebraic.AC0.DualRail.inputEncoder n)

theorem Algebraic.AC0.DualRail.normalize_negationsAtInputs {n m : ℕ} (circuit : Circuit signature n m) : Program.NegationsAtInputs (normalize circuit).program

The normalized circuit satisfies the checked input-negation invariant.

@[simp]

theorem Algebraic.AC0.DualRail.normalize_eval {n m : ℕ} (circuit : Circuit signature n m) (input : Fin n → Bool) : (normalize circuit).eval interpretation input = circuit.eval interpretation input

Normalization preserves the full output vector on every Boolean input.

@[simp]

theorem Algebraic.AC0.DualRail.normalize_logicalOutputDepths {n m : ℕ} (circuit : Circuit signature n m) : Circuit.logicalOutputDepths (normalize circuit) = Circuit.logicalOutputDepths circuit

Normalization preserves the logical depth of every designated output.

@[simp]

theorem Algebraic.AC0.DualRail.normalize_logicalDepth {n m : ℕ} (circuit : Circuit signature n m) : Circuit.logicalDepth (normalize circuit) = Circuit.logicalDepth circuit

Normalization preserves maximum logical depth exactly.

@[simp]

theorem Algebraic.AC0.DualRail.compile_andOrCost {n m : ℕ} (circuit : Circuit signature n m) : (translation.compile circuit).cost andOrCost = 2 * circuit.cost andOrCost

The compiled dual-rail DAG has exactly twice the source AND/OR cost.

@[simp]

theorem Algebraic.AC0.DualRail.normalize_andOrCost {n m : ℕ} (circuit : Circuit signature n m) : (normalize circuit).cost andOrCost = 2 * circuit.cost andOrCost

Whole-circuit normalization has exactly twice the source AND/OR cost.

@[simp]

theorem Algebraic.AC0.DualRail.normalize_size {n m : ℕ} (circuit : Circuit signature n m) : (normalize circuit).size = n + 2 * circuit.cost andOrCost

Normalization uses one input-literal gate per input and two gates per charged source gate.

Family-level normalization

def Algebraic.AC0.DualRail.normalizeFamily {m : ℕ} (family : Circuit.Family signature m) : Circuit.Family signature m

Normalize every member of a circuit family.

Equations

• Algebraic.AC0.DualRail.normalizeFamily family = { circuit := fun (n : ℕ) => Algebraic.AC0.DualRail.normalize (family.circuit n) }

@[simp]

theorem Algebraic.AC0.DualRail.normalizeFamily_circuit {m : ℕ} (family : Circuit.Family signature m) (n : ℕ) : (normalizeFamily family).circuit n = normalize (family.circuit n)

The member at width n is the normalization of the source member.

@[simp]

theorem Algebraic.AC0.DualRail.normalizeFamily_cost {m : ℕ} (family : Circuit.Family signature m) (n : ℕ) : (normalizeFamily family).cost andOrCost n = 2 * family.cost andOrCost n

Family normalization doubles charged cost pointwise.

@[simp]

theorem Algebraic.AC0.DualRail.normalizeFamily_gateCount {m : ℕ} (family : Circuit.Family signature m) (n : ℕ) : (normalizeFamily family).gateCount n = n + 2 * family.cost andOrCost n

Family normalization has one input-literal gate per input and two gates per charged source gate.

@[simp]

theorem Algebraic.AC0.DualRail.normalizeFamily_logicalDepth {m : ℕ} (family : Circuit.Family signature m) (n : ℕ) : Family.logicalDepth (normalizeFamily family) n = Family.logicalDepth family n

Family normalization preserves logical depth pointwise.

theorem Algebraic.AC0.DualRail.normalizeFamily_computes {m : ℕ} (family : Circuit.Family signature m) (target : Target.Family Bool m) (computes : family.Computes interpretation target) : (normalizeFamily family).Computes interpretation target

Family normalization preserves the computed target.

theorem Algebraic.AC0.DualRail.normalizeFamily_negationsAtInputs {m : ℕ} (family : Circuit.Family signature m) : Family.NegationsAtInputs (normalizeFamily family)

Every normalized family member has only input-level negations.

theorem Algebraic.AC0.DualRail.normalizeFamily_hasPolynomialCost {m : ℕ} (family : Circuit.Family signature m) (bounded : family.HasPolynomialCost andOrCost) : (normalizeFamily family).HasPolynomialCost andOrCost

Polynomial AND/OR cost is preserved by family normalization.

theorem Algebraic.AC0.DualRail.normalizeFamily_hasPolynomialSize {m : ℕ} (family : Circuit.Family signature m) (bounded : family.HasPolynomialCost andOrCost) : (normalizeFamily family).HasPolynomialSize

Normalization turns polynomial charged cost into polynomial total gate count, with the explicit bound (2 * coefficient + 1) * (n + 1) ^ (degree + 1).

theorem Algebraic.AC0.DualRail.normalizeFamily_hasConstantLogicalDepth {m : ℕ} (family : Circuit.Family signature m) (bounded : Family.HasConstantLogicalDepth family) : Family.HasConstantLogicalDepth (normalizeFamily family)

Constant logical depth is preserved by family normalization.

theorem Algebraic.AC0.DualRail.normalizeFamily_isSmallDepth (family : Circuit.Family signature 1) (smallDepth : Family.IsRawSmallDepth family) : Family.IsSmallDepth (normalizeFamily family)

Every raw small-depth family has an equivalent checked family.

theorem Algebraic.AC0.rawComputable_iff_computable (target : Target.Family Bool 1) : RawComputable target ↔ Computable target

Raw and input-negation-normalized presentations define the same nonuniform AC0 class.