Fixed-width one-sample output matching -- proof internals

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationMatch.length_circuit_internal (inputWidth gateBound : ℕ) (expected : Bool) : List.length (circuit inputWidth gateBound expected) = List.length (EvaluationOutput.circuit inputWidth gateBound) + 1

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

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationMatch.eval?_circuit_eq_some_true_iff_internal {inputWidth gateBound : ℕ} {description : Description inputWidth gateBound} (hdescription : description.WellFormed) (input : BitString inputWidth) (expected : Bool) : (circuit inputWidth gateBound expected).eval? (EvaluationSequence.combinedInput description input).toList = some true ↔ description.toRawCircuit.eval? input.toList = some expected