From 71453ee6e6d903cacc0cbaead9cfff8b0f72e0cf Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <SamuelSchlesinger@users.noreply.github.com>
Date: Fri, 23 Oct 2026 15:29:10 -0400
Subject: [PATCH 1/2] feat(circuit): construct uniform logarithmic-depth binary
 addition

Build an actual prefix-doubling carry-lookahead circuit with exact unsigned
carry-in/out semantics, modular addition, explicit logarithmic depth and
polynomial size. Certify native generation of complete binary circuit codes
and supply a logarithmic-depth carry-save finishing client.

Reuse reviewed variable-size code composition through a fixed-formula template
API. Add a shared bit-string/word value bridge and a bound charging every
encoded gate, output reference and framing bit.

Source: Ladner and Fischer, Parallel Prefix Computation (1980), Section 4;
the implementation uses the simple doubling network and OR-propagate summaries.
All six scripts/check.sh gates passed on the final combined source tree.
AI-assisted implementation by Codex (worker-codex-carry-lookahead-20261023).
---
 Complexity.lean                               |   4 +
 .../Circuit/Boolean/CarryLookahead.lean       | 547 ++++++++++++++++++
 .../Boolean/CarryLookahead/PolyTime.lean      | 450 ++++++++++++++
 .../Circuit/Boolean/CodeTemplate.lean         |  71 +++
 .../Circuit/Boolean/EncodingSize.lean         |  68 +++
 .../Computability/Circuit/Boolean/Word.lean   |  30 +
 ComplexityTests.lean                          |   1 +
 ComplexityTests/CarryLookahead.lean           | 149 +++++
 8 files changed, 1320 insertions(+)
 create mode 100644 Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
 create mode 100644 Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean
 create mode 100644 Complexity/Computability/Circuit/Boolean/CodeTemplate.lean
 create mode 100644 Complexity/Computability/Circuit/Boolean/EncodingSize.lean
 create mode 100644 ComplexityTests/CarryLookahead.lean

diff --git a/Complexity.lean b/Complexity.lean
index 32982b1eb..787815ed7 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -125,9 +125,12 @@ public import Complexity.Computability.Circuit.Boolean.BinaryCost
 public import Complexity.Computability.Circuit.Boolean.BitBlast
 public import Complexity.Computability.Circuit.Boolean.BoundedError
 public import Complexity.Computability.Circuit.Boolean.Broadcast
+public import Complexity.Computability.Circuit.Boolean.CarryLookahead
+public import Complexity.Computability.Circuit.Boolean.CarryLookahead.PolyTime
 public import Complexity.Computability.Circuit.Boolean.CarrySave
 public import Complexity.Computability.Circuit.Boolean.CodeComposition
 public import Complexity.Computability.Circuit.Boolean.CodeSubstitution
+public import Complexity.Computability.Circuit.Boolean.CodeTemplate
 public import Complexity.Computability.Circuit.Boolean.CompareSwap
 public import Complexity.Computability.Circuit.Boolean.Comparison
 public import Complexity.Computability.Circuit.Boolean.Conondeterministic
@@ -141,6 +144,7 @@ public import Complexity.Computability.Circuit.Boolean.DuplicateFlags
 public import Complexity.Computability.Circuit.Boolean.ElementDistinctness
 public import Complexity.Computability.Circuit.Boolean.Encoding
 public import Complexity.Computability.Circuit.Boolean.Encoding.Certificate
+public import Complexity.Computability.Circuit.Boolean.EncodingSize
 public import Complexity.Computability.Circuit.Boolean.Equality
 public import Complexity.Computability.Circuit.Boolean.EvaluationTime
 public import Complexity.Computability.Circuit.Boolean.FanInTwo
diff --git a/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean b/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
new file mode 100644
index 000000000..35587403f
--- /dev/null
+++ b/Complexity/Computability/Circuit/Boolean/CarryLookahead.lean
@@ -0,0 +1,547 @@
+/-
+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.Circuit.Boolean.CarrySave
+public import Complexity.Computability.Circuit.Boolean.Word
+
+/-!
+# Carry lookahead by parallel prefix doubling
+
+A carry summary `(g, p)` acts on a carry `c` by `g || (p && c)`. Summaries are composed in
+significance order. Each round doubles the interval summarized by each cell; cells without a
+neighbour retain their summary. The initial carry is an additional cell, so width zero still
+has one output: that carry.
+
+The construction uses the associative carry-transfer operation underlying parallel-prefix
+addition [Ladner and Fischer, Section 4][LadnerFischer1980]. OR-propagate summaries represent
+the same carry functions. It uses the simple doubling network, rather than their optimized
+linear-size prefix network. All gates, including constants and negations, count.
+
+## Main definitions
+
+* `Cslib.Circuits.Boolean.CarryLookahead.step`: one prefix-doubling circuit.
+* `Cslib.Circuits.Boolean.CarryLookahead.scan`: the prefix circuit after a specified number
+  of rounds.
+* `Cslib.Circuits.Boolean.carryLookahead`: full addition with carry-in and carry-out.
+* `Cslib.Circuits.Boolean.carryLookaheadAdd`: modular addition of two unsigned words.
+* `Cslib.Circuits.Boolean.carryLookaheadFinish`: finish a carry-save pair in logarithmic depth.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.val_eval_carryLookahead`: exact unsigned addition at every width.
+* `Cslib.Circuits.Boolean.depth_carryLookahead_le`, `size_carryLookahead`: depth at most
+  `7 + 2 * clog 2 (w + 1)` and exactly `15*w + 2*(w+1) + 3*(w+1)*clog 2 (w+1)` gates.
+* `Cslib.Circuits.Boolean.val_eval_carryLookaheadAdd`: addition modulo `2^w`.
+* `Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod`: a finishing client
+  for the existing carry-save reduction.
+
+Native polynomial-time generation of the complete codes is proved in `CarryLookahead.PolyTime`.
+
+## References
+
+* [R. E. Ladner, M. J. Fischer, *Parallel Prefix Computation*][LadnerFischer1980]
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Boolean
+
+namespace CarryLookahead
+
+variable {k : ℕ}
+
+/-- Compose the high-significance summary with the low-significance summary. -/
+def combine (high low : Bool × Bool) : Bool × Bool :=
+  (high.1 || (high.2 && low.1), high.2 && low.2)
+
+private theorem combine_assoc (a b c : Bool × Bool) :
+    combine (combine a b) c = combine a (combine b c) := by
+  rcases a with ⟨a, a'⟩; rcases b with ⟨b, b'⟩; rcases c with ⟨c, c'⟩
+  cases a <;> cases a' <;> cases b <;> cases b' <;> cases c <;> cases c' <;> rfl
+
+@[simp] theorem combine_unit_left (a : Bool × Bool) : combine (false, true) a = a := by
+  cases a; simp [combine]
+
+@[simp] theorem combine_unit_right (a : Bool × Bool) : combine a (false, true) = a := by
+  cases a; simp [combine]
+
+@[simp] theorem combine_self (a : Bool × Bool) : combine a a = a := by
+  rcases a with ⟨a, b⟩; cases a <;> cases b <;> rfl
+
+/-- Consecutive carry summaries, with the most significant one first. -/
+def rangeSummary (row : ℕ → Bool × Bool) (start : ℕ) : ℕ → Bool × Bool
+  | 0 => (false, true)
+  | count + 1 => combine (row start) (rangeSummary row (start + 1) count)
+
+private theorem rangeSummary_add (row : ℕ → Bool × Bool) (start m n : ℕ) :
+    rangeSummary row start (m + n) =
+      combine (rangeSummary row start m) (rangeSummary row (start + m) n) := by
+  induction m generalizing start with
+  | zero => simp [rangeSummary]
+  | succ m ih =>
+    rw [show m + 1 + n = (m + n) + 1 by omega, rangeSummary, ih, rangeSummary,
+      combine_assoc]
+    simp [Nat.add_left_comm, Nat.add_comm]
+
+private theorem rangeSummary_eq_unit (row : ℕ → Bool × Bool) {start : ℕ}
+    (h : ∀ i, start ≤ i → row i = (false, true)) (count : ℕ) :
+    rangeSummary row start count = (false, true) := by
+  induction count generalizing start with
+  | zero => rfl
+  | succ count ih =>
+    rw [rangeSummary, h start le_rfl, combine_unit_left, ih]
+    intro i hi
+    exact h i (by omega)
+
+/-- Read one summary from two equal-width rows, using the identity after the row ends. -/
+def readRow {k : ℕ} (row : BitString (k + k)) (i : ℕ) : Bool × Bool :=
+  if h : i < k then (row (Fin.castAdd k ⟨i, h⟩), row (Fin.natAdd k ⟨i, h⟩))
+  else (false, true)
+
+/-- The neighbour at the given distance, or the cell itself if the neighbour is absent. -/
+def neighbour (k distance : ℕ) (i : Fin k) : Fin k :=
+  if h : i.val + distance < k then ⟨i.val + distance, h⟩ else i
+
+/-- The generate output of one prefix cell. Inactive cells use idempotence to retain their value,
+so the scalar circuit has exactly two gates in either branch. -/
+def generateFormula (k distance : ℕ) (i : Fin k) : Formula signature (k + k) :=
+  (Formula.input (Fin.castAdd k i)).or
+    ((Formula.input (Fin.natAdd k i)).and (Formula.input (Fin.castAdd k (neighbour k distance i))))
+
+/-- The propagate output of one prefix cell. -/
+def propagateFormula (k distance : ℕ) (i : Fin k) : Formula signature (k + k) :=
+  (Formula.input (Fin.natAdd k i)).and (Formula.input (Fin.natAdd k (neighbour k distance i)))
+
+/-- One round of parallel carry composition, with all generate bits before all propagate bits. -/
+def step (k distance : ℕ) : Circuit signature (k + k) (k + k) :=
+  (Circuit.pi fun i => (generateFormula k distance i).toCircuit).append
+    (Circuit.pi fun i => (propagateFormula k distance i).toCircuit)
+
+@[simp] theorem size_step (k distance : ℕ) : (step k distance).size = 3 * k := by
+  simp [step, generateFormula, propagateFormula, Formula.size_toCircuit]
+  omega
+
+theorem depth_step_le (k distance : ℕ) : (step k distance).depth ≤ 2 := by
+  apply (Circuit.depth_append_le _ _).trans
+  apply max_le
+  · apply Circuit.depth_pi_le
+    intro i
+    exact (Formula.depth_toCircuit_le _).trans (by simp [generateFormula])
+  · apply Circuit.depth_pi_le
+    intro i
+    exact (Formula.depth_toCircuit_le _).trans (by simp [propagateFormula])
+
+private theorem readRow_step (row : BitString (k + k)) (i distance : ℕ) :
+    readRow ((step k distance).eval interpretation row) i =
+      if i < k then
+        combine (readRow row i) (readRow row (i + distance))
+      else (false, true) := by
+  by_cases hi : i < k
+  · simp only [readRow, hi, ↓reduceDIte, ite_true, step, Circuit.eval_append,
+      Fin.append_left, Fin.append_right, Circuit.eval_pi, Formula.eval_toCircuit,
+      generateFormula, propagateFormula, Formula.eval_or, Formula.eval_and, Formula.eval_input]
+    by_cases hd : i + distance < k
+    · simp [neighbour, hd, combine]
+    · simp only [neighbour, hd, ↓reduceDIte, combine]
+      cases row (Fin.castAdd k ⟨i, hi⟩) <;> cases row (Fin.natAdd k ⟨i, hi⟩) <;> rfl
+  · simp [readRow, hi]
+
+/-- The doubling network on an existing row of carry summaries. -/
+def scan (k : ℕ) : ℕ → Circuit signature (k + k) (k + k)
+  | 0 => Circuit.wiring signature id
+  | t + 1 => (step k (2 ^ t)).comp (scan k t)
+
+@[simp] theorem size_scan (k t : ℕ) : (scan k t).size = 3 * k * t := by
+  induction t with
+  | zero => rfl
+  | succ t ih => simp only [scan, Circuit.size_comp, size_step, ih, Nat.mul_succ]
+
+theorem depth_scan_le (k t : ℕ) : (scan k t).depth ≤ 2 * t := by
+  induction t with
+  | zero => simp [scan]
+  | succ t ih =>
+    exact (Circuit.depth_comp_le _ _).trans
+      ((Nat.add_le_add (depth_step_le _ _) ih).trans (by omega))
+
+/-- After `t` rounds every cell summarizes the next `2^t` original cells, with identity padding. -/
+theorem readRow_scan (row : BitString (k + k)) (t i : ℕ) :
+    readRow ((scan k t).eval interpretation row) i =
+      rangeSummary (readRow row) i (2 ^ t) := by
+  induction t generalizing i with
+  | zero => simp [scan, rangeSummary]
+  | succ t ih =>
+    rw [scan, Circuit.eval_comp, readRow_step]
+    by_cases hi : i < k
+    · rw [ite_eq_left hi, ih, ih, pow_succ, Nat.mul_two, rangeSummary_add]
+    · rw [ite_eq_right hi]
+      symm
+      apply rangeSummary_eq_unit
+      intro j hj
+      simp [readRow, show ¬ j < k by omega]
+
+/-- Input bit `i` of the first word. -/
+def leftInput (w : ℕ) (i : Fin w) : Fin (w + w + 1) :=
+  Fin.castAdd 1 (Fin.castAdd w i)
+
+/-- Input bit `i` of the second word. -/
+def rightInput (w : ℕ) (i : Fin w) : Fin (w + w + 1) :=
+  Fin.castAdd 1 (Fin.natAdd w i)
+
+/-- Generate one reversed input summary; the final cell supplies the incoming carry. -/
+def initialGenerate (w : ℕ) (i : Fin (w + 1)) : Circuit signature (w + w + 1) 1 :=
+  if h : i.val < w then
+    Circuit.oneGate .and ![leftInput w ⟨w - 1 - i.val, by omega⟩,
+      rightInput w ⟨w - 1 - i.val, by omega⟩]
+  else Circuit.oneGate .or ![Fin.last (w + w), Fin.last (w + w)]
+
+/-- Propagate one reversed input summary; the incoming carry is a constant transfer. -/
+def initialPropagate (w : ℕ) (i : Fin (w + 1)) : Circuit signature (w + w + 1) 1 :=
+  if h : i.val < w then
+    Circuit.oneGate .or ![leftInput w ⟨w - 1 - i.val, by omega⟩,
+      rightInput w ⟨w - 1 - i.val, by omega⟩]
+  else Circuit.oneGate (.const false) Fin.elim0
+
+/-- Carry summaries in descending significance, followed by the incoming carry. -/
+def initial (w : ℕ) : Circuit signature (w + w + 1) ((w + 1) + (w + 1)) :=
+  (Circuit.pi (initialGenerate w)).append (Circuit.pi (initialPropagate w))
+
+@[simp] theorem size_initialGenerate (w : ℕ) (i : Fin (w + 1)) :
+    (initialGenerate w i).size = 1 := by unfold initialGenerate; split <;> rfl
+
+@[simp] theorem size_initialPropagate (w : ℕ) (i : Fin (w + 1)) :
+    (initialPropagate w i).size = 1 := by unfold initialPropagate; split <;> rfl
+
+@[simp] theorem size_initial (w : ℕ) : (initial w).size = 2 * (w + 1) := by
+  simp [initial, two_mul]
+
+theorem depth_initial_le (w : ℕ) : (initial w).depth ≤ 1 := by
+  apply (Circuit.depth_append_le _ _).trans
+  apply max_le <;> apply Circuit.depth_pi_le <;> intro i
+  · unfold initialGenerate; split <;> simp
+  · unfold initialPropagate; split <;> simp
+
+/-- The carry network; `w - i` is the generate-wire index of the carry into bit `i`. -/
+def carries (w : ℕ) : Circuit signature (w + w + 1) ((w + 1) + (w + 1)) :=
+  (scan (w + 1) (Nat.clog 2 (w + 1))).comp (initial w)
+
+/-- One sum bit, reading the original inputs followed by the carry network. -/
+def sumFormula (w : ℕ) (i : Fin w) :
+    Formula signature ((w + w + 1) + ((w + 1) + (w + 1))) :=
+  ((Formula.input (Fin.castAdd ((w + 1) + (w + 1)) (leftInput w i))).xor
+    (.input (Fin.castAdd ((w + 1) + (w + 1)) (rightInput w i)))).xor
+    (.input (Fin.natAdd (w + w + 1) ⟨w - i.val, by omega⟩))
+
+/-- Convert carry summaries to sum bits and retain the final carry as the last output. -/
+def finish (w : ℕ) :
+    Circuit signature ((w + w + 1) + ((w + 1) + (w + 1))) (w + 1) :=
+  (Circuit.pi fun i => (sumFormula w i).toCircuit).append
+    (Circuit.wiring signature fun _ : Fin 1 => Fin.natAdd (w + w + 1) ⟨0, by omega⟩)
+
+@[simp] theorem size_sumFormula (w : ℕ) (i : Fin w) : (sumFormula w i).size = 15 := by
+  simp [sumFormula]
+
+@[simp] theorem size_finish (w : ℕ) : (finish w).size = 15 * w := by
+  simp [finish, Nat.mul_comm]
+
+theorem depth_finish_le (w : ℕ) : (finish w).depth ≤ 6 := by
+  apply (Circuit.depth_append_le _ _).trans
+  apply max_le
+  · apply Circuit.depth_pi_le
+    intro i
+    apply (Formula.depth_toCircuit_le _).trans
+    apply (Formula.depth_xor_le _ _).trans
+    have h := Formula.depth_xor_le
+      (Formula.input (σ := signature)
+        (Fin.castAdd ((w + 1) + (w + 1)) (leftInput w i)))
+      (Formula.input (Fin.castAdd ((w + 1) + (w + 1)) (rightInput w i)))
+    simp only [Formula.depth_input] at h ⊢
+    omega
+  · simp
+
+/-- The arithmetic carry into bit `i`, used only as the specification. -/
+def inputCarry {w : ℕ} (u : BitString (w + w + 1)) (i : ℕ) : Bool :=
+  BitVec.carry i (word (u ∘ leftInput w)) (word (u ∘ rightInput w)) (u (Fin.last (w + w)))
+
+private theorem readRow_initial {w : ℕ} (u : BitString (w + w + 1)) (i : Fin (w + 1)) :
+    readRow ((initial w).eval interpretation u) i.val =
+      if h : i.val < w then
+        (u (leftInput w ⟨w - 1 - i.val, by omega⟩) &&
+          u (rightInput w ⟨w - 1 - i.val, by omega⟩),
+         u (leftInput w ⟨w - 1 - i.val, by omega⟩) ||
+          u (rightInput w ⟨w - 1 - i.val, by omega⟩))
+      else (u (Fin.last (w + w)), false) := by
+  simp only [readRow, i.isLt, ↓reduceDIte, initial, Circuit.eval_append, Fin.append_left,
+    Fin.append_right, Circuit.eval_pi, initialGenerate, initialPropagate]
+  split <;> simp [Circuit.eval_oneGate, interpretation]
+
+private theorem rangeSummary_initial {w : ℕ} (u : BitString (w + w + 1)) (i : ℕ)
+    (hi : i ≤ w) :
+    rangeSummary (readRow ((initial w).eval interpretation u)) (w - i) (i + 1) =
+      (inputCarry u i, false) := by
+  induction i with
+  | zero =>
+    rw [rangeSummary, rangeSummary, combine_unit_right]
+    simpa [inputCarry] using readRow_initial u (Fin.last w)
+  | succ i ih =>
+    rw [rangeSummary]
+    have hs : w - (i + 1) + 1 = w - i := by omega
+    rw [hs, ih (by omega)]
+    have hr := readRow_initial u ⟨w - (i + 1), by omega⟩
+    have hj : w - (i + 1) < w := by omega
+    have hidx : w - 1 - (w - (i + 1)) = i := by omega
+    simp only [hj, ↓reduceDIte, hidx] at hr
+    rw [hr]
+    simp only [combine, Bool.and_false, inputCarry, BitVec.carry_succ,
+      getLsbD_word (u ∘ leftInput w) ⟨i, by omega⟩,
+      getLsbD_word (u ∘ rightInput w) ⟨i, by omega⟩, Function.comp_apply]
+    cases u (leftInput w ⟨i, by omega⟩) <;>
+      cases u (rightInput w ⟨i, by omega⟩) <;>
+      cases BitVec.carry i (word (u ∘ leftInput w)) (word (u ∘ rightInput w))
+        (u (Fin.last (w + w))) <;> rfl
+
+/-- The generate output at reversed index `w-i` is exactly carry `i`, including both endpoints. -/
+theorem eval_carries {w : ℕ} (u : BitString (w + w + 1)) (i : Fin (w + 1)) :
+    (carries w).eval interpretation u ⟨w - i.val, by omega⟩ = inputCarry u i.val := by
+  have hpow : w + 1 ≤ 2 ^ Nat.clog 2 (w + 1) := Nat.le_pow_clog (by decide) _
+  have h := readRow_scan ((initial w).eval interpretation u) (Nat.clog 2 (w + 1)) (w - i.val)
+  have he : 2 ^ Nat.clog 2 (w + 1) = (i.val + 1) +
+      (2 ^ Nat.clog 2 (w + 1) - (i.val + 1)) := by omega
+  rw [he, rangeSummary_add, rangeSummary_initial u i.val (by omega)] at h
+  have hz : rangeSummary (readRow ((initial w).eval interpretation u))
+      (w - i.val + (i.val + 1)) (2 ^ Nat.clog 2 (w + 1) - (i.val + 1)) = (false, true) := by
+    apply rangeSummary_eq_unit
+    intro j hj
+    simp [readRow, show ¬j < w + 1 by omega]
+  rw [hz, combine_unit_right] at h
+  have hg := congrArg Prod.fst h
+  simpa [readRow, show w - i.val < w + 1 by omega, carries, Circuit.eval_comp] using hg
+
+end CarryLookahead
+
+/-- Add two unsigned words and an input carry. Inputs are the first word, the second word, then
+one carry bit. Outputs are the low `w` sum bits followed by the output carry. -/
+def carryLookahead (w : ℕ) : Circuit signature (w + w + 1) (w + 1) :=
+  (CarryLookahead.finish w).comp
+    ((Circuit.wiring signature id).append (CarryLookahead.carries w))
+
+/-- The exact number of gates in the doubling adder. -/
+theorem size_carryLookahead (w : ℕ) :
+    (carryLookahead w).size = 15 * w + 2 * (w + 1) +
+      3 * (w + 1) * Nat.clog 2 (w + 1) := by
+  simp [carryLookahead, CarryLookahead.carries, Nat.add_assoc, Nat.add_left_comm, Nat.add_comm]
+
+/-- Every gate has fan-in at most two, and the adder has logarithmic depth. -/
+theorem depth_carryLookahead_le (w : ℕ) :
+    (carryLookahead w).depth ≤ 7 + 2 * Nat.clog 2 (w + 1) := by
+  apply (Circuit.depth_comp_le _ _).trans
+  have h₁ := Circuit.depth_append_le (Circuit.wiring signature id) (CarryLookahead.carries w)
+  have h₂ := Circuit.depth_comp_le
+    (CarryLookahead.scan (w + 1) (Nat.clog 2 (w + 1))) (CarryLookahead.initial w)
+  have h₃ := CarryLookahead.depth_scan_le (w + 1) (Nat.clog 2 (w + 1))
+  have h₄ := CarryLookahead.depth_initial_le w
+  have h₅ := CarryLookahead.depth_finish_le w
+  simp only [Circuit.depth_wiring, zero_max] at h₁
+  change (CarryLookahead.carries w).depth ≤ _ at h₂
+  omega
+
+/-- An explicit absolute-constant logarithmic depth bound, including width zero. -/
+theorem depth_carryLookahead_le_log (w : ℕ) :
+    (carryLookahead w).depth ≤ 7 * (Nat.clog 2 (w + 1) + 1) := by
+  have := depth_carryLookahead_le w
+  omega
+
+/-- A coarse polynomial bound on the complete adder's number of gates. -/
+theorem size_carryLookahead_le (w : ℕ) :
+    (carryLookahead w).size ≤ 20 * (w + 1) ^ 2 := by
+  have hlog : Nat.clog 2 (w + 1) ≤ w + 1 :=
+    Nat.clog_le_of_le_pow (Nat.le_of_lt (Nat.lt_pow_self (by decide)))
+  rw [size_carryLookahead]
+  nlinarith [Nat.mul_le_mul_left (3 * (w + 1)) hlog]
+
+/-- Each low output bit is the sum bit with the specified incoming carry. -/
+theorem eval_carryLookahead_sum {w : ℕ} (u : BitString (w + w + 1)) (i : Fin w) :
+    (carryLookahead w).eval interpretation u i.castSucc =
+      (word (u ∘ CarryLookahead.leftInput w) + word (u ∘ CarryLookahead.rightInput w) +
+        BitVec.setWidth w (BitVec.ofBool (u (Fin.last (w + w))))).getLsbD i.val := by
+  simp only [carryLookahead, Circuit.eval_comp, CarryLookahead.finish, Circuit.eval_append,
+    show i.castSucc = Fin.castAdd 1 i from rfl, Fin.append_left, Circuit.eval_pi,
+    Formula.eval_toCircuit, CarryLookahead.sumFormula, Formula.eval_xor, Formula.eval_input,
+    Circuit.eval_wiring, Function.comp_apply, Fin.append_right]
+  rw [CarryLookahead.eval_carries u ⟨i.val, by omega⟩]
+  rw [BitVec.getLsbD_add_add_bool i.isLt,
+    getLsbD_word (u ∘ CarryLookahead.leftInput w) i,
+    getLsbD_word (u ∘ CarryLookahead.rightInput w) i]
+  exact Bool.xor_assoc _ _ _
+
+/-- The last output is the final carry, also at width zero. -/
+theorem eval_carryLookahead_carry {w : ℕ} (u : BitString (w + w + 1)) :
+    (carryLookahead w).eval interpretation u (Fin.last w) = CarryLookahead.inputCarry u w := by
+  change (carryLookahead w).eval interpretation u (Fin.natAdd w 0) = _
+  simp only [carryLookahead, Circuit.eval_comp, CarryLookahead.finish, Circuit.eval_append,
+    Fin.append_right, Circuit.eval_wiring, Function.comp_apply]
+  simpa using CarryLookahead.eval_carries u (Fin.last w)
+
+/-- Exact unsigned addition, including the output carry. -/
+theorem val_eval_carryLookahead {w : ℕ} (a b : BitString w) (c : Bool) :
+    (BitString.equivFin (w + 1)
+      ((carryLookahead w).eval interpretation (Fin.append (Fin.append a b) (fun _ => c))) : ℕ) =
+        (BitString.equivFin w a : ℕ) + (BitString.equivFin w b : ℕ) + c.toNat := by
+  let u := Fin.append (Fin.append a b) (fun _ : Fin 1 => c)
+  have hl : u ∘ CarryLookahead.leftInput w = a := by
+    ext i
+    simp only [u, Function.comp_apply, CarryLookahead.leftInput, Fin.append_left]
+  have hr : u ∘ CarryLookahead.rightInput w = b := by
+    ext i
+    simp only [u, Function.comp_apply, CarryLookahead.rightInput, Fin.append_left, Fin.append_right]
+  have hc : u (Fin.last (w + w)) = c := Fin.append_right _ _ 0
+  have hs : word (Fin.init ((carryLookahead w).eval interpretation u)) =
+      word a + word b + BitVec.setWidth w (BitVec.ofBool c) := by
+    apply BitVec.eq_of_getLsbD_eq
+    intro i hi
+    rw [getLsbD_word _ ⟨i, hi⟩]
+    simpa only [Fin.init, hl, hr, hc] using eval_carryLookahead_sum u ⟨i, hi⟩
+  have hout := eval_carryLookahead_carry u
+  simp only [CarryLookahead.inputCarry, hl, hr, hc, BitVec.carry_width] at hout
+  change (BitString.equivFin (w + 1) ((carryLookahead w).eval interpretation u) : ℕ) = _
+  rw [BitString.val_equivFin_succ, ← toNat_word_eq_equivFin, hs, hout]
+  simp only [BitVec.toNat_add, BitVec.toNat_setWidth, BitVec.toNat_ofBool,
+    Nat.mod_add_mod, Nat.add_mod_mod, toNat_word_eq_equivFin]
+  have ha := (BitString.equivFin w a).isLt
+  have hb := (BitString.equivFin w b).isLt
+  have hcb := Bool.toNat_le c
+  by_cases h : (BitString.equivFin w a : ℕ) + (BitString.equivFin w b : ℕ) + c.toNat ≥ 2 ^ w
+  · simp only [h, decide_true, Bool.toNat_true, one_mul]
+    rw [Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt (by omega)]
+    omega
+  · simp only [h, decide_false, Bool.toNat_false, zero_mul, Nat.add_zero]
+    exact Nat.mod_eq_of_lt (by omega)
+
+/-- Discard the final carry and hardwire a false incoming carry. -/
+def carryLookaheadAdd (w : ℕ) : Circuit signature (w + w) w :=
+  (Circuit.wiring signature (fun i : Fin w => i.castSucc)).comp
+    ((carryLookahead w).comp
+      ((Circuit.wiring signature id).append (Circuit.oneGate (.const false) Fin.elim0)))
+
+/-- The modular result used to collapse a carry-save pair. -/
+theorem val_eval_carryLookaheadAdd {w : ℕ} (a b : BitString w) :
+    (BitString.equivFin w ((carryLookaheadAdd w).eval interpretation (Fin.append a b)) : ℕ) =
+      ((BitString.equivFin w a : ℕ) + (BitString.equivFin w b : ℕ)) % 2 ^ w := by
+  have h := val_eval_carryLookahead a b false
+  rw [BitString.val_equivFin_succ] at h
+  simp only [Bool.toNat_false, Nat.add_zero] at h
+  have hm := congrArg (· % 2 ^ w) h
+  rw [Nat.add_mul_mod_self_right] at hm
+  have he : (carryLookaheadAdd w).eval interpretation (Fin.append a b) =
+      Fin.init ((carryLookahead w).eval interpretation
+        (Fin.append (Fin.append a b) (fun _ => false))) := by
+    simp only [carryLookaheadAdd, Circuit.eval_comp, Circuit.eval_append, Circuit.eval_wiring]
+    rfl
+  rw [he]
+  exact (Nat.mod_eq_of_lt (BitString.equivFin w _).isLt).symm.trans hm
+
+@[simp] theorem size_carryLookaheadAdd (w : ℕ) :
+    (carryLookaheadAdd w).size = (carryLookahead w).size + 1 := by
+  simp [carryLookaheadAdd, Nat.add_comm]
+
+theorem depth_carryLookaheadAdd_le (w : ℕ) :
+    (carryLookaheadAdd w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1) := by
+  have h₁ := Circuit.depth_comp_le (carryLookahead w)
+    ((Circuit.wiring signature id).append (Circuit.oneGate (.const false) Fin.elim0))
+  have h₂ := Circuit.depth_append_le (Circuit.wiring signature id)
+    (Circuit.oneGate (σ := signature) (n := w + w) (.const false) Fin.elim0)
+  have h₃ := depth_carryLookahead_le w
+  apply (Circuit.depth_comp_le _ _).trans
+  simp only [Circuit.depth_wiring, zero_add]
+  simp only [Circuit.depth_wiring, Circuit.depth_oneGate, zero_max] at h₂
+  omega
+
+/-- An explicit absolute-constant depth bound for modular addition. -/
+theorem depth_carryLookaheadAdd_le_log (w : ℕ) :
+    (carryLookaheadAdd w).depth ≤ 8 * (Nat.clog 2 (w + 1) + 1) := by
+  have := depth_carryLookaheadAdd_le w
+  omega
+
+/-- Polynomial size after fixing the incoming carry and selecting the modular result. -/
+theorem size_carryLookaheadAdd_le (w : ℕ) :
+    (carryLookaheadAdd w).size ≤ 21 * (w + 1) ^ 2 := by
+  rw [size_carryLookaheadAdd]
+  have := size_carryLookahead_le w
+  have : 0 < (w + 1) ^ 2 := by positivity
+  omega
+
+/-- A drop-in carry-save finisher: the first word is the modular sum and the second is zero. -/
+def carryLookaheadFinish (w : ℕ) : Circuit signature (w + w) (w + w) :=
+  (carryLookaheadAdd w).append
+    ((Circuit.wiring signature (fun _ : Fin w => (0 : Fin 1))).comp
+      (Circuit.oneGate (.const false) Fin.elim0))
+
+/-- Only one extra constant gate is needed to clear the second carry-save word. -/
+@[simp] theorem size_carryLookaheadFinish (w : ℕ) :
+    (carryLookaheadFinish w).size = (carryLookaheadAdd w).size + 1 := by
+  simp [carryLookaheadFinish]
+
+/-- The carry-save finisher has logarithmic depth in the word width. -/
+theorem depth_carryLookaheadFinish_le (w : ℕ) :
+    (carryLookaheadFinish w).depth ≤ 8 + 2 * Nat.clog 2 (w + 1) := by
+  apply (Circuit.depth_append_le _ _).trans
+  apply max_le (depth_carryLookaheadAdd_le w)
+  apply (Circuit.depth_comp_le _ _).trans
+  simp only [Circuit.depth_wiring, Circuit.depth_oneGate]
+  omega
+
+/-- A polynomial gate bound for the drop-in carry-save finisher. -/
+theorem size_carryLookaheadFinish_le (w : ℕ) :
+    (carryLookaheadFinish w).size ≤ 22 * (w + 1) ^ 2 := by
+  rw [size_carryLookaheadFinish]
+  have := size_carryLookaheadAdd_le w
+  have : 0 < (w + 1) ^ 2 := by positivity
+  omega
+
+/-- The replacement finishing stage preserves every carry-save value modulo `2^w`. -/
+theorem pairVal_eval_carryLookaheadFinish_mod {w : ℕ} (p : BitString (w + w)) :
+    pairVal ((carryLookaheadFinish w).eval interpretation p) % 2 ^ w = pairVal p % 2 ^ w := by
+  have hp : Fin.append (BitString.fstBits p) (BitString.sndBits p) = p := by
+    ext i
+    induction i using Fin.addCases <;>
+      simp only [BitString.fstBits, BitString.sndBits, Fin.append_left, Fin.append_right,
+        Function.comp_apply]
+  have h := val_eval_carryLookaheadAdd (BitString.fstBits p) (BitString.sndBits p)
+  rw [hp] at h
+  simp only [carryLookaheadFinish, Circuit.eval_append, Circuit.eval_comp, Circuit.eval_wiring]
+  change pairVal (Fin.append ((carryLookaheadAdd w).eval interpretation p) (fun _ => false)) %
+    2 ^ w = _
+  rw [pairVal_append, BitString.val_equivFin_false, Nat.add_zero, h, Nat.mod_mod]
+  rfl
+
+/-- Every bit of the second output word is false after the logarithmic-depth finisher. -/
+theorem sndBits_eval_carryLookaheadFinish {w : ℕ} (p : BitString (w + w)) :
+    BitString.sndBits ((carryLookaheadFinish w).eval interpretation p) = fun _ => false := by
+  simp only [carryLookaheadFinish, Circuit.eval_append, Circuit.eval_comp, Circuit.eval_wiring,
+    BitString.sndBits_append]
+  rfl
+
+/-- A 4-to-2 carry-save reduction followed by the new finisher computes the same modular sum.
+The existing carry-save circuit is unchanged. -/
+theorem pairVal_eval_carryLookaheadFinish_csa4to2_mod {w : ℕ}
+    (p q : BitString (w + w)) :
+    pairVal (((carryLookaheadFinish w).comp (csa4to2 w)).eval interpretation
+      (Fin.append p q)) % 2 ^ w = (pairVal p + pairVal q) % 2 ^ w := by
+  rw [Circuit.eval_comp, pairVal_eval_carryLookaheadFinish_mod,
+    pairVal_eval_csa4to2_mod]
+
+/-- Finishing a 4-to-2 reduction adds only a constant to the logarithmic depth bound. -/
+theorem depth_carryLookaheadFinish_comp_csa4to2_le (w : ℕ) :
+    ((carryLookaheadFinish w).comp (csa4to2 w)).depth ≤
+      20 + 2 * Nat.clog 2 (w + 1) := by
+  have := Circuit.depth_comp_le (carryLookaheadFinish w) (csa4to2 w)
+  have := depth_carryLookaheadFinish_le w
+  have := depth_csa4to2_le w
+  omega
+
+end Cslib.Circuits.Boolean
diff --git a/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean b/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean
new file mode 100644
index 000000000..df5807f5c
--- /dev/null
+++ b/Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean
@@ -0,0 +1,450 @@
+/-
+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.Circuit.Boolean.CarryLookahead
+public import Complexity.Computability.Circuit.Boolean.CodeTemplate
+import Complexity.Computability.Circuit.Boolean.EncodingSize
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Iteration
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log
+
+/-!
+# Native generation of carry-lookahead circuit codes
+
+All constructors return the actual binary gate-and-output encoding. Widths and loop counts are
+unary; distances and wire references are binary. The prefix loop carries its already generated
+code and appends one fixed-width round at a time. Bounds on the complete intermediate encoding
+justify the loop, including tags, delimiters and output references.
+
+## Main definitions
+
+* `Cslib.Circuits.Boolean.CarryLookahead.stepCode`: one round on raw parameters.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.CarryLookahead.stepCode_eq`: agreement with the typed round.
+* `Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookahead`: native generation of
+  the complete adder code from unary width.
+* `Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadAdd`,
+  `computableTidilyInPolyTime_carryLookaheadFinish`: the modular and carry-save finishing codes.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Boolean
+
+namespace CarryLookahead
+
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+/-- The total raw neighbour rule used by the doubling layer. -/
+def neighbourIndex (k distance i : ℕ) : ℕ := if i + distance < k then i + distance else i
+
+private def generateTemplate : Formula signature 3 :=
+  (Formula.input 0).or ((Formula.input 1).and (.input 2))
+
+private def propagateTemplate : Formula signature 2 :=
+  (Formula.input 0).and (.input 1)
+
+/-- The generate cell's full code, also defined on out-of-range raw coordinates. -/
+def generateCode (k distance i : ℕ) : List (Op × List ℕ) × List ℕ :=
+  formulaCode (k + k) ((Formula.input (n := 3) 0).or ((Formula.input 1).and (.input 2)))
+    ![i, k + i, neighbourIndex k distance i]
+
+/-- The propagate cell's full code. -/
+def propagateCode (k distance i : ℕ) : List (Op × List ℕ) × List ℕ :=
+  formulaCode (k + k) ((Formula.input (n := 2) 0).and (.input 1))
+    ![k + i, k + neighbourIndex k distance i]
+
+private theorem generateCode_eq (k distance : ℕ) (i : Fin k) :
+    generateCode k distance i.val = (generateFormula k distance i).toCircuit.code := by
+  let wires : Fin 3 → Fin (k + k) :=
+    ![Fin.castAdd k i, Fin.natAdd k i, Fin.castAdd k (neighbour k distance i)]
+  have hw : (fun j => (wires j).val) = ![i.val, k + i.val, neighbourIndex k distance i.val] := by
+    funext j
+    by_cases h : distance + i.val < k <;>
+      fin_cases j <;> simp [wires, neighbour, neighbourIndex, h, Nat.add_comm]
+  have h := formulaCode_eq_code generateTemplate wires
+  rw [hw] at h
+  exact h
+
+private theorem propagateCode_eq (k distance : ℕ) (i : Fin k) :
+    propagateCode k distance i.val = (propagateFormula k distance i).toCircuit.code := by
+  let wires : Fin 2 → Fin (k + k) := ![Fin.natAdd k i, Fin.natAdd k (neighbour k distance i)]
+  have hw : (fun j => (wires j).val) = ![k + i.val, k + neighbourIndex k distance i.val] := by
+    funext j
+    by_cases h : distance + i.val < k <;>
+      fin_cases j <;> simp [wires, neighbour, neighbourIndex, h, Nat.add_comm]
+  have h := formulaCode_eq_code propagateTemplate wires
+  rw [hw] at h
+  exact h
+
+private theorem generateCode_polyTime {α : Type} {enc : α ↪ List Bool}
+    {k distance i : α → ℕ} (hk : ComputableTidilyInPolyTime k enc encNat)
+    (hd : ComputableTidilyInPolyTime distance enc encNat)
+    (hi : ComputableTidilyInPolyTime i enc encNat) :
+    ComputableTidilyInPolyTime (fun a => generateCode (k a) (distance a) (i a)) enc encCode := by
+  apply computableTidilyInPolyTime_formulaCode _ (by fun_prop)
+  intro j
+  fin_cases j
+  · exact hi
+  · change ComputableTidilyInPolyTime (fun a => k a + i a) enc encNat
+    fun_prop
+  · change ComputableTidilyInPolyTime (fun a => neighbourIndex (k a) (distance a) (i a)) enc encNat
+    unfold neighbourIndex
+    fun_prop
+
+private theorem propagateCode_polyTime {α : Type} {enc : α ↪ List Bool}
+    {k distance i : α → ℕ} (hk : ComputableTidilyInPolyTime k enc encNat)
+    (hd : ComputableTidilyInPolyTime distance enc encNat)
+    (hi : ComputableTidilyInPolyTime i enc encNat) :
+    ComputableTidilyInPolyTime (fun a => propagateCode (k a) (distance a) (i a)) enc encCode := by
+  apply computableTidilyInPolyTime_formulaCode _ (by fun_prop)
+  intro j
+  fin_cases j
+  · change ComputableTidilyInPolyTime (fun a => k a + i a) enc encNat
+    fun_prop
+  · change ComputableTidilyInPolyTime
+      (fun a => k a + neighbourIndex (k a) (distance a) (i a)) enc encNat
+    unfold neighbourIndex
+    fun_prop
+
+/-- Bundle the fixed-size generate and propagate blocks of one doubling round. -/
+def stepCode (k distance : ℕ) : List (Op × List ℕ) × List ℕ :=
+  appendCode (k + k)
+    (bundleCode (k + k) 2 ((List.range k).map (generateCode k distance)))
+    (bundleCode (k + k) 1 ((List.range k).map (propagateCode k distance)))
+
+/-- The raw round is exactly the typed circuit's code, with no malformed-input assumption. -/
+theorem stepCode_eq (k distance : ℕ) : stepCode k distance = (step k distance).code := by
+  have hg : (List.range k).map (generateCode k distance) =
+      List.ofFn (fun i : Fin k => (generateFormula k distance i).toCircuit.code) := by
+    apply List.ext_getElem (by simp)
+    intro i hi hj
+    simpa using generateCode_eq k distance ⟨i, by simpa using hi⟩
+  have hp : (List.range k).map (propagateCode k distance) =
+      List.ofFn (fun i : Fin k => (propagateFormula k distance i).toCircuit.code) := by
+    apply List.ext_getElem (by simp)
+    intro i hi hj
+    simpa using propagateCode_eq k distance ⟨i, by simpa using hi⟩
+  rw [stepCode, hg, hp, bundleCode_code _ _ (by intro i; simp [generateFormula]),
+    bundleCode_code _ _ (by intro i; simp [propagateFormula]), appendCode_code]
+  rfl
+
+/-- A doubling round is generated uniformly from a unary width and a binary distance. -/
+theorem computableTidilyInPolyTime_stepCode {α : Type} {enc : α ↪ List Bool}
+    {k distance : α → ℕ} (hk : ComputableTidilyInPolyTime k enc encUnary)
+    (hd : ComputableTidilyInPolyTime distance enc encNat) :
+    ComputableTidilyInPolyTime (fun a => stepCode (k a) (distance a)) enc encCode := by
+  have hk' := unary_to_binary.comp hk
+  have hn : ComputableTidilyInPolyTime (fun a => k a + k a) enc encNat := by fun_prop
+  have hg : ComputableTidilyInPolyTime
+      (fun p : α × ℕ => generateCode (k p.1) (distance p.1) p.2)
+      (encPair enc encUnary) encCode :=
+    generateCode_polyTime (hk'.comp (fst _ _)) (hd.comp (fst _ _))
+      (unary_to_binary.comp (snd _ _))
+  have hp : ComputableTidilyInPolyTime
+      (fun p : α × ℕ => propagateCode (k p.1) (distance p.1) p.2)
+      (encPair enc encUnary) encCode :=
+    propagateCode_polyTime (hk'.comp (fst _ _)) (hd.comp (fst _ _))
+      (unary_to_binary.comp (snd _ _))
+  exact computableTidilyInPolyTime_appendCode hn
+    (computableTidilyInPolyTime_bundleCode hn (const 2) (mapWith hg id' (range.comp hk)))
+    (computableTidilyInPolyTime_bundleCode hn (const 1) (mapWith hp id' (range.comp hk)))
+
+private theorem code_wiring_id (k : ℕ) :
+    (Circuit.wiring signature (id : Fin k → Fin k)).code = ([], List.range k) := by
+  apply Prod.ext
+  · rfl
+  change List.ofFn (fun i : Fin k => i.val) = List.range k
+  apply List.ext_getElem (by simp)
+  intro i hi hj
+  simp
+
+/-- Generate any number of doubling rounds from unary width and round count. The native loop
+keeps the accumulated code and unary round counter, with polynomial intermediate encoded length. -/
+theorem computableTidilyInPolyTime_scan :
+    ComputableTidilyInPolyTime (fun p : ℕ × ℕ => (scan p.1 p.2).code)
+      (encPair encUnary encUnary) encCode := by
+  let stateEnc := encPair encUnary encCode
+  let init (k : ℕ) : ℕ × (List (Op × List ℕ) × List ℕ) := (0, ([], List.range (k + k)))
+  let next (k : ℕ) (state : ℕ × (List (Op × List ℕ) × List ℕ)) :=
+    (state.1 + 1, compCode (k + k) (stepCode k (2 ^ state.1)) state.2)
+  have hn : ComputableTidilyInPolyTime
+      (fun p : ℕ × (ℕ × (List (Op × List ℕ) × List ℕ)) => next p.1 p.2)
+      (encPair encUnary stateEnc) stateEnc := by
+    have hk := fst encUnary stateEnc
+    have ht := (snd encUnary stateEnc).fst'
+    have hc := (snd encUnary stateEnc).snd'
+    have hd := binary_two_pow.comp ht
+    have hk' := unary_to_binary.comp hk
+    have ht' : ComputableTidilyInPolyTime
+        (fun p : ℕ × (ℕ × (List (Op × List ℕ) × List ℕ)) => p.2.1 + 1)
+        (encPair encUnary stateEnc) encUnary := by fun_prop
+    exact ht'.prod (computableTidilyInPolyTime_compCode
+      (by fun_prop) (computableTidilyInPolyTime_stepCode hk hd) hc)
+  have hi : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => init p.1)
+      (encPair encUnary encUnary) stateEnc := by
+    have hr := unary_to_binary.map.comp
+      (range.comp (show ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 + p.1)
+        (encPair encUnary encUnary) encUnary from by fun_prop))
+    simpa only [Function.comp_def, List.map_id_fun', id_eq, init] using
+      (const (encMid := encUnary) 0).prod ((const (encMid := encList encGate) []).prod hr)
+  have heq (k t : ℕ) : (next k)^[t] (init k) = (t, (scan k t).code) := by
+    induction t with
+    | zero => simp [init, scan, code_wiring_id]
+    | succ t ih =>
+      rw [Function.iterate_succ_apply' (f := next k), ih]
+      simp only [next, stepCode_eq, compCode_code, scan]
+  let bound (p : ℕ × ℕ) := 2 * p.2 + 1 +
+    (2 * (3 * p.1 * p.2) * (23 + 8 * ((p.1 + p.1) + 3 * p.1 * p.2)) + 1 +
+      (p.1 + p.1) * (2 * ((p.1 + p.1) + 3 * p.1 * p.2) + 1))
+  have hb : PolyBounded (fun p : ℕ × ℕ => (encPair encUnary encUnary p).length) bound :=
+    polyBounded (by unfold bound; fun_prop)
+  have h := iterateWith (par := Prod.fst) (count := Prod.snd) (init := fun p => init p.1)
+    (step := next) (fst _ _) (snd _ _) hi hn hb (fun p i hit => by
+      rw [heq]
+      have hsize : (scan p.1 i).size ≤ 3 * p.1 * p.2 := by
+        rw [size_scan]
+        exact Nat.mul_le_mul_left _ hit
+      have hcode := length_encCode_le (scan p.1 i)
+      have hbound : (encCode (scan p.1 i).code).length ≤
+          2 * (3 * p.1 * p.2) * (23 + 8 * ((p.1 + p.1) + 3 * p.1 * p.2)) + 1 +
+            (p.1 + p.1) * (2 * ((p.1 + p.1) + 3 * p.1 * p.2) + 1) :=
+        hcode.trans (by gcongr)
+      change (encPair encUnary encCode (i, (scan p.1 i).code)).length ≤ _
+      rw [length_encPair]
+      simp only [encUnary_apply, List.length_replicate]
+      dsimp only [bound]
+      omega)
+  simpa only [Function.comp_def, heq] using h.snd'
+
+/-- The generate gate of an initial cell, expressed as raw circuit data. -/
+def initialGenerateCode (w i : ℕ) : List (Op × List ℕ) × List ℕ :=
+  if i < w then ([(.and, [w - 1 - i, w + (w - 1 - i)])], [w + w + 1])
+  else ([(.or, [w + w, w + w])], [w + w + 1])
+
+/-- The propagate gate of an initial cell, expressed as raw circuit data. -/
+def initialPropagateCode (w i : ℕ) : List (Op × List ℕ) × List ℕ :=
+  if i < w then ([(.or, [w - 1 - i, w + (w - 1 - i)])], [w + w + 1])
+  else ([(.const false, [])], [w + w + 1])
+
+private theorem initialGenerateCode_eq (w : ℕ) (i : Fin (w + 1)) :
+    initialGenerateCode w i.val = (initialGenerate w i).code := by
+  unfold initialGenerateCode initialGenerate
+  split <;> rfl
+
+private theorem initialPropagateCode_eq (w : ℕ) (i : Fin (w + 1)) :
+    initialPropagateCode w i.val = (initialPropagate w i).code := by
+  unfold initialPropagateCode initialPropagate
+  split <;> rfl
+
+/-- The whole initial row, with one gate per generate or propagate cell. -/
+def initialCode (w : ℕ) : List (Op × List ℕ) × List ℕ :=
+  appendCode (w + w + 1)
+    (bundleCode (w + w + 1) 1 ((List.range (w + 1)).map (initialGenerateCode w)))
+    (bundleCode (w + w + 1) 1 ((List.range (w + 1)).map (initialPropagateCode w)))
+
+private theorem initialCode_eq (w : ℕ) : initialCode w = (initial w).code := by
+  have hg : (List.range (w + 1)).map (initialGenerateCode w) =
+      List.ofFn (fun i : Fin (w + 1) => (initialGenerate w i).code) := by
+    apply List.ext_getElem (by simp)
+    intro i hi hj
+    simpa only [List.getElem_map, List.getElem_range, List.getElem_ofFn] using
+      initialGenerateCode_eq w ⟨i, by simpa using hi⟩
+  have hp : (List.range (w + 1)).map (initialPropagateCode w) =
+      List.ofFn (fun i : Fin (w + 1) => (initialPropagate w i).code) := by
+    apply List.ext_getElem (by simp)
+    intro i hi hj
+    simpa only [List.getElem_map, List.getElem_range, List.getElem_ofFn] using
+      initialPropagateCode_eq w ⟨i, by simpa using hi⟩
+  rw [initialCode, hg, hp, bundleCode_code _ _ (size_initialGenerate w),
+    bundleCode_code _ _ (size_initialPropagate w), appendCode_code]
+  rfl
+
+/-- Native generation of the complete initial carry row from unary width. -/
+theorem computableTidilyInPolyTime_initial :
+    ComputableTidilyInPolyTime (fun w => (initial w).code) encUnary encCode := by
+  have hw : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1)
+      (encPair encUnary encUnary) encNat := unary_to_binary.comp (fst _ _)
+  have hi : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.2)
+      (encPair encUnary encUnary) encNat := unary_to_binary.comp (snd _ _)
+  have hg : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => initialGenerateCode p.1 p.2)
+      (encPair encUnary encUnary) encCode := by unfold initialGenerateCode; fun_prop
+  have hp : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => initialPropagateCode p.1 p.2)
+      (encPair encUnary encUnary) encCode := by unfold initialPropagateCode; fun_prop
+  have hn : ComputableTidilyInPolyTime (fun w : ℕ => w + w + 1) encUnary encNat := by
+    have h := unary_to_binary
+    fun_prop
+  have hr : ComputableTidilyInPolyTime (fun w : ℕ => List.range (w + 1))
+      encUnary (encList encUnary) := by fun_prop
+  have h := computableTidilyInPolyTime_appendCode hn
+    (computableTidilyInPolyTime_bundleCode hn (const 1) (mapWith hg id' hr))
+    (computableTidilyInPolyTime_bundleCode hn (const 1) (mapWith hp id' hr))
+  simpa only [← initialCode_eq, initialCode] using h
+
+/-- Native generation of all the input carries from unary word width. -/
+theorem computableTidilyInPolyTime_carries :
+    ComputableTidilyInPolyTime (fun w => (carries w).code) encUnary encCode := by
+  have hw : ComputableTidilyInPolyTime (fun w : ℕ => w + 1) encUnary encUnary := by fun_prop
+  have ht := (unary_clog_const 2).comp hw
+  have hs := computableTidilyInPolyTime_scan.comp (hw.prod ht)
+  have hn : ComputableTidilyInPolyTime (fun w : ℕ => w + w + 1) encUnary encNat := by
+    have h := unary_to_binary
+    fun_prop
+  simpa only [Function.comp_def, compCode_code, carries] using
+    computableTidilyInPolyTime_compCode hn hs computableTidilyInPolyTime_initial
+
+private def sumTemplate : Formula signature 3 :=
+  ((Formula.input 0).xor (.input 1)).xor (.input 2)
+
+/-- The sum cell's raw code, using the original inputs and the reversed carry row. -/
+def sumCode (w i : ℕ) : List (Op × List ℕ) × List ℕ :=
+  formulaCode ((w + w + 1) + ((w + 1) + (w + 1)))
+    (((Formula.input (n := 3) 0).xor (.input 1)).xor (.input 2))
+    ![i, w + i, (w + w + 1) + (w - i)]
+
+private theorem sumCode_eq (w : ℕ) (i : Fin w) :
+    sumCode w i.val = (sumFormula w i).toCircuit.code := by
+  let wires : Fin 3 → Fin ((w + w + 1) + ((w + 1) + (w + 1))) :=
+    ![Fin.castAdd ((w + 1) + (w + 1)) (leftInput w i),
+      Fin.castAdd ((w + 1) + (w + 1)) (rightInput w i),
+      Fin.natAdd (w + w + 1) ⟨w - i.val, by omega⟩]
+  have hw : (fun j => (wires j).val) = ![i.val, w + i.val, (w + w + 1) + (w - i.val)] := by
+    funext j
+    fin_cases j <;> simp [wires, leftInput, rightInput, Nat.add_comm]
+  have h := formulaCode_eq_code sumTemplate wires
+  rw [hw] at h
+  exact h
+
+/-- The full final-output code, including the carry-out reference. -/
+def finishCode (w : ℕ) : List (Op × List ℕ) × List ℕ :=
+  appendCode ((w + w + 1) + ((w + 1) + (w + 1)))
+    (bundleCode ((w + w + 1) + ((w + 1) + (w + 1))) 15 ((List.range w).map (sumCode w)))
+    ([], [w + w + 1])
+
+private theorem finishCode_eq (w : ℕ) : finishCode w = (finish w).code := by
+  have hs : (List.range w).map (sumCode w) =
+      List.ofFn (fun i : Fin w => (sumFormula w i).toCircuit.code) := by
+    apply List.ext_getElem (by simp)
+    intro i hi hj
+    simpa only [List.getElem_map, List.getElem_range, List.getElem_ofFn] using
+      sumCode_eq w ⟨i, by simpa using hi⟩
+  rw [finishCode, hs, bundleCode_code _ _ (by intro i; simp)]
+  have hc : ([], [w + w + 1]) =
+      (Circuit.wiring signature (fun _ : Fin 1 =>
+        (Fin.natAdd (w + w + 1) ⟨0, by omega⟩ :
+          Fin ((w + w + 1) + ((w + 1) + (w + 1)))))).code := rfl
+  rw [hc, appendCode_code]
+  rfl
+
+/-- Native generation of sum-bit and carry-out wiring from unary width. -/
+theorem computableTidilyInPolyTime_finish :
+    ComputableTidilyInPolyTime (fun w => (finish w).code) encUnary encCode := by
+  have hw : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1)
+      (encPair encUnary encUnary) encNat := unary_to_binary.comp (fst _ _)
+  have hi : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.2)
+      (encPair encUnary encUnary) encNat := unary_to_binary.comp (snd _ _)
+  have hs : ComputableTidilyInPolyTime (fun p : ℕ × ℕ => sumCode p.1 p.2)
+      (encPair encUnary encUnary) encCode := by
+    apply computableTidilyInPolyTime_formulaCode _ (by fun_prop)
+    intro j
+    fin_cases j
+    · exact hi
+    · change ComputableTidilyInPolyTime (fun p : ℕ × ℕ => p.1 + p.2) _ encNat
+      fun_prop
+    · change ComputableTidilyInPolyTime
+        (fun p : ℕ × ℕ => (p.1 + p.1 + 1) + (p.1 - p.2)) _ encNat
+      fun_prop
+  have hw' := unary_to_binary
+  have hn : ComputableTidilyInPolyTime
+      (fun w : ℕ => (w + w + 1) + ((w + 1) + (w + 1))) encUnary encNat := by fun_prop
+  have hc : ComputableTidilyInPolyTime (fun w : ℕ => ([], [w + w + 1]))
+      encUnary encCode := by fun_prop
+  have h := computableTidilyInPolyTime_appendCode hn
+    (computableTidilyInPolyTime_bundleCode hn (const 15) (mapWith hs id' range)) hc
+  simpa only [← finishCode_eq, finishCode] using h
+
+/-- Identity-wire codes are generated from a unary input count, with binary output references. -/
+private theorem computableTidilyInPolyTime_identityCode :
+    ComputableTidilyInPolyTime
+      (fun k => (Circuit.wiring signature (id : Fin k → Fin k)).code) encUnary encCode := by
+  have h := (const (encMid := encList encGate) []).prod (unary_to_binary.map.comp range)
+  simpa only [code_wiring_id, Function.comp_def, List.map_id_fun', id_eq] using h
+
+end CarryLookahead
+
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+/-- One native polynomial-time algorithm generates the entire logarithmic-depth adder code
+from unary width. Every binary gate reference, output reference and framing bit is charged. -/
+theorem computableTidilyInPolyTime_carryLookahead :
+    ComputableTidilyInPolyTime (fun w => (carryLookahead w).code) encUnary encCode := by
+  have hn : ComputableTidilyInPolyTime (fun w : ℕ => w + w + 1) encUnary encUnary := by fun_prop
+  have hn' := unary_to_binary.comp hn
+  have hi := CarryLookahead.computableTidilyInPolyTime_identityCode.comp hn
+  have h := computableTidilyInPolyTime_compCode hn'
+    CarryLookahead.computableTidilyInPolyTime_finish
+    (computableTidilyInPolyTime_appendCode hn' hi
+        CarryLookahead.computableTidilyInPolyTime_carries)
+  simpa only [Function.comp_def, appendCode_code, compCode_code, carryLookahead] using h
+
+/-- The modular adder is generated by the same uniform native algorithm plus free output wiring
+and one hardwired carry gate. -/
+theorem computableTidilyInPolyTime_carryLookaheadAdd :
+    ComputableTidilyInPolyTime (fun w => (carryLookaheadAdd w).code) encUnary encCode := by
+  have hn : ComputableTidilyInPolyTime (fun w : ℕ => w + w) encUnary encUnary := by fun_prop
+  have hn' := unary_to_binary.comp hn
+  have hi := CarryLookahead.computableTidilyInPolyTime_identityCode.comp hn
+  have hz : ComputableTidilyInPolyTime
+      (fun w => (Circuit.oneGate (σ := signature) (n := w + w) (.const false) Fin.elim0).code)
+      encUnary encCode := by
+    have h : ComputableTidilyInPolyTime (fun w : ℕ => ([(Op.const false, [])], [w + w]))
+        encUnary encCode := (const _).prod (hn'.cons' (const []))
+    exact h
+  have ho : ComputableTidilyInPolyTime
+      (fun w => (Circuit.wiring signature (fun i : Fin w => i.castSucc)).code)
+      encUnary encCode := by
+    have he (w : ℕ) : (Circuit.wiring signature (fun i : Fin w => i.castSucc)).code =
+        ([], List.range w) := by
+      apply Prod.ext
+      · rfl
+      change List.ofFn (fun i : Fin w => i.val) = List.range w
+      apply List.ext_getElem (by simp)
+      intro i hi hj
+      simp
+    have h := (const (encMid := encList encGate) []).prod (unary_to_binary.map.comp range)
+    simpa only [he, Function.comp_def, List.map_id_fun', id_eq] using h
+  have h := computableTidilyInPolyTime_compCode hn' ho
+    (computableTidilyInPolyTime_compCode hn' computableTidilyInPolyTime_carryLookahead
+      (computableTidilyInPolyTime_appendCode hn' hi hz))
+  simpa only [Function.comp_def, appendCode_code, compCode_code, carryLookaheadAdd] using h
+
+/-- Generate the complete carry-save finishing code, including its repeated zero output wires. -/
+theorem computableTidilyInPolyTime_carryLookaheadFinish :
+    ComputableTidilyInPolyTime (fun w => (carryLookaheadFinish w).code) encUnary encCode := by
+  have hn : ComputableTidilyInPolyTime (fun w : ℕ => w + w) encUnary encNat := by fun_prop
+  have hz : ComputableTidilyInPolyTime
+      (fun w => ((Circuit.wiring signature (fun _ : Fin w => (0 : Fin 1))).comp
+        (Circuit.oneGate (σ := signature) (n := w + w) (.const false) Fin.elim0)).code)
+      encUnary encCode := by
+    have he (w : ℕ) : ((Circuit.wiring signature (fun _ : Fin w => (0 : Fin 1))).comp
+        (Circuit.oneGate (σ := signature) (n := w + w) (.const false) Fin.elim0)).code =
+        ([(Op.const false, [])], List.replicate w (w + w)) := by
+      apply Prod.ext
+      · rfl
+      change List.ofFn (fun _ : Fin w => w + w) = _
+      simp
+    simpa only [he] using (const [(Op.const false, [])]).prod (replicate id' hn)
+  have h := computableTidilyInPolyTime_appendCode hn
+    computableTidilyInPolyTime_carryLookaheadAdd hz
+  simpa only [appendCode_code, carryLookaheadFinish] using h
+
+end Cslib.Circuits.Boolean
diff --git a/Complexity/Computability/Circuit/Boolean/CodeTemplate.lean b/Complexity/Computability/Circuit/Boolean/CodeTemplate.lean
new file mode 100644
index 000000000..54a98dd5c
--- /dev/null
+++ b/Complexity/Computability/Circuit/Boolean/CodeTemplate.lean
@@ -0,0 +1,71 @@
+/-
+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.Circuit.Boolean.CodeComposition
+public import Complexity.Computability.Circuit.Boolean.Formula
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pi
+
+/-!
+# Uniform instantiation of fixed Boolean formula templates
+
+The formula is fixed, while the target input count and its selected binary input references may
+vary. The certificate constructs the actual code of the renamed formula. It does not use a
+finite encoding of circuits at a fixed width. Variable-size families of instances can use
+`appendCodes` after providing their uniform scalar generator.
+
+## Main definitions
+
+* `Cslib.Circuits.Boolean.formulaCode`: the actual code of a fixed formula at selected wires.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.formulaCode_eq_code`: exact agreement with typed instantiation.
+* `Cslib.Circuits.Boolean.computableTidilyInPolyTime_formulaCode`: instantiate a fixed formula
+  at efficiently computed input wires.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Boolean
+
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+/-- Instantiate a formula at raw wire numbers. This algorithm is total even when a selected
+wire is outside the declared input count; its typed correctness theorem requires valid wires. -/
+def formulaCode {m : ℕ} (n : ℕ) (F : Formula signature m) (wires : Fin m → ℕ) :
+    List (Op × List ℕ) × List ℕ :=
+  match F with
+  | .input i => ([], [wires i])
+  | .gate op args => compCode n (Circuit.oneGate (σ := signature) op id).code
+      (appendCodes n (List.ofFn fun i => formulaCode n (args i) wires))
+
+/-- Instantiating valid input wires constructs exactly the renamed formula's circuit code. -/
+theorem formulaCode_eq_code {n m : ℕ} (F : Formula signature m) (wires : Fin m → Fin n) :
+    formulaCode n F (fun i => (wires i).val) = (F.rename wires).toCircuit.code := by
+  induction F with
+  | input i => rfl
+  | gate op args ih =>
+    simp only [formulaCode, ih, appendCodes_code, compCode_code,
+      Formula.rename, Formula.gate_bind, Formula.toCircuit]
+
+/-- A fixed formula's full instantiated code is polynomial-time in the target input count and
+its selected binary wire numbers. This is uniform in every target width and reference. -/
+theorem computableTidilyInPolyTime_formulaCode {α : Type} {enc : α ↪ List Bool}
+    {n : α → ℕ} {m : ℕ} (F : Formula signature m) {wires : α → Fin m → ℕ}
+    (hn : ComputableTidilyInPolyTime n enc encNat)
+    (hwires : ∀ i, ComputableTidilyInPolyTime (fun a => wires a i) enc encNat) :
+    ComputableTidilyInPolyTime (fun a => formulaCode (n a) F (wires a)) enc encCode := by
+  induction F with
+  | input i => exact (const []).prod ((hwires i).cons' (const []))
+  | gate op args ih =>
+    exact computableTidilyInPolyTime_compCode hn
+      (const (Circuit.oneGate (σ := signature) op id).code)
+      (computableTidilyInPolyTime_appendCodes hn (ofFn (fun i => ih i)))
+
+end Cslib.Circuits.Boolean
diff --git a/Complexity/Computability/Circuit/Boolean/EncodingSize.lean b/Complexity/Computability/Circuit/Boolean/EncodingSize.lean
new file mode 100644
index 000000000..ca231ba48
--- /dev/null
+++ b/Complexity/Computability/Circuit/Boolean/EncodingSize.lean
@@ -0,0 +1,68 @@
+/-
+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.Circuit.Boolean.Encoding
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LinearSpaceArith
+import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List
+
+/-!
+# Bounding the complete binary encoding of a circuit
+
+A circuit's typed wires bound every binary reference by its input and gate counts. This gives a
+polynomial bound on its complete serialized code, including gate tags, outputs and framing.
+It is useful for certifying circuit-construction loops whose intermediate circuits have bounded
+size, without making a claim about the complexity of the functions those circuits compute.
+
+## Main results
+
+* `Cslib.Circuits.Boolean.length_encCode_le`: a bound in the input, output and gate counts.
+-/
+
+@[expose] public section
+
+namespace Cslib.Circuits.Boolean
+
+open Turing.MultiTapeTM
+
+/-- The full code of a typed De Morgan circuit has polynomially bounded encoded length. -/
+theorem length_encCode_le {n m : ℕ} (c : Circuit signature n m) :
+    (encCode c.code).length ≤
+      2 * c.size * (23 + 8 * (n + c.size)) + 1 + m * (2 * (n + c.size) + 1) := by
+  have hgate (line : Line signature n c.size) :
+      (encGate line.code).length ≤ 11 + 4 * (n + c.size) := by
+    have hop : (encOp line.op).length ≤ 4 := by
+      cases line.op with
+      | const b => cases b <;> decide
+      | _ => decide
+    have hargs : (encList encNat line.code.2).length ≤ 2 * (2 * (n + c.size) + 1) := by
+      have h := length_encList_le encNat line.code.2 (b := n + c.size) (fun i hi => by
+        obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hi
+        exact (length_encNat_le_self _).trans (Wire.toNat_lt (line.wires j)).le)
+      have ha : line.code.2.length ≤ 2 := by
+        rw [Line.length_code_snd]
+        cases line.op <;> simp
+      exact h.trans (Nat.mul_le_mul_right _ ha)
+    simp only [encGate, length_encPair, Line.code_fst]
+    omega
+  have hgates : (encList encGate c.code.1).length ≤ c.size * (23 + 8 * (n + c.size)) := by
+    have h := length_encList_le encGate c.code.1 (b := 11 + 4 * (n + c.size)) (fun g hg => by
+      rw [Circuit.code, Program.code_eq_ofFn_lines] at hg
+      obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hg
+      exact hgate (c.program.lines j))
+    rw [show c.code.1.length = c.size from Program.length_code c.program] at h
+    nlinarith
+  have houtputs : (encList encNat c.code.2).length ≤ m * (2 * (n + c.size) + 1) := by
+    have h := length_encList_le encNat c.code.2 (b := n + c.size) (fun i hi => by
+      obtain ⟨j, rfl⟩ := List.mem_ofFn.mp hi
+      exact (length_encNat_le_self _).trans (Wire.toNat_lt (c.outputs j)).le)
+    simpa [Circuit.code] using h
+  simp only [encCode, length_encPair]
+  nlinarith
+
+end Cslib.Circuits.Boolean
diff --git a/Complexity/Computability/Circuit/Boolean/Word.lean b/Complexity/Computability/Circuit/Boolean/Word.lean
index 9f05438c9..e5a8ff2fb 100644
--- a/Complexity/Computability/Circuit/Boolean/Word.lean
+++ b/Complexity/Computability/Circuit/Boolean/Word.lean
@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Complexity.Computability.Circuit.Boolean.Synthesis
 public import Complexity.Computability.Circuit.Iteration
+public import Complexity.Foundations.Data.BitString.Basic
 public import Init.Data.BitVec.Bitblast
 public import Mathlib.Data.List.OfFn
 
@@ -74,6 +75,35 @@ theorem getLsbD_word (bits : BitString w) (i : Fin w) :
 theorem word_getLsbD (a : BitVec w) : word (fun i : Fin w => a.getLsbD i.val) = a :=
   BitVec.eq_of_getLsbD_eq fun i hi => getLsbD_word _ ⟨i, hi⟩
 
+/-- The word representation and the bit-string numbering use the same unsigned value. -/
+theorem toNat_word_eq_equivFin {w : ℕ} (x : BitString w) :
+    (word x).toNat = (BitString.equivFin w x : ℕ) := by
+  induction w with
+  | zero =>
+    have h := (BitString.equivFin 0 x).isLt
+    simp only [pow_zero, Nat.lt_one_iff] at h
+    have hx := (word x).isLt
+    simp only [pow_zero, Nat.lt_one_iff] at hx
+    exact hx.trans h.symm
+  | succ w ih =>
+    have heq : x = Fin.cons (x 0) (fun i => x i.succ) := by
+      funext i
+      induction i using Fin.cases <;> rfl
+    rw [heq, BitString.val_equivFin_cons]
+    have hw : word (Fin.cons (x 0) (fun i => x i.succ)) =
+        (word (fun i => x i.succ)).concat (x 0) := by
+      apply BitVec.eq_of_getLsbD_eq
+      intro i hi
+      rw [getLsbD_word _ ⟨i, hi⟩, BitVec.getLsbD_concat]
+      cases i with
+      | zero => simp
+      | succ i =>
+        simp only [Nat.add_eq_zero_iff, Nat.one_ne_zero, and_false, ite_false,
+          Nat.add_sub_cancel]
+        exact (getLsbD_word (fun i => x i.succ) ⟨i, by omega⟩).symm
+    rw [hw, BitVec.toNat_concat, ih]
+    omega
+
 /-- The coordinate functions of a word-valued function. -/
 def wordWires (a : BitString n → BitVec w) : Set (BooleanFunction n) :=
   Set.range fun i : Fin w => fun x => (a x).getLsbD i.val
diff --git a/ComplexityTests.lean b/ComplexityTests.lean
index 7b748a683..51117dbc4 100644
--- a/ComplexityTests.lean
+++ b/ComplexityTests.lean
@@ -63,6 +63,7 @@ import ComplexityTests.BooleanHierarchyPH
 import ComplexityTests.Broadcast
 import ComplexityTests.CNF
 import ComplexityTests.CNFPolyTime
+import ComplexityTests.CarryLookahead
 import ComplexityTests.CircuitCertificate
 import ComplexityTests.CircuitEvaluation
 import ComplexityTests.CircuitHamming.Approximation
diff --git a/ComplexityTests/CarryLookahead.lean b/ComplexityTests/CarryLookahead.lean
new file mode 100644
index 000000000..f073f7fe2
--- /dev/null
+++ b/ComplexityTests/CarryLookahead.lean
@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.Circuit.Boolean.CarryLookahead.PolyTime
+
+/-!
+# Carry-lookahead arithmetic and uniform generation clients
+
+The examples distinguish significance order, preserve carry-in at width zero, exercise a
+non-power-of-two propagation chain, and finish an existing carry-save reduction. Runtime clients
+generate complete binary circuit codes at growing widths and at arbitrary binary scan distances.
+-/
+
+namespace ComplexityTests.CarryLookahead
+
+open Cslib Cslib.Circuits Cslib.Circuits.Boolean
+open Turing.MultiTapeTM ComputableTidilyInPolyTime
+
+-- At width zero the carry is the sole output, whereas the modular output is empty.
+example (c : Bool) :
+    (carryLookahead 0).eval interpretation (fun _ => c) = fun _ => c := by
+  funext i
+  fin_cases i
+  cases c <;> rfl
+
+example : (carryLookaheadAdd 0).eval interpretation Fin.elim0 = Fin.elim0 := by
+  funext i
+  exact i.elim0
+
+-- Low generate/high kill and low kill/high generate must not be interchanged.
+example : (carryLookahead 2).eval interpretation
+    (Fin.append (Fin.append ![true, false] ![true, false]) (fun _ => false)) =
+      ![false, true, false] := by
+  apply (BitString.equivFin 3).injective
+  apply Fin.ext
+  rw [val_eval_carryLookahead]
+  decide
+
+example : (carryLookahead 2).eval interpretation
+    (Fin.append (Fin.append ![false, true] ![false, true]) (fun _ => false)) =
+      ![false, false, true] := by
+  apply (BitString.equivFin 3).injective
+  apply Fin.ext
+  rw [val_eval_carryLookahead]
+  decide
+
+-- Five is not a power of two: carry-in crosses all five positions and becomes the output carry.
+example : (carryLookahead 5).eval interpretation
+    (Fin.append (Fin.append (fun _ => true) (fun _ => false)) (fun _ => true)) =
+      ![false, false, false, false, false, true] := by
+  apply (BitString.equivFin 6).injective
+  apply Fin.ext
+  rw [val_eval_carryLookahead]
+  decide
+
+-- The same overflow is discarded by the modular interface.
+example : (BitString.equivFin 5 ((carryLookaheadAdd 5).eval interpretation
+    (Fin.append (fun _ => true) ![true, false, false, false, false])) : ℕ) = 0 := by
+  rw [val_eval_carryLookaheadAdd]
+  decide
+
+-- An inactive round retains every summary even at a large binary-encoded distance.
+example : (Cslib.Circuits.Boolean.CarryLookahead.step 3 (2 ^ 100)).eval interpretation
+    ![true, false, true, false, true, false] = ![true, false, true, false, true, false] := by
+  funext i
+  fin_cases i <;>
+    simp only [Cslib.Circuits.Boolean.CarryLookahead.step,
+      Circuit.eval_append, Circuit.eval_pi, Formula.eval_toCircuit,
+      Formula.eval_or, Formula.eval_and, Formula.eval_input,
+      Cslib.Circuits.Boolean.CarryLookahead.generateFormula,
+      Cslib.Circuits.Boolean.CarryLookahead.propagateFormula,
+      Cslib.Circuits.Boolean.CarryLookahead.neighbour,
+      Formula.eval_or, Formula.eval_and, Formula.eval_input] <;> decide
+
+-- The replacement finishes an existing 4-to-2 carry-save circuit, with every input arbitrary.
+example (w : ℕ) (p q : BitString (w + w)) :
+    pairVal (((carryLookaheadFinish w).comp (csa4to2 w)).eval interpretation
+      (Fin.append p q)) % 2 ^ w = (pairVal p + pairVal q) % 2 ^ w ∧
+    BitString.sndBits (((carryLookaheadFinish w).comp (csa4to2 w)).eval interpretation
+      (Fin.append p q)) = (fun _ => false) := by
+  exact ⟨pairVal_eval_carryLookaheadFinish_csa4to2_mod p q,
+    by rw [Circuit.eval_comp]; exact sndBits_eval_carryLookaheadFinish _⟩
+
+example (w : ℕ) : (carryLookaheadAdd w).depth ≤ 8 * (Nat.clog 2 (w + 1) + 1) ∧
+    (carryLookaheadAdd w).size ≤ 21 * (w + 1) ^ 2 :=
+  ⟨depth_carryLookaheadAdd_le_log w, size_carryLookaheadAdd_le w⟩
+
+-- The actual generated code is accepted by the ordinary checked circuit decoder.
+example (w : ℕ) : Circuit.ofCode (σ := signature) (w + w + 1) (w + 1) (carryLookahead w).code =
+    some (carryLookahead w) := Circuit.ofCode_code _
+
+/-- A single native algorithm generates full adder codes at an unbounded computed width. -/
+theorem growingWidth_polynomialTime :
+    ComputableTidilyInPolyTime (fun k : ℕ => (carryLookahead (2 * k + 1)).code)
+      encUnary encCode :=
+  computableTidilyInPolyTime_carryLookahead.comp (by fun_prop)
+
+/-- The modular and carry-save finishing generators are also uniform in the unary width. -/
+theorem modularAndFinish_polynomialTime :
+    ComputableTidilyInPolyTime (fun w => ((carryLookaheadAdd w).code,
+      (carryLookaheadFinish w).code)) encUnary (encPair encCode encCode) :=
+  computableTidilyInPolyTime_carryLookaheadAdd.prod
+    computableTidilyInPolyTime_carryLookaheadFinish
+
+/-- Distances are binary and need not be polynomially bounded as natural numbers. -/
+theorem arbitraryDistance_polynomialTime :
+    ComputableTidilyInPolyTime
+      (fun p : ℕ × ℕ => Cslib.Circuits.Boolean.CarryLookahead.stepCode p.1 p.2)
+      (encPair encUnary encNat) encCode :=
+  Cslib.Circuits.Boolean.CarryLookahead.computableTidilyInPolyTime_stepCode
+    (fst _ _) (snd _ _)
+
+/-- info: 'Cslib.Circuits.Boolean.val_eval_carryLookahead' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.val_eval_carryLookahead
+/-- info: 'Cslib.Circuits.Boolean.depth_carryLookahead_le_log' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.depth_carryLookahead_le_log
+/-- info: 'Cslib.Circuits.Boolean.size_carryLookahead_le' depends on axioms:
+[propext, Classical.choice, Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.size_carryLookahead_le
+/-- info: 'Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.pairVal_eval_carryLookaheadFinish_csa4to2_mod
+/-- info: 'Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookahead' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookahead
+/-- info: 'Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadAdd' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadAdd
+/-- info: 'Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadFinish' depends on axioms: [propext,
+ Classical.choice,
+ Quot.sound] -/
+#guard_msgs in
+#print axioms Cslib.Circuits.Boolean.computableTidilyInPolyTime_carryLookaheadFinish
+
+end ComplexityTests.CarryLookahead

From f55fc77fe1c67ae6e85ee95be40534549713a817 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <SamuelSchlesinger@users.noreply.github.com>
Date: Fri, 23 Oct 2026 15:29:22 -0400
Subject: [PATCH 2/2] doc(circuit): record uniform carry-lookahead arithmetic

Record the exact arithmetic and native-generation milestone, credit
Ladner--Fischer, and retain the open stronger-uniformity and shallow-decryption
objectives. The curated headline abstracts are unaffected.

AI-assisted by Codex (worker-codex-carry-lookahead-20261023).
---
 ROADMAP.md     |  9 +++++++++
 references.bib | 12 ++++++++++++
 2 files changed, 21 insertions(+)

diff --git a/ROADMAP.md b/ROADMAP.md
index 4e752933e..f4cc65f71 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -843,6 +843,15 @@ batches.
      now certifies construction of circuit codes from encoded instances, with separately
      prescribed unary input/output widths. Its proof reuses the uniform tableau writer,
      prefix hardwiring and shared-input circuit composition; it establishes no depth bound.
+     The [carry-lookahead adder](Complexity/Computability/Circuit/Boolean/CarryLookahead.lean)
+     computes exact unsigned addition with carry-in and carry-out at every width, including zero.
+     Its depth is at most `7 + 2*ceil(log₂(w+1))`, with polynomial size and every gate charged.
+     The modular version has depth at most `8 + 2*ceil(log₂(w+1))`; a carry-save finishing client
+     preserves the existing 4-to-2 reducer's value modulo `2^w` and clears its second word.
+     The [native generators](Complexity/Computability/Circuit/Boolean/CarryLookahead/PolyTime.lean)
+     construct the complete binary gate/output codes from unary width, reusing fixed formula
+     templates and shared-input code assembly. This establishes polynomial-time uniformity for
+     these arithmetic circuits; stronger uniformity and shallow cryptographic decryption remain open.
      Define logspace and DLOGTIME uniformity with explicit gate-address, direct-connection and
      input encodings. Certify circuit generation and evaluation and the relevant machine-to-
      circuit simulations, preserving size, depth and construction-resource bounds. Prove
diff --git a/references.bib b/references.bib
index 59661405e..0d31c71a6 100644
--- a/references.bib
+++ b/references.bib
@@ -6,6 +6,18 @@ @misc{LeanCanny2026
   note = {Source revision 2a50a2ee00ae0699cc3f0c2bff5100c4687d2d8e}
 }
 
+@article{LadnerFischer1980,
+  author = {Ladner, Richard E. and Fischer, Michael J.},
+  title = {Parallel Prefix Computation},
+  journal = {Journal of the ACM},
+  volume = {27},
+  number = {4},
+  pages = {831--838},
+  year = {1980},
+  doi = {10.1145/322217.322232},
+  url = {https://doi.org/10.1145/322217.322232}
+}
+
 @article{MorenoRivera2016,
   author = {Moreno, Rutilo and Rivera, Luis Manuel},
   title = {Blocks in Cycles and {$k$}-Commuting Permutations},