tropical-types/Resource.lean at main · hyperpolymath/tropical-types · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
-- SPDX-License-Identifier: MPL-2.0
-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
import Resource.Algebra.Interface
import Resource.Algebra.Ordered
import Resource.Algebra.Dioid
import Resource.Algebra.ParametricLaws
import Resource.Instances.Linear
import Resource.Instances.Affine
import Resource.Instances.MaxPlus
import Resource.Instances.MinPlus
import Resource.Instances.MinMax
import Resource.Stress
import Resource.EchoBridge
import Resource.Conformance
import Resource.Bridge
import Resource.Closure

/-!
  # `Resource` — the resource-grade axis (aggregator)

  Author: Jonathan D.A. Jewell (hyperpolymath)
  Verified: Lean 4.13.0 (pinned via `lean-toolchain`), no Mathlib.

  This is the single import a downstream language (e.g. `my-lang`) needs to pick
  up the entire **resource-grade axis** that `tropical-resource-typing` exports.
  See `FOUNDATION_CONTRACT.md` for the boundary invariant and the consumer rule.

  ## Layers

  * `Resource.Algebra.Interface`     — `ResourceSemiring` (the algebra core).
  * `Resource.Algebra.Ordered`       — `ResourceAlgebra` (ordered + monotone),
                                        plus the `PartialOrdered…` refinement.
  * `Resource.Algebra.Dioid`         — canonical-order builder for idempotent
                                        (tropical) semirings; no carrier case-split.
  * `Resource.Algebra.ParametricLaws`— `ConsumerLawBundle` and the transport
                                        theorem `parametric_resource_transport`
                                        (alias `resource_laws_sufficient_for_consumers`).

  ## Instances (all satisfy the one `ResourceAlgebra` interface)

  | module                      | carrier            | `⊞` (choice) | `⊠` (seq) | finite? |
  | --------------------------- | ------------------ | ------------ | --------- | ------- |
  | `Resource.Instances.Linear` | `{0,1,ω}`          | usage-add    | scale     | yes     |
  | `Resource.Instances.Affine` | `{0,1,ω}`          | usage-add    | scale     | yes     |
  | `Resource.Instances.MaxPlus`| `ℕ ∪ {−∞}`         | `max`        | `+`       | NO      |
  | `Resource.Instances.MinPlus`| `ℕ ∪ {+∞}`         | `min`        | `+`       | NO      |
  | `Resource.Instances.MinMax` | `ℕ ∪ {+∞}`         | `min`        | `max`     | NO      |

  * `Resource.Stress`     — the tropical carriers are proved **infinite**.
  * `Resource.EchoBridge` — a resource algebra may *measure* opaque (Echo)
                            residues; Echo is **not** a resource instance.
  * `Resource.Conformance`— all five instances satisfy the one interface, and a
                            parametric consumer lemma instantiates at each.
  * `Resource.Bridge`     — the two original twins (`TropicalSessionTypes`,
                            `TropicalAdapterPath`) exhibited as instances of this
                            axis (QTT refinement and `hub_ceiling` restated in `⊑`).
  * `Resource.Closure`    — the Kleene / Floyd–Warshall all-pairs **closure**
                            layer (`Mat`, `matMul`, `matStar`), parametric over
                            `ResourceAlgebra`; instantiates at `MinPlus`
                            (all-pairs shortest path) and `MinMax` (all-pairs
                            bottleneck).  The `EntryBounded` / `AllPairsCosts`
                            certificate and `matStar` monotonicity mirror
                            `typed-wasm`'s Idris `Tropical.idr` onto the axis.
-/