Native De Morgan complexity under circuit operations

Expressions, input rewiring, and Boolean combinations give direct upper bounds on minimum circuit size. The source circuits retain their internal sharing; constants, negations, and all other internal gates count toward native size.

theorem Algebraic.DeMorgan.complexity_expression_le {n : ℕ} (expression : Expression n) : (complexity fun (input : Fin n → Bool) => Expression.eval input expression) ≤ expression.gateCount

A compiled expression upper-bounds the complexity of its semantics.

theorem Algebraic.DeMorgan.complexity_and_le {n : ℕ} (left right : ScalarFunction Bool n) : (complexity fun (input : Fin n → Bool) => left input && right input) ≤ complexity left + complexity right + 1

Conjunction uses each source circuit once and adds one gate.

theorem Algebraic.DeMorgan.complexity_or_le {n : ℕ} (left right : ScalarFunction Bool n) : (complexity fun (input : Fin n → Bool) => left input || right input) ≤ complexity left + complexity right + 1

Disjunction uses each source circuit once and adds one gate.

theorem Algebraic.DeMorgan.complexity_not_le {n : ℕ} (function : ScalarFunction Bool n) : (complexity fun (input : Fin n → Bool) => !function input) ≤ complexity function + 1

Negating the output of a shared circuit adds exactly one gate.

theorem Algebraic.DeMorgan.complexity_mapInputs_le {n m : ℕ} (function : ScalarFunction Bool n) (map : Fin n → Fin m) : (complexity fun (input : Fin m → Bool) => function (input ∘ map)) ≤ complexity function

Rewiring input coordinates cannot increase native gate complexity.

@[simp]

theorem Algebraic.DeMorgan.complexity_input {n : ℕ} (index : Fin n) : (complexity fun (input : Fin n → Bool) => input index) = 0

A designated input is a free output, requiring no gates.

theorem Algebraic.DeMorgan.complexity_xor_le {n : ℕ} (left right : ScalarFunction Bool n) : (complexity fun (input : Fin n → Bool) => left input ^^ right input) ≤ complexity left + complexity right + 4

XOR combines two shared circuits with four additional native gates.