feat(polytime): prove plain binary-index list lookup directly

Complexity.lean

@@ -1045,6 +1045,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Partrec
 public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Reduction
 public import Complexity.Computability.Machines.Turing.MultiTape.Halting.Rice
 public import Complexity.Computability.Machines.Turing.MultiTape.Halting.SMN
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap
 public import Complexity.Computability.Machines.Turing.MultiTape.Machine

Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListMap
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fold
 public import Complexity.Computability.Machines.Turing.MultiTape.PolyTime
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option

Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListBinaryLookup.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 Erik Demaine, Christian Reitwiessner, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Erik Demaine, Christian Reitwiessner, Samuel Schlesinger
+-/
+module
+-- upstream: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListLookup
+public import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeNatFrontends
+import Complexity.Foundations.Data.BitString.List.Binary
+import Mathlib.Data.List.GetD
+
+/-!
+# 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.
+-/
+
+@[expose] public section
+
+namespace Turing.MultiTapeTM.ComputableInPolyTime
+
+open Cslib
+
+/-- 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. -/
+theorem 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 := by
+  have hlen : ComputableInPolyTime (fun x => (l x).length) encIn encUnary := by
+    have h := foldl' (encA := encA) (encL := encL) (encB := encUnary) (list := l)
+      (init := fun _ => 0) (step := fun n _ => n + 1) hl (const 0)
+      (unary_succ.comp (fst encUnary encA)) (B := fun x => (encL (l x)).length)
+      hl.polyBounded_length (fun x j _ => by
+        simpa [List.foldl_const] using (Nat.min_le_right j (l x).length).trans
+          (SizedListEncoding.length_le (encA := encA) (encL := encL) (l x)))
+    simpa [List.foldl_const] using h
+  have hstep : ComputableInPolyTime
+      (fun p : (ℕ × ℕ) × Bool => min p.1.1 (2 * p.1.2 + p.2.toNat))
+      (encPair (encPair encUnary encUnary) encBool) encUnary := by
+    have hq := fst (encPair encUnary encUnary) encBool
+    have hb : ComputableInPolyTime (fun p : (ℕ × ℕ) × Bool => p.2.toNat)
+        (encPair (encPair encUnary encUnary) encBool) encUnary :=
+      (of_finite (encIn := encBool) (encOut := encUnary) Bool.toNat).comp
+        (snd (encPair encUnary encUnary) encBool)
+    have h := unary_sub.comp (hq.fst'.prod (unary_sub.comp
+      ((unary_sub.comp ((unary_sub.comp (hq.fst'.prod hq.snd')).prod hq.snd')).prod hb)))
+    have heq : (fun p : (ℕ × ℕ) × Bool => min p.1.1 (2 * p.1.2 + p.2.toNat)) =
+        fun p => p.1.1 - (p.1.1 - p.1.2 - p.1.2 - p.2.toNat) := by
+      funext p
+      omega
+    rw [heq]
+    simpa only [Function.comp_def] using h
+  have hcap : ComputableInPolyTime
+      (fun x => BitString.boundedBinaryValue (l x).length (encNat (i x)).reverse)
+      encIn encUnary :=
+    foldlWith (encA := encBool) (encL := encBits) (encP := encUnary) (encB := encUnary)
+      (par := fun x => (l x).length) (list := fun x => (encNat (i x)).reverse)
+      (step := fun cap value bit => min cap (2 * value + bit.toNat))
+      hlen (bitsReverse.comp (hi.of_enc_eq (encD := encBits) fun _ => rfl)) (const 0) hstep
+      (B := fun x => (l x).length)
+      (by simpa only [encUnary_apply, List.length_replicate] using hlen.polyBounded_length)
+      (fun x j _ => by
+        simpa only [encUnary_apply, List.length_replicate, BitString.boundedBinaryValue] using
+          BitString.boundedBinaryValue_le (l x).length ((encNat (i x)).reverse.take j))
+  have heq : (fun x => (l x).getD (i x) d) = fun x =>
+      (l x).getD (BitString.boundedBinaryValue (l x).length (encNat (i x)).reverse) d := by
+    funext x
+    rw [BitString.boundedBinaryValue_eq, encNat_apply, BitString.binaryValue_reverse_bits]
+    rcases le_total (i x) (l x).length with h | h
+    · rw [Nat.min_eq_right h]
+    · rw [Nat.min_eq_left h, List.getD_eq_default _ _ h, List.getD_eq_default _ _ le_rfl]
+  rw [heq]
+  exact (listGetD d).comp (hl.prod hcap)
+
+end Turing.MultiTapeTM.ComputableInPolyTime

ComplexityTests/Machines/Turing/MultiTape/Internal/ListBinaryLookup.lean

@@ -0,0 +1,72 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+module
+-- upstream: local-only (test driver)
+
+import Complexity.Computability.Machines.Turing.MultiTape.Internal.PolyTimeListBinaryLookup
+
+/-! # Generic, framed and raw-bit lookup at a binary index -/
+
+open Turing.MultiTapeTM
+
+run_elab do
+  for name in #[`Turing.MultiTapeTM.ComputableTidilyInPolyTime,
+      `Turing.MultiTapeTM.ComputableTidilyInDegree, `Turing.MultiTapeTM.ComputableTidilyInO] do
+    if (← Lean.getEnv).contains name then throwError "unexpected higher tidy calculus: {name}"
+
+-- The complete telescope: arbitrary element and input encodings, any sized list encoding,
+-- a fixed default, a computed list and a computed binary index.
+example {α γ : 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 := by
+  -- Neither the unary lookup rule nor automation accepts a binary index certificate.
+  fail_if_success exact (ComputableInPolyTime.listGetD d).comp (hl.prod hi)
+  fail_if_success fun_prop
+  exact ComputableInPolyTime.listGetD_binary d hl hi
+
+-- A unary index certificate does not match the binary premise.
+example {α γ : 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 encUnary) :
+    ComputableInPolyTime (fun x => (l x).getD (i x) d) encIn encA := by
+  fail_if_success exact ComputableInPolyTime.listGetD_binary d hl hi
+  exact (ComputableInPolyTime.listGetD d).comp (hl.prod hi)
+
+-- Without the size premise on the list encoding the rule does not apply.
+example {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool}
+    {encL : List α ↪ List Bool} [ListEncoding encA encL]
+    {l : γ → List α} {i : γ → ℕ} (_d : α)
+    (_hl : ComputableInPolyTime l encIn encL) (_hi : ComputableInPolyTime i encIn encNat) :
+    True := by
+  fail_if_success
+    have := ComputableInPolyTime.listGetD_binary (encA := encA) (encL := encL) _d _hl _hi
+  trivial
+
+-- Raw bit strings: read a bit at a binary position.
+example : ComputableInPolyTime (fun p : List Bool × ℕ => p.1.getD p.2 false)
+    (encPair encBits encNat) encBool :=
+  ComputableInPolyTime.listGetD_binary (encA := encBool) false
+    (ComputableInPolyTime.fst encBits encNat) (ComputableInPolyTime.snd encBits encNat)
+
+-- Framed lists of binary naturals.
+example : ComputableInPolyTime (fun p : List ℕ × ℕ => p.1.getD p.2 0)
+    (encPair (encList encNat) encNat) encNat :=
+  ComputableInPolyTime.listGetD_binary 0
+    (ComputableInPolyTime.fst (encList encNat) encNat) (ComputableInPolyTime.snd _ encNat)
+
+-- A binary index computed from the input: follow the pointer stored in the first entry.
+example : ComputableInPolyTime (fun l : List ℕ => l.getD (l.getD 0 0) 0) (encList encNat) encNat :=
+  ComputableInPolyTime.listGetD_binary 0 ComputableInPolyTime.id'
+    ((ComputableInPolyTime.listGetD 0).comp
+      (ComputableInPolyTime.id'.prod (ComputableInPolyTime.const 0)))
+
+-- Beyond the list every lookup returns the default, however large the binary index.
+example : ([true, false] : List Bool).getD 1 true = false := by decide
+example : ([true, false] : List Bool).getD (2 ^ 64) true = true := by decide
+example : ([] : List ℕ).getD (2 ^ 64) 7 = 7 := by decide