From e213906766d1b5ce043bbd8170ddb4b9b0a3f41f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 5 Aug 2026 01:28:16 +0100 Subject: [PATCH 1/4] =?UTF-8?q?docs:=20state=20the=20idea=20=E2=80=94=20do?= =?UTF-8?q?main=20transition,=20silent=20failure,=20and=20the=20007=20dual?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The clearest articulation of what this repo is for existed in exactly one place: a dated entry in DESIGN.md from 2026-06-18. The README said 'semantic overlay for tracing how claims move from source to target', which is true but too abstract to build from, and ARCHITECTURE.md is template boilerplate ('Separation of Concerns', 'Each module has a single responsibility') that says nothing about this repo. State it properly: a claim can hold on BOTH sides of a domain transition and still not MEAN the same thing on both sides. The invariant is not 'true here and true there' but 'the same claim here and there'. The failure is silent by construction — cross-domain equality is not expressible from inside either domain, so every per-domain test can pass forever while the load-bearing claim is already broken. Also names the dual explicitly: 007's hermeneutic semantics is the mirror case (same syntax, different readings) where this is many syntaxes, one meaning. Anyone working on one should read the other. And states the profile rule that was only implicit: a profile is a lens onto a corpus that lives elsewhere and does NOT vendor it (see pmpl). examples/same-cube violates this today; flagged inline. Co-Authored-By: Claude Fable 5 --- README.md | 85 +++++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 79 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index aa075b4..7eb45ba 100644 --- a/README.md +++ b/README.md @@ -8,10 +8,80 @@ SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell src="https://api.thegreenwebfoundation.org/greencheckimage/github.com" data-link="https://www.thegreenwebfoundation.org/green-web-check/?url=github.com" /> -Invariant Path is a repo-native semantic overlay MVP for tracing how -claims move from source evidence/specification to target conclusions. +# Invariant Path -It is a claim-path debugger, not a truth engine. +**Invariant Path traces what a claim *means* when it crosses from one domain +into another — and finds the crossings where the meaning quietly changed.** + +It is a claim-path debugger, not a truth engine. It does not decide whether a +claim is true. It shows you the path a claim took, and where along that path it +stopped meaning what it meant at the start. + +## The idea + +A claim is asserted in some domain. It is then re-expressed in another — a +specification lowered into code, a licence text asserting facts about its own +file tree, a source language emitted through several backends, a proof +obligation discharged in a different logic. + +Two things can be true at once: + +* the claim holds on **both** sides of the transition, and +* it does **not mean the same thing** on both sides. + +That second case is the one this tool exists for. Nothing on the surface +signals it: both sides pass their own checks, both look green, and the +divergence is invisible precisely because each side is internally consistent. +The invariant is not "the claim is true here and true there" — it is +**"the claim is the *same claim* here and there."** That is the path, and the +path is what has to be invariant. + +### The failure is silent, which is why it needs tooling + +Per-domain tests are the wrong instrument by construction. A test inside domain +A checks A against itself; a test inside domain B checks B against itself. +Neither can see that A's claim and B's claim have drifted apart, because +**cross-domain equality is not expressible from inside either domain.** Every +individual test can pass forever while the thing you actually care about is +already broken. + +### The worked example: "different faces, same cube" + +AffineScript presents several *faces* — surface syntaxes — that all lower to +one canonical form. Per-face snapshot tests catch drift *within* a face and +never compare face A's cube against face B's. **The cross-face equality is the +load-bearing claim**, and no per-face test can state it. + +Invariant Path grounds that claim: every face's `preview-*` lowering must +normalise to the same canonical text, and when one breaks, the profile locates +*which* face broke it. + +## Its dual: 007 and hermeneutic semantics + +Invariant Path and the hermeneutic-semantics work in `007` are two halves of one +concern, and each is the other's mirror: + +| | Syntax | Semantics | The silent failure | +|---|---|---|---| +| **Invariant Path** | **different** | must be **the same** | forms diverge in meaning while each stays self-consistent | +| **007 / hermeneutic** | **the same** | may be **read differently** | one form silently carries two readings, and the wrong one is assumed | + +*Many forms, one meaning* against *one form, many meanings*. Both fail the same +way — silently, because the surface text carries no signal of the divergence. +If you are working on one, read the other; a fix in either that ignores the +dual will be incomplete. + +## What a profile is + +A **profile** is a lens this tool applies to a corpus that lives **somewhere +else**. It names a target corpus by path, states the claim being traced, and +supplies whatever verifier grounds it. + +**A profile does not vendor the corpus it examines.** See `profiles/pmpl.md` +for the intended shape: it points at the palimpsest-license tree and copies +nothing. A profile that carries a copy of its target will drift from the real +thing and quietly start grounding a claim about a stale fixture — which is this +tool's own failure mode, turned inward. # Workspace Layout @@ -29,11 +99,14 @@ It is a claim-path debugger, not a truth engine. - `docs/EXTENDING.md` — extension guide for invariant types and heuristics -- `examples/` — seeded and realistic examples (incl. - `examples/same-cube/` — the AffineScript faces corpus) +- `examples/` — seeded examples. NOTE: `examples/same-cube/` currently + vendors an AffineScript corpus, which contradicts the profile rule + above; see the open issue to point it at the real tree instead. - `profiles/` — profile notes for `echidna`, `panll`, `hypatia`, `pmpl`, - and `faces` (AffineScript "different faces, same cube") + `standards-docs`, and `faces` (AffineScript "different faces, same + cube" — pending rename to `affinescript`, matching the others, which + are named for their target corpus rather than for one claim inside it) - `scripts/verify-same-cube.sh` — grounds the faces same-cube invariant (see `profiles/faces.md`) From 37c0279a228da9ed782f92dd23db5a5619f6e9c6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 5 Aug 2026 01:31:51 +0100 Subject: [PATCH 2/4] docs(manifest): put the core idea where agents read first, marked do-not-paraphrase MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The manifest is the universal AI entry point, and its purpose field said 'monorepo for heuristic extraction and classification, provides a shared CLI'. That describes the plumbing. An agent reading it learns nothing about domain transitions or claim identity, so it reads the code and invents its own account — which is how this idea has been re-derived and distorted repeatedly, each restatement plausible and each drifting further. Add a core-idea block carrying the canonical statement, why the failure is silent by construction, the faces/cube worked example, the explicit dual with 007, the profile vendor-nothing rule, and the known deviation (issue #54). Marked DO NOT PARAPHRASE: quote or link, and if you think it is wrong, argue the point rather than silently improving the wording. The purpose field now says outright that reading only it is how the idea gets lost. Co-Authored-By: Claude Fable 5 --- 0-AI-MANIFEST.a2ml | 71 +++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 70 insertions(+), 1 deletion(-) diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 15c7214..264d05e 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -16,9 +16,78 @@ (milestones (phase-a "COMPLETE" "2026-04-15" "Multi-root grounding, proptest, and benchmarks")) + ;; ========================================================================== + ;; CORE IDEA — CANONICAL STATEMENT + ;; + ;; READ THIS BEFORE WRITING ANYTHING ABOUT THIS REPOSITORY. + ;; + ;; This statement has been re-derived from the code by successive agents and + ;; distorted each time — each restatement plausible, each drifting further + ;; from the idea. Treat the text below as the definition, not as one + ;; description among several. + ;; + ;; DO NOT paraphrase it in commits, PRs, docs, issues or manifests. + ;; QUOTE it, or link to it. If you believe it is wrong, say so explicitly + ;; and argue the point — do not silently improve the wording. + ;; ========================================================================== + (core-idea + (statement + "A claim can hold on BOTH sides of a domain transition and still NOT MEAN + THE SAME THING on both sides. The invariant is not 'true here and true + there' — it is 'the SAME CLAIM here and there'. That path is what must + be invariant.") + + (why-tooling-is-required + "The failure is silent BY CONSTRUCTION: cross-domain equality is not + expressible from inside either domain. A test in domain A checks A + against itself; a test in B checks B against itself. Every per-domain + test can pass forever while the load-bearing claim is already broken — + and everything looks green, because each side really is internally + consistent.") + + (worked-example + "AffineScript presents several FACES — surface syntaxes — that all lower + to one canonical form. Per-face snapshot tests catch drift WITHIN a face + and can never compare face A's cube against face B's. The cross-face + equality is the load-bearing claim, and no per-face test can express + it. 'Different faces, same cube.'") + + (what-this-is-not + "Not a truth engine. It does not decide whether a claim is true. It shows + the path a claim took and where along that path it stopped meaning what + it meant at the start.") + + (dual "007" + "007's hermeneutic semantics is the MIRROR of this repo, and the two are + halves of one concern: + invariant-path : DIFFERENT syntax, must be the SAME semantics + (forms diverge in meaning, each self-consistent) + 007 : the SAME syntax, may be READ DIFFERENTLY + (one form carries two readings; the wrong one is assumed) + Many forms/one meaning, against one form/many meanings. Both fail + SILENTLY, because the surface text carries no signal of the divergence. + Work on either one without reading the other and the fix is incomplete.") + + (profile-rule + "A PROFILE is a lens onto a corpus that lives ELSEWHERE. It names a target + corpus by path and VENDORS NOTHING — see profiles/pmpl.md, which points + at the palimpsest-license tree and copies no part of it. A profile + carrying a copy of its target drifts from the real thing and then grounds + a claim about a stale fixture while reporting success: this tool's own + failure mode, turned inward. Profiles are named for their TARGET, not for + one claim about it.") + + (known-deviation + "examples/same-cube/ currently vendors an AffineScript corpus and the + profile is named 'faces' rather than 'affinescript' — both violate + profile-rule above. Tracked as issue #54; not silently corrected.")) + (purpose "Monorepo for Invariant Path heuristic extraction and classification. - Provides a shared CLI for multiple estate components (echidna, panll, hypatia).") + Provides a shared CLI for multiple estate components (echidna, panll, + hypatia). NOTE: this describes the PLUMBING. For what the repository is + FOR, see core-idea above — reading only this line is how the idea has + previously been lost.") (canonical-locations (ai-manifest "0-AI-MANIFEST.a2ml" "THIS FILE") From 56ea64d50346f0c09db72f05490223cd7b5ba346 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 5 Aug 2026 09:38:06 +0100 Subject: [PATCH 3/4] =?UTF-8?q?docs(adr):=20the=20sortal=20layer=20?= =?UTF-8?q?=E2=80=94=20three=20of=20five=20counts=20against=20the=20knot?= =?UTF-8?q?=20layer=20broke=20(#55)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stacked on #53 (it quotes the `(core-idea (statement …))` block that #53 introduces). Base retargets to `main` automatically when #53 merges. ## What this is The three-layer claim-checking architecture (type / trope / knot) invited an obvious attack: if Layer 1's diode makes every admissible strand monotone in time, the configurations are braids rather than knots, and Layer 3 looks like an optimizer rather than a layer. I built the sharpest five-count case against Layer 3 I could, then had it attacked adversarially, with a separate fact-check of the theorems it relied on. **Three of the five counts broke** — two of them on checkable errors in my own argument. This ADR records the surviving position. ## Why an ADR and not a `DESIGN.md` entry Deliberate. The core idea of this repository was written down correctly, and only, in a dated `DESIGN.md` entry (2026-06-18). It was accurate and invisible: readers took the plumbing description from the manifest, went to the code, and reconstructed the idea their own way. This record has the same failure profile — a load-bearing conclusion that reverses a plausible position — so it goes where it can be found. This adds `docs/decisions/` (the estate norm, present in trope-checker, typell, boj-server). The repo had no ADR infrastructure. ## The three counts that broke **Count 1 — "topology cannot form" — wrong.** The diode constrains *edges*, but it cannot constrain the Morse structure at *vertices*, and Layer 2 mandates them. A merge is a local maximum of time along any cycle through it; a split is a local minimum. So a confluence diamond is a closed curve with one min and one max — the profile of a round circle — and two of them link with **every edge strictly forward in time**. No closure, no time-reversal. The supporting lemmas all fact-checked correct; the false premise was *unpinned*: shared anchors and shared conclusions identify endpoints, and Artin combing needs a free boundary. **Count 2 — "the plane is notation" — falls to intrinsic linking.** Conway–Gordon properties are fixed by incidence alone yet quantify over all realizations. Drawing-invariant and epistemically contentful, and no Layer 1 predicate quantifies over embeddings. **Count 5 — "it is only a complexity switch" — falls to the doubling attack.** Present one derivation twice, paraphrased, under distinct labels. Label-honest (diode silent), well-founded, exogenously attested, each copy individually warranted. It has an **identical pass/fail profile to genuine two-witness corroboration on every subdiagram** — so the exponential sweep cannot distinguish them even in principle — yet corroboration weight is 2 vs 1. Worse, the sweep answers *its own* robustness question wrongly without the identity quotient supplied as input. ## The decision Layer 3 is retained, with a restated charter: it adjudicates **identity of an argument across presentations**, issuing equivalence certificates (a move sequence whose every intermediate stays green) or obstruction certificates. Reduction to an equivalence proof is not a demotion — detection and equivalence-certification are dual. And the dependency arrow was missing one direction. The design ran L1 → L3 (temporality gives clean orientations). The missing arrow is **L3 → L2**: overlapping presentations must be recognised as the same argument *before* resource accounting, or L2 double-counts. ## ⚠ Two things recorded as open, not resolved **The Layer 2 vocabulary does not match committed code.** Of the six terms in play (strength, consistency, coherence, resemblance-warrant-on-merge, p-residue, p-sufficiency), only **p-sufficiency** is real — `floor(U) ⊑ acc(v)`. **`p-residue` does not exist anywhere in the estate.** What is built in `trope-checker@69221ad` is a six-coordinate `Grade`, nine `p-*` effects, a `Floor`, and a witness-carrying `Verdict`. This matters because Count 3 read p-residue as affine resource accounting — a term I could not ground — so the reachability result should be re-derived against the actual grade algebra. Also, `check-vocabulary.sh` hard-fails on entries outside the nine. **"Knot" is already taken — by a repo doing this exact job.** quandledb hosts KRL (Knot Resolution Language) and 007 proves a knot composition monoid with a real `unknot`. More interesting than a clash: QuandleDB describes itself as *"the invariant/equivalence + semantic-identity face"* — the charter this ADR assigns to Layer 3. ## Verification - **Quote check**: the canonical `(statement …)` is reproduced verbatim — diffed character-by-character against `0-AI-MANIFEST.a2ml`, identical. - `asciidoctor -o /dev/null docs/decisions/*.adoc` — parses clean, no warnings. - `reuse lint` — none of the new files flagged; missing-info count unchanged from baseline (1, pre-existing). - Every cross-repo `file:line` citation re-resolved against a recorded SHA. - No code touched. Note: `trope-checker` has two working copies at different commits (`hyper-repos` @ `69221ad`, `_TROPES _SET` @ `680fc20`). Citations use the former and record the SHA. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5 --- docs/decisions/0000-template.adoc | 36 ++ docs/decisions/0001-the-sortal-layer.adoc | 704 ++++++++++++++++++++++ docs/decisions/README.adoc | 47 ++ 3 files changed, 787 insertions(+) create mode 100644 docs/decisions/0000-template.adoc create mode 100644 docs/decisions/0001-the-sortal-layer.adoc create mode 100644 docs/decisions/README.adoc diff --git a/docs/decisions/0000-template.adoc b/docs/decisions/0000-template.adoc new file mode 100644 index 0000000..23dafe5 --- /dev/null +++ b/docs/decisions/0000-template.adoc @@ -0,0 +1,36 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += ADR-0000: Template + +*Date:* YYYY-MM-DD + +*Status:* Proposed | Accepted | Deprecated | Superseded by NNNN | Rejected + +== Context + +What is the issue, and why does it need deciding now? State the problem, not the +solution. If the decision reverses an earlier position, say what that position +was and why it was plausible — a reader who cannot reconstruct the losing case +will re-derive it. + +== Decision + +What was decided, in the imperative. One paragraph if possible. + +== Argument + +What was actually established, and how far it reaches. Name the fragment in +which the opposing case is *right*, because an unbounded claim is not checkable. +Where a conclusion rests on a source outside this repository, cite it as +`path:line` with a commit SHA. + +== Consequences + +What becomes easier, what becomes harder, and what is now load-bearing that was +not before. + +== Open + +Questions this record deliberately does not settle. An ADR that resolves a +question it has no evidence for is worse than one that leaves it open — mark +them, and say what evidence would settle each. diff --git a/docs/decisions/0001-the-sortal-layer.adoc b/docs/decisions/0001-the-sortal-layer.adoc new file mode 100644 index 0000000..a6eb164 --- /dev/null +++ b/docs/decisions/0001-the-sortal-layer.adoc @@ -0,0 +1,704 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += ADR-0001: The sortal layer — what survives the case against the knot layer + +*Date:* 2026-08-05 + +*Status:* Accepted + +== Context + +The claim-checking architecture under design has three layers. Layer 1, *type*: +formal admissibility, checkable on form alone — well-formedness, continuity or +through-line, and temporality, a forward-only ordering constraint (the *diode*) +requiring that evidence precede conclusion, applied per claim-type. Layer 2, +*trope*: particularity and warrant, purpose-indexed, judging whether +individuated context-bound evidence survives the leap to the conclusion for this +use. Layer 3, *knot*: structure — once each strand has passed Layers 1 and 2, +distinguishing *real tangles*, interdependencies that cannot be separated +without cutting a claim, from *false tangles* that look interlinked and slide +apart when pulled. + +The stated rationale for siting temporality in Layer 1 was that Layer 3 needs +its strand orientations from a clean form-only rule, so the topology does not +inherit Layer 2's purpose-indexed messiness. + +That rationale invites an obvious attack, and the attack was commissioned +deliberately: *does the diode, pushed into Layer 1 and applied per claim-type, +abolish Layer 3's subject matter?* If every admissible strand is monotone in +time, the configurations are braids rather than knots, and the case for a third +layer looks like a case for an optimizer. + +A five-count prosecution was built to make that case as sharply as possible, +then attacked by three independent adversarial reviews with a separate +mathematical fact-check of the theorems it relied on. *Three of the five counts +broke.* This record exists because the surviving position reverses a plausible +one, and a reversal that is not written down where it can be found will be +re-derived wrongly. That failure has already happened once in this repository: +the core idea was stated correctly and only in a dated `DESIGN.md` entry +(2026-06-18), where it was accurate and invisible. + +== Decision + +*Layer 3 is retained, and its charter is restated.* It is not a detector of +knots in a diagram of the argument. It is the *sortal layer*: it adjudicates +*identity of an argument across presentations*, and it issues certificates +rather than verdicts. + +*The name is "sortal", ruled 2026-08-05.* A sortal — Locke, Strawson, Geach, +Wiggins, Lowe — is a concept that supplies a *criterion of identity* and a +*principle of counting* for its instances. That is this layer's charter twice +over: adjudicating identity across presentations is the criterion, and the +doubling attack, where corroboration weight is 2 or 1 according to whether two +presentations are one argument, is the count. The name also states the layer +ORDER, which no alternative did: you cannot account resources over instances +until you have fixed what counts as one instance, so the sortal must be settled +before Layer 2's accounting is sound (see <>). + +It was chosen over nine alternatives on four weighted criteria — accuracy, +collision-freedom, peer fit with "type" and "trope", and honesty about the +mathematics. Runner-up was *congruence* (an equivalence relation compatible with +the structure — technically sharper, but already live inside Layer 2's own +soundness proofs). The former working title, *the equivalence layer*, came +LAST: it escapes the metaphor collision only to land in a charter collision, +since quandledb self-describes as the "invariant/equivalence + semantic-identity" +layer and Tangle ships a "storage/equivalence layer". See <>. + +"Knot layer" is retired, not retained. The two certificate names below are +unaffected and keep their existing terms. + +== The prosecution, and which counts fell + +[cols="1,3,1",options="header"] +|=== +| Count | Charge | Verdict + +| 1 +| *Jurisdictional suicide.* The diode makes every strand monotone in time. Cups + and caps — local extrema of the time function, the generators of genuine + knotting — are exactly time-reversal points, banned by Layer 1. Braid closure + requires identifying a strand end with an earlier strand start, which the DAG + discipline forbids. With endpoints unpinned, braids comb out flat. The rule + Layer 3 demanded abolishes Layer 3's subject matter. +| *Falls* + +| 2 +| *The second dimension is notation.* A crossing lives in the drawing, not the + argument. Isotopy invariance, applied honestly, quotients the drawing away, + and the quotient is just the DAG with its incidence and resource structure. +| *Falls* + +| 3 +| *Proof-theoretic absorption.* The genuine structural content is substructural + proof theory, already owned by Layers 1 and 2; the one global condition, a + proof-net correctness criterion, is form-only and cheap and belongs in Layer + 1's continuity sub-layer. +| *Survives only in a fragment* + +| 4 +| *Supervenience dilemma.* Either tangledness cashes out in Layer 1/2 verdicts + over partitions — hence is definable, merely expensive — or it does not, in + which case nothing epistemic hangs on it and it is notation. +| *Survives only in a fragment* + +| 5 +| *Residual identity.* The only unannexed content is a fast-certificate + calculus standing in for a complete-but-exponential sweep. That is complexity + management: a job description, not a subject matter. +| *Falls* +|=== + +=== Why Count 1 falls + +The mechanism was checked and is wrong. The diode constrains *edges*: each edge +is strictly monotone in epistemic time. It cannot constrain the Morse structure +at *vertices*, and Layer 2 mandates vertices — merging two strands under a +resemblance warrant, splitting shared evidence across two uses. + +Walk any undirected cycle in the DAG. A merge vertex, where both cycle edges +enter, is a local *maximum* of time along that cycle; a split vertex, where both +leave, is a local *minimum*. So a confluence diamond — one evidence node split +into two lemma strands that merge into one conclusion — is a closed curve with +exactly one minimum, one maximum, and monotone arcs between: the Morse profile +of a round circle. Two such diamonds embed with linking number 1, every edge +strictly forward in time, no closure operation and no time-reversal anywhere. A +cycle alternating two splits and two merges carries four extrema, enough for a +trefoil in 2-bridge position. + +The supporting lemmas were individually correct — a critical-point-free strand +does straighten; unpinned strand systems do comb flat; the braid word problem is +polynomial by Garside normal form. The false premise was *unpinned*. Endpoints +are identified, not free: multiple strands leave the same observation token and +enter the same conclusion node, and identification is asserted content. Artin +combing requires a free boundary. Pinning is precisely what makes braid +non-triviality possible. + +Layer 1's diode and Layer 2's merge rule do not abolish Layer 3's subject +matter. They jointly manufacture it. + +=== Why Count 2 falls + +The count offers a dichotomy — structure is either in the drawing, hence +notation, or in the DAG's incidence and resource data, hence already owned. +Intrinsic linking is neither. Conway–Gordon (1983): in *every* embedding of +K6 in 3-space the sum of linking numbers over disjoint triangle pairs is odd, so +some pair is non-trivially linked; every embedding of K7 contains a knotted +Hamiltonian cycle. The property is fixed by the abstract graph, yet what it +asserts quantifies over all realizations: however you present this dependency +structure, some pair of its confluence cycles interpenetrates. That is +drawing-invariant and epistemically contentful, and no Layer 1 predicate — +well-formedness, continuity, diode — quantifies over embeddings. + +Robertson–Seymour–Thomas cuts both ways and the concession is recorded: linkless +embeddability is characterised by excluding the seven-graph Petersen family as +minors, so *detection* is polynomial and annexable to Layer 1. The count loses +the philosophical point and keeps the organizational one. Note in passing that +the Petersen family is closed under Δ-Y exchange, and the Y is a trivalent +vertex: the obstruction family is generated by the same merge vertices Layer 2 +introduces. + +=== Why Count 5 falls: the doubling attack + +Present one internally-derived line of evidence *twice*, paraphrased, under +distinct labels — two apparently independent corroborating lines for a +conclusion that are in fact one derivation with its rule order permuted and its +intermediate claims re-worded. + +Every node is label-honest: each timestamp truly records when that presentation +was committed, so the diode is silent. Every grounding chain terminates in +genuinely attested exogenous anchors, so attestation and well-foundedness both +pass — what is doubled is the internal derivation *over* honest anchors. Each +line individually passes Layer 2. No resemblance-warrant fires, because a +label-keyed ledger sees two tokens and never registers a contraction. + +Now apply Count 4's own supervenience test. The doubled web and an honestly +redundant two-witness web have *identical* pass/fail profiles over *every* +subdiagram: delete either line and the other passes, in both webs. The +complete-but-exponential sweep cannot distinguish them even in principle, +because its supervenience base is Boolean and the two webs agree on every +Boolean. Yet corroboration weight is two versus one. + +So there is a judgement that is epistemically load-bearing, provably not +supervenient on Layer 1/2 runs, not attestation, not well-foundedness, and not +complexity management — it is a different *relation*, not a faster decision +procedure for the sweep's relation. + +Worse for Count 5, this inverts its mechanism. The sweep's counterfactuals +quantify over strands, which presupposes knowing where one strand ends and +another begins. Under the doubling attack the sweep answers *its own* questions +wrongly: asked which claim, if cut, collapses the web, it reports the conclusion +robust — cut line one, line two survives — when in truth a single cut collapses +everything. Load-bearing and robustness analysis are not further applications +the sweep owns; they are computations the sweep gets *wrong* unless the identity +quotient is supplied to it as input. A component that the complete procedure +depends on for its own correctness is not an optimizer over that procedure. + +== The fragment where the prosecution is right + +This bound is part of the finding, not a hedge. Assume a single global epistemic +clock, a fixed and finite purpose index, strand monotonicity, and support-only +warrant with no defeaters. In that fragment: + +* literal knot theory has no subject matter — no closures, no static knot types, + and crossings as drawn are notation; +* the deletion-and-partition sweep genuinely annexes static detection. An + attempt to construct two structures with identical Layer 1/2 verdicts on every + subdiagram *including* deletion counterfactuals but differing tangle-hood + failed inside this fragment: deletion sweeps see pooling, Brunnian arity, and + blast radius. + +Everything below turns on the architecture not living in that fragment. + +== The three results that survive + +=== Separability is reachability, not a verdict profile + +Two tokens, affine — *at most* one use each — pooled by a warranted merge that +supports two claims, each above its sufficiency floor. The sweep tests the partition +"first token to first claim, second to second": both parts pass in isolation, so +the formula returns *false tangle*. + +Now try to pull it apart as moves on the committed state. The token cannot be +pre-attached to its claim, because its residue is already consumed inside the +merge — the affine accounting forbids the staging duplicate. The merge cannot be +detached first, because that leaves a claim momentarily unsupported, which is a +cut. The merge cannot be split in place without dangling edges, a Layer 1 +violation. And an atomic multi-edge transaction is unavailable, because on an +append-only ledger an atomic swap is indistinguishable from a retroactive +rewrite — precisely the forgery the ledger exists to expose. + +Every route passes through a cut. By the operative definition — inseparable +*without cutting a claim*; false tangles *slide apart when pulled* — this is a +real tangle. The sweep says false. The extensional formula therefore yields the +wrong extension. + +Realness is a *reachability* property of the space of Layer-1/2-passing states +under the legal moves, with strand endpoints pinned by resource identity. +Path-connectivity is never a function of pointwise vertex properties, so no +quantified formula over static verdicts on subdiagrams computes it. + +[#discipline] +==== Which resource discipline, exactly + +*Affine — at most once — not linear.* Linear would require every token to be +consumed exactly once, so an uncited piece of evidence sitting in the store +would be a type error. That is the wrong norm for an evidence store: weakening +must be free. + +The argument above is indifferent to the choice. What it leans on is the +*absence of contraction* — a token cannot be duplicated to stage the separation +— and linear and affine both forbid that. They differ only over weakening, which +the argument never uses. So the reachability result holds under either reading; +only the gloss was overstated. + +But neither label is exactly right, and the gap is load-bearing. This +architecture does not forbid contraction outright: *resemblance-warrant-on-merge* +permits it *when warranted*. The discipline is therefore affine with a guarded +contraction rule — contraction available only against a warrant — which is not +plain affine logic but a controlled-contraction variant of it. + +That distinction is exactly where the doubling attack lives. Two failure modes +double-count evidence, and affinity sees only one of them: + +* *Contraction taken freely* — one token duplicated and spent twice. Banned by + affinity, caught by the ledger. +* *Contraction never taken though mandatory* — two tokens that are one token, + never merged, so corroboration is counted twice. **Affinity is blind to this**, + because nothing illegal happens: two distinct labels really are spent once + each. + +The doubling attack is the second. It is not an illegal contraction; it is a +*missing* one. This sharpens the dependency argument below: Layer 3 is not +merely an input to Layer 2's accounting, it closes a specific and permanent +blind spot in it. No resource discipline can detect a contraction it was never +asked to perform, because the omission is invisible in the resource algebra — +it is a fact about identity, which lives outside that algebra. + +=== The purpose quantifier is beyond any finite sweep + +Layer 2 verdicts are purpose-indexed, so tangle-hood inherits the index: the +same pooled structure is separable at a permissive sufficiency floor and +inseparable at a strict one. "Real versus false" is not a property the sweep can +return at all — only real-*at*-purpose. + +One sweep per purpose is available if and only if the purpose set is finite and +enumerated at check time. It is not, by the architecture's own charter: Layer 2 +exists precisely because warrant does not transfer across uses, including uses +not yet specified. The valuable judgements are the quantified ones — separable +for *every* purpose, hence safe to modularize permanently; inseparable for every +purpose, hence structural rather than a threshold artifact. Universal claims +over an open index are not decidable by any finite family of Layer 1/2 runs. + +They are, however, certifiable structurally. An untangling that uses only +form-preserving moves — no merge, no split, no residue reallocation, no warrant +touched — is purpose-blind, and therefore certifies false-tangle-hood for all +purposes at once, including future ones. So the advantage over the sweep is +*expressive*, not merely a matter of cost. This is the point on which the +prosecution's Count 4 was most confidently wrong. + +=== Composition-forgery, and what the diode actually buys + +The diode's clock must be *epistemic* — when evidence became available or was +committed — not ontic. Otherwise retrodiction, which is most of history and all +of forensics, fails to type-check. That concession is unavoidable and it is +expensive. + +First, it means the diode disposes only of *label-honest* backward edges. Since +forgery is precisely the crime of having correct form, and type systems verify +structure given trusted labels, the diode buys well-formedness, not security. + +Second, epistemic time in a multi-source system is a *partial* order — distinct +sources commit at causally unrelated instants. There is then no slab, no level +planes, and no single Morse function, so Count 1's geometry is not merely false +but ill-formed in the general case. Stipulating a single sequential verifier +restores it, at the price that verdicts now depend on an arbitrary interleaving +of causally incomparable commits; soundness then demands proving verdict +invariance across admissible interleavings, which is the same question in +another vocabulary. + +Third, and concretely: because the diode is applied *per claim-type*, and claim +types carry constitutively different clocks, the web is a union of differently +ordered charts glued along type-conversion edges — a dated document grounds a +historical event-claim, which grounds a forensic inference, whose confirmation +grounds a new reading of another document. A composite path can be forward in +each chart's own order while its endpoints, compared in one order, land the +conclusion *earlier* than where the path began. This manufactures priority with +no single backward edge, no forged label, no fabricated anchor, and no cycle. +Formally it is holonomy: every chart is flat — the combing argument is valid +per-slab — and the twist lives in the gluing. + +Where a global conservative extension of the union of typed orders exists, +demanding acyclicity of the glued preorder is cheap and form-only, and that +fragment belongs in Layer 1's continuity sub-layer. Where the clocks are +incommensurable by design — the retrodiction cases that forced epistemic time in +the first place — blanket acyclicity would falsely reject legitimate +retrodiction, and the check must instead *classify* composite paths as licit or +illicit mixed-order transports. + +== The restated charter + +The sortal layer adjudicates *identity of an argument across presentations*, and +delivers one of two things: + +*Equivalence certificate* — a sequence of moves, every intermediate of which +passes Layers 1 and 2, transforming one presentation into the other. Isotopy to +an essentially unique flat embedding; productive unrolling of a guarded loop; +dihomotopy of two interleavings; collapse of an apparently independent line onto +the line it duplicates. + +*Obstruction certificate* — an invariant separating the two under the same +quotient. A Petersen-family minor; an unguarded self-support loop; a distinct +dihomotopy class; a linking-style invariant of the support incidence. + +Three consequences worth stating explicitly. + +*Reduction to an equivalence proof is not a demotion.* Detection and +equivalence-certification are dual: a false-tangle certificate *is* a move +sequence collapsing one strand onto another, and a real-tangle certificate is an +invariant that refuses to. "It is only an equivalence proof" is the job +described correctly. + +*The certificate is the deliverable, not a stand-in.* Count 5 required the fast +path to approximate a slow ground truth. Here the untangling witness — the +refactoring whose every intermediate state remains green — is what the user +wanted; there is no slower procedure it approximates. + +*Layer 2 already works this way.* Its verdict is not a bare Boolean: an +insufficiency carries a witness naming the coordinate and edge responsible +(`trope-checker/src/idris2/Checker/Check.idr:74`, `Insufficient (List String) +(Maybe (String, String))`, at `69221ad`). Certificate-shaped output is the +established idiom in this architecture, not a novelty introduced for Layer 3. + +[#arrow] +== The reversed dependency arrow + +The design rationale ran Layer 1 → Layer 3: temporality sits in Layer 1 so the +topology inherits clean orientations from a form-only rule. + +The missing arrow runs Layer 3 → Layer 2. Overlapping presentations from +different sources must be recognised as the same argument *before* resource +accounting runs, or Layer 2 double-counts — this is exactly what the doubling +attack exploits. An affine ledger is well-defined only relative to a +token-identity relation, and that relation cannot be read off labels, because +labels are what forgery attacks. + +Layer 3 is therefore upstream of Layer 2's soundness, not decoration downstream +of it. The dependency runs both ways through the third layer, which is what +being load-bearing means. + +Stated at full strength (see <>): the omission is not merely +undetected, it is *undetectable in the resource algebra*. Affinity governs +contractions that are taken; a contraction that was never taken leaves no trace +in it, because two distinct labels really were spent once each. Whether they +were the same token is a fact about identity, and identity is not a resource +property. So this is not a gap Layer 2 could close by being more careful. + +== Relation to the canonical statement + +The following is quoted verbatim from `0-AI-MANIFEST.a2ml`, `(core-idea +(statement …))`. It is marked do-not-paraphrase there, and it is reproduced +rather than summarised here for that reason. + +[quote] +____ +A claim can hold on BOTH sides of a domain transition and still NOT MEAN +THE SAME THING on both sides. The invariant is not 'true here and true +there' — it is 'the SAME CLAIM here and there'. That path is what must +be invariant. +____ + +*The following is a new claim, and is not part of the canonical statement.* It +is argued here rather than absorbed into the statement, per that block's own +instruction to argue openly rather than silently improve the wording. + +The claim: Layer 3's restated subject matter — identity of an argument under +structure-preserving moves — and the canonical statement's "the SAME CLAIM here +and there" are the same question asked of different transformations. The +canonical statement is about *domain transitions*: the same claim carried across +a boundary between formalisms, where cross-domain equality is not expressible +from inside either domain. Layer 3 is about *presentation moves*: the same +argument carried across a re-derivation, re-wording, re-ordering, or refactor, +where equality is not expressible from inside either presentation. + +The structural similarity is exact in the respect that matters: in both cases +every local check passes while the load-bearing identity is already broken, and +each side really is internally consistent, so nothing looks wrong. The doubling +attack is the presentation-move instance of the same silent failure that "different +faces, same cube" is the domain-transition instance of. + +What is *not* claimed: that these are one mechanism, or that a tool for one is a +tool for the other. Domain transitions cross formalisms; presentation moves stay +within one. Whether a single quotient covers both is open, and would need +argument rather than assertion. + +[#naming] +== The collision, measured + +An earlier draft of this record stated that the knot vocabulary lived only in +conversation and in this ADR's own branch. *That was wrong*, and the correction +matters more than the name. + +*The three-layer metaphor is committed on main, one repository over.* +`_LANGUAGES _SET/nextgen-language-evangeliser` carries "types → carrier · tropes +→ recurring equivalence-figures · knot theory → certificate" across seven files +(`EXPLAINME.adoc:154-156`, `docs/theory/CORRESPONDENCE-MODEL.adoc:107-112`, +`README.adoc:66`, `CLAUDE.md:24`, `ROADMAP.adoc:23`, and two `META.a2ml` +entries), and already names invariant-path as "the governance front-end". It has +its own ADR-6 disclaiming literal knot theory as "an aspirational lens, not a +computation" — the same conclusion this record reaches by argument. The public +estate site (`_WEBSITES _SET/hyperpolymath/README.adoc:33`) also carries the +metaphorical sense fourteen lines from a literal one. + +*The literal surface is roughly three times what this record first claimed* — +about 13,355 match lines estate-wide for knot/unknot/tangle/braid/quandle/skein/ +Reidemeister/isotopy. The largest holder is not quandledb (1,507) but +*Tangle-the-language* (4,699), whose stated premise is "programs are braids and +equivalence is isotopy", with a real `braid_equiv` engine and mechanised +isotopy in `proofs/Tangle.lean`. Two further repositories own this layer's exact +former words: `frayed-knot-toolkit` (Agda `Unknot`, `Strand`, +`project : Knot -> Strand -> StrandPath`) and +`fraying-model-computational-testbed`. + +*A correction to this record's own earlier text:* `typell/crates/typell-tangle` +was dismissed here as an unrelated homonym. It is not — it maps Tangle's +braid-word types. The dismissal was wrong. + +*Blast radius of the rename is small:* about eleven prose and metadata files +across three repositories, and *zero code identifiers, type names, function +names, test names, or schema surface*. invariant-path's own main branch was +clean; the vocabulary existed only on this unmerged branch. Renaming here, before +merge, costs two files. The remaining files in nextgen-language-evangeliser and +on the public site are follow-up work, not a blocker. + +=== QuandleDB is a homonym — the open probe is closed, answered NO + +The earlier draft asked whether QuandleDB's "invariant/equivalence + +semantic-identity" API could carry argument presentations. It cannot, on three +independent grounds, and the question should not be reopened without new +evidence. + +*The object is wrong and hard-coded.* QuandleDB is a fixed twenty-column SQLite +table keyed by `knot_name` (`server/serve.jl:39-60`); the sole ingestion path is +`KnotRecord → PD code → Skein.to_planardiagram → quandle_descriptor(::PlanarDiagram)` +(`server/quandle_semantic.jl:489`). There is no generic-structure entry point. + +*The equivalence engine is a GROUP BY, and the certificate-shaped parts are +stubs.* `find_equivalent` resolves to two SQL selects over `descriptor_hash` and +`quandle_key` (`server/serve.jl:332-353`); `find_path` — the only stage shaped +like an equivalence certificate — is an explicit stub deferring "full BFS path +search" (`Evaluator.jl:664-691`), as is `match`. The e-graph engine the +whitepaper makes central exists only as prose plus a TLA+ model: a search for +egraph/egglog/saturat across all sources returns zero hits. All thirty-six +shipped rows carry `descriptor_version = 'fallback-v1'`, meaning no quandle was +ever computed. + +*And the mathematics does not match, which is decisive.* Quandle invariants are +invariants of a fixed combinatorial diagram modulo isotopy. Every move this +layer must quotient by — rule permutation, rewiring, paraphrase, unrolling, +interleaving — CHANGES the abstract graph; unrolling adds vertices, which no +isotopy can do. Worse, paraphrase changes labels, and topological invariants are +blind to labels: a quandle fingerprint therefore cannot see the doubling +attack's defining feature, and would return FALSE POSITIVES by equating +genuinely independent derivations that happen to share a shape. + +One thing there is worth borrowing, and it is not the engine: KRL ships a +four-level confidence lattice (`ConfExact`/`ConfSufficient`/`ConfNecessary`/ +`ConfHeuristic`, `server/krl/Ast.jl:68-73`) whose necessary/sufficient split +mirrors this layer's obstruction/equivalence duality. + +[#substrate] +== Existing formal work: what can and cannot be reused + +Surveyed 2026-08-05 across `_TYPES _SET` and `_PROVER-SOLVER _SET`, with proofs +independently typechecked rather than taken on trust. + +*Layer 1 — nothing, in any repository.* There is no syntax of claims, premises, +steps or evidence anywhere, and no ordering on evidence events of any kind. All +three sub-layers must be built from scratch. Two names promise otherwise and do +not deliver: `choreographic-types` is a pre-registration stub whose +`git log --all --diff-filter=A` returns no source file in any language on any +branch, ever; and typell's "Level 9 Temporal safety" passes iff a named field is +present, examining no event and no order. + +*Layer 2 — two real, verified contributions.* `tropical-types` derives the whole +retention order (reflexivity, transitivity, antisymmetry, monotonicity in both +operations) from one line of idempotence with no case split on the carrier +(`Resource/Algebra/Dioid.lean:36-99`), and makes absorption of deceptive +elements a semiring law every instance must discharge rather than a stipulation +(`Interface.lean:78-80`). `#print axioms` on its load-bearing theorems reports +none, and its CI greps a 23-theorem axiom audit and exits 1 — a real gate. +Separately, `echo-types` proves that path-independence of grade degradation +holds *precisely* if the retention order is propositional, and supplies a +countermodel refuting it otherwise (`EchoGraded.agda:145-171`, +`EchoSeparating.agda:131-141`). That is a mechanised necessary condition on this +architecture's six-coordinate `Grade`, and checking it is an audit, not a build. + +*This layer — a quarter, on the obstruction side only.* `echo-types` supplies a +compiling home for the object this layer's question ranges over: `Echo f y = Σ A +(λ x → f x ≡ y)` (`Echo.agda:16-17`), the fibre of a lossy map — "which distinct +inputs collapsed to the same output". `echo-not-prop` (`EchoTruncation.agda:76-82`) +is a general "here is an invariant separating two members of one fibre", and +`FiberSize-fin` mechanises "identified members count once" — the counting half +of the sortal, exactly. But there is *nothing* on the equivalence-certificate +side: no move relation, no quotient, no normal form, no confluence result, in +any repository surveyed. And the piece most needed is the repo's own unclosed +debt — propositional truncation is postulated under `--safe` +(`EchoImageFactorizationPropPostulated.agda:108`) and constructed only in a +`--cubical` island that Agda's flag rules forbid the main cone from importing. +"Merely inhabited versus how many witnesses" is precisely what the doubling +attack turns on. + +=== absolute-zero's CNO: refuted as a substrate, valuable as a case study + +The hypothesis was attractive: an equivalence certificate is a move sequence +non-null on the presentation but provably null on the claim, i.e. a Certified +Null Operation on semantic content, and `CNOCategory.v` would supply the +category. It does not survive, and the refutation is machine-checked against the +repository's own Coq. + +`is_CNO` is nullity against one hard-coded projection that deliberately excludes +the program counter (`CNO.v:63-71`), from which follows the axiom-free +`any_jump_is_cno`: an unconditional jump to an arbitrary target is a CNO, +because under that projection control flow does not exist. Every move this layer +must adjudicate is a control-flow move. Worse, the exclusion is documented as +having been made *because* requiring PC-equality made "every non-empty CNO claim +FALSE" — the widen-the-invariant-until-your-moves-are-null circularity, executed +in the file proposed as the substrate. And `CNOCategory.v` is a category of +machine states whose hom-sets are *not* quotiented by any semantic equivalence, +which is the opposite of the construction needed. + +What genuinely survives is a negative case study, and it is worth an afternoon +before this layer's first definition is written: `CNO.v:646-658` records two +axioms deleted as unsound because the quotient and the move relation disagreed — +congruence must be proved, never assumed; and `LandauerDerivation.v:330-343` +records an attempt to reason modulo a quotient that failed and became an axiom, +naming the missing ingredients exactly. `CNO.v:576-589` draws the right +conclusion from Rice's theorem — be a checker, not a searcher. + +[WARNING] +.Do not take a dependency on absolute-zero's Lean development +==== +`proofs/lean4/FilesystemCNO.lean` and `proofs/lean4/LambdaCNO.lean` each derive +`False` from their own axioms: `mkdir_rmdir_inverse` (`:98`) is stated without +the precondition its Coq counterpart carries, and `eta_equivalence` (`:264`) is +refuted by absolute-zero's own `LambdaCNO.v:430`. `lake build` reports success, +and CI never runs the Lean leg at all. Reported for that repository to fix; noted +here so no one imports it. +==== + +=== A tooling ruling that follows + +Mechanise this layer in *Agda with `--cubical`*, not Idris 2. Its core +construction is a quotient by admissible moves, and kategoria's +`Level10_CubicalTypes.idr:191-199` argues correctly that Idris 2's QTT cannot +host path types, transport, higher inductive types or quotients. This is the one +useful thing that survey produced from kategoria. + +[#numbering] +=== Never write bare "L1", "L2", "L3" + +Three L-numberings are live in adjacent repositories and the near-misses are +worse than the collisions: kategoria's L1–L10 is a language-feature ladder, +typell/VCL's L1–L10 is a database-query safety scale, and this architecture's is +type/trope/sortal. Both neighbours put temporality at *L9* while this +architecture puts it at *Layer 1c*; kategoria's L7 is linear/affine (this +architecture's Layer 2 concern) and its L10 is type-identity (reads as this +layer). A cross-claim has already been made in error on number adjacency alone +(`routes/delta-aggregate/TYPELL-BRIDGE.adoc:33-56`). Write `Layer 1 (type)`, +`Layer 2 (trope)`, `Layer 3 (sortal)`; prefix foreign references `kat-L7`, +`ty-L9`. + +== Consequences + +=== Positive + +* The third layer has a subject matter that survives the strongest available + attack, rather than a job description that dissolves under it. +* Its output type is fixed: certificates, dual in form, checkable independently + of the procedure that found them. +* Two form-only fragments are correctly reassigned *to Layer 1*, where they are + cheap: Petersen-minor testing for intrinsic linking, and acyclicity of the + glued preorder wherever a global conservative extension of the per-type orders + exists. + +=== Negative + +* Layer ordering is no longer a clean stack. Layer 3 is upstream of Layer 2's + soundness and downstream of Layer 1's orientations, so implementation cannot + proceed strictly bottom-up. +* Verdict-level caching across Layer 2 is unsafe without an identity quotient, + because token identity is an input to resource accounting rather than a + consequence of it. + +=== Neutral + +* The diode is retained unchanged and remains correct. Its scope is now stated + accurately: it disposes of label-honest backward edges, which is a real but + narrow class. +* Exogenous anchor fraud remains outside every layer. It is attestation and + provenance infrastructure, not a checking layer, and no internal discipline + can catch it. + +[#open] +== Open + +=== The Layer 2 vocabulary does not match committed code + +The vocabulary used in the discussion that produced this record — strength, +consistency, coherence, resemblance-warrant-on-merge, p-residue, p-sufficiency — +does not match what is built. In `trope-checker` at `69221ad`, Layer 2 is: + +* a six-coordinate grade — `verification/proofs/idris2/Trope/Grade.idr:19`, + `record Grade` with `fQuality`, `fBearer`, `fContext`, `fRecord : Fate`, + `bond : Bond`, `merge : Merge`; +* nine `p-*` effects in + `trope-particularity-workbench/vocabulary/` — preserving, projecting, + collapsing, detaching, attenuating, falsifying, misbinding, conflating, + fusing; +* a floor as partial demand vector — `src/idris2/Checker/Ir.idr:36`; +* a verdict `Sufficient | Insufficient` with a witness edge — + `src/idris2/Checker/Check.idr:74`. + +Of the six terms, *only p-sufficiency is real*, defined as `floor(U) ⊑ acc(v)` +(`hermeneia/docs/THEORY.adoc:57`). *`p-residue` does not exist anywhere in the +estate* — a case-insensitive search over all repositories returns nothing. + +This is recorded rather than reconciled, for two reasons. First, the +prosecution's Count 3 read p-residue as affine resource accounting, so part of +the argument above rests on a term that could not be grounded; the +reachability result in particular assumes affinity and should be re-derived +against the actual grade algebra. Second, +`trope-particularity-workbench/tests/check-vocabulary.sh` is a live consistency +gate that hard-fails on any vocabulary entry outside the nine effects, so +introducing these terms as if they were established would break a real check. + +*What would settle it:* a ruling on whether the six terms are a new Layer 2 +design superseding the grade algebra, an informal gloss of it, or drift. If new, +they need reconciling against `Grade` and the nine effects before either +vocabulary is cited as canonical. + +=== Not settled here + +* *Who owns the total-evidence requirement.* Affinity makes weakening free: + leaving evidence uncited is costless in the resource algebra, which is the + right call for a store but leaves cherry-picking invisible. Suppressing + contrary evidence is epistemically culpable and violates no rule in any of the + three layers — Layer 1 sees well-formed structure, Layer 2 sees a strand that + passes for its use, Layer 3 sees a presentation identical to itself. Detecting + it requires comparing the argument against evidence *not in it*, so it is not a + property of the committed web at all. Either a fourth obligation or an explicit + out-of-scope ruling; currently it is neither. +* Whether guarded self-support — bisimulation-style arguments, precedent whose + authority is constituted by continued citation — is admitted. If it is, + closures exist and knot types proper become realizable. If it is not, the + checker rejects a recognised class of sound arguments, *and* loses the ability + to distinguish sound coinduction from self-grounding forgery, which share the + same Layer 1 form. +* Whether the correctness criterion remains tractable. Multiplicative proof-net + correctness is linear-time without units, but proof *equivalence* with units + is PSPACE-complete (Heijltjes–Houston 2014). The sortal layer asks the + second question, not the first. +* Whether Milnor invariants suffice as obstruction certificates. They classify + Brunnian links up to link-homotopy, but boundary links have all Milnor + invariants zero while remaining non-trivial, so they cannot be the general + certificate format. diff --git a/docs/decisions/README.adoc b/docs/decisions/README.adoc new file mode 100644 index 0000000..1f6d666 --- /dev/null +++ b/docs/decisions/README.adoc @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += Architecture Decision Records + +Decisions about *what this repository is for* and *what its parts mean* live +here, one file per decision, numbered and never renumbered. + +== Why here and not in DESIGN.md + +`DESIGN.md` is a dated build log: what was done, and when. It answers "why is +the code shaped like this?" and it is read by someone already working in the +tree. + +An ADR answers "what is the claim, and what argument survived?" — and it has to +be findable by someone who has not yet formed an opinion. That distinction is +not academic in this repository. The core idea of Invariant Path was written +down correctly, and only, in a dated `DESIGN.md` entry (2026-06-18). It was +accurate and it was invisible: readers took the plumbing description from the +manifest, went to the code, and reconstructed the idea their own way each time. +The cure was to move the statement to the file agents read first and mark it +do-not-paraphrase. This directory is the same cure for arguments rather than +statements. + +Rule of thumb: if getting it wrong would cost a rebuild, it is an ADR. + +== Convention + +* Filename `NNNN-kebab-slug.adoc`, numbered from `0001`. +* SPDX header on every file; prose in this repository is `CC-BY-SA-4.0`. +* Status is one of `Proposed`, `Accepted`, `Deprecated`, `Superseded by NNNN`, + `Rejected`. Superseded records are kept, never deleted — the wrong turn is + part of the record. +* Cite `file:line` with the commit SHA when the citation is to another + repository, because line numbers drift and several estate repositories have + more than one working copy at different commits. +* Quote canonical statements; do not restate them. + +== Index + +[cols="1,4,1",options="header"] +|=== +| ADR | Title | Status + +| link:0001-the-sortal-layer.adoc[0001] +| The sortal layer — what survives the case against the knot layer +| Accepted +|=== From 17c2480da5871b5f1fd20e3f8b55c2946189c82e Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 7 Aug 2026 13:49:54 +0100 Subject: [PATCH 4/4] docs: refresh human + machine documentation, add a live debt register (#60) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stacked on #53. Retargets to `main` automatically when that merges. ## The correction that drove this The **three-layer claim checker** is this repository's principal subject — and it was barely documented, while the AffineScript same-cube example was over-represented relative to it. `faces` is one profile of six, a lens onto a corpus that lives elsewhere: a good demonstration of the idea in miniature, not the subject. This PR fixes that proportion. ## Human **`ARCHITECTURE.md` was template boilerplate** describing `src/`, `tests/`, `config/` and `README.adoc` — none of which match this repo — duplicating the real `docs/ARCHITECTURE.md`, and saying *nothing whatever* about the three layers. (Closed PR #58 independently spotted this as "drop false ARCHITECTURE"; it did not land, so the problem persisted.) Rewritten in two parts: **Part I** the layer architecture — Layer 1 (`type`) and what the diode actually buys, with its three open problems (epistemic vs ontic clock, partial-order time, composition-forgery as holonomy); Layer 2 (`trope`) as actually built in `trope-checker`/`hermeneia`, affine with a guarded contraction rule; Layer 3 (`sortal`), the doubling attack, and the `L3 -> L2` dependency arrow. **Part II** the shipping extractor/classifier. **`README.md` had drifted from the tool.** It said every face's lowering "must normalise to the same canonical text"; the verifier now compiles each face to typed-wasm and compares `sha256`, keeping text diffs as a diagnostic only. The README asserted something that held on both sides of a transition while no longer meaning the same thing — **this repository's own failure mode, turned inward.** ## Machine `0-AI-MANIFEST.a2ml`: real structure (it omitted `docs/decisions/`, `proofs/`, `examples/`, `src/ui/`); new `(architecture …)` block with the three layers, dependency order, doubling attack, decided-not-built status and the `L1`/`L2`/`L3` numbering hazard; new `(debt …)` block; ADR-0001 in milestones. **The do-not-paraphrase `(core-idea)` block is untouched.** **Wiki** was a one-line stub → `Home` + `Three-Layers` (pushed separately — wikis are their own git repo). ## Debt — new `docs/DEBT.md` | | Dimension | Open | Worst | |---|---|---|---| | A | Architecture | 3 | **HIGH** | | C | CI/CD | 3 | MEDIUM | | L | Licence | 3 | MEDIUM | | D | Docs | 3 | MEDIUM | | P | Proof | 2 | MEDIUM | | K | Code | 1 | LOW | **The headline finding went stale mid-audit, and that is recorded rather than hidden.** C1 was filed CRITICAL — no lockfile, every workflow `startup_failure` on every branch, `main` never green. **PR #56 fixed it while this was being written.** Re-measured: 10 workflows green on `main` including Rust CI, CodeQL and Secret Scanner. C1 is now RESOLVED with the history kept, and the residue split into C2 (Scorecard still `startup_failure`), C3 (two workflows failing on *content*, untriaged — invisible until the lockfile landed), C4 (no proof gate). Other findings: - **L1** — GitHub reported **no licence**. Cause found: `LICENSE` deviated from canonical MPL-2.0 by a **trailing space** (line 38) and `http` vs `https` (line 360). Replaced with the canonical text. - **A1–A3** — Layer 1 has no substrate anywhere; Layer 3's equivalence side does not exist; Layer 2's vocabulary does not match its implementation (**`p-residue` exists in no repository**). - **P1** — `SameCube.agda` is genuinely good (`--safe`, zero postulates, zero holes) but **ungated**. `docs/tech-debt-2026-05-26.md`'s "RESOLVED" banner was **partly wrong** and is corrected in place: licence was not actually detected, and proof debt was half closed. ## Repo metadata (applied via API, not in this diff) - **Description** was `Dual-use claim-grounder (Phase A in progress)` — vague and stale. Now states what the tool does and its governance role. - **Topics** were `development, hyperpolymath, open-source, rust, software, tooling` — owner name, generic words, and a language GitHub detects itself. Replaced with eight concept-level ones: `claim-checking`, `argumentation`, `semantic-drift`, `provenance`, `cross-domain-equivalence`, `architecture-decision-records`, `formal-methods`, `static-analysis`. ## Verification - `0-AI-MANIFEST.a2ml` parens and quotes balance - `reuse lint` missing-info count **unchanged** from baseline (1, pre-existing) — verified by stashing and re-running - every path cited in `ARCHITECTURE.md` exists on disk - CI state re-measured per workflow before publishing the claim - no code touched 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5 --- 0-AI-MANIFEST.a2ml | 113 +++++++++++++- ARCHITECTURE.md | 280 +++++++++++++++++++++++++++++---- LICENSE | 4 +- README.md | 37 ++++- docs/DEBT.md | 291 +++++++++++++++++++++++++++++++++++ docs/tech-debt-2026-05-26.md | 18 ++- 6 files changed, 698 insertions(+), 45 deletions(-) create mode 100644 docs/DEBT.md diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 264d05e..4f6eea7 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -14,7 +14,8 @@ (status "starred")) (milestones - (phase-a "COMPLETE" "2026-04-15" "Multi-root grounding, proptest, and benchmarks")) + (phase-a "COMPLETE" "2026-04-15" "Multi-root grounding, proptest, and benchmarks") + (adr-0001 "ACCEPTED" "2026-08-05" "Layer 3 ruled: the SORTAL layer; 3 of 5 counts against it broke")) ;; ========================================================================== ;; CORE IDEA — CANONICAL STATEMENT @@ -91,14 +92,114 @@ (canonical-locations (ai-manifest "0-AI-MANIFEST.a2ml" "THIS FILE") - (launcher "invariant-path-launcher" "Standardized launcher")) + (launcher "invariant-path-launcher" "Standardized launcher") + (decisions "docs/decisions/" "ADRs — the layer rulings") + (architecture "ARCHITECTURE.md" "How the work is arranged") + (debt "docs/DEBT.md" "Live debt register")) (structure "invariant-path/ - ├── crates/ # Rust crates (CLI, core logic) - ├── profiles/ # Scan profiles for different repos - ├── schemas/ # JSON schemas for annotations - └── scripts/ # Management and installation scripts") + ├── docs/decisions/ # ADRs — the LAYER RULINGS. Start at 0001. + ├── crates/invariant-path-core # extractor, classifier, model, annotations + ├── crates/invariant-path-cli # the binary (single main.rs) + ├── schemas/ # JSON schema for persisted annotations + ├── profiles/ # lenses onto corpora ELSEWHERE; vendor nothing + ├── proofs/ # SameCube.agda (the faces worked example) + ├── examples/same-cube/ # vendored corpus — violates profile-rule, issue #54 + ├── scripts/ # verify-same-cube.sh, install-desktop.sh + ├── src/ui/ # AffineScript GUI SKETCH — in NO build + └── desktop/, assets/ # launcher entry and icons") + + (architecture + (headline + "Two faces. (1) The GOVERNANCE FRONT-END for a three-layer claim checker — + this is where the layer architecture is decided and recorded, and where + most of the intellectual work lives. (2) A shipping Rust CLI that extracts + and classifies claim transitions. The second is NOT an implementation of + the first; keep that distinction visible.") + + (layer-1 "type" + "Formal admissibility, checkable on FORM ALONE. Sub-layers: well-formedness; + continuity/through-line; temporality = 'the diode', a forward-only ordering + (evidence precedes conclusion, no backward edges) applied PER CLAIM-TYPE. + OPEN: the diode's clock must be EPISTEMIC not ontic or retrodiction fails + to type-check; epistemic time across sources is a PARTIAL order, so verdicts + need invariance across interleavings; per-type diodes glue into differently + clocked charts, so a path forward in every chart can reach backwards + globally (composition-forgery — holonomy).") + + (layer-2 "trope" + "Particularity and warrant, PURPOSE-INDEXED, per strand. IMPLEMENTED + ELSEWHERE (trope-checker + hermeneia): a six-coordinate Grade, nine p-* + effects (three deceptive and absorbing), a Floor as partial demand vector, + and a verdict Sufficient|Insufficient CARRYING A WITNESS EDGE. p-sufficiency + is floor(U) [= acc(v). Resource discipline is AFFINE (at most once) WITH A + GUARDED CONTRACTION RULE — not plain affine logic.") + + (layer-3 "sortal" + "Adjudicates IDENTITY OF AN ARGUMENT ACROSS PRESENTATIONS, issuing an + EQUIVALENCE CERTIFICATE (a move sequence whose every intermediate still + passes layers 1 and 2) or an OBSTRUCTION CERTIFICATE (an invariant + separating them under the same quotient). Detection and equivalence- + certification are DUAL. Named for the sortal of Locke/Strawson/Wiggins/Lowe: + a concept supplying a CRITERION OF IDENTITY and a PRINCIPLE OF COUNTING. + Ruled in docs/decisions/0001-the-sortal-layer.adoc after 3 of 5 counts + against the layer broke under adversarial review.") + + (dependency-order + "Layer 1 --orientations--> Layer 3 --identities--> Layer 2. + Layer 3 is UPSTREAM of Layer 2's soundness. Overlapping presentations must + be recognised as the same argument BEFORE resource accounting, or Layer 2 + double-counts. This arrow was missing from the original design.") + + (killer-case "the doubling attack" + "One derivation presented TWICE, paraphrased, under distinct labels. + Label-honest (the diode is silent), well-founded, exogenously attested, + each copy individually warranted — and it has an IDENTICAL pass/fail profile + to genuine two-witness corroboration on EVERY subdiagram, so no layer-1 or + layer-2 sweep can see it, while corroboration weight is 2 versus 1. + It is NOT an illegal contraction; it is a contraction that was MANDATORY AND + NEVER TAKEN, to which the affine resource algebra is structurally blind.") + + (status + "DECIDED, NOT BUILT. Nothing in this repository implements these layers. + Layer 1 has NO substrate anywhere in the estate. Layer 2 has real support + from tropical-types and echo-types. Layer 3 has ~a quarter, obstruction + side only, from echo-types' fibre. QuandleDB and absolute-zero's CNO were + both investigated as substrates and REFUTED WITH EVIDENCE — do not reopen + either without new evidence. See docs/DEBT.md sections A1-A3.") + + (numbering-hazard + "NEVER write bare L1/L2/L3. Three unrelated L1-L10 schemes are live in + adjacent repositories (kategoria = language-feature ladder, typell/VCL = + query-safety scale), and BOTH neighbours put temporality at their L9 while + this architecture puts it at Layer 1c. Write 'Layer 1 (type)', + 'Layer 2 (trope)', 'Layer 3 (sortal)'; prefix foreign refs kat-L7, ty-L9.")) + + (debt + (register "docs/DEBT.md" "live; supersedes docs/tech-debt-2026-05-26.md") + (resolved "CI/CD: the lockfile epidemic is CURED (PR #56, 2026-08-05). + Until then ALL workflows were startup_failure on EVERY branch and + main had never been green. Now 10 green on main including Rust CI, + CodeQL and Secret Scanner — the gates are real. Residual: OSSF + Scorecard still startup_failure; Well-Known Standards and Workflow + Security Linter fail on content, untriaged. NOTE, because it will + recur: `gh pr checks` shows nothing wrong for a parse-rejected + workflow, since it emits no check run; use `gh run list`.") + (high "Architecture: layer 1 has no substrate; layer 3's equivalence side + (move relation, quotient, normal form) does not exist anywhere.") + (medium "Layer 2 VOCABULARY MISMATCH: of strength/consistency/coherence/ + resemblance-warrant-on-merge/p-residue/p-sufficiency, only + p-sufficiency is real. p-residue exists in NO repository. Left + deliberately unreconciled; see docs/DEBT.md A3.") + (medium "Proof: proofs/SameCube.agda is real (--safe, zero postulates, zero + holes) but UNGATED — no workflow compiles it. verify-same-cube.sh + exits 0 on a missing compiler.") + (medium "Licence: GitHub reports NO licence — LICENSE deviated from canonical + MPL-2.0 (trailing space line 38, http vs https line 360). SPDX + identifiers sit on line 2-3 behind an opening comment, which the + estate linter (head -1 only) reads as missing. Do NOT fix by adding + headers — MOVE them; a blind sweep previously mis-licensed files.")) (format-meta (version "2.1.0") diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md index 607e3d8..5e88e4f 100644 --- a/ARCHITECTURE.md +++ b/ARCHITECTURE.md @@ -1,47 +1,267 @@ + + # Architecture -## Overview +> **Read `0-AI-MANIFEST.a2ml` first.** Its `(core-idea …)` block is the canonical +> statement of what this repository is for, and it is marked do-not-paraphrase. +> This file describes how the work is arranged; it does not restate the idea. + +Invariant Path is a claim-path debugger, not a truth engine. It has two faces: + +1. **The governance front-end for a three-layer claim checker.** This is where + the layer architecture is decided and recorded. Most of the intellectual + work lives here. +2. **A working extractor and classifier.** A Rust CLI that finds claim + transitions in repository artifacts and records what each one preserves and + loses. This is what currently ships. + +The second is not an implementation of the first. Keeping that distinction +visible is the point of this document. + +--- + +## Part I — The three-layer claim checker + +A claim is checked by three layers, each answering a question the others +cannot. `nextgen-language-evangeliser` names this repository as the *governance +front-end* for that architecture: rulings are recorded here as ADRs, and each +equivalence claim is anchored to its code locations plus a witness, +human-in-the-loop and editable. + +### Layer 1 — `type`: formal admissibility + +Checkable on **form alone**, with no judgement of evidence quality. Three +sub-layers: + +- **Well-formedness** — is this a claim at all? +- **Continuity / through-line** — does the argument connect end to end? +- **Temporality — "the diode"** — a forward-only ordering constraint: evidence + must precede conclusion, no backward edges, applied **per claim-type**. + +The diode was sited in Layer 1 deliberately, so that anything downstream +inherits strand orientations from a clean form-only rule rather than from Layer +2's purpose-indexed judgements. + +**What is settled, and what is not.** The diode is correct but narrower than it +looks: it rejects only *label-honest* backward edges. Three open problems are +recorded in ADR-0001: + +- Its clock must be **epistemic** (when evidence was committed) rather than + ontic (when events happened), or retrodiction — history, forensics — falsely + fails to type-check. +- Epistemic time across multiple sources is therefore a **partial order**, not + a scalar clock, so verdicts must be proved invariant across admissible + interleavings of causally incomparable commits. +- Because the diode applies *per claim-type*, differently-clocked charts glue + together, and a composite path can run forward in every chart while its + endpoints reach backwards globally. ADR-0001 calls this **composition-forgery**; + it is a holonomy phenomenon — every chart flat, the twist in the gluing. + +### Layer 2 — `trope`: particularity and warrant + +**Purpose-indexed**, per strand: does individuated, context-bound evidence +survive the leap to *this* conclusion for *this* use? + +This is the layer with a real implementation, and it lives in +`trope-checker` and `hermeneia`, not here: + +- a six-coordinate **`Grade`** — four `Fate` fields plus `Bond` and `Merge` + (`Trope/Grade.idr`); +- nine **`p-*` effects** in `trope-particularity-workbench/vocabulary/`, of + which three are *deceptive* and absorbing under composition; +- a **`Floor`** — a use-model expressed as a partial demand vector + (`Checker/Ir.idr`); +- a verdict `Sufficient | Insufficient` that **carries a witness edge** on + failure (`Checker/Check.idr`); +- **p-sufficiency**, defined as `floor(U) ⊑ acc(v)` — the declared floor lies + below the accumulated grade in a componentwise retention order. + +Grades compose associatively along transformation paths, with the fidelity +coordinate accumulating tropically. + +**Resource discipline: affine, with a guarded contraction rule.** At most once +— weakening is free, contraction is not — but contraction *is* permitted when a +resemblance warrant licenses it. That is not plain affine logic, and the +distinction is load-bearing; see the doubling attack below. + +### Layer 3 — `sortal`: identity across presentations + +Ruled 2026-08-05 in `docs/decisions/0001-the-sortal-layer.adoc`, after a +five-count case against the layer was built deliberately and **three of the +five counts broke** under adversarial review. + +The layer adjudicates **identity of an argument across presentations**, and +issues one of two things: + +- an **equivalence certificate** — a sequence of moves, every intermediate of + which still passes Layers 1 and 2, transforming one presentation into the + other; +- an **obstruction certificate** — an invariant separating them under the same + quotient. + +Detection and equivalence-certification are **dual**, so "it is only an +equivalence proof" is the job stated correctly, not a demotion. + +The name is from the same literature `trope` came from: a **sortal** supplies a +*criterion of identity* and a *principle of counting* for its instances. Both +halves do work — the criterion decides "same argument", the count decides +whether two corroborating lines are two witnesses or one witness echoed. -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. +### The doubling attack, and why Layer 3 precedes Layer 2 -## Directory Structure +Present one derivation **twice**, paraphrased, under distinct labels. Every +node is label-honest, so the diode is silent. Every chain terminates in +genuinely attested exogenous anchors, so attestation and well-foundedness both +pass. Each copy individually passes Layer 2. + +The doubled web and an honestly-redundant two-witness web have **identical +pass/fail profiles on every subdiagram** — yet corroboration weight is two +versus one. + +This is not an illegal contraction. It is a contraction that was **mandatory +and never taken**, and the affine resource algebra is structurally blind to it: +nothing illegal happened, two distinct labels really were spent once each. +Whether they were the same token is a fact about *identity*, which is not a +resource property. + +Hence the dependency arrow that the original design was missing: ``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation +Layer 1 (type) ──orientations──▶ Layer 3 (sortal) ──identities──▶ Layer 2 (trope) ``` -## Design Principles - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized +Overlapping presentations must be recognised as the same argument **before** +resource accounting runs, or Layer 2 double-counts. Layer 3 is upstream of +Layer 2's soundness, not decoration downstream of it. -## Dependencies +### Status: decided, not built -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility +**Nothing in this repository implements these layers.** ADR-0001 is a decision +record about an architecture, and says so. A survey of existing formal work +(recorded in the ADR) found: -## Security Considerations +- **Layer 1** — no substrate anywhere in the estate. No syntax of claims, no + ordering on evidence events. Must be built from scratch. +- **Layer 2** — real support from `tropical-types` (the retention order derived + from one line of idempotence, axiom-free, behind a genuine CI gate) and + `echo-types` (path-independence of degradation holds precisely if the + retention order is propositional, with a countermodel). +- **Layer 3** — roughly a quarter, obstruction side only. `echo-types` supplies + the fibre `Echo f y = Σ A (λ x → f x ≡ y)` — "which distinct presentations + collapsed to the same argument" — and "identified members count once". There + is **nothing** on the equivalence side: no move relation, no quotient, no + normal form, anywhere. -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed +Two candidate substrates were investigated and **refuted with evidence**: +QuandleDB (a homonym — topological invariants are blind to labels, so a quandle +fingerprint cannot see the doubling attack and would return false positives) +and absolute-zero's CNO (machine-checked refutation against its own Coq). -## Maintainability +### Conventions -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently +Do not write bare `L1` / `L2` / `L3`. Three unrelated L-numberings are live in +adjacent repositories, and both neighbours put temporality at *their* L9 while +this architecture puts it at Layer 1c. Write `Layer 1 (type)`, +`Layer 2 (trope)`, `Layer 3 (sortal)`; prefix foreign references `kat-L7`, +`ty-L9`. --- -*Last updated: 2026-07-18* +## Part II — The shipping tool + +What actually compiles and runs today: a pipeline from artifact text to a +reviewable record. + +``` +artifact text + │ + ▼ + extractor candidate claim transitions, anchored by trigger phrase + │ and byte span + ▼ + classifier invariant type; losses/preserved; break condition; + │ a Classification + ▼ + annotations JSONL, upsert-on-write, visibility + status + │ + ▼ + CLI scan / accept / dismiss / clarify / add / update / overlay +``` + +Two commitments explain most of the code. + +**Heuristics are deliberately strict.** The extractor triggers on explicit +transition markers and accepts false negatives to avoid annotation noise +(`DESIGN.md`, 2026-04-10). A noisy suggester costs more trust than it saves. + +**The path is retained, never discarded.** A bare `Classification` cannot +recover the claim-path that produced it, so `ClassificationOutcome` carries +`losses` and `preserved` alongside the verdict — the `echo-types` fibre +discipline applied to a classifier. See `docs/ECHO-TYPES.md`. + +### Domain model + +In `crates/invariant-path-core/src/model.rs`: + +- **`ClaimCandidate`** — source span, target text, matched trigger, path + description. +- **`InvariantType`** — what is meant to be preserved: `CausalRelationship`, + `StatisticalRelationship`, `LogicalImplication`, `Mechanism`, + `RiskProbability`, `NormativeBridge`, `ResourceBudget`, `Provenance`. +- **`Classification`** — `ValidPath`, `Overextended`, `Conflation`, + `Incomplete`, `Abstain`. +- **`ClassificationOutcome`** — the verdict *plus* `losses`, `preserved`, break + condition. The retained echo. +- **`Annotation`** — the persisted record, with `Visibility` and `Status`. + +The classifier is pure and offline: term lists in `classifier.rs`, no model, no +network, no external state. + +### Profiles + +A profile is a **lens onto a corpus that lives elsewhere**. It names a target +by path and **vendors nothing**. `pmpl.md` is the reference implementation. + +The rule exists because a profile carrying a copy of its target drifts from the +real thing and then grounds a claim about a stale fixture *while reporting +success* — this tool's own failure mode, turned inward. Profiles are named for +their **target**, not for one claim about it. + +Six exist: `echidna`, `faces`, `hypatia`, `panll`, `pmpl`, `standards-docs`. + +`faces` is the one worked example that is fully grounded end to end: it checks +that AffineScript's several surface syntaxes all lower to one canonical form, +by compiling each to typed-wasm and comparing `sha256` hashes. It is a good +demonstration of the whole idea in miniature — and it is *an example*, not the +subject of this repository. It also violates the profile rule twice (it vendors +its corpus, and it is named for a claim rather than a target), which is issue +#54. Details in `profiles/faces.md`; its Agda companion is `proofs/SameCube.agda`. + +## Layout + +| Path | What lives there | +|---|---| +| `docs/decisions/` | **ADRs — the layer rulings. Start at ADR-0001.** | +| `crates/invariant-path-core/` | The library: `extractor.rs`, `classifier.rs`, `model.rs`, `annotations.rs`, `doc_claims.rs`, `pipeline.rs`. | +| `crates/invariant-path-cli/` | The binary. Single `main.rs`; parsing and output only. | +| `schemas/annotation.schema.json` | The contract between this tool and anything reading its store. | +| `profiles/` | One markdown file per target corpus. Vendors nothing. | +| `proofs/`, `examples/same-cube/`, `scripts/verify-same-cube.sh` | The `faces` worked example and its grounding check. | +| `docs/` | `ARCHITECTURE.md` (module contracts), `EXTENDING.md`, `ECHO-TYPES.md`, `DEBT.md`. | +| `desktop/`, `assets/` | `.desktop` launcher entry and icons. | +| `src/ui/` | `invariant_path_gui.affine` — an AffineScript GUI sketch. **Not in the Cargo workspace; built by nothing.** Design material, not code. | + +The Cargo workspace is exactly the two crates in `members`; nothing under +`src/` is compiled. + +## What this is not + +- Not a truth engine. It never decides whether a claim is true. +- Not an implementation of the three layers. Those are decided, not built. +- Not a prover. `proofs/` grounds one claim in one worked example. +- Not networked. No service, no telemetry, no model calls. +- Not a general NLP pipeline. The classifier is term lists and pattern matches, + chosen so a reader can audit every decision it makes. diff --git a/LICENSE b/LICENSE index 14e2f77..d0a1fa1 100644 --- a/LICENSE +++ b/LICENSE @@ -35,7 +35,7 @@ Mozilla Public License Version 2.0 means any form of the work other than Source Code Form. 1.7. "Larger Work" - means a work that combines Covered Software with other material, in + means a work that combines Covered Software with other material, in a separate file or files, that is not Covered Software. 1.8. "License" @@ -357,7 +357,7 @@ Exhibit A - Source Code Form License Notice This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. If a copy of the MPL was not distributed with this - file, You can obtain one at http://mozilla.org/MPL/2.0/. + file, You can obtain one at https://mozilla.org/MPL/2.0/. If it is not possible or desirable to put the notice in a particular file, then You may include the notice in a location (such as a LICENSE diff --git a/README.md b/README.md index 7eb45ba..c266541 100644 --- a/README.md +++ b/README.md @@ -52,9 +52,40 @@ one canonical form. Per-face snapshot tests catch drift *within* a face and never compare face A's cube against face B's. **The cross-face equality is the load-bearing claim**, and no per-face test can state it. -Invariant Path grounds that claim: every face's `preview-*` lowering must -normalise to the same canonical text, and when one breaks, the profile locates -*which* face broke it. +Invariant Path grounds that claim: each face is compiled to typed-wasm and the +modules are compared by `sha256`, so the faces must land in **one wasm +equivalence class**. The wasm *is* the cube, which makes this a far stronger +bar than matching canonical text. When a face falls outside the class, a +normalised text diff is printed to locate *where* — as a diagnostic, not as the +check itself. + +This is one worked example, not the subject of the repository. See +`profiles/faces.md` for its limits, including the two classes the `greet` +corpus genuinely splits into. + +## The three-layer claim checker + +Invariant Path is the **governance front-end** for a layered checker. Each +layer answers a question the others cannot: + +| Layer | Name | Question | +|---|---|---| +| 1 | **type** | Is this admissible *on form alone*? Well-formedness, through-line, and a forward-only ordering on evidence — "the diode". | +| 2 | **trope** | Does this particular evidence survive the leap to this conclusion *for this use*? Purpose-indexed warrant. | +| 3 | **sortal** | Are these two presentations *the same argument*? Identity, and therefore counting. | + +Layer 3 was ruled on in +[ADR-0001](docs/decisions/0001-the-sortal-layer.adoc) after a five-count case +against it was built deliberately and three of the five counts broke. Its +killer case is the **doubling attack**: one derivation presented twice, +paraphrased, under distinct labels is invisible to every Layer 1 and Layer 2 +check — identical pass/fail on every subdiagram — while corroboration weight is +two instead of one. That is why Layer 3 runs *before* Layer 2: identity must be +settled before resource accounting, or Layer 2 double-counts. + +**These layers are decided, not built.** The ADR is a decision record. What +ships today is the extractor, classifier and annotation store described below. +Open architectural gaps are tracked in [`docs/DEBT.md`](docs/DEBT.md). ## Its dual: 007 and hermeneutic semantics diff --git a/docs/DEBT.md b/docs/DEBT.md new file mode 100644 index 0000000..61f13ee --- /dev/null +++ b/docs/DEBT.md @@ -0,0 +1,291 @@ + + +# Debt register — invariant-path + +**Audited 2026-08-05** by reading the tree and querying the GitHub API. This is +the *live* register: findings stay until closed, and each carries the evidence +that would prove it fixed. + +Supersedes `docs/tech-debt-2026-05-26.md`, whose "RESOLVED" banner overstates +the proof item — see [P1](#p1). + +| | Dimension | Open | Worst | +|---|---|---|---| +| A | Architecture — the three layers | 3 | **HIGH** | +| C | CI/CD | 3 | MEDIUM | +| L | Licence | 3 | MEDIUM | +| D | Docs | 3 | MEDIUM | +| P | Proof | 2 | MEDIUM | +| K | Code | 1 | LOW | + +--- + +## Architecture debt + +This is where the substantial work is, and where the substantial gaps are. +ADR-0001 settled Layer 3's charter and name; it did not build anything, and it +was explicit about what remains. + + +### A1 — Layer 1 has no substrate anywhere. `HIGH` + +A survey of `_TYPES _SET` and `_PROVER-SOLVER _SET` (recorded in ADR-0001) +found **no syntax of claims, premises, steps or evidence in any repository**, +and **no ordering on evidence events of any kind**. All three sub-layers — +well-formedness, continuity, temporality — must be built from scratch. + +Two names promise otherwise and do not deliver: `choreographic-types` has never +contained a line of source on any branch, and typell's "Level 9 Temporal +safety" passes iff a named field is present, examining no event and no order. + +**Closed when:** a claim syntax and an evidence-event ordering exist, with the +diode enforced on the latter. + +### A2 — Layer 3's equivalence side does not exist. `HIGH` + +`echo-types` supplies roughly a quarter of the layer, and only the +*obstruction* half: the fibre `Echo f y = Σ A (λ x → f x ≡ y)`, an invariant +separating two members of one fibre, and "identified members count once". + +There is **no move relation, no quotient, and no normal form anywhere** — which +is the entire equivalence-certificate side. And the one piece most needed is +`echo-types`' own unclosed debt: propositional truncation is *postulated* under +`--safe` and constructed only in a `--cubical` island that Agda's flag rules +forbid the main cone from importing. "Merely inhabited versus how many +witnesses" is exactly what the doubling attack turns on. + +Two candidate substrates were investigated and **refuted with evidence** — +QuandleDB and absolute-zero's CNO — so this is not a matter of wiring something +up. Do not reopen either without new evidence; both refutations are in +ADR-0001. + +**Recorded ruling:** mechanise in **Agda `--cubical`**, not Idris 2. The core +construction is a quotient by admissible moves, and Idris 2's QTT cannot host +quotients or higher inductive types. + +**Closed when:** a move relation and a quotient exist, and an equivalence +certificate can be produced and checked for a worked pair. + +### A3 — Layer 2's vocabulary does not match its implementation. `MEDIUM` + +The terms in circulation — strength, consistency, coherence, +resemblance-warrant-on-merge, p-residue, p-sufficiency — are not the terms in +code. Only **p-sufficiency** is real (`floor(U) ⊑ acc(v)`). **`p-residue` does +not exist in any repository in the estate.** + +What is built (`trope-checker`) is a six-coordinate `Grade`, nine `p-*` +effects, a `Floor`, and a witness-carrying `Verdict`. + +This matters beyond tidiness: part of the ADR-0001 argument read p-residue as +affine resource accounting — a term that could not be grounded — so the +reachability result should be re-derived against the actual grade algebra. +`trope-particularity-workbench/tests/check-vocabulary.sh` hard-fails on any +vocabulary entry outside the nine effects, so introducing these terms as if +established would break a live gate. + +Left deliberately unreconciled in ADR-0001 rather than quietly harmonised. + +**Closed when:** a ruling records whether the six terms are a new Layer 2 +design superseding the grade algebra, an informal gloss of it, or drift. + +--- + +## CI/CD debt + +### C1 — The lockfile epidemic is CURED. `RESOLVED 2026-08-05` + +Until 2026-08-05 there was no Actions lockfile, and **every** workflow +terminated as `startup_failure` before a single step ran, on every branch. +`main` had never been green, which made every other gate decorative. + +Fixed by PR #56, which adopted `.github/workflows/actions.lock`. Re-measured on +`main` the same day — latest run per workflow: + +``` +GREEN (10) Code Quality · CodeQL Security Analysis · Governance · + Guix/Nix Package Policy · Hypatia Security Scan · + RSR Anti-Pattern Check · Runtime Policy · Rust CI · + Secret Scanner · Security Policy +``` + +The gates are now real: Rust CI, CodeQL and Secret Scanner actually execute and +can actually fail. Three residual items remain, tracked below. + +> **Diagnosis trap, retained because it will recur.** `gh pr checks` shows +> *nothing wrong* for a parse-rejected workflow — it emits no check run at all, +> so a PR looks unchecked rather than broken. Use `gh run list --branch `; +> a `?status=failure` query also **excludes** `startup_failure`. + +### C2 — OSSF Scorecard still fails to start. `MEDIUM` + +The one workflow the lockfile fix did not reach: `OSSF Scorecard` is still +`startup_failure` on `main`, so it has never produced a result. PR #59 proposes +making it periodic rather than per-push, which may or may not address the +startup cause — the two are independent. + +**Closed when:** Scorecard produces a conclusion other than `startup_failure`. + +### C3 — Two workflows fail on content. `MEDIUM` + +Genuine failures, not startup problems — which means they are now doing their +job and reporting something real: + +- `Well-Known Standards (RFC 9116 + RSR)` +- `Workflow Security Linter` + +Both were invisible until the lockfile landed, because neither could start. +Neither has been triaged. + +**Closed when:** each either passes or has its finding recorded here as +accepted. + +### C4 — No proof gate. `MEDIUM` + +No workflow invokes Agda, and none runs `scripts/verify-same-cube.sh`. The CI +half of [P1](#p1) and [P2](#p2). Unaffected by the lockfile fix. + +**Closed when:** a workflow compiles `proofs/SameCube.agda` and runs the +verifier, and both can fail the build. + +--- + +## Licence debt + +### L1 — GitHub reports **no licence** for this repository. `MEDIUM` + +`gh repo view --json licenseInfo` returns `null`, despite a 373-line MPL-2.0 +`LICENSE` at the root and `license = "MPL-2.0"` in `Cargo.toml`. The repository +shows as unlicensed to anyone browsing it and to tooling reading the API. + +Cause: `LICENSE` deviates from canonical MPL-2.0 in two places — a **trailing +space** at line 38, and `http://` rather than `https://` at line 360. +`LICENSES/MPL-2.0.txt` is the clean copy. + +Fixed in this change by replacing `LICENSE` with the canonical text; detection +is recomputed on push, so the API result must be re-checked after merge. + +**Closed when:** `gh repo view --json licenseInfo` reports `MPL-2.0`. + +### L2 — SPDX headers are not on line 1. `MEDIUM` + +Twelve of thirteen root-level documents open with `