|
| 1 | +<!-- SPDX-License-Identifier: MPL-2.0 --> |
| 2 | +<!-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> --> |
| 3 | + |
| 4 | +# my-lang Axis Architecture — the proof-factoring map |
| 5 | + |
| 6 | +**Status:** active · **Created:** 2026-06-13 · **Owner:** @hyperpolymath |
| 7 | + |
| 8 | +This is the conceptual parent of [`ALIGNMENT-PLAN.md`](./ALIGNMENT-PLAN.md) (the phased |
| 9 | +roadmap) and [`STATUS.md`](./STATUS.md) (what is actually proved). It records *how the |
| 10 | +proof effort factors* and the **one invariant that must not erode**. |
| 11 | + |
| 12 | +> The mechanised solo-core (Coq, axiom-free `progress`/`preservation`) is **one rung on one |
| 13 | +> axis**. The architecture below explains why the other work is not "more of the same." |
| 14 | +
|
| 15 | +--- |
| 16 | + |
| 17 | +## 1. Four orthogonal axes |
| 18 | + |
| 19 | +my-lang factors into four axes that compose but **must not be collapsed into each other**. |
| 20 | +Each factors *differently* — the design mistake would be a single strategy (all top-down or |
| 21 | +all bottom-up) for what are genuinely different kinds of structure. |
| 22 | + |
| 23 | +``` |
| 24 | + AXIS MEMBERS HOW IT FACTORS DIRECTION |
| 25 | + ─────────────────────────────────────────────────────────────────────────────────────── |
| 26 | + 1 RESOURCE linear {0,1,ω} · affine CUT ACROSS parametric |
| 27 | + (quantity) {0,?,1,ω} · tropical max-plus prove Soundness ONCE (the "bridge") |
| 28 | + (cost) · min-max (bottleneck) over a semiring → |
| 29 | + the rest are INSTANCES |
| 30 | + 2 STRUCTURE solo (λ/QTT) ⊂ duet (sessions) STACK, asymmetric bottom-up solo; |
| 31 | + (judgements) ⊂ ensemble (π-calculus) duet ⊂ ensemble (project) ensemble-first |
| 32 | + but solo ⊄ ensemble on process side |
| 33 | + 3 MODALITY echo (loss-grading) SEPARATE LAYER own metatheory |
| 34 | + (graded poset) thin poset; own theorems (foundations repo) |
| 35 | + (no-section, degrade-comp) |
| 36 | + 4 SURFACE me (visual / blocks) FREE (elaboration) desugar → solo, |
| 37 | + adequacy lemma, not new reuse soundness |
| 38 | + progress/preservation |
| 39 | +``` |
| 40 | + |
| 41 | +Key structural facts (verified 2026-06-13): |
| 42 | +- **`solo ⊄ ensemble`** — the sequential QTT λ-calculus is *not* a fragment of the |
| 43 | + π-calculus; a top-down "pivot to ensemble" would **not** subsume solo. Keep solo as the |
| 44 | + proven foundation; do the *process* side top-down (ensemble-first, recover duet by |
| 45 | + projection). |
| 46 | +- **`me` is surface, not metatheory** — covering it is an elaboration-correctness lemma over |
| 47 | + the already-proven solo core, not a fresh soundness proof. |
| 48 | + |
| 49 | +--- |
| 50 | + |
| 51 | +## 2. Vocabulary — "echo-grade" is **deprecated** |
| 52 | + |
| 53 | +The phrase "echo-grade" straddles two different things and invites the resource and modality |
| 54 | +axes to re-collapse. Use exactly three terms: |
| 55 | + |
| 56 | +| Term | Axis | Meaning | |
| 57 | +|------|------|---------| |
| 58 | +| **resource grade** | 1 | the `q` annotating a binder: usage / cost / latency — linear, affine, tropical | |
| 59 | +| **echo index** | 3 | the thin-poset modality index: `keep ≤ residue ≤ forget` (and `linear ⊑ affine`) | |
| 60 | +| **residue measure** | seam | a semiring-valued *observation* attached to a residue | |
| 61 | + |
| 62 | +Directionality: resource algebras are **produced** by the semiring functor; the echo layer |
| 63 | +**consumes** one as a measure. Echo never *produces* a `Soundness` instance. |
| 64 | + |
| 65 | +--- |
| 66 | + |
| 67 | +## 3. The invariant — **Echo IS-NOT a resource instance** |
| 68 | + |
| 69 | +> *Echo Types, as currently intended and mechanised, are not an instance of the my-lang |
| 70 | +> resource/Soundness functor. Any semiring encoding would be a lossy measure or quotient, |
| 71 | +> not the Echo foundation itself.* |
| 72 | +
|
| 73 | +This is load-bearing; treat it as an estate IS-NOT registry entry. **Why it holds:** |
| 74 | + |
| 75 | +1. **Category.** `Soundness(S)` is QTT λ-calculus progress/preservation over a *usage* |
| 76 | + algebra `S`. Echo's grades are not usage counts; Echo's theorems (no-section, |
| 77 | + degrade-compose) need *thinness* (`≤g-prop`, a poset fact), not a semiring. An "echo |
| 78 | + instance of `Soundness`" is ill-typed against the interface, or proves the wrong theorem. |
| 79 | +2. **Mechanised separation (in echo-types).** `sep-degrade-compose-fails`: drop thinness and |
| 80 | + you get a *checked* `true ≢ false`. Plus the matched-negative that the entropy / numeric |
| 81 | + **shadow is blind where Echo distinguishes**. Encoding Echo as a semiring shadow is itself |
| 82 | + a lossy collapse — the shadow is a *residue* of Echo, not Echo. *Backing artifacts (echo-types):* |
| 83 | + `echo.index.thinposet`, `echo.modality.core`, and `echo.separation.notresourceinstance`. |
| 84 | + |
| 85 | +**Interaction, not identification.** The axes couple at exactly one seam: |
| 86 | + |
| 87 | +``` |
| 88 | + ResourceAlgebra R -- axis 1 (semiring) |
| 89 | + EchoModality E -- axis 3 (thin poset) |
| 90 | + Measure : Residue E → R -- the ONLY coupling |
| 91 | +``` |
| 92 | + |
| 93 | +Echo core stays **measure-independent**; `Cost` / `Prob` / `Tropical` are decorations *at the |
| 94 | +seam*. (cf. `!` kept distinct from the multiplicatives in linear logic, related by precise |
| 95 | +rules.) Tropical proves the quantity axis is real; echo proves the modality axis is real; |
| 96 | +my-lang is parametric over **both**, and identifies **neither**. |
| 97 | + |
| 98 | +--- |
| 99 | + |
| 100 | +## 4. The proof ladder (rungs + dependencies) |
| 101 | + |
| 102 | +`✓` done · `◑` in flight · `☐` open. See `STATUS.md` for the authoritative per-artefact state. |
| 103 | + |
| 104 | +``` |
| 105 | + LANGUAGE THREAD (this repo) FOUNDATIONS THREAD(S) (sibling repos) |
| 106 | + ───────────────────────────────────── ────────────────────────────────────── |
| 107 | + R0 ✓ solo progress + preservation (Coq, ECHO (echo-types, Agda) |
| 108 | + axiom-free) E1 ☐ Buchholz ordinal global WF (10/13 |
| 109 | + ──bridge── → close or fence) |
| 110 | + R1 ✓ q_reassoc de-concretise (now SoloCore.v) E2 ☐ (epi,mono) image factorisation — |
| 111 | + R2 ✓ SEMIRING functor; Include Linear3 = decide the 1 truncation postulate |
| 112 | + R0, axiom-free (consolidated) E3 ☐ proof-CI gate (agda --safe) |
| 113 | + R3 ☐ ORDERED_SEMIRING + subusage rule → E4 ☐ SEAM: Measure : Residue E → R, |
| 114 | + Affine4 (affine_pres becomes DISTINCT, echo core proven measure-INDEP |
| 115 | + not an alias) ── makes "affine" real E5 ☐ Pillar E paper write-up |
| 116 | + R4 ☐ Tropical instance (cost) ── acceptance |
| 117 | + test: infinite carrier, analytic laws TROPICAL (tropical-resource-typing, Lean/Isabelle) |
| 118 | + R5 ☐ static-split ≡ usage-walk (F1.4 tail) T1 ☐ independently re-verify Isabelle 2025-1 |
| 119 | + ── linchpin for a VERIFIED checker T2 ☐ session ext: choice / recursion / multiparty |
| 120 | + ──parity / surface── T3 ☐ firm the Lean↔Isabelle cross-links |
| 121 | + P1 ☐ Idris twin of solo (close ?todo) + T4 ☐ WithTop ∞ (drop tcZero=1e6 hack) |
| 122 | + mirror subst2 fix + parametric design |
| 123 | + M1 ☐ me elaboration-correctness (→ solo) SEAM CAPSTONE (joint): E4 needs R2 (a SEMIRING) |
| 124 | + ──structure climb (last, hardest)── + a solid echo core. It is where "interaction, |
| 125 | + S1 ☐ ensemble π metatheory (subject red., not identification" becomes a theorem. |
| 126 | + session fidelity) |
| 127 | + S2 ☐ duet = ensemble │2-party (by projection, |
| 128 | + falls out of S1) |
| 129 | +``` |
| 130 | + |
| 131 | +Dependency spine: `R0 → R1 → R2 → {R3, R4} ; R3 → R5` ; `R2 + echo-core → E4` ; `S1 → S2`. |
| 132 | +`P1`, `M1`, and the foundations ladders run **in parallel** with the bridge. |
| 133 | + |
| 134 | +### 4.1 Progress — 2026-06-13 |
| 135 | + |
| 136 | +- **R1 done.** `q_reassoc` (`Soundness.v`) is now derived from the named semiring laws |
| 137 | + (`qmul_distrib_l/r`, `qmul_assoc`, `qadd_assoc/comm`), not a 729-case carrier |
| 138 | + enumeration. `progress`/`preservation`/`affine_pres` re-verified axiom-free. |
| 139 | +- **R2 boundary drafted.** `ResourceAlgebra.v` defines `Module Type SEMIRING` — the **10 |
| 140 | + equational laws the functorised proof consumes** — plus an inert `ORDERED_SEMIRING` |
| 141 | + extension, and validates them via `Module Linear3 <: SEMIRING` (reusing `Quantity`) and |
| 142 | + a sealed `Linear3_Sealed : SEMIRING`. The contract is machine-pinned: **`qle`, |
| 143 | + `qmul_comm` and `qmul_one_r` are provably absent** — grade *addition* must be commutative |
| 144 | + (the separated-context payoff), but grade *multiplication need not be*, and the order is |
| 145 | + inert until a subusage rule exists. *Remaining (R2 proper):* functorize `Soundness` over |
| 146 | + `SEMIRING`. |
| 147 | +- **The 10th law (`qmul_zero_l`) — functorisation audit, 2026-06-13.** The first boundary |
| 148 | + draft listed nine laws and excluded `qmul_zero_l`. An adversarial abstract-carrier probe |
| 149 | + of `Soundness.v:1022-1028` (`uadd_uscaleZero_r`, on the live preservation path via |
| 150 | + `hv_subst`/`ht_subst`) showed `uscale Zero` leaves `qmul zero qe` **irreducible** without |
| 151 | + it: the concrete proof only closed because `simpl` computes it on `|Q|=3`. So |
| 152 | + `qmul_zero_l` is required *for the abstraction* (it joins `qadd_zero_l`, already named for |
| 153 | + the same simpl-reduction reason) and is now the 10th `SEMIRING` law — discharged |
| 154 | + axiom-free by `Quantity.qmul_zero_l`. `qmul_comm`/`qmul_one_r` stay out (reached by |
| 155 | + neither citation nor reduction). |
| 156 | +- **Diffusion finding (adversarial audit).** `|Q|=3` is **not** isolated at `q_reassoc` — |
| 157 | + the `Quantity.v` laws are themselves carrier enumerations reached independently. So |
| 158 | + carrier-abstraction requires the Module-Type lift (each instance supplies its own laws); |
| 159 | + there is no single-seam shortcut. |
| 160 | +- **Functorisation strategy — Coq generativity, probe-verified 2026-06-13.** Coq module |
| 161 | + functors are **generative for inductives**: re-applying `SyntaxF M` inside a downstream |
| 162 | + `UsageF` yields a *different* `ty` (verified — `probe1` fails). So the naïve "each file is |
| 163 | + `Module F (M:SEMIRING)`, chained by re-application" is broken. Two paths share inductives |
| 164 | + (both probe-verified): **consolidated** (one functor spanning Syntax+Usage+Typing+Soundness, |
| 165 | + instantiated once) or **signature-threaded** (each layer's instance passed as a module |
| 166 | + parameter via a per-layer `Module Type`). |
| 167 | +- **R2 DONE — consolidated, executed 2026-06-13.** The four chain files are merged into |
| 168 | + `SoloCore.v` as `Module SoloCoreF (M : SEMIRING)`; `Include SoloCoreF Linear3` recovers |
| 169 | + `progress`/`preservation`/`affine_pres` **axiom-free** (`Print Assumptions` closed; clean |
| 170 | + rebuild + CI updated). What made it near-mechanical: `Import M` resolves every operator/law |
| 171 | + name to `M`'s fields, and `Local Notation Zero/One` re-aliases the two literal tokens |
| 172 | + (single-token identifiers like `uadd_uscaleZero_r` untouched). Only **five** sites needed |
| 173 | + real fixes, each where the abstract carrier no longer computes `qmul`/`qadd` on literals: |
| 174 | + `uscale_one` (qmul_one_l), `uadd_zero_l` (qadd_zero_l), `uadd_ushift` (qadd_zero_r), the |
| 175 | + left-annihilation `qmul zero qe` in `uadd_uscaleZero_r` (qmul_zero_l — the 10th law), and a |
| 176 | + `qadd_zero_r`-before-`congruence` in `subst2_lemma`. `Context.v`/`ContextProps.v` (dead |
| 177 | + branch, kept concrete on `Quantity`) and `EchoResidue.v` were repointed to `SoloCore`; the |
| 178 | + *transparent* `Linear3` (never `Linear3_Sealed`) keeps the concrete re-export compatible. |
| 179 | + `SoloCoreF` is now ready to instantiate at tropical/affine algebras (R4). |
| 180 | +- **Echo side (echo-types):** `echo.index.thinposet`, `echo.modality.core`, and |
| 181 | + `echo.separation.notresourceinstance` are done. The Coq `EchoMode.v` / `EchoResidue.v` / |
| 182 | + `TEcho` are already **`Quantity`-independent**, so the measure seam can attach without |
| 183 | + disturbing the resource layer. *Seam prerequisite:* `EchoResidue.v` currently exposes |
| 184 | + residues *operationally* (via the `Weaken` rule), not as an algebra with a composition |
| 185 | + operator — naming that algebra is the gating step before `Measure : Residue → R`. |
| 186 | + |
| 187 | +--- |
| 188 | + |
| 189 | +## 5. Pointers |
| 190 | +- Phased roadmap: [`ALIGNMENT-PLAN.md`](./ALIGNMENT-PLAN.md) (AffineScript parity). |
| 191 | +- Authoritative status: [`STATUS.md`](./STATUS.md). |
| 192 | +- Working brief / handoff seed (off-repo): `~/developer/dev-notes/my-lang/MY-LANG-FOUNDATIONS-BRIEF.md`. |
| 193 | +- Foundations: `hyperpolymath/echo-types` (axis 3), `hyperpolymath/tropical-resource-typing` (axis 1 witness). |
0 commit comments