Computation models

Aggregation module for the machine models: the core Turing-machine semantics, the single-tape simulation, machine combinators, Hoare-style specifications, reusable subroutines, determinism results, and the universal machine. 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.