feat(types,docs): Echo types in type checker + comprehensive documentation pass (#55)

Add Type::Echo / Type::EchoR structured-loss formers (distinct from carrier T; ghost-erased
at runtime) to compiler/bet-core; lower + structurally unify them in compiler/bet-check
(27 tests pass); Ty.echo / Ty.echoR formers in proofs/BetLang.lean (machine-checked via
Lean 4 lake build, Progress/Preservation unaffected); echo-types entry in spec/SPEC.core.scm
+ grammar note; docs/echo-types.adoc design doc.

Documentation pass: new EXPLAINME.adoc guided tour; README.adoc/README.md refresh;
.machine_readable/6a2 STATE/META/ECOSYSTEM/AGENTIC (milestones, ADRs, ecosystem, agent
protocol); betlang-specific contractiles (Mustfile/Dustfile/README).

Echo operations (echo_intro, echo_to_residue, sample_echo, etc.) remain RESERVED/deferred.

Author: hyperpolymath

.machine_readable/6a2/AGENTIC.a2ml

@@ -3,8 +3,8 @@
 #
 # AGENTIC.a2ml — AI agent constraints and capabilities
 [metadata]
-version = "0.1.0"
-last-updated = "2026-04-11"
+version = "1.1"
+last-updated = "2026-06-02"
 
 [agent-permissions]
 can-edit-source = true
@@ -15,11 +15,30 @@ can-create-files = true
 
 [agent-constraints]
 # What AI agents must NOT do:
-# - Never use banned language patterns (believe_me, unsafeCoerce, etc.)
+# - Never use banned language patterns in Lean: sorry, admit, Admitted, postulate, believe_me, assert_total, unsafeCoerce
+# - `axiom` is NOT banned — it is used for classified obligations (see docs/proof-debt.adoc)
 # - Never commit secrets or credentials
-# - Never use banned languages (TypeScript, Python, Go, etc.)
+# - Never use banned languages (TypeScript outside playground, Python, Go, Java, Kotlin, Swift, Node.js, npm)
 # - Never place state files in repository root (must be in .machine_readable/)
 # - Never use AGPL license (use MPL-2.0)
+# - PROOF-NEEDS.md is a stub — do not overwrite it; its intentional format is preserved
+# - Echo canonical operation names (echo_intro, echo_to_residue, etc.) are RESERVED — do not implement
+# - Echo T is distinct from T; no implicit Echo T → T coercion; unify(Echo T, T) must fail
+# - EchoR T operations are fully deferred; do not add runtime payload to Echo T / EchoR T
+
+[agent-entry-protocol]
+# On entering a session working on this repo:
+# 1. Read .machine_readable/6a2/STATE.a2ml (current phase, blockers, next actions)
+# 2. Read .machine_readable/6a2/META.a2ml (ADRs, architecture decisions)
+# 3. If touching proofs: read PROOF-NEEDS.md and PROOF-STATUS.md
+# 4. If touching echo types: read docs/echo-types.adoc
+# 5. If touching governance: read .hypatia-ignore and .governance-allowlist
+
+[agent-exit-protocol]
+# On completing a session:
+# 1. Update STATE.a2ml with session outcomes (last-updated, milestones completed, next actions)
+# 2. Update PROOF-STATUS.md if any proof obligations changed
+# 3. Commit documentation and state updates together with code changes
 
 [maintenance-integrity]
 fail-closed = true
@@ -28,7 +47,20 @@ allow-silent-skip = false
 require-rerun-after-fix = true
 release-claim-requires-hard-pass = true
 
+[proof-toolchain]
+lean-version = "leanprover/lean4:v4.15.0"
+build-command = "lake build"
+scan-command = "tools/proof-scan.sh"
+banned-patterns = ["sorry", "admit", "Admitted", "postulate", "believe_me", "assert_total", "unsafeCoerce"]
+permitted-axioms = ["substTop_preserves_typing  # classified, standards#203, docs/proof-debt.adoc"]
+
 [automation-hooks]
-# on-enter: Read 0-AI-MANIFEST.a2ml, then STATE.a2ml
+# on-enter: Read STATE.a2ml, then META.a2ml
 # on-exit: Update STATE.a2ml with session outcomes
 # on-commit: Run just validate-rsr
+
+[typescript-policy]
+# No new TypeScript files.
+# Approved exemption: playground/** (6 .ts files, sandbox only).
+# Enforcement: .governance-allowlist + .hypatia-ignore.
+# Unblock condition: migrate playground to AffineScript or delete once experiment is settled.

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -3,18 +3,61 @@
 #
 # ECOSYSTEM.a2ml — Betlang ecosystem position
 [metadata]
-version = "1.0"
-last-updated = "2026-04-11"
+version = "1.1"
+last-updated = "2026-06-02"
 
 [project]
 name = "Betlang"
 purpose = "Ternary probabilistic programming with Dutch book prevention and gambling harm reduction"
 role = "programming-language"
+license = "PMPL-1.0 (SPDX: MPL-2.0)"
+repo = "https://github.com/hyperpolymath/betlang"
 
 [position-in-ecosystem]
 category = "probabilistic-programming"
+paradigm = ["functional", "probabilistic", "symbolic"]
+core-primitive = "(bet A B C) — ternary stochastic choice"
+type-system = "Hindley-Milner + Echo T / EchoR T structured-loss formers"
+proof-layer = "Lean 4 (machine-checked Progress + Preservation + monad laws)"
 
 [related-projects]
-projects = [
-  # No related projects recorded
-]
+# upstream / source-of-truth
+[[related-projects.upstream]]
+name = "echo-types"
+repo = "https://github.com/hyperpolymath/echo-types"
+language = "Agda"
+role = "Source of truth for Echo types (Echo f y := Σ(x:A), f x ≡ y proof-relevant fibre)"
+relationship = "betlang borrows the unary Echo T / EchoR T formers; does NOT implement the dependent fibre"
+
+[[related-projects.upstream]]
+name = "EchoTypes.jl"
+repo = "https://github.com/hyperpolymath/EchoTypes.jl"
+language = "Julia"
+role = "Executable finite-domain companion to echo-types"
+relationship = "betlang canonical operation names mirror EchoTypes.jl (echo_intro, echo_to_residue, etc.)"
+
+# engineering-position reference
+[[related-projects.alignment-target]]
+name = "affinescript"
+repo = "https://github.com/hyperpolymath/affinescript"
+language = "AffineScript / OCaml"
+role = "AffineScript compiler — RSR engineering position betlang is aligning toward"
+relationship = "betlang proof infrastructure and verification/ layout modelled on affinescript's RSR posture"
+
+[[related-projects.alignment-target]]
+name = "affinescriptiser"
+repo = "https://github.com/hyperpolymath/affinescriptiser"
+language = "AffineScript"
+role = "AffineScript tooling"
+
+# ecosystem tools
+[[related-projects.tooling]]
+name = "palimpsest-license"
+repo = "https://github.com/hyperpolymath/palimpsest-license"
+role = "PMPL-1.0 license definition (betlang uses PMPL-1.0 / SPDX: MPL-2.0)"
+
+[external-dependencies]
+proof-verifier = "Lean 4 (leanprover/lean4:v4.15.0)"
+build-tool = "Lake (bundled with Lean 4)"
+racket = "8.11 / 8.12 / current"
+rust-edition = "2021"

.machine_readable/6a2/META.a2ml

@@ -3,22 +3,67 @@
 #
 # META.a2ml — Betlang meta-level information
 [metadata]
-version = "0.1.0"
-last-updated = "2026-04-11"
+version = "1.1"
+last-updated = "2026-06-02"
 
 [project-info]
-license = "MPL-2.0"
+license = "PMPL-1.0 (SPDX: MPL-2.0)"
 author = "Jonathan D.A. Jewell (hyperpolymath)"
+contact = "j.d.a.jewell@open.ac.uk"
 
 [architecture-decisions]
-decisions = [
-  # No ADRs recorded
-]
+# ADR-001: Ternary core primitive
+[[architecture-decisions.records]]
+id = "ADR-001"
+title = "Ternary (bet A B C) as core primitive, not binary"
+status = "accepted"
+rationale = "Real-world decisions are three-valued; musical ternary form A-B-A provides compositional structure. Dutch book semantics require three outcomes minimum."
+
+# ADR-002: Lean 4 + Lake for mechanised proofs
+[[architecture-decisions.records]]
+id = "ADR-002"
+title = "Lean 4 / Lake for proofs, pure-core (no Mathlib)"
+status = "accepted"
+rationale = "Lean 4 provides a buildable, CI-checkable proof project with Lake. Pure-core avoids Mathlib version coupling. Progress + Preservation + monad laws are mechanised; 0 sorry, 1 classified axiom."
+
+# ADR-003: Echo T / EchoR T unary formers, distinct from carrier
+[[architecture-decisions.records]]
+id = "ADR-003"
+title = "Echo T and EchoR T as distinct unary type formers (not subtypes of T)"
+status = "accepted"
+rationale = "Upstream echo-types Agda repo defines Echo f y := Σ(x:A), f x ≡ y. BetLang is non-dependent; adds unary Echo T / EchoR T. Distinctness (unify(Echo T, T) fails) is the entire point of retained loss. Ghost/erased at runtime until operations demand payload."
+reference = "docs/echo-types.adoc, spec/SPEC.core.scm#echo-types"
+
+# ADR-004: AffineScript replaces TypeScript/ReScript for editor tooling
+[[architecture-decisions.records]]
+id = "ADR-004"
+title = "AffineScript (not TypeScript or ReScript) for VS Code extension source"
+status = "accepted"
+rationale = "Hyperpolymath language policy: no new TypeScript. ReScript was the previous choice (now deleted). AffineScript is the canonical replacement. Playground TypeScript files are an approved time-limited exemption."
+reference = ".claude/CLAUDE.md TypeScript Exemptions table"
+
+# ADR-005: Three-PR AffineScript alignment strategy
+[[architecture-decisions.records]]
+id = "ADR-005"
+title = "Separate PRs for proofs infrastructure, governance cleanup, and echo types"
+status = "accepted"
+rationale = "PR #53 (proofs) + PR #54 (governance) + PR #55 (echo types) kept independent so each is reviewable in isolation. Governance fixes isolated from proof infrastructure so neither blocks the other."
+
+# ADR-006: Echo operation names mirror EchoTypes.jl (reserved/deferred)
+[[architecture-decisions.records]]
+id = "ADR-006"
+title = "Canonical echo operation names are RESERVED cross-repo anchors, not committed semantics"
+status = "accepted"
+rationale = "echo_intro, echo_to_residue, residue_strictly_loses, echo_input, echo_output mirror EchoTypes.jl for cross-repo conceptual consistency. Not implemented in BetLang yet — no runtime/proof story settled. Error-Lang's stability penalty for echo_to_residue does NOT apply to BetLang."
+reference = "docs/echo-types.adoc#deferred"
 
 [development-practices]
 versioning = "SemVer"
-documentation = "AsciiDoc"
-build-tool = "just"
+documentation = "AsciiDoc (primary) + Markdown (secondary)"
+build-tool = "just (Justfile)"
+proof-build = "lake (lakefile.lean)"
+ci = "GitHub Actions (SHA-pinned)"
+package-management = "Guix (primary) / Nix (fallback) / Deno (JS)"
 
 [maintenance-axes]
 scoping-first = true

.machine_readable/6a2/STATE.a2ml

@@ -5,49 +5,78 @@
 [metadata]
 project = "betlang"
 version = "0.8.0-dev"
-last-updated = "2026-02-07"
+last-updated = "2026-06-02"
 status = "active"
-session = "converted from scheme — 2026-04-11"
+session = "affinescript-alignment + governance + echo-types — 2026-06-02"
 
 [project-context]
 name = "Betlang"
-purpose = """Safe probabilistic programming with Dutch book prevention and gambling harm reduction"""
-completion-percentage = 82
+purpose = """
+Safe probabilistic programming with Dutch book prevention and gambling harm reduction.
+Core primitive: (bet A B C) — ternary stochastic choice. Type system adds Echo T / EchoR T
+structured-loss formers (proof-relevant, ghost-erased). Proofs machine-checked in Lean 4.
+"""
+completion-percentage = 87
 
 [position]
-phase = "v0.8-julia-backend-development"   # design | implementation | testing | maintenance | archived
+phase = "proof-foundation + governance-alignment + echo-types-integration"
 maturity = "experimental"  # experimental | alpha | beta | production | lts
 
+[recent-sessions]
+# Session 2026-06-02: AffineScript alignment, governance cleanup, Echo types
+# PR #53: Lean 4 proof infrastructure (lakefile, proofs.yml, verification/, PROOF-STATUS.md)
+# PR #54: Governance/CI debt — Cargo.toml license, rackunit conflict, timeout-minutes,
+#          .governance-allowlist, .hypatia-ignore, delete Java, ReScript → AffineScript
+# PR #55: Echo T / EchoR T type formers in Rust checker + Lean + spec + docs
+
 [route-to-mvp]
 milestones = [
-  # No milestones recorded
+  "M1: Proof foundation — lakefile.lean + proofs.yml CI + banned-pattern gate [DONE #53]",
+  "M2: Governance clean — licence, language policy, Racket tests, timeout [DONE #54]",
+  "M3: Echo types core — Type::Echo/EchoR, unify, lower, Lean Ty.echo/echoR [DONE #55]",
+  "M4: Discharge substTop_preserves_typing axiom (PROOF-STATUS TP-4)",
+  "M5: Echo operations — echo_intro, proj1, echo_to_residue; typing rules",
+  "M6: sample_echo / bet_echo probabilistic bridge",
+  "M7: Julia backend Phase 2 — core language features",
 ]
 
+[proof-obligations]
+# See PROOF-STATUS.md for the full register (13 obligations)
+proved = ["TP-1 Progress", "TP-2 Preservation", "TP-3 Monad laws"]
+axioms = ["substTop_preserves_typing (classified, standards#203, docs/proof-debt.adoc)"]
+remaining = 10
+
 [blockers-and-issues]
 issues = [
-  # No blockers recorded
+  "bet-wasm E0308: pre-existing WASM backend breakage (match arm type mismatch, not caused by any of #53-55)",
+  "substTop_preserves_typing: classified axiom; discharge is M4 (Phase 2 proofs)",
+  "Echo operations deferred: no echo_intro/proj1/echo_to_residue until runtime/proof story settled",
 ]
 
 [critical-next-actions]
 actions = [
-  "Continue Julia backend Step 2: Core language features",
-  ")))
-    (optional-future-work
-      ((",
-  ")
-       (",
-  ")
-       (",
-  ")
-       (",
-  ")
-       (",
-  ")
-       (",
-  ")
-       (",
+  "Merge PR #54 → main (all-green)",
+  "Rebase PR #53 onto updated main, re-CI, merge",
+  "Retarget PR #55 to main, mark ready, merge",
+  "Phase 2 proof obligations: discharge substTop_preserves_typing",
+  "Echo operations pass: introduce echo_intro, echo_to_residue, proj1; typing rules in Lean",
+  "sample_echo / bet_echo probabilistic bridge (Dist T → Echo T)",
 ]
 
+[language-policy]
+primary = "Racket"          # core semantics
+proofs = "Lean 4"           # mechanised safety proofs
+compiler-tooling = "Rust"   # bet-core, bet-check, bet-parse, bet-wasm (paused)
+editor-tooling = "AffineScript"  # replaces TypeScript/ReScript in editors/
+compute-backend = "Julia"   # numerical/statistical kernel
+scripts = "Bash/POSIX shell + Just"
+config = "Nickel / 6a2 Scheme (.a2ml)"
+banned = ["TypeScript (except playground sandbox)", "Node.js", "npm", "Go", "Python", "Java", "Kotlin", "Swift"]
+
 [maintenance-status]
-last-run-utc = "2026-02-07T00:00:00Z"
-last-result = "unknown"  # unknown | pass | warn | fail
+last-run-utc = "2026-06-02T14:00:00Z"
+last-result = "pass"  # unknown | pass | warn | fail
+# Racket tests: pass (current + 8.11 + 8.12 on PR #54)
+# Governance: pass (all checks on PR #54)
+# Lean proofs: pass (proofs.yml lake build on PR #53)
+# Echo types: pass (cargo test -p bet-check: 27 tests pass on PR #55)