End-to-end serialized circuit evaluator

This file composes the outer-pair validator and staging machine with the streaming evaluator core. It proves the raw-tape Hoare contract, packages the machine as a decider for circuitEvalLanguage, and records the concrete quadratic running-time bound.

theorem Complexity.CircuitCode.Machine.Internal.evalFamilyTM_hoareTime_internal (bits : List Bool) : evalFamilyTM.HoareTime (PairStagePre bits) (EvalFamilyPost bits) (evalFamilyTime bits.length)

Internal proof of the total end-to-end evaluator contract.

theorem Complexity.CircuitCode.Machine.Internal.evalFamilyTM_decidesInTime_internal : evalFamilyTM.DecidesInTime circuitEvalLanguage evalFamilyTime

Internal proof that the serialized evaluator decides its target language within the concrete end-to-end time budget.

theorem Complexity.CircuitCode.Machine.Internal.evalFamilyTime_bigO_quadratic_internal : BigO evalFamilyTime fun (x : ℕ) => x ^ 2

The concrete end-to-end evaluator budget is quadratic.