Model.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.BoundedTreewidthL1.walkLength line 12
Source documentation
Sum of the given positive real edge lengths along a graph walk.
Also declared: ComparatorChallenges/BoundedTreewidthL1.lean:14 (same declaration text).
```
def walkLength (ℓ : G.edgeSet → ℝ) : {u v : V} → G.Walk u v → ℝ
  | _, _, .nil => 0
  | u, _, .cons (v := v) h p => ℓ ⟨s(u, v), h⟩ + walkLength ℓ p
```
def OAI.BoundedTreewidthL1.shortestPathDistance line 16
Also declared: ComparatorChallenges/BoundedTreewidthL1.lean:18 (same declaration text).
def OAI.BoundedTreewidthL1.HasTreeDecomposition line 19
Also declared: ComparatorChallenges/BoundedTreewidthL1.lean:21 (same declaration text).
def OAI.BoundedTreewidthL1.HasL1Embedding line 28
Source documentation
A map to genuine finite-dimensional real ℓ₁, not just a cut pseudometric.
Also declared: ComparatorChallenges/BoundedTreewidthL1.lean:30 (same declaration text).
```
def HasL1Embedding (ℓ : G.edgeSet → ℝ) (C : ℝ) : Prop :=
…
```
def OAI.BoundedTreewidthL1.MainStatement line 34
Also declared: ComparatorChallenges/BoundedTreewidthL1.lean:36 (same declaration text).