Direct charged resource combinators

Composition with a linear outer computation preserves independent time/workspace budgets: the inner machine's clock bounds the intermediate word for time, and its explicit output charge bounds that same word for workspace. Concatenation and framed pairing retain their output charge. All construction proofs use only plain certificates and machine-level combinators.

theorem Turing.MultiTapeTM.ComputableInO.length_le {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} (h : ComputableInO f encIn encMid T S) : ∃ (c : ℕ), ∀ (a : α), (encMid (f a)).length ≤ c * (S a + 1)

The encoded value is within the certificate's existing workspace charge.

theorem Turing.MultiTapeTM.ComputableInO.length_le_time {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {f : α → β} (h : ComputableInO f encIn encMid T S) : ∃ (c : ℕ), ∀ (a : α), (encMid (f a)).length ≤ c * (T a + 1)

The encoded value is within the time bound, since the machine writes it.

theorem Turing.MultiTapeTM.ComputableInO.of_linear {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLinearTimeAndSpace f encIn encMid) : ComputableInO f encIn encMid (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

A common linear certificate includes the output bound through its actual clock.

theorem Turing.MultiTapeTM.ComputableInO.comp_linear {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {T S : α → ℕ} {f : β → γ} {g : α → β} (hf : ComputableInO f encMid encOut (fun (b : β) => (encMid b).length) fun (b : β) => (encMid b).length) (hg : ComputableInO g encIn encMid T S) : ComputableInO (f ∘ g) encIn encOut T S

A linear outer computation preserves both independent bounds of the inner certificate.

theorem Turing.MultiTapeTM.ComputableInO.append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {enc₂ : δ ↪ List Bool} {f₁ : α → β} {f₂ : α → δ} {g : α → γ} {T₁ S₁ T₂ S₂ : α → ℕ} (h₁ : ComputableInO f₁ encIn encMid T₁ S₁) (h₂ : ComputableInO f₂ encIn enc₂ T₂ S₂) (hg : ∀ (a : α), encOut (g a) = encMid (f₁ a) ++ enc₂ (f₂ a)) : ComputableInO g encIn encOut (fun (a : α) => T₁ a + T₂ a) fun (a : α) => S₁ a + S₂ a

Concatenate two computed encodings, retaining the sum of both charged bounds.

theorem Turing.MultiTapeTM.ComputableInO.constZero {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableInO (fun (x : α) => b) encIn encMid (fun (a : α) => (encIn a).length) fun (x : α) => 0

A fixed output is charged within constant workspace, even when its input is unbounded.

theorem Turing.MultiTapeTM.ComputableInO.const {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableInO (fun (x : α) => b) encIn encMid (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

A fixed output fits the input-length charged workspace bound.

theorem Turing.MultiTapeTM.ComputableInO.prod {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁} {g : α → β₂} {T₁ S₁ T₂ S₂ : α → ℕ} (hf : ComputableInO f encIn enc₁ T₁ S₁) (hg : ComputableInO g encIn enc₂ T₂ S₂) : ComputableInO (fun (a : α) => (f a, g a)) encIn (encPair enc₁ enc₂) (fun (a : α) => T₁ a + T₂ a) fun (a : α) => S₁ a + S₂ a

Standard framed pairing, with the sum of the original time and charged workspace bounds.

theorem Turing.MultiTapeTM.ComputableInO.of_eq {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = encIn a) : ComputableInO f encIn encMid (fun (a : α) => (encIn a).length) fun (a : α) => (encIn a).length

Copy an encoded value without changing its independent representation.

theorem Turing.MultiTapeTM.ComputableInO.fst {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableInO Prod.fst (encPair enc₁ enc₂) enc₁ (fun (p : β₁ × β₂) => ((encPair enc₁ enc₂) p).length) fun (p : β₁ × β₂) => ((encPair enc₁ enc₂) p).length

The first component of a standard framed pair, with linear charged bounds.

theorem Turing.MultiTapeTM.ComputableInO.snd {β₁ β₂ : Type u} (enc₁ : β₁ ↪ List Bool) (enc₂ : β₂ ↪ List Bool) : ComputableInO Prod.snd (encPair enc₁ enc₂) enc₂ (fun (p : β₁ × β₂) => ((encPair enc₁ enc₂) p).length) fun (p : β₁ × β₂) => ((encPair enc₁ enc₂) p).length

The second component of a standard framed pair, with linear charged bounds.

theorem Turing.MultiTapeTM.ComputableInO.fst' {α : Type u_1} {encIn : α ↪ List Bool} {T S : α → ℕ} {β₁ β₂ : Type u} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (h : ComputableInO f encIn (encPair enc₁ enc₂) T S) : ComputableInO (fun (a : α) => (f a).1) encIn enc₁ T S

Project the first computed component without changing either independent budget.

theorem Turing.MultiTapeTM.ComputableInO.snd' {α : Type u_1} {encIn : α ↪ List Bool} {T S : α → ℕ} {β₁ β₂ : Type u} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {f : α → β₁ × β₂} (h : ComputableInO f encIn (encPair enc₁ enc₂) T S) : ComputableInO (fun (a : α) => (f a).2) encIn enc₂ T S

Project the second computed component without changing either independent budget.

theorem Turing.MultiTapeTM.ComputableInO.of_equiv {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {T S : α → ℕ} {δ : Type u_5} {f : α → β} (h : ComputableInO f encIn encMid T S) (e : δ ≃ α) : ComputableInO (f ∘ ⇑e) (encOfEquiv e encIn) encMid (T ∘ ⇑e) (S ∘ ⇑e)

Reinterpret an encoding along an equivalence, retaining the same machine and budgets.