chore(machine-readable): correct STATE.a2ml proof-status lie (Refs standards#134) (#103)

## Summary

`.machine_readable/6a2/STATE.a2ml` claimed:

```
# No active blockers. Formal proofs FULLY CLOSED (67 Qed, 0 Admitted).
```

This was wrong on both axes:

- `formal/Semantics.v::preservation` carries `Qed.` but `coqc` 8.18.0
rejects it with "Attempt to save an incomplete proof (there are
remaining open goals)" — the proof never actually closed. PR#92 (MERGED)
marked it `Admitted.` to restore CI green; PR#102 (OPEN) reduces the
open-goal count from 910 to ~29 via the standard remember-cfg
preservation pattern. So there's at least 1 `Admitted`, not 0.
- `src/formal/Ephapax/Formal/RegionLinear.idr::regionSafetyExtract` /
`noGCExtract` are **vacuous tautological wrappers** (body is the input
unchanged: `= ne` / `= (ne, lc)`). ROADMAP citing them as
"regionSafetyTheorem"/"noGCTheorem" complete is overstated. The honest
E3 (region no-escape) and E4 (no-runtime-GC) obligations are stated in
`src/abi/Ephapax/ABI/Invariants.idr` (the Rust/SPARK seam landed via
PR#95-MERGED).

## What changed

- `phase`, `next_action`, `last_action`, `updated` brought to
2026-05-20.
- `@blockers` block now lists the residual proof debt accurately:
  - Semantics.v `preservation` Admitted (with handoff doc pointer)
  - vacuous RegionLinear wrappers
  - E1–E6 invariant register from the new ABI seam

## What's not in this PR

No source/proof changes. This is purely the machine-readable artefact
catching up to the actual code state. The human-readable docs
(`ROADMAP.adoc`, `PROOF-NEEDS.md`, `RUST-SPARK-STANCE.adoc`) already
reflect this after the 2026-05-20 batch of PR#92 + #95 + #102.

## Refs

Refs standards#134 (**NOT Closes** — joint-close on agreement).

## Test plan

- [x] No `.v` / `.idr` / Rust files touched — build state unaffected
- [x] STATE.a2ml syntax preserved (comment lines + `@state` block +
`@blockers` block + matching `@end`s)
- [ ] CI green (no jobs apply to machine-readable artefacts)

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -6,11 +6,28 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Wire real PipeWire session through type checker (PipeWire Proving Ground)"
-last_action: "Standardized to RSR 2026 with v2 STATE format and 6a2 alignment"
-updated: 2026-04-23T13:00:00Z
+next_action: "Close residual ~29 open goals in formal/Semantics.v preservation theorem (see formal/PRESERVATION-HANDOFF.md for per-case checklist)"
+last_action: "Rust/SPARK ABI seam landed (PR#95); preservation proof now Admitted with honest open-goal count after 910 -> 29 reduction (PR#102)"
+updated: 2026-05-20T19:00:00Z
 
 @blockers:
-# No active blockers. Formal proofs FULLY CLOSED (67 Qed, 0 Admitted).
+# Formal proofs NOT fully closed (earlier "FULLY CLOSED (67 Qed, 0 Admitted)"
+# claim was wrong — `coqc` 8.18.0 rejects `Qed.` on preservation).
+#   - formal/Semantics.v `preservation`: Admitted (down from 910 to ~29 open
+#     goals via remember-cfg pattern, PR#102). The prior in-file `Qed.` was
+#     rejected with "Attempt to save an incomplete proof"; the build-oracle
+#     is now source of truth. PR#92 marked it Admitted and reverted PR#87's
+#     propagated "Qed, closed 2026-04-27" claim from ROADMAP+PROOF-NEEDS.
+#   - src/formal/Ephapax/Formal/RegionLinear.idr `regionSafetyExtract` /
+#     `noGCExtract`: vacuous wrappers (body is the input unchanged); ROADMAP
+#     citing them as "regionSafetyTheorem"/"noGCTheorem" complete is
+#     overstated. Honest E3/E4 obligations stated in src/abi/Ephapax/ABI/
+#     Invariants.idr (PR#95-MERGED).
+#   - src/abi/Ephapax/ABI/Invariants.idr E1-E6: E1 (preservation) OWED;
+#     E2 (linear consumption) PARTIAL (head form discharged via
+#     splitLinearCoverage PR#85); E3 (region no-escape) PARTIAL (narrow
+#     form discharged via noEscapeTheorem); E4 (no-runtime-GC) OWED;
+#     E5 (WASM compilation) OWED; E6 (IR lowering) OWED.
+# Estate proof-debt arm: standards#134 (OPEN).
 @end
 @end