Sequential fixed-width gate evaluation -- proof internals

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_stepCircuit_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) : List.length (stepCircuit inputWidth gateBound slot) = GateFormula.gateSize inputWidth gateBound slot

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_stepCircuitAt_internal (inputWidth gateBound index : ℕ) : List.length (stepCircuitAt inputWidth gateBound index) = EvaluationLayout.sizeAt inputWidth gateBound index

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_prefixCircuit_internal (inputWidth gateBound count : ℕ) : List.length (prefixCircuit inputWidth gateBound count) = EvaluationLayout.prefixSize inputWidth gateBound count

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.length_circuit_internal (inputWidth gateBound : ℕ) : List.length (circuit inputWidth gateBound) = EvaluationLayout.prefixSize inputWidth gateBound gateBound

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.topologicallyWellFormed_stepCircuit_internal {inputWidth gateBound : ℕ} (slot : Fin gateBound) : RawCircuit.TopologicallyWellFormed (EvaluationLayout.stepAvailable inputWidth gateBound slot) (stepCircuit inputWidth gateBound slot)

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.topologicallyWellFormed_prefixCircuit_internal (inputWidth gateBound count : ℕ) (hcount : count ≤ gateBound) : RawCircuit.TopologicallyWellFormed (EvaluationLayout.baseWireCount inputWidth gateBound) (prefixCircuit inputWidth gateBound count)

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationSequence.topologicallyWellFormed_circuit_internal (inputWidth gateBound : ℕ) : RawCircuit.TopologicallyWellFormed (EvaluationLayout.baseWireCount inputWidth gateBound) (circuit inputWidth gateBound)