feat(polytime): add plain binary list length rules and wire into PolyTime

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

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

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
 

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

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

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

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
 

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`. -/

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

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

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