chore(betlang): housekeeping — axiom-free doc reconciliation, rot untrack, SPDX, license badge

Reconcile docs to the axiom-free reality. substTop_preserves_typing is a
proved theorem (proofs/BetLang.lean:918), verified by `lake build`; zero
`axiom` declarations remain. Six artefacts still called it a live axiom:
- docs/proof-debt.adoc: move substTop from §(c) NECESSARY AXIOM to §(a)
  DISCHARGED; marker count 1 -> 0.
- PROOF-STATUS.md: TP-4 -> Done; axiom-free note; banned-patterns wording.
- PROOF-NEEDS.md: TP-4 status -> done.
- .machine_readable/6a2/STATE.a2ml: M4 done; axioms=[]; remaining 10->9;
  drop already-merged-PR (#53/#54/#55) next-actions.
- README.md / README.adoc / EXPLAINME.adoc: "one permitted axiom" -> axiom-free.

Untrack build rot + tidy:
- remove 8 stale *.bak.20250719-182140 backups.
- untrack 321 Gleam build artefacts under lsp/bet-lsp/build/ (already gitignored).
- remove broken root symlink SPEC.core.scm (target migrated .scm -> .a2ml).
- gitignore lake-manifest.json (zero-dep project; regenerated on every build).

Conformance:
- add SPDX headers to core/betlang.rkt, lib/ternary.rkt, repl/shell.rkt,
  tests/basics.rkt (Mustfile requires SPDX on .rkt).
- drop redundant/incorrect PMPL-1.0 license badge (LICENSE + SPDX = MPL-2.0).

Verified: `lake build` green (Lean v4.15.0), tools/proof-scan.sh clean,
working tree clean. No Lean sources changed.

https://claude.ai/code/session_01VwbFNQJw23tW8tqM7utWku

Author: claude

.gitignore

@@ -49,3 +49,4 @@ dist/
 *.olean
 lake-packages/
 lakefile.olean
+lake-manifest.json

.machine_readable/6a2/STATE.a2ml

@@ -34,33 +34,30 @@ milestones = [
   "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)",
+  "M4: Discharge substTop_preserves_typing axiom (PROOF-STATUS TP-4) [DONE — now a proved theorem; axiom-free core]",
   "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
+proved = ["TP-1 Progress", "TP-2 Preservation", "TP-3 Monad laws", "TP-4 substTop_preserves_typing (discharged — axiom-free)"]
+axioms = []
+remaining = 9
 
 [blockers-and-issues]
 issues = [
   "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 = [
-  "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",
+  "TP-5: Echo-operation typing rules + metatheory in Lean (echo_intro, echo_to_residue, proj1)",
   "sample_echo / bet_echo probabilistic bridge (Dist T → Echo T)",
+  "Julia backend Phase 2 — core language features",
+  "bet-wasm E0308: fix pre-existing WASM backend match-arm type mismatch",
 ]
 
 [language-policy]

EXPLAINME.adoc

@@ -80,8 +80,8 @@ there.
 * **Preservation** — typing is invariant under small-step reduction.
 * **Distribution monad laws** — the probability monad is correctly structured.
 
-One permitted axiom: `substTop_preserves_typing` — classified, triaged in
-`docs/proof-debt.adoc`, tracked as standards#203.
+Axiom-free: `substTop_preserves_typing` is a proved theorem (formerly a
+classified axiom, since discharged; see `docs/proof-debt.adoc` §(a), standards#203).
 
 Proof infrastructure: `lakefile.lean`, `lean-toolchain` (pins `leanprover/lean4:v4.15.0`),
 `.github/workflows/proofs.yml` (runs `lake build` + `tools/proof-scan.sh` on every PR).
@@ -222,8 +222,8 @@ structurally: `Echo T ~ Echo T'` iff `T ~ T'`.
 
 === Proof debt
 
-`docs/proof-debt.adoc` — records the single classified axiom
-(`substTop_preserves_typing`, standards#203). No other unsoundness.
+`docs/proof-debt.adoc` — records the discharged `substTop_preserves_typing`
+lemma (formerly a classified axiom; standards#203). No axioms remain; no other unsoundness.
 
 === PROOF-STATUS.md
 
@@ -269,7 +269,6 @@ Tracks the 13 proof obligations across their completion stages. Currently 3/13 d
 * Runtime residue payload for `Echo T` / `EchoR T` — ghost-erased until operations demand
 * WASM backend (`compiler/bet-wasm/`) — pre-existing breakage, non-critical
 * Julia backend Phase 2 — active but separate work stream
-* `substTop_preserves_typing` discharge — Phase 2 proof obligation
 
 == For AI agents
 

PROOF-NEEDS.md

@@ -27,7 +27,7 @@ This file defines *what* must be proven. Completion is tracked in
 | TP-1   | Progress (well-typed ⇒ value or steps)             | TP   | Lean4  | P1 | ✅ done |
 | TP-2   | Preservation (typing preserved under step)          | TP   | Lean4  | P1 | ✅ done |
 | TP-3   | Distribution monad laws (×3)                        | TP   | Lean4  | P1 | ✅ done |
-| TP-4   | Discharge `substTop_preserves_typing` axiom         | TP   | Lean4  | P1 | remaining |
+| TP-4   | Discharge `substTop_preserves_typing` axiom         | TP   | Lean4  | P1 | ✅ done |
 | TP-5   | Echo-operation typing rules + metatheory (Progress/Preservation) | TP | Lean4 | P2 | remaining |
 | SEM-1  | Continuous measure-theoretic denotation             | SEM  | Lean4  | P2 | remaining |
 | STAT-1 | Maximum entropy of uniform ternary = log₂3          | STAT | Lean4  | P2 | remaining |

PROOF-STATUS.md

@@ -29,11 +29,12 @@ See `docs/AFFINESCRIPT-ALIGNMENT.adoc` for the phased plan and
 | TP-1 | Progress — well-typed closed term is a value or steps | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
 | TP-2 | Preservation — typing preserved under reduction | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
 | TP-3 | Distribution monad laws (left id, right id, assoc) | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
+| TP-4 | Discharge `substTop_preserves_typing` (de Bruijn subst lemma) — now a proved theorem, axiom-free | Lean4 | `proofs/BetLang.lean` | `lake build` (CI: `proofs.yml`) |
 
-> Note: TP-2 currently depends on the classified necessary axiom
-> `substTop_preserves_typing` (`proofs/BetLang.lean`). It is an explicit
-> axiom, **not** a `sorry` — see `docs/proof-debt.adoc` §(c). Discharging
-> it (TP-4) yields an axiom-free core.
+> Note: TP-2 is axiom-free. `substTop_preserves_typing`
+> (`proofs/BetLang.lean:918`) is a fully proved `theorem` — the former
+> classified axiom (TP-4) has been discharged (see `docs/proof-debt.adoc`
+> §(a)). No `axiom` declarations remain.
 
 ## Proofs In Progress
 
@@ -51,7 +52,6 @@ See `docs/AFFINESCRIPT-ALIGNMENT.adoc` for the phased plan and
 
 | ID | Proof | Category | Prover | Phase | Priority |
 |----|-------|----------|--------|-------|----------|
-| TP-4   | Discharge `substTop_preserves_typing` (de Bruijn subst lemma) | TP   | Lean4  | 2 | P1 |
 | TP-5   | Echo-operation typing rules + metatheory — mirror `bet-check`'s functor/comonad surface (`echo`, `echo_map`, `echo_output`, `echo_duplicate`, `echo_to_residue`, `sample_echo`), incl. the comonad laws from `EchoGradedComonad.agda` | TP | Lean4 | 2 | P2 |
 | SEM-1  | Continuous measure-theoretic denotational semantics           | SEM  | Lean4  | 2 | P2 |
 | STAT-1 | Maximum entropy of uniform ternary = log₂3 bits               | STAT | Lean4  | 2 | P2 |
@@ -75,8 +75,9 @@ just proof-scan           # banned-pattern gate only
 
 `sorry` / `admit` (Lean), `Admitted` (Coq), `postulate` / `believe_me` /
 `assert_total` (Idris2/Agda), `unsafeCoerce`. Enforced by
-`tools/proof-scan.sh` in CI (`.github/workflows/proofs.yml`). The single
-classified `axiom` is permitted by policy (standards#203).
+`tools/proof-scan.sh` in CI (`.github/workflows/proofs.yml`). No `axiom`
+declarations remain; any future classified `axiom` would be permitted by
+policy (standards#203) and registered in `docs/proof-debt.adoc`.
 
 ## Changelog
 

README.adoc

@@ -79,8 +79,8 @@ Over time, the full **uncertainty number tower migrates here**.
 === Lean 4 — Proof / Verification Layer
 
 * Machine-checks **Progress**, **Preservation**, and distribution **monad laws**
-* **Zero `sorry`** — one permitted classified axiom (`substTop_preserves_typing`,
-  see `docs/proof-debt.adoc`)
+* **Zero `sorry`, zero `axiom`** — `substTop_preserves_typing` is fully proved
+  (formerly a classified axiom, since discharged; see `docs/proof-debt.adoc`)
 * `lakefile.lean` + `lean-toolchain` make proofs a first-class Lake project
 * `.github/workflows/proofs.yml` verifies every PR via `lake build`
 

README.md

@@ -3,7 +3,6 @@
 
 [![Sponsor](https://img.shields.io/badge/Sponsor-%E2%9D%A4-pink?logo=github)](https://github.com/sponsors/hyperpolymath)
 [![License: MPL-2.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](LICENSE)
-[![License: PMPL-1.0](https://img.shields.io/badge/License-PMPL--1.0-indigo.svg)](PALIMPSEST.adoc)
 
 # BetLang
 
@@ -64,7 +63,7 @@ demand a payload. See [docs/echo-types.adoc](docs/echo-types.adoc).
 
 - `lakefile.lean` + `lean-toolchain` → buildable Lake project
 - `.github/workflows/proofs.yml` → CI-checked on every PR (`lake build` + banned-pattern scan)
-- One permitted classified axiom: `substTop_preserves_typing` (see `docs/proof-debt.adoc`)
+- Axiom-free: `substTop_preserves_typing` is fully proved — no `axiom`/`sorry` (see `docs/proof-debt.adoc`)
 
 ---
 
@@ -117,7 +116,7 @@ See [CONTRIBUTING.md](CONTRIBUTING.md). For a guided tour, read [EXPLAINME.adoc]
 
 ## License
 
-BetLang uses **PMPL-1.0** (Palimpsest Public License). SPDX identifier: `MPL-2.0`.
+BetLang is licensed under **MPL-2.0**. SPDX identifier: `MPL-2.0`.
 
 See [LICENSE](LICENSE) and [PALIMPSEST.adoc](PALIMPSEST.adoc).
 

SPEC.core.scm

@@ -1,4 +1,6 @@
 #lang racket
+; SPDX-License-Identifier: MPL-2.0
+; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
 (provide bet
          bet/weighted
          bet/conditional