Computation models

Aggregation module for the machine models: the core Turing-machine semantics, the single-tape simulation, machine combinators, time- and space-aware Hoare specifications, direct work-symbol branching, experimental first-order routine lowering and proof-carrying binary stream routines, reusable read-only-input and binary-work-tape loops, binary count-up loops, binary successor, binary predecessor and length, value-iterating and width-linear canonical binary addition, fixed-constant addition, copying, multiply-add, and fixed-polynomial evaluation, framed work-tape clearing, unary length, and pair-emission subroutines, computed-value/input fanout, finite space-to-time bounds, determinism results, the universal machine, and the logarithmic-cost random access machine (Complexitylib.Models.RandomAccessMachine), including its verified structured imperative frontend and Hamming-weight benchmark with exact steps and explicit quasilinear logarithmic-time and peak-space bounds, plus a generic verified typed finite-state scanner compiler with pair-validation, last-bit, and exact-3-CNF syntax instances. Proof-internal modules (…/Internal/…, register machinery, emitter plumbing) are deliberately not imported here — they stay in the build through the surface modules and theorem files that need them.