Direct charged bounds for binary-word normalization

Reverse the raw little-endian word, drop its leading false symbols with the existing transducer, and reverse back. Both component machines have linear clocks and zero work tapes; composition retains linear time and linear workspace, including the encoded output charge. No qualitative polynomial-time certificate supplies the quantitative bound.

Main results

• Turing.MultiTapeTM.ComputableInO.bitsToNat: linear-time, charged linear-space binary decoding.

theorem Turing.MultiTapeTM.ComputableInO.bitsToNat : ComputableInO ofBits encBits encNat List.length List.length

Read arbitrary little-endian words in linear time and charged linear workspace, including empty words and noncanonical trailing false symbols.