This file is the single coherent story of what Tangle proves, what it assumes, and what it has left to prove.
For the per-obligation checklist with status/prover/effort, see PROOF-NEEDS.md. For the registry of every load-bearing unproven assumption, see ASSUMPTIONS.md.
Tangle is the semantic core of a four-layer federated stack:
┌─────────────────────────────────────────────────────────┐
│ KRL surface language (hyperpolymath/krl) │
└─────────────────┬───────────────────────────────────────┘
│ lowers via KR-1, KR-2 to
▼
┌─────────────────────────────────────────────────────────┐
│ TangleIR (canonical interchange obj) │
└─────────────────┬───────────────────────────────────────┘
│ has semantics via
▼
┌─────────────────────────────────────────────────────────┐
│ Tangle CORE (THIS REPO) │
│ proofs/Tangle.lean — mechanised results (26 HasType, 55 Step) │
│ compiler/lib/*.ml — OCaml implementation │
│ compiler/tangle-wasm — WASM backend │
│ compiler/tangle-lsp — LSP server │
│ dialects/ — braid-calculus, quantum-circuit, etc. │
└─────────────────┬───────────────────────────────────────┘
│ persisted/queried via
▼
┌─────────────────────────────────────────────────────────┐
│ Skein.jl + QuandleDB │
└─────────────────────────────────────────────────────────┘
Consequence: Tangle owes a real metatheory. It owns the type system that everyone above and below depends on. Tangle.lean already delivers a substantial slice of this; this document makes the delivered slice and the remaining gap explicit.
All results live in proofs/Tangle.lean
(Lean 4, no sorry, no axiom).
Build oracle. As of 2026-06-01 (PR closing TG-0,
#32), the file is verified at every push/PR by
.github/workflows/lean-proofs.yml, pinned to
proofs/lean-toolchain = leanprover/lean4:v4.14.0. Empirical result
on the original 2026-03-30 commit: 121 errors on every Lean 4 version
4.9–4.16 — the file had never compiled. The current commit returns 0
errors, verified locally on v4.10/4.11/4.12/4.13/4.14/4.15/4.16, with
CI gating both lean Tangle.lean and a sorry/axiom/admit
slippage check. Future drift will fail CI rather than land silently.
Echo-types — now integrated as a type-system feature (2026-06-03). The
earlier audit
(feedback_echo_types_audit_krl_tangle_quandledb_not_relevant.md)
correctly found that the external echo-types Agda library
(hyperpolymath/echo-types) carries no lambda-calculus / progress /
preservation content of its own, so it does not perturb the four base
theorems. That verdict stands for the external library. Tangle now
ships its own simply-typed shadow of echo-types as a first-class feature
of the type system (Ty.echo ρ τ, constructors
echoClose/lower/ residue, rules
T-Echo-Close/T-Lower/T-Residue). The motivation is intrinsic
to Tangle: close : Word[n] → Word[0] is the canonical lossy map (the
analogue of echo-types’ collapse : Bool → ⊤), and the echo layer
makes that loss recoverable at the type level — the residue Word[n]
is retained and projected back out. Progress, Preservation, Determinism,
and Type Safety in proofs/Tangle.lean now cover the echo fragment,
and three capstone theorems (echo_lower_collapses,
echo_residue_recovers, echo_distinguishes_collapsed) reproduce
echo-types’ no-section / sigma-distinguishes barrier inside
Tangle. See PROOF-NARRATIVE §2.5.
| ID | Statement | Where |
|---|---|---|
T-Progress |
Every well-typed closed term is either a value or can take a step. |
|
T-Preservation |
Stepping preserves types:
|
|
T-Determinism |
The step relation is deterministic:
|
|
T-TypeSafety |
Well-typed closed terms never get stuck (Progress |
|
Each is proven for the full core fragment: numerals, strings, booleans, identity, braid literals, composition, tensor, pipeline, close, addition, equality, variables, let-binding, the complete echo/product fragment (see §2.5), and decidable type inference (see §2.7). The “let-free fragment” caveat is retired — TG-1 and TG-2 are both landed.
| ID | Statement | Where |
|---|---|---|
T-ValueNoStep |
Values are normal forms: |
|
T-CanonicalNum |
A typed-Num value is |
|
T-CanonicalStr |
A typed-Str value is |
|
T-CanonicalWord |
A typed-Word[n] value is |
|
T-CanonicalEcho |
A typed-Echo value is |
|
T-CanonicalProd |
A typed-Prod value is |
|
T-WidthAppend |
|
|
T-WidthShift |
|
|
T-Weakening |
Inserting a fresh hypothesis at de Bruijn position
|
|
T-SubstPreserves |
Typing is preserved under capture-avoiding substitution of a typed term for a variable (TG-1). |
|
Tangle.lean also defines, as inductive types (so they are themselves
proofs of the form “these are the rules”):
-
Expr— the AST (mirrorscompiler/lib/ast.ml) -
Ty—num,str,bool,word n -
IsValue— value predicate -
HasType— typing judgment, 26 rules: 13 base (tNum,tStr,tBool,tIdentity,tBraid,tComposeWord,tTensorWord,tPipeline,tCloseWord,tAddNum,tEqWord,tEqNum,tEqStr); 4 echo-close (tEchoClose,tLower,tResidue,tEchoVal); 7 product+echo-binary (tPair,tFst,tSnd,tEchoAdd,tEchoEqWord,tEchoEqNum,tEchoEqStr); 2 let/var (tVar,tLet) -
Step— small-step semantics, 55 rules: 27 base, 9 echo-close/lower/residue, 6 product, 11 echoAdd/echoEq, 2 let (plus a separate 2-constructorStepStarreflexive-transitive closure:refl,head)
These are the formal spec the OCaml implementation is meant to refine (see TG-3 below).
Echo types are integrated into the core type system (not a separate
layer). The design mirrors echo-types’ fibre definition
Echo f y := Σ (x : A), f x ≡ y (hyperpolymath/echo-types,
Echo.agda) in Tangle’s simply-typed setting, motivated by Tangle’s
own canonical lossy operation.
Why close. close : Word[n] → Word[0] collapses every braid
word to the identity, discarding the word — exactly the kind of
information-destroying map echo-types is about
(cf. collapse : Bool → ⊤ in EchoResidue.agda). Echo types make
that loss recoverable in the type system.
| Construct | Form | Echo-types analogue |
|---|---|---|
Type former |
|
|
|
|
|
|
|
the
collapse / |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Metatheory. Progress, Preservation, Determinism, and Type Safety all
cover echoClose/lower/residue (the inductions are exhaustive
over the extended Step/HasType). A new canonical-forms lemma
canonical_echo characterises echo values; value_no_step became
structurally recursive because a formed echo echoClose v is a value
iff its residue v is.
Capstone theorems (the echo-types content, Tangle.lean
§ECHO-TYPES): - echo_lower_collapses — every closed braid lowers to
identity (the lossy step, re-derived through the echo). -
echo_residue_recovers —
residue (echoClose (braidLit gs)) ⟶ braidLit gs (the witness is
retained; close becomes reversible). -
echo_distinguishes_collapsed — distinct braids collapse to the
same identity under lower, yet their residues stay distinct. This
is the Tangle instantiation of echo-types’ non-injectivity barrier
(collapse-residue-same + no-section-collapse-to-residue). -
echo_roundtrip_typed — the round-trip is well-typed: residue
returns a Word[n], lower returns a Word[0].
Tracked as obligation TG-10 in PROOF-NEEDS.md (landed).
As of 2026-06-14 (PRs #45–#46), the OCaml pipeline (compiler/lib/)
covers the complete echo + product fragment described in §2.5:
| Layer | Echo/product coverage |
|---|---|
|
|
|
8 |
|
|
|
Keyword tokens + grammar productions for all 8 surface forms |
|
Pretty-printers for all 8 forms |
|
TG-4 round-trip property test: 26-entry corpus including all 8 echo/product constructors |
Build oracle: dune build + dune test green (run
dune runtest for the live count — ~597 across 8 suites). The pre-PR
#46 main did not compile due to two Warning 8 exhaustiveness
gaps (both fixed: strand_type_of_ty in typecheck.ml; debug token
printer in bin/main.ml).
TG-3 landed (translation validation): the OCaml typechecker is proven
to refine HasType on the core fragment —
proofs/TG3Differential.lean emits 496 obligations generated from
infer_expr that Lean’s proven infer kernel-checks, plus a
closure proof and 1008 OCaml --check assertions. The two documented
divergences are close (D1) and bool == bool (D2). See
proofs/TG3-REFINEMENT.md and §TG-3 below.
Both obligations landed in proofs/Tangle.lean and are documented in
§TG-1 and §TG-2 of the remaining-obligations section below (those
sections now carry LANDED verdicts). Key structural points:
-
TG-1 (let-binding):
weakening+subst_preservesuse the de Bruijn combined-context invariant —subst_preservestypes the substitutee inΓ₁ + Γ₂`, not merely `+Γ₂. This is the genuine inductive invariant; theletRedconsumer usesΓ₁ := []where both forms coincide. -
TG-2 (decidability):
inferis a single structural recursion covering all 26HasTyperules. Both soundness and completeness are proven;type_uniquefollows as a corollary. ThedecidableHasTypeinstance makesHasType [] e τa decidable proposition directly usable by Lean’s typeclass system.
hyperpolymath/echo-types (commit f7a965f, 2026-06-14) added an
experimental ℕ∪\{∞} min-plus grade semiring
(experimental/echo-additive/Grade.agda) and a variance gate
(VarianceGate.agda). Key findings and their implications for Tangle:
-
The combining direction (
D_r(D_s A) → D_{r+s} A) has monadic variance. Tangle’sechoAdd/echoEquse exactly this direction: two residues are merged into apair(the lax monoidal μ map). The current implementation is correct for this reading. -
The splitting direction (
D_{r+s} A → D_r(D_s A)) has comonadic variance and requires a full graded adjunction F_r ⊣ U_r. If Tangle ever needs to split anEcho(ρ×σ)value back into independentEcho(ρ)andEcho(σ), that is a non-trivial structural addition — it cannot be derived from the combining map alone. -
The grade semiring (
fin n= information count,inf= total collapse) is a candidate carrier for a future grade-indexed type formerEcho[n] ρ τin Tangle.echoAddwould then have typeNum → Num → Echo[2] (Num×Num) Num(2 units of information retained). This is prospective; the experimental subtree is firewalled until the comparative protocol (monadic vs comonadic) concludes. -
No Tangle design change is required now. The current
Ty.echo/Ty.prodfragment is faithful to the monadic/combining direction and the experimental work is explicitly gated (experimental/echo-additive/is not imported by any shipped module in echo-types or Tangle).
What’s not yet proven, why it matters, and what assumption each rests on.
Status: LANDED (proofs/Tangle.lean §METATHEORY, lines 492–668).
Claim. Type safety (Progress, Preservation, Determinism, TypeSafety)
extends to the full core language including var and let.
What was proven. - weakening (line 521) — inserting a fresh
hypothesis σ at de Bruijn position Γ₁.length preserves typing,
with the term shifted by shift 1 Γ₁.length. - subst_preserves
(line 589) — typing is closed under replacing the variable at
Γ₁.length by a well-typed term s. The substitutee is typed in
the combined context Γ₁ + Γ₂` (the genuine inductive invariant; the
`+letRed consumer instantiates Γ₁ := []). - All four main theorems
(Progress, Preservation, Determinism, TypeSafety) were extended with
var and letStep/letRed cases. Step gained letStep
and letRed; HasType gained tVar and tLet.
Implementation notes. - Variable lookup uses List.getElem? (not
the deprecated List.get?); the append splits go through
List.getElem?_append_left / _append_right. - Each derivation is
taken apart with cases h; rename_i rather than
cases h with | tCtor, because under induction e the binder
arguments unify with the context and positional arm naming doesn’t
align. - The subst_preserves combined-context invariant closes the
var = Γ₁.length case by exact hs with no separate
shift-composition lemma needed.
Status: LANDED (proofs/Tangle.lean §TG-2, lines 1399–1604).
Claim. There is a total function infer : Expr → Option Ty such
that infer e = some τ ↔ HasType [] e τ.
What was proven. - infer (line 1410) — total structural recursion
on Expr; covers all 26 HasType rules including the echo/product
fragment and let-binding. - infer_complete (line 1487) —
HasType Γ e τ → infer Γ e = some τ. - infer_sound (line 1493) —
infer Γ e = some τ → HasType Γ e τ. - infer_iff_hasType (line
1588) — the biconditional packaging both directions. - type_unique
(line 1593) — HasType Γ e τ₁ → HasType Γ e τ₂ → τ₁ = τ₂ (follows
from infer_complete + infer_sound). - decidableHasType (line
1601) — Decidable (HasType [] e τ) instance via infer.
Status: LANDED (2026-06-14, translation-validation level). Full
write-up: proofs/TG3-REFINEMENT.md.
Claim. For every core-fragment e accepted by
compiler/lib/typecheck.ml with type τ, the Lean-level
proposition HasType [] e (T τ) holds (and conversely on rejection),
where T is the type translation
TNum↦num … TWord n↦word n, TEcho↦echo, TProd↦prod.
Why valuable. Bridges the metatheory (Lean) to the implementation (OCaml) — the two systems are now checked to be the same on the modelled fragment.
How it was discharged. 1. Reduction (via TG-2).
infer_iff_hasType gives infer ≡ HasType, so the claim becomes
“OCaml infer_expr ≡ Lean infer on the core fragment”. 2.
Closure proof. infer_expr keeps core terms inside the translatable
types (never TTangle), under a strengthened entire-type-tree IH.
close is the sole core gateway out of T’s domain and is
excluded. 3. Machine-checked half. proofs/TG3Differential.lean —
496 obligations infer [] e = T(infer_expr e) := by decide, generated
from the OCaml checker by compiler/test/tg3/tg3_emit.ml, verified by
proofs/check-tg3-differential.sh. 4. OCaml half.
compiler/test/tg3 --check: 1008 dune runtest assertions
(closure invariant, curated pins, named→de Bruijn translation,
divergences).
Divergences (complete). D1 close (Tangle[I,I] vs word 0)
family D1b/c/d through pipeline/compose/add; D2 bool == bool (OCaml
accepts, Lean rejects). Both sides pinned.
Assumptions / boundary. - The core OCaml AST/ty is in
bijection with the Lean AST/Ty under T (TTangle has no image
— handled by the closure proof). - Not claimed: a universal Lean theorem
over all OCaml runs (route 2 below); extra-core features are excluded,
not modelled; refinement is OCaml→Lean only. - Future route 2 (airtight
refinement): mechanise the OCaml algorithm in Lean and prove
equivalence to HasType — out of scope here (see §7 of
TG3-REFINEMENT.md).
Status: LANDED (PR #46). compiler/test/test_roundtrip.ml is a
26-entry corpus including all 8 echo/product constructors (52 round-trip
runs); the full suite is green (run dune runtest for the live
total).
Claim. parse(pretty e) = e for every closed value e.
Why valuable. Free fuzz oracle. Also the foundation of any “IR
viewer” tooling that re-parses what pretty emitted.
Assumptions. - pretty.ml’s bracketing is unambiguous
w.r.t. the grammar. - Lexer never strips information needed
by the parser (e.g. whitespace within braid literals).
How to discharge. Property test in compiler/test/ — discharged.
Claim. Every rewrite in compiler/lib/compositional.ml (418 LoC)
preserves typing: Γ ⊢ e : τ ∧ e ↝ e' ⟹ Γ ⊢ e' : τ.
Why valuable. That file has zero test coverage (see [B6] in the bug audit) and is a high-blast-radius refactor target. Type preservation is the cheapest soundness contract.
Assumptions. - Each rewrite is a function from Expr
to Expr — no in-place mutation. - No rewrite introduces
a new free variable.
How to discharge. First, add a test file
(compiler/test/compositional_test.ml) covering each rewrite. Then
add Lean-level rewrite-preservation lemmas, one per rewrite, in a new
file proofs/Compositional.lean parameterised on Tangle.lean’s
HasType.
Claim. For every closed well-typed e, the source-level evaluation
of e and the WASM execution of compile_to_wasm(e) agree on the
observable result.
Why valuable. The compiler correctness theorem. Warranted because Tangle claims structural reasoning means something on the runtime. Without this, Tangle’s wasm backend is “trust us, the structure survives.”
Assumptions. - Standard WASM semantics (assumed; specified by Wasm Cert / Wasm spec). - No floating-point non-determinism in the source semantics (Tangle has only Int currently).
How to discharge. Bisimulation between OCaml eval and the WASM
small-step. Heavy — this is the high-value research-paper-grade slice
(see typed-wasm proof debt in the estate).
Claim. Step.eqBraids should decide braid-group equivalence, not
list equivalence. I.e., σ_i σ_j σ_i = σ_j σ_i σ_j when |i-j|=1 and
σ_i σ_j = σ_j σ_i when |i-j|≥2 should be decidable in finite
generators.
Why valuable. The README claims “program equivalence is defined by
isotopy.” Currently eqBraids only checks list equality, so
σ_1 σ_2 σ_1 and σ_2 σ_1 σ_2 are reported unequal. That’s the
trivial reading.
Status — LANDED 2026-07-29 (owner ruling #50), with a stated trusted
base. == on braids now decides braid-group equivalence in both
engines:
-
OCaml —
eval.mlEq(andIsotopy, which for braids denotes the same relation) route throughcompiler/lib/braid_equiv.ml(Dehornoy handle reduction).IdentityisVBraid [], so identity comparisons flow through the same case. -
Lean —
Step.eqBraids/eqIdBraid/eqBraidId, and the threeechoEqcounterparts, usebraidEquiv/isTrivialBraid: a faithful in-Lean port of the same procedure, in §BRAID-GROUP EQUIVALENCE ofTangle.lean.
σ₁σ₂σ₁ == σ₂σ₁σ₂ is now true, which is what the README’s
“equivalence is defined by isotopy” always claimed. Progress /
Preservation / Determinism were re-verified unchanged — all three need
only that the right-hand side is a total function into Bool`, which
`braidEquiv is; Determinism in particular is immediate, since a
function applied to fixed arguments yields a fixed result.
==== ⚠ TRUSTED, NOT PROVEN — the honest boundary
braidEquivis a definition, not an axiom: nothing is postulated, and the sorry/axiom gate passes legitimately. But the gate passing does NOT mean this claim is proven. What is established is that the metatheory holds relative tobraidEquiv. What is not established is thatbraidEquivcorrectly decides braid-group equality — that is the mechanised Garside/Dehornoy correctness proof, which remains research-grade and out of scope (#51).Correctness is currently evidenced by testing only:
compiler/test/tg7(2220 assertions — defining relations, 400 constructed-equivalent pairs, invariant-distinguished negatives) plus 8 semantics-distinguishing cases intest_eval.ml. Testing is not proof.Termination in the Lean port is by an explicit fuel bound mirroring the OCaml
max_steps, not by a well-founded measure. Dehornoy reduction does terminate, but proving that is the research obligation above; fuel keeps the definitions total without smuggling in an unproven termination claim.
Assumptions. - Word problem in the braid group is
solvable in polynomial time on finitely many strands (Birman–Ko–Lee /
Garside-normal-form algorithm — known true). -
braidEquiv (Lean) and braid_equiv.ml (OCaml) implement Dehornoy
handle reduction correctly, and agree with each other. Evidenced by
testing, not proof. This is the load-bearing unproven assumption of
TG-7.
Claim. Each dialect under dialects/ (braid-calculus,
quantum-circuit, skein-algebra, string-diagram,
virtual-knot) is a conservative extension of core Tangle: any core
program embedded into the dialect typechecks iff it typechecked in core.
Why valuable. Lets dialect work proceed without re-proving safety each time. Also stops dialect-introduced ambiguities from quietly weakening core soundness.
Assumptions. - Each dialect’s grammar is a strict superset of core’s EBNF. - Each dialect’s typing rules are additive — they only add new constructors and their typing rules, never modify existing ones.
How to discharge. Per dialect: define HasType_dialect in Lean as
HasType plus new rules; prove embedding preservation.
Claim. Every diagnostic emitted by tangle-lsp corresponds to a
failure of the HasType judgment in Tangle.lean. (No LSP-only
diagnostics that the spec doesn’t reject.)
Why valuable. Stops IDE drift from the language definition. Without it, users get red squigglies in the editor for things that compile, or vice versa.
How discharged (by construction, not by proof). The audit found the
LSP was emitting several LSP-only false positives from a hand-rolled
lexical scan: it skipped -- comments (Tangle uses # /
(* *)), counted delimiters inside string literals, incremented
block-depth on every def (firing “unclosed block” on every
multi-def file), and flagged function parameters as “possibly
undefined”. None of these corresponded to a HasType failure.
The refactor removes all hand-rolled diagnostics and routes the LSP
through the real compiler: - compiler/lib/check.ml
(check_source) is the single diagnostic source — parse-with-recovery
+ Typecheck.check_program. - tanglec --check exposes it as
SEVERITY⇥LINE⇥COL⇥MESSAGE. - tangle-lsp shells out to
tanglec --check and forwards exactly those diagnostics
(run_compiler_diagnostics); the lexical scan now only extracts
definitions/references for navigation. If the binary is absent it emits
nothing — ∅ ⊆ HasType failures, never a false positive.
So the subset relation holds by construction: the LSP cannot author a diagnostic the compiler would not produce.
Evidence. compiler/test/test_check.ml (the diagnostic source is
exactly parse + type failures) and tangle-lsp’s unit tests
(parse_check_line, analyze authors no diagnostics, and a gated
end-to-end delegation test against a real tanglec).
Locations. Type errors scoped to a definition now carry that def’s
source line (def_line, threaded from the parser through
check_program), and the former duplicate diagnostic (pass 1b + pass
2 both reporting a def error) is removed. Statement-level errors
(assertions / computations / weave blocks) are not yet located and still
surface at the file top; column spans for expressions remain future
work. None of this affects the subset property — only where a diagnostic
points.
For completeness, we explicitly do not pursue:
-
"``Expr` has exactly these constructors`" — enforced by the inductive definition.
-
"`Compose is left-associative`" — surface syntax decision, not a semantic claim.
-
"``compile_to_wasm` returns a Vec`" — Rust type assertion.
-
"
generatorWidth (g :: gs) ≥ g.idx + 1" — implied by T-WidthAppend-
cons semantics, no extra proof gains anything.
-
-
Add a row to PROOF-NEEDS.md with
TG-Nid, category, prover, priority, effort. -
Add the narrative entry here with statement, why valuable, status, assumptions, how to discharge. Assumptions block is non-optional.
-
Each new assumption gets an entry in ASSUMPTIONS.md with
A-TG-N.Mid and MATH/DESIGN/EMPIRICAL/CRYPTO classification.
-
Implementation:
compiler/lib/(OCaml, 2649 LoC). -
Formal core:
proofs/Tangle.lean(Lean 4, 560 LoC, allQed). -
Decisions:
docs/spec/DECISIONS-LOCKED.md. -
Companion narratives:
-
hyperpolymath/krl/PROOF-NARRATIVE.md— surface-language obligations -
hyperpolymath/quandledb/PROOF-NARRATIVE.md— quandle / DB proofs
-