docs: ADR-6 resolved — the third layer is the sortal layer - #52
Conversation
…ry retired This repo has carried the same three-layer framing as invariant-path — "types -> carrier · tropes -> recurring equivalence-figures · knot theory -> certificate" — across seven files, with the knot-theory lens honestly flagged as "an aspirational lens, not a literal computation" and "perceived as rhetoric, pending historical confirmation". It is no longer pending. The framing was tested adversarially and ruled on in invariant-path ADR-0001 (2026-08-05). ADR-6 anticipated the conclusion; this commit records the argument behind it and the resulting name. What the ruling found: - Classical knot theory genuinely does not apply. A forward-only ordering on evidence makes admissible strands monotone in time, and monotone strands comb flat. ADR-6's caveat was correct. - But the third layer is not thereby empty, which the caveat left open. Merge and split vertices are critical points of the time function, so confluence diamonds are closed curves and two of them link with every edge still forward in time. What survives is not topology but individuation. - The layer adjudicates identity of an argument across presentations, issuing an equivalence certificate (a move sequence preserving the claim) or an obstruction certificate. - Hence "sortal", from the same literature "trope" came from: a sortal supplies a criterion of identity AND a principle of counting for its instances. Both halves are load-bearing — the criterion decides "same idea", the count decides whether two corroborating lines are two witnesses or one witness echoed. Worth noting a convergence rather than a coincidence: this repo already reaches for echo-types' fibre (`Echo f y := Σ (x : A), f x ≡ y`) to model "crossings are lossy-with-residue". The fibre is precisely "which distinct presentations collapsed to the same argument" — the sortal question in echo-types' own vocabulary. The two lines of thought arrived at the same construction independently, which is better evidence for it than either alone. No claim is strengthened here: "invariant" keeps its precise sense, no knot-invariant is computed, and no Curry-Howard fidelity is claimed. What changes is that a hedge becomes a citation. Co-Authored-By: Claude Opus 5 <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 ✅ ApprovedDocumentation update resolving ADR-6 to establish the sortal layer as the criterion of identity and principle of counting, retiring knot theory across seven files. 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}
1 participant
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):
tropecame 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:63already 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 _SETrepos 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:
invariantkeeps its precise sense, no knot-invariant is computed, no Curry–Howard fidelity is claimed. A hedge becomes a citation.Verified:
asciidoctorparses all four.adocfiles clean; bothMETA.a2mlfiles balance (parens, brackets, quotes) and each changed exactly one line.🤖 Generated with Claude Code