Direct plain folds with reachable-prefix bounds

Derived from the machine-level plain fold of the credited #869 supplier. The accumulator is bounded only on reachable prefixes; no bound on arbitrary unreachable states is assumed. The rules use the canonical direct core and its independent polynomial-growth algebra.

theorem Turing.MultiTapeTM.ComputableInPolyTime.polyBounded {α : Type u_1} {input : α ↪ List Bool} {f : α → ℕ} (hf : ComputableInPolyTime f input encUnary) : PolyBounded (fun (x : α) => (input x).length) f

A unary-output certificate bounds the actual numeric value by a polynomial in input size.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldl' {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [hS : SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB) {B : γ → ℕ} (hB : PolyBounded (fun (x : γ) => (encIn x).length) B) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl step (init x) (List.take i (list x)))).length ≤ B x) : ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

A polynomial bound on the encoded accumulators of reachable prefixes suffices for a uniform polynomial-time fold. The list and callback encodings are preserved.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldlWith {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} (hpar : ComputableInPolyTime par encIn encP) (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB) {B : γ → ℕ} (hB : PolyBounded (fun (x : γ) => (encIn x).length) B) (hstates : ∀ (x : γ), ∀ i ≤ (list x).length, (encB (List.foldl (step (par x)) (init x) (List.take i (list x)))).length ≤ B x) : ComputableInPolyTime (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB

A captured parameter is computed uniformly, retained through every step, and bounded separately from the accumulator. Only reachable prefix states need the supplied bound.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterateWith {α β π : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {encPar : π ↪ List Bool} {par : α → π} {count : α → ℕ} {init : α → β} {step : π → β → β} (hpar : ComputableInPolyTime par encIn encPar) (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime (fun (p : π × β) => step p.1 p.2) (encPair encPar encState) encState) {bound : α → ℕ} (hbound : PolyBounded (fun (x : α) => (encIn x).length) bound) (hstates : ∀ (x : α), ∀ i ≤ count x, (encState ((step (par x))^[i] (init x))).length ≤ bound x) : ComputableInPolyTime (fun (x : α) => (step (par x))^[count x] (init x)) encIn encState

A computed captured parameter and a unary loop count give a uniform loop when every reachable iterate has polynomially bounded encoded size.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterate {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime step encState encState) {bound : α → ℕ} (hbound : PolyBounded (fun (x : α) => (encIn x).length) bound) (hstates : ∀ (x : α), ∀ i ≤ count x, (encState (step^[i] (init x))).length ≤ bound x) : ComputableInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState

A unary count and a bound only on the reachable states suffice for polynomial-time iteration, with the original state encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldlWith_spec {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} (hpar : ComputableInPolyTime par encIn encP) (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB) (invariant : γ → List α → β → Prop) (hbase : ∀ (x : γ), invariant x [] (init x)) (hpreserve : ∀ (x : γ) (consumed : List α) (state : β) (value : α), consumed ++ [value] <+: list x → invariant x consumed state → invariant x (consumed ++ [value]) (step (par x) state value)) {size : γ → ℕ} (hsize : PolyBounded (fun (x : γ) => (encIn x).length) size) (hbound : ∀ (x : γ) (consumed : List α) (state : β), consumed <+: list x → invariant x consumed state → (encB state).length ≤ size x) : ComputableInPolyTime (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB ∧ ∀ (x : γ), invariant x (list x) (List.foldl (step (par x)) (init x) (list x))

A prefix invariant supplies both the accumulator bound and the final postcondition for a fold with a captured parameter. The size bound may depend on the original input and need not be computable. The step certificate is uniform jointly in the parameter, accumulator and element.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldl_spec {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB) (invariant : γ → List α → β → Prop) (hbase : ∀ (x : γ), invariant x [] (init x)) (hpreserve : ∀ (x : γ) (consumed : List α) (state : β) (value : α), consumed ++ [value] <+: list x → invariant x consumed state → invariant x (consumed ++ [value]) (step state value)) {size : γ → ℕ} (hsize : PolyBounded (fun (x : γ) => (encIn x).length) size) (hbound : ∀ (x : γ) (consumed : List α) (state : β), consumed <+: list x → invariant x consumed state → (encB state).length ≤ size x) : ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB ∧ ∀ (x : γ), invariant x (list x) (List.foldl step (init x) (list x))

A prefix invariant supplies both the accumulator bound and the final postcondition. The size bound may depend on the original input and need not be computable. The list and step must have uniform polynomial-time certificates.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldlWith_of_bounded_growth {γ α β π : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {encP : π ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {par : γ → π} {list : γ → List α} {init : γ → β} {step : π → β → α → β} (hpar : ComputableInPolyTime par encIn encP) (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : (π × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encP encB) encA) encB) {growth : γ → ℕ} (hpoly : PolyBounded (fun (x : γ) => (encIn x).length) growth) (hgrowth : ∀ (x : γ) (state : β), ∀ value ∈ list x, (encB (step (par x) state value)).length ≤ (encB state).length + growth x) : ComputableInPolyTime (fun (x : γ) => List.foldl (step (par x)) (init x) (list x)) encIn encB

A captured fold may add a polynomial amount of storage per element, measured against the original input. The growth bound covers every accumulator and each element in the runtime list; the joint step certificate still covers all parameters, accumulators and elements.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldlWithInput_of_bounded_growth {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} {list : γ → List α} {init : γ → β} {step : γ → β → α → β} (hinit : ComputableInPolyTime init encIn encB) (hcompute : ComputableInPolyTime list encIn encL ∧ ComputableInPolyTime (fun (p : (γ × β) × α) => step p.1.1 p.1.2 p.2) (encPair (encPair encIn encB) encA) encB ∧ ListEncoding encA encL ∧ SizedListEncoding encA encL) {growth : γ → ℕ} (hbound : PolyBounded (fun (x : γ) => (encIn x).length) growth ∧ ∀ (x : γ) (state : β), ∀ value ∈ list x, (encB (step x state value)).length ≤ (encB state).length + growth x) : ComputableInPolyTime (fun (x : γ) => List.foldl (step x) (init x) (list x)) encIn encB

A fold callback may capture its original input. Growth is needed only on elements of the runtime list, for every accumulator. Joint computation and encoding evidence lets automation choose compatible list and callback certificates; paired growth obligations select a common polynomial bound. The general foldlWith_of_bounded_growth contract takes separate premises.

theorem Turing.MultiTapeTM.ComputableInPolyTime.foldl_of_bounded_growth {γ α β : Type} {encIn : γ ↪ List Bool} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {list : γ → List α} {init : γ → β} {step : β → α → β} (hlist : ComputableInPolyTime list encIn encL) (hinit : ComputableInPolyTime init encIn encB) (hstep : ComputableInPolyTime (fun (p : β × α) => step p.1 p.2) (encPair encB encA) encB) {growth : ℕ} (hgrowth : ∀ (state : β) (value : α), (encB (step state value)).length ≤ (encB state).length + growth) : ComputableInPolyTime (fun (x : γ) => List.foldl step (init x) (list x)) encIn encB

Constant additive growth discharges the fold's intermediate-size obligation.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterateWith_spec {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {π : Type} {encPar : π ↪ List Bool} {par : α → π} {count : α → ℕ} {init : α → β} {step : π → β → β} (hpar : ComputableInPolyTime par encIn encPar) (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime (fun (p : π × β) => step p.1 p.2) (encPair encPar encState) encState) (invariant : α → ℕ → β → Prop) (hbase : ∀ (x : α), invariant x 0 (init x)) (hpreserve : ∀ (x : α) (i : ℕ) (state : β), i < count x → invariant x i state → invariant x (i + 1) (step (par x) state)) {size : α → ℕ} (hsize : PolyBounded (fun (x : α) => (encIn x).length) size) (hbound : ∀ (x : α) (i : ℕ) (state : β), i ≤ count x → invariant x i state → (encState state).length ≤ size x) : ComputableInPolyTime (fun (x : α) => (step (par x))^[count x] (init x)) encIn encState ∧ ∀ (x : α), invariant x (count x) ((step (par x))^[count x] (init x))

Iteration may capture a computed parameter. The joint step certificate must be uniform in that parameter; the invariant and size bound concern the original input. The bound need not be computable and may use properties of the input beyond its encoded length.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterate_spec {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime step encState encState) (invariant : α → ℕ → β → Prop) (hbase : ∀ (x : α), invariant x 0 (init x)) (hpreserve : ∀ (x : α) (i : ℕ) (state : β), i < count x → invariant x i state → invariant x (i + 1) (step state)) {size : α → ℕ} (hsize : PolyBounded (fun (x : α) => (encIn x).length) size) (hbound : ∀ (x : α) (i : ℕ) (state : β), i ≤ count x → invariant x i state → (encState state).length ≤ size x) : ComputableInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState ∧ ∀ (x : α), invariant x (count x) (step^[count x] (init x))

One invariant proves both the resource bound and the final loop postcondition.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterateWith_of_bounded_growth {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {π : Type} {encPar : π ↪ List Bool} {par : α → π} {count : α → ℕ} {init : α → β} {step : π → β → β} (hpar : ComputableInPolyTime par encIn encPar) (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime (fun (p : π × β) => step p.1 p.2) (encPair encPar encState) encState) {growth : α → ℕ} (hpoly : PolyBounded (fun (x : α) => (encIn x).length) growth) (hgrowth : ∀ (x : α) (state : β), (encState (step (par x) state)).length ≤ (encState state).length + growth x) : ComputableInPolyTime (fun (x : α) => (step (par x))^[count x] (init x)) encIn encState

A captured loop may add a polynomial amount of storage per iteration, measured against the original input. A bound depending only on the current state would not justify this rule.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterateWithInput_of_bounded_growth {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : α → β → β} (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime (fun (p : α × β) => step p.1 p.2) (encPair encIn encState) encState) {growth : α → ℕ} (hbound : PolyBounded (fun (x : α) => (encIn x).length) growth ∧ ∀ (x : α) (state : β), (encState (step x state)).length ≤ (encState state).length + growth x) : ComputableInPolyTime (fun (x : α) => (step x)^[count x] (init x)) encIn encState

An iteration step may capture its original input. Paired growth obligations let automation select a common polynomial bound. The uniform joint step certificate charges the captured input on every iteration; the growth bound need not itself be computable.

theorem Turing.MultiTapeTM.ComputableInPolyTime.iterate_of_bounded_growth {α β : Type} {encIn : α ↪ List Bool} {encState : β ↪ List Bool} {count : α → ℕ} {init : α → β} {step : β → β} (hcount : ComputableInPolyTime count encIn encUnary) (hinit : ComputableInPolyTime init encIn encState) (hstep : ComputableInPolyTime step encState encState) {growth : ℕ} (hgrowth : ∀ (state : β), (encState (step state)).length ≤ (encState state).length + growth) : ComputableInPolyTime (fun (x : α) => step^[count x] (init x)) encIn encState

A loop with constant additive state growth has polynomially bounded intermediate states.