Experimental first-order Turing-machine routines — proof internals

This module proves that the structural Routine.TransducerSafe certificate is preserved by lowering through sequential composition and read-only-input loops.

theorem Complexity.TM.Experimental.Routine.TransducerSafe.lower_isTransducer_internal {n : ℕ} {routine : Routine n} (h : routine.TransducerSafe) : routine.lower.IsTransducer

Lowering a transducer-safe routine produces a concrete one-way-output transducer.