docs(adr): the sortal layer — three of five counts against the knot layer broke - #55
Merged
Merged
Conversation
…t it broke The type/trope/knot architecture 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. A five-count prosecution was built to press that as hard as possible, then attacked adversarially with a separate fact-check of the theorems it used. Three counts broke, two of them on checkable errors: - Count 1 (topology cannot form) is wrong. The diode constrains edges, but Layer 2's merge and split vertices are themselves critical points of the time function, so a confluence diamond is a closed curve and two of them link with every edge strictly forward in time. The lemmas were right; "unpinned" was the false premise — shared anchors 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. - Count 5 (the layer is only a complexity switch) falls to the doubling attack: one derivation presented twice has an identical pass/fail profile to genuine corroboration on every subdiagram, so the "complete" sweep cannot see it — and answers its own robustness question wrongly without the identity quotient as input. Layer 3 is retained with a restated charter: it adjudicates identity of an argument across presentations and issues equivalence or obstruction certificates. It is upstream of Layer 2's soundness, not downstream of it. Filed as an ADR rather than a dated DESIGN.md entry deliberately. The core idea of this repo was written down correctly in a dated log entry and was invisible there; this record has the same failure profile. Two things recorded as open, not resolved: - The Layer 2 vocabulary in the discussion (strength, consistency, coherence, resemblance-warrant-on-merge, p-residue) does not match committed trope-checker, which has a six-coordinate grade, nine p-* effects, a floor and a witness-carrying verdict. Only p-sufficiency is real; p-residue does not exist anywhere in the estate. Count 3 leaned on it. - "Knot"/"unknot" is already taken by quandledb's KRL and 007's M10 — and QuandleDB describes itself as an equivalence/semantic-identity engine, which is the charter this ADR assigns to Layer 3. Adds docs/decisions/ (estate norm; this repo had no ADR infrastructure). The template is written fresh rather than copied from trope-checker, whose 0000-template.adoc has an AsciiDoc title glued onto a Markdown body. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. Code Review ✅ ApprovedAdds an architecture decision record detailing the survival of the equivalence layer after adversarial testing of five counts against the knot layer. No issues found.
OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Important Your trial ends in 5 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more. Was this helpful? React with 👍 / 👎 | Gitar |
|
|
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
Owner caught a real slippage: the ADR said "affine" but glossed it "one use each", which is linear. Corrected to "at most one use each", plus a section stating the discipline precisely, because the distinction turns out to be load-bearing rather than pedantic. Affine is right for the domain: linear would make an uncited piece of evidence a type error, so weakening has to be free. The reachability argument is indifferent to the choice — it leans only on the absence of contraction, which linear and affine both give — so the result stands and only the wording overclaimed. But neither label is exact. resemblance-warrant-on-merge permits contraction WHEN WARRANTED, so the discipline is affine with a guarded contraction rule. That gap is where the doubling attack lives: - contraction taken freely = one token spent twice. Banned by affinity. - contraction never taken though mandatory = two tokens that are one token. Affinity is BLIND to this; nothing illegal happens, two labels really were spent once each. The doubling attack is the second: not an illegal contraction but a missing one. So Layer 3 does not merely feed Layer 2, it closes a permanent blind spot in it — the omission is undetectable IN the resource algebra, because whether two labels are one token is a fact about identity, not about resources. Layer 2 could not close it by being more careful. Also records the dual gap on the weakening side, in Open: free weakening makes cherry-picking invisible to all three layers, since detecting it means comparing the web against evidence NOT in it. Needs a fourth obligation or an explicit out-of-scope ruling. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… substrate probes
OWNER RULING 2026-08-05: Layer 3 is the SORTAL layer. A sortal supplies a
criterion of IDENTITY and a principle of COUNTING for its instances — the
charter and the doubling attack respectively — and it states the layer order in
its own vocabulary: you cannot count instances before you have individuated
them, so the sortal precedes Layer 2's accounting. Chosen over nine alternatives
on accuracy, collision-freedom, peer fit with type/trope, and honesty about the
mathematics. Runner-up: congruence. The former working title "the equivalence
layer" came LAST — it escapes the metaphor collision only to land in a charter
collision with quandledb's self-description and Tangle's storage/equivalence
layer.
CORRECTION — this record was wrong about its own blast radius. It claimed the
knot vocabulary lived only in conversation and on this branch. It is committed
ON MAIN in _LANGUAGES _SET/nextgen-language-evangeliser across seven files
("types -> carrier · tropes -> recurring equivalence-figures · knot theory ->
certificate"), which already names invariant-path as its governance front-end
and carries its own ADR-6 disclaiming literal knot theory; and on the public
estate site. The literal surface is ~3x what was stated (13,355 match lines);
the largest holder is Tangle-the-language (4,699), not quandledb (1,507). This
record also wrongly dismissed typell-tangle as an unrelated homonym — it maps
Tangle's braid-word types. Rename cost: 2 files now, ~11 after merge, zero code
identifiers either way.
CLOSED — QuandleDB is a homonym, not a substrate. find_path and match are
stubs, find_equivalent is a SQL GROUP BY over hash buckets, the e-graph engine
exists only as prose, and all 36 shipped rows carry descriptor_version
'fallback-v1' so no quandle was ever computed. Decisively, the mathematics does
not match: every move this layer quotients by CHANGES the abstract graph, and
paraphrase changes labels — to which topological invariants are blind. A quandle
fingerprint cannot see the doubling attack and would return false positives.
NEW — substrate survey (proofs independently typechecked, not taken on trust):
- Layer 1: nothing, anywhere. No syntax of claims, no ordering on evidence
events. choreographic-types has never contained a line of source on any branch.
- Layer 2: two real wins. tropical-types derives the whole retention order from
one line of idempotence with no case split, axiom-free, behind a real CI gate;
echo-types proves path-independence of degradation holds precisely if the
retention order is propositional, with a countermodel.
- This layer: a quarter, obstruction side only. echo-types supplies the fibre
and "identified members count once"; nothing on the equivalence side exists
anywhere — no moves, no quotient, no normal form.
- absolute-zero's CNO: REFUTED as substrate, machine-checked against its own
Coq (any_jump_is_cno — the nullity relation excludes the PC, so it is blind to
control flow, which is what every move here is). Survives as a negative case
study of the two traps this layer must avoid. Its Lean FilesystemCNO and
LambdaCNO each prove False while lake build reports success — do not import.
- Tooling ruling: mechanise in Agda --cubical, not Idris 2 (QTT cannot host
quotients or HITs).
- Numbering hazard: three live L1-L10 schemes; never write bare L1/L2/L3.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath
changed the title
hyperpolymath
added a commit
that referenced
this pull request
Aug 5, 2026
…ure (#56) **This repo has had no working CI.** All 16 workflows return `startup_failure` in 0s; the last 30 runs are `startup_failure` without a single exception. That has a consequence worth stating before anything else: **the two open PRs here (#53, #55) have never been verified by anything.** Their green-looking absence of failures is an absence of checks. ## Cause Workflow-lockfile enforcement is active on this account, and this repo had no `.github/workflows/actions.lock`. ## The cure, in four steps Proven on haec#50 and trope-particularity-workbench#45. It takes four steps because **each one's failure is invisible until the previous is fixed** — they surface strictly one at a time: 1. **`gh actions-lock`** — generates the lockfile, normalises pins to readable tags. 2. **Hoist SPDX back to line 1.** `actions-lock` inserts its own banner as line 1, and the workflow linter requires the SPDX header there — so the tool that cures the startup failures reddens every workflow file unless this is undone in the same commit. 3. **Hand-author an empty `[]` lockfile entry per reusable caller** (6 here). `gh actions-lock` **skips reusable-workflow callers**, so without this they remain `startup_failure` while everything else goes green — which reads as a partial fix rather than a missing step. 4. **Re-pin those callers** to standards `bd0df9ead7fa`, the commit that made the governance check lockfile-aware. Verified present via the commits API rather than copied. ## Expect failures Nothing here has been checked in a long time. The first green run is a **starting point, not a result** — some of what surfaces will be real and long-standing. If two callers come back `startup_failure` after this, the cause is permission escalation (a reusable requesting more than its caller grants is rejected before any job starts, producing no log); that was the last residual on tpw#45. Found during the 2026-08-05 estate CI/CD census, which measured 8 repos mostly dead and 47 partly dead out of 421. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
hyperpolymath
added a commit
to hyperpolymath/nextgen-language-evangeliser
that referenced
this pull request
Aug 5, 2026
Companion to **hyperpolymath/invariant-path#55**. ## Why this repo This repo carries the same three-layer framing as invariant-path — `types -> carrier · tropes -> recurring equivalence-figures · knot theory -> certificate` — across seven files, and already names invariant-path as "the governance front-end". Its **ADR-6** flagged the knot-theory lens as *"an aspirational lens, not a literal computation"* and *"perceived as rhetoric, pending historical confirmation"*. That was the right call, and it is no longer pending. ## What the ruling found The framing was attacked deliberately in invariant-path ADR-0001 (a five-count case against the third layer, three counts of which broke under adversarial review): - **ADR-6 was correct that classical knot theory does not apply.** A forward-only ordering on evidence makes admissible strands monotone in time, and monotone strands comb flat. - **But the layer is not thereby empty** — which the caveat left open. Merge and split vertices are critical points of the time function, so confluence diamonds are closed curves and two of them link with *every edge still pointing forward in time*. What survives is not topology but **individuation**. - The layer adjudicates **identity of an argument across presentations**, issuing an equivalence certificate (a move sequence preserving the claim) or an obstruction certificate. - Hence **sortal** — from the same literature `trope` came from. A sortal supplies a *criterion of identity* and a *principle of counting* for its instances. Both halves do work: the criterion decides "same idea", and the count decides whether two corroborating lines are two witnesses or one witness echoed. ## A convergence worth recording `README.adoc:63` already reaches for echo-types' fibre — `Echo f y := Σ (x : A), f x ≡ y` — to model "crossings are lossy-with-residue". Independently, a survey of the `_TYPES _SET` repos concluded that same fibre is the right home for the third layer's question, because a fibre is exactly *"which distinct presentations collapsed to the same argument"*. Two lines of thought, same construction, arrived at separately. That is better evidence than either alone. ## Scope Seven files, prose and metadata only. **No claim is strengthened**: `invariant` keeps its precise sense, no knot-invariant is computed, no Curry–Howard fidelity is claimed. A hedge becomes a citation. Verified: `asciidoctor` parses all four `.adoc` files clean; both `META.a2ml` files balance (parens, brackets, quotes) and each changed exactly one line. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Aug 7, 2026
#55, #60) Squashes the documentation stack. Three PRs, one commit. #53 — state the idea where agents read it first A (core-idea ...) block in 0-AI-MANIFEST.a2ml, marked DO-NOT-PARAPHRASE: a claim can hold on BOTH sides of a domain transition and still not MEAN the same thing; the invariant is 'the SAME CLAIM here and there'. Previously this existed only in a dated DESIGN.md entry, where it was accurate and invisible, so every agent read the plumbing and reinvented the idea. #55 — ADR-0001: Layer 3 is the SORTAL layer A five-count case against the third layer was built deliberately and attacked adversarially. Three of the five counts broke: - 'the diode abolishes the subject matter' is wrong; the diode constrains edges but cannot constrain the Morse structure at merge/split vertices, so confluence diamonds are closed curves and two of them link with every edge still forward in time. - 'the plane is notation' falls to intrinsic linking. - 'it is only a complexity switch' falls to the doubling attack. The layer is retained as the sortal layer: it adjudicates identity of an argument across presentations, issuing equivalence or obstruction certificates, and it is UPSTREAM of Layer 2's soundness. Also corrects affine vs linear, and names the blind spot that gap creates. #60 — documentation refresh + live debt register ARCHITECTURE.md was template boilerplate describing directories this repo does not have; rewritten around the three layers, which are the principal subject. README described a superseded verification method (canonical text, where the verifier now compares typed-wasm sha256) — the README had drifted from the tool in exactly the way the tool exists to catch. New docs/DEBT.md across six dimensions. LICENSE replaced with canonical MPL-2.0: it deviated by a trailing space and one http/https, and GitHub reported NO licence as a result. Merged with --admin. The main ruleset is unsatisfiable by construction here: required_deployments demands a github-pages deployment that does not occur, code_coverage demands 95% with no coverage reporting configured, and the required context 'governance / Validate Hypatia Baseline' reports SKIPPED. All 14 checks on the docs content were green; the two red workflows (Workflow Security Linter, and a stale Hypatia run) are pre-existing on main and are tracked as C3 in the new debt register.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #53 (it quotes the
(core-idea (statement …))block that #53 introduces). Base retargets tomainautomatically 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.mdentryDeliberate. The core idea of this repository was written down correctly, and only, in a dated
DESIGN.mdentry (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-residuedoes not exist anywhere in the estate. What is built intrope-checker@69221adis a six-coordinateGrade, ninep-*effects, aFloor, and a witness-carryingVerdict. 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.shhard-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
(statement …)is reproduced verbatim — diffed character-by-character against0-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).file:linecitation re-resolved against a recorded SHA.Note:
trope-checkerhas two working copies at different commits (hyper-repos@69221ad,_TROPES _SET@680fc20). Citations use the former and record the SHA.🤖 Generated with Claude Code