One-step TM-to-RAM simulation -- proof internals

This aggregation module contains the checked layout, head-symbol loading, selected transition-action, nested finite-dispatch, and source-resource layers. The public surface transfers the resulting measured execution to compiled RAM.