Lean declarations

def BoyerMoore.majority EconCSLib @ cef01c7, EconCSLib.Examples.CostM.BoyerMoore

def majority : List A → CostM Cells (Option A)
  | []      => pure none
  | x :: xs => do
    ✓[Cells.alloc 2] do
      let result ← loop x 1 xs
      ✓[Cells.free 2] pure result
where
  /-- Single-pass loop carrying the current candidate and counter as
  parameters — no allocation, no ticks. -/
  loop (cand : A) (cnt : ℕ) : List A → CostM Cells (Option A)
    | []      => pure (some cand)
    | y :: ys =>
      if y = cand then loop cand (cnt + 1) ys
      else if cnt = 0 then loop y 1 ys
      else loop cand (cnt - 1) ys

theorem BoyerMoore.loop_cost EconCSLib @ cef01c7, EconCSLib.Examples.CostM.BoyerMoore
The loop has zero cost: it overwrites the two slots without allocating.
```
theorem loop_cost (cand : A) (cnt : ℕ) (xs : List A) :
    (majority.loop cand cnt xs).cost = 0
```
theorem BoyerMoore.majority_peak_le EconCSLib @ cef01c7, EconCSLib.Examples.CostM.BoyerMoore
```
theorem majority_peak_le (xs : List A) : (majority xs).cost.peak ≤ 2
```

Modules: EconCSLib.Examples.CostM.BoyerMoore

Worked Example: Constant-Space Boyer–Moore Majority

The Boyer–Moore majority vote in CostM Cells (Peak-Memory Cost via the Cells Monoid), proving a constant peak-memory bound: regardless of input length, the peak working set is two cells — one candidate and one counter, $$ (\operatorname{majority}\,xs).\mathrm{cost}.\mathrm{peak} \;\le\; 2, $$ which is majority_peak_le. The mechanism is that the single-pass loop allocates nothing — loop_cost : (majority.loop \ldots).cost = 0 — so the only contributions to the peak come from one alloc 2 / free 2 pair bracketing the pass. Because peak (not sum) is the resource, the tropical Cells monoid is essential here; an additive ℕ cost cannot state this bound.

This example deliberately does not prove functional correctness (that majority returns the true majority when one exists). That omission is the point: in CostM the complexity bound lives on .cost and is provable in complete isolation from the .ret value, demonstrating the correctness/complexity decoupling described in The CostM Complexity Monad.