diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index 44689b5..823b1bd 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.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] diff --git a/.machine_readable/META.a2ml b/.machine_readable/META.a2ml index 808dfa3..7da2f59 100644 --- a/.machine_readable/META.a2ml +++ b/.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") diff --git a/CLAUDE.md b/CLAUDE.md index 72871ba..a88a84d 100644 --- a/CLAUDE.md +++ b/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 diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index d141632..829e89c 100644 --- a/EXPLAINME.adoc +++ b/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 diff --git a/README.adoc b/README.adoc index 01e5081..61c56fe 100644 --- a/README.adoc +++ b/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 diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 4979f6b..b499bb9 100644 --- a/ROADMAP.adoc +++ b/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` diff --git a/docs/theory/CORRESPONDENCE-MODEL.adoc b/docs/theory/CORRESPONDENCE-MODEL.adoc index ce2904e..eeaf25e 100644 --- a/docs/theory/CORRESPONDENCE-MODEL.adoc +++ b/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]