Circuit input reindexing -- definitions

This layer transports a circuit along an arbitrary map from its original primary inputs into a new positive input tuple. Internal gates keep their order and every source internal wire retains its gate index.

def Complexity.Circuit.reindexInputWire {N N' G : ℕ} (mapInput : Fin N → Fin N') : Fin (N + G) → Fin (N' + G)

Map an input-or-gate wire into a new primary-input namespace while preserving the internal-gate index.

Equations

• Complexity.Circuit.reindexInputWire mapInput i = Fin.addCases (fun (input : Fin N) => Fin.castAdd G (mapInput input)) (fun (gate : Fin G) => Fin.natAdd N' gate) i

def Complexity.Circuit.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 B N' M G

Reindex a circuit's primary inputs without changing its gates, outputs, or resource counts.

Equations

• One or more equations did not get rendered due to their size.