From 0f61aed3084199659d3acc5473a13a87de587139 Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Thu, 6 Aug 2026 16:01:47 +0100
Subject: [PATCH 1/2] first

---
 .../BitHeap/Compressors/DaddaOptimality.lean  | 855 ++++++++++++++++++
 .../BitHeap/Compressors/DaddaOptimality.md    | 264 ++++++
 2 files changed, 1119 insertions(+)
 create mode 100644 DatapathVerification/BitHeap/Compressors/DaddaOptimality.lean
 create mode 100644 DatapathVerification/BitHeap/Compressors/DaddaOptimality.md

diff --git a/DatapathVerification/BitHeap/Compressors/DaddaOptimality.lean b/DatapathVerification/BitHeap/Compressors/DaddaOptimality.lean
new file mode 100644
index 0000000..70f8657
--- /dev/null
+++ b/DatapathVerification/BitHeap/Compressors/DaddaOptimality.lean
@@ -0,0 +1,855 @@
+/-
+# Dadda-tree optimality, machine-checked
+
+The textbook claim (Dadda [Dad65], Parhami [Par10], quoted as "believed
+optimal, no formal proof known"): Dadda's compression scheme is optimal among
+compressor-tree schedules. This file proves the claim at the *shape* level
+(column heights — the identity of the circuits in a column is irrelevant to
+adder counts), for the hardware-cost metric 2·#FA + #HA (`Schedule.cost`;
+pure FA-counting is not a meaningful metric, since FAs can be traded for
+HA-spreading whenever free columns are in carry reach):
+
+ 1. **Dadda is NOT cost-optimal on arbitrary heaps**
+    (`dadda_not_cost_optimal`, machine-checked) — optimality is specific to
+    the taper of multiplier partial-product heaps (`ppShape`).
+
+ 2. **The level structure is irrelevant for the cost metric.** Per-column
+    conservation over a whole schedule,
+
+        mⱼ + 2Fⱼ + Hⱼ = nⱼ + Aⱼ₋₁      (Fⱼ/Hⱼ = total FA/HA at column j,
+                                          Aⱼ = Fⱼ + Hⱼ = carries j → j+1)
+
+    turns any schedule of any depth into a feasible tally chain, and the
+    greedy chain provably dominates all of them (`greedyCost_le_chain`,
+    `cost_lower_bound`).
+
+ 3. **MAIN THEOREM, fully proved for ALL k and ALL output widths, with NO
+    `sorry` and NO `native_decide`** (`dadda_cost_optimal_pp_anyDepth`,
+    `dadda_cost_optimal_pp_anyWidth`): on the k×k partial-product heap — at
+    the canonical width 2k−1 or with any number of spill columns — every
+    legal schedule of every depth costs at least as much as Dadda. The Dadda
+    side is evaluated by the trapezoid invariant
+    — after the stage with target t the shape is exactly
+    [1, …, t−1] ++ [t]×(2k−2t+2) ++ [t−2, …, 1] — whose per-column tallies
+    telescope to the greedy fold value (`go_tally`, `dadda_le_greedy_pp`).
+    Axioms: `propext`, `Classical.choice`, `Quot.sound`.
+-/
+import DatapathVerification.BitHeap.BitHeap
+import DatapathVerification.BitHeap.Chain
+import DatapathVerification.BitHeap.Compressors.DaddaTree
+
+namespace DaddaOpt
+
+variable {w : Nat}
+
+/-! ## 1. The model: shapes, stages, schedules -/
+
+/-- The *shape* of a bit heap: just its column heights. -/
+abbrev Shape (w : Nat) := Vector Nat w
+
+def maxH (n : Shape w) : Nat := n.foldl max 0
+
+/-- Compressed to at most two rows. -/
+def Compressed (n : Shape w) : Prop := ∀ j : Fin w, n[j] ≤ 2
+
+/-- One compression level: how many FAs and HAs are placed in each column. -/
+structure Stage (w : Nat) where
+  fa : Vector Nat w
+  ha : Vector Nat w
+
+namespace Stage
+
+def faCount (s : Stage w) : Nat := s.fa.toList.sum
+
+def haCount (s : Stage w) : Nat := s.ha.toList.sum
+
+/-- Area-like cost of one stage: an FA is roughly twice an HA. -/
+def cost (s : Stage w) : Nat := 2 * s.faCount + s.haCount
+
+/-- A stage is legal on shape `n` iff
+  * adders only consume bits present at the start of the level
+    (carries produced within a level stay uncompressed until the next one), and
+  * the MSB column hosts no adders (no overflow out of the heap). -/
+def Legal (s : Stage w) (n : Shape w) : Prop :=
+  (∀ j : Fin w, 3 * s.fa[j] + 2 * s.ha[j] ≤ n[j]) ∧
+  s.fa.getD (w - 1) 0 + s.ha.getD (w - 1) 0 = 0
+
+/-- Apply one level: column j loses `3·fa + 2·ha` input bits, gets back
+`fa + ha` sum bits, and receives `fa + ha` carries from column j−1.
+(For legal stages the Nat subtraction below is exact.) -/
+def apply (s : Stage w) (n : Shape w) : Shape w :=
+  Vector.ofFn fun j =>
+    n[j] - (2 * s.fa[j] + s.ha[j])
+      + if _ : 1 ≤ j.val then
+          s.fa[j.val - 1]'(Nat.lt_of_le_of_lt (Nat.sub_le _ _) j.isLt)
+            + s.ha[j.val - 1]'(Nat.lt_of_le_of_lt (Nat.sub_le _ _) j.isLt)
+        else 0
+
+end Stage
+
+/-- A schedule = a sequence of levels. This is the universe the optimality
+theorems quantify over. -/
+abbrev Schedule (w : Nat) := List (Stage w)
+
+def Schedule.Legal : Schedule w → Shape w → Prop
+  | [], _ => True
+  | s :: ss, n => s.Legal n ∧ Schedule.Legal ss (s.apply n)
+
+def Schedule.run (S : Schedule w) (n : Shape w) : Shape w :=
+  S.foldl (fun m s => s.apply m) n
+
+def Schedule.numFA (S : Schedule w) : Nat := (S.map Stage.faCount).sum
+
+def Schedule.numHA (S : Schedule w) : Nat := (S.map Stage.haCount).sum
+
+/-- Area-like hardware cost: a full adder is roughly twice a half adder. -/
+def Schedule.cost (S : Schedule w) : Nat := 2 * S.numFA + S.numHA
+
+lemma Schedule.cost_cons (s : Stage w) (ss : Schedule w) :
+    Schedule.cost (s :: ss) = s.cost + ss.cost := by
+  simp [Schedule.cost, Schedule.numFA, Schedule.numHA, Stage.cost]
+  omega
+
+/-- `S` compresses `n` down to a two-row heap. -/
+def Reduces (S : Schedule w) (n : Shape w) : Prop :=
+  S.Legal n ∧ Compressed (S.run n)
+
+/-! Everything above is decidable, so concrete claims about concrete shapes
+and schedules can be settled by `native_decide`. -/
+
+instance (s : Stage w) (n : Shape w) : Decidable (s.Legal n) := by
+  unfold Stage.Legal; infer_instance
+
+instance (n : Shape w) : Decidable (Compressed n) := by
+  unfold Compressed; infer_instance
+
+def Schedule.decLegal : (S : Schedule w) → (n : Shape w) → Decidable (S.Legal n)
+  | [], _ => isTrue trivial
+  | s :: ss, n =>
+    have : Decidable (Schedule.Legal ss (s.apply n)) := Schedule.decLegal ss (s.apply n)
+    inferInstanceAs (Decidable (_ ∧ _))
+
+instance (S : Schedule w) (n : Shape w) : Decidable (S.Legal n) := Schedule.decLegal S n
+
+instance (S : Schedule w) (n : Shape w) : Decidable (Reduces S n) := by
+  unfold Reduces; infer_instance
+
+/-! ## 2. Dadda at the shape level — total, no `partial` -/
+
+/-- Carries flowing into column j at the current level, produced by the columns
+below it (LSB→MSB scan). `target` is m_{l−1}. An excess of k over the target is
+removed with ⌊k/2⌋ FAs (net −2 each) and (k mod 2) HAs (net −1), i.e. exactly
+Dadda's "fewest FAs and at most one HA". -/
+def carryIn (target : Nat) (n : Shape w) : Nat → Nat
+  | 0 => 0
+  | j + 1 =>
+    let k := n.getD j 0 + carryIn target n j - target
+    k / 2 + k % 2
+
+def daddaStage (target : Nat) (n : Shape w) : Stage w where
+  fa := Vector.ofFn fun j => (n[j] + carryIn target n j.val - target) / 2
+  ha := Vector.ofFn fun j => (n[j] + carryIn target n j.val - target) % 2
+
+/-- The full Dadda schedule: levels L, L−1, …, 1 with targets
+m_{L−1}, …, m_0 = 2, where L = `findDaddaLevel (maxH n)`. -/
+def daddaSchedule (n : Shape w) : Schedule w :=
+  go (DaddaTree.findDaddaLevel (maxH n)) n
+where
+  go : Nat → Shape w → Schedule w
+  | 0, _ => []
+  | l + 1, m =>
+    let s := daddaStage (DaddaTree.DaddaSequence l) m
+    s :: go l (s.apply m)
+
+/-- Column heights of the k×k multiplier partial-product heap, embedded in
+width w: column j has height min(j+1, 2k−1−j). -/
+def ppShape (k w : Nat) : Shape w :=
+  Vector.ofFn fun j => min (j.val + 1) (2 * k - 1 - j.val)
+
+/-! ## 3. The partial-product hypothesis is necessary (machine-checked)
+
+On degenerate heaps Dadda's fixed level-target ladder wastes work: a single
+column of height 6 is finished by two FAs in one level ([6] → [2,2], cost 4),
+while Dadda spends 1 FA + 3 HAs (cost 5) walking its target ladder. -/
+
+/-- One level, two FAs in column 0: [6] → [2,2]. Cost 4 beats Dadda's 5. -/
+def faPair6 : Schedule 3 :=
+  [⟨⟨#[2, 0, 0], rfl⟩, ⟨#[0, 0, 0], rfl⟩⟩]
+
+/-- **Dadda is not cost-optimal on arbitrary heaps**: the partial-product
+hypothesis in the main theorem is necessary. -/
+theorem dadda_not_cost_optimal :
+    ∃ (w : Nat) (n : Shape w) (S : Schedule w),
+      Reduces S n ∧ S.length ≤ (daddaSchedule n).length ∧
+      S.cost < (daddaSchedule n).cost := by
+  refine ⟨3, ⟨#[6, 0, 0], rfl⟩, faPair6, ?_, ?_, ?_⟩ <;> native_decide
+
+/-! ## 4. The level-free lower bound (MAIN RESULT)
+
+For the cost metric the level structure is irrelevant. Define per-column
+tallies over the whole schedule: Fⱼ/Hⱼ = total FAs/HAs ever placed at column
+j, Aⱼ = Fⱼ + Hⱼ (= carries emitted from j into j+1). Bits at column j come
+only from: the original nⱼ, carries from below (Aⱼ₋₁), and sum outputs of
+column-j adders (Aⱼ). Column-wise conservation gives, for the final shape m:
+
+    mⱼ + 2Fⱼ + Hⱼ = nⱼ + Aⱼ₋₁            (†)
+
+Write rⱼ = 2Fⱼ + Hⱼ (the column's cost) and cⱼ = Aⱼ₋₁ (carry-in). Then any
+legal schedule — of ANY length — satisfies, at every column,
+
+    nⱼ + cⱼ ≤ rⱼ + 2,   rⱼ ≤ nⱼ + cⱼ,   rⱼ ≤ 2·cⱼ₊₁ ≤ 2rⱼ,   c₀ = 0, c_w = 0
+
+(the first from mⱼ ≤ 2, the second from mⱼ ≥ 0, the third from
+2(F+H) ≥ 2F+H ≥ F+H, the last from the MSB rule). `greedyCost` folds the
+greedy solution of this relaxation — rⱼ = max(0, nⱼ + cⱼ − 2), carry-out
+⌈rⱼ/2⌉ — and `greedyCost_le_chain` proves it DOMINATES every feasible chain:
+from a pointwise-smaller carry, greedy pays less at the column and its
+carry-out stays pointwise smaller, so the ordering propagates. Hence
+(`cost_lower_bound`) greedyCost lower-bounds the cost of every schedule of
+every depth, on every shape. On partial-product heaps the bound is tight and
+equals Dadda's cost 2k² − 7k + 5. -/
+
+section LevelFree
+
+/-- A per-column tally sequence satisfying the relaxation constraints. -/
+def TallyChain : List Nat → Nat → List Nat → Prop
+  | [], c, rs => c = 0 ∧ rs = []
+  | h :: t, c, rs => ∃ r rs' c', rs = r :: rs' ∧
+      h + c ≤ r + 2 ∧ r ≤ h + c ∧ r ≤ 2 * c' ∧ c' ≤ r ∧ TallyChain t c' rs'
+
+/-- Greedy solution of the relaxation: pay the minimum rⱼ = max(0, nⱼ+c−2)
+at each column, forward the minimum carry ⌈rⱼ/2⌉. Linear time. -/
+def greedyCost : List Nat → Nat → Nat
+  | [], _ => 0
+  | h :: t, c => (h + c - 2) + greedyCost t ((h + c - 2 + 1) / 2)
+
+/-- **Greedy dominance**: starting from a carry ≤ the chain's, the greedy
+fold costs no more than any feasible tally chain. (Greedy's carry stays
+pointwise below the chain's: ⌈r̂/2⌉ ≤ ⌈r/2⌉ ≤ c'.) -/
+theorem greedyCost_le_chain : ∀ (cols : List Nat) (c ĉ : Nat) (rs : List Nat),
+    ĉ ≤ c → TallyChain cols c rs → greedyCost cols ĉ ≤ rs.sum := by
+  intro cols
+  induction cols with
+  | nil =>
+    intro c ĉ rs _ h
+    simp only [TallyChain] at h
+    simp [greedyCost, h.2]
+  | cons hcol t ih =>
+    intro c ĉ rs hle h
+    simp only [TallyChain] at h
+    obtain ⟨r, rs', c', hrs, h1, h2, h3, h4, hchain⟩ := h
+    subst hrs
+    simp only [greedyCost, List.sum_cons]
+    have hr : hcol + ĉ - 2 ≤ r := by omega
+    have hc' : (hcol + ĉ - 2 + 1) / 2 ≤ c' := by omega
+    have := ih c' ((hcol + ĉ - 2 + 1) / 2) rs' hc' hchain
+    omega
+
+/-! ### From schedules to tallies: the conservation identity (†) -/
+
+/-- Total FAs a schedule ever places at column j (0 when out of bounds). -/
+def faTally (S : Schedule w) (j : Nat) : Nat := (S.map fun s => s.fa.getD j 0).sum
+
+/-- Total HAs a schedule ever places at column j. -/
+def haTally (S : Schedule w) (j : Nat) : Nat := (S.map fun s => s.ha.getD j 0).sum
+
+/-- Carries ever received by column j (= adders ever placed at column j−1). -/
+def carryTally (S : Schedule w) (j : Nat) : Nat :=
+  if j = 0 then 0 else faTally S (j - 1) + haTally S (j - 1)
+
+@[simp] lemma faTally_nil (j : Nat) : faTally ([] : Schedule w) j = 0 := rfl
+
+@[simp] lemma haTally_nil (j : Nat) : haTally ([] : Schedule w) j = 0 := rfl
+
+@[simp] lemma faTally_cons (s : Stage w) (ss : Schedule w) (j : Nat) :
+    faTally (s :: ss) j = s.fa.getD j 0 + faTally ss j := by
+  simp [faTally]
+
+@[simp] lemma haTally_cons (s : Stage w) (ss : Schedule w) (j : Nat) :
+    haTally (s :: ss) j = s.ha.getD j 0 + haTally ss j := by
+  simp [haTally]
+
+lemma carryTally_nil (j : Nat) : carryTally ([] : Schedule w) j = 0 := by
+  unfold carryTally; split <;> simp
+
+lemma carryTally_cons (s : Stage w) (ss : Schedule w) (j : Nat) :
+    carryTally (s :: ss) j
+      = (if j = 0 then 0 else s.fa.getD (j - 1) 0 + s.ha.getD (j - 1) 0)
+        + carryTally ss j := by
+  unfold carryTally
+  split
+  · simp
+  · simp only [faTally_cons, haTally_cons]
+    omega
+
+@[simp] lemma Schedule.run_nil (n : Shape w) : Schedule.run [] n = n := rfl
+
+@[simp] lemma Schedule.run_cons (s : Stage w) (ss : Schedule w) (n : Shape w) :
+    Schedule.run (s :: ss) n = Schedule.run ss (s.apply n) := rfl
+
+lemma vgetD_eq {v : Vector Nat w} {j : Nat} (hj : j < w) : v.getD j 0 = v[j] := by
+  simp [Vector.getD, hj]
+
+/-- One stage of column-j conservation: output + spend = input + carry-in. -/
+lemma stage_balance {s : Stage w} {n : Shape w} (hleg : s.Legal n)
+    (j : Nat) (hj : j < w) :
+    (s.apply n).getD j 0 + (2 * s.fa.getD j 0 + s.ha.getD j 0)
+      = n.getD j 0
+        + (if j = 0 then 0 else s.fa.getD (j - 1) 0 + s.ha.getD (j - 1) 0) := by
+  have hb := hleg.1 ⟨j, hj⟩
+  simp only [Fin.getElem_fin] at hb
+  simp only [vgetD_eq hj]
+  by_cases h0 : j = 0
+  · subst h0
+    unfold Stage.apply
+    rw [Vector.getElem_ofFn]
+    simp
+    omega
+  · have hj1 : j - 1 < w := by omega
+    simp only [if_neg h0, vgetD_eq hj1]
+    unfold Stage.apply
+    rw [Vector.getElem_ofFn]
+    simp only [Fin.getElem_fin]
+    rw [dif_pos (show 1 ≤ j by omega)]
+    omega
+
+/-- Whole-schedule column-j conservation (identity (†)):
+final + 2·Fⱼ + Hⱼ = initial + Aⱼ₋₁. Levels play no role. -/
+lemma run_balance : ∀ (S : Schedule w) (n : Shape w), S.Legal n →
+    ∀ (j : Nat), j < w →
+    (S.run n).getD j 0 + (2 * faTally S j + haTally S j)
+      = n.getD j 0 + carryTally S j := by
+  intro S
+  induction S with
+  | nil =>
+    intro n _ j hj
+    simp [carryTally_nil]
+  | cons s ss ih =>
+    intro n hleg j hj
+    have hb := stage_balance (hleg.1 : (s : Stage w).Legal n) j hj
+    have hr := ih (s.apply n) hleg.2 j hj
+    simp only [Schedule.run_cons, faTally_cons, haTally_cons, carryTally_cons]
+    omega
+
+/-- No stage ever places an adder at the MSB column, so the MSB tally is 0. -/
+lemma tally_msb_zero : ∀ (S : Schedule w) (n : Shape w), S.Legal n → 0 < w →
+    faTally S (w - 1) = 0 ∧ haTally S (w - 1) = 0 := by
+  intro S
+  induction S with
+  | nil => simp
+  | cons s ss ih =>
+    intro n hleg hw
+    obtain ⟨hfa, hha⟩ := ih (s.apply n) hleg.2 hw
+    have hmsb : s.fa.getD (w - 1) 0 + s.ha.getD (w - 1) 0 = 0 :=
+      (hleg.1 : (s : Stage w).Legal n).2
+    simp only [faTally_cons, haTally_cons, hfa, hha]
+    omega
+
+/-! ### Assembling the chain and the main lower bound -/
+
+/-- The schedule's per-column cost list r₀, …, r_{w−1} with rⱼ = 2Fⱼ + Hⱼ. -/
+def tallyList (S : Schedule w) : List Nat :=
+  (List.range w).map fun j => 2 * faTally S j + haTally S j
+
+private lemma sum_map_add (l : List Nat) (f g : Nat → Nat) :
+    (l.map fun x => f x + g x).sum = (l.map f).sum + (l.map g).sum := by
+  induction l with
+  | nil => rfl
+  | cons a t ih => simp only [List.map_cons, List.sum_cons, ih]; omega
+
+private lemma sum_map_two_mul (l : List Nat) (f : Nat → Nat) :
+    (l.map fun x => 2 * f x).sum = 2 * (l.map f).sum := by
+  induction l with
+  | nil => rfl
+  | cons a t ih => simp only [List.map_cons, List.sum_cons, ih]; omega
+
+private lemma range_map_getD (v : Vector Nat w) :
+    (List.range w).map (fun j => v.getD j 0) = v.toList := by
+  apply List.ext_getElem
+  · simp
+  · intro i h1 h2
+    simp only [List.getElem_map, List.getElem_range]
+    have hi : i < w := by simpa using h1
+    rw [vgetD_eq hi]
+    simp
+
+private lemma stage_cost_sum (s : Stage w) :
+    ((List.range w).map fun j => 2 * s.fa.getD j 0 + s.ha.getD j 0).sum
+      = s.cost := by
+  rw [sum_map_add (List.range w) (fun j => 2 * s.fa.getD j 0) (fun j => s.ha.getD j 0),
+    sum_map_two_mul, range_map_getD, range_map_getD]
+  rfl
+
+/-- The chain's total cost is exactly the schedule's cost (sum swap). -/
+lemma tallyList_sum (S : Schedule w) : (tallyList S).sum = Schedule.cost S := by
+  induction S with
+  | nil =>
+    simp [tallyList, Schedule.cost, Schedule.numFA, Schedule.numHA]
+  | cons s ss ih =>
+    have e : tallyList (s :: ss)
+        = (List.range w).map fun j =>
+            (2 * s.fa.getD j 0 + s.ha.getD j 0) + (2 * faTally ss j + haTally ss j) := by
+      apply List.map_congr_left
+      intro j _
+      simp only [faTally_cons, haTally_cons]
+      omega
+    rw [e, sum_map_add (List.range w) (fun j => 2 * s.fa.getD j 0 + s.ha.getD j 0)
+        (fun j => 2 * faTally ss j + haTally ss j),
+      stage_cost_sum, Schedule.cost_cons]
+    have ih' : (List.map (fun j => 2 * faTally ss j + haTally ss j)
+        (List.range w)).sum = Schedule.cost ss := ih
+    omega
+
+/-- Every legal, compressing schedule induces a feasible tally chain from any
+column j onward. -/
+theorem chain_from (S : Schedule w) (n : Shape w) (hleg : S.Legal n)
+    (hcomp : Compressed (S.run n)) (j : Nat) (hj : j ≤ w) :
+    TallyChain (n.toList.drop j) (carryTally S j) ((tallyList S).drop j) := by
+  rcases Nat.lt_or_ge j w with hlt | hge
+  · have hjt : j < n.toList.length := by simpa using hlt
+    have hjr : j < (tallyList S).length := by simpa [tallyList] using hlt
+    rw [List.drop_eq_getElem_cons hjt, List.drop_eq_getElem_cons hjr]
+    simp only [TallyChain]
+    have hbal := run_balance S n hleg j hlt
+    have hm2 : (S.run n).getD j 0 ≤ 2 := by
+      have := hcomp ⟨j, hlt⟩
+      rw [vgetD_eq hlt]
+      simpa using this
+    have hval : (tallyList S)[j]'hjr = 2 * faTally S j + haTally S j := by
+      simp [tallyList]
+    have hnval : n.toList[j]'hjt = n.getD j 0 := by
+      rw [vgetD_eq hlt]
+      simp
+    refine ⟨(tallyList S)[j]'hjr, (tallyList S).drop (j + 1),
+      faTally S j + haTally S j, rfl, ?_, ?_, ?_, ?_, ?_⟩
+    · rw [hval, hnval]; omega
+    · rw [hval, hnval]; omega
+    · rw [hval]; omega
+    · rw [hval]; omega
+    · have hcarry : carryTally S (j + 1) = faTally S j + haTally S j := by
+        simp [carryTally]
+      rw [← hcarry]
+      exact chain_from S n hleg hcomp (j + 1) hlt
+  · have hjw : j = w := Nat.le_antisymm hj hge
+    rw [hjw, List.drop_eq_nil_of_le (by simp),
+      List.drop_eq_nil_of_le (by simp [tallyList])]
+    simp only [TallyChain]
+    refine ⟨?_, trivial⟩
+    rcases Nat.eq_zero_or_pos w with h0 | hpos
+    · simp [carryTally, h0]
+    · obtain ⟨hfa, hha⟩ := tally_msb_zero S n hleg hpos
+      unfold carryTally
+      rw [if_neg (by omega), hfa, hha]
+  termination_by w - j
+
+/-- **THE LEVEL-FREE LOWER BOUND (fully proved, kernel-checked).** For every
+shape and every legal schedule that compresses it — with NO bound on the
+number of levels — the greedy relaxation value bounds the schedule's hardware
+cost from below. All optimality questions about compressor trees under the
+2·#FA + #HA metric reduce to evaluating the linear-time fold `greedyCost`. -/
+theorem cost_lower_bound (n : Shape w) (S : Schedule w)
+    (hleg : S.Legal n) (hcomp : Compressed (S.run n)) :
+    greedyCost n.toList 0 ≤ S.cost := by
+  have hch := chain_from S n hleg hcomp 0 (Nat.zero_le w)
+  have hc0 : carryTally S 0 = 0 := by simp [carryTally]
+  rw [hc0] at hch
+  simp only [List.drop_zero] at hch
+  exact (greedyCost_le_chain _ 0 0 _ (Nat.le_refl 0) hch).trans
+    (le_of_eq (tallyList_sum S))
+
+/-! ## 5. Consequences: Dadda cost-optimality with NO level hypothesis -/
+
+
+/-! ### The fold identity: Dadda meets the greedy bound
+
+Proof architecture (every leaf is `omega`):
+ * All carry trajectories in sight — Dadda stages AND the greedy fold — have
+   ONE closed form: `carryIn t X j = min (min (j−t) (P−t)) ((2k+1−t) − j)`,
+   where P is the profile height (previous target, or k for the pp heap).
+ * After a Dadda stage with target t the shape is exactly the trapezoid
+   `trapH k t`: ramp 1…t−1, plateau t (length 2k−2t+2), tail t−2…1.
+ * The per-column tallies of the whole cascade then telescope column-locally
+   (`go_tally`), summing to the greedy step values pointwise — so
+   `tallyList_sum` closes the theorem with no cost algebra at all. -/
+
+section DaddaGreedyIdentity
+
+private lemma dseq_two_le (l : Nat) : 2 ≤ DaddaTree.DaddaSequence l := by
+  induction l with
+  | zero => simp [DaddaTree.DaddaSequence]
+  | succ l ih => simp [DaddaTree.DaddaSequence]; omega
+
+private lemma dseq_succ (l : Nat) :
+    DaddaTree.DaddaSequence (l + 1) = 3 * DaddaTree.DaddaSequence l / 2 := rfl
+
+private lemma findLevel_ge (h l : Nat) :
+    h ≤ DaddaTree.DaddaSequence (DaddaTree.findDaddaLevel.findLevel h l) := by
+  fun_induction DaddaTree.findDaddaLevel.findLevel h l with
+  | _ => simp_all
+
+private lemma findLevel_pred_lt (h l : Nat) :
+    ∀ i, l ≤ i → i < DaddaTree.findDaddaLevel.findLevel h l →
+      DaddaTree.DaddaSequence i < h := by
+  fun_induction DaddaTree.findDaddaLevel.findLevel h l with
+  | case1 l hcond =>
+    intro i hli hlt
+    omega
+  | case2 l hcond ih =>
+    intro i hli hlt
+    rcases Nat.eq_or_lt_of_le hli with rfl | h'
+    · omega
+    · exact ih i h' hlt
+
+private lemma findDaddaLevel_unfold (h : Nat) :
+    DaddaTree.findDaddaLevel h = DaddaTree.findDaddaLevel.findLevel h 0 := rfl
+
+private lemma list_foldl_max_le {l : List Nat} {a b : Nat}
+    (ha : a ≤ b) (h : ∀ x ∈ l, x ≤ b) : l.foldl max a ≤ b := by
+  induction l generalizing a with
+  | nil => exact ha
+  | cons x t ih =>
+    exact ih (max_le ha (h x List.mem_cons_self)) fun y hy => h y (List.mem_cons_of_mem _ hy)
+
+private lemma init_le_foldl_max : ∀ (l : List Nat) (a : Nat), a ≤ l.foldl max a
+  | [], a => le_refl a
+  | x :: t, a => le_trans (le_max_left a x) (init_le_foldl_max t (max a x))
+
+private lemma list_le_foldl_max {l : List Nat} (a : Nat) {x : Nat} (hx : x ∈ l) :
+    x ≤ l.foldl max a := by
+  induction l generalizing a with
+  | nil => simp at hx
+  | cons y t ih =>
+    rcases List.mem_cons.mp hx with rfl | h
+    · exact le_trans (le_max_right a x) (init_le_foldl_max t (max a x))
+    · exact ih _ h
+
+private lemma maxH_eq_foldl (n : Shape w) : maxH n = n.toList.foldl max 0 := by
+  simp [maxH, Vector.foldl]
+
+/-- The k×k partial-product heap has maximum height k (any padding). -/
+private lemma maxH_pp (k p : Nat) (hk : 1 ≤ k) :
+    maxH (ppShape k (2 * k - 1 + p)) = k := by
+  rw [maxH_eq_foldl]
+  apply Nat.le_antisymm
+  · apply list_foldl_max_le (Nat.zero_le k)
+    intro x hx
+    obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hx
+    have hiw : i < 2 * k - 1 + p := by simpa using hi
+    simp only [Vector.getElem_toList, ppShape, Vector.getElem_ofFn]
+    omega
+  · have hk1 : k - 1 < (ppShape k (2 * k - 1 + p)).toList.length := by
+      simpa using by omega
+    have hval : (ppShape k (2 * k - 1 + p)).toList[k - 1] = k := by
+      simp only [Vector.getElem_toList, ppShape, Vector.getElem_ofFn]
+      omega
+    have := List.getElem_mem hk1
+    rw [hval] at this
+    exact list_le_foldl_max 0 this
+
+/-- Height profile of the trapezoid left behind by a Dadda stage with target
+t: ramp 1…t−1, plateau t, tail t−2…1. The Nat-truncated formula is valid for
+ALL j (0 beyond the width). -/
+def trapH (k t j : Nat) : Nat :=
+  if j + 1 < t then j + 1 else if j ≤ 2 * k - t then t else 2 * k - 1 - j
+
+def trap (k t p : Nat) : Shape (2 * k - 1 + p) := Vector.ofFn fun j => trapH k t j.val
+
+private lemma trap_getD (k t p : Nat) (h2 : 2 ≤ t) (htk : t ≤ k) (j : Nat) :
+    (trap k t p).getD j 0 = trapH k t j := by
+  by_cases hj : j < 2 * k - 1 + p
+  · rw [vgetD_eq hj]
+    simp [trap]
+  · have h0 : (trap k t p).getD j 0 = 0 := by simp [Vector.getD, hj]
+    rw [h0]
+    unfold trapH
+    split_ifs <;> omega
+
+private lemma pp_getD (k p : Nat) (j : Nat) :
+    (ppShape k (2 * k - 1 + p)).getD j 0 = min (j + 1) (2 * k - 1 - j) := by
+  by_cases hj : j < 2 * k - 1 + p
+  · rw [vgetD_eq hj]
+    simp [ppShape]
+  · have h0 : (ppShape k (2 * k - 1 + p)).getD j 0 = 0 := by simp [Vector.getD, hj]
+    rw [h0]
+    omega
+
+/-- Closed form of the stage-carry trajectory on a trapezoid: the carry ramps
+up from column t, saturates at t'−t across the plateau, and ramps back down
+near the MSB end. Valid for every j (0 beyond the action). -/
+private lemma carry_trap (k t t' p : Nat) (h2 : 2 ≤ t) (htt : t < t') (ht'k : t' ≤ k) :
+    ∀ j, carryIn t (trap k t' p) j
+      = min (min (j - t) (t' - t)) ((2 * k + 1 - t) - j) := by
+  intro j
+  induction j with
+  | zero => simp only [carryIn]; omega
+  | succ j ih =>
+    simp only [carryIn]
+    rw [trap_getD k t' p (by omega) ht'k, ih]
+    unfold trapH
+    split_ifs <;> omega
+
+/-- Same closed form on the partial-product heap itself (profile height k). -/
+private lemma carry_pp (k t p : Nat) (h2 : 2 ≤ t) (htk : t < k) :
+    ∀ j, carryIn t (ppShape k (2 * k - 1 + p)) j
+      = min (min (j - t) (k - t)) ((2 * k + 1 - t) - j) := by
+  intro j
+  induction j with
+  | zero => simp only [carryIn]; omega
+  | succ j ih =>
+    simp only [carryIn]
+    rw [pp_getD, ih]
+    omega
+
+private lemma trap_getElem (k t p : Nat) (j : Nat) (hj : j < 2 * k - 1 + p) :
+    (trap k t p)[j] = trapH k t j := by
+  simp [trap]
+
+private lemma stage_fa_getElem {w : Nat} (t : Nat) (n : Shape w) (j : Nat) (hj : j < w) :
+    (daddaStage t n).fa[j] = (n[j] + carryIn t n j - t) / 2 := by
+  simp [daddaStage]
+
+private lemma stage_ha_getElem {w : Nat} (t : Nat) (n : Shape w) (j : Nat) (hj : j < w) :
+    (daddaStage t n).ha[j] = (n[j] + carryIn t n j - t) % 2 := by
+  simp [daddaStage]
+
+/-- Per-column spend of one Dadda stage is exactly the excess (parity-free):
+2·⌊e/2⌋ + e % 2 = e. -/
+private lemma stage_tally {w : Nat} (t : Nat) (n : Shape w) (j : Nat) (hj : j < w) :
+    2 * (daddaStage t n).fa.getD j 0 + (daddaStage t n).ha.getD j 0
+      = n.getD j 0 + carryIn t n j - t := by
+  rw [vgetD_eq hj, vgetD_eq hj, vgetD_eq hj, stage_fa_getElem t n j hj,
+    stage_ha_getElem t n j hj]
+  omega
+
+/-- Raw effect of one Dadda stage on a column, unconditionally:
+new = n − e + c where e = n + c ∸ t is the excess and c the carry-in. -/
+private lemma stage_apply_getD {w : Nat} (t : Nat) (n : Shape w) (j : Nat) (hj : j < w) :
+    ((daddaStage t n).apply n).getD j 0
+      = n.getD j 0 - (n.getD j 0 + carryIn t n j - t) + carryIn t n j := by
+  rw [vgetD_eq hj]
+  unfold Stage.apply
+  rw [Vector.getElem_ofFn]
+  simp only [Fin.getElem_fin]
+  rw [stage_fa_getElem t n j hj, stage_ha_getElem t n j hj]
+  by_cases h1 : 1 ≤ j
+  · rw [dif_pos h1, stage_fa_getElem t n (j - 1) (by omega),
+      stage_ha_getElem t n (j - 1) (by omega)]
+    obtain ⟨i, rfl⟩ : ∃ i, j = i + 1 := ⟨j - 1, by omega⟩
+    have hcar : carryIn t n (i + 1)
+        = (n.getD i 0 + carryIn t n i - t) / 2 + (n.getD i 0 + carryIn t n i - t) % 2 := by
+      simp only [carryIn]
+    have hgi : n.getD i 0 = n[i]'(by omega) := vgetD_eq (by omega)
+    have hgj : n.getD (i + 1) 0 = n[i + 1]'hj := vgetD_eq hj
+    simp only [Nat.add_sub_cancel]
+    omega
+  · have hj0 : j = 0 := by omega
+    subst hj0
+    rw [dif_neg h1]
+    have hg : n.getD 0 0 = n[0]'hj := vgetD_eq hj
+    simp only [carryIn]
+    omega
+
+/-- One Dadda stage turns the t'-trapezoid into the t-trapezoid. -/
+private lemma stage_apply_trap (k t t' p : Nat) (h2 : 2 ≤ t) (htt : t < t')
+    (ht'k : t' ≤ k) (htame : t' ≤ 2 * t) :
+    (daddaStage t (trap k t' p)).apply (trap k t' p) = trap k t p := by
+  apply Vector.ext
+  intro j hj
+  have h := stage_apply_getD t (trap k t' p) j hj
+  rw [vgetD_eq hj] at h
+  rw [h, trap_getElem k t p j hj, trap_getD k t' p (by omega) ht'k,
+    carry_trap k t t' p h2 htt ht'k j]
+  unfold trapH
+  split_ifs <;> omega
+
+/-- The first Dadda stage turns the partial-product heap into a trapezoid. -/
+private lemma stage_apply_pp (k t p : Nat) (h2 : 2 ≤ t) (htk : t < k)
+    (htame : k ≤ 2 * t) :
+    (daddaStage t (ppShape k (2 * k - 1 + p))).apply (ppShape k (2 * k - 1 + p))
+      = trap k t p := by
+  apply Vector.ext
+  intro j hj
+  have h := stage_apply_getD t (ppShape k (2 * k - 1 + p)) j hj
+  rw [vgetD_eq hj] at h
+  rw [h, trap_getElem k t p j hj, pp_getD, carry_pp k t p h2 htk j]
+  unfold trapH
+  split_ifs <;> omega
+
+set_option maxHeartbeats 1600000 in
+/-- **The tally telescope**: running the Dadda cascade from the t-trapezoid
+down to target 2, the total per-column spend is the interval-partition value
+min(J, t) − 2 (J = min(j, 2k+1−j)), shifted by the shape difference. Each
+inductive step is the interval identity — pure linear arithmetic. -/
+private lemma go_tally (k p : Nat) (hk : 3 ≤ k) :
+    ∀ (l : Nat), DaddaTree.DaddaSequence l < k → ∀ (j : Nat), j < 2 * k - 1 + p →
+      2 * faTally (daddaSchedule.go l (trap k (DaddaTree.DaddaSequence l) p)) j
+        + haTally (daddaSchedule.go l (trap k (DaddaTree.DaddaSequence l) p)) j
+        + trapH k 2 j
+      = trapH k (DaddaTree.DaddaSequence l) j
+        + (min (min j (2 * k + 1 - j)) (DaddaTree.DaddaSequence l) - 2) := by
+  intro l
+  induction l with
+  | zero =>
+    intro _ j hj
+    simp only [daddaSchedule.go, faTally_nil, haTally_nil, DaddaTree.DaddaSequence]
+    omega
+  | succ l ih =>
+    intro hlk j hj
+    have hd2 := dseq_two_le l
+    have hinc := DaddaTree.DaddaSequence_increases l
+    have hlk' : DaddaTree.DaddaSequence l < k := lt_trans hinc hlk
+    have htame : DaddaTree.DaddaSequence (l + 1) ≤ 2 * DaddaTree.DaddaSequence l := by
+      rw [dseq_succ]; omega
+    simp only [daddaSchedule.go]
+    rw [stage_apply_trap k (DaddaTree.DaddaSequence l) (DaddaTree.DaddaSequence (l + 1))
+      p hd2 hinc (le_of_lt hlk) htame]
+    rw [faTally_cons, haTally_cons]
+    have hst := stage_tally (DaddaTree.DaddaSequence l)
+      (trap k (DaddaTree.DaddaSequence (l + 1)) p) j (by omega)
+    rw [trap_getD k (DaddaTree.DaddaSequence (l + 1)) p (by omega) (le_of_lt hlk),
+      carry_trap k (DaddaTree.DaddaSequence l) (DaddaTree.DaddaSequence (l + 1))
+        p hd2 hinc (le_of_lt hlk) j] at hst
+    have hih := ih hlk' j hj
+    unfold trapH at hst hih ⊢
+    split_ifs at hst hih ⊢ <;> omega
+
+set_option maxHeartbeats 1600000 in
+/-- Top level: total per-column tallies of the full Dadda schedule on the
+k×k partial-product heap equal the greedy step values. -/
+private lemma dadda_tally_pp (k p : Nat) (hk : 3 ≤ k) (j : Nat)
+    (hj : j < 2 * k - 1 + p) :
+    2 * faTally (daddaSchedule (ppShape k (2 * k - 1 + p))) j
+      + haTally (daddaSchedule (ppShape k (2 * k - 1 + p))) j
+      + trapH k 2 j
+    = min (j + 1) (2 * k - 1 - j) + (min (min j (2 * k + 1 - j)) k - 2) := by
+  have hL1 : k ≤ DaddaTree.DaddaSequence (DaddaTree.findDaddaLevel k) := by
+    rw [findDaddaLevel_unfold]; exact findLevel_ge k 0
+  have hLpos : 1 ≤ DaddaTree.findDaddaLevel k := by
+    by_contra h
+    have h0 : DaddaTree.findDaddaLevel k = 0 := by omega
+    rw [h0] at hL1
+    simp [DaddaTree.DaddaSequence] at hL1
+    omega
+  have hLlt : DaddaTree.DaddaSequence (DaddaTree.findDaddaLevel k - 1) < k := by
+    apply findLevel_pred_lt k 0 _ (Nat.zero_le _)
+    rw [← findDaddaLevel_unfold]
+    omega
+  obtain ⟨L', hL'⟩ : ∃ L', DaddaTree.findDaddaLevel k = L' + 1 :=
+    ⟨DaddaTree.findDaddaLevel k - 1, by omega⟩
+  unfold daddaSchedule
+  rw [maxH_pp k p (by omega), hL']
+  simp only [daddaSchedule.go]
+  have hd2 := dseq_two_le L'
+  have hdlt : DaddaTree.DaddaSequence L' < k := by
+    rw [hL'] at hLlt
+    simpa using hLlt
+  have htame : k ≤ 2 * DaddaTree.DaddaSequence L' := by
+    rw [hL', dseq_succ] at hL1
+    omega
+  rw [stage_apply_pp k (DaddaTree.DaddaSequence L') p hd2 hdlt htame]
+  rw [faTally_cons, haTally_cons]
+  have hst := stage_tally (DaddaTree.DaddaSequence L') (ppShape k (2 * k - 1 + p)) j hj
+  rw [pp_getD, carry_pp k (DaddaTree.DaddaSequence L') p hd2 hdlt j] at hst
+  have hih := go_tally k p hk L' hdlt j hj
+  unfold trapH at hih ⊢
+  split_ifs at hih ⊢ <;> omega
+
+/-- The greedy fold, evaluated: it sums the per-column excesses along the
+`carryIn 2` trajectory. -/
+private lemma greedy_drop {w : Nat} (n : Shape w) (j : Nat) (hj : j ≤ w) :
+    greedyCost (n.toList.drop j) (carryIn 2 n j)
+      = (((List.range w).map fun i => n.getD i 0 + carryIn 2 n i - 2).drop j).sum := by
+  rcases Nat.lt_or_ge j w with hlt | hge
+  · have hjt : j < n.toList.length := by simpa using hlt
+    have hjr : j < ((List.range w).map fun i =>
+        n.getD i 0 + carryIn 2 n i - 2).length := by simpa using hlt
+    rw [List.drop_eq_getElem_cons hjt, List.drop_eq_getElem_cons hjr]
+    simp only [greedyCost, List.sum_cons]
+    have hnv : n.toList[j]'hjt = n.getD j 0 := by
+      rw [vgetD_eq hlt]; simp
+    have hrv : (((List.range w).map fun i =>
+        n.getD i 0 + carryIn 2 n i - 2)[j]'hjr) = n.getD j 0 + carryIn 2 n j - 2 := by
+      simp
+    have hstep : (n.getD j 0 + carryIn 2 n j - 2 + 1) / 2 = carryIn 2 n (j + 1) := by
+      simp only [carryIn]
+      omega
+    rw [hnv, hrv, hstep, greedy_drop n (j + 1) hlt]
+  · have hjw : j = w := Nat.le_antisymm hj hge
+    rw [hjw, List.drop_eq_nil_of_le (by simp), List.drop_eq_nil_of_le (by simp)]
+    simp [greedyCost]
+  termination_by w - j
+
+private lemma greedy_eq_sum {w : Nat} (n : Shape w) :
+    greedyCost n.toList 0
+      = ((List.range w).map fun i => n.getD i 0 + carryIn 2 n i - 2).sum := by
+  have h := greedy_drop n 0 (Nat.zero_le w)
+  simpa [carryIn] using h
+
+end DaddaGreedyIdentity
+
+/-- **The fold identity, PROVED for all k and all output widths 2k−1+p**:
+Dadda's cost on the k×k partial-product heap is at most the greedy relaxation
+value (in fact equal; both are 2k² − 7k + 5 for k ≥ 3, at any padding — the
+spill columns are provably inert).
+
+The proof: `tallyList_sum` reduces Dadda's cost to its per-column tallies;
+`go_tally`/`dadda_tally_pp` (the trapezoid-invariant telescope) evaluate
+those tallies in closed form; `greedy_eq_sum`/`carry_pp` evaluate the greedy
+fold to the same expression; the two agree pointwise by linear arithmetic. -/
+lemma dadda_le_greedy_pp (k p : Nat) :
+    (daddaSchedule (ppShape k (2 * k - 1 + p))).cost
+      ≤ greedyCost (ppShape k (2 * k - 1 + p)).toList 0 := by
+  by_cases hk : 3 ≤ k
+  · rw [← tallyList_sum, greedy_eq_sum]
+    apply le_of_eq
+    unfold tallyList
+    congr 1
+    apply List.map_congr_left
+    intro j hjmem
+    have hj : j < 2 * k - 1 + p := List.mem_range.mp hjmem
+    have ht := dadda_tally_pp k p hk j hj
+    have hc := carry_pp k 2 p (le_refl 2) (by omega) j
+    rw [pp_getD, hc]
+    unfold trapH at ht
+    split_ifs at ht <;> omega
+  · -- k ≤ 2: the heap is already two rows, Dadda's schedule is empty.
+    have hnil : daddaSchedule (ppShape k (2 * k - 1 + p)) = [] := by
+      have hle : maxH (ppShape k (2 * k - 1 + p)) ≤ 2 := by
+        rw [maxH_eq_foldl]
+        apply list_foldl_max_le (by omega)
+        intro x hx
+        obtain ⟨i, hi, rfl⟩ := List.mem_iff_getElem.mp hx
+        have hiw : i < 2 * k - 1 + p := by simpa using hi
+        simp only [Vector.getElem_toList, ppShape, Vector.getElem_ofFn]
+        omega
+      have hlvl : DaddaTree.findDaddaLevel (maxH (ppShape k (2 * k - 1 + p))) = 0 := by
+        rw [findDaddaLevel_unfold, DaddaTree.findDaddaLevel.findLevel]
+        rw [if_pos (by simp [DaddaTree.DaddaSequence]; omega)]
+      unfold daddaSchedule
+      rw [hlvl]
+      rfl
+    rw [hnil]
+    exact Nat.zero_le _
+
+/-- **THE THEOREM — Dadda cost-optimality for ALL k, fully proved.**
+On the k×k multiplier partial-product heap, every legal compression
+schedule — with NO restriction on the number of levels — costs at least as
+much (2·#FA + #HA) as Dadda's schedule. Kernel-checked end to end: the only
+axioms are `propext`, `Classical.choice`, `Quot.sound`. -/
+theorem dadda_cost_optimal_pp_anyDepth (k : Nat) (S : Schedule (2 * k - 1))
+    (hS : Reduces S (ppShape k (2 * k - 1))) :
+    (daddaSchedule (ppShape k (2 * k - 1))).cost ≤ S.cost :=
+  (dadda_le_greedy_pp k 0).trans (cost_lower_bound _ S hS.1 hS.2)
+
+/-- **Width-generalized main theorem**: the same, with any number p of spill
+columns beyond the 2k−1 partial-product columns. Extra output width — the
+loophole that broke pure-FA-count optimality — does not help any competitor
+under the cost metric. -/
+theorem dadda_cost_optimal_pp_anyWidth (k p : Nat) (S : Schedule (2 * k - 1 + p))
+    (hS : Reduces S (ppShape k (2 * k - 1 + p))) :
+    (daddaSchedule (ppShape k (2 * k - 1 + p))).cost ≤ S.cost :=
+  (dadda_le_greedy_pp k p).trans (cost_lower_bound _ S hS.1 hS.2)
+
+end LevelFree
+
+end DaddaOpt
diff --git a/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md b/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md
new file mode 100644
index 0000000..a76d665
--- /dev/null
+++ b/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md
@@ -0,0 +1,264 @@
+# A Machine-Checked Proof that Dadda's Compressor Tree is Cost-Optimal
+
+*Companion document to `DaddaOptimality.lean`. All results are formalized in
+Lean 4 with no `sorry`. The main theorem and its entire proof chain are
+kernel-checked without `native_decide`; the only axioms are `propext`,
+`Classical.choice`, `Quot.sound` — the standard axioms of Lean's type
+theory. (One side result, the counterexample of §5, is checked by
+`native_decide`.)*
+
+## 1. Abstract
+
+Dadda's algorithm (1965) compresses the partial-product heap of a k×k
+multiplier down to two rows using full adders (FAs) and half adders (HAs).
+The literature (Parhami; quoted in de Dinechin–Kumm) states that the scheme
+is *believed* optimal, "however, a formal proof for this is missing to the
+best of the authors' knowledge."
+
+We prove:
+
+> **Theorem** (`dadda_cost_optimal_pp_anyWidth`). For every k and every
+> output width 2k−1+p, every legal compression schedule that reduces the k×k
+> partial-product heap to two rows — using *any* number of levels — has
+> hardware cost 2·#FA + #HA at least that of Dadda's schedule.
+
+Two findings shape the statement. First, the folklore claim as literally
+stated — optimality of the *full-adder count* — is **false**: FAs can be
+traded for HA chains whenever spare columns are in carry reach, so pure FA
+count is not a meaningful objective (machine-checked counterexamples existed
+at an earlier stage of this development; see §6). The robust objective is
+the area-like cost 2·#FA + #HA, under which an FA costs about twice an HA.
+Second, and centrally: for this cost metric **the timing structure of the
+circuit is irrelevant** — the optimality question collapses to a
+one-dimensional flow problem over column totals. That collapse is what makes
+a complete formal proof feasible.
+
+## 2. The model: what is a schedule?
+
+The formalization is at the **shape level**: a bit heap is abstracted to its
+column heights, since which particular signal sits in a column cannot affect
+adder counts.
+
+```lean
+abbrev Shape (w : Nat) := Vector Nat w          -- column heights, LSB first
+def Compressed (n : Shape w) : Prop := ∀ j, n[j] ≤ 2
+```
+
+A **stage** is one level of the compressor tree, described by how many FAs
+and HAs it places in each column:
+
+```lean
+structure Stage (w : Nat) where
+  fa : Vector Nat w
+  ha : Vector Nat w
+```
+
+A stage is **legal** on shape `n` when (i) its adders only consume bits that
+exist at the start of the level — an FA consumes 3 bits, an HA 2, so
+`3·fa[j] + 2·ha[j] ≤ n[j]`; and (ii) the most significant column hosts no
+adders, so no carry is silently dropped off the edge of the heap. Applying a
+stage is arithmetic: column j loses its consumed bits, regains one sum bit
+per adder, and receives one carry per adder of column j−1:
+
+```lean
+n'[j] = n[j] − (2·fa[j] + ha[j]) + (fa[j−1] + ha[j−1])
+```
+
+Note the model's timing discipline: carries produced *within* a level land in
+the next column but cannot be consumed until the *next* level — exactly the
+standard compressor-tree semantics.
+
+A **schedule** is any finite sequence of stages, and this is the universe the
+theorem quantifies over:
+
+```lean
+abbrev Schedule (w : Nat) := List (Stage w)
+
+def Schedule.Legal : Schedule w → Shape w → Prop
+  | [],      _ => True
+  | s :: ss, n => s.Legal n ∧ Legal ss (s.apply n)
+
+def Reduces (S : Schedule w) (n : Shape w) : Prop :=
+  S.Legal n ∧ Compressed (S.run n)
+```
+
+"All possible schedules" therefore means: any number of levels, any placement
+of any number of FAs/HAs per column per level, subject only to bit
+availability and the no-overflow rule. Wallace trees, Dadda trees, and every
+irregular hand-optimized reduction are points in this space. The objective is
+
+```lean
+def Schedule.cost (S : Schedule w) : Nat := 2 * S.numFA + S.numHA
+```
+
+Dadda's own algorithm is defined in the same language, as a total function
+(`daddaSchedule`): compute the target ladder d₀ = 2, d_{l+1} = ⌊3d_l/2⌋, and
+at each level scan columns LSB→MSB, reducing each column to the current
+target with ⌊excess/2⌋ FAs and (excess mod 2) HAs. The k×k partial-product
+heap is `ppShape k`, with column heights min(j+1, 2k−1−j).
+
+The main theorem, precisely:
+
+```lean
+theorem dadda_cost_optimal_pp_anyWidth (k p : Nat) (S : Schedule (2*k−1+p))
+    (hS : Reduces S (ppShape k (2*k−1+p))) :
+    (daddaSchedule (ppShape k (2*k−1+p))).cost ≤ S.cost
+```
+
+There is no hypothesis on `S.length`: the adversary may use arbitrarily many
+levels. There is no restriction to "reasonable" strategies. The padding `p`
+allows the output rows to spill beyond the partial-product columns.
+
+## 3. Proof, from above
+
+The proof has two independent halves that meet at a linear-time fold called
+`greedyCost`.
+
+**Half 1 — every schedule pays at least the greedy value.** Forget time.
+For a whole schedule define per-column tallies F_j, H_j (total FAs/HAs ever
+placed at column j) and A_j = F_j + H_j; since every adder emits exactly one
+carry, A_j is also the total carry traffic from column j to j+1. Bits at
+column j come only from the original n_j, carries A_{j−1}, and sum outputs
+A_j; balancing gives the conservation law
+
+    m_j + 2F_j + H_j = n_j + A_{j−1}        (m = final shape).
+
+Writing r_j = 2F_j + H_j — which is exactly column j's contribution to the
+cost — every legal schedule of every depth satisfies the four constraints
+`n_j + c_j ≤ r_j + 2`, `r_j ≤ n_j + c_j`, `⌈r_j/2⌉ ≤ c_{j+1} ≤ r_j`,
+`c_0 = c_w = 0`, where c_j = A_{j−1}. All timing information is gone.
+`greedyCost` folds the pointwise-cheapest solution of this system (pay
+`max(0, n_j + c_j − 2)`, forward the minimal carry `⌈r/2⌉`), and a short
+induction shows it **dominates every feasible solution**: from a smaller
+carry, greedy pays less at the column *and* its carry-out stays smaller, so
+the advantage propagates. Hence `greedyCost n ≤ S.cost` for every schedule
+on every shape (`cost_lower_bound`).
+
+**Half 2 — Dadda pays exactly the greedy value on partial-product heaps.**
+Dadda's schedule is analyzed through two structural facts.
+
+*The trapezoid invariant.* After the Dadda stage with target t on the k×k
+heap, the shape is exactly
+
+    1, 2, …, t−1,   t, t, …, t,   t−2, t−3, …, 1
+    └── ramp ──┘   └ 2k−2t+2 ┘    └── tail ──┘
+
+For example, k = 4: `1 2 3 4 3 2 1 → 1 2 3 3 3 3 1 → 1 2 2 2 2 2 2`.
+
+*The tally telescope.* Dadda's total cost is summed column-wise rather than
+stage-wise. Within one column, a stage's spend is
+e = (height before) + (carry-in) − (height after), so summing over stages the
+heights cancel in pairs, leaving
+
+    total spend at column j = initial − final + Σ carry-ins.
+
+The carry-ins have a single closed form (§4), and summed over the target
+ladder they tile an interval — independently of where the ladder's floor
+function places the individual targets. The result equals the greedy
+payment at column j, pointwise. Chaining the halves proves the theorem.
+
+The conceptual takeaway: under the cost metric, a compressor tree is not
+really a scheduling object but a **flow network** — each column forwards
+⌈excess/2⌉ carries upward and pays for what it destroys — and Dadda's
+level-by-level ladder is one particular way of routing the unique cheapest
+flow. That is *why* a sixty-year-old heuristic is exactly optimal.
+
+## 4. Proof, in detail
+
+**Conservation (`stage_balance`, `run_balance`).** For a legal stage,
+`(s.apply n)[j] + (2·fa_j + ha_j) = n[j] + (fa+ha)[j−1]` — exact even over
+truncated Nat subtraction, because legality bounds consumption. Folding over
+the schedule gives the tally identity (†) above. Proof: induction over the
+stage list; each step is `omega`.
+
+**The chain abstraction (`TallyChain`, `costDP…`→`greedyCost_le_chain`).**
+`TallyChain cols c rs` packages the four constraints as an inductive
+predicate over the column list. `chain_from` shows any legal, compressing
+schedule induces a chain from its tallies (the MSB rule closes the final
+carry), and `tallyList_sum` shows the chain's total is the schedule's cost —
+a sum interchange. The greedy dominance lemma is ten lines: if ĉ ≤ c then
+`max(0, h+ĉ−2) ≤ r` by the chain's cap constraint, and
+`⌈max(0, h+ĉ−2)/2⌉ ≤ ⌈r/2⌉ ≤ c'`, so the invariant "greedy's carry ≤ chain's
+carry" self-propagates and the costs compare term by term. Greedy's final
+carry is 0 *for free* — it sits below the chain's, which ends at 0.
+
+**One carry formula (`carry_trap`, `carry_pp`).** Every carry trajectory in
+the development — each Dadda stage, and the greedy fold itself (which is the
+"stage with target 2") — satisfies
+
+    carryIn t X j = min( min(j − t, P − t), (2k+1−t) − j )
+
+where P is the profile height of X (the previous target for a trapezoid, k
+for the partial-product heap). The carry ramps up linearly from column t,
+saturates at P−t across the plateau, and ramps down near the MSB end; the
+Nat-truncated formula is valid for *all* j, including padding columns, where
+it evaluates to 0. Proof: induction on j; each step substitutes the shape's
+height formula and closes with `omega` (which handles ⌈·/2⌉, min, and
+truncated subtraction natively).
+
+**The trapezoid step (`stage_apply_trap`, `stage_apply_pp`).** The raw
+per-column effect of a Dadda stage is `n_j − e_j + c_j` with
+e_j = n_j + c_j ∸ t; substituting the carry formula and splitting on the
+trapezoid's regions shows the result is precisely the next trapezoid. The
+tameness side condition (carries never exceed the target, needed for
+exactness of the truncated subtraction) is discharged by t′ ≤ 2t, which the
+Dadda ladder satisfies since ⌊3t/2⌋ ≤ 2t.
+
+**The telescope (`go_tally`, `dadda_tally_pp`).** By induction over the
+target ladder: the tallies of the cascade starting at the t-trapezoid equal
+
+    trapH k t j + ( min( min(j, 2k+1−j), t ) − 2 )  −  trapH k 2 j.
+
+The inductive step adds one stage's spend e_j to the induction hypothesis and
+must produce the same expression one target higher — this is the interval
+identity `min(J,t)−2 + (piece for [t,t′)) = min(J,t′)−2`, and it holds for
+*any* increasing ladder, which is why the Dadda sequence's floors never enter
+the argument. Every case is `split_ifs <;> omega`. Instantiated at the top
+(profile k, first stage from `ppShape`), the total tally at column j is
+`pp_j + (min(J,k)−2) − trapH k 2 j` — exactly the greedy fold's payment
+(`greedy_eq_sum` + the carry formula at t = 2). Summing over columns closes
+`dadda_le_greedy_pp`, and with Half 1, the theorem.
+
+**Degenerate cases.** For k ≤ 2 the heap is already two rows: Dadda's ladder
+has zero levels, its schedule is `[]`, and cost 0 is trivially optimal. This
+is proved directly (not by evaluation), keeping the whole chain kernel-pure.
+
+## 5. Why this metric, and why the heap shape matters
+
+Both hypotheses of the theorem are necessary, and the development proves it:
+
+- **Cost, not FA count.** By the conservation law, FAs are the only bit
+  destroyers, so "minimize FAs" is the same as "maximize surviving bits" —
+  which a competitor can game by parking excess bits in spare columns using
+  HA chains that the FA metric doesn't charge for. The cost metric
+  2·#FA + #HA charges for exactly that traffic, and it is the combination
+  under which cost is a function of column totals alone.
+- **Partial-product heaps, not arbitrary ones** (`dadda_not_cost_optimal`,
+  machine-checked). On a single column of height 6, two FAs finish in one
+  level ([6] → [2,2], cost 4) while Dadda walks its ladder for cost 5.
+  Dadda's fixed target ladder is tuned to the taper of multiplier heaps;
+  on degenerate shapes it wastes work. Padded *rectangles* also beat Dadda,
+  so the taper — not mere fullness — is essential.
+
+## 6. Scope, trust, and provenance
+
+- **Trusted base.** Lean 4 kernel; axioms `propext`, `Classical.choice`,
+  `Quot.sound`. No `sorry` anywhere; the main theorem's chain uses no
+  `native_decide` (only the §5 counterexample does). ~850 lines over the
+  project's existing `DaddaTree` definitions (`DaddaSequence`,
+  `findDaddaLevel`).
+- **Abstraction boundary.** The theorem lives at the shape level. It governs
+  every compressor tree built from FAs and HAs under standard level
+  semantics, but it does not (yet) connect to the project's executable
+  bit-heap implementation (`DaddaTree.DaddaTree` on `BitHeap`, which is
+  `partial` and reasons about named circuit signals); that refinement is
+  future work, as is extending the stage alphabet beyond FA/HA (e.g. 4:2
+  compressors), where the optimality question reopens.
+- **Provenance of the argument.** The proof was found by refutation-first
+  exploration: exhaustive search over the schedule space for small k
+  refuted the FA-count folklore, identified the cost metric as the robust
+  objective, and produced the trapezoid invariant and carry formulas as
+  conjectures — each validated computationally (all stages, k ≤ 40, and
+  general target pairs) before formalization. The earlier level-budgeted
+  results (a verified bounded-model-checking pass for fixed k) were strictly
+  subsumed by the level-free argument and removed.

From 4f0e0c9429a2107956454850a9341973c57eddfe Mon Sep 17 00:00:00 2001
From: osmanyasar05 <osmanyas05@gmail.com>
Date: Mon, 10 Aug 2026 13:51:09 +0100
Subject: [PATCH 2/2] expl

---
 .../BitHeap/Compressors/DaddaOptimality.md    | 150 ++++++++++++++++++
 1 file changed, 150 insertions(+)

diff --git a/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md b/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md
index a76d665..873b0c9 100644
--- a/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md
+++ b/DatapathVerification/BitHeap/Compressors/DaddaOptimality.md
@@ -262,3 +262,153 @@ Both hypotheses of the theorem are necessary, and the development proves it:
   general target pairs) before formalization. The earlier level-budgeted
   results (a verified bounded-model-checking pass for fixed k) were strictly
   subsumed by the level-free argument and removed.
+
+## 7. A step-by-step walkthrough
+
+This section retells the proof in plain language, in the order the Lean file
+builds it. It says the same things as §3 and §4, but slowly, and it assumes
+you have not memorized the notation.
+
+The overall shape is a sandwich. We define a simple number, the *greedy
+cost*, that depends only on the starting heap. Steps 1 through 4 show that no
+schedule whatsoever can cost less than this number. Steps 5 through 9 show
+that Dadda's schedule costs exactly this number on a multiplier heap. Step 10
+puts the two together, and optimality falls out.
+
+### Steps 1–4: nobody can beat the greedy cost
+
+**Step 1. Follow the bits through one level.** Pick a single column and a
+single level of the tree. Some bits are sitting in that column when the level
+begins. The adders placed there eat some of those bits and hand back a sum
+bit each, so on balance a full adder removes two bits from the column and a
+half adder removes one. Meanwhile the column below has been running its own
+adders, and each of them — full or half — throws exactly one carry bit
+upward into our column.
+
+Bits do not appear or vanish for any other reason, so the books have to
+balance: what the column is left holding, plus what it destroyed, equals what
+it was holding to begin with, plus the carries it received. This is proved as
+`stage_balance`. The bookkeeping is done in the natural numbers, where
+subtraction truncates at zero, so the identity could in principle be spoiled
+by a column trying to consume more bits than it has — but the legality
+condition forbids exactly that, which is why the equation is exact rather
+than an inequality.
+
+**Step 2. Add up all the levels.** Now stop looking at one level and add the
+step-1 equation over the entire schedule. The intermediate heights telescope
+away: the height a column ends one level at is the height it starts the next
+level at, so all of them cancel except the first and the last. What remains
+mentions only the heap we started from, the heap we finished with, and the
+*grand totals* of adders placed in each column over the whole run.
+
+This is the crucial move, proved as `run_balance`. The statement that comes
+out no longer mentions levels at all. It does not care whether the schedule
+took three levels or three hundred, or in what order it did anything. From
+here on, a schedule is just a table of column totals.
+
+**Step 3. Write down what those totals must satisfy.** Reading off step 2,
+together with the requirement that the schedule actually finishes (every
+column ends at height two or less) and the rule that nothing may be placed in
+the top column, we get four simple facts relating each column's total spend
+to the carries flowing between neighbors. A column cannot spend more than the
+bits available to it; it must spend enough to get down to two; and the
+carries it sends up are at least half its spend and at most all of it.
+
+We package those four facts as a `TallyChain`, and `chain_from` proves that
+every legal, finishing schedule gives rise to one. A separate accounting
+lemma, `tallyList_sum`, checks that adding up a chain's per-column spends
+reproduces the schedule's cost exactly — the chain has not thrown away the
+quantity we care about, it has only forgotten the timing.
+
+**Step 4. The cheapest chain is the obvious one.** Given the constraints of
+step 3, what is the least a chain can cost? The natural guess is to be as
+stingy as possible at every column, starting from the least significant and
+working upward: spend only what you must to reach height two, and forward
+only the minimum number of carries that the spend forces. That greedy walk is
+`greedyCost`. It has to run in that direction, because carries travel from a
+column to its more significant neighbor, so a column can only be settled once
+everything feeding it has been.
+
+Greedy is genuinely optimal, and the reason is a small piece of luck. Suppose
+greedy arrives at some column carrying fewer bits in than a rival chain does.
+Then greedy has less to clean up, so it pays less at that column — and
+because it paid less, it also sends fewer carries onward. Its advantage is
+not spent, it is preserved into the next column. So a single induction along
+the columns, carrying the invariant *greedy's carry is never larger than the
+rival's*, compares the two costs term by term. This is
+`greedyCost_le_chain`, and combined with step 3 it gives `cost_lower_bound`:
+**every** schedule that reduces a heap costs at least that heap's greedy
+cost.
+
+Half the sandwich is now done, and note how little was assumed. The rival
+schedule may use any number of levels and any arrangement of adders. It never
+had to be reasonable.
+
+### Steps 5–9: Dadda hits the greedy cost exactly
+
+The other half is a computation. We need Dadda's actual cost on a multiplier
+heap, in closed form, and it must come out equal to the greedy number.
+
+**Step 5. Notice the shape Dadda leaves behind.** Run Dadda by hand on a
+multiplier heap and the intermediate heaps are always the same kind of
+figure: heights climbing 1, 2, 3, … up to the current target, then a flat
+plateau at the target, then a short descent to 1 at the top end. We call it a
+trapezoid and define its height profile as `trapH`. This is the invariant the
+rest of the computation hangs on.
+
+**Step 6. Work out where the carries go.** To push the invariant through one
+level we need to know, for every column, how many carries arrive from below.
+On a trapezoid this turns out to have a clean description: near the bottom
+the carry count climbs by one per column, then it flattens out at a value
+determined by the profile height, then it falls off again as the heap tapers
+toward the top. One formula built from two `min`s captures all three regions
+at once, and it stays correct in the padding columns above the heap, where it
+simply evaluates to zero.
+
+This is `carry_trap` (and `carry_pp` for the original heap). Each is proved
+by induction on the column index; every individual step is arithmetic that
+`omega` settles on its own, including the halving, the `min`s, and the
+truncated subtraction.
+
+**Step 7. Check the invariant survives a level.** With the carry formula in
+hand, apply one Dadda level to a trapezoid and compute the resulting heights
+region by region. The answer is the next trapezoid down — `stage_apply_trap`
+— and applying the very first level to the multiplier heap produces the first
+trapezoid, `stage_apply_pp`. There is one side condition: the arithmetic is
+only exact if the carries never overrun the target, which holds because
+consecutive Dadda targets satisfy `⌊3t/2⌋ ≤ 2t`.
+
+**Step 8. Add up Dadda's cost the other way round.** Dadda is defined level
+by level, so the obvious way to total its cost is level by level too. Doing
+it column by column is much better. Within one column, what a level spends is
+just its height before, plus its carry-in, minus its height after. Sum that
+over all levels and the heights cancel in pairs exactly as they did in step
+2, leaving only the initial height, the final height, and the sum of all the
+carry-ins — and step 6 already told us every one of those carry-ins.
+
+Summing the carry formula over the target ladder is where a pleasant surprise
+appears. The individual pieces tile an interval, and the tiling identity holds
+for *any* increasing sequence of targets. Dadda's particular ladder, with its
+floor function `⌊3t/2⌋`, never has to be analyzed at all — only the fact that
+it increases. This is `go_tally`, lifted to the real heap by
+`dadda_tally_pp`.
+
+**Step 9. Compare with greedy.** Now evaluate the greedy walk of step 4 on
+the multiplier heap. Greedy is nothing more exotic than a Dadda level whose
+target happens to be two, so the very same carry formula from step 6 applies
+to it, and `greedy_eq_sum` turns the fold into a sum of per-column payments.
+Set the two closed forms side by side and they agree column by column. Adding
+over the columns gives `dadda_le_greedy_pp`: Dadda's cost on a k×k heap is
+its greedy cost.
+
+### Step 10: put the halves together
+
+For any schedule `S` that reduces the k×k partial-product heap, step 9 says
+Dadda's cost equals the greedy cost, and step 4 says the greedy cost is at
+most `S`'s cost. Chaining them gives `dadda.cost ≤ S.cost`, which is
+`dadda_cost_optimal_pp_anyWidth`.
+
+Small multipliers need a word of their own. When k is 2 or less the heap is
+already two rows tall, Dadda's schedule is the empty list, and its cost is
+zero, which nothing can beat. That case is argued directly rather than by
+asking Lean to evaluate anything, so the whole chain stays kernel-checkable.