hyperpolymath · hyperpolymath · Jul 29, 2026 · Jul 29, 2026
@@ -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` |

@@ -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) |

@@ -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

@@ -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. *)

@@ -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;

@@ -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

@@ -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 };

@@ -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. *)