Primitive raw-circuit fragment gates

This definitions layer provides the small proof-free gates shared by raw circuit fragment builders. A duplicated-input gate copies or negates an existing wire, while a wire paired with its negation supplies either Boolean constant.

def Complexity.CircuitCode.RawGate.copy (input : ℕ) (negated : Bool := false) : RawGate

Copy an existing wire, optionally negating it for free on both input edges.

Equations

• Complexity.CircuitCode.RawGate.copy input negated = { op := Complexity.AndOrOp.and, input₀ := input, input₁ := input, negated₀ := negated, negated₁ := negated }

def Complexity.CircuitCode.RawGate.constant (input : ℕ) : Bool → RawGate

Produce a Boolean constant from an existing wire and its negation.

Equations

• Complexity.CircuitCode.RawGate.constant input false = { op := Complexity.AndOrOp.and, input₀ := input, input₁ := input, negated₀ := false, negated₁ := true }
• Complexity.CircuitCode.RawGate.constant input true = { op := Complexity.AndOrOp.or, input₀ := input, input₁ := input, negated₀ := false, negated₁ := true }