Normalized machine witnesses for charged space bounds

Native multi-pass simulations need machines with aligned tape origins. Normalize a plain charged space certificate at that boundary, retaining its encoding and output charge. Time remains existential; the space window changes by a uniform constant factor.

theorem Turing.MultiTapeTM.Internal.NormalForm.space {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} {S : α → ℕ} (h : ComputableInSpace f encIn encOut S) : ∃ (T : α → ℕ) (c : ℕ), (∃ (k : ℕ) (State : Type) (_ : Finite State) (tm : MultiTapeTM k Bool State), ∀ (a : α), tm.ComputesTidilyInTimeAndSpace (encIn a) (encOut (f a)) (c * (T a + 1)) (c * (S a + 1))) ∧ ∀ (a : α), (encOut (f a)).length ≤ c * (S a + 1)

A normalized realizing machine for a plain charged-space certificate.