feat(tg-11): epistemic types — Epi[k, ρ, τ], non-factive by construction (#98)

Wires `hyperpolymath/epistemic-types` into the mechanised core,
following the route TG-10 took for echo. **Lean 0 errors, sorry/axiom
gate clean.**

## The commitment: a warrant is not knowledge

`Epi[κ, ρ, τ]` — at standpoint κ, evidence of type ρ purporting to
support a claim of type τ. The claim type appears in the type and **no
elimination rule delivers it**. `evidence` is the sole projection, and
it yields ρ.

That mirrors upstream precisely:

- `Warrant.agda` gives the record only an `Evidence` field —
deliberately *not* `Evidence → A`, because that "would make every
warrant factive" — and puts extraction in a separate `SoundWarrant`.
- `Base.agda` splits `FactiveModality` (with `reflect : E κ A → A`) from
`BeliefModality` (without), rather than treating belief as knowledge
with a missing proof.

The absence here is that same design choice, mechanised.

## Six capstones

| Theorem | What it establishes |
|---|---|
| `epi_evidence_recovers` | `evidence ∘ warrant` returns the token |
| **`epi_claim_is_opaque`** | two warrants, same evidence, **different
claims**, observationally identical |
| `epi_only_yields_evidence` | from `Epi[κ,ρ,τ]` the only elimination is
at ρ |
| `epi_distinguishes_standpoints` | κ₁ ≠ κ₂ gives genuinely different
types |
| `epi_roundtrip_typed` | type safety of intro + projection |
| `epi_over_echo_typed` | `Epi[κ, Echo[ρ,τ], σ]` — the modalities
**nest** |

`epi_claim_is_opaque` is the exact dual of
`echo_distinguishes_collapsed`: **echo *reveals* what `close` forgot; a
warrant *withholds* what it purports.** Holding evidence is not holding
the fact.

`epi_over_echo_typed` mirrors `EpistemicEcho` in `EchoBridge.agda`,
which is explicit that these are different modalities — echo grades
irrecoverability, epi indexes standpoints — and that they compose
without collapsing.

## Metatheory extended, not weakened

Progress, Preservation, Determinism, TypeSafety, `infer_sound`,
`infer_complete` all cover the new fragment, plus a new `canonical_epi`
lemma.

Worth noting where non-factivity actually lands: in preservation, the
`evidenceVal` case inverts `tEvidence` then `tEpiVal` and returns the
**token's** typing (`he`), never the claim's (`hc`). Non-factivity is
discharged by the type system rather than asserted in a comment.

## Both engines

OCaml mirrors it — `TEpi` former, `Warrant`/`EpiVal`/`Evidence`, `VEpi`
runtime value, typing and evaluation. TG-3 extended with 4 pins
(including that `evidence` yields the *evidence* type, never the claim);
differential regenerated and **kernel-checked: 496 obligations, 0
errors**. TG-3 self-check 1008 → 1012.

## ⚠ Registered honestly — A-TG-11.1

What the simply-typed shadow does **not** model:

- standpoints are `Nat`, not an arbitrary index set `K`;
- upstream's `LawfulModality` functor laws, `FactiveModality.reflect`
and `ReturnModality.return` are omitted (all opt-in there);
- **the real gap** — the claim is *carried* in the value rather than
*erased*, because erasing it would break uniqueness of typing in a
system without quantities.

A **QTT** treatment (quantity `0` on the claim) would be the faithful
version — which is the same conclusion the linear/affine discussion
reached independently.

## Tests

6 typecheck cases, including two negatives: that `evidence` never
returns the claim type when the two differ, and that `evidence` of a
non-warrant is rejected. Typecheck suite 129 → 135; all suites green;
corpus and RSR gates pass.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

ASSUMPTIONS.md

@@ -34,6 +34,7 @@ Cross-references use `[[A-TG-N.M]]` syntax, resolved here.
 | A-TG-7.1 | MATH | Word problem in the braid group `B_n` is solvable in polynomial time (Birman–Ko–Lee / Garside normal form) | TG-7 | Birman–Ko–Lee 1998; _A New Approach to the Word and Conjugacy Problems in the Braid Groups_ |
 | A-TG-7.2 | IMPL | `braidEquiv` (`proofs/Tangle.lean`) and `braid_equiv.ml` implement Dehornoy handle reduction **correctly**, and agree with each other. Since the 2026-07-29 ruling (#50) routed `==` through them, this is **load-bearing for the semantics of `==`**: the Step relation's metatheory is proven only *relative to* `braidEquiv`, never that it decides braid-group equality. Evidenced by testing (2220 + 8 assertions), not proof. Retired by the mechanised Garside/Dehornoy proof (#51, research-grade). The Lean port is additionally **fuel-bounded**, so termination is assumed rather than proven. | TG-7 | `compiler/lib/braid_equiv.ml`; `proofs/Tangle.lean` §BRAID-GROUP EQUIVALENCE; `compiler/test/tg7` |
 | A-TG-92.1 | MATH | Comparing braid words of different widths is decided in B_max(n,m) via the standard embedding Bn -> Bn+1 (adjoin a strand no generator touches). Used to justify widening `T-Eq-Word` (#92) and the match-arm width join. The embedding is standard mathematics but is **asserted in prose, not mechanised** — no Lean lemma states it. What IS machine-checked is that the metatheory (Progress/Preservation/Determinism/TypeSafety, infer_sound/complete) holds under the widened rule, and that OCaml `infer_expr` still agrees with Lean `infer` on the corpus (TG-3, 496 obligations). | TG-7 / #92 | `proofs/Tangle.lean` (`tEqWord`, `infer`); `compiler/lib/typecheck.ml` |
+| A-TG-11.1 | DESIGN | The simply-typed shadow is FAITHFUL to `epistemic-types`: `Epi[k,rho,tau]` models `Epi K k A` (Warrant.agda) with standpoints as Nat indices rather than an arbitrary index set K, and it omits the upstream `LawfulModality` functor laws, `FactiveModality.reflect` and `ReturnModality.return` (all deliberately opt-in upstream). What IS mechanised here is non-factivity: no elimination yields the claim. Erasure and quantity are NOT modelled - the claim is carried in the value rather than erased, because erasing it would break uniqueness of typing in a system without quantities. A QTT treatment (quantity 0 for the claim) would be the faithful version. | TG-11 | `proofs/Tangle.lean` section EPISTEMIC; `epistemic-types/src/EpistemicTypes/{Base,Warrant,EchoBridge}.agda` |
 | A-TG-8.1 | DESIGN | Each dialect's grammar is a strict superset of core's EBNF (`tangle.ebnf`) | TG-8 | `dialects/*/grammar.ebnf` |
 | A-TG-8.2 | DESIGN | Each dialect's typing rules are additive (new constructors + their typing rules only; no modification of existing rules) | TG-8 | Per-dialect spec |
 | A-TG-9.1 | DESIGN | `tangle-lsp` emits diagnostics in four documented categories (`PARSE_ERROR`, `MISSPELLING_HINT`, `STRUCTURAL_HINT`, `NAME_HINT`); only `PARSE_ERROR` corresponds to a grammar-level rejection. The other three are LSP-only by design (Option B from TG-9 audit; Option A — full refinement via FFI to `typecheck.ml` — remains queued at #28). Each emission site is tagged in the `Diagnostic.source` field as `tangle-lsp[CATEGORY]`. | TG-9 | `compiler/tangle-lsp/src/backend.rs`; `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md` |

PROOF-NEEDS.md

@@ -60,6 +60,7 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli
 | TG-5 | `compositional.ml` (418 LoC) rewriter preserves types | TP | OCaml property test | P2 | — | **LANDED** (`compiler/test/tg5/tg5_invariants.ml`, 189 assertions in `dune runtest`). compositional is below the Ty layer, so "preserves types" = preserves the PD-lowering structural invariants + echo residue-recovery: `OpenWord`/`ClosedDiagram`/`EchoClosed` each pinned (closedness, `\|crossings\|`=unit-length, source unit-expanded, **verbatim residue** for `EchoClose` with `expand(residue)=diagram word` and echo-diagram pdv1-identical to plain `close`), error paths, count pins. Lean IR model = optional later rung |
 | TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | differential + Lean bisimulation | P1 | — | **RUNG LANDED (differential)**: `compiler/tangle-wasm/tests/differential.rs` EXECUTES the generated wasm with the `wasmi` interpreter (dev-dep) and checks the braid strand-permutation equals an independent reference model (trefoil, non-commuting pairs, braid-relation pairs, 5-strand weave). Validates codegen vs the permutation semantics; not a cross-binary diff against `eval.ml`, and Markov helpers untested. Full source↔wasm bisimulation (WasmCert) remains research-grade |
 | TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | — | **SEMANTICS LANDED 2026-07-29** (owner ruling #50 → (a) true braid-group equivalence). `==` on braids now decides braid-group equality in BOTH engines: OCaml `eval.ml` `Eq`/`Isotopy` route through `compiler/lib/braid_equiv.ml`; Lean `Step.eqBraids`/`eqIdBraid`/`eqBraidId` (and the three `echoEq` counterparts) use `braidEquiv`, a faithful in-Lean port of the same Dehornoy procedure. Progress/Preservation/Determinism re-verified unchanged (they need only a total function into `Bool`). Tested: `compiler/test/tg7` 2220 assertions + 8 new semantics-distinguishing cases in `test_eval.ml`. **Remaining (research-grade): the mechanised Garside/Dehornoy correctness proof — `braidEquiv` is TRUSTED, NOT PROVEN; the Step relation is proven only RELATIVE to it** |
+| TG-11 | Epistemic types: `Epi[k, rho, tau]` former + `warrant`/`epiVal`/`evidence`, with Progress/Preservation/Determinism/TypeSafety extended to cover them, and NON-FACTIVITY established (no elimination delivers the claim) | TP / DOM | Lean 4 | P1 | - | **LANDED**: `proofs/Tangle.lean` §EPISTEMIC. Six capstones: `epi_evidence_recovers`, `epi_claim_is_opaque`, `epi_only_yields_evidence`, `epi_distinguishes_standpoints`, `epi_roundtrip_typed`, `epi_over_echo_typed`. Mirrors `hyperpolymath/epistemic-types` (Warrant.agda / Base.agda / EchoBridge.agda). TG-3 extended: 4 new pins, differential regenerated and kernel-checked (496 obligations, 0 errors) |
 | TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | OCaml model + Lean per-dialect | P3 | — | **TEMPLATE LANDED (virtual-knot)**: `compiler/lib/dialect_vk.ml` models VBₙ ⊃ Bₙ as core + a virtual layer that DELEGATES to `Braid_equiv` on the real fragment, so conservativity holds by construction; `compiler/test/tg8` (2311 assertions) verifies faithful embedding, core-delegation, invariant agreement, proper extension, virtual involution, honest undecided-frontier. Remaining: surface-syntax parser integration, the other 4 dialects (replicate the template), and a Lean conservativity proof |
 | TG-9 | LSP diagnostics are a subset of `HasType` failures (no LSP-only diagnostics) | INV | Audit + refactor | P2 | — | **LANDED** (`tangle-lsp` delegates all diagnostics to `tanglec --check` ⇒ `compiler/lib/check.ml`; hand-rolled LSP-only false positives removed. Subset holds by construction. Tests: `test_check.ml` + tangle-lsp unit/delegation tests) |
 | TG-10 | Echo-types integrated into the type system: `Echo[ρ,τ]` former + `echoClose`/`lower`/`residue`/`echoAdd`/`echoEq` + product type (`pair`/`fst`/`snd`), with Progress/Preservation/Determinism/TypeSafety extended to cover them and the non-injectivity / residue-recovery capstones proven | TP / DOM | Lean 4 | P1 | — | **LANDED** (`proofs/Tangle.lean` §ECHO-TYPES) |

compiler/lib/ast.ml

@@ -93,6 +93,14 @@ and expr =
   | EchoAdd   of expr * expr          (* echo-preserving addition (residue = summand pair) *)
   | EchoEq    of expr * expr          (* echo-preserving equality (residue = operand pair) *)
 
+  (* ---- Epistemic (warranted claim) — mirrors §EPISTEMIC in
+   *      proofs/Tangle.lean and epistemic-types' Warrant.agda.
+   *      NON-FACTIVE: `Evidence` is the only elimination.  There is no
+   *      operation taking a warrant to the thing warranted. ---- *)
+  | Warrant   of int * expr * expr    (* warrant κ claim evidence (redex) *)
+  | EpiVal    of int * expr * expr    (* formed warrant: standpoint, claim, token *)
+  | Evidence  of expr                 (* project the evidence token (ONLY elimination) *)
+
   (* ---- Literals ---- *)
   | BraidLit  of generator list
   | Identity

compiler/lib/eval.ml

@@ -42,6 +42,11 @@ type value =
   | VFun       of string list * expr * env  (** Closure: params, body, captured env *)
   | VUnit                             (** Unit / void result *)
   | VInvariant of string * string     (** Invariant name, result string *)
+  | VEpi       of int * value * value  (** Formed warrant: standpoint, claim, token.
+                                          The claim is CARRIED but has no
+                                          projection — `Evidence` is the only
+                                          elimination.  Mirrors epiVal in
+                                          proofs/Tangle.lean. *)
   | VEcho      of value * value       (** Formed echo: residue, result —
                                           mirrors [echoVal] in proofs/Tangle.lean *)
   | VPair      of value * value       (** Product value *)
@@ -92,6 +97,8 @@ let rec pp_value (v : value) : string =
   | VFun _        -> "<function>"
   | VUnit         -> "()"
   | VInvariant (name, result) -> Printf.sprintf "%s = %s" name result
+  | VEpi (k, c, ev) ->
+    Printf.sprintf "warrant[%d](%s, %s)" k (pp_value c) (pp_value ev)
   | VEcho (res, result) ->
     "echo(" ^ pp_value res ^ ", " ^ pp_value result ^ ")"
   | VPair (a, b) ->
@@ -396,6 +403,21 @@ let rec eval_expr (env : env) (e : expr) : value =
              (pp_value v)
     end
 
+  (* Epistemic.  `warrant` forms the value; `evidence` is the sole projection
+     and yields the TOKEN.  There is deliberately no operation returning the
+     claim — holding a warrant is not holding the fact. *)
+  | Warrant (k, claim, ev) ->
+    VEpi (k, eval_expr env claim, eval_expr env ev)
+
+  | EpiVal (k, claim, ev) ->
+    VEpi (k, eval_expr env claim, eval_expr env ev)
+
+  | Evidence e ->
+    begin match eval_expr env e with
+    | VEpi (_, _, ev) -> ev
+    | v -> eval_error "evidence requires a warrant, got %s" (pp_value v)
+    end
+
   | Cap (_e1, _e2) ->
     (* Cap creates a tangle that absorbs two strands — a single-crossing
        cup/cap pair.  Represented as an empty closed tangle. *)

compiler/lib/pretty.ml

@@ -276,6 +276,17 @@ let rec pp_expr ctx = function
     emit ctx " yield strands ";
     pp_strand_list ctx w.weave_outputs
 
+  | Warrant (k, c, ev) ->
+    emit ctx "warrant["; emit ctx (string_of_int k); emit ctx "](";
+    pp_expr ctx c; emit ctx ", "; pp_expr ctx ev; emit ctx ")"
+
+  | EpiVal (k, c, ev) ->
+    emit ctx "epiVal["; emit ctx (string_of_int k); emit ctx "](";
+    pp_expr ctx c; emit ctx ", "; pp_expr ctx ev; emit ctx ")"
+
+  | Evidence e ->
+    emit ctx "evidence("; pp_expr ctx e; emit ctx ")"
+
   | Crossing (a, op, b) ->
     emit ctx "(";
     emit ctx a;

compiler/lib/typecheck.ml

@@ -44,6 +44,11 @@ type ty =
   | TProd   of ty * ty              (** ρ × σ — product / residue carrier for lossy ops *)
   | TEcho   of ty * ty              (** Echo[ρ, τ] — structured loss: residue ρ, result τ.
                                         Mirrors Ty.echo in proofs/Tangle.lean. *)
+  | TEpi    of int * ty * ty        (** Epi[κ, ρ, τ] — at standpoint κ, evidence ρ
+                                        purporting to support claim τ.  Mirrors
+                                        Ty.epi in proofs/Tangle.lean.  τ appears
+                                        in the type but NO rule eliminates to it:
+                                        a warrant is not knowledge. *)
 
 (** Function signature: (param_types) -> return_type. *)
 type fun_sig = {
@@ -100,6 +105,7 @@ let rec pp_ty = function
   | TStr           -> "Str"
   | TProd (a, b)   -> Printf.sprintf "(%s * %s)" (pp_ty a) (pp_ty b)
   | TEcho (r, t)   -> Printf.sprintf "Echo[%s, %s]" (pp_ty r) (pp_ty t)
+  | TEpi (k, r, t) -> Printf.sprintf "Epi[%d, %s, %s]" k (pp_ty r) (pp_ty t)
 
 (* ================================================================== *)
 (*  Environment operations                                             *)
@@ -218,6 +224,26 @@ let rec infer_expr (gamma : env) (sigma : strand_ctx) (e : expr) : ty =
     ) wb.weave_outputs in
     TTangle (input_boundary, output_boundary)
 
+  (* [T-Warrant] / [T-Epi-Val] / [T-Evidence] — epistemic.
+     Note the absence: no case here produces τ from an Epi.  `Evidence` yields
+     the token type ρ, and that is the only elimination.  Contrast `Lower`,
+     which DOES deliver an echo's result. *)
+  | Warrant (k, claim, ev) ->
+    let t_claim = infer_expr gamma sigma claim in
+    let t_ev    = infer_expr gamma sigma ev in
+    TEpi (k, t_ev, t_claim)
+
+  | EpiVal (k, claim, ev) ->
+    let t_claim = infer_expr gamma sigma claim in
+    let t_ev    = infer_expr gamma sigma ev in
+    TEpi (k, t_ev, t_claim)
+
+  | Evidence e ->
+    begin match infer_expr gamma sigma e with
+    | TEpi (_, rho, _) -> rho
+    | t -> type_error "evidence requires an Epi[k, rho, tau], got %s" (pp_ty t)
+    end
+
   (* ---- Variables [T-Var] ---- *)
 
   | Var name ->
@@ -652,6 +678,7 @@ and strand_type_of_ty (t : ty) : strand_type =
   | TTangle _ -> StrandDefault
   | TProd _ -> StrandDefault
   | TEcho _ -> StrandDefault
+  | TEpi _ -> StrandDefault
 
 (** Convert a strand_type to a boundary element for self-crossing. *)
 and strand_to_type (st : strand_type) : strand_type = st
@@ -725,7 +752,9 @@ let rec expr_calls (f : string) (e : expr) : bool =
   | Cap (e1, e2) | Cup (e1, e2) | Pair (e1, e2)
   | EchoAdd (e1, e2) | EchoEq (e1, e2) -> go e1 || go e2
   | UnaryOp (_, e1) | Close e1 | Mirror e1 | Reverse e1 | Simplify e1
-  | Twist e1 | EchoClose e1 | Lower e1 | Residue e1 | Fst e1 | Snd e1 -> go e1
+  | Twist e1 | EchoClose e1 | Lower e1 | Residue e1 | Fst e1 | Snd e1
+  | Evidence e1 -> go e1
+  | Warrant (_, c, ev) | EpiVal (_, c, ev) -> go c || go ev
   | Weave wb -> go wb.weave_body
   | BraidLit _ | Identity | BoolLit _ | IntLit _ | FloatLit _
   | StringLit _ | Var _ | Crossing _ -> false

compiler/test/test_typecheck.ml

@@ -1089,6 +1089,40 @@ let test_echo_types () =
     ] in
     infer [] (Match (BraidLit [sigma 1], arms)) = TWord 2);
 
+  (* ---------------------------------------------------------------- *)
+  (* EPISTEMIC TYPES. The commitment is NON-FACTIVITY: holding a warrant  *)
+  (* is not holding the fact. `Evidence` is the ONLY elimination, and it  *)
+  (* yields the token type, never the claim type.                        *)
+  (* ---------------------------------------------------------------- *)
+
+  test "epi: warrant types as Epi[k, rho, tau]" (fun () ->
+    infer [] (Warrant (0, IntLit 1, BraidLit [sigma 1]))
+      = TEpi (0, TWord 2, TNum));
+
+  test "epi: evidence yields the EVIDENCE type, not the claim" (fun () ->
+    (* The heart of it. Claim is Num, evidence is Word[2]; the projection
+       must give Word[2]. If it gave Num, the warrant would be factive. *)
+    infer [] (Evidence (Warrant (0, IntLit 1, BraidLit [sigma 1])))
+      = TWord 2);
+
+  test "epi: NO elimination delivers the claim type" (fun () ->
+    (* Guard: evidence must never return the claim type when the two differ. *)
+    infer [] (Evidence (Warrant (0, StringLit "claimed", BraidLit [sigma 1])))
+      <> TStr);
+
+  test "epi: standpoints are distinguished" (fun () ->
+    infer [] (Warrant (1, IntLit 1, IntLit 2))
+      <> infer [] (Warrant (2, IntLit 1, IntLit 2)));
+
+  test "epi: composes over echo without collapsing into it" (fun () ->
+    (* EpistemicEcho from EchoBridge.agda: standpoint k with access to an
+       echo. The two modalities nest; neither absorbs the other. *)
+    infer [] (Warrant (1, IntLit 0, EchoClose (BraidLit [sigma 1])))
+      = TEpi (1, TEcho (TWord 2, TWord 0), TNum));
+
+  test "epi: evidence of a non-warrant is rejected" (fun () ->
+    raises (fun () -> infer [] (Evidence (IntLit 1))));
+
   test "#92 match arms of genuinely different KINDS still fail" (fun () ->
     let arms = [
       { arm_pattern = PatIdentity;  arm_body = IntLit 1 };

compiler/test/tg3/tg3_emit.ml

@@ -61,6 +61,7 @@ let rec lean_ty (t : ty) : string =
   | TWord n      -> Printf.sprintf "(.word %d)" n
   | TEcho (r, v) -> Printf.sprintf "(.echo %s %s)" (lean_ty r) (lean_ty v)
   | TProd (a, b) -> Printf.sprintf "(.prod %s %s)" (lean_ty a) (lean_ty b)
+  | TEpi (k, r, t) -> Printf.sprintf "(.epi %d %s %s)" k (lean_ty r) (lean_ty t)
   | TTangle _    ->
     failwith "TG-3: TTangle has no Lean image — a non-core term leaked into the corpus"
 
@@ -69,6 +70,7 @@ let rec lean_ty (t : ty) : string =
 let rec ty_tangle_free = function
   | TTangle _              -> false
   | TEcho (a, b) | TProd (a, b) -> ty_tangle_free a && ty_tangle_free b
+  | TEpi (_, r, t) -> ty_tangle_free r && ty_tangle_free t
   | TWord _ | TNum | TStr | TBool -> true
 
 (* ================================================================== *)
@@ -130,6 +132,13 @@ let rec lean_expr (scope : string list) (e : expr) : string =
   | Snd e1       -> Printf.sprintf "(.snd %s)"       (lean_expr scope e1)
   | EchoAdd (a, b) -> Printf.sprintf "(.echoAdd %s %s)" (lean_expr scope a) (lean_expr scope b)
   | EchoEq  (a, b) -> Printf.sprintf "(.echoEq %s %s)"  (lean_expr scope a) (lean_expr scope b)
+  (* Epistemic is IN the mechanised core (proofs/Tangle.lean §EPISTEMIC), so
+     these are translated, not rejected. *)
+  | Warrant (k, c, ev) ->
+    Printf.sprintf "(.warrant %d %s %s)" k (lean_expr scope c) (lean_expr scope ev)
+  | EpiVal (k, c, ev) ->
+    Printf.sprintf "(.epiVal %d %s %s)" k (lean_expr scope c) (lean_expr scope ev)
+  | Evidence e1 -> Printf.sprintf "(.evidence %s)" (lean_expr scope e1)
   (* Non-core: must never appear in the corpus (close is the boundary gateway). *)
   | FloatLit _ | BinOp ((Sub | Mul | Div | Isotopy), _, _) | UnaryOp _
   | Close _ | Mirror _ | Reverse _ | Simplify _ | Cap _ | Cup _ | Twist _
@@ -360,6 +369,17 @@ let check () =
   (* #92: widths need not agree, so this is now WELL-TYPED rather than
      rejected. It is the `identity == braid` shape the Lean step relation has
      always had rules for (eqIdBraid / eqBraidId). *)
+  (* Epistemic pins: OCaml infer_expr must agree with Lean infer on the new
+     constructors. The `evidence` pin is the important one: it must yield the
+     EVIDENCE type, never the claim type. *)
+  pin "warrant num/word"     (Warrant (0, IntLit 1, BraidLit [s 1]))
+    (TEpi (0, TWord 2, TNum));
+  pin "warrant word/str"     (Warrant (3, BraidLit [s 1], StringLit "ev"))
+    (TEpi (3, TStr, TWord 2));
+  pin "evidence yields rho"  (Evidence (Warrant (0, IntLit 1, BraidLit [s 1])))
+    (TWord 2);
+  pin "epi over echo"        (Warrant (1, IntLit 0, EchoClose (BraidLit [s 1])))
+    (TEpi (1, TEcho (TWord 2, TWord 0), TNum));
   pin "eq diff-width word"   (BinOp (Eq, BraidLit [s 1], Identity))            TBool;
 
   (* 3. Reject pins — these must raise Type_error. *)