Padded fixed-width raw-circuit semantics -- proof internals

theorem Complexity.CircuitCode.FixedWidth.Description.slot_wellFormedAt_of_wellFormed_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (slot : Fin gateBound) : (description.slots slot).WellFormedAt (inputWidth + ↑slot)

theorem Complexity.CircuitCode.FixedWidth.Description.length_toPaddedRawCircuit_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : List.length description.toPaddedRawCircuit = gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.take_toPaddedRawCircuit_gateCount_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) : List.take description.gateCountNat description.toPaddedRawCircuit = description.toRawCircuit

theorem Complexity.CircuitCode.FixedWidth.Description.get_toPaddedRawCircuit_internal {inputWidth gateBound : ℕ} (description : Description inputWidth gateBound) (slot : Fin (List.length description.toPaddedRawCircuit)) : List.get description.toPaddedRawCircuit slot = (description.slots ⟨↑slot, ⋯⟩).toRawGate

theorem Complexity.CircuitCode.FixedWidth.Description.topologicallyWellFormed_toPaddedRawCircuit_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) : RawCircuit.TopologicallyWellFormed inputWidth description.toPaddedRawCircuit