diff --git a/Complexity.lean b/Complexity.lean
index 390a2ae80e..6c305cd33a 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -908,6 +908,7 @@ public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Poly
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.Binary
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Int.BinaryDiv
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Matrix.Binary
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership
diff --git a/Complexity/Computability/Circuit/Boolean/CodeComposition.lean b/Complexity/Computability/Circuit/Boolean/CodeComposition.lean
index dc93382de4..2b859e3c6e 100644
--- a/Complexity/Computability/Circuit/Boolean/CodeComposition.lean
+++ b/Complexity/Computability/Circuit/Boolean/CodeComposition.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
 public import Complexity.Computability.Circuit.Pi
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
@@ -219,7 +220,7 @@ theorem computableTidilyInPolyTime_appendCode {α : Type} {enc : α ↪ List Boo
     (hd : ComputableTidilyInPolyTime d enc encCode) :
     ComputableTidilyInPolyTime (fun a => appendCode (n a) (c a) (d a)) enc encCode := by
   have hlen : ComputableTidilyInPolyTime (fun a => (c a).1.length) enc encNat :=
-    unary_to_binary.comp ((length_list encGate).comp hc.fst')
+    (ComputableInPolyTime.length_list_binary encGate).tidy.comp hc.fst'
   have hshift := computableTidilyInPolyTime_shiftCode hn hlen hd
   exact (listAppend' hc.fst' hshift.fst').prod (listAppend' hc.snd' hshift.snd')
 
@@ -302,7 +303,7 @@ theorem computableTidilyInPolyTime_appendCodes {α : Type} {enc : α ↪ List Bo
   have hprefixGates := flatMapWithInput (encB := encGate)
     (f := fun (_ : α × ((List (Op × List ℕ) × List ℕ) × ℕ)) c => c.1)
     hprefix ((snd _ encCode).fst')
-  have hoffset := unary_to_binary.comp ((length_list encGate).comp hprefixGates)
+  have hoffset := (ComputableInPolyTime.length_list_binary encGate).tidy.comp hprefixGates
   have hshift := computableTidilyInPolyTime_shiftCode (hn.comp hpar) hoffset hentry.fst'
   have hgates := flatMapWithInput (encB := encGate)
     (f := fun a (q : (List (Op × List ℕ) × List ℕ) × ℕ) =>
@@ -485,9 +486,9 @@ theorem compCode_code {n m p : ℕ} (d : Circuit signature m p)
     (hi : ComputableTidilyInPolyTime i enc encNat) :
     ComputableTidilyInPolyTime (fun a => compCodeWire (n a) (c a) (i a)) enc encNat := by
   have houtputs : ComputableTidilyInPolyTime (fun a => (c a).2.length) enc encNat :=
-    unary_to_binary.comp ((length_list encNat).comp hc.snd')
+    (ComputableInPolyTime.length_list_binary encNat).tidy.comp hc.snd'
   have hgates : ComputableTidilyInPolyTime (fun a => (c a).1.length) enc encNat :=
-    unary_to_binary.comp ((length_list encGate).comp hc.fst')
+    (ComputableInPolyTime.length_list_binary encGate).tidy.comp hc.fst'
   have hlookup : ComputableTidilyInPolyTime (fun a => (c a).2.getD (i a) 0) enc encNat :=
     listGetD_binary 0 hc.snd' hi
   unfold compCodeWire
diff --git a/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean b/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean
index 0f7699f3f8..2c350a4db5 100644
--- a/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean
+++ b/Complexity/Computability/Complexity/Classes/MIP/NEXP.lean
@@ -19,6 +19,7 @@ import Complexity.Computability.Complexity.Classes.IP.Simulation
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Finite
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fold
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
@@ -806,7 +807,7 @@ theorem computableTidilyInPolyTime_checkCert (c d : ℕ) :
     have hlen : ComputableTidilyInPolyTime
         (fun q : List Bool × Cert => q.2.length)
         (encPair encBits encCert) encNat :=
-      unary_to_binary.comp ((length_list encCertEntry).comp (snd encBits encCert))
+      (ComputableInPolyTime.length_list_binary encCertEntry).tidy.comp (snd encBits encCert)
     exact binary_lt' hpow (binary_mul' (const 2) hlen)
   exact bool_and' (bool_and' (bool_and' h1 h2) h3) h4
 
diff --git a/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean b/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean
index 0daaeb80aa..f15948d70d 100644
--- a/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean
+++ b/Complexity/Computability/Complexity/FineGrained/OrthogonalVectors.lean
@@ -13,6 +13,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.Streaming
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
@@ -373,8 +374,8 @@ theorem exists_computableTidilyInO_stream {half : CNF ℕ → List ℕ}
   -- the start of the stream: the state and the number of rounds in unary
   obtain ⟨d₀, _, hp₀⟩ := (show ComputableTidilyInPolyTime (fun φ : CNF ℕ => ((φ, half φ), 0))
     encCNF encStreamState by fun_prop).exists_degree
-  obtain ⟨d₁, _, hp₁⟩ := (ComputableTidilyInPolyTime.unary_to_binary.comp
-    ((ComputableTidilyInPolyTime.length_list encNat).comp hhalf)).exists_degree
+  obtain ⟨d₁, _, hp₁⟩ :=
+    ((ComputableInPolyTime.length_list_binary encNat).tidy.comp hhalf).exists_degree
   have h := hstream.comp (hp₀.inO.prod (unary_two_pow hp₁.inO))
   -- the bounds
   obtain ⟨cv, dv, hV⟩ := hhalf.polyBounded_length.exists_le
diff --git a/Complexity/Computability/Complexity/Problems/CircuitValue/Compilation.lean b/Complexity/Computability/Complexity/Problems/CircuitValue/Compilation.lean
index e7df5c72d7..4c7c0fd961 100644
--- a/Complexity/Computability/Complexity/Problems/CircuitValue/Compilation.lean
+++ b/Complexity/Computability/Complexity/Problems/CircuitValue/Compilation.lean
@@ -150,8 +150,7 @@ theorem exists_uniformCircuitFamily {α : Type} {enc : α ↪ List Bool}
   have hzero := hbits.comp ((ComputableTidilyInPolyTime.id' (encIn := enc)).prod
     (ComputableTidilyInPolyTime.const 0))
   have hblock : ComputableTidilyInPolyTime (fun a => (bits a 0).size) enc encNat := by
-    have h := ComputableTidilyInPolyTime.unary_to_binary.comp
-      ((ComputableTidilyInPolyTime.length_list encGate).comp hzero.fst')
+    have h := (ComputableInPolyTime.length_list_binary encGate).tidy.comp hzero.fst'
     convert h using 1
     funext a
     exact (Circuit.length_code_fst (bits a 0)).symm
diff --git a/Complexity/Computability/Complexity/Problems/Graph.lean b/Complexity/Computability/Complexity/Problems/Graph.lean
index 51e493d09d..2c61640d9b 100644
--- a/Complexity/Computability/Complexity/Problems/Graph.lean
+++ b/Complexity/Computability/Complexity/Problems/Graph.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.NP.Witness
 public import Mathlib.Combinatorics.SimpleGraph.Basic
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 
@@ -186,7 +187,8 @@ theorem computableTidilyInPolyTime_verifySubset {rel : Graph → ℕ → ℕ →
       (encPair (encPair encGraph encNat) encBits) encBool := by
   refine computableTidilyInPolyTime_subsetVerifier (encγ := encNat)
     (by unfold encGraph; fun_prop) (bool_and' ?_ ?_)
-  · exact (unary_to_binary.comp ((length_list encNat).comp (snd _ _))).decide_eq' (by fun_prop)
+  · exact (((ComputableInPolyTime.length_list_binary encNat).tidy.comp (snd _ _)).decide_eq'
+      (by fun_prop))
   · apply allWithInput (snd _ _)
     apply allWithInput ((snd _ _).comp (fst _ _))
     have hproj : ComputableTidilyInPolyTime
diff --git a/Complexity/Computability/Complexity/Problems/IndependentSet.lean b/Complexity/Computability/Complexity/Problems/IndependentSet.lean
index b1c5bcffd0..ca080840a4 100644
--- a/Complexity/Computability/Complexity/Problems/IndependentSet.lean
+++ b/Complexity/Computability/Complexity/Problems/IndependentSet.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Problems.SAT
 public import Complexity.Computability.Complexity.Reduction
 public import Mathlib.Combinatorics.SimpleGraph.Clique
 import Complexity.Computability.Complexity.CookLevin.Completeness
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 
@@ -329,7 +330,7 @@ theorem Occurrence.computableTidilyInPolyTime_conflict :
 theorem computableTidilyInPolyTime_toIndependentSet :
     ComputableTidilyInPolyTime toIndependentSet encCNF (encPair encGraph encNat) := by
   have hlen : ComputableTidilyInPolyTime (fun φ : CNF ℕ => φ.length) encCNF encNat :=
-    unary_to_binary.comp (length_list _)
+    (ComputableInPolyTime.length_list_binary _).tidy
   unfold toIndependentSet encGraph
   fun_prop
 
diff --git a/Complexity/Computability/Complexity/Problems/VertexCover.lean b/Complexity/Computability/Complexity/Problems/VertexCover.lean
index 9814158514..58058183e7 100644
--- a/Complexity/Computability/Complexity/Problems/VertexCover.lean
+++ b/Complexity/Computability/Complexity/Problems/VertexCover.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Computability.Complexity.Problems.IndependentSet
 public import Mathlib.Combinatorics.SimpleGraph.VertexCover
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 
@@ -230,7 +231,8 @@ theorem computableTidilyInPolyTime_verifier :
   have hadj := Graph.computableTidilyInPolyTime_adjBool.comp hproj
   refine computableTidilyInPolyTime_subsetVerifier (encγ := encNat) (by unfold encGraph; fun_prop)
     (bool_and' ?_ (allWithInput hV (allWithInput (hV.comp (fst _ _)) ?_)))
-  · exact (unary_to_binary.comp ((length_list encNat).comp (snd _ _))).decide_eq' (by fun_prop)
+  · exact (((ComputableInPolyTime.length_list_binary encNat).tidy.comp (snd _ _)).decide_eq'
+      (by fun_prop))
   · fun_prop
 
 /-- `VertexCover` belongs to `NP`. -/
diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Length.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Length.lean
new file mode 100644
index 0000000000..12fee5430f
--- /dev/null
+++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Length.lean
@@ -0,0 +1,51 @@
+/-
+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: candidate
+
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain
+public import Complexity.Tactic.PolyTime.Init
+
+/-!
+# Binary list length in polynomial time
+
+`Turing.MultiTapeTM.ComputableTidilyInPolyTime.length_list` computes the length of a framed list in
+unary (`encUnary`), the representation required by bounded loops and `List.range`. Verifiers and
+reductions that compare a list length against a binary parameter or add it to binary wire and
+vertex indices instead need the length in the binary natural encoding `encNat`. Composing
+`length_list` with `unary_to_binary` provides plain rules for `fun_prop` and `polytime`.
+
+## Main results
+
+* `Turing.MultiTapeTM.ComputableInPolyTime.length_list_binary`: the length of a framed list in
+  the binary encoding `encNat`.
+* `Turing.MultiTapeTM.ComputableInPolyTime.length_list_binary'`: the binary length of a computed
+  framed list, fixing the intermediate list encoding for proof search.
+-/
+
+public section
+
+namespace Turing.MultiTapeTM.ComputableInPolyTime
+
+/-- Length of a framed list in binary (`encNat`); the element encoding is inferred from the list
+encoding. -/
+@[fun_prop, aesop safe -30 apply (rule_sets := [PolyTime])]
+theorem length_list_binary {α : Type} (enc : α ↪ List Bool) :
+    ComputableInPolyTime (fun l : List α => l.length) (encList enc) encNat :=
+  .of_tidy (ComputableTidilyInPolyTime.unary_to_binary.comp (.length_list enc))
+
+/-- Length of a computed framed list in binary (`encNat`), fixing the intermediate list encoding for
+proof search. -/
+@[fun_prop, aesop safe -30 apply (rule_sets := [PolyTime])]
+theorem length_list_binary' {α β : Type} {input : α ↪ List Bool} {enc : β ↪ List Bool}
+    {list : α → List β} (hlist : ComputableInPolyTime list input (encList enc)) :
+    ComputableInPolyTime (fun a => (list a).length) input encNat :=
+  (length_list_binary enc).comp hlist
+
+end Turing.MultiTapeTM.ComputableInPolyTime
diff --git a/Complexity/Tactic/PolyTime.lean b/Complexity/Tactic/PolyTime.lean
index 0087bd0792..d553303de0 100644
--- a/Complexity/Tactic/PolyTime.lean
+++ b/Complexity/Tactic/PolyTime.lean
@@ -9,6 +9,7 @@ module
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.BitString
+public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Length
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Membership
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
diff --git a/ComplexityTests/PolyTimeTactic.lean b/ComplexityTests/PolyTimeTactic.lean
index 306b7897e2..51f9930cf4 100644
--- a/ComplexityTests/PolyTimeTactic.lean
+++ b/ComplexityTests/PolyTimeTactic.lean
@@ -462,4 +462,17 @@ example : ComputableInPolyTime
     (encList (encPair encNat encNat)) := by
   polytime
 
+-- Binary list length is reached from `Complexity.Tactic.PolyTime`.
+example : ComputableInPolyTime (fun l : List ℕ => l.length)
+    (encList encNat) encNat := by
+  polytime
+
+example : ComputableInPolyTime (fun l : List ℕ => l.length)
+    (encList encNat) encNat := by
+  fun_prop
+
+example : ComputableInPolyTime (fun p : List ℕ × ℕ => p.1.length)
+    (encPair (encList encNat) encNat) encNat := by
+  fun_prop
+
 end ComplexityTests.PolyTimeTactic