feat(polytime): expose plain framed and computed-word lengths

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 :
@@ -988,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

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