Lean declarations

structure CostM EconCSLib @ cef01c7, EconCSLib.Foundation.CostM

structure CostM (C : Type*) (A : Type*) where
  /-- The result of the computation. -/
  ret  : A
  /-- The accumulated cost in `C`. -/
  cost : C

def CostM.pure EconCSLib @ cef01c7, EconCSLib.Foundation.CostM
Lift a pure value at zero cost.
```
protected def pure [Zero C] (a : A) : CostM C A := ⟨a, 0⟩
```
def CostM.bind EconCSLib @ cef01c7, EconCSLib.Foundation.CostM
Sequential composition. The cost of `m >>= f` is `m.cost + (f m.ret).cost`.
```
protected def bind [Add C] (m : CostM C A) (f : A → CostM C B) : CostM C B :=
  let r := f m.ret
  ⟨r.ret, m.cost + r.cost⟩
```
def CostM.tick EconCSLib @ cef01c7, EconCSLib.Foundation.CostM
Charge a cost of `c`, returning unit. Use inside a `do`-block.
```
def tick (c : C) : CostM C PUnit := ⟨.unit, c⟩
```

instance CostM.instMonad EconCSLib @ cef01c7, EconCSLib.Foundation.CostM

instance instMonad [Zero C] [Add C] : Monad (CostM C) where
  pure := Pure.pure
  bind := Bind.bind
  map := Functor.map
  seq := Seq.seq
  seqLeft := SeqLeft.seqLeft
  seqRight := SeqRight.seqRight

instance CostM.instLawfulMonad EconCSLib @ cef01c7, EconCSLib.Foundation.CostM
`CostM C` is a lawful monad whenever `C` is an additive monoid.
```
instance instLawfulMonad [AddMonoid C] : LawfulMonad (CostM C)
```

def CostM.Bounded EconCSLib @ cef01c7, EconCSLib.Foundation.CostM

The cost of `alg i` is bounded by `bound (size i)` for every input `i`.

def Bounded {Input Output : Type*} [LE C]
    (alg : Input → CostM C Output) (size : Input → ℕ) (bound : ℕ → C) : Prop :=
  ∀ i, (alg i).cost ≤ bound (size i)

def CostM.IsPolyBounded EconCSLib @ cef01c7, EconCSLib.Foundation.CostM

Specialization of `Bounded` for `C = ℕ`: cost is polynomial in input size.

def IsPolyBounded {Input Output : Type*}
    (alg : Input → CostM ℕ Output) (size : Input → ℕ) : Prop :=
  ∃ c k, Bounded alg size (fun n => c * n^k)

Modules: EconCSLib.Foundation.CostM

The CostM Complexity Monad

CostM C α is the writer monad over an arbitrary additive monoid C: a return value of type α paired with an accumulated cost in C, $$ \mathrm{CostM}\,C\,\alpha \;=\; \alpha \times C. $$ Sequential composition (bind, written >>=) adds the cost components, $$ \mathrm{bind}(m, f).\mathrm{cost} \;=\; m.\mathrm{cost} \,+\, (f\,m.\mathrm{ret}).\mathrm{cost}, \qquad (\mathrm{pure}\,a).\mathrm{cost} = 0, $$ so a program's total cost is the monoid-sum of the costs charged along its execution.

The cost type C is deliberately abstract: choosing C is what selects the resource being measured, while the monad is identical for all of them.

C := ℕ (additive) — count comparisons, recursive calls, modulus operations: the conventional "time" instance.
C := A × B — track two additive costs at once via Prod.instAddMonoid.
C := Visited α (idempotent, s + s = s) — the set of subproblems touched; the algebraic shadow of memoization. See Memoization Footprint via the Visited Monoid.
C := Cells (tropical peak/delta) — peak memory, the one resource shape additive cost fundamentally cannot express. See Peak-Memory Cost via the Cells Monoid.

Discipline: cost annotations are trusted

The elaborator does not verify that tick calls correspond to real work. Each algorithm file documents its own cost model — what a unit is, what is free, whether recursive calls are charged — and the author ticks accordingly. Proofs then separate cleanly along the two structure fields:

functional correctness lives on m.ret (alias ⟪m⟫);
complexity bounds live on m.cost.

The two are independent: changing the cost model never disturbs a correctness proof, and refactoring the algorithm preserves cost annotations by construction. The Boyer–Moore example (Worked Example: Constant-Space Boyer–Moore Majority) proves a cost bound while deliberately not proving correctness, to exhibit the decoupling.