|
| 1 | += D-2026-05-20 — Gate 1 adjacency refresh (cross-check against current taxonomy) |
| 2 | +:toc: macro |
| 3 | +:toclevels: 2 |
| 4 | +:sectnums: |
| 5 | +:sectnumlevels: 2 |
| 6 | +:icons: font |
| 7 | + |
| 8 | +[.lead] |
| 9 | +Coherence pass requested by `roadmap.md` § "Theory work" item |
| 10 | +"Gate 1 adjacency refresh: the five existing adjacency notes |
| 11 | +predate the taxonomy. Cross-check each against the current axes |
| 12 | +and flag any neighbour whose identity claim should be |
| 13 | +re-evaluated." This note is the refresh artefact. It does *not* |
| 14 | +rewrite any adjacency note in place; it issues a per-note |
| 15 | +verdict against the post-2026-05 taxonomy and lists the |
| 16 | +follow-up rewrites that any *re-evaluate* verdict would trigger. |
| 17 | + |
| 18 | +toc::[] |
| 19 | + |
| 20 | +== The five notes |
| 21 | + |
| 22 | +The five adjacency notes named by the roadmap entry are the |
| 23 | +original neighbour set indexed in |
| 24 | +`docs/gate-1-distinct-phenomenon.adoc` § "Neighbouring theories" |
| 25 | +and `docs/adjacency/README.adoc` § "File index". They predate |
| 26 | +both axis 2 (formalised 2026-04-27 in `EchoApprox.agda`) and |
| 27 | +axis 8 (promoted to a numbered axis 2026-04-28, with the first |
| 28 | +Agda artefact `EchoDecidable.agda` landing then and the graded |
| 29 | +`EchoAccess.agda` thin slice landing 2026-05-20). Two further |
| 30 | +notes (`modal-type-theories.adoc`, `hott-fibers.adoc`) were |
| 31 | +added after the original five and are explicitly excluded from |
| 32 | +this refresh — see `gate-1-distinct-phenomenon.adoc` lines |
| 33 | +54–63. |
| 34 | + |
| 35 | +. *`quotients.adoc`* (`docs/adjacency/quotients.adoc`, lines 1–137). |
| 36 | + Claim: echo is distinct from quotient types / setoid quotients |
| 37 | + because echo retains witness identity that quotients collapse |
| 38 | + (truncation argument) *and* because the natural 2-cells in |
| 39 | + sophisticated quotient encodings — equalizer, join-of-kernels, |
| 40 | + indexed coherence families — are themselves Σ-over-preimages |
| 41 | + (2-cell argument). Both arguments formally exhibited |
| 42 | + (`EchoVsQuotient.Sophisticated` + the gate-3 |
| 43 | + `echo-not-prop` family). |
| 44 | + |
| 45 | +. *`galois-connections.adoc`* (lines 1–158). Claim: echo is |
| 46 | + distinct from Galois connections / abstract interpretation |
| 47 | + because the natural 2-cell in the abstraction lattice — the |
| 48 | + meet of two abstractions — is structurally Σ-over-preimages |
| 49 | + with a paired predicate, and because the powerset-on-the- |
| 50 | + concrete-side framing of Galois cannot reproduce the |
| 51 | + witness-identity content (`EchoVsGalois.Sophisticated`, |
| 52 | + `meet→echo-intersection`, `meet-on-diagonal→equalizer`). |
| 53 | + |
| 54 | +. *`refinement-types.adoc`* (lines 1–209). Narrow claim: echo |
| 55 | + coincides with Σ-relevant refinement types (Agda, Coq — these |
| 56 | + *are* echo) and is distinct from propositional-predicate |
| 57 | + refinement (F*, Liquid Haskell) via the truncation argument. |
| 58 | + Tied-case acknowledged explicitly. Formalisation via the |
| 59 | + gate-3 `echo-not-prop` exhibits; no dedicated |
| 60 | + `proofs/agda/adjacency/Refinement.agda`. |
| 61 | + |
| 62 | +. *`information-flow.adoc`* (lines 1–190). Split claim. Against |
| 63 | + relational IFC (Goguen-Meseguer lineage): distinct by |
| 64 | + `EpistemicUpdate.echo-not-prop` — the propositional |
| 65 | + equivalence-class formulation cannot carry the witness-identity |
| 66 | + content that programmable knowledge update needs. Against |
| 67 | + type-theoretic IFC variants: *open* — the recipe-level |
| 68 | + comparison has not been performed. No dedicated Agda |
| 69 | + formalisation. |
| 70 | + |
| 71 | +. *`provenance.adoc`* (lines 1–215). Claim: distinct against |
| 72 | + single-witness provenance via the *multiplicity argument* |
| 73 | + (distinguished from the truncation argument: "one witness was |
| 74 | + selected and the others were discarded as data", not "the |
| 75 | + predicate was reduced to a proposition"). Transitive |
| 76 | + provenance under composition reduces structurally to the |
| 77 | + indexed-families case (S-2). Multi-witness type-relevant |
| 78 | + provenance would be co-extensive with echo, mirroring the |
| 79 | + Σ-relevant refinement case. |
| 80 | + |
| 81 | +== The current taxonomy lens |
| 82 | + |
| 83 | +The taxonomy that the notes are being cross-checked against |
| 84 | +(`docs/echo-types/taxonomy.md`, refreshed through 2026-05-20) |
| 85 | +is now eight numbered axes plus three open candidates. The |
| 86 | +five distinctness claims sit in a richer axis-space than they |
| 87 | +were originally written against: |
| 88 | + |
| 89 | +* *Axis 1 — extensional vs intensional.* Stable from inception. |
| 90 | + Every "echo retains witness identity" claim in the notes |
| 91 | + factors through this axis: the loss the notes are arguing |
| 92 | + *against* is collapse to the extensional shadow. |
| 93 | +* *Axis 2 — exact vs approximate* (formalised in |
| 94 | + `EchoApprox.agda`; ε-fibre over a `Tolerance` monoid and a |
| 95 | + `PseudoMetric`). Not in scope when the notes were written. |
| 96 | +* *Axis 6 — static vs dynamic.* Stable; the modal flavour |
| 97 | + (epistemic update, choreographic role observation, dynamic |
| 98 | + scheduler residue) is the load-bearing reading. |
| 99 | +* *Axis 7 — proof-relevant vs proof-irrelevant.* Stable; the |
| 100 | + `echo-not-prop` family is the formal witness to this axis |
| 101 | + being load-bearing. |
| 102 | +* *Axis 8 — information-theoretic vs computational access.* New |
| 103 | + since the notes were written. Formalised in `EchoDecidable.agda` |
| 104 | + (refinement 3, the decidability-respecting echo) and |
| 105 | + `EchoAccess.agda` (refinement 2, the graded access modality); |
| 106 | + the cost-indexed and witness-search refinements (1, 4) have |
| 107 | + thin slices in `EchoCost.agda` / `EchoSearch.agda` as of |
| 108 | + 2026-05-20. This axis names "preimage exists" vs "preimage is |
| 109 | + findable" — a distinction none of the original five notes |
| 110 | + could see. |
| 111 | + |
| 112 | +Two further developments inflect the refresh: |
| 113 | + |
| 114 | +* *Pillars A–D landed.* The Pillar B universal-property work |
| 115 | + (`EchoPullback.agda`, terminal cone), the Pillar C separating |
| 116 | + model (`EchoSeparating.agda`), and the Pillar D |
| 117 | + carrier-parametricity package (`EchoRelModel.agda`) all |
| 118 | + shipped after the notes; the Pillar A `Echo ≃ fib` |
| 119 | + identification (`EchoFiberBridge.agda`) is now load-bearing |
| 120 | + for any neighbour comparison that invokes the homotopy fibre. |
| 121 | +* *2-cat ruled out (`decisions/no-2-cat.adoc`).* The notes |
| 122 | + speak of "2-cell arguments" liberally. Those arguments are |
| 123 | + intact — they are about the *structural shape* of the |
| 124 | + comparison Σ, not about a 2-category overlay on echo itself — |
| 125 | + but the rule-out clarifies that the 2-cell shape is content |
| 126 | + the notes are reading off, not a category-theoretic |
| 127 | + organisation echo is committing to. |
| 128 | + |
| 129 | +== Per-note verdict |
| 130 | + |
| 131 | +=== `quotients.adoc` — *REFINED* |
| 132 | + |
| 133 | +The truncation and 2-cell arguments survive unchanged. The |
| 134 | +refinement is to state both in terms of the now-numbered axes: |
| 135 | +the truncation argument is the *axis-7-load-bearing* claim |
| 136 | +(`echo-not-prop` certifies proof-relevance is not vacuous), |
| 137 | +and the 2-cell argument is the *axis-5-compositional* shape of |
| 138 | +the sophisticated 2-categorical encoding's equalizer. Axis 8 |
| 139 | +also applies: the quotient projection `A → A / ker f` |
| 140 | +information-theoretically retains the same image as `f` but is |
| 141 | +*computationally* even less informative than the propositional |
| 142 | +truncation, so the gap echo names extends downward in the |
| 143 | +access lattice. No retraction conditions are exhibited; no |
| 144 | +rewrite is required. A one-line cross-reference in the note's |
| 145 | +"Status" section, pointing to axes 1 / 7 / 8, would suffice. |
| 146 | + |
| 147 | +=== `galois-connections.adoc` — *REFINED* |
| 148 | + |
| 149 | +Both the meet-Σ argument and the powerset-on-concrete-side |
| 150 | +truncation argument survive. The refinement: the truncation |
| 151 | +argument should now be filed under axis 1 (the powerset framing |
| 152 | +is *extensional* about set membership, where echo is |
| 153 | +*intensional* about witnesses) and the meet argument under |
| 154 | +axis 5 (compositional: the meet IS Σ-over-preimages whether or |
| 155 | +not the Galois user reaches for echo). Axis 8 sharpens the |
| 156 | +honest-tied paragraph: lattice-wide reasoning in AI is |
| 157 | +information-theoretic (the closure operator γ ∘ α is a property |
| 158 | +of the lattice, not of any extractor); fiber-wise reasoning in |
| 159 | +echo can carry computational-access data per fibre once |
| 160 | +`EchoAccess` / `EchoCost` are wired into the comparison. The |
| 161 | +diagonal correspondence (`meet-on-diagonal→equalizer`) is |
| 162 | +unchanged. No rewrite is required. |
| 163 | + |
| 164 | +=== `refinement-types.adoc` — *REFINED* |
| 165 | + |
| 166 | +The narrow Σ-relevant-vs-propositional-predicate split is |
| 167 | +*sharpened* by the axis-8 layer, not weakened. The note's |
| 168 | +existing tied case (Σ-relevant refinement IS echo) sits at the |
| 169 | +axis-1-intensional pole. The propositional-predicate camp sits |
| 170 | +at axis-7-proof-irrelevant. Axis 8 adds a new dimension the |
| 171 | +note does not name: a propositional-predicate refinement |
| 172 | +system that ships a *constructive decider* for its predicate |
| 173 | +(SMT-discharged or otherwise) is providing axis-8 |
| 174 | +computational access at the same time as it loses axis-7 |
| 175 | +proof-relevance — these are *orthogonal*, and the note |
| 176 | +currently conflates "loses witness data" with "is or isn't a |
| 177 | +constructive theory". `EchoDecidable.agda` makes the |
| 178 | +separation explicit. The refinement is to add a short |
| 179 | +"Cross-axis note" subsection making clear that the truncation |
| 180 | +argument is axis-7 / axis-1 content and the |
| 181 | +decidability-respecting decoration is axis-8 content. Q2.1 |
| 182 | +(the general truncation theorem) remains the right open |
| 183 | +obligation. |
| 184 | + |
| 185 | +=== `information-flow.adoc` — *REFINED* |
| 186 | + |
| 187 | +The split into "relational variants closed" and "type-theoretic |
| 188 | +variants open" is intact and is now the *correct* |
| 189 | +factorisation given axis 8. Relational IFC sits at axis-1 |
| 190 | +extensional (states quotiented by low-equivalence) and |
| 191 | +axis-7-proof-irrelevant (the relation is propositional); echo |
| 192 | +wins on both. Type-theoretic IFC variants distribute across |
| 193 | +axes 1, 5, 6, 7, and 8 differently depending on the variant, |
| 194 | +which is *why* the recipe-level comparison is genuinely open |
| 195 | +work and not a clerical exercise. The refinement: the "open |
| 196 | +obligation" paragraph should explicitly list which axes the |
| 197 | +recipe needs to be tested against for each type-theoretic IFC |
| 198 | +variant (axis 5 for compositional security types, |
| 199 | +axis 6 / dynamic for runtime monitoring approaches, axis 8 for |
| 200 | +SMT-discharged information-flow types). No rewrite is |
| 201 | +required; the open work the note describes is still the right |
| 202 | +open work. |
| 203 | + |
| 204 | +=== `provenance.adoc` — *REFINED* |
| 205 | + |
| 206 | +The multiplicity-vs-truncation distinction is the note's most |
| 207 | +valuable contribution and survives untouched. The refinement |
| 208 | +is axis-8-shaped: provenance systems in practice are deeply |
| 209 | +concerned with *access* (can you actually recover the source |
| 210 | +record from the output? at what cost?), which is exactly |
| 211 | +axis 8. The note currently treats this implicitly under the |
| 212 | +how-provenance / semiring discussion; an explicit axis-8 cross |
| 213 | +reference would land the point. The 2-cell argument (transitive |
| 214 | +provenance reduces to S-2) is unchanged. The "multi-witness |
| 215 | +type-relevant provenance would be co-extensive with echo" |
| 216 | +framing is unchanged but should additionally note that such a |
| 217 | +system would need to commit to an axis-8 stance (do the |
| 218 | +witness annotations carry access-class data?) — which most |
| 219 | +deployed provenance systems do not, giving echo a sharper edge |
| 220 | +than the current prose suggests. |
| 221 | + |
| 222 | +== Cross-cutting findings |
| 223 | + |
| 224 | +Three findings cut across multiple notes. |
| 225 | + |
| 226 | +* *Five out of five refresh to REFINED, zero to RE-EVALUATE, |
| 227 | + zero to STILL-VALID-as-stated.* The notes are not invalidated |
| 228 | + by the post-2026-05 taxonomy; every distinctness claim |
| 229 | + survives. But every note benefits from being re-stated in |
| 230 | + terms of the now-numbered axes, because the original prose |
| 231 | + uses ad-hoc terms ("propositional", "type-data", "witness |
| 232 | + identity") that the axes now name precisely. This is a |
| 233 | + coherence finding, not a correctness finding. |
| 234 | + |
| 235 | +* *Axis 8 sharpens four of five notes.* `quotients.adoc`, |
| 236 | + `galois-connections.adoc`, `refinement-types.adoc`, and |
| 237 | + `provenance.adoc` all gain a new sub-distinction once |
| 238 | + computational access is named as a separate axis. Only |
| 239 | + `information-flow.adoc` is *already* about axis-8-flavoured |
| 240 | + content (security-typed lambda calculi with SMT discharge), |
| 241 | + and even there the explicit axis-8 framing would clarify the |
| 242 | + open obligation. The recommended Q2.x-flavoured follow-up: |
| 243 | + add an "axis-8 sub-test" to the recipe-evaluation protocol |
| 244 | + in `gate-2-handoff.adoc`, so future neighbour comparisons |
| 245 | + test the recipe against all eight axes rather than the |
| 246 | + pre-2026-05 five. |
| 247 | + |
| 248 | +* *The two-argument-families framing in |
| 249 | + `docs/adjacency/README.adoc` is also refresh-eligible.* The |
| 250 | + README currently splits the distinctness arguments into |
| 251 | + "truncation" and "2-cell" families. Post-refresh, this is |
| 252 | + cleanly "axis 7 / axis 1 family" and "axis 5 family". The |
| 253 | + multiplicity argument (provenance) is its own family in the |
| 254 | + README; it sits at axis-1-intensional plus axis-7-proof- |
| 255 | + relevant. A README refresh is a separate (smaller) follow-up. |
| 256 | + |
| 257 | +== Recommended next moves |
| 258 | + |
| 259 | +The refresh is *complete as a coherence pass*. No adjacency |
| 260 | +note requires a content rewrite; every note's distinctness |
| 261 | +claim survives the new taxonomy. The recommended follow-ups |
| 262 | +are coherence-flavoured and can be batched: |
| 263 | + |
| 264 | +. *Per-note one-line axis cross-reference.* Each of the five |
| 265 | + notes gains one line in its "Status" section pointing to the |
| 266 | + specific axes the note's arguments now factor through. ~5 |
| 267 | + minutes per note; cosmetic. |
| 268 | + |
| 269 | +. *README refresh.* `docs/adjacency/README.adoc` § "The two |
| 270 | + argument families" promoted to "The three argument families |
| 271 | + (truncation = axis 7, 2-cell = axis 5, multiplicity = axis |
| 272 | + 1+7)" with cross-references. ~15 minutes. |
| 273 | + |
| 274 | +. *Recipe-evaluation protocol extension.* |
| 275 | + `docs/gate-2-handoff.adoc` Observation G adds an axis-8 |
| 276 | + sub-test, ensuring future neighbour comparisons test the |
| 277 | + recipe against all eight axes. Owner-gated; out of scope for |
| 278 | + this refresh. |
| 279 | + |
| 280 | +. *No new RE-EVALUATE work.* If a future axis is added to |
| 281 | + `taxonomy.md`, this refresh should be re-run; the protocol |
| 282 | + is the same. The refresh is *not* premature — the five notes |
| 283 | + do predate axes 2 and 8 and the post-2026-05 Pillars A–D |
| 284 | + package, and the coherence gain from naming the axes |
| 285 | + explicitly is real. |
| 286 | + |
| 287 | +== Status |
| 288 | + |
| 289 | +* Refresh: *complete*. All five notes survive; all five refine |
| 290 | + to the numbered-axes presentation. |
| 291 | +* No content rewrites scheduled in this PR; the coherence |
| 292 | + follow-ups (per-note one-liner, README refresh) are listed |
| 293 | + above as separate optional moves. |
| 294 | +* `roadmap.md` § "Theory work" entry updated from `[unblocked]` |
| 295 | + to `[refreshed — see decisions/gate1-adjacency-refresh.adoc]`. |
| 296 | + |
| 297 | +== Cross-references |
| 298 | + |
| 299 | +* `docs/echo-types/roadmap.md` — Theory-work entry updated to |
| 300 | + `[refreshed]`. |
| 301 | +* `docs/echo-types/taxonomy.md` — the eight-axis post-2026-05 |
| 302 | + taxonomy this refresh cross-checks against. |
| 303 | +* `docs/adjacency/README.adoc` — the directory index; itself |
| 304 | + refresh-eligible (see § "Cross-cutting findings"). |
| 305 | +* `docs/adjacency/{quotients, galois-connections, |
| 306 | + refinement-types, information-flow, provenance}.adoc` — the |
| 307 | + five notes refreshed against (no in-place edits in this PR). |
| 308 | +* `docs/echo-types/decisions/no-2-cat.adoc` — the template |
| 309 | + style this note follows, and the rule-out that clarifies the |
| 310 | + notes' "2-cell argument" wording. |
| 311 | +* `docs/gate-1-distinct-phenomenon.adoc` — the consolidated |
| 312 | + gate-1 doc that names the original five neighbours. |
0 commit comments