Fixed-width one-sample output matching

The fixed-label extension is one gate larger than the complete evaluator, remains topologically valid, and accepts exactly when the represented raw circuit returns the selected label on the supplied sample input.

@[simp]

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

One fixed-label check adds exactly one final gate.

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

The fixed-label evaluator is topologically valid from the encoded description and sample input block.

theorem Complexity.CircuitCode.FixedWidth.Description.EvaluationMatch.eval?_circuit_eq_some_true_iff {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

A valid fixed-width description passes the fixed-label check exactly when its ordinary raw circuit returns that label on the sample.