Complete finite-alphabet computations on binary inputs

Parsing, source simulation, and encoded emission preserve complete words with linear endpoint overhead. Invalid inputs halt before source execution. Source bounds need only hold when the corresponding binary input satisfies the chosen validity predicate.

theorem Complexity.MathlibTM0.AlphabetMachine.computes_proof {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {input : List Input} {output : List Output} {time : ℕ} (h : M.OutputsWithin input output time) : (M.machine ci co).ComputesInTimeAndSpace (ci.encode input) (co.encode output) (2 * (ci.encode input).length + time + (co.size + 1) * output.length + 4) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg (ci.encode input)) (2 * (ci.encode input).length + time + (co.size + 1) * output.length + 4))

theorem Complexity.MathlibTM0.AlphabetMachine.computes_with_bounds {Input Output : Type} (M : AlphabetMachine Input Output) (ci : FiniteAlphabetCode Input) (co : FiniteAlphabetCode Output) {f : List Input → List Output} {p q : Polynomial ℕ} {P : List Bool → Prop} (h : ∀ (xs : List Input), P (ci.encode xs) → M.OutputsWithin xs (f xs) (Polynomial.eval xs.length p)) (hlen : ∀ (xs : List Input), P (ci.encode xs) → (f xs).length ≤ Polynomial.eval xs.length q) (w : List Bool) (hw : P w) : (M.machine ci co).ComputesInTimeAndSpace w (ci.map co f w) (2 * w.length + Polynomial.eval w.length p + (co.size + 1) * Polynomial.eval w.length q + 4) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg w) (2 * w.length + Polynomial.eval w.length p + (co.size + 1) * Polynomial.eval w.length q + 4))