docs(coq): correct stale "only ONE case" claim in preservation PROOF STATUS (#104)

## Summary

Docs-only correction to the `PROOF STATUS [preservation]` comment in
`formal/Semantics.v` (lines 3328+). PR #92 honestly marked preservation
`Admitted.` after `coqc` rejected the `Qed.`, but the earlier in-file
comment at line 3269 continued to claim **"Only ONE case remains open:
S_Region_Step + T_Region_Active"** — that's the *language-design*
bottleneck, not the actual goal count.

## Diagnostic

```bash
# Replace `Admitted.` with `Qed.` at line 3327; insert before it:
#   all: match goal with |- ?G => idtac G end.
$ coqc -Q . Ephapax Semantics.v 2>&1 | grep '^REMAINING' | wc -l
40
```

40 goals remain open across many type-shape variants:

```
exists G_out, R'; G  |- e' : T0           -| G_out   (many)
exists G_out, R'; G  |- e' : TBase TUnit  -| G_out
exists G_out, R'; G  |- e' : TBase TBool  -| G_out
exists G_out, R'; G  |- e' : TBase TI32   -| G_out
exists G_out, R'; G0 |- e' : TString r0   -| G_out
exists G_out, R'; G0 |- e' : TFun  T1 T2  -| G_out
exists G_out, R'; G0 |- e' : TProd T1 T2  -| G_out
exists G_out, R'; G0 |- e' : TSum  T1 T2  -| G_out
exists G_out, R'; G0 |- e' : TBorrow T    -| G_out
exists G_out, R'; G0 |- e' : TProd T T    -| G_out
```

## Root cause

These are mostly **congruence-case failures**, not the documented
`S_Region_Step` language-design item. The proof script's IH-application
pattern picks **ANY** `has_type` hypothesis in scope:

```coq
match goal with
| [ IH : forall _ _ _, _ -> exists _, _ |- _ ] =>
  match goal with
  | [ H : has_type _ _ _ _ _ |- _ ] =>
      destruct (IH _ _ _ H) ...
```

With multiple inversion-introduced `has_types` (one per typing premise
of each compound expression), it often picks the wrong one.
`eassumption` then fails silently inside `try solve [...]`.

## What this PR does

Updates the `PROOF STATUS` comment block at line 3328+ to:
- Quote the ~40 goal count
- List the type-shape variants
- Explain why the existing `try solve [...]` scaffolding fails (pattern
picks wrong `has_type`)
- Document that closing these goals is **multi-day proof engineering**,
separate from the S_Region_Step language-design item

No proof change. `Admitted.` remains; `Qed.`-proven supporting lemmas
are still `Qed.`.

## Verification

```
$ coqc -Q . Ephapax Semantics.v
(builds clean, ~1 minute)
```

## Refs

- `ephapax#92` (honest framing of preservation Admitted)
- `standards#124` (proof-debt audit epic)

## Test plan

- [x] `coqc -Q . Ephapax Semantics.v` builds clean
- [x] No proof tactic changed; only the comment block at lines 3328+
- [ ] CI green

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -10,7 +10,7 @@
 - Coq admitted proofs remaining in `formal/Semantics.v`: 1 (`preservation`)
 
 ## What needs proving
-- **`preservation`**: Close the remaining open goals in the proof script at `formal/Semantics.v` L3215–L3326 so the `Qed` lands and the file builds without `Admitted.` The supporting lemmas (`region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`) are Qed; the residual gap is in the top-level case analysis on `step`.
+- **`preservation`**: Close the remaining **~40 open goals** in the proof script at `formal/Semantics.v` L3215–L3326 so the `Qed` lands and the file builds without `Admitted.` The supporting lemmas (`region_env_perm_typing`, `region_add_typing`, `region_shrink_preserves_typing`) are Qed; the residual gap is in the top-level case analysis on `step`. Diagnostic build (2026-05-20, `Admitted → Qed` + `idtac` at the remaining-goals point) shows the open goals span ten distinct type-shape variants: `TBase TUnit/TBool/TI32`, `T0`, `TString`, `TFun`, `TProd`, `TSum`, `TBorrow`. Most are congruence-case failures — the proof script's IH-application pattern picks ANY `has_type` in scope and frequently picks the wrong one when inversion introduces multiple typing premises. Closing them is multi-day proof engineering: each step-constructor's congruence case needs its IH applied to the specific inner-expression typing (not just any `has_type`), then the outer typing reconstructed by the matching typing constructor. An earlier in-file comment in `formal/Semantics.v` claimed "Only ONE case remains open: S_Region_Step + T_Region_Active" — that's the *language-design* bottleneck (region-env weakening for non-values), real, but the ~40 figure is the congruence-case overcount on top of it.
 - **Linear type consumption**: Prove resources with linear types are consumed exactly once across all execution paths (region boundaries, exception handlers)
 - **Effect system soundness**: Prove the effect type system correctly tracks side effects and that effect-free terms are truly pure
 - **Region safety**: Prove that region-based memory management prevents use-after-free and dangling references across region boundaries

formal/Semantics.v

@@ -3326,14 +3326,47 @@ Proof.
     end).
 Admitted.
 (* PROOF STATUS [preservation] — ADMITTED.
-   Earlier in-file note claimed "FULLY CLOSED (2026-04-27). Zero Admitted." with
-   `Qed.` here, but `coqc` (8.18.0) rejects that with "Attempt to save an
-   incomplete proof (there are remaining open goals)" — the proof script's nested
-   tactic combinator does not discharge every case of the inductive predicate.
-   Until the open goals are identified and closed, the honest mark is `Admitted.`
-   so the Coq formalisation builds and downstream docs (ROADMAP, PROOF-NEEDS)
-   accurately reflect the proof state. Supporting lemmas remain Qed:
+
+   Earlier in-file note (above, around line 3269) claimed "Only ONE
+   case remains open: S_Region_Step + T_Region_Active." Diagnostic
+   build (Admitted -> Qed + `all: match goal with |- ?G => idtac G end`
+   inserted before the Qed) on 2026-05-20 disproves that count:
+   ~40 goals remain open across the following type-shape variants —
+
+     exists G_out, R'; G  |- e' : T0           -| G_out   (many)
+     exists G_out, R'; G  |- e' : TBase TUnit  -| G_out
+     exists G_out, R'; G  |- e' : TBase TBool  -| G_out
+     exists G_out, R'; G  |- e' : TBase TI32   -| G_out
+     exists G_out, R'; G0 |- e' : TString r0   -| G_out
+     exists G_out, R'; G0 |- e' : TFun  T1 T2  -| G_out
+     exists G_out, R'; G0 |- e' : TProd T1 T2  -| G_out
+     exists G_out, R'; G0 |- e' : TSum  T1 T2  -| G_out
+     exists G_out, R'; G0 |- e' : TBorrow T    -| G_out
+     exists G_out, R'; G0 |- e' : TProd T T    -| G_out
+
+   The "only ONE case" framing — accurate for the *language-design*
+   bottleneck (S_Region_Step + T_Region_Active needs region-env
+   weakening for non-values) — has obscured that the surrounding
+   try-solve scaffolding ALSO fails to close many simpler congruence
+   cases. The proof script's IH-application pattern
+       match goal with
+       | [ IH : forall _ _ _, _ -> exists _, _ |- _ ] =>
+         match goal with
+         | [ H : has_type _ _ _ _ _ |- _ ] =>
+             destruct (IH _ _ _ H) ...
+       end end
+   picks ANY has_type in scope; with multiple inversion-introduced
+   has_types it often picks the wrong one and the subsequent
+   `eassumption` fails silently inside `try solve [...]`.
+
+   Closing the additional ~40 goals is multi-day proof engineering:
+   each step-constructor's congruence case needs its IH applied to
+   the specific inner-expression typing (not just any has_type), then
+   the outer typing reconstructed by the matching typing constructor.
+   Tracked separately from the S_Region_Step language-design item.
+
+   Supporting lemmas remain Qed:
      region_env_perm_typing: Qed (transfers typing across region-env permutations).
      region_add_typing: Qed (adding a region to R preserves typing).
      region_shrink_preserves_typing: Qed (T_Region_Active shadowing case closed via in_dec).
-   preservation itself: Admitted, pending discharge of the residual open goals. *)
+   preservation itself: Admitted, pending discharge of the residual ~40 open goals. *)