SamuelSchlesinger · Oct 24, 2026 · Oct 24, 2026 · Oct 24, 2026 · Oct 24, 2026
diff --git a/Complexity.lean b/Complexity.lean
@@ -1646,9 +1646,13 @@ public import Complexity.Foundations.Data.Finset.Sampling
 public import Complexity.Foundations.Data.Finset.SymmDiff
 public import Complexity.Foundations.Data.Hamming
 public import Complexity.Foundations.Data.HammingBound
+public import Complexity.Foundations.Data.List.Append
 public import Complexity.Foundations.Data.List.BalancedFold
 public import Complexity.Foundations.Data.List.Basic
+public import Complexity.Foundations.Data.List.Counting
 public import Complexity.Foundations.Data.List.Equiv
+public import Complexity.Foundations.Data.List.Fold
+public import Complexity.Foundations.Data.List.Lookup
 public import Complexity.Foundations.Data.List.OfFn
 public import Complexity.Foundations.Data.ListDecoding
 public import Complexity.Foundations.Data.Matrix.Binary

diff --git a/Complexity/Computability/Circuit/Boolean/DepthTime.lean b/Complexity/Computability/Circuit/Boolean/DepthTime.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
 public import Complexity.Computability.Circuit.Depth
 
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # Computing the depths of a Boolean circuit

diff --git a/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean b/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean
@@ -14,7 +14,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Finite
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean b/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Circuit.Boolean.Layered
 public import Complexity.Computability.Circuit.Boolean.DepthTime
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Circuit.Boolean.Encoding
 public import Complexity.Computability.Circuit.Boolean.Tableau.Layout
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # The uniform tableau circuit of a multi-tape machine

diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Circuit.Boolean.Tableau.Basic
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Circuit/Rational/EncodingBounds.lean b/Complexity/Computability/Circuit/Rational/EncodingBounds.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Init
 public import Complexity.Computability.Circuit.Rational.IntegralLift
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Counting
 import Mathlib.Data.Nat.Digits.Lemmas
 import Mathlib.LinearAlgebra.Matrix.AbsoluteValue
 

diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean
@@ -11,7 +11,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace
 public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Formula
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram
 public import Complexity.Logics.FirstOrder.Encoding.Layout
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # First-order model checking in logarithmic space

diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram
 public import Complexity.Logics.FirstOrder.Basic
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # Shared first-order counter-program control

diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Output.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Output.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # Shared output routines for first-order interpretation transducers

diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Output
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output
 public import Complexity.Logics.FirstOrder.Interpretation.Rank
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # The domain-counting interpretation transducer

diff --git a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean
@@ -14,6 +14,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fo
 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.Option
+import Complexity.Foundations.Data.List.Counting
 
 /-!
 # Generalized Geography is in `PSPACE`

diff --git a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean
@@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Classes.Space.TQBF.Prenex
 import Complexity.Computability.Complexity.Classes.Space.TQBF.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
+import Complexity.Foundations.Data.List.Counting
 
 /-!
 # Generalized Geography is `PSPACE`-hard

diff --git a/Complexity/Computability/Complexity/Problems/Coloring.lean b/Complexity/Computability/Complexity/Problems/Coloring.lean
@@ -14,7 +14,7 @@ import Complexity.Computability.Complexity.CookLevin.Completeness
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Counting
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Complexity/Problems/GeneralizedGeography.lean b/Complexity/Computability/Complexity/Problems/GeneralizedGeography.lean
@@ -8,7 +8,6 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Complexity.Problems.IndependentSet
-public import Complexity.Foundations.Data.List.Basic
 
 /-!
 # Generalized Geography

diff --git a/Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean b/Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean
@@ -16,7 +16,7 @@ import Complexity.Computability.Complexity.Problems.Hamiltonian.Directed
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean b/Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Computability.Complexity.Problems.IndependentSet
 public import Complexity.Computability.Complexity.Problems.SubsetSum
 import Complexity.Computability.Complexity.FineGrained.Assignment
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Counting
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 

diff --git a/Complexity/Computability/Complexity/Problems/SharpSAT.lean b/Complexity/Computability/Complexity/Problems/SharpSAT.lean
@@ -14,7 +14,7 @@ public import Complexity.Logics.Propositional.CNF.ModelCount
 import Complexity.Computability.Complexity.Problems.SAT.PolyTime
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Complexity/Problems/USTCON.lean b/Complexity/Computability/Complexity/Problems/USTCON.lean
@@ -12,7 +12,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
 public import Mathlib.Data.List.OfFn
 public import Mathlib.Data.List.GetD
 public import Mathlib.Data.Nat.Size
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Append
 
 /-!
 # Undirected s–t connectivity

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean
@@ -10,7 +10,6 @@ module
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.QueryMachine
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpace.Bit
-import Complexity.Foundations.Data.List.Basic
 import Mathlib.Data.List.GetD
 
 /-!

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Fold
 import Mathlib.Data.Fintype.Basic
 
 /-!

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Fold
 
 /-!
 # Polynomial-time folds

diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO
 import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Reverse
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Fold
 public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StreamFold
 import Mathlib.Tactic.Linarith
 

diff --git a/Complexity/Computability/Probabilistic/Finite.lean b/Complexity/Computability/Probabilistic/Finite.lean
@@ -8,7 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Computability.Probabilistic.PPT.Capture
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Fold
 import Mathlib.Data.Fintype.Basic
 
 /-!

diff --git a/Complexity/Computability/Probabilistic/Oracle/Tidy.lean b/Complexity/Computability/Probabilistic/Oracle/Tidy.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Computability.Probabilistic.Oracle
 public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Tidy
 public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Fold
 import Mathlib.Data.Fintype.Basic
 
 /-!

diff --git a/Complexity/Computability/TreeEval/Encoding.lean b/Complexity/Computability/TreeEval/Encoding.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Computability.TreeEval.Basic
 public import Mathlib.Data.List.OfFn
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Append
 
 /-!
 # Bit encodings of Tree Evaluation instances

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized
 import Mathlib.Algebra.BigOperators.Fin
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 
 /-!
 # Exact bridges for the serialized GSW algorithms

diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean
@@ -10,7 +10,7 @@ module
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness
 public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption
 import Mathlib.Algebra.BigOperators.Fin
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Lookup
 import Complexity.Foundations.Data.Nat.Bits
 
 /-!

diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid.lean
@@ -9,7 +9,7 @@ module
 
 public import Complexity.Crypto.Computational.Homomorphic.KeyChain
 public import Complexity.Crypto.Computational.Homomorphic.BitEncryption
-import Complexity.Foundations.Data.List.Basic
+import Complexity.Foundations.Data.List.Append
 import Complexity.Probability.PMF
 
 /-!

diff --git a/Complexity/Foundations/Data/List/Append.lean b/Complexity/Foundations/Data/List/Append.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner, Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Data.List.Basic
+
+/-!
+# List append boundaries and unary delimiters
+
+## Main results
+
+* `List.zip_tail_append_cons`: split adjacent pairs at a shared boundary element.
+* `List.replicate_not_append_cons_inj`, `List.replicate_true_append_false_inj`: a unary block
+  followed by its delimiter determines both its length and the remaining suffix.
+-/
+
+@[expose] public section
+
+/-- Split consecutive pairs at a boundary element shared by the two list segments. -/
+theorem List.zip_tail_append_cons {α : Type*} (before : List α) (middle : α)
+    (after : List α) :
+    (before ++ middle :: after).zip (before ++ middle :: after).tail =
+      (before ++ [middle]).zip (before ++ [middle]).tail ++ (middle :: after).zip after := by
+  induction before with
+  | nil => simp
+  | cons first before ih =>
+    cases before with
+    | nil => simp
+    | cons second before =>
+      simpa only [List.cons_append, List.tail_cons, List.zip_cons_cons] using
+        congrArg (List.cons (first, second)) ih
+
+/-- A unary block of copies of `!a` followed by the delimiter `a` determines both its length and the
+remaining suffix. -/
+theorem List.replicate_not_append_cons_inj {a : Bool} {m m' : ℕ} {l l' : List Bool}
+    (h : List.replicate m (!a) ++ a :: l = List.replicate m' (!a) ++ a :: l') :
+    m = m' ∧ l = l' := by
+  induction m generalizing m' <;> cases m' <;> simp_all [List.replicate_succ]
+
+/-- A unary block of `true` bits followed by `false` determines both its length and the remaining
+suffix. -/
+theorem List.replicate_true_append_false_inj {m m' : ℕ} {l l' : List Bool}
+    (h : List.replicate m true ++ false :: l = List.replicate m' true ++ false :: l') :
+    m = m' ∧ l = l' :=
+  List.replicate_not_append_cons_inj (a := false) h