Circuit input reindexing

Reindexing transports a circuit along an arbitrary map from its original primary inputs into a new positive input tuple. It preserves the internal and output gates exactly, so size is unchanged and evaluation is precomposition with the supplied input map.

@[simp]

theorem Complexity.Circuit.reindexInputWire_input {N N' G : ℕ} (mapInput : Fin N → Fin N') (input : Fin N) : reindexInputWire mapInput (Fin.castAdd G input) = Fin.castAdd G (mapInput input)

Reindexing maps a primary-input wire through the supplied input map.

@[simp]

theorem Complexity.Circuit.reindexInputWire_gate {N N' G : ℕ} (mapInput : Fin N → Fin N') (gate : Fin G) : reindexInputWire mapInput (Fin.natAdd N gate) = Fin.natAdd N' gate

Reindexing preserves every internal-gate wire index.

theorem Complexity.Circuit.wireValue_reindexInputs {B : Basis} {N N' M G : ℕ} [NeZero N] [NeZero N'] [NeZero M] (circuit : Circuit B N M G) (mapInput : Fin N → Fin N') (input : BitString N') (wire : Fin (N + G)) : (circuit.reindexInputs mapInput).wireValue input (reindexInputWire mapInput wire) = circuit.wireValue (input ∘ mapInput) wire

Reindexing preserves the value of every source wire after input precomposition.

@[simp]

theorem Complexity.Circuit.eval_reindexInputs {B : Basis} {N N' M G : ℕ} [NeZero N] [NeZero N'] [NeZero M] (circuit : Circuit B N M G) (mapInput : Fin N → Fin N') (input : BitString N') : (circuit.reindexInputs mapInput).eval input = circuit.eval (input ∘ mapInput)

Reindexing circuit inputs is semantic precomposition.

@[simp]

theorem Complexity.Circuit.size_reindexInputs {B : Basis} {N N' M G : ℕ} [NeZero N] [NeZero N'] [NeZero M] (circuit : Circuit B N M G) (mapInput : Fin N → Fin N') : (circuit.reindexInputs mapInput).size = circuit.size

Reindexing primary inputs preserves exact circuit size.