ARCHITECTURE.adoc

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:

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.

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

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.