hyperpolymath
diff --git a/‎.machine_readable/6a2/STATE.a2ml‎
Lines changed: 60 additions & 39 deletions b/‎.machine_readable/6a2/STATE.a2ml‎
Lines changed: 60 additions & 39 deletions
diff --git a/‎CLAUDE.md‎
Lines changed: 137 additions & 0 deletions b/‎CLAUDE.md‎
Lines changed: 137 additions & 0 deletions
@@ -6,51 +6,72 @@
 
 @state(version="2.0"):
 phase: "implementation"
-next_action: "Discharge ~8 per-goal cases in step_preserves_type_at_pre + ~11 in step_output_context_eq_at_pre (port from upstream's per-goal sections, ~2-3h each). Then re-attack preservation's 12 cascading goals using step_preserves_type + step_output_context_eq as oracles (~4-8h, may need region-env weakening for non-values)."
-last_action: "Path 3 (at-pre helper) landed 2026-05-26 eve. step_preserves_type AND step_output_context_eq both now Qed (was Admitted with 1 shared admit each at S_Region_Step r=r1 cross-case). Two new helper lemmas introduced (Admitted with most cases auto-closed by verbatim block copy). 4 proof commits + 1 doc commit pushed to lemma-b-phase2 (ephapax#146)."
-updated: 2026-05-26T19:00:00Z
+next_action: "Layered preservation work, NOT legacy patching. Per owner directive 2026-05-27 (see CLAUDE.md): do not attempt to close Theorem preservation in formal/Semantics.v (provably false via Counterexample.v); do not extend Semantics.v with closure-support lemmas (step_preserves_type_at_pre and similar are all in this anti-pattern class); do not close residual Semantics_L1.v axioms via ad-hoc proof tricks. Affirmative work: per-layer preservation derivation against the four-layer redesign in formal/PRESERVATION-DESIGN.md. L2 modality landed in-place (PRs #176 + #177); 6 L1 supporting lemmas regressed to Admitted post-L2-hybrid — bullet-rewrite needed for the 3 new Affine-only constructors of has_type_l1 in Semantics_L1.v."
+last_action: "Doc lockdown landed on main (PR TBD): CLAUDE.md adds owner-directive §, PRESERVATION-DESIGN.md + PRESERVATION-HANDOFF.md gain banners, ROADMAP.adoc §preservation-closure-plan obsoleted, this STATE.a2ml updated. The lockdown originated on the proof/l1-region-threading-design branch (PR #175 against that branch); replayed to main because the design branch is DIRTY+superseded by the L2 hybrid path (#176+#177). PR #153 to be closed as superseded."
+updated: 2026-05-27T11:30:00Z
+
+@directive(source="owner", date="2026-05-27", canonical="CLAUDE.md"):
+# Captured durable directive — preservation work is the four-layer redesign,
+# NOT closure of the legacy theorem. Pre-discovery patching paths are
+# closed.
+#
+# DO NOT:
+#   - close `Theorem preservation` in formal/Semantics.v (provably false)
+#   - extend Semantics.v with closure-support lemmas (Lemma B variants,
+#     step_preserves_type_at_pre, step_output_context_eq_at_pre,
+#     region_add_typing_for_non_values, strengthened subst variants)
+#   - close residual Semantics_L1.v axioms via proof tricks
+#   - follow any pre-2026-05-26 "preservation closure plan"
+#   - patch the legacy Typing.v judgment
+#
+# DO:
+#   - read formal/PRESERVATION-DESIGN.md first
+#   - work per-layer: preservation_l1, preservation_l2, etc.
+#   - escalate before patching when a side-condition is needed
+#
+# Anti-pattern detector: sibling-region-disjointness side conditions,
+# region-weakening predicates indexed on syntactic shape, admit-shuffling
+# between Semantics.v and a new lemma. Any of these → escalate.
+#
+# Companion memory: feedback_ephapax_no_patching_legacy_preservation.md
+@end
 
 @blockers:
-# Formal proofs NOT fully closed; current shape (verified by coqc 8.18 on
-# 2026-05-26 eve):
-#   - formal/Semantics.v `step_preserves_type` (line 4355): Qed ✓
-#   - formal/Semantics.v `step_output_context_eq` aka Lemma B: Qed ✓
-#   - formal/Semantics.v `step_preserves_type_at_pre` (NEW, line ~3625):
-#     Admitted with `all: admit.` catch-all. 27 of 35 cases closed via
-#     verbatim copy of step_preserves_type's tactic blocks (Cluster A+B).
-#     8 per-goal cases remaining: S_StringConcat_Step2, S_Let_Step,
-#     S_LetLin_Step, S_App_Step2, S_If_Step, S_Pair_Step1, S_Pair_Step2,
-#     S_Case_Step.
-#   - formal/Semantics.v `step_output_context_eq_at_pre` (NEW, line ~5698):
-#     Admitted with `all: admit.` catch-all. ~24-27 of 35 cases closed via
-#     verbatim copy. S_Region_Step block deliberately excluded (would
-#     self-reference). ~11 cases remaining.
-#   - formal/Semantics.v `preservation`: 12 cascading goals — SEPARATE
-#     structural problem (region-env weakening for non-values), NOT the
-#     shared admit closed by Path 3.
+# Layered work in progress; legacy preservation deliberately not addressed.
 #
-# Path 3 (at-pre helper) lands. Path 1 (mutual induction) and Path 2
-# (structural recursion via expr_free_of_region) both AVOIDED — Path 2
-# was blocked by counterexample, Path 1 would have been heavier refactor.
-# Path 3 wins by sidestepping the cross-case via shared-env framing.
+# Current state (verified by coqc 8.18 on main, post-#176/#177):
+#   - formal/Semantics.v `preservation`: Admitted — PROVABLY FALSE per
+#     Counterexample.v (three Qed lemmas). NOT to be closed.
+#   - formal/Semantics.v `step_preserves_type`, `step_output_context_eq`,
+#     and their at_pre helpers are Qed but support legacy-preservation
+#     closure attempts that are now ruled out. Retained for diagnostic
+#     value; no new lemmas in this class.
+#   - formal/Semantics_L1.v `preservation_l1`: in progress; 6 supporting
+#     lemmas regressed to Admitted post-L2-hybrid (PRs #176+#177).
+#     Bullet-structure rewrite needed for 3 new Affine-only constructors.
+#   - formal/TypingL1.v: now m-indexed (`has_type_l1 m R G e T R' G'`),
+#     `linear_to_affine` Qed zero axioms.
+#   - formal/Echo.v: K-free scaffold, no postulates, forward-looking
+#     (not yet wired into has_type_l1).
+#   - formal/Modality.v: thin-poset Linear ≤ Affine, all Qed.
 #
-# Other proof-debt items (out of standards#134 scope):
-#   - 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.
-#   - 30 unsafe Rust blocks (was 49); concentrated in
-#     src/ephapax-runtime/src/{lib,list}.rs and src/ephapax-interp/src/lib.rs.
-#     Per-block contract audit out of scope for standards#134.
-# Estate proof-debt arm: standards#134 (OPEN; 4/5 sub-tasks DONE pre-2026-05-26).
+# Other proof-debt items (out of preservation scope):
+#   - src/abi/Ephapax/ABI/Invariants.idr E1-E6: E1 (preservation) OWED at
+#     the Idris2 layer too; E2/E3 PARTIAL; E4/E5/E6 OWED.
+#   - 30 unsafe Rust blocks; per-block contract audit out of scope.
 @end
 
 @artifacts:
-# Doc-only commits parked on `lemma-b-phase2` (PR ephapax#146):
-#   032e8ea - audit reconciliation (docs/reports/audit/audit-2026-05-26-standards-134-reconciliation.md)
-#   83e1e31 - handoff case-count correction (formal/PRESERVATION-HANDOFF.md)
-#   36ff88e - Option 2 obstacle + Path 1 pivot (docs/reports/audit/audit-2026-05-26-lemma-b-option-2-obstacle.md)
-# Plus this STATE update + session note (docs/sessions/SESSION-2026-05-26-lemma-b-pivot.adoc).
+# Layered files on main (post-L2-hybrid):
+#   formal/Counterexample.v   — 3 Qed lemmas; preservation FALSE
+#   formal/Echo.v             — L3 scaffold, K-free
+#   formal/Modality.v         — L2 thin poset, all Qed
+#   formal/TypingL1.v         — m-indexed has_type_l1 (post-#176)
+#   formal/Semantics_L1.v     — in progress; 6 supporting Admitted
+# Doc lockdown:
+#   CLAUDE.md                       — owner directive §
+#   formal/PRESERVATION-DESIGN.md   — CANONICAL banner
+#   formal/PRESERVATION-HANDOFF.md  — ARCHAEOLOGY ONLY banner
+#   ROADMAP.adoc                    — closure-plan section removed
 @end
 @end
@@ -68,3 +68,140 @@ Most questions touch exactly one layer. The design rationale is in `formal/PRESE
 - The legacy preservation closure plan is superseded by `formal/PRESERVATION-DESIGN.md` (four-layer redesign). `formal/PRESERVATION-HANDOFF.md` carries the historical diagnostic record only.
 - Ephapax-affine type proofs are **NOT** done — `formal/` mechanises a single legacy judgment + L1's `has_type_l1`; there is no separate mechanised ephapax-affine until L2 + the Linear ⇒ Affine weakening lemma land. See `PRESERVATION-DESIGN.md §12.15`.
 - All commits GPG-signed (key `4A03639C1EB1F86C7F0C97A91835A14A2867091E`), email `6759885+hyperpolymath@users.noreply.github.com`. Auto-merge ON for every PR.
+
+---
+
+## 🛑 Owner directive 2026-05-27 — preservation work
+
+> Read this before touching anything in `formal/`. Several Claude sessions
+> burned hours walking the pre-discovery patching path. This block
+> exists so that doesn't happen again.
+
+### TL;DR
+
+Ephapax preservation as originally stated in `formal/Semantics.v` is
+**provably false**. `formal/Counterexample.v` exhibits a concrete
+configuration that types, steps, and lands at an untypable post-state
+— all three lemmas `Qed`. The work is therefore **not** to close
+`Theorem preservation` in `Semantics.v`. The work is the **four-layer
+principled redesign** (L1 region capabilities / L2 modality (now
+`m`-indexed into `has_type_l1`) / L3 echo / L4 dyadic mode) documented
+in `formal/PRESERVATION-DESIGN.md`. Preservation is **re-derived** in
+the new architecture from explicit invariants, not forced through
+the old one.
+
+### DO NOT
+
+These are anti-patterns that have wasted real session time. Refuse
+them if asked; if asked anyway, push back and link this section.
+
+1. **DO NOT close `Theorem preservation` in `formal/Semantics.v`.**
+   It is FALSE. No proof technique closes it because no proof
+   exists. The `Admitted.` is correct.
+
+2. **DO NOT extend `formal/Semantics.v`** with new lemmas aimed at
+   closing the legacy preservation: not Lemma B variants
+   (`sibling_typing_transfers_across_step` /
+   `step_output_context_eq` / `step_preserves_type_at_pre` /
+   `step_output_context_eq_at_pre` were earlier attempts in this
+   class), not `region_add_typing_for_non_values`, not strengthened
+   substitution lemmas. The legacy judgment lacks the structural
+   invariant the counterexample demands; no lemma collection bolted
+   onto it will help.
+
+3. **DO NOT close any residual axiom in `formal/Semantics_L1.v`
+   (e.g. `region_liveness_at_split_l1` if it returns) by adding
+   proof tricks, side-conditions discharged ad-hoc, or strengthened
+   lemma signatures within the current judgment shape.** This is
+   *the same kind of patching that produced the legacy admits*, one
+   layer up. The post-L2-hybrid main carries the `Modality`
+   parameter directly in `has_type_l1`; closures that previously
+   looked like "an L1 fix" are now cross-layer and must be
+   reasoned-about at the layered level.
+
+4. **DO NOT follow the "Preservation closure plan" steps in
+   historical PRs / branches / comments.** Anything dated before
+   2026-05-26 (the counterexample landing) that proposes closing
+   `preservation` to `Qed.` is pre-discovery. PRs #92, #102, #104,
+   #106, #114, #116, #117, #121, #146 are part of the historical
+   reduction-from-910-goals record; treat them as archaeology, not
+   instructions.
+
+5. **DO NOT patch the legacy `Typing.v` judgment.** It is the
+   pre-redesign judgment. `Counterexample.v` depends on its
+   falsity for the regression theorem. Leave it.
+
+### DO
+
+1. **DO read `formal/PRESERVATION-DESIGN.md` first.** It is the
+   canonical design source. The four-layer architecture, the
+   missing-invariant statement, and the per-layer plan are all
+   there.
+
+2. **DO continue the layered build:**
+   - L1 (`TypingL1.v` + `Semantics_L1.v`): R-threading + modality
+     parameter (post-L2-hybrid). Residual admits are L1 design
+     follow-ups, not legacy patching.
+   - L2: modality landed in-place via PRs #176 + #177
+     (`has_type_l1` now carries `m : Modality`;
+     `linear_to_affine` Qed with zero axioms). 6 L1 supporting
+     lemmas in `Semantics_L1.v` regressed to Admitted post-L2 —
+     bullet-structure rewrite needed for the 3 new Affine-only
+     constructors.
+   - L3 (`Echo.v`): K-free, forward-looking. Not wired into L1/L2
+     judgments yet — that's L1 ⇒ L3 follow-up.
+   - L4: not started; design in §7 of the design doc.
+
+3. **DO derive preservation per-layer.** `preservation_l1` is
+   proved in the L1 vocabulary, against the L1 judgment, using L1
+   invariants. The same shape for L2 / L3 / L4 as each lands.
+
+4. **DO escalate before patching.** If a proof attempt requires
+   adding a side-condition to fix a sibling-region-disjointness
+   issue (or analogous cross-rule constraint), that is the signal
+   to escalate to a layer-design discussion — the architecture is
+   asking for a new invariant, not a clever lemma.
+
+### Anti-pattern detector
+
+If your session is producing any of the following, stop and
+escalate to the owner:
+
+- `sibling-region-disjointness` side conditions on compound rules,
+- region-weakening predicates indexed on syntactic shape,
+- admit-shuffling between `Semantics.v` and a new lemma,
+- "the previous-PR-line-of-attack just needs one more lemma,"
+- proposing to close `Theorem preservation` in `Semantics.v` to
+  `Qed.` by any chain of reasoning,
+- adding new `Axiom` declarations to discharge L1/L2 gaps.
+
+### If you're unsure
+
+Two questions to ask before touching `formal/`:
+
+1. **Am I about to add an `Admitted` or `Axiom` to close a gap in
+   the old judgment?** If yes — stop. The old judgment is provably
+   incomplete; the right answer is to encode the missing invariant
+   in a new layer, not to admit it.
+
+2. **Am I about to close an L1/L2/L3 admit by reasoning that
+   crosses layers?** If yes — check `PRESERVATION-DESIGN.md` for
+   the cross-layer dependency annotations. The layered design
+   intentionally splits some closures across layers; trying to
+   close them within one layer alone is the trap.
+
+If unsure: ask the owner before writing code. Pause to escalate
+costs less than a 4-hour patching session.
+
+### Memory hooks
+
+If you have access to the user's auto-memory store, relevant
+entries include:
+
+- `feedback_ephapax_no_patching_legacy_preservation.md` — the
+  durable directive captured 2026-05-27 (this section).
+- `project_ephapax_four_layer_redesign.md` — current project state.
+- `project_ephapax_l2_modality_landed.md` — L2 hybrid landing
+  (PRs #176 + #177).
+- `feedback_ephapax_affine_proofs_not_done.md` — what counts as
+  "done" for the ephapax-affine half.