chore(machine-readable): housekeeping checkpoint — refresh 6a2, add ANCHOR, fix bot_directives

Reconciles the repo's machine-readable metadata with the post-echo-types basis
(PR #34, #36) and fixes accumulated template drift found in a structural audit.

- 6a2/STATE.a2ml: was stale to 2026-02-12 ("begin lexer implementation"); now
  reflects the OCaml compiler + Lean metatheory + echo types + decidability +
  CI bootstrap, with the live milestone/next-action list.
- 6a2/META.a2ml: record ADR-1..6 (Lean spec is source of truth; de Bruijn ctx;
  echo types intrinsic; decidability via infer; toolchain bootstrap; open echo
  value-shape fork).
- 6a2/ECOSYSTEM.a2ml: real stack position + related projects; documents the
  echoClose-residue ↔ QuandleDB quandle-presentation seam.
- anchors/ANCHOR.a2ml: NEW authoritative anchor (schema hyperpolymath.anchor/1),
  established on the echo-types realignment; golden path = lean oracle.
- bot_directives/: NEW — fixes the dangling .bot_directives symlink (target
  never existed); directives for hypatia/gitbot-fleet/git-private-farm.
- contractiles/README.adoc: corrected stale refs (trust/Trustfile.hs →
  trust/Trustfile.a2ml; lust/Intentfile → intend/Intentfile.a2ml) and noted the
  dual-representation / template-generation status.

https://claude.ai/code/session_01PgHpCFzwYB7Qy9L6kmR8CE

Author: Jonathan D.A. Jewell

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -3,18 +3,29 @@
 #
 # ECOSYSTEM.a2ml — Tangle ecosystem position
 [metadata]
-version = "1.0.0"
-last-updated = "2026-04-11"
+version = "1.1.0"
+last-updated = "2026-06-05"
 
 [project]
 name = "Tangle"
 purpose = "A Turing-complete topological programming language where programs are isotopy classes of tangles"
-role = "specification"
+role = "semantic-core"
 
 [position-in-ecosystem]
-category = ""
+category = "language / verified semantic core"
+summary = """Tangle is the semantic core of a four-layer federated stack:
+KRL (surface) → TangleIR (interchange) → Tangle core (this repo; Lean metatheory
++ OCaml/Rust impl) → Skein.jl + QuandleDB (persistence/invariants). KRL and
+QuandleDB rest on Tangle's metatheory."""
 
 [related-projects]
 projects = [
-  # No related projects recorded
+  "hyperpolymath/krl — KRL surface language; lowers to TangleIR (rests on Tangle's type safety). NOTE: repo currently half-instantiated from rsr-template (see checkpoint 2026-06-05).",
+  "hyperpolymath/quandledb — consumes TangleIR via quandle_presentation(ir)::QuandlePresentation. SEAM: echoClose's residue is the pre-closure braid, exactly the data QuandleDB extracts the quandle from.",
+  "hyperpolymath/Skein.jl — knot-theoretic database (Julia); persistence/invariants layer. No Julia development from the Tangle side.",
+  "hyperpolymath/echo-types — reference theory for echo types (Echo f y := Σ(x:A), f x ≡ y). Tangle ships a simply-typed shadow as a type-system feature (TG-10).",
 ]
+
+[downstream-contract]
+conservative-extension = "Echo-type additions to Ty/Expr/HasType are conservative; prior theorems unchanged. Flag any change that surfaces in TangleIR."
+coordinate-with = ["quandledb session — echo residue → TangleIR threading"]

.machine_readable/6a2/META.a2ml

@@ -3,22 +3,29 @@
 #
 # META.a2ml — Tangle meta-level information
 [metadata]
-version = "1.0.0"
-last-updated = "2026-04-11"
+version = "1.1.0"
+last-updated = "2026-06-05"
 
 [project-info]
 license = "MPL-2.0"
 author = "Jonathan D.A. Jewell (hyperpolymath)"
 
 [architecture-decisions]
 decisions = [
-  # No ADRs recorded
+  "ADR-1: The Lean 4 inductives (HasType, Step) in proofs/Tangle.lean ARE the formal spec; the OCaml compiler refines them (TG-3). Metatheory is the source of truth.",
+  "ADR-2: Typing context is de Bruijn (Ctx = List Ty), so the core is ready for binders (let, TG-1) without renaming machinery.",
+  "ADR-3: Echo types are intrinsic to the type system, not a bolt-on. `close : Word[n]→Word[0]` is the canonical lossy map; Ty.echo ρ τ is the simply-typed shadow of echo-types' Echo f y := Σ(x:A), f x ≡ y (hyperpolymath/echo-types). echoClose=echo-intro, lower=collapse, residue=witness. All four safety theorems cover it.",
+  "ADR-4: Decidability is proved by an algorithmic `infer : Ctx → Expr → Option Ty` shown equivalent to HasType (infer_sound/infer_complete); yields type uniqueness + a Decidable instance (TG-2).",
+  "ADR-5: Lean toolchain setup is a single source of truth (proofs/bootstrap-lean.sh): normal elan path on open networks, GitHub-asset fallback when release.lean-lang.org is off-allowlist (sandboxed/web). CI and the SessionStart hook both call it.",
+  "ADR-6 (OPEN): echo value shape — uniform `echoVal (residue,result)` (faithful to Echo=Σ; reworks merged single-step capstones to Step*) vs per-operation lower/residue computation rules. Decision pending; gates the add/eq generalisation.",
 ]
 
 [development-practices]
 versioning = "SemVer"
 documentation = "AsciiDoc"
 build-tool = "just"
+proof-assistant = "Lean 4 (pinned leanprover/lean4:v4.14.0)"
+proof-discipline = "no sorry/axiom/admit (CI-enforced); every edit ends with a Lean compile"
 
 [maintenance-axes]
 scoping-first = true

.machine_readable/6a2/STATE.a2ml

@@ -4,40 +4,53 @@
 # STATE.a2ml — Tangle project state
 [metadata]
 project = "tangle"
-version = "0.1.0"
-last-updated = "2026-02-12"
+version = "0.2.0-dev"
+last-updated = "2026-06-05"
 status = "active"
-session = "converted from scheme — 2026-04-11"
+session = "echo-types realignment + decidability + CI bootstrap — 2026-06-05"
 
 [project-context]
 name = "Tangle"
-purpose = """A Turing-complete topological programming language"""
-completion-percentage = 35
+purpose = """A Turing-complete topological programming language whose core type
+system is mechanised in Lean 4. `close` (braid closure) is the canonical lossy
+map; echo types make that loss recoverable at the type level."""
+completion-percentage = 55
 
 [position]
-phase = "specification-complete"   # design | implementation | testing | maintenance | archived
-maturity = "experimental"  # experimental | alpha | beta | production | lts
+phase = "implementation"            # design | implementation | testing | maintenance | archived
+maturity = "alpha"                  # experimental | alpha | beta | production | lts
 
 [route-to-mvp]
 milestones = [
-  # No milestones recorded
+  "DONE: OCaml compiler — lexer, parser, typecheck, eval, pretty, compositional (compiler/lib/*.ml)",
+  "DONE: Rust tangle-wasm backend + tangle-lsp",
+  "DONE (TG-0): proofs/Tangle.lean compiles clean; CI build oracle wired (lean-proofs.yml)",
+  "DONE: Type safety (Progress/Preservation/Determinism/TypeSafety) for the let-free core",
+  "DONE (TG-10): echo types integrated into the type system (Ty.echo, echoClose/lower/residue); all four theorems extended; residue-recovery + non-injectivity capstones",
+  "DONE (TG-2): decidability — infer ≡ HasType, type uniqueness, Decidable instance",
+  "DONE: reproducible Lean toolchain bootstrap (proofs/bootstrap-lean.sh) + SessionStart hook; CI consolidated onto it",
+  "NEXT (TG-1): extend type safety to let-binding (full de Bruijn substitution)",
+  "NEXT: generalise echo to add/eq (needs a product/residue type in Ty)",
+  "NEXT: thread echo residue into TangleIR (coordinate with quandledb)",
+  "NEXT: full OCaml echo pipeline (ast/typecheck/eval/parser/pretty)",
+  "LATER (TG-3): OCaml typecheck.ml refines the Lean HasType spec",
+  "LATER (TG-5/6/7): compositional rewriter preservation; WASM semantic preservation; braid-group eqBraids",
 ]
 
 [blockers-and-issues]
 issues = [
-  # No blockers recorded
+  "DESIGN (open, user): echo value shape — uniform `echoVal (residue,result)` (faithful to Echo=Σ, reworks merged capstones to multi-step Step*) vs per-operation lower/residue rules. Blocks the echo generalisation to add/eq.",
 ]
 
 [critical-next-actions]
 actions = [
-  "Begin lexer implementation (Task 1 in SONNET-TASKS.md)",
-  "Set up Rust project structure with cargo",
-  "Complete lexer with mode switching",
-  "Begin TANGLE parser (recursive descent)",
-  "Complete parser + type checker",
-  "Begin evaluator",
+  "Resolve the echo value-shape design fork (A vs B), then add the product type",
+  "TG-1: let-binding type safety via de Bruijn substitution",
+  "Generalise echo to add/eq; thread residue into TangleIR with the quandledb session",
+  "Extend the OCaml typechecker (typecheck.ml/ast.ml) with echo types",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-02-12T00:00:00Z"
-last-result = "unknown"  # unknown | pass | warn | fail
+last-run-utc = "2026-06-05T00:00:00Z"
+last-result = "pass"               # unknown | pass | warn | fail
+notes = "lean-proofs oracle GREEN (PR #34, #36 merged); Tangle.lean 0 errors, no sorry/axiom/admit"

.machine_readable/anchors/ANCHOR.a2ml

@@ -0,0 +1,76 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# ANCHOR.a2ml - authoritative anchor for this repository
+#
+# Established 2026-06-05 on the echo-types realignment: echo types became an
+# intrinsic feature of the Tangle type system (not external reference), the
+# safety metatheory was extended to cover them, and type checking was proved
+# decidable. This anchor records the post-realignment canonical baseline.
+
+[metadata]
+version = "1.0.0"
+last-updated = "2026-06-05"
+
+[anchor]
+schema = "hyperpolymath.anchor/1"
+repo = "hyperpolymath/tangle"
+authority = "upstream-canonical"
+
+purpose = [
+  "Define the canonical type-system semantics for the Tangle stack.",
+  "Declare what downstream repos (KRL, QuandleDB) may extend but not redefine.",
+  "Provide a stable golden path and invariant contract for proof/release readiness.",
+]
+
+[identity]
+project = "Tangle"
+kind = "language"
+one-sentence = "Tangle — a Turing-complete topological (braid/tangle) programming language whose core type system is mechanised in Lean 4."
+domain = "knot-theory / topological computing"
+
+[semantic-authority]
+policy = "canonical"
+
+owns = [
+  "Core type system: HasType (typing) and Step (small-step) inductives.",
+  "Type-safety metatheory: Progress, Preservation, Determinism, Type Safety.",
+  "Echo-types semantics: Ty.echo, echoClose/lower/residue (structured loss over `close`).",
+  "Decidability of type checking: infer ≡ HasType.",
+  "TangleIR semantics consumed by KRL (lowering) and QuandleDB (quandle extraction).",
+]
+
+[realignment-log]
+events = [
+  "2026-06-05 R1: echo types integrated into the type system (TG-10); all four safety theorems extended; echo-types audit verdict changed from NOT-RELEVANT to integrated feature.",
+  "2026-06-05 R2: decidability landed (TG-2) — infer/HasType equivalence, type uniqueness, Decidable instance.",
+]
+
+[implementation-policy]
+allowed = ["Lean4", "OCaml", "Rust", "Scheme", "Shell", "Just", "AsciiDoc", "Markdown", "Nickel"]
+forbidden = ["TypeScript", "Node.js", "npm", "Go", "Python", "Java", "Kotlin", "Swift"]
+
+[golden-path]
+smoke-test-command = [
+  "cd proofs && lean Tangle.lean",
+  "just test",
+]
+
+success-criteria = [
+  "proofs/Tangle.lean reports 0 errors under the pinned toolchain",
+  "No sorry/axiom/admit/Admitted outside comments (CI-enforced)",
+  "Core tests pass; quality gates pass",
+]
+
+[satellite-policy]
+must-pin-upstream = true
+must-declare-authority = true
+must-have-anchor = true
+must-have-golden-path = true
+
+[semantic-authority-files]
+formal-proofs = "proofs/Tangle.lean"
+language-spec = "docs/spec/FORMAL-SEMANTICS.md"
+proof-narrative = "PROOF-NARRATIVE.md"
+proof-needs = "PROOF-NEEDS.md"
+build-proofs = "proofs/README.md"

.machine_readable/bot_directives/README.adoc

@@ -0,0 +1,23 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+= Bot directives — Tangle
+
+Machine-readable directives for the hyperpolymath bot fleet operating on this
+repository (Hypatia governance/scan, gitbot-fleet, and the `.git-private-farm`
+automation). The repo-root `.bot_directives` symlink points here.
+
+Until 2026-06-05 the `.bot_directives` symlink dangled (target did not exist);
+it was created during the echo-types realignment housekeeping checkpoint.
+
+== Files
+
+* `tangle.directives.a2ml` — the active directive set for bots on this repo:
+  development branch, proof discipline, toolchain bootstrap, and cross-repo
+  coordination notes.
+
+== Authority
+
+These directives are subordinate to `.machine_readable/anchors/ANCHOR.a2ml`
+(canonical semantics) and the contractiles (`MUST` / `TRUST` / `INTENT` /
+`ADJUST`). Where a directive conflicts with the anchor or a contractile, the
+anchor/contractile wins and the directive must be corrected.

.machine_readable/bot_directives/tangle.directives.a2ml

@@ -0,0 +1,40 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# tangle.directives.a2ml — directives for the bot fleet on hyperpolymath/tangle
+[metadata]
+version = "1.0.0"
+last-updated = "2026-06-05"
+applies-to = ["hypatia", "gitbot-fleet", "git-private-farm"]
+
+[development]
+# Where bots should develop. Never push to main directly.
+dev-branch = "claude/<session>"
+default-base = "main"
+pr-policy = "open as draft; CI must be green before ready-for-review"
+
+[proof-discipline]
+# Tangle owns a real metatheory — these are hard gates.
+prover = "Lean 4"
+toolchain-pin = "proofs/lean-toolchain (leanprover/lean4:v4.14.0)"
+banned-tokens = ["sorry", "axiom", "admit", "Admitted"]   # CI-enforced, outside comments
+rule = "every edit to proofs/ ends with: cd proofs && lean Tangle.lean (expect 0 errors)"
+oracle-workflow = ".github/workflows/lean-proofs.yml"
+
+[toolchain-bootstrap]
+# Sandboxed/web environments cannot reach release.lean-lang.org.
+script = "proofs/bootstrap-lean.sh"        # normal elan path + GitHub-asset fallback
+session-hook = ".claude/hooks/session-start.sh"   # auto-bootstraps web sessions
+note = "Do NOT hand-roll elan installs; call the bootstrap script (single source of truth)."
+
+[cross-repo-coordination]
+# Tangle is the semantic core; KRL and QuandleDB rest on its metatheory.
+downstream = ["hyperpolymath/krl", "hyperpolymath/quandledb"]
+tangle-ir = "Changes to Ty/Expr/HasType are conservative extensions; flag any that reach TangleIR (QuandleDB consumes it)."
+quandle-seam = "echoClose's residue is the pre-closure braid — exactly what QuandleDB extracts a quandle presentation from. Coordinate echo→IR threading with the quandledb session."
+echo-types = "hyperpolymath/echo-types is the reference theory (Echo f y := Σ(x:A), f x ≡ y); Tangle ships a simply-typed shadow as a type-system feature."
+
+[no-go]
+# Do not develop these here.
+julia = "No Julia development in this repo (Skein.jl/QuandleDB own the Julia layer)."
+languages = "No TypeScript/Node/npm/Go/Python/Kotlin/Swift (see ANCHOR implementation-policy)."

contractiles/README.adoc

@@ -1,19 +1,36 @@
-= Contractiles Template Set
+// SPDX-License-Identifier: MPL-2.0
+= Tangle Contractiles
 :toc:
 :sectnums:
 
-This directory contains the generalized contractiles templates. Copy the `contractiles/` directory into a new repo to establish a consistent operational, validation, trust, recovery, and intent framework.
+The contractiles for this repository: a consistent operational, validation,
+trust, recovery, and intent framework. (Originally scaffolded from the RSR
+template; the file references below are corrected to the files actually
+shipped here.)
 
-== Fill-In Instructions
+== Contents
 
-1. Update the Mustfile to reflect your real invariants (paths, schema versions, ports).
-2. Replace Trustfile.hs placeholders with your actual key paths and verification commands.
-3. Adjust Dustfile handlers to match your rollback and recovery tooling.
-4. Update Intentfile to mirror the roadmap you want the system to evolve toward.
+* `must/Mustfile` — required invariants and validations.
+* `trust/Trustfile.a2ml` — trust / verification steps.
+* `dust/Dustfile` — rollback and recovery semantics.
+* `intend/Intentfile.a2ml` — future intent and roadmap direction.
 
-== Contents
+NOTE: This repo also carries the S-expression companion set under
+`.machine_readable/` (`MUST.contractile`, `TRUST.contractile`,
+`INTENT.contractile`, `ADJUST.contractile`). The two representations coexist
+because tangle was scaffolded at an intermediate RSR-template generation; the
+canonical layout is being reconciled estate-wide (the template master, krl,
+has since relocated `contractiles/` *into* `.machine_readable/` and added
+`adjust/` + `bust/`). Until that reconciliation lands, treat
+`.machine_readable/*.contractile` as authoritative and the `contractiles/<name>/`
+tree as the human-readable mirror.
+
+== Maintenance
+
+Keep these in step with reality:
 
-* `must/Mustfile` - required invariants and validations.
-* `trust/Trustfile.hs` - cryptographic verification steps.
-* `dust/Dustfile` - rollback and recovery semantics.
-* `lust/Intentfile` - future intent and roadmap direction.
+1. `must/Mustfile` — real invariants (proof discipline, paths, schema versions).
+2. `trust/Trustfile.a2ml` — actual key paths and verification commands.
+3. `dust/Dustfile` — rollback and recovery tooling.
+4. `intend/Intentfile.a2ml` — the roadmap (see `.machine_readable/6a2/STATE.a2ml`
+   `route-to-mvp` for the live milestone list).