Internal laws for appendable raw-circuit fragments

This module proves generic composition and prefix-preservation facts for the iterative raw-circuit evaluator. The statements are exposed by Complexitylib.Circuits.Encoding.Fragment.

theorem Complexity.CircuitCode.RawGate.eval_copy_internal (input : ℕ) (negated value : Bool) : (copy input negated).eval value value = (negated ^^ value)

Internal semantic equation for duplicated-input copy gates.

theorem Complexity.CircuitCode.RawGate.eval_constant_internal (input : ℕ) (constantValue wireValue : Bool) : (constant input constantValue).eval wireValue wireValue = constantValue

Internal semantic equation for dual-input constant gates.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_append_internal (first second : RawCircuit) (wires : Array Bool) : (first ++ second).evalAux? wires = (first.evalAux? wires).bind second.evalAux?

Internal append law for iterative raw evaluation.

theorem Complexity.CircuitCode.RawCircuit.eval?_append_copy_internal (circuit : RawCircuit) (input : List Bool) (negated : Bool) (hnonempty : circuit ≠ []) : (circuit ++ [RawGate.copy (input.length + List.length circuit - 1) negated]).eval? input = Option.map (fun (value : Bool) => negated ^^ value) (circuit.eval? input)

Appending a copy gate to a nonempty circuit maps its original output by the gate's optional negation.

theorem Complexity.CircuitCode.RawCircuit.encode_appendOutputMatch_internal (inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) : (appendOutputMatch inputWidth circuit expected).encode = NatCode.encode (List.length circuit + 1) ++ List.flatMap RawGate.encode circuit ++ (RawGate.copy (inputWidth + List.length circuit - 1) !expected).encode

Exact serialization of an output-match extension.

theorem Complexity.CircuitCode.RawCircuit.eval?_appendOutputMatch_eq_some_true_iff_internal (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) : (appendOutputMatch input.length circuit expected).eval? input = some true ↔ circuit.eval? input = some expected

An output-match extension returns true exactly when the original nonempty circuit returns the selected bit.

theorem Complexity.CircuitCode.RawCircuit.evalCode_appendOutputMatch_encode_iff_of_length_internal (inputWidth : ℕ) (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) (hwidth : input.length = inputWidth) : evalCode inputWidth (appendOutputMatch inputWidth circuit expected).encode input = some true ↔ circuit.eval? input = some expected

Exact decoding turns an output-match extension into a true-evaluation test at the declared input width.

theorem Complexity.CircuitCode.RawCircuit.encode_appendOutputMatchBit_internal (inputWidth : ℕ) (circuit : RawCircuit) (expected : Bool) : (appendOutputMatchBit inputWidth circuit expected).encode = NatCode.encode (List.length circuit + 2) ++ List.flatMap RawGate.encode circuit ++ (RawGate.copy (inputWidth + List.length circuit - 1) expected).encode ++ (RawGate.copy (inputWidth + List.length circuit) true).encode

Exact serialization of a two-gate live-bit output-match extension.

theorem Complexity.CircuitCode.RawCircuit.eval?_appendOutputMatchBit_eq_some_true_iff_internal (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) : (appendOutputMatchBit input.length circuit expected).eval? input = some true ↔ circuit.eval? input = some expected

The two-gate live-bit output-match extension returns true exactly when the original nonempty circuit returns the selected bit.

theorem Complexity.CircuitCode.RawCircuit.evalCode_appendOutputMatchBit_encode_iff_of_length_internal (inputWidth : ℕ) (circuit : RawCircuit) (input : List Bool) (expected : Bool) (hnonempty : circuit ≠ []) (hwidth : input.length = inputWidth) : evalCode inputWidth (appendOutputMatchBit inputWidth circuit expected).encode input = some true ↔ circuit.eval? input = some expected

Exact decoding turns a two-gate live-bit output-match extension into a true-evaluation test at the declared input width.

theorem Complexity.CircuitCode.RawCircuit.topologicallyWellFormed_append_internal (available : ℕ) (first second : RawCircuit) : TopologicallyWellFormed available (first ++ second) ↔ TopologicallyWellFormed available first ∧ TopologicallyWellFormed (available + List.length first) second

Internal topological decomposition for appended raw fragments.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_preserves_prefix_internal {circuit : RawCircuit} {wires result : Array Bool} (heval : circuit.evalAux? wires = some result) {i : ℕ} (hi : i < wires.size) : result[i]? = wires[i]?

Internal proof that raw evaluation only appends memo entries.