fix(coq): preservation 29 → 22 open goals via universal-IH + atomic closers

[hyperpolymath]

Summary

Builds on PR #102 (910 → 29 reduction). Closes 7 more residuals via two structural fixes.

State	Open goals
Pre-#102	910
Post-#102	29
This PR	22

1. Universal-IH revert (closes 6 congruence-case goals)

PR #102's remember (mu, R, e) as cfg discharged cross-cases but left congruence-case IHs unusable — they inherited the OUTER cfg equation:

IHHstep : (mu_inner, R_inner, e_inner) = (mu, R, EOuter ...) -> ...

which is inconsistent in general (the inner expression is not the outer compound). Fix: revert mu R e mu' R' e' Hcfg Hcfg' before induction Hstep. Each case's IH now carries clean universal quantification:

IHHstep : forall mu R e mu' R' e',
            (?mu_in, ?R_in, ?e_in) = (mu, R, e) ->
            (?mu_out, ?R_out, ?e_out) = (mu', R', e') ->
            forall G T G', R; G |- e : T -| G' ->
                           exists G_out, R'; G |- e' : T -| G_out

The 6 congruence cases closed by this are the ones whose sibling typing premises don't need region/context bridging.

2. Per-class closing tactics (closes 1 axiom-case goal)

The new T_Loc inversion tactic handles S_StringConcat's "type mismatch: result is ELoc l' r but goal asks TString r0" — inverting the sibling ELoc l1 r typing yields r0 = r, then T_Loc applies.

Added 5 more atomic closers (T_StringNew, T_I32, T_Unit, T_Pair, subst_preserves_typing) — these are pre-emptive for cases the existing chain may not have hit, but empirically contributed 0 closures in this PR's diff.

Remaining 22 goals

All need additional metatheoretic lemmas:

1. Sibling typing under post-step region: for S_X_Step1 congruence cases, the unstepped sibling expression is typed under R but the reconstructed compound needs it under R'. Needs a "step preserves R unless inner expression is region-touching" lemma + a region-invariance application.

2. Context bridging: same congruence cases also need the sibling's typing context (G') to bridge to the new context (G_inner from IH). Needs a "step preserves linearity tracking on siblings" lemma — substantial.

3. EBorrow inversion for S_StringLen_Step: typing premise wraps EBorrow e, not e directly; needs an extra inversion step before IH application.

4. S_Region_Step + T_Region_Active: the documented language-design blocker — needs a region-env weakening lemma for non-values (~50–150 LOC by itself).

Per formal/PRESERVATION-HANDOFF.md these are 1–2 days of tactic work plus the region-weakening lemma. The Admitted. stays on preservation; supporting lemmas already Qed.

Verification

$ coqc -Q . Ephapax Semantics.v
(builds clean, Admitted at the 22-goal residue)

$ # Empirical count via Show Existentials:
$ # (insert before Admitted, rebuild, grep '^Existential ')
22

Refs

• standards#124 (proof-debt audit epic)
• ephapax#102 (910 → 29 reduction)
• ephapax#104 (PROOF STATUS docs correction)

Test plan

• coqc -Q . Ephapax Semantics.v builds clean
• Show Existentials. before Admitted reports 22 (down from 29 on main)
• No new Qed.-proven lemmas added; no proof-engineering shortcuts via assert / admit
• CI green

🤖 Generated with Claude Code