docs: ADR-6 resolved — the third layer is the sortal layer

.machine_readable/6a2/META.a2ml

@@ -17,7 +17,7 @@ decisions = [
   "ADR-3 Engine vs cartridge — we build the engine/interface/vocabulary; per-language facts are cartridges (standards/cartridges)",
   "ADR-4 Host ReScript -> AffineScript (Zig FFI + Idris2 ABI seams); ReScript host removed (Deno + cartridges interim), retained only as a legacy target language",
   "ADR-5 Emit into PanLL (octads -> VeriSimDB -> panels); not itself the IDE",
-  "ADR-6 Knot-theory framing is an aspirational lens, not a literal computation",
+  "ADR-6 Knot-theory framing is an aspirational lens, not a literal computation — RESOLVED 2026-08-05: the third layer is the SORTAL layer (invariant-path ADR-0001)",
 ]
 
 [development-practices]

.machine_readable/META.a2ml

@@ -12,7 +12,7 @@
     (adr-3 "Engine vs cartridge — we build the general engine, interface and vocabulary; per-language facts are authored as cartridges (standards/cartridges)")
     (adr-4 "Host moves ReScript -> AffineScript with Zig FFI + Idris2 ABI seams; the ReScript host has been removed (Deno + cartridges is the interim surface), ReScript retained only as a legacy target language")
     (adr-5 "The engine emits into PanLL (octads -> VeriSimDB -> panels); it is not itself the IDE")
-    (adr-6 "Knot-theory framing is an aspirational lens, not a literal computation — documented honestly"))
+    (adr-6 "Knot-theory framing is an aspirational lens, not a literal computation — documented honestly; RESOLVED 2026-08-05, the third layer is the SORTAL layer, see invariant-path ADR-0001"))
   (development-practices
     (code-style "standard")
     (security "openssf-scorecard + panic-attack static-analysis-gate")

CLAUDE.md

@@ -21,7 +21,7 @@ Canonical design: `docs/theory/CORRESPONDENCE-MODEL.adoc` — this file mirrors
 Classification is a **graded `CorrespondenceKind`**, not a boolean — six grades of the Echo fibre, each with a pedagogy:
 **cognate** (transfer) · **false-friend** (warn) · **antonym** (remap) · **alien-realization** (bridge) · **novel / no-anchor** (teach de novo) · **vanished** (re-route). Classification runs *per stratum* (surface → structure → intention → trope → invariant).
 
-Carrier = **Dyadic relation + Echo loss-with-residue** (`proven-tests-and-benches` `Dyadic.idr` + `hyperpolymath/echo-types`); `invariant-path` is the governance front-end. "Knot theory" is an aspirational lens, **not** a literal computation.
+Carrier = **Dyadic relation + Echo loss-with-residue** (`proven-tests-and-benches` `Dyadic.idr` + `hyperpolymath/echo-types`); `invariant-path` is the governance front-end. The third layer is the **sortal** layer (identity of an argument across presentations); "knot theory" was its working name and is retired — see invariant-path ADR-0001.
 
 ## Engine vs. Cartridge
 

EXPLAINME.adoc

@@ -151,11 +151,22 @@ The model is grounded in the estate's own formalism, not a bespoke lookup table:
 
 [IMPORTANT]
 ====
-*"Knot theory" is an aspirational lens, not a computation.* The framing _types → carrier
-· tropes → recurring equivalence-figures · knot theory → certificate_ is load-bearing for
-intuition, but there is *no literal knot-invariant computation here*. We use *invariant*
-in the precise sense of a _preserved quantity that certifies "same idea"_, and we make no
-Curry–Howard-fidelity claim.
+*The third layer is the "sortal" layer; "knot theory" is retired as its name.* The
+framing was _types → carrier · tropes → recurring equivalence-figures · knot theory →
+certificate_. Adversarial review (*invariant-path ADR-0001*, 2026-08-05) confirmed
+there is *no literal knot-invariant computation here* — classical knot theory does not
+apply, because a forward-only ordering on evidence makes admissible strands monotone
+in time and monotone strands comb flat.
+
+But the layer is not empty: it adjudicates *identity of an argument across
+presentations*, issuing an equivalence certificate (a move sequence preserving the
+claim) or an obstruction certificate. A *sortal* — from the same literature as "trope"
+— is a concept supplying a criterion of identity and a principle of counting for its
+instances, which is both halves of that job: what makes two writings the same idea,
+and whether two corroborating lines are two witnesses or one witness echoed.
+
+We use *invariant* in the precise sense of a _preserved quantity that certifies "same
+idea"_, and we make no Curry–Howard-fidelity claim.
 ====
 
 === Engine vs. cartridge — the division of labour

README.adoc

@@ -63,7 +63,7 @@ Classification runs *per stratum* — surface → structure → semantic intenti
 * *Crossings are lossy-with-residue = Echo fibre* (`hyperpolymath/echo-types`, Agda): `Echo f y := Σ (x : A), f x ≡ y`. The residue is precisely what is lost or added going A→B.
 * *`invariant-path`* is the governance front-end: it anchors each equivalence _claim_ to two code locations plus a witness, human-in-the-loop.
 
-NOTE: "Knot theory" is an aspirational lens for intuition, not a literal computation. "Invariant" here means a _preserved quantity that certifies "same idea"_ — no knot-invariant is computed, and we do not claim Curry–Howard fidelity.
+NOTE: The third layer is the *sortal* layer — it decides identity of an argument across presentations, and issues equivalence or obstruction certificates. "Knot theory" was its working name and is retired: no knot-invariant is computed, and classical knot theory provably does not apply here (invariant-path ADR-0001, 2026-08-05). "Invariant" means a _preserved quantity that certifies "same idea"_, and we do not claim Curry–Howard fidelity.
 
 == Engine vs. Cartridge
 

ROADMAP.adoc

@@ -20,7 +20,7 @@ design), link:CLAUDE.md[CLAUDE.md], and link:README.adoc[README.adoc] for overvi
 * [x] Six `CorrespondenceKind`s (cognate / false-friend / antonym / alien-realization / novel / vanished) as graded Echo fibres
 * [x] Strata ("levels of objects": surface → structure → intention → trope → invariant)
 * [x] Formal carrier: Dyadic `Relation` + Echo loss-with-residue; `invariant-path` as governance front-end
-* [x] Honesty caveat recorded: "knot theory" is an aspirational lens, not a computation
+* [x] Honesty caveat recorded, then RESOLVED: the third layer is the *sortal* layer; "knot theory" retired as its name (invariant-path ADR-0001, 2026-08-05)
 
 === M1 — Standards / repo hygiene ✅
 * [x] Repo renamed `rescript-evangeliser` → `nextgen-languages-evangeliser`

docs/theory/CORRESPONDENCE-MODEL.adoc

@@ -104,13 +104,36 @@ The model is grounded in the estate's own formalism, not a bespoke mapping table
 
 [IMPORTANT]
 ====
-*Honesty note on "knot theory."* The owner's framing — *types → carrier · tropes →
-recurring equivalence-figures · knot theory → certificate* — is load-bearing for
-intuition, but there is *no literal knot-invariant computation* here, and the
-knot-theory lens is flagged (by the owner) as "perceived as rhetoric, pending
-historical confirmation". We use *invariant* in the precise sense of a _preserved
-quantity that certifies "same idea"_, and keep knot theory as an aspirational lens, not
-a faked dependency.
+*Settled: the third layer is the "sortal" layer, and knot theory is retired as its
+name.* The owner's framing was *types → carrier · tropes → recurring
+equivalence-figures · knot theory → certificate*, with the knot-theory lens flagged
+as "perceived as rhetoric, pending historical confirmation". That is no longer
+pending. It was tested adversarially and ruled on in *invariant-path ADR-0001*
+(2026-08-05), which this repository's ADR-6 anticipated.
+
+What the ruling found, in short. Classical knot theory genuinely does not apply: a
+forward-only ordering on evidence makes admissible strands monotone in time, and
+monotone strands comb flat. But the third layer is *not* thereby empty — merge and
+split vertices are critical points of the time function, so confluence diamonds are
+closed curves and two of them link with every edge still pointing forward. What
+survives is not topology but *individuation*: the layer adjudicates identity of an
+argument across presentations, issuing an equivalence certificate (a move sequence
+preserving the claim) or an obstruction certificate.
+
+Hence *sortal*, from the same literature "trope" came from: a sortal supplies a
+criterion of identity and a principle of counting for its instances. Both halves are
+load-bearing — the criterion decides "same idea", and the count decides whether two
+corroborating lines are two witnesses or one witness echoed.
+
+Note the convergence with this document's own carrier. "Crossings are
+lossy-with-residue = Echo fibre" already reaches for `Echo f y := Σ (x : A), f x ≡ y`
+— and the fibre is exactly "which distinct presentations collapsed to the same
+argument", which is the sortal question stated in `echo-types`' vocabulary. The two
+lines of thought arrived at the same construction independently.
+
+*invariant* keeps its precise sense here — a _preserved quantity that certifies "same
+idea"_ — and no knot-invariant is computed. What changes is that this is now a
+recorded ruling with an argument behind it, not a caveat awaiting confirmation.
 ====
 
 [#taxonomy]