Lean declarations

def ParSum.parSum EconCSLib @ cef01c7, EconCSLib.Examples.CostM.ParSum
```
def parSum (xs : List ℕ) : CostM ℕ ℕ
```

theorem ParSum.parSum_cost_le_clog EconCSLib @ cef01c7, EconCSLib.Examples.CostM.ParSum

theorem parSum_cost_le_clog (xs : List ℕ) :
    (parSum xs).cost ≤ Nat.clog 2 xs.length

theorem ParSum.parSum_cost_le_length EconCSLib @ cef01c7, EconCSLib.Examples.CostM.ParSum
Loose linear upper bound on parallel-sum depth.
```
theorem parSum_cost_le_length (xs : List ℕ) :
    (parSum xs).cost ≤ xs.length
```

Modules: EconCSLib.Examples.CostM.ParSum

Worked Example: Balanced Parallel Sum Depth

A divide-and-conquer list sum built from par (Parallel Composition in CostM), where cost is combined by ⊔ so that .cost measures parallel depth, not total work. Splitting the list in half and summing the halves in parallel gives a logarithmic depth, $$ (\operatorname{parSum}\,xs).\mathrm{cost} \;\le\; \lceil \log_2 |xs| \rceil, $$ i.e. parSum_cost_le_clog (Nat.clog 2 xs.length). The coarser linear bound parSum_cost_le_length is also provided. This is the depth-side counterpart of the additive-work examples: the same algorithm under + would cost O(n), but under ⊔ the independent branches overlap and only the tree height counts.