|
| 1 | +<!-- |
| 2 | +SPDX-License-Identifier: MPL-2.0 |
| 3 | +Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 4 | +--> |
| 5 | +# Echo residue threading into TangleIR — cross-repo contract |
| 6 | + |
| 7 | +**Status:** design / coordination contract (2026-06-14). Authored in `tangle` |
| 8 | +(the semantics owner). The TangleIR type change and the QuandleDB consumer |
| 9 | +change live in **`KRLAdapter.jl`** (TangleIR definition + adapters) and |
| 10 | +**`quandledb`** — both Julia, outside this session's scope — so this file is |
| 11 | +the *contract* those repos implement, not the implementation. |
| 12 | + |
| 13 | +## 1. Why threading the residue matters |
| 14 | + |
| 15 | +Tangle's `close : Word[n] → Word[0]` is the canonical **lossy** map: it |
| 16 | +collapses a braid to the identity, discarding the word. Echo types |
| 17 | +(`proofs/Tangle.lean` §ECHO-TYPES; `compiler/lib/typecheck.ml`) make that loss |
| 18 | +recoverable — `echoClose b` retains the braid as a **residue**, and |
| 19 | +`residue (echoClose b) ⟶ b` (`echo_residue_recovers`). |
| 20 | + |
| 21 | +The seam with QuandleDB is exact, not incidental: |
| 22 | + |
| 23 | +> A **quandle presentation is an invariant of the knot**, and the knot is the |
| 24 | +> **closure of the braid**. `close` is precisely the braid→knot step. So the |
| 25 | +> residue retained by `echoClose` — the *pre-closure braid* — is exactly the |
| 26 | +> object `quandle_presentation(ir::TangleIR)::QuandlePresentation` derives the |
| 27 | +> quandle from. |
| 28 | +
|
| 29 | +`echo_distinguishes_collapsed` (Lean) says distinct braids can close to the |
| 30 | +same diagram while keeping distinct residues. Threading the residue therefore |
| 31 | +gives QuandleDB **provenance**: which braid produced a given closed diagram, |
| 32 | +disambiguating cases that plain `close` would conflate. |
| 33 | + |
| 34 | +## 2. The contract per layer |
| 35 | + |
| 36 | +| Layer | Repo | Responsibility | |
| 37 | +|---|---|---| |
| 38 | +| Semantics | `tangle` (this repo) | Defines echo types + residue semantics. `residue (echoClose b) = b`; `lower (echoClose b) = identity`. Mechanised in `proofs/Tangle.lean`; checked in `typecheck.ml` (`TEcho`/`TProd`, rules `[T-Echo-Close]`/`[T-Lower]`/`[T-Residue]`). | |
| 39 | +| Interchange | `KRLAdapter.jl` | TangleIR represents an echo-closed term **carrying the residue braid alongside the closed result** (see §3). A plain `close` node is unchanged (no residue). | |
| 40 | +| Consumer | `quandledb` | `quandle_presentation` reads the residue braid of an echo-closed node to compute the quandle (the pre-closure braid determines the knot). Plain-`close` behaviour unchanged. | |
| 41 | + |
| 42 | +## 3. Proposed TangleIR representation (for KRLAdapter.jl) |
| 43 | + |
| 44 | +Mirror the Lean `echoVal (residue, result)` shape. Two equivalent options; |
| 45 | +recommend (a): |
| 46 | + |
| 47 | +* **(a) Residue-carrying closure node.** Add an IR node |
| 48 | + `EchoClosed(residue::BraidWord, result::ClosedDiagram)` — the closed diagram |
| 49 | + plus the braid it came from. `lower`/`residue` IR projections read `.result` |
| 50 | + / `.residue`. This keeps the closed diagram identical to the plain-`close` |
| 51 | + output (so existing consumers are unaffected) while exposing the braid. |
| 52 | +* **(b) Residue as closure metadata.** Keep the existing closure node and attach |
| 53 | + the pre-closure braid as an optional metadata field |
| 54 | + (`residue::Union{BraidWord,Nothing}`). Lighter, but makes the residue |
| 55 | + optional rather than type-guaranteed — weaker than the Lean guarantee. |
| 56 | + |
| 57 | +Products (`Ty.prod` / `pair`/`fst`/`snd`) are the residue carrier for the |
| 58 | +binary lossy ops (`echoAdd`/`echoEq`): their residue is the **pair of operands**. |
| 59 | +If TangleIR needs to represent those, add a `Pair(a, b)` IR node with `fst`/`snd` |
| 60 | +projections. (For QuandleDB specifically, only the `echoClose` residue is |
| 61 | +knot-relevant; `echoAdd`/`echoEq` residues are scalar provenance.) |
| 62 | + |
| 63 | +## 4. Consumer contract (for quandledb) |
| 64 | + |
| 65 | +``` |
| 66 | +quandle_presentation(ir::TangleIR) = |
| 67 | + case ir of |
| 68 | + EchoClosed(residue, _result) -> quandle_of_braid(residue) # use the braid |
| 69 | + Close(diagram) -> quandle_of_diagram(diagram) # unchanged |
| 70 | + ... |
| 71 | +``` |
| 72 | + |
| 73 | +The invariant to preserve: for any braid `b`, |
| 74 | +`quandle_presentation(EchoClosed(b, close(b)))` ≡ |
| 75 | +`quandle_presentation(Close(close(b)))` whenever the closed diagram alone |
| 76 | +suffices — the residue path must agree with the diagram path on the quandle, |
| 77 | +and additionally retains `b` for provenance. This mirrors |
| 78 | +`echo_roundtrip_typed` (the residue/result projections are well-typed) and the |
| 79 | +`lower`/`residue` agreement in the Lean model. |
| 80 | + |
| 81 | +## 5. Scope / coordination |
| 82 | + |
| 83 | +- **No TangleIR or QuandleDB code is changed by this document.** Those are |
| 84 | + KRLAdapter.jl/quandledb (Julia) changes, to be made by the quandle session. |
| 85 | +- This contract is additive and conservative: plain `close` is untouched, so |
| 86 | + existing TangleIR producers/consumers keep working; echo-closed nodes are new. |
| 87 | +- Cross-reference: `proofs/Tangle.lean` (`echo_residue_recovers`, |
| 88 | + `echo_distinguishes_collapsed`, `echo_roundtrip_typed`), |
| 89 | + `.machine_readable/6a2/ECOSYSTEM.a2ml` (the echo↔quandle seam), |
| 90 | + and `quandledb`'s `quandle_presentation`. |
0 commit comments