Skip to content

Commit dd4f543

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
docs: add FOUNDATIONS_BRIDGE.md downstream integration brief
Proof-free brief consolidating the echo-types (residual-modality) and tropical-resource-typing (resource-grade) FOUNDATION_CONTRACT.md files for downstream consumers (my-lang et al.): two independent axes, the one-directional ResidueMeasure seam, import pattern, vocabulary, and boundary invariants. Adds no new proofs. Licence per owner directive: MPL-2.0 AND CC-BY-SA-4.0. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 70673fa commit dd4f543

1 file changed

Lines changed: 179 additions & 0 deletions

File tree

‎FOUNDATIONS_BRIDGE.md‎

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
1+
<!--
2+
SPDX-License-Identifier: MPL-2.0 AND CC-BY-SA-4.0
3+
SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
4+
Licence is owner-directed: MPL-2.0 (code) and CC-BY-SA-4.0 (documentation),
5+
applied across echo-types, tropical-resource-typing, and any my-lang consumer.
6+
A downstream repo under a different licence policy should have this header
7+
reset by the owner (manual, file-by-file).
8+
-->
9+
10+
# Foundations bridge — consuming `echo-types` and `tropical-resource-typing`
11+
12+
This is a downstream integration brief for `my-lang` or any other consumer of
13+
the two foundations. It coordinates their outputs; it **adds no new proofs**.
14+
Every theorem named below is already mechanised upstream — this document only
15+
tells a downstream language *how to depend on the two foundations without
16+
collapsing them into each other*.
17+
18+
Source of truth:
19+
20+
| Foundation | Axis exported | Contract | Machine-checked in |
21+
|---|---|---|---|
22+
| `tropical-resource-typing` | resource-grade axis | `FOUNDATION_CONTRACT.md` | Lean 4 `Resource.*` |
23+
| `echo-types` | residual-modality axis | `FOUNDATION_CONTRACT.md` | Agda `Echo.*` (`--safe --without-K`) |
24+
25+
---
26+
27+
## 1. Two independent axes
28+
29+
A consumer tracks **two orthogonal things**. They are not refinements of one
30+
another and they meet only at the one-directional seam in §2.
31+
32+
> The numbering (`1`, `3`) follows the upstream axis taxonomy. Only these two
33+
> axes are in scope for this brief; they are mutually independent at the core.
34+
35+
### Axis 1 — Resource algebra (`tropical-resource-typing`)
36+
37+
- **What it is:** binder/resource *quantities* — usage, cost, latency, critical
38+
path, bottleneck — living in an ordered-semiring / usage-algebra interface.
39+
- **Interface:** `Resource.ResourceAlgebra` (= `Resource.ResourceSemiring` + an
40+
order). `⊞` = choice/alternative, `⊠` = sequential composition.
41+
- **Instances:** `Resource.Instances.{Linear, Affine, MaxPlus, MinPlus, MinMax}`
42+
— i.e. linear / affine usage and the tropical (max-plus / min-plus / min-max)
43+
algebras. The tropical instances double as an **infinite-carrier stress test**
44+
(`Resource.Stress`, `Resource.Infinite`).
45+
- **Used by:** QTT-style / quantitative **resource soundness**. Prove soundness
46+
*parametrically* over the interface via `Resource.ConsumerLawBundle`
47+
(`parametric_resource_transport`, alias `resource_laws_sufficient_for_consumers`),
48+
then instantiate at any algebra above with no algebraic re-proof.
49+
50+
### Axis 3 — Echo modality (`echo-types`)
51+
52+
- **What it is:** structured **residue / loss / forgetting / projection** — the
53+
remainder of an information-losing map, `Echo f y := Σ (x : A), (f x ≡ y)`.
54+
- **Indexed by a thin poset:** `Echo.Index.ThinPoset`; the canonical index is the
55+
three-point loss order `keep ≤ residue ≤ forget` (`grade-thinPoset`). Thinness
56+
(order proofs are propositional) is load-bearing, not cosmetic.
57+
- **Proves residual metatheory:** `Echo.Modality.Core` /
58+
`Echo.Modality.Interface` give `degrade`, the unit law `degrade-id`, the
59+
path-independence law `degrade-compose`, and the no-section theorem
60+
`no-section-of-collapsing-map`; the downstream-instantiable record is
61+
`EchoModality` (canonical witness `grade-echoModality`).
62+
- **Independent of the resource algebra at the core:** `Echo.Modality.Core`,
63+
`Echo.Modality.Interface`, and `Echo.Index.ThinPoset` import **no**
64+
semiring / resource-algebra machinery. The proof-relevant content of `degrade`
65+
is carried by the thin order of the index, not by any semiring-valued grade.
66+
67+
---
68+
69+
## 2. The seam
70+
71+
The only sanctioned connection between the axes is a **measure**, pointing in
72+
exactly one direction:
73+
74+
```
75+
ResidueMeasure : Echo residue ──▶ ResourceAlgebra carrier
76+
```
77+
78+
- **Direction:** a resource algebra is *consumed as a measure by* Echo. The
79+
residue carrier is opaque; only the codomain is a resource algebra.
80+
- **Never the reverse:** Echo is **not** produced as a resource instance, nor as
81+
a `Soundness(R)` instance.
82+
83+
The seam is mechanised on both sides — pick whichever framing matches your
84+
downstream proof obligation; both fix the same `E → R` direction:
85+
86+
**echo-types side (order-monotone view)** — `Echo.Measure.Interface`:
87+
88+
```agda
89+
record ResidueMeasure (E : EchoModality P ℓc) (R : OrderedCarrier ℓm ℓo) where
90+
field
91+
measure : ∀ {i} → ⟦ i ⟧ → Carrier R
92+
monotone : ∀ {i j} (p : i ≤ j) (x : ⟦ i ⟧) →
93+
measure x ≤R measure (degrade p x)
94+
```
95+
96+
**tropical side (monoid-homomorphism view)** — `Resource.EchoBridge`:
97+
98+
```lean
99+
structure ResidueMeasure (E : Type) (R : Type) [ResourceAlgebra R] where
100+
combine : E → E → E -- Echo-side residue accumulation (opaque)
101+
empty : E
102+
measure : E → R -- the measurement into a resource grade
103+
measure_empty : measure empty = one
104+
measure_combine : ∀ e₁ e₂, measure (combine e₁ e₂) = measure e₁ ⊠ measure e₂
105+
```
106+
107+
In both, the residue carrier `E` carries **no** `ResourceAlgebra` instance and
108+
nothing gives it one. `echo-types` and `tropical-resource-typing` have **no
109+
dependency on each other**; the seam is supplied downstream.
110+
111+
---
112+
113+
## 3. Downstream import pattern
114+
115+
A consuming language (e.g. `my-lang`) should expose:
116+
117+
```
118+
Resource parameter R : ResourceAlgebra -- Axis 1
119+
Echo parameter E : EchoModality -- Axis 3
120+
Optional seam M : ResidueMeasure E R -- §2, only if you measure residues
121+
```
122+
123+
Prove resource soundness against `R` parametrically (quote
124+
`Resource.ConsumerLawBundle`), instantiate Echo at your own fibration via
125+
`EchoModality`, and reach for `M` *only* when you genuinely measure residues.
126+
127+
It should **not** introduce any of:
128+
129+
- ✗ Echo as an instance of `ResourceAlgebra`
130+
- ✗ Echo as an instance of `Soundness(R)` (resource soundness)
131+
- ✗ Tropical (any of the resource instances) as an Echo modality
132+
133+
These three are exactly the collapses the foundations are built to prevent.
134+
135+
---
136+
137+
## 4. Vocabulary
138+
139+
Use these three terms precisely — they name three orthogonal things:
140+
141+
| Use | Meaning |
142+
|---|---|
143+
| **resource grade** | a binder/resource quantity on the resource-algebra axis (Axis 1) |
144+
| **echo index** | an inhabitant of the thin-poset index of the Echo modality, e.g. `keep ≤ residue ≤ forget` (Axis 3) |
145+
| **residue measure** | a resource-algebra-valued *observation* of an Echo residue (the §2 seam) |
146+
147+
**Avoid / deprecate `echo-grade`.** It ambiguously fuses the *echo index* (the
148+
retention axis of the modality) with the *resource grade* (the semiring axis) —
149+
which is precisely the collapse this bridge forbids. If the term must be
150+
explained, explain it as that ambiguity.
151+
152+
---
153+
154+
## 5. Boundary invariants
155+
156+
These hold as mechanised upstream results; downstream code must not violate them.
157+
158+
1. **Echo IS-NOT a resource instance.** Do not model Echo as a `Soundness(S)` /
159+
resource-algebra instance. (Upstream: `Echo.Separation.NotResourceInstance`;
160+
the proof-relevant Echo structure is carried by thinness of the index, not by
161+
any semiring grade.)
162+
2. **Tropical IS a resource-algebra instance.** Max-plus / min-plus / min-max are
163+
instances of `Resource.ResourceAlgebra` and belong on the resource-grade axis
164+
— they are not Echo modalities.
165+
3. **Residue measures are observations, not definitions of Echo.** A
166+
`ResidueMeasure` is a lossy, one-directional read-out; `Echo.Modality.Core`
167+
never depends on it, and never may.
168+
4. **Equal residue measure does not imply equal Echo.** A measure can send two
169+
genuinely-distinct Echo residues to the same value while the modality keeps
170+
them apart — so no measure is the identity criterion of Echo. (Upstream:
171+
`equal-measure-does-not-imply-equal-echo`, and the sharper informative-measure
172+
witness `equal-informative-measure-does-not-imply-equal-echo`.)
173+
174+
---
175+
176+
*This brief restates the two `FOUNDATION_CONTRACT.md` files for the downstream
177+
direction and adds nothing to them. For the full contracts and the parametric
178+
transport / anti-collapse theorems, read each foundation's `FOUNDATION_CONTRACT.md`
179+
and (tropical) `docs/ECHO-RESIDUE-BRIDGE.adoc`.*

0 commit comments

Comments
 (0)