Three Layers

The three-layer claim checker

A claim is checked by three layers, each answering a question the others cannot. Invariant Path is the governance front-end: 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	Name	Question	Where it is built
1	type	Is this admissible on form alone?	Nowhere yet
2	trope	Does this evidence survive the leap for this use?	trope-checker, hermeneia
3	sortal	Are these two presentations the same argument?	Nowhere yet

Never 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) and so on; prefix foreign references kat-L7, ty-L9.

Layer 1 — type

Formal admissibility, checkable on form alone, with no judgement of evidence quality.

• Well-formedness — is this a claim at all?
• Continuity / through-line — does the argument connect end to end?
• Temporality, "the diode" — evidence must precede conclusion; no backward edges; applied per claim-type.

The diode sits in Layer 1 deliberately, so anything downstream inherits strand orientations from a clean form-only rule rather than from Layer 2's purpose-indexed judgements.

What the diode actually buys

Less than it looks. It rejects only label-honest backward edges — and forgery is precisely the crime of having correct form. Type systems verify structure given trusted labels; forgery attacks the labels. So the diode buys well-formedness, not security.

Three open problems follow:

1. The clock must be epistemic, not ontic. It must record when evidence became available or was committed, not when events happened — otherwise retrodiction (history, forensics) falsely fails to type-check.
2. Epistemic time is a partial order. Distinct sources commit at causally unrelated instants, so there is no scalar clock, and verdicts must be proved invariant across admissible interleavings.
3. Composition-forgery. Because the diode applies 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 composite path can run forward in every chart while its endpoints land the conclusion earlier than where it began — manufacturing priority with no backward edge, no forged label, no fabricated anchor, and no cycle. This is holonomy: 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, in trope-checker and hermeneia:

• a six-coordinate Grade — four Fate fields plus Bond and Merge;
• nine p-* effects, three of them deceptive and absorbing under composition;
• a Floor — a use-model as a partial demand vector;
• a verdict Sufficient | Insufficient that carries a witness edge naming the coordinate and edge responsible;
• p-sufficiency: floor(U) ⊑ acc(v).

Grades compose associatively along transformation paths, the fidelity coordinate accumulating tropically.

Resource discipline: affine with a guarded contraction rule. At most once — weakening free, contraction not free — but contraction is permitted when a resemblance warrant licenses it. That is not plain affine logic, and the gap is where the doubling attack lives.

⚠ Vocabulary warning. The terms in circulation are not the terms in code. Of strength, consistency, coherence, resemblance-warrant-on-merge, p-residue and p-sufficiency, only p-sufficiency is real, and p-residue exists in no repository in the estate. check-vocabulary.sh hard-fails on any entry outside the nine effects.

Layer 3 — sortal

Ruled 2026-08-05 in ADR-0001, 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, issuing:

• 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.

Why "sortal"

From the same literature trope came from. A sortal (Locke, Strawson, Geach, Wiggins, Lowe) is a concept supplying a criterion of identity and a principle of counting for its instances. Both halves are load-bearing: the criterion decides "same argument", the count decides whether two corroborating lines are two witnesses or one witness echoed.

It was chosen over nine alternatives. Runner-up was congruence. The former working title "the equivalence layer" came last — it escapes a metaphor collision only to land in a charter collision.

The doubling attack

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. No resemblance-warrant fires, because a label-keyed ledger sees two tokens.

The doubled web and an honestly-redundant two-witness web have identical pass/fail profiles on every subdiagram — so no sweep can 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.

It 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.

The dependency arrow

Layer 1 (type) ──orientations──▶ Layer 3 (sortal) ──identities──▶ Layer 2 (trope)

The original design had only the first arrow: temporality sits in Layer 1 so the layer above inherits clean orientations. The missing arrow is the second. 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, and says so.

A survey of existing formal work found:

• Layer 1 — no substrate anywhere. No syntax of claims, no ordering on evidence events. Build from scratch. (choreographic-types has never contained a line of source on any branch.)
• Layer 2 — real support from tropical-types (retention order derived from one line of idempotence, axiom-free, real CI gate) and echo-types (path-independence of degradation holds precisely if the retention order is propositional, with a countermodel).
• Layer 3 — about a quarter, obstruction side only, from echo-types' fibre Echo f y = Σ A (λ x → f x ≡ y). Nothing on the equivalence side exists anywhere: no move relation, no quotient, no normal form.

Two candidate substrates were refuted with evidence and should not be reopened without new evidence: QuandleDB (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).

Tooling ruling: mechanise Layer 3 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.

Open gaps are tracked as A1–A3 in docs/DEBT.md.