Direct finite-table construction, lookup and update

The fixed index order and framed-list representation are unchanged. Lookup composes the existing head and tail codec machines; finite runtime dispatch retains the full captured input in each branch. The direct proofs introduce no default inhabitant requirement on the value or index type.

theorem Turing.MultiTapeTM.ComputableInPolyTime.finite_cases {α β Tag : Type} [Finite Tag] {input : α ↪ List Bool} {output : β ↪ List Bool} {tagEncoding : Tag ↪ List Bool} {tag : α → Tag} {branch : Tag → α → β} (htag : ComputableInPolyTime tag input tagEncoding) (hbranch : ∀ (choice : Tag), ComputableInPolyTime (branch choice) input output) : ComputableInPolyTime (fun (a : α) => branch (tag a) a) input output

A fixed finite tag selects a certified branch, charging the tag and captured input. Neither the tag nor the result type requires a default inhabitant.

theorem Turing.MultiTapeTM.ComputableInPolyTime.ofFn {α Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} {count : ℕ} {values : α → Fin count → Value} (hvalues : ∀ (i : Fin count), ComputableInPolyTime (fun (a : α) => values a i) input enc) : ComputableInPolyTime (fun (a : α) => List.ofFn (values a)) input (encList enc)

Construct a list of a fixed number of efficiently computed entries.

theorem Turing.MultiTapeTM.ComputableInPolyTime.pi {α Index Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} [Fintype Index] {values : α → Index → Value} (hvalues : ∀ (i : Index), ComputableInPolyTime (fun (a : α) => values a i) input enc) : ComputableInPolyTime values input (encPi enc)

Construct a table by computing each entry, retaining the original input in each computation.

theorem Turing.MultiTapeTM.ComputableInPolyTime.pi_apply {Index Value : Type} [Fintype Index] (enc : Value ↪ List Bool) (i : Index) : ComputableInPolyTime (fun (values : Index → Value) => values i) (encPi enc) enc

Read a fixed entry, charging for the stored prefix without requiring a default value.

theorem Turing.MultiTapeTM.ComputableInPolyTime.pi_update {α Index Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} [Fintype Index] [DecidableEq Index] {values : α → Index → Value} {value : α → Value} (hvalues : ComputableInPolyTime values input (encPi enc)) (hvalue : ComputableInPolyTime value input enc) (i : Index) : ComputableInPolyTime (fun (a : α) => Function.update (values a) i (value a)) input (encPi enc)

Update a fixed table entry while charging for all preserved entries.

theorem Turing.MultiTapeTM.ComputableInPolyTime.pi_apply' {α Index Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} [Fintype Index] {indexEncoding : Index ↪ List Bool} {values : α → Index → Value} {index : α → Index} (hvalues : ComputableInPolyTime values input (encPi enc)) (hindex : ComputableInPolyTime index input indexEncoding) : ComputableInPolyTime (fun (a : α) => values a (index a)) input enc

Read a computed index of a fixed finite table, charging the index and all stored entries.

theorem Turing.MultiTapeTM.ComputableInPolyTime.pi_update' {α Index Value : Type} {input : α ↪ List Bool} {enc : Value ↪ List Bool} [Fintype Index] [DecidableEq Index] {indexEncoding : Index ↪ List Bool} {values : α → Index → Value} {index : α → Index} {value : α → Value} (hvalues : ComputableInPolyTime values input (encPi enc)) (hindex : ComputableInPolyTime index input indexEncoding) (hvalue : ComputableInPolyTime value input enc) : ComputableInPolyTime (fun (a : α) => Function.update (values a) (index a) (value a)) input (encPi enc)

Update a computed index while retaining and charging every other entry.