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.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.