Linear-time canonical binary subtraction -- output discipline

The borrow scan, backward cleanup, and operand rewinds leave the public output tape one-way, so the core and complete machines are safe transducers.

theorem Complexity.TM.binaryRippleSubCoreTM_isTransducer_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : (binaryRippleSubCoreTM lhsIdx rhsIdx resultIdx).IsTransducer

The direct subtraction core never moves the public output head left.

theorem Complexity.TM.binaryRippleSubTM_isTransducer_internal {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : (binaryRippleSubTM lhsIdx rhsIdx resultIdx).IsTransducer

Backward canonicalization followed by both operand rewinds remains a transducer.