Phase 1 scaffold for Lemma B (step_output_context_eq) (#124)

## Summary

This PR introduces the Phase 1 scaffold for `step_output_context_eq`
(Lemma B), which proves that a single step preserves the output context.
The lemma body is stated with a `cfg`-remember pattern and an
atomic-axiom closure tactic, with 31 of 35 step-rule cases remaining as
`admit`.

## Key Changes

- **New lemma `subst_preserves_typing_strong`**: A strengthened variant
of `subst_preserves_typing` that exposes the specific output context
(instead of hiding it behind an existential). This is needed by the 7
β-reduction step cases (`S_Let_Val`, `S_LetLin_Val`, `S_App_Fun`,
`S_If_True/False`, `S_Case_Inl/Inr`) where the existential in the
original lemma blocks output-context equality proofs.

- **`step_output_context_eq` Phase 1 scaffold**: Introduced with the
`cfg`-remember pattern (mirroring `step_R_eq_or_touches_region` and
`preservation`) plus an atomic-axiom closure tactic. This closes 4 of 35
step rules:
- `S_StringNew`, `S_StringConcat`, `S_Drop` (atomic cases with
identity-output typing rules)
- `S_Borrow_Step` (accidental congruence closure: both `T_Borrow` and
`T_Borrow_Val` preserve the input context)

- **Documentation**: Added detailed per-case status map in
`formal/PRESERVATION-HANDOFF.md` clustering the remaining 31 cases into
three groups:
- **Cluster A** (~7): β-reduction cases needing
`subst_preserves_typing_strong`
- **Cluster B** (~18): congruence cases needing
`step_R_eq_or_touches_region` dispatch + IH + recursive Lemma B
- **Cluster C** (~6): region/compound-value cases with mixed closure
requirements

- **Effort revision**: Updated ROADMAP from "3–4 hours" to "8–15 focused
hours" based on empirical baseline from `coqc 8.18.0`.

## Notable Implementation Details

- `subst_preserves_typing_strong` leverages the explicit `remove_at k
Gout` shape already present in `subst_typing_gen`, which collapses to
`G` for `k = 0` via `remove_at 0 ((T, b) :: G) = G`.
- The atomic-axiom closure tactic uses a `repeat match` to force
re-inversion of leaf values (`ELoc`, `EI32`, `EUnit`, `EBool`) to pin
their output contexts to the input.
- Identified circularity risk: some Cluster B cases may need "step
preserves type" before applying the IH, but that lemma is part of
preservation itself.

https://claude.ai/code/session_01USr4ovnvN6SLrwi6z9MUhQ

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

ROADMAP.adoc

@@ -188,6 +188,14 @@ up the proof should follow.
 | After per-case manual closures
 | **12**
 | 10 β-reduction / value-step cases discharged. PR #116.
+
+| Phase 1 scaffold (Lemma B stated, body `Admitted`)
+| 12
+| `step_output_context_eq` introduced. PR #121.
+
+| Phase 1 empirical baseline (2026-05-24)
+| 12 (preservation) / **31 of 35** (Lemma B itself)
+| `cfg`-remember pattern + atomic-axiom tactic on Lemma B closes 4 of its 35 step-rule cases (`S_StringNew`, `S_StringConcat`, `S_Drop`, `S_Borrow_Step`); the remaining 31 cluster across β-reduction / congruence / region-and-compound-value branches. Per-case map in `formal/PRESERVATION-HANDOFF.md`.
 |===
 
 98.7% reduction across one day. Remaining 12 = 11 congruence cases
@@ -218,11 +226,31 @@ via `G' = G_out`.
 **Approach**: induction on `step` with `type_determinacy` per case.
 Same pattern as `step_R_eq_or_touches_region`.
 
-**Effort**: 3–4 hours focused session.
-
-**Risk**: `G_end = G_out` may need weakening to "context-equivalent up
-to flag positions" via the existing `types_agree` machinery. If so,
-the lemma is slightly harder but still tractable.
+**Effort**: ~~3–4 hours focused session~~ → **8–15 focused hours**
+(revised 2026-05-24). Empirical baseline from `coqc 8.18.0`: the
+`cfg`-remember + atomic-axiom tactic closes 4 of 35 step rules
+(`S_StringNew`, `S_StringConcat`, `S_Drop`, `S_Borrow_Step`); the
+remaining 31 split across 3 clusters needing distinct recipes. Full
+per-case map in `formal/PRESERVATION-HANDOFF.md` §"Lemma B per-case
+status".
+
+**Risk**:
+
+. **Type-determinacy across stepped pairs**: some Cluster B
+  congruence cases need to know `e` and `e'` have the same type
+  before applying the IH. `type_determinacy` only handles
+  same-expression pairs; the natural "step preserves type" lemma
+  is part of preservation itself. Watch for circularity when
+  attacking the first congruence case.
+. **Output-context equality may need weakening** to
+  "context-equivalent up to flag positions" via the existing
+  `types_agree` machinery. If so, the lemma is slightly harder
+  but still tractable.
+. **Strengthened subst lemma needed for Cluster A**: the existing
+  `subst_preserves_typing` hides the output context behind an
+  existential; the 7 β-reduction cases need a
+  `subst_preserves_typing_strong` variant exposing the specific
+  `remove_at k Gout` shape already present in `subst_typing_gen`.
 
 === Phase 2 — Apply Lemma B → close 11 congruence cases
 

formal/PRESERVATION-HANDOFF.md

@@ -139,6 +139,98 @@ mechanical 28 are 1–2 days of tactic work.
   estate's "build is the only oracle" policy. The honest mark is one
   `Admitted.` on `preservation`, not 29.
 
+## Lemma B per-case status (2026-05-24)
+
+Empirically verified against `coqc 8.18.0`. The Phase 1 scaffold for
+`step_output_context_eq` now uses the `cfg`-remember pattern that
+mirrors `step_R_eq_or_touches_region` and `preservation`, plus an
+atomic-axiom closure tactic. **4 of 35 step rules close**; 31 remain.
+
+### Closed (4)
+
+| Step rule | Why it closes |
+|-----------|---------------|
+| `S_StringNew` | atomic: `EStringNew → ELoc`, both type to identity-output |
+| `S_StringConcat` | atomic: `EStringConcat (ELoc _) (ELoc _) → ELoc`, all premises invert to identity-output T_Loc |
+| `S_Drop` | atomic: `EDrop (ELoc _) → EUnit`, both T_Drop and T_Unit are identity-output |
+| `S_Borrow_Step` | **accidental congruence closure**: both `T_Borrow` and `T_Borrow_Val` output the input context unchanged, so `Ga = G = Gb` regardless of whether the inner step is reachable. Vacuous-but-closes. |
+
+### Open (31)
+
+Three clusters, ordered by closure tractability:
+
+#### Cluster A — β-reduction (~7)
+
+Need a strengthened `subst_preserves_typing_strong` exposing the
+specific output context (currently hidden behind an existential).
+`subst_typing_gen` already has the `remove_at k Gout` shape — wrap
+it.
+
+| Step rule | Post-step expr (from coqc dump) |
+|-----------|---------------------------------|
+| `S_Let_Val` | `subst 0 v1 e2` |
+| `S_LetLin_Val` | `subst 0 v1 e2` |
+| `S_App_Fun` | `subst 0 v2 ebody` |
+| `S_If_True` | `e0'` (the `e2` branch, abstract) |
+| `S_If_False` | `e0'` (the `e3` branch, abstract) |
+| `S_Case_Inl` | `subst 0 v e1` |
+| `S_Case_Inr` | `subst 0 v e2` |
+
+#### Cluster B — congruence (~18)
+
+Every `S_*_Step` except `S_Borrow_Step`. Recipe per case: apply
+`step_R_eq_or_touches_region` → in the R-equal branch, apply IH for
+the inner step + recursive Lemma B for siblings. RIGHT branch
+(`touches_region`) is blocked on the same region-env weakening
+lemma as preservation Phase 3 — these cases share the bottleneck.
+
+`S_StringConcat_Step1`, `S_StringConcat_Step2`, `S_StringLen_Step`,
+`S_Let_Step`, `S_LetLin_Step`, `S_App_Step1`, `S_App_Step2`,
+`S_If_Step`, `S_Pair_Step1`, `S_Pair_Step2`, `S_Fst_Step`,
+`S_Snd_Step`, `S_Inl_Step`, `S_Inr_Step`, `S_Case_Step`,
+`S_Drop_Step`, `S_Copy_Step`. (17 listed; +1 region congruence
+`S_Region_Step` belongs to cluster C.)
+
+#### Cluster C — region / compound-value (~6)
+
+| Step rule | What's needed |
+|-----------|---------------|
+| `S_Region_Enter` | `T_Region` ↔ `T_Region_Active` dispatch via `In r R`; needs `output_ctx_det` sub-lemma on `e_inner` |
+| `S_Region_Exit` | needs `region_shrink_preserves_typing` (already Qed) + value-output-context invariance |
+| `S_Region_Step` | **blocked on Phase 3** — region-env weakening for non-values |
+| `S_StringLen` (atomic!) | inversion of `T_StringLen` → `T_Borrow_Val` → `T_Loc` chain needs explicit nested invocation; my repeat-match doesn't cover the `EBorrow (ELoc _ _)` shape |
+| `S_Copy` | atomic but compound: `T_Copy` outputs `G'` where `G'` is value-input; needs `value_context_unchanged` invocation |
+| `S_Fst` / `S_Snd` | atomic but inversion of `T_Pair` premise needs `value_context_unchanged` to align inner v1/v2 typings |
+
+### Effort revision
+
+The ROADMAP's "3-4 hours focused session" estimate for Phase 1 was
+optimistic. Empirical evidence:
+
+- 4 trivial cases closed by a uniform tactic in ~30 minutes.
+- Each of the remaining 31 needs a hand-rolled per-case tactic block.
+- Cluster A (7) needs one shared sub-lemma first
+  (`subst_preserves_typing_strong`).
+- Cluster B (17–18) shares the same recipe but each case names
+  different premises and constructor arguments — call it ~10 minutes
+  per case once the recipe is debugged on the first one.
+- Cluster C (6) is a mixed bag; `S_Region_Step` carries Phase 3 risk.
+
+**Revised estimate**: **8–15 focused hours** for Lemma B alone,
+assuming no circularity surprises with `type_determinacy` across
+stepped pairs. Phase 2 (apply Lemma B to preservation's congruence
+cases) remains ~2 hours of mechanical wiring once Lemma B is closed.
+
+### Watch for: circularity risk
+
+Some Cluster B cases require knowing that `e` and `e'` have the
+same type before applying the IH. `type_determinacy` operates on
+same-expression pairs, not stepped pairs. The natural lemma —
+"step preserves type" — is part of what preservation itself
+proves. If the inductive structure of Lemma B turns out to need
+preservation as a sub-lemma, the closure path needs revision.
+Watch for this when attacking the first Cluster B case.
+
 ## Unwind checklist (when finally closed)
 
 1. Replace `Admitted.` with `Qed.`

formal/Semantics.v

@@ -2826,6 +2826,34 @@ Proof.
   - reflexivity.
 Qed.
 
+(** Strengthened variant that exposes the specific output context
+    (instead of an existential). Used by [step_output_context_eq]
+    (Lemma B, Phase 1) to discharge the beta-reduction step cases
+    where the existential in [subst_preserves_typing] blocks the
+    output-context equality proof.
+
+    Both the witness ([G_v = G]) and the specific output context
+    ([G']) come from [subst_typing_gen]'s explicit
+    [remove_at k Gout] shape, which collapses for [k = 0] via
+    [remove_at 0 ((T, b) :: G) = G]. *)
+Lemma subst_preserves_typing_strong :
+  forall R G e T2 G' T1 v G_v,
+    R; (T1, false) :: G |- e : T2 -| (T1, true) :: G' ->
+    R; G |- v : T1 -| G_v ->
+    is_value v ->
+    G_v = G /\ R; G |- subst 0 v e : T2 -| G'.
+Proof.
+  intros R G e T2 G' T1 v G_v Htype Hv Hval.
+  assert (HGv: G_v = G) by (eapply value_context_unchanged; eassumption).
+  split; [exact HGv|].
+  subst G_v.
+  assert (Hlin: is_linear_ty T1 = true).
+  { eapply (flag_false_to_true_implies_linear _ _ _ _ _ 0 T1 Htype); simpl; reflexivity. }
+  pose proof (subst_typing_gen _ _ _ _ _ Htype 0 T1 v false eq_refl Hval Hlin Hv true eq_refl) as Hsubst.
+  simpl in Hsubst.
+  exact Hsubst.
+Qed.
+
 (** Helper: types_agree and false_preserved are reflexive *)
 Lemma ctx_types_agree_refl : forall G, ctx_types_agree G G.
 Proof.
@@ -3318,13 +3346,68 @@ Lemma step_output_context_eq :
       R'; G |- e' : T -| G_b ->
       G_a = G_b.
 Proof.
+  (* Phase 1 scaffold (PR #121) + cfg-remember pattern + atomic-axiom
+     closure. cfg-remember mirrors [step_R_eq_or_touches_region] and
+     [preservation] (PRs #102 / #106): substitutes the outer
+     expression slots into each induction case so per-case inversion
+     sees concrete syntax. *)
   intros mu R e mu' R' e' Hstep.
-  induction Hstep; intros G0 T0 Ga Gb Htype_e Htype_e'.
-  (* Attempt: aggressive inversion + auto on each case. The hope is
-     that for the syntax-directed typing relation, inversion of both
-     typings extracts component typings with matching output
-     contexts, which `eauto` then unifies. *)
-  all: try (inversion Htype_e; inversion Htype_e'; subst; auto).
+  remember (mu, R, e) as cfg eqn:Hcfg.
+  remember (mu', R', e') as cfg' eqn:Hcfg'.
+  revert mu R e mu' R' e' Hcfg Hcfg'.
+  induction Hstep;
+    intros mu0 R0 e0 mu0' R0' e0' Hcfg Hcfg';
+    inversion Hcfg; subst;
+    inversion Hcfg'; subst;
+    intros G0 T0 Ga Gb Htype_e Htype_e'.
+  (* Atomic-axiom + accidental-congruence cases that close by full
+     inversion of both typings + leaf-value re-inversion +
+     reflexivity. Empirically (coqc 8.18.0) closes 4 of 35 step
+     rules:
+       S_StringNew    ([EStringNew r s]   -> [ELoc l r])
+       S_StringConcat ([EStringConcat (ELoc _ _) (ELoc _ _)]
+                                           -> [ELoc l' r])
+       S_Drop         ([EDrop (ELoc _ _)] -> [EUnit])
+       S_Borrow_Step  ([EBorrow e]        -> [EBorrow e'])
+         (closes accidentally: both T_Borrow and T_Borrow_Val output
+         the input context unchanged, so Ga = G = Gb regardless of
+         the inner step's IH.)
+     The leaf re-inversion forces inner [has_type _ _ (ELoc _ _) _ _]
+     and friends to pin their output to the input (T_Loc /
+     T_StringNew / T_I32 / T_Unit all preserve the linearity
+     context). *)
+  all: try (
+    inversion Htype_e; subst;
+    inversion Htype_e'; subst;
+    repeat match goal with
+    | [ H : has_type _ _ (ELoc _ _) _ _ |- _ ] =>
+        inversion H; subst; clear H
+    | [ H : has_type _ _ (EI32 _) _ _ |- _ ] =>
+        inversion H; subst; clear H
+    | [ H : has_type _ _ EUnit _ _ |- _ ] =>
+        inversion H; subst; clear H
+    | [ H : has_type _ _ (EBool _) _ _ |- _ ] =>
+        inversion H; subst; clear H
+    end;
+    reflexivity).
+  (* 31 cases remain. Per-case map: PRESERVATION-HANDOFF.md
+     section "Lemma B per-case status". Three clusters:
+       - beta-reduction (~7): S_Let_Val, S_LetLin_Val, S_App_Fun,
+         S_If_True/False, S_Case_Inl/Inr. Need a strengthened
+         subst-output-context lemma (subst_typing_gen already has
+         the [remove_at k Gout] shape; subst_preserves_typing hides
+         it behind an existential).
+       - congruence (~18, every S_*_Step except S_Borrow_Step):
+         apply [step_R_eq_or_touches_region] to dispatch [R = R'];
+         in the R-eq branch, apply IH for the inner step + recursive
+         Lemma B for siblings. RIGHT branch (touches_region) is
+         blocked on the same region-env weakening lemma as
+         preservation Phase 3.
+       - region / compound-value (~6): S_Region_Enter/Exit/Step,
+         S_StringLen (atomic, blocked on TBorrow/EStringLen
+         inversion shape — does NOT close trivially despite being
+         atomic), S_Copy, S_Fst, S_Snd. S_Region_Step blocks on
+         Phase 3. *)
   all: admit.
 Admitted.