Comparing standard and native De Morgan gate costs

Constants and identities are free in standardCost, while native complexity counts every internal gate. A contextual translation shares two constant gates across the whole circuit and removes identities. Its native size is exactly the original standard cost plus two.

def Algebraic.DeMorgan.withSharedConstants {n m : ℕ} (circuit : Circuit signature n m) : Circuit signature n m

Compile a circuit while sharing two constant gates and eliminating identity gates.

Equations

• Algebraic.DeMorgan.withSharedConstants circuit = Algebraic.DeMorgan.rawWithSharedConstants✝ circuit

theorem Algebraic.DeMorgan.withSharedConstants_eval {n m : ℕ} (circuit : Circuit signature n m) (input : Fin n → Bool) : (withSharedConstants circuit).eval interpretation input = circuit.eval interpretation input

Sharing constants preserves every designated output.

theorem Algebraic.DeMorgan.withSharedConstants_size {n m : ℕ} (circuit : Circuit signature n m) : (withSharedConstants circuit).size = circuit.cost standardCost + 2

The translated native size is precisely standard logical-gate cost plus two.

theorem Algebraic.DeMorgan.complexity_le_standardCost_add_two {n : ℕ} (circuit : Circuit signature n 1) {function : ScalarFunction Bool n} (computes : circuit.ComputesWith interpretation fun (input : Fin n → Bool) (x : Fin 1) => function input) : complexity function ≤ circuit.cost standardCost + 2

Any standard-cost circuit yields a native upper bound with only two extra gates.