refactor: migrate Markdown to AsciiDoc

ASSUMPTIONS.adoc

@@ -0,0 +1,173 @@
+== Assumptions Registry — Tangle
+
+Every load-bearing *unproven* assumption used in this repo, with an ID,
+classification, and the obligation it supports.
+
+Classifications: - *MATH* — true by an external mathematical theorem
+(cite it) - *DESIGN* — true by construction in our code (must remain
+true; flag if you change the named code) - *EMPIRICAL* — believed from
+testing; not formally verified - *CRYPTO* — standard
+cryptographic-primitive assumption
+
+Cross-references use `+[[A-TG-N.M]]+` syntax, resolved here.
+
+'''''
+
+[width="100%",cols="11%,14%,22%,20%,33%",options="header",]
+|===
+|ID |Class |Statement |Cited by |Where it lives
+|A-TG-1.1 |DESIGN |Capture-avoiding substitution is well-defined on the
+de Bruijn representation `+HasType+` uses |TG-1 |`+Tangle.lean+` `+Ctx+`
+definition + de Bruijn discipline
+
+|A-TG-1.2 |MATH |Standard weakening + substitution lemmas hold for the
+`+HasType+` rules (POPLmark / TAPL §8) |TG-1 |TAPL Ch. 9; Pierce 2002
+
+|A-TG-2.1 |DESIGN |Type-checking proceeds by syntactic recursion on
+`+Expr+` (no impredicative steps; matches `+typecheck.ml+`’s shape)
+|TG-2 |`+compiler/lib/typecheck.ml+`
+
+|A-TG-2.2 |DESIGN |Equality on `+Ty+` is decidable (Lean:
+`+deriving DecidableEq+`; OCaml: structural `+=+`) |TG-2
+|`+Tangle.lean::Ty+`; `+compiler/lib/ast.ml+`
+
+|A-TG-3.1 |DESIGN |The OCaml AST in `+compiler/lib/ast.ml+` is in
+bijection with the Lean AST in `+Tangle.lean::Expr+` |TG-3 |Both files,
+by construction
+
+|A-TG-3.2 |DESIGN |OCaml `+String.equal+`, `+Int.equal+` coincide with
+Lean’s `+==+` on the values used at runtime |TG-3 |Standard library
+agreement; verify at the FFI boundary
+
+|A-TG-4.1 |DESIGN |`+pretty.ml+`’s bracketing is unambiguous w.r.t.
+`+parser.mly+`’s precedence |TG-4 |`+compiler/lib/pretty.ml+`,
+`+compiler/lib/parser.mly+`
+
+|A-TG-4.2 |DESIGN |Lexer never strips information needed by the parser
+(e.g. whitespace within braid literals) |TG-4
+|`+compiler/lib/lexer.mll+`
+
+|A-TG-5.1 |DESIGN |Every rewrite in `+compositional.ml+` is
+`+Expr → Expr+` (no mutation) |TG-5 |`+compiler/lib/compositional.ml+`
+
+|A-TG-5.2 |DESIGN |No rewrite introduces a new free variable |TG-5 |Each
+rewrite, individually
+
+|A-TG-6.1 |MATH |WASM small-step semantics is well-defined; assume the
+official Wasm spec / WasmCert-Isabelle definition |TG-6 |wasm-spec,
+WasmCert-Isabelle
+
+|A-TG-6.2 |DESIGN |Source semantics has no floating-point
+non-determinism (Tangle has only `+Int+` currently) |TG-6
+|`+Tangle.lean::Ty+` lacks `+.float+`
+
+|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+`
+|===
+
+'''''
+
+=== How to use this file
+
+* *Reading code.* When you see a function whose correctness depends on
+something not enforced by the local types — _that’s an assumption_. Find
+or add the entry here and reference it by ID.
+* *Writing a proof.* Every proof obligation in PROOF-NARRATIVE.md names
+its assumptions by ID. Before discharging the proof, audit the
+assumptions block.
+* *Modifying load-bearing code.* Each DESIGN assumption names a
+file/component. If you edit that file, re-validate the assumption (or
+update the obligation if the design changed intentionally).
+
+=== Promoting / demoting assumptions
+
+[cols=",,",options="header",]
+|===
+|From |To |Trigger
+|EMPIRICAL → MATH |discharge with a citation |
+|EMPIRICAL → DESIGN |refactor to make it a structural invariant |
+|MATH → (delete) |obligation has been re-cast not to need it |
+|DESIGN → MATH (rare) |the design happens to encode a known theorem |
+|===
+
+When you change a row, leave a one-line note in the changelog with the
+date and reason.
+
+'''''
+
+=== Changelog
+
+[width="100%",cols="32%,42%,26%",options="header",]
+|===
+|Date |Change |By
+|2026-06-01 |Initial registry, scoped to Tangle metatheory +
+implementation refinement obligations |Audit
+
+|2026-06-01 |A-TG-9.1 reformulated under TG-9 Option B — accept LSP-only
+categories instead of pretending refinement (full Option A queued at
+#28). See `+compiler/tangle-lsp/docs/lsp-diagnostic-categories.md+`.
+|TG-9 Option B PR
+
+|2026-06-01 |TG-0 closed: `+proofs/Tangle.lean+` previously had 121
+errors on Lean 4.9–4.16 (commit 8ce7be7 was committed without ever
+compiling). Repaired: 62/51 diff, 0 errors on Lean 4.10–4.16. CI oracle
+at `+.github/workflows/lean-proofs.yml+` pinned to v4.14.0 via
+`+proofs/lean-toolchain+`. Sorry/axiom/admit slippage check added.
+Closes hyperpolymath/tangle#32. |TG-0 PR
+|===