proof(solo-core/idris): close preservation (#108) — total, hole-free

AFFIRMATION.adoc

@@ -4,8 +4,8 @@
 = Affirmation
 :toc: preamble
 :sectnums:
-:revdate: 2026-06-19T21:35:54Z
-:revnumber: 1
+:revdate: 2026-06-21T02:22:08Z
+:revnumber: 2
 
 This AFFIRMATION records the standing of *my-lang* against the hyperpolymath
 standards and this project's own honesty discipline, at the timestamp below.
@@ -29,12 +29,17 @@ Rust compiler. The normative obligation — the *must* — is that the language
 
 To the verified state of this repository, I affirm:
 
-. *Soundness is mechanised, not asserted.* The Coq solo-core proves
-  `progress`, `preservation`, and `affine_pres`; the algorithmic checker
-  (`check`, R5) and the affine decision (`aff_type_dec`, R5b); the
-  `me -> solo` elaboration adequacy (M1); the session-pi metatheory through
-  S3c.3; and the echo residue-measure seam (E4). All are real `Qed`,
-  *axiom-free* (`Print Assumptions` closed), and CI-gated.
+. *Soundness is mechanised, not asserted — now on BOTH tracks.* The Coq
+  solo-core proves `progress`, `preservation`, and `affine_pres`; the
+  algorithmic checker (`check`, R5) and the affine decision (`aff_type_dec`,
+  R5b); the `me -> solo` elaboration adequacy (M1); the session-pi metatheory
+  through S3c.3; and the echo residue-measure seam (E4). All are real `Qed`,
+  *axiom-free* (`Print Assumptions` closed), and CI-gated. The *Idris2 twin*
+  now also proves both `progress` and `preservation` (#108, discharged
+  2026-06-21): total, hole-free functions under `%default total` with no
+  postulates — `:total preservation` confirms — via the QTT substitution
+  lemmas `htSubst` / `substLemma0` / `subst2Lemma` (with `uaddAssoc`). The
+  solo core is hole-free on both tracks.
 
 . *No overclaim.* Every proof hole is recorded as an obligation, never as a
   result (`proofs/STATUS.md` is authoritative and wins over any prose).
@@ -56,20 +61,23 @@ To the verified state of this repository, I affirm:
 
 * Coq: `.github/workflows/proofs.yml` compiles the solo-core and asserts the
   headline theorems are axiom-free on every PR touching `proofs/verification/**`.
-* Idris2: `idris2 --build` under `%default total`; the only open marker is
-  `?todo_preservation` plus the five `htSubst` usage-splitting holes.
+* Idris2: `idris2 --build solo-core.ipkg` exits 0 under `%default total`,
+  no postulates / `believe_me` / `assert_total`; the solo core is HOLE-FREE
+  (`preservation`, `affinePreservation`, `htSubst`, `substLemma0`,
+  `subst2Lemma`, `uaddAssoc` all `:total`).
 * Rust: `cargo test -p my-qtt` and `cargo test -p my-lang qtt_bridge` green;
   `my-qtt` carries the R5/R5b oracle tests.
 
 == Affirmed NOT done (the honest boundary)
 
-The Idris twin's `preservation` (`#108`) is *not* proved. The QTT substitution
-lemma `htSubst` is structurally landed (10 of 15 cases; the `b`-index erasure
-resolved) and committed locally; the five usage-splitting cases, the
-`substLemma0` / `subst2Lemma` corollaries, and `preservation` itself remain
-open. This is the single outstanding *must*. The wasm / RISC-V / mobile /
-typed-wasm legs are *intends* and *wishes* (`docs/STATUS.adoc`), not affirmed
-as done.
+The normative *must* (a mechanised-sound core, coupled into the compiler) is
+met on both proof tracks. What remains is *intends* and *wishes*
+(`docs/STATUS.adoc`), affirmed as NOT done: making the QTT axis the *default*
+in `checker.rs`; surface quantity syntax for real per-binder linearity; the
+`wasm32` and `RISC-V` backend legs; the typed-wasm WasmGC verified leg
+(blocked on `typed-wasm` / AffineScript / Ephapax being added to the session);
+and Android / iOS via Tauri / Dioxus. The non-Solo dialect compilers (Duet /
+Ensemble) are scaffold only.
 
 == Affirmation
 
@@ -81,7 +89,7 @@ herein is described as proved that a proof assistant does not accept today.
 |===
 | Affirmed by | Jonathan D.A. Jewell (@hyperpolymath) <j.d.a.jewell@open.ac.uk>
 | Repository  | hyperpolymath/my-lang
-| Timestamp (UTC) | 2026-06-19T21:35:54Z
-| Verified basis | `main` @ `a7765e7` (merged: PR #116 `my-qtt`, PR #117 coupling step 2); dev `acd29d6` (`htSubst` structure)
+| Timestamp (UTC) | 2026-06-21T02:22:08Z
+| Verified basis | `claude/dreamy-hypatia-O8XHo` (Idris `preservation` #108 discharged, solo core hole-free) atop `main` @ `a7765e7` (PR #116 `my-qtt`, PR #117 coupling step 2)
 | Authority | `proofs/STATUS.md` (proofs) · `docs/STATUS.adoc` (programme) · `.machine_readable/contractiles/Mustfile.a2ml` (invariants)
 |===

docs/STATUS.adoc

@@ -18,11 +18,10 @@ file is the priority-grouped programme view.
 
 == Position (one line)
 
-my-lang's normative must is essentially met — the Coq metatheory is complete
-and axiom-free, and the verified usage-checker is merged into the Rust
-toolchain. The single open must is the Idris twin's `preservation`,
-structurally landed (10/15 `htSubst` cases, `b`-erasure solved), committed
-locally at `acd29d6`.
+my-lang's normative must is met — the Coq metatheory is complete and
+axiom-free, the verified usage-checker is merged into the Rust toolchain, and
+the Idris twin's `preservation` (#108) is now DISCHARGED (total, hole-free;
+`:total preservation`). The solo core is hole-free on both tracks.
 
 == MUST — my-lang itself (sound core, verified-coupled, compiling)
 
@@ -38,15 +37,14 @@ locally at `acd29d6`.
 | Surface -> core coupling (named engine + real `ast::Expr` bridge) | `[x]` | `main` (PR #117)
 | Idris twin `progress` (total, hole-free) | `[x]` | `main`
 | Working compiler pipeline parse->HIR->MIR->LLVM->native (x86_64 / aarch64) | `[x]` | `main`
-| **Idris twin `preservation` (#108)** — `htSubst` structure + `b`-erasure solved | `[~]` 10/15 cases | local `acd29d6`
+| **Idris twin `preservation` (#108)** — full `htSubst` + `subst2Lemma` + `uaddAssoc`, `Step`-induction, total + hole-free | `[x]` | `claude/dreamy-hypatia-O8XHo`
 |===
 
 == INTEND — planned next
 
 [cols="4,1,3",options="header"]
 |===
 | Item | Status | Note
-| Close Idris `preservation`: 5 `htSubst` split cases -> `substLemma0` / `subst2Lemma` | `[~]` next | consumes the landed `usplit3` / `uaddSplitBoundary2` / `substReassocAdd` / `substReassocMult`
 | Make the resource axis the *default* in `crates/my-lang/src/checker.rs` | `[ ]` | the QTT bridge is opt-in (`qtt_bridge::check_expr`) today
 | Surface *quantity syntax* so the bridge enforces real per-binder linearity | `[ ]` | `Param` has no quantity field; bridge defaults to `One`
 | `wasm32` via the existing LLVM backend (`TargetSpec::wasm32` + `wasm-ld`) | `[ ]` | fastest target leg; backend already emits objects
@@ -67,6 +65,6 @@ locally at `acd29d6`.
 == Provenance
 
 * Coq: axiom-free (`Print Assumptions` closed), CI-gated (`.github/workflows/proofs.yml`), no `Admitted`/`Axiom` in the trusted base.
-* Idris: `idris2 --build`-checked, `%default total`, no postulates; only `?todo_preservation` and the 5 `htSubst` split holes open.
+* Idris: `idris2 --build solo-core.ipkg` exits 0, `%default total`, no postulates / `believe_me` / `assert_total`; the solo core is HOLE-FREE (`preservation`, `affinePreservation`, `subst2Lemma`, `uaddAssoc`, `substLemma0`, `htSubst` all `:total`).
 * Rust: `cargo test -p my-qtt` (20 tests incl. the R5/R5b `reflexivity` oracle tests + the surface-coupling tests) and `cargo test -p my-lang qtt_bridge` (6 tests) green.
-* Landed this programme increment: PR #116 (`my-qtt`), PR #117 (coupling step 2); local `acd29d6` (`htSubst` structure).
+* Landed this programme increment: PR #116 (`my-qtt`), PR #117 (coupling step 2); `preservation` #108 discharged (this increment).

docs/handoff/NEXT-SESSION.md

@@ -10,38 +10,40 @@ branch `claude/dreamy-hypatia-O8XHo`; commit green slices; push and open a
 **draft** PR when a slice is complete. Read `docs/STATUS.adoc` (musts/intends/
 wishes) and `proofs/STATUS.md` (authoritative proof registry) first.
 
-## The one open MUST: close Idris `preservation` (#108)
+## The one open MUST is now CLOSED: Idris `preservation` (#108) ✓
 
-The Coq metatheory is complete and axiom-free. The Idris twin's `progress` is
-done; **`preservation` is the last normative obligation** (`?todo_preservation`
-in `proofs/verification/idris/solo-core/Soundness.idr`). It rests on the QTT
-substitution lemma `htSubst`, which is now **structurally landed** (commit
-`acd29d6` on the dev branch, build green 8/8):
+The Coq metatheory is complete and axiom-free, and **the Idris twin's
+`preservation` is now DISCHARGED** (2026-06-21): a total, hole-free function
+by induction on `Step` in `proofs/verification/idris/solo-core/Soundness.idr`,
+`:total preservation` confirmed, `%default total`, no postulates. The whole
+solo core is HOLE-FREE on both tracks. `htSubst` (all 15 cases), `substLemma0`,
+`subst2Lemma`, and `uaddAssoc` all land in `Substitution.idr` (the module
+dependency was inverted: `Soundness` now imports `Substitution`).
 
-- **10/15 `htSubst` cases proved**: Var, Unit, Lam, With, Fst, Snd, Inl, Inr,
-  MkEcho, Weaken.
-- **5 usage-splitting holes remain** in `Substitution.idr`:
-  `?htSubst_app`, `?htSubst_tensor`, `?htSubst_letpair`, `?htSubst_case`,
-  `?htSubst_let`.
-
-### Do this, in order
-1. Fill the 5 split holes. Each mirrors the Coq `ht_subst` case in
-   `proofs/verification/coq/solo-core/SoloCore.v` (≈ lines 1618–1889) and
-   **consumes already-landed lemmas**: `usplit3`, `uaddSplitBoundary2`,
-   `substReassocAdd` (additive, for App/Let), `substReassocMult` (for
-   Tensor/LetPair/Case), `uaddUappend`, `uscaleUappend`, `ushiftUscale`.
-   App splits `d1` and the `q`-scaled `d2`; Tensor/LetPair/Case split `d1`,`d2`;
-   Let scales `d1`. The binder cases (LetPair/Case/Let) recurse into bodies with
-   the prefix `I` extended (mirror the `hvSubst`/`htShift` binder pattern).
-2. Add `substLemma0` (the `I = TEmpty` corollary) and `subst2Lemma` (two-var,
-   for `LetPair`), mirroring Coq `subst_lemma0` / `subst2_lemma` (≈ 1893–1937).
-3. Fill `?todo_preservation` in `Soundness.idr` by induction on `Step`
-   (mirror Coq `preservation`, ≈ 1941–2036): reduction cases use
-   `substLemma0`/`subst2Lemma`; congruence cases recurse.
-4. Move the `preservation` row in `proofs/STATUS.md` to *machine-checked* and
-   update `docs/STATUS.adoc`.
+### Where the normative work goes next (the compilation axis)
+The sound core is done and coupled. The open items are *intends*/*wishes* in
+`docs/STATUS.adoc`:
+1. Make the QTT resource axis the **default** in `crates/my-lang/src/checker.rs`
+   (the bridge is opt-in today via `qtt_bridge::check_expr`).
+2. Add surface **quantity syntax** so the bridge enforces real per-binder
+   linearity (`Param` has no quantity field; the bridge defaults to `One`).
+3. **wasm32** via the existing LLVM backend (`TargetSpec::wasm32` + `wasm-ld`),
+   then **RISC-V** (`riscv64gc-unknown-linux-gnu`), then the **typed-wasm**
+   WasmGC verified leg (blocked until `typed-wasm` / AffineScript / Ephapax are
+   added to the working session).
 
 ### Load-bearing context (do NOT relitigate)
+- **`preservation` takes the reduct term `t` explicitly** (relevant), exactly
+  as `progress` does. Idris erases the derivation's term/type indices, but the
+  substitution lemmas compute on the bound body + substituted value, so those
+  must come from a matched (relevant) term; `{g}`/`{d}` are relevant for the
+  same reason. `subst2Lemma`'s result type `c` is an erased implicit.
+- **Per-clause pattern variables that unify** (the Lam/arrow quantity, the
+  Inl/Inr annotation vs the sum's summand, the Let quantity) must share ONE
+  name in the LHS — Idris rejects two names that provably unify.
+- **`let`-block rule**: don't mix type-annotated bindings with dependent-pair
+  pattern bindings in one block (parse error). Use single-binding nested
+  `let … in let …`, or inline.
 - **`b`-erasure is solved.** The result type `b` is a genuine type index, so
   `hvSubst` and `htSubst` both carry it as an **erased implicit** (`{0 b}` /
   auto-bound). Passing an *unrestricted* `b` (or an erased `b` to an
@@ -51,11 +53,12 @@ substitution lemma `htSubst`, which is now **structurally landed** (commit
 - **`THLet`/`THCase`/`THLetPair` carry explicit bound-type fields** (Option A,
   already merged) — that is how the binder cases recover the body context under
   erasure. Don't revert it.
-- Toolchain: Idris2 0.7.0 isn't preinstalled — bootstrap from source
-  (`make bootstrap SCHEME=chezscheme && make install`, ~10 min), then
-  `cd proofs/verification/idris/solo-core && idris2 --build solo-core.ipkg`.
-  Discipline: every edit ends with a compile; `--safe`/`%default total`; no
-  postulates; pin headline theorems where the repo convention does.
+- Toolchain: if Idris2 0.7.0 isn't preinstalled, bootstrap from source
+  (`make bootstrap SCHEME=chezscheme && make install`, ~10 min). Then
+  `cd proofs/verification/idris/solo-core && idris2 --build solo-core.ipkg`
+  (exit 0), and check totality with `:total <name>` in the REPL. Discipline:
+  every edit ends with a compile; `%default total`; no postulates; pin
+  headline theorems where the repo convention does.
 
 ## The other axis: fundamentals -> compilation (see docs/STATUS.adoc)
 

proofs/STATUS.md

@@ -61,7 +61,7 @@ Last verified: 2026-06-14.
 | `progress` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem progress : Progress.` real `Qed`, axiom-free. Phase F1.3. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed. |
 | `progress` | Idris2 `solo-core/Soundness` | **locally-checked** | Hole-free total function (no `?todo_progress`); accepted by `idris2`, package built in CI (`proofs.yml`). Phase F1.3. **Re-proven over the SEPARATED context (`Tctx`/`Uvec`) + both products (`TWith`/`TTensor`, `LetPair`) in the 2026-06-15 F1.4 design migration** — closed-term inversions now massage only the usage vector (`uaddEmpty`/`uscaleEmpty`), since the shared type context stays `TEmpty` automatically; `:total progress` confirms totality. |
 | `preservation` | Coq `solo-core/SoloCore` | **machine-checked** | `Theorem preservation : Preservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI: `proofs.yml` compiles it + asserts `Print Assumptions` closed (and likewise `affine_pres`). |
-| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`, **now stated over the CORRECT design** (separated context + genuine products). The OLD Idris design (split-intro `Pair` + project-elim `Fst`/`Snd`) made the same-usage statement UNSOUND (issue #93); the 2026-06-15 migration makes it provable. Proof obligation = Phase F1.4 (Idris track), #108 — the QTT substitution lemma (`htSubst` + `subst2Lemma`) lands in a companion `Substitution.idr` and is wired in here once discharged. NOT described as proved. **Progress (2026-06-19): `Substitution.idr` (in the ipkg) now carries the append-context algebra, the shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift` (term weakening, all 14 cases), the substitution accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`), `hvSubst`, the FULL `htSubst` (the QTT substitution lemma — all 15 cases, total, hole-free), and `substLemma0` (the `subst0` corollary). The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` as an erased implicit in `hvSubst`/`htSubst`. `idris2 --build` exits 0; the ONLY remaining hole in the whole solo-core is `?todo_preservation`. REMAINING for `preservation`: `uaddAssoc` -> `subst2Lemma` (two-variable LetPair substitution) -> the `Step`-induction. PENDING (still NOT proved).** |
+| `preservation` | Idris2 `solo-core/Soundness` | **locally-checked** | **DISCHARGED 2026-06-21 (#108).** `preservation : (t : Tm) -> Has g d t a -> Step t t' -> Has g d t' a` is a total, hole-free function by induction on `Step` — `:total preservation` confirms; `%default total`, no `postulate`/`believe_me`/`assert_total`/`?hole`. Mirrors the Coq twin `preservation`: the β/projection/elimination cases consume the QTT substitution lemmas from `Substitution.idr` — `substLemma0` (App/Case/Let single-variable) and `subst2Lemma` (LetPair two-variable) — realigning the residual usage with `d` via `uadd` commutativity/associativity (`uaddAssoc`) and `uscale One`; congruence cases recurse structurally. Stated over the CORRECT design (separated context + genuine products) that made the same-usage statement sound (issue #93). The reduct term `t` is taken explicitly (relevant), exactly as `progress` does, because Idris erases the derivation's term/type indices while the substitution lemmas compute on the bound body + substituted value. `affinePreservation` follows as the Solo-kernel corollary (`:total` too). Supporting chain in `Substitution.idr` (all total, hole-free): append-context algebra, shape invariant (`shapeVar`/`shapeType`), `hvShift`/`htShift`, the accounting algebra (`qReassoc`/`vecReassoc`/`substReassocAdd`/`substReassocMult`/`usplit3`/`uaddSplitBoundary2`/`uaddAssoc`), `hvSubst`, the FULL `htSubst` (all 15 cases), `substLemma0`, `subst2Lemma`. The `b`-index-erasure obstruction (ADR-003) is resolved by carrying `b` erased. `idris2 --build solo-core.ipkg` exits 0; **the solo core is now HOLE-FREE**. CI: `proofs.yml` Idris job. |
 | Small-step `step` | Coq `solo-core/SoloCore` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. |
 | Small-step `Step` | Idris2 `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, both products: additive `SFst`/`SSnd` fire on `With` values, multiplicative `SLetPair` fires on a `Tensor` value via `subst2`; plus the echo residue rules (`SWeaken`). Consumed by the verified `progress`. Migrated 2026-06-15. |
 | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. |
@@ -86,7 +86,7 @@ Last verified: 2026-06-14.
 | Topic AS has | my-lang status | Plan phase |
 |--------------|----------------|-----------|
 | Mechanised QTT solo-core | **commenced** (this PR) | F1 |
-| Mechanised progress/preservation | Coq **machine-checked** (axiom-free `Qed`, CI-guarded); Idris twin pending | F1.3 / F1.4 |
+| Mechanised progress/preservation | Coq **machine-checked** (axiom-free `Qed`, CI-guarded); Idris twin **locally-checked** (both total + hole-free; `preservation` #108 discharged 2026-06-21) | F1.3 / F1.4 |
 | Algorithmic typing / decidable typecheck (static-split ≡ usage-walk) | Coq **machine-checked** (`check_correct`, axiom-free) — **overtakes AS** (states it as prose "future work" only) | F1.4 |
 | Surface→core elaboration correctness (`me` → `solo`) | Coq **machine-checked** (`me_wt_sound` over the WHOLE `me_tm` + `elab_data_check`, axiom-free, M1.1/M1.1b — M1 complete) — **overtakes AS** (solo-only; no `me`-like dialect, nothing analogous as surveyed (AS@main 2026-06-02)) | M1 |
 | Quantitative-types (dedicated doc) | folded into solo affine doc | F4 |