Space-aware Hoare specifications — proof internals

This module supplies structural rules, sequential composition, and the bridge from fresh-start contracts to TM.ComputesInSpace.

theorem Complexity.Cfg.WithinAuxSpace.mono_internal {n : ℕ} {Q : Type} {c : Cfg n Q} {inputLength inputLength' space space' : ℕ} (h : c.WithinAuxSpace inputLength space) (hinput : inputLength ≤ inputLength') (hspace : space ≤ space') : c.WithinAuxSpace inputLength' space'

Internal monotonicity of the honest auxiliary-space predicate.

theorem Complexity.Cfg.WithinAuxSpace.transition_internal {n : ℕ} {Q : Type} {c : Cfg n Q} {inputLength space : ℕ} (h : c.WithinAuxSpace inputLength space) : { state := c.state, input := TM.transitionInput c.input, work := fun (i : Fin n) => TM.transitionTape (c.work i), output := TM.transitionTape c.output }.WithinAuxSpace inputLength (space + 1)

Internal phase-boundary bound: the standard input/work tape transition moves every head by at most one.

theorem Complexity.Cfg.WithinAuxSpace.reachesIn_internal {n : ℕ} {tm : TM n} {c c' : Cfg n tm.Q} {time inputLength space : ℕ} (h : c.WithinAuxSpace inputLength space) (hreach : tm.reachesIn time c c') : c'.WithinAuxSpace inputLength (space + time)

Internal reachability rule: after time concrete transitions, one extra auxiliary-space cell per transition covers every input and work head.

theorem Complexity.TM.HoareSpace.weaken_pre_internal {n : ℕ} {tm : TM n} {pre pre' : TapePred n} {inputLength space : ℕ} (h : tm.HoareSpace pre inputLength space) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) : tm.HoareSpace pre' inputLength space

Internal precondition weakening for all-reachable space contracts.

theorem Complexity.TM.HoareSpace.mono_internal {n : ℕ} {tm : TM n} {pre : TapePred n} {inputLength inputLength' space space' : ℕ} (h : tm.HoareSpace pre inputLength space) (hinput : inputLength ≤ inputLength') (hspace : space ≤ space') : tm.HoareSpace pre inputLength' space'

Internal numerical monotonicity for all-reachable space contracts.

theorem Complexity.TM.HoareTime.toHoareTimeSpace_internal {n : ℕ} {tm : TM n} {pre post : TapePred n} {time inputLength initialSpace : ℕ} (htime : tm.HoareTime pre post time) (hinitial : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → { state := tm.qstart, input := inp, work := work, output := out }.WithinAuxSpace inputLength initialSpace) : tm.HoareTimeSpace pre post time inputLength (initialSpace + time)

Internal time-to-space bridge. Determinism bounds every reachable prefix by the terminating run supplied by the Hoare triple, and tape heads grow by at most one cell per step.

theorem Complexity.TM.HoareTimeSpace.consequence_internal {n : ℕ} {tm : TM n} {pre pre' post post' : TapePred n} {time time' inputLength inputLength' space space' : ℕ} (h : tm.HoareTimeSpace pre post time inputLength space) (hpre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre' inp work out → pre inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), post inp work out → post' inp work out) (htime : time ≤ time') (hinput : inputLength ≤ inputLength') (hspace : space ≤ space') : tm.HoareTimeSpace pre' post' time' inputLength' space'

Internal consequence rule for time-and-space Hoare contracts.

theorem Complexity.TM.IsTransducer.seqTM_internal {n : ℕ} {tm₁ tm₂ : TM n} (h₁ : tm₁.IsTransducer) (h₂ : tm₂.IsTransducer) : (tm₁.seqTM tm₂).IsTransducer

Internal transducer closure under sequential composition.

theorem Complexity.TM.seqTM_hoareTimeSpace_internal {n : ℕ} (tm₁ tm₂ : TM n) {pre mid mid' post : TapePred n} {b₁ b₂ inputLength space₁ space₂ : ℕ} (h₁ : tm₁.HoareTimeSpace pre mid b₁ inputLength space₁) (htrans : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid inp work out → mid' (transitionInput inp) (fun (i : Fin n) => transitionTape (work i)) (transitionTape out)) (h₂ : tm₂.HoareTimeSpace mid' post b₂ inputLength space₂) : (tm₁.seqTM tm₂).HoareTimeSpace pre post (b₁ + 1 + b₂) inputLength (max space₁ space₂)

Internal sequential composition rule. Both phases use one shared logical input length and auxiliary-space budget; the phase boundary is covered by the second contract at its reflexive initial configuration.

theorem Complexity.TM.computesInSpace_of_hoareTimeSpace_internal {n : ℕ} {tm : TM n} {f : List Bool → List Bool} {T S : ℕ → ℕ} (htrans : tm.IsTransducer) (h : ∀ (x : List Bool), tm.HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init []) (fun (x_1 : Tape) (x_2 : Fin n → Tape) (out : Tape) => out.HasOutput (f x)) (T x.length) x.length (S x.length)) : tm.ComputesInSpace f S

Internal bridge from fresh-start time-and-space contracts to function computation in space.