proof(solo-core): QTT substitution lemma + preservation (axiom-free) — F1.4 phase 4

Discharge F1.4: `Theorem preservation : Preservation.` and
`affine_pres : AffinePreservation.` are now real `Qed.`, axiom-free
(`Print Assumptions` = "Closed under the global context"), over the
separated QTT context (Usage.v).

Architecture (standard de Bruijn type-soundness, adapted to the
separated tctx+uvec context):
- shape invariant: has_type G D t a -> ulen D = tlen G
- weakening (ht_shift): insert a fresh Zero-usage variable at any
  de Bruijn depth; structural over all 15 term constructors
- substitution (ht_subst): open-context QTT substitution at a context
  boundary; the affine accounting is pure usage-vector algebra
  (subst_reassoc_add / subst_reassoc_mult), where uadd_comm /
  uadd_assoc / uscale_add pay off — no non-commutative context fact is
  ever needed (the promised payload of the separated context)
- preservation: induction on `step`; redex cases use the substitution
  corollaries (subst_lemma0 / subst2_lemma), congruence cases the IH

Kernel fix (Syntax.v): subst2 now pre-shifts the inner substitutee —
subst0 u1 (subst0 (shift 0 u2) t) — so it is correct for OPEN tensor
components (required by preservation over a non-empty context; the old
form corrupted u2's index-0 free variable). Identical to the old
definition on CLOSED values (shift 0 is the identity there), so
closed-program evaluation and `progress` are unchanged.

Docs: README.md / proofs/STATUS.md / Soundness.v header updated to mark
the Coq track of progress/preservation as locally-checked (axiom-free
Qed); the Idris twin remains a tracked obligation (Phase F5 parity).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

README.md

@@ -65,7 +65,7 @@ proof is described as "proved" there until a proof assistant accepts it.
 | Solo syntax, contexts, typing (Coq + Idris2) | *locally-checked* |
 | Operational semantics (CBV small-step) | *locally-checked* — Phase **F1.1 done** (both tracks) |
 | **Progress** | *locally-checked* — Phase **F1.3 done**: Coq `Theorem … Qed.` (axiom-free); Idris total, hole-free |
-| Preservation | *statement-only* — Phase F1.4, **gated on the product/elimination decision** ([#93](https://github.com/hyperpolymath/my-lang/issues/93)) |
+| Preservation | *locally-checked (Coq)* — Phase **F1.4 done** on the Coq track: `Theorem preservation : Preservation.` and `affine_pres` are real `Qed.` (axiom-free, `Print Assumptions` closed), via the open-context QTT substitution lemma `ht_subst`. Product/elimination decision settled (additive `&` + multiplicative `⊗` both coherent). Idris twin pending (Phase F5 parity). |
 | Echo in the type system (`TEcho`, `MkEcho`/`Weaken`, `THEcho`/`THWeaken`, `EchoMode`, `EchoResidue`) | *locally-checked* — Echo is a first-class type former in the formal kernel; `EchoResidue` backs the Rust `Ty::Echo` (5/5 unit tests are its laws) |
 | Paper proofs (~6.3k lines) | *proved-on-paper* |
 | Proof CI | *absent* — Phase F5 (wiring `coqc` + `idris2 --build`) |

proofs/STATUS.md

@@ -34,10 +34,12 @@ Last verified: 2026-06-02.
 | QTT semiring + laws | Idris2 `idris/solo-core/Quantity.idr` | **locally-checked** | Semiring + ordering laws by exhaustive `Refl`, `%default total`. CI leg pending (Phase F5). |
 | QTT semiring + laws | Coq `coq/solo-core/Quantity.v` | **locally-checked** | Laws by `destruct; reflexivity`, real `Qed`. CI leg pending (F5). |
 | Solo syntax / contexts / typing | Idris2 + Coq `solo-core/` | **definitions-only** | de Bruijn terms, QTT context split/scale/zero, context-splitting typing judgement. |
-| `progress` | Idris2 + Coq `solo-core/Soundness` | **statement-only** | Coq `Definition Progress : Prop`; Idris `?todo_progress`. Proof = Phase F1.3. |
-| `preservation` | Idris2 + Coq `solo-core/Soundness` | **statement-only** | Coq `Definition Preservation : Prop`; Idris `?todo_preservation`. Proof = Phase F1.4. |
-| `affine_preservation` | Idris2 + Coq `solo-core/Soundness` | **statement-only** | Corollary of preservation. |
-| Small-step `Step`/`step` | Idris2 + Coq `solo-core/Soundness` | **statement-only** | Relation declared with no constructors yet; committed in F1.1. |
+| `progress` | Coq `solo-core/Soundness` | **locally-checked** | `Theorem progress : Progress.` real `Qed`, axiom-free (`Print Assumptions` closed). Phase F1.3. CI leg pending (F5). |
+| `progress` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_progress`. Proof = Phase F1.3 (Idris track). |
+| `preservation` / `affine_pres` | Coq `solo-core/Soundness` | **locally-checked** | `Theorem preservation : Preservation.` and `affine_pres : AffinePreservation.`, real `Qed`, axiom-free, via the open-context QTT substitution lemma `ht_subst`. Phase F1.4. CI leg pending (F5). |
+| `preservation` | Idris2 `solo-core/Soundness` | **statement-only** | `?todo_preservation`. Proof = Phase F1.4 (Idris track). |
+| Small-step `step` | Coq `solo-core/Soundness` | **definitions-only** | CBV left-to-right relation, all redex + congruence constructors. Committed in F1.1. |
+| Small-step `Step` | Idris2 `solo-core/Soundness` | **statement-only** | Idris twin (unverified on this track). |
 | General core typing + substitution | Coq `coq/Typing.v` | **locally-checked** | Pre-existing: 9 `Qed`, 0 `Admitted`. Non-quantitative; substitution lemma proved. |
 
 ## Paper proofs (`proofs/**.md`)
@@ -59,7 +61,7 @@ Last verified: 2026-06-02.
 | Topic AS has | my-lang status | Plan phase |
 |--------------|----------------|-----------|
 | Mechanised QTT solo-core | **commenced** (this PR) | F1 |
-| Mechanised progress/preservation | statement-only | F1.3 / F1.4 |
+| Mechanised progress/preservation | Coq **locally-checked** (axiom-free `Qed`); Idris twin pending | F1.3 / F1.4 |
 | Quantitative-types (dedicated doc) | folded into solo affine doc | F4 |
 | Row-polymorphism proof | absent | F4 |
 | Dependent/refinement types proof | absent | F4 |