From 5eb47491ba1e28fc9d719093f8c43390dcff4fc2 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 24 Oct 2026 10:05:18 -0400
Subject: [PATCH 1/2] feat(polytime): expose plain framed-list length
 certificate

---
 .../MultiTape/Complexity/PolyTime/List.lean      |  6 ++++++
 ComplexityTests/ListZipIdx.lean                  | 16 ++++++++++++++++
 2 files changed, 22 insertions(+)

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
index f43a59c2d..fadabcf2c 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
@@ -951,6 +951,12 @@ theorem headD {α : Type}
   encL encA :=
   .of_tidy (@Turing.MultiTapeTM.ComputableTidilyInPolyTime.headD α encA encL _inst3 fallback)
 
+/-- Length of a framed list, for any element encoding, with a unary result. -/
+@[fun_prop]
+theorem length_list {α : Type} (enc : α ↪ List Bool) :
+    ComputableInPolyTime (fun l : List α => l.length) (encList enc) encUnary :=
+  .of_tidy (ComputableTidilyInPolyTime.length_list enc)
+
 /-- Length of a raw bit string. -/
 @[fun_prop]
 theorem length_bits :
diff --git a/ComplexityTests/ListZipIdx.lean b/ComplexityTests/ListZipIdx.lean
index 747545d97..d9554a619 100644
--- a/ComplexityTests/ListZipIdx.lean
+++ b/ComplexityTests/ListZipIdx.lean
@@ -27,4 +27,20 @@ example {α Input : Type} (enc : α ↪ List Bool) (input : Input ↪ List Bool)
   fail_if_success (clear hlist; fun_prop)
   polytime
 
+-- Framing supplies the length; no element decoder or computational hypothesis is needed.
+example {α : Type} (enc : α ↪ List Bool) :
+    ComputableInPolyTime (fun list : List α => list.length) (encList enc) encUnary := by
+  fun_prop
+
+example (empty : Empty ↪ List Bool) :
+    ComputableInPolyTime (fun list : List Empty => list.length) (encList empty) encUnary := by
+  fun_prop
+
+-- The list may be computed from the complete caller context.
+example {α Input : Type} (enc : α ↪ List Bool) (input : Input ↪ List Bool)
+    (list : Input → List α) (hlist : ComputableInPolyTime list input (encList enc)) :
+    ComputableInPolyTime (fun x => (list x).length) input encUnary := by
+  fail_if_success (clear hlist; fun_prop)
+  fun_prop
+
 end ComplexityTests.ListZipIdx

From f2b1294bfdf71cbac2dc60200295ca1e7f88ff51 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sat, 24 Oct 2026 10:41:55 -0400
Subject: [PATCH 2/2] fix(polytime): infer the encoding of computed word
 lengths

---
 .../Turing/MultiTape/Complexity/PolyTime/List.lean         | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
index fadabcf2c..3d469155b 100644
--- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/List.lean
@@ -994,4 +994,11 @@ theorem bitsDropWithInput {α : Type} {input : α ↪ List Bool}
     ComputableInPolyTime (fun a => (list a).drop (count a)) input encBits :=
   .of_tidy (ComputableTidilyInPolyTime.bitsDropWithInput hlist.tidy hcount.tidy)
 
+/-- Length of a computed raw word, fixing the intermediate encoding for proof search. -/
+@[fun_prop]
+theorem length_bits_comp {α : Type} {input : α ↪ List Bool} {word : α → List Bool}
+    (hword : ComputableInPolyTime word input encBits) :
+    ComputableInPolyTime (fun a => (word a).length) input encUnary :=
+  length_bits.comp hword
+
 end Turing.MultiTapeTM.ComputableInPolyTime