Relocating raw circuit fragments

Uniformly shifting a raw fragment preserves its gate count and local topology. Evaluation after a memo prefix is exactly the prefix followed by the original local evaluation result.

@[simp]

theorem Complexity.CircuitCode.RawGate.eval_shift (offset : ℕ) (gate : RawGate) (value₀ value₁ : Bool) : (shift offset gate).eval value₀ value₁ = gate.eval value₀ value₁

Wire relocation does not change a gate's Boolean operation.

theorem Complexity.CircuitCode.RawGate.wellFormedAt_shift_iff (offset available : ℕ) (gate : RawGate) : (shift offset gate).WellFormedAt (offset + available) ↔ gate.WellFormedAt available

A shifted gate is valid at the shifted boundary exactly when the original gate is valid at its local boundary.

@[simp]

theorem Complexity.CircuitCode.RawCircuit.length_shift (offset : ℕ) (circuit : RawCircuit) : List.length (shift offset circuit) = List.length circuit

Wire relocation preserves the exact gate count.

theorem Complexity.CircuitCode.RawCircuit.topologicallyWellFormed_shift_iff (offset available : ℕ) (circuit : RawCircuit) : TopologicallyWellFormed (offset + available) (shift offset circuit) ↔ TopologicallyWellFormed available circuit

Uniform relocation preserves and reflects local topological validity.

theorem Complexity.CircuitCode.RawCircuit.evalAux?_shift (offset : ℕ) (circuit : RawCircuit) (leading wires : Array Bool) (hleading : leading.size = offset) : (shift offset circuit).evalAux? (leading ++ wires) = Option.map (fun (result : Array Bool) => leading ++ result) (circuit.evalAux? wires)

Evaluating a relocated fragment after a prefix preserves that prefix and reproduces the original local result behind it.