Direct plain list lookup at a binary index

Lookup in a computed list at a computed index encoded in binary. The index is first capped at the length of the list by the saturating fold Cslib.BitString.boundedBinaryValue, which reads the binary digits most significant first and caps every partial value. An index far beyond the list therefore costs only its encoded length and is never expanded to unary; beyond the list every lookup returns the default.

The capped-binary fold is the one used by the binary lookup rule of the raw calculus in Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean. Here it is certified directly, with the plain fold, the unary list length, unary subtraction and lookup at a unary index. The saturating step min cap (2 * v + b) is computed as cap - (cap - v - v - b).

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.listGetD_binary: lookup with a fixed default at a binary index, in any sized list encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listGetD_binary {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] {l : γ → List α} {i : γ → ℕ} (d : α) (hl : ComputableInPolyTime l encIn encL) (hi : ComputableInPolyTime i encIn encNat) : ComputableInPolyTime (fun (x : γ) => (l x).getD (i x) d) encIn encA

Lookup in a computed list at a computed binary index, with a fixed default, in any sized list encoding. The index is first capped at the length of the list, reading its binary digits most significant first and capping every partial value, so an index far beyond the list costs only its encoded length; beyond the list every lookup returns the default.