Lean declarations

def Visited EconCSLib @ cef01c7, EconCSLib.Foundation.CostM.Visited
```
def Visited (A : Type*) : Type _ := Finset A
```
def Visited.toFinset EconCSLib @ cef01c7, EconCSLib.Foundation.CostM.Visited
View a `Visited A` as the underlying `Finset A`.
```
def toFinset (v : Visited A) : Finset A := v
```
def Visited.ofFinset EconCSLib @ cef01c7, EconCSLib.Foundation.CostM.Visited
View a `Finset A` as a `Visited A`.
```
def ofFinset (s : Finset A) : Visited A := s
```
def Visited.singleton EconCSLib @ cef01c7, EconCSLib.Foundation.CostM.Visited
Mark a single sub-problem `a` as visited.
```
def singleton (a : A) : Visited A := ({a} : Finset A)
```

Modules: EconCSLib.Foundation.CostM.Visited

Memoization Footprint via the Visited Monoid

Visited α is the cost monoid that records the set of subproblems touched by a recursive algorithm. It is Finset α with union as addition and the empty set as zero: $$ s + t = s \cup t, \qquad 0 = \varnothing. $$ The defining feature is idempotence, s + s = s: revisiting a subproblem adds nothing. This is the algebraic shadow of memoization — under a memo table the second visit is free, so the cost (the footprint) is exactly the set of distinct subproblems, not the number of calls. A memoized algorithm's .cost is therefore the set of table entries it fills.

Visited α is a type synonym for Finset α (def Visited α := Finset α), introduced specifically to firewall Mathlib's scoped pointwise Zero (Finset α) instance: the cost-monoid 0 = ∅ and + = ∪ must not collide with pointwise arithmetic on finsets. toFinset/ofFinset move across the synonym boundary.