From 7e2d391ddfe1d94105a9aa2406fe9b8d30560451 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 5 Aug 2026 06:03:08 +0100 Subject: [PATCH] =?UTF-8?q?docs:=20ADR-6=20resolved=20=E2=80=94=20the=20th?= =?UTF-8?q?ird=20layer=20is=20the=20sortal=20layer,=20knot=20theory=20reti?= =?UTF-8?q?red?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This repo has carried the same three-layer framing as invariant-path — "types -> carrier · tropes -> recurring equivalence-figures · knot theory -> certificate" — across seven files, with the knot-theory lens honestly flagged as "an aspirational lens, not a literal computation" and "perceived as rhetoric, pending historical confirmation". It is no longer pending. The framing was tested adversarially and ruled on in invariant-path ADR-0001 (2026-08-05). ADR-6 anticipated the conclusion; this commit records the argument behind it and the resulting name. What the ruling found: - Classical knot theory genuinely does not apply. A forward-only ordering on evidence makes admissible strands monotone in time, and monotone strands comb flat. ADR-6's caveat was correct. - But the third layer is not thereby empty, which the caveat left open. 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 forward in time. 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", the count decides whether two corroborating lines are two witnesses or one witness echoed. Worth noting a convergence rather than a coincidence: this repo already reaches for echo-types' fibre (`Echo f y := Σ (x : A), f x ≡ y`) to model "crossings are lossy-with-residue". The fibre is precisely "which distinct presentations collapsed to the same argument" — the sortal question in echo-types' own vocabulary. The two lines of thought arrived at the same construction independently, which is better evidence for it than either alone. No claim is strengthened here: "invariant" keeps its precise sense, no knot-invariant is computed, and no Curry-Howard fidelity is claimed. What changes is that a hedge becomes a citation. Co-Authored-By: Claude Opus 5 --- .machine_readable/6a2/META.a2ml | 2 +- .machine_readable/META.a2ml | 2 +- CLAUDE.md | 2 +- EXPLAINME.adoc | 21 +++++++++++---- README.adoc | 2 +- ROADMAP.adoc | 2 +- docs/theory/CORRESPONDENCE-MODEL.adoc | 37 ++++++++++++++++++++++----- 7 files changed, 51 insertions(+), 17 deletions(-) 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]