From 7e76c4e0a4791bf14e65beab18ea3807598c4ee4 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 25 Oct 2026 10:26:09 -0400 Subject: [PATCH] feat(polytime): prove plain binary-index list lookup directly Add `Turing.MultiTapeTM.ComputableInPolyTime.listGetD_binary`, the plain counterpart of the raw-calculus binary lookup rule, with its complete telescope: arbitrary element and input encodings, any `ListEncoding` with `SizedListEncoding`, a fixed default, a computed list and a computed binary (`encNat`) index. The proof reuses the capped-binary fold of the raw rule and uses only the direct plain prerequisites: the unary length by the direct fold, the capped index by the direct captured fold over the reversed index bits (states bounded by the length, so an unbounded binary index is never expanded to unary), the saturating step through `min cap (2v + b) = cap - (cap - v - v - b)` with the direct unary subtraction, and the direct unary lookup. The new Internal module does not import the tidy calculus; `PolyTime/List.lean` re-exports it. Tests cover generic, framed and raw-bit clients, a computed binary index, and controls: the unary rule and `fun_prop` reject a binary index certificate, the new rule rejects a unary one, and it does not apply without `SizedListEncoding`. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --- Complexity.lean | 1 + .../MultiTape/Complexity/PolyTime/List.lean | 1 + .../Internal/PolyTimeListBinaryLookup.lean | 96 +++++++++++++++++++ .../MultiTape/Internal/ListBinaryLookup.lean | 72 ++++++++++++++ 4 files changed, 170 insertions(+) create mode 100644 Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListBinaryLookup.lean create mode 100644 ComplexityTests/Machines/Turing/MultiTape/Internal/ListBinaryLookup.lean diff --git a/Complexity.lean b/Complexity.lean index eda377b71..73bdb42b6 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean index 226f6cddd..86d7514e9 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean +++ b/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 diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListBinaryLookup.lean b/Complexity/Computability/Machines/Turing/MultiTape/Internal/PolyTimeListBinaryLookup.lean new file mode 100644 index 000000000..30176caa9 --- /dev/null +++ b/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 diff --git a/ComplexityTests/Machines/Turing/MultiTape/Internal/ListBinaryLookup.lean b/ComplexityTests/Machines/Turing/MultiTape/Internal/ListBinaryLookup.lean new file mode 100644 index 000000000..054d21874 --- /dev/null +++ b/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