refactor: migrate Markdown to AsciiDoc

ARCHITECTURE.adoc

@@ -0,0 +1,299 @@
+== Architecture
+
+____
+*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:
+
+[arabic]
+. *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.
+. *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.
+
+==== The doubling attack, and why Layer 3 precedes Layer 2
+
+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:
+
+....
+Layer 1 (type) ──orientations──▶ Layer 3 (sortal) ──identities──▶ Layer 2 (trope)
+....
+
+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.
+
+==== Status: decided, not built
+
+*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:
+
+* *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.
+
+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).
+
+==== Conventions
+
+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+`.
+
+'''''
+
+=== 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
+
+[width="100%",cols="50%,50%",options="header",]
+|===
+|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.