== Proof needs — Ephapax (linear + affine sublanguages)

____
=== 🛑 First-read disambiguation (human + machine readers)

*This document is for `+hyperpolymath/ephapax+`.* Ephapax is a research
language for compile-time WebAssembly memory safety with formal artifacts
in Coq and Idris2. Current Coq counterexamples refute legacy and
unrestricted L1 preservation; no unconditional L2 theorem or
implementation-refinement proof is established.

*Ephapax is NOT `+hyperpolymath/affinescript+`.* AffineScript is a
separate, unrelated language (JS/TS/AffineScript successor, OCaml +
AffineScript runtime, no mechanised proofs, no first-class regions). The
two share only the compile target (`+hyperpolymath/typed-wasm+`).

*`+ephapax-affine+` (in this document) is the affine _sublanguage_ of
Ephapax* — the versatile prototyping companion to `+ephapax-linear+`. It
lives inside this repo (`+ephapax-linear/+` crate). *It is NOT
AffineScript.* The lexical overlap of the word `+affine+` is a
coincidence of substructural-logic terminology, not a project
relationship. Do not apply lessons or tactics across the boundary.

If you found this document by searching for "`affine type system`",
verify which language you actually need before proceeding. Canonical
side-by-side table:
https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md
____

=== Reading guide

This file is the proof-status audit for Ephapax. It supersedes earlier
versions that treated the legacy preservation closure plan as viable.
Keep these categories distinct:

* *Legacy archaeology*: the original `+preservation+` statement is false;
  its durable `+Admitted.+` and pinned five-`+Qed+` regression in
  `+formal/Counterexample.v+` are intentional and must remain together.
* *Redesigned judgments*: L1/L2 change typing interfaces; conceptual
  vocabulary or results from another repo do not discharge Ephapax's
  language-soundness obligations.
* *Proved regressions*: counterexamples and positive controls are
  machine-checked evidence about exact statements, not general preservation
  theorems.
* *Genuinely open obligations*: only unrefuted statements belong here. A
  refuted theorem requires an explicit redesign or restricted replacement,
  not an attempt to prove the old claim.

The current preservation boundary is:

[cols="18%,26%,56%",options="header"]
|===
|Layer |Status |Evidence / boundary
|Legacy |*False as stated; pinned archaeology* |`+Counterexample.v+` has
5 `+Qed+` lemmas. Keep the one durable `+Admitted.+` in
`+Semantics.v+`; do not relabel it ordinary debt or replace it with a fake
proof.
|L1 |*Current universal statement false as stated* |`+Counterexample_StepPop.v+`
refutes `+step_pop_disjoint_from_type_l1+`; `+Counterexample_PreservationL1.v+`
refutes the modality-polymorphic `+preservation_l1+` via its Linear
instance (the pre-state witness types in both modes). It does not by itself
refute a separate Affine-only theorem. The existing
`+bad_input_untypable_l1+` only rejects the original legacy witness; it does
not establish L1 preservation.
|L2 |*No unconditional theorem established* |`+preservation_l2+` is not
declared as a theorem in the current tree. `+Counterexample_L2.v+` and
`+Counterexample_L2_nested.v+` witness distinct β-preservation gaps. The
Qed β-case lemmas in `+TypingL2.v+` are conditional and do not assert the
refuted unrestricted claim.
|Replacement work |*Open design obligation* |Specify sound judgments /
side conditions and state exact replacement preservation theorems. These
are new obligations; the refuted legacy and L1 statements remain pinned.
|===

==== Estate proofing policy and Grade 3 target

Follow the estate's canonical references for proof method and grade:

* link:https://github.com/hyperpolymath/mathesis/blob/main/estate-mathematical-architecture[`hyperpolymath/mathesis/estate-mathematical-architecture`]
  defines Grade 3 as an Agda proof that type-checks locally and has not been
  independently translated. Grade 2/1 claims require their separate
  translation/API evidence.
* link:https://github.com/hyperpolymath/standards/blob/main/3-practice/PROOF-POLICY.adoc[`hyperpolymath/standards/3-practice/PROOF-POLICY.adoc`]
  assigns implementation-specific engineering obligations to Idris2 and
  implementation-independent theory to Agda, rechecked in Rocq and Lean.
  Its deciding test is whether a claim names a repository-specific type,
  function, or wire format. The
  link:https://github.com/hyperpolymath/standards/blob/main/docs/README-EXPLAINME-STANDARD.adoc[proof-ledger standard]
  also requires every claimed proof (including open/refuted claims) to
  appear in `+EXPLAINME.adoc+` with status, checker, location, and trust
  boundary.

*Grade 3 is the requested target, not a status to apply retroactively.* The
current regression witnesses are Coq scripts (`+Qed+`), so they are not
Mathesis Grade 3 receipts. The Ephapax-specific `+has_type_l1+`/`+step+`
claims also appear engineering-specific under the current standards mapping;
that mapping does not automatically make them Agda theory. Until an
owner-approved formulation resolves this boundary, record current Coq
results as Coq evidence, retain `+COUNTEREXAMPLE+` for refuted statements,
and do not label them Grade 3. A future Agda Grade 3 receipt must include
the exact proposition, assumptions, source commit, pinned Agda/toolchain,
canonical invocation, and evidence that it is the same Ephapax statement;
it must not be inferred from shared vocabulary or another repository's
proof. No Grade 2/1 claim is made here.

The audit is split by sublanguage:

* *§1* — what’s done (mechanised, Qed) for each sublanguage.
* *§2* — what’s todo (active work, by layer).
* *§3* — what’s banned (explicit do-not-do anti-patterns).
* *§4* — counts and file-by-file map.

For the architectural background see link:STATUS.adoc[`+STATUS.adoc+`]
and
link:formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc+`].

'''''

=== §1. What’s done

==== ephapax-linear (strict / obligation-preserving sublanguage)

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Component |File |Status
|L1 judgment (`+has_type_l1+`) |`+formal/TypingL1.v+` |100% — 0 admits,
2 Qed

|L1 judgment indexed by modality `+m : Modality+` |`+formal/TypingL1.v+`
|landed via PRs #176 + #177

|L2 modality core (`+Modality.v+`, `+linear_to_affine+`)
|`+formal/Modality.v+` |1 Qed, zero axioms

|L3 calculus (echo / residue fiber + degrade + no-section proof)
|`+formal/Echo.v+` |12 Qed, 0 admits

|Linear-mode forward progress lemmas |`+formal/Semantics_L1.v+` |37 Qed;
*2* outer `+Admitted.+` markers (`+step_pop_disjoint_from_type_l1+` /
`+preservation_l1+`) cover *2* internal `+admit.+` cases at current
lines 3315/3336 (rebuilt `+coqc 8.18.0+` ground truth 2026-06-27; the
earlier 5-internal / lines-576/646/1994/2014/3132 figure is
pre-dissolution, superseded by the §4 marker = 3 total). Phase 3b Stage
1a (#252, MERGED 2026-05-30: `+tfuneff_lambda_free+` +
`+Counterexample_L2_nested.v+`) and Stage 1b (#253, MERGED 2026-05-31:
closed-value substitution + `+preservation_l2_app_eff_beta+` β-case for
TFunEff). Slice 4 L3 wiring delivered
`+preservation_l3_region_active_echo+` / `+preservation_l3_drop_echo+` /
`+preservation_l3+` umbrella.

|L2 β-case lemmas (Stage 1b) |`+formal/TypingL2.v+` |10 Qed total:
`+weaken_modality+` family (5), `+preservation_l2_via_l1+` (conditional
on `+preservation_l1+`), `+linear_value_retype_l1_m+`, and 3
`+preservation_l2_app_eff_beta_*+` variants (Linear / ground_nonlinear /
TFunEff conditional on their listed side conditions). The separate L2
counterexamples below show why these restrictions matter; planned Stages
2/3/4 are not evidence that the unrestricted theorem has been proved, and
no unconditional `+preservation_l2+` is present in this tree.

|L4 labelling scaffold (Phase A, 2026-05-28) |`+formal/L4.v+`
|`+ProgramMode+` enum (`+PModeLinear+` / `+PModeAffine+` /
`+PModeBoundaryMix+`) + `+program_mode_to_modality+` round-trip.
Definitions only — no theorems, zero axioms.

|Counterexample_L2 regression witnesses (Phase 4c + 3b)
|`+formal/Counterexample_L2.v+`, `+formal/Counterexample_L2_nested.v+`
|5 + 5 Qed pinning the Phase 4c (fresh-region scope crossing) and Phase
3b (nested TFunEff) soundness-gap classes

|Pinned legacy counterexample + L1 positive regression
|`+formal/Counterexample.v+` |5 Qed in total: three lemmas establish the
legacy counterexample; `+t_loc_l1_R_preserving+` supports the L1 argument;
`+bad_input_untypable_l1+` rejects this one input in both modes. This is
not a proof of L1 preservation.

|Operational checker (Rust, ephapax-linear sublanguage)
|`+ephapax-linear/src/linear.rs+` |working — discharges resource-exact
obligation
|===

==== ephapax-affine (relaxed / degradable sublanguage)

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Component |File |Status
|Affine-mode judgment indexing |`+formal/TypingL1.v+` (`+m = Affine+`
branch) |landed; 3 Affine-only rules `+T_Lam_L1_Affine+`,
`+T_Case_L1_Affine+`, `+T_If_L1_Affine+`

|Linear ⇒ Affine weakening |`+formal/TypingL1.v+` `+linear_to_affine+`
|Qed, zero axioms

|Operational checker (Rust, ephapax-affine sublanguage)
|`+ephapax-linear/src/affine.rs+` |working — permits weakening /
graceful abandonment

|Affine-mode echo discipline (LEcho Affine = lowered triple)
|`+formal/Echo.v+` (calculus) |calculus done; rule wiring pending

|L1/L2 conditional helper infrastructure |`+formal/Semantics_L1.v+` and `+formal/TypingL2.v+`
|Stage 3b and β-case helpers landed with explicit premises; they are not
unconditional preservation theorems. The unrestricted region-shrink helper
and former region-liveness lemma were refuted and removed; the restricted
`+region_shrink_msperm+`/value/neutral results are Qed. Two outer L1
`+Admitted+` markers remain, and both unrestricted statements are now
refuted by pinned counterexamples (see §1 boundary and §4 seam audit).
|===

==== Counterexample regression

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Lemma |Status |What it shows
|`+bad_input_untypable_l1+` |Qed |the configuration that
steps-and-untypes is rejected at type check under the new L1 judgment,
in both Linear and Affine modes

|4 supporting lemmas |Qed |the legacy judgment _types_ the same
configuration
|===

→ The L1 judgment rejects the *specific legacy input*. The later
`+Counterexample_PreservationL1.v+` shows that this local regression does
not make the current L1 preservation theorem sound.

'''''

=== §2. What’s todo

==== L1/L2 preservation boundary (historical lemmas vs. open redesign)

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Item |File |Estimate
|✅ Close 3 pure bullet-structure regressions
(typing_preserves_bindings_l1, unrestricted_flag_unchanged_l1,
shift_typing_gen_l1) |`+formal/Semantics_L1.v+` |done 2026-05-27

|✅ Generalise typing_preserves_length_l1 to modality-polymorphic
|`+formal/Semantics_L1.v+` |done 2026-05-27

|✅ Generalise subst_typing_gen_l1 to modality-polymorphic + Linear
wrapper (also generalised typing_preserves_bindings_l1,
output_shape_at_l1, loc_retype_at_R_l1) |`+formal/Semantics_L1.v+` |done
2026-05-27 (L2-β follow-up #2)

|✅ Restore region_shrink_preserves_typing_l1_gen bullet structure via
m-polymorphic helper (residual list-vs-multiset structural admit
isolated to T_Region_Active_L1 shadowed case inside _gen_m)
|`+formal/Semantics_L1.v+` |done 2026-05-27 (L2-β follow-up #3)

|✅ Replace the unrestricted region-shrink helper |`+formal/Semantics_L1.v+`,
`+Counterexample_RegionShrink.v+` |the unrestricted statement is refuted;
`+region_shrink_msperm+` and the value/neutral corollaries are Qed. Do not
attempt to prove the old unrestricted helper.

|Redesign the L1 judgment / step interface and state a sound replacement
for `+preservation_l1+` |`+formal/Semantics_L1.v+`,
`+Counterexample_PreservationL1.v+` |open design obligation; the current
unrestricted statement is refuted and must not be treated as closable debt
|===

==== L3 wiring (scoped result; not general preservation)

The L3 calculus and its specific typing/step-rule integration are present.
`+preservation_l3_region_active_echo+`, `+preservation_l3_drop_echo+`, and
`+preservation_l3+` are Qed for their matching echo-emitting cases. These
results are scoped to those rule pairs; they do not repair or imply general
L1/L2 preservation. See `+formal/Semantics_L1.v+` and
`+formal/PRESERVATION-DESIGN.adoc+` for the exact theorem statements.

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Item |What it does |Notes
|✅ Extend AST with [TEcho : ty -> ty] and [EEcho : ty -> expr -> expr]
|Type former + runtime value form for L3 echoes |done 2026-05-27 (L3
wiring slice 1 — Syntax.v + free_regions + value/shift/subst cases)

|✅ Add `+T_Observe_L1+` typing rule + `+EObserve+` expr form |Consumes
a `+TEcho T+` echo, returns `+TBase TUnit+` |done 2026-05-27 (L3 wiring
slice 2 — modality-polymorphic single rule; mandatoriness via
`+is_linear_ty TEcho+`/implicit-drop discipline is a follow-up)

|✅ Add `+T_Echo_L1+` typing rule |Types runtime [EEcho T v] residue
values at `+TEcho T+` |done 2026-05-27 (L3 wiring slice 3a — typing-side
counterpart of forthcoming `+S_Region_Exit_Echo+` / `+S_Drop_Echo+` step
rules; mode-polymorphic)

|✅ Add parallel typing rules `+T_Region_L1_Echo+` /
`+T_Region_Active_L1_Echo+` / `+T_Drop_L1_Echo+` |Output `+TEcho T+`
instead of `+T+` / `+TBase TUnit+`. Programs choose at typing time which
path |done 2026-05-27 (L3 wiring slice 3b — owner-approved parallel-rule
strategy). Initial +3 internal admits in
[region_shrink_preserves_typing_l1_gen_m] +
[region_liveness_at_split_l1_gen] were parallel-rule MIRRORS of
pre-existing structural admits; the avoidable T_Region_L1_Echo mirror
was CLOSED in slice 4 — only the two true T_Region_Active_*_L1_Echo
shadowed-case mirrors remain, both blocked by the same pre-existing
list-vs-multiset structural debt as the originals

|✅ Add collapse-function emission to step rules at irreversible
boundaries |`+S_Region_Exit_Echo+` emits `+EEcho T v+` paralleling
`+S_Region_Exit+` (untouched); `+S_Drop_Echo+` emits
`+EEcho T (ELoc l r)+` paralleling `+S_Drop+` |done 2026-05-27 (L3
wiring slice 3c — owner-approved parallel-rule strategy in Semantics.v;
updated `+step_from_eregion+` to 4-disjunct classification +
`+step_R_change_shape+` + `+no_leaks_gen+` cascade); rules quantified
over witness type T

|[line-through]#Thread `+G+` (echo context) alongside `+R+` (region
context) through compound rules# |[line-through]#New context parameter
on every L1 compound rule# |*OBSOLETE 2026-05-27*: under the
owner-approved parallel-rules design (slices 3a–3c), echoes are values
of type `+TEcho T+` that flow through the existing `+ctx+` G. No
separate echo-context parameter is needed.

|✅ State and prove `+preservation_l3+` |Per-layer preservation theorem
against the L3 invariants for the new echo-emitting step rules +
echo-typed paths |done 2026-05-27 (L3 wiring slice 4 — capstone). Two
per-case Qed lemmas (`+preservation_l3_region_active_echo+` for
`+S_Region_Exit_Echo+` × `+T_Region_Active_L1_Echo+`, and
`+preservation_l3_drop_echo+` for `+S_Drop_Echo+` × `+T_Drop_L1_Echo+`)
plus an umbrella `+preservation_l3+` (their conjunction, Qed). Zero new
admits or axioms. Per-case alignment forced by `+T_Echo_L1+`’s
witness-type premise; non-deterministic crossover cases are
non-preserving by design (typing derivation pins the path).
Qed for the stated matching echo paths; this is not a general L1/L2
preservation theorem and has no dependency on the refuted unrestricted
region-shrink statement.

|⏸ Register `+TEcho+` as linear via `+is_linear_ty+` (Phase B Slice 1) —
DEFERRED 2026-05-28 |Realises the design intent annotated at
`+TypingL1.v:T_Observe_L1+`: under Linear discipline, unobserved
`+TEcho+` must fail typing closure |*deferred until Phase D*.
Investigation 2026-05-28: adding `+| TEcho _ => true+` to
`+is_linear_ty+` is structurally non-vacuous at L1 — `+EEcho T v+` is
both a value (`+VEcho+`) and typed at `+TEcho T+` (via `+T_Echo_L1+`,
TypingL1.v:351-354), refuting the conclusion of
`+linear_value_is_loc_l1+` (Semantics_L1.v:891) and breaking 9
call-sites in `+subst_typing_gen_l1_m+` (Semantics_L1.v:1326-1605, Qed).
Realising the wire requires a disjunctive rewrite of
`+linear_value_is_loc_l1+` plus per-caller handling of the TEcho
disjunct — substantially larger than the original "`1-line
definitional`" framing. Owner deferred to after Phase D (L2 effect-typed
TFun) when the L1 substitution chain reshapes naturally. The legacy
`+Semantics.v+` branch is vacuous (no rule produces `+TEcho+`) and would
have closed trivially.

|⏸ Close the L1 list-vs-multiset structural admits at
`+Semantics_L1.v:553/621+` (Phase C) — DEFERRED 2026-05-28 |The
`+T_Region_Active_L1+`-shadowed sub-case of
`+region_shrink_preserves_typing_l1_gen_m+` requires bridging body
derivations across input shrinkage when the outer region matches a
body-internal active occurrence |*deferred until Phase D*. Four design
paths surfaced + analytically evaluated 2026-05-28 (recorded in this
session’s memory + companion design note `+Semantics_L1.v:366-402+`):
(a) Permutation-based perm-l1 leaves a list-structure output mismatch
(concrete counterexample at `+R_body = [a; rr; b; c]+` vs
`+R_body' = [b; rr; a; c]+`); (b) multiset reformulation of
`+remove_first_L1+` cascades through every L1 rule’s output threading;
(c) `+T_Region_*_L1+` rule redesign (Permutation premise on body output)
was implemented in-flight on `+proof/phase-c-l1-multiset-bridge+` —
closes sub-sub-case (ii) (R has exactly 1 rr via count-vacuity) but
leaves sub-sub-case (i) (R has ≥2 rr) requiring body-input-shrinkage,
which itself is NOT a theorem (T_Loc_L1 counterexample at count=1; T_Let
composition fails for the count-≥-2 precondition); (d) defer was
selected as the most mathematically safe + elegant path. Phase D (L2
effect-typed TFun) introduces the natural setting: lambda bodies’ R-flow
becomes effect-typed, which gives the structural invariant that lets
body-input-shrinkage discharge. The 2 admits at lines 553/621 remain as
documented L1 debt, and the outer `+Admitted.+` at line 653 + the
`+preservation_l3+` dependency annotation in PRESERVATION-DESIGN.adoc §5.1
continue to attribute them correctly.
|===

==== Mid-term (L4 — scaffold landed 2026-05-28)

L4 covers dyadic interaction semantics (mother–child distinction). Per
`+formal/PRESERVATION-DESIGN.adoc §7+`, L4 is "`not a separate proof
layer. It is a labelling discipline at the program / module level… No
proofs change.`"

Phase A scaffold landed 2026-05-28:

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Item |File |Status
|✅ L4 design page |`+formal/L4-DYADIC.md+` |done — extracts + extends
design doc §7

|✅ Labelling enum `+ProgramMode+` + `+program_mode_to_modality+`
mapping to L2 |`+formal/L4.v+` |done — Definitions only, no theorems, no
admit, no axiom
|===

Future L4 work (post-Phase D, optional): surface-syntax wiring in the
borrow checker so `+#![ephapax_linear]+` / `+#![ephapax_affine]+` /
`+#![module_boundary_mix]+` parse and select the L2 modality. This is
implementation, not proof debt.

==== Value-prop directions (committed and speculative)

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Direction |Status |Proof obligation
|Linear Echo + Region-Based Memory Management (S_Region_Exit
certified-evidence emission) |Committed for v1 |`+preservation_l3+` for
the Region branch

|Selective reversibility via L2 modality (Linear ≤ Affine thin-poset)
|Committed for v1 |Already mechanised in `+Modality.v+`

|Debugging / provenance via Linear Echoes as type-system receipts
|Committed for v1 |Follows from L3 wiring

|Linear discipline on deterministic drop (Rust-style) for critical
resources |Speculative |Compatible with L3 wiring; not committed v1

|GDPR-style certified erasure as compliance use-case |Direction
|Concrete instantiation; no separate proof obligation
|===

'''''

=== §3. What’s NOT to do (banned anti-patterns)

These are not preferences. They are explicit, durable, owner-issued
2026-05-27 directives.

==== A. Do not close the legacy preservation theorem

* ❌ `+Theorem preservation+` in `+formal/Semantics.v+` is *provably
false*. No proof closes it. The `+Admitted.+` is correct. Leave it.
* ❌ Do not add lemmas to `+formal/Semantics.v+` aimed at that closure.
Examples that have wasted real session time:
** Lemma B variants (`+step_preserves_type+`,
`+step_output_context_eq+`, `+step_preserves_type_at_pre+`,
`+step_output_context_eq_at_pre+`)
** `+region_add_typing_for_non_values+`
** Strengthened substitution lemmas
** `+sibling_typing_transfers_across_step+`-style helpers
* ❌ Do not patch the legacy `+formal/Typing.v+` judgment.
`+Counterexample.v+` depends on its falsity.

==== B. Do not close L1/L2 admits by ad-hoc cross-layer reasoning

* ❌ `+region_liveness_at_split_l1+` (if it returns) must NOT be closed
by adding proof tricks, side conditions discharged ad-hoc, or
strengthened lemma signatures within the current judgment shape.
Post-L2-hybrid these closures are cross-layer; the layered design
intentionally splits some closures across layers.
* ❌ The 9 Semantics_L1.v admits are L2-integration debt (bullet
structure for new Affine constructors). They are _not_ invitations to
introduce new `+Axiom+` declarations.

==== C. Do not bake linearity into Echo Types

Echo semantics (L3) and structural discipline (L2) must remain
orthogonal and compositional.

* ❌ Do not write `+LinearEcho+` and `+AffineEcho+` as separate type
formers. There is *one* type former (the fiber); the two modes are
_applications_ of it with different witness shapes.
* ❌ Do not pattern-match on `+Linear+`/`+Affine+` inside `+Echo.v+`.
The discipline is read from L2’s `+m : Modality+` at the typing-rule
boundary, not inside the calculus.

==== D. Do not treat Echo Types as a tracing-GC replacement

* ❌ Echo Types do not solve reachability or cycles.
* ❌ Echo Types are not a "`fire-and-forget`" automatic memory manager.
* ✅ Echo Types are a _type-theoretic discipline for accountability of
irreversible reclamation_ — strongest in conjunction with RBMM (regions)
or deterministic ownership (Rust-style drop).

==== E. Do not follow pre-2026-05-26 plans

* ❌ Anything dated before 2026-05-26 that proposes closing
`+preservation+` to `+Qed.+` is pre-discovery. PRs #92, #102, #104,
#106, #114, #116, #117, #121, #146 are archaeology.
* ❌ Branch `+lemma-b-phase2-middle-narrow+` (deleted post-archaeology
cherry-pick) was the most recent pre-discovery attempt. Do not
resurrect.

==== F. Do not conflate `+ephapax-affine+` with AffineScript

* ❌ `+ephapax-affine+` lives in this repo’s `+ephapax-linear/+` crate
alongside `+ephapax-linear+`. It is a _sublanguage_ of Ephapax.
* ❌ `+AffineScript+` (`+hyperpolymath/affinescript+`) is a different
language with no source-level overlap. Borrow-checker tactics from
`+affinescript/lib/borrow.ml+` do not apply here, and vice versa.
* ❌ The lexical overlap of the word `+affine+` is a coincidence.
Substructural-logic family terminology, not project relationship.

==== 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 file
* "`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
* writing a `+LinearEcho+` distinct from an `+AffineEcho+`
* applying tactics or framings from `+hyperpolymath/affinescript+` here

'''''

=== §4. Counts + file-by-file map

Coq `+Admitted.+` marker count: *3* (current source inventory): one
legacy marker plus two in `+Semantics_L1.v+`. This is a marker count, not
a count of sound obligations still awaiting routine proof.

CI count marker only (source markers, not routine proof debt):
Coq admitted proofs remaining: 3


* `+formal/Semantics.v+` `+preservation+`: false as stated; durable
  legacy archaeology, pinned by `+Counterexample.v+`.
* `+formal/Semantics_L1.v+` `+step_pop_disjoint_from_type_l1+` and
  `+preservation_l1+`: both unrestricted statements are refuted by
  `+Counterexample_StepPop.v+` and
  `+Counterexample_PreservationL1.v+`; neither is ordinary proof debt.
* The false unrestricted region-shrink helper was replaced by
  `+region_shrink_msperm+` and proved value/neutral corollaries. The
  false unconditional region-liveness helper was removed and replaced at
  call sites by the no-exit formulation. These are separate refuted
  helper statements and do not create additional live `+Admitted.+`
  markers.

Open work is redesigning L1/L2 judgments and stating sound replacement
theorems with exact hypotheses. See the current boundary at the start of
this document; the dated detail below is historical.
==== Archived per-file Qed / Admitted summary (2026-06-01; superseded)

[width="100%",cols="23%,>28%,>28%,21%",options="header",]
|===
|File |Qed |Admitted |Disposition
|`+formal/Semantics.v+` (legacy) |n/a |*1* |🛑 archaeology — single
`+Admitted.+` at line 9257 (`+Theorem preservation+`, provably false);
do not extend

|`+formal/Typing.v+` (legacy) |n/a |0 |🛑 archaeology —
`+Counterexample.v+` depends on falsity

|`+formal/Counterexample.v+` |*5* |0 |✅ pinned regression witness
(`+bad_typable+`, `+bad_step+`, `+bad_post_untypable+`,
`+t_loc_l1_R_preserving+`, `+bad_input_untypable_l1+`)

|`+formal/Counterexample_L2.v+` |*5* |0 |✅ Phase 4c soundness-gap
witness — fresh-region scope crossing (`+v_typed_at_empty+`,
`+outer_typed+`, `+e_before_typed+`, `+e_step+`, `+e_after_untypable+`)

|`+formal/Counterexample_L2_nested.v+` |*5* |0 |✅ Phase 3b
soundness-gap witness — nested TFunEff (analogue structure to
`+Counterexample_L2.v+`)

|`+formal/TypingL1.v+` |*2* |0 |✅ active — L1 judgment,
modality-indexed

|`+formal/Semantics_L1.v+` |*54* |*2* |✅ active — Phase 3b Stage 1a +
1b landed via PRs #252 + #253. *2* outer `+Admitted.+` markers —
`+step_pop_disjoint_from_type_l1+` and `+preservation_l1+`; both
unrestricted statements are refuted by later pinned regressions, not
ordinary open obligations. *Updated 2026-06-26: `+region_shrink…gen_m+`
dissolved (2026-06-16) and `+region_liveness_at_split_l1_gen+` removed
(this branch) via the honest `+val_region_no_exit+` reformulation — see
the §4 marker note. `+preservation_l3+` and the L2 β-case lemmas are now
unconditionally axiom-free. Counts are rebuilt `+coqc 8.18.0+` ground
truth on this branch.*

|`+formal/Modality.v+` |*1* |0 |✅ active — L2 core, zero axioms
(`+linear_to_affine+`)

|`+formal/Echo.v+` |*12* |0 |✅ active — L3 calculus mechanised

|`+formal/TypingL2.v+` |*10* |0 |✅ active — `+weaken_modality+` (+
Affine_id + 3 `+_le_*+` variants), `+preservation_l2_via_l1+`
(conditional on `+preservation_l1+`), `+linear_value_retype_l1_m+`, and
3 β-case lemmas (`+preservation_l2_app_eff_beta_linear+`,
`+_ground_nonlinear+`, `+_tfuneff+` conditional on Stage 1b side
conditions). NOT a wrapper.

|`+formal/L4.v+` |(Definitions only) |0 |✅ active — L4 labelling
discipline (`+PModeLinear+` / `+PModeAffine+` / `+PModeBoundaryMix+` +
`+program_mode_to_modality+` round-trip). No theorems. Phase A scaffold
landed 2026-05-28.

|`+src/abi/Ephapax/…+` (Idris2) |n/a |(E1–E6 + compileOk = 7
`+0+`-quantity postulates) |✅ active — ABI; postulates are explicit
OWED-to-Coq forwards. See §1 Idris row below.

|`+src/formal/Ephapax/…+` (Idris2) |working |none |✅ active — Region
linearity, narrow no-escape proof; no `+believe_me+` / `+sorry+` /
`+assert_total+`
|===

==== Archived seam audit (2026-06-01; superseded by current classifications)

The current `+admit.+` / `+Admitted.+` set in `+formal/*.v+`. The
remaining admits are exactly the *pre-existing L1 structural debt* (with
one true parallel mirror that closes when its original closes) plus the
*sacrosanct legacy preservation* (provably false per
`+Counterexample.v+`).

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Location |Class |Closes when
|`+Semantics_L1.v:576+` (`+admit.+`) |*Pre-existing* L1 structural —
`+region_shrink_preserves_typing_l1_gen_m+` / T_Region_Active_L1
shadowed sub-case; list-vs-multiset gap |L1 perm/multiset bridge OR
`+T_Region_*_L1+` redesign (deferred to Phase D)

|`+Semantics_L1.v:646+` (`+admit.+`) |*Parallel mirror* of `+:576+` —
T_Region_Active_L1_Echo shadowed sub-case; structurally identical |Same
as `+:576+` (mechanical replay)

|`+Semantics_L1.v:678+` (`+Admitted.+`) |*Outer marker* — depends on
internal `+:576+` + `+:646+` |When both internal admits close

|`+Semantics_L1.v:1994+` (`+admit.+`) |*Pre-existing* L1 structural —
`+region_liveness_at_split_l1_gen+` / T_Region_Active_L1 `+binder = rv+`
sub-case; *GENUINELY FALSE as stated* (single-case counterexample
documented at site lines 1923-1926); current `+Admitted.+` is a
transparency mark, not "`almost done`" |L2 effect-typed `+TFun+` per
`+PRESERVATION-DESIGN.adoc §5.1+`; closure requires reformulation, not
direct proof

|`+Semantics_L1.v:2014+` (`+admit.+`) |*Parallel mirror* of `+:1994+` —
T_Region_Active_L1_Echo `+binder = rv+` sub-case; inherits same falsity
|Same as `+:1994+`

|`+Semantics_L1.v:2028+` (`+Admitted.+`) |*Outer marker* — depends on
internal `+:1994+` + `+:2014+` |When both internal admits close (i.e.,
never directly — only via reformulation)

|`+Semantics_L1.v:3132+` (`+admit.+`) |*Pre-existing* —
`+preservation_l1+` body, covering S_StringConcat_Step2 + S_App_Step2 +
S_Pair_Step2 cases; lambda-rigidity gap per
`+PRESERVATION-DESIGN.adoc §4.8+` |Phase 3b Stages 2/3/4 (#240/#241/#242)
— L2 effect-typed lambdas with `+R_in/R_out+` syntactic annotations

|`+Semantics_L1.v:3133+` (`+Admitted.+`) |*Outer marker* — depends on
internal `+:3132+` |When `+:3132+` closes

|`+Semantics.v:9257+` (`+Admitted.+`) |*🛑 Sacrosanct* — legacy
`+Theorem preservation+`, *provably false* per `+Counterexample.v+`
(owner directive 2026-05-27) |Never. The `+Admitted.+` is correct.
|===

*Falsity audit* — two admits are not "`unproven but true`"; they are
*provably false as stated*:

[arabic]
. `+Semantics.v:9257+` — refuted by `+Counterexample.v+`; sacrosanct.
. `+Semantics_L1.v:1994+` (and its mirror `+:2014+`) — refuted by
single-case counterexample `+ERegion rv (EI32 5)+` at `+R=[rv]+`
documented in the source at lines 1923-1926. Their `+Admitted.+` is a
transparency mark acknowledging the residual sub-case is false. Closure
requires reformulation at the L2 layer (lambda-rigidity gap), not a
direct proof.

No `+Axiom+` declarations in `+formal/*.v+`. `+Counterexample.v+` /
`+Counterexample_L2.v+` / `+Counterexample_L2_nested.v+` carry 5 + 5 + 5
Qed respectively; `+TypingL1.v+` / `+Modality.v+` / `+Echo.v+` /
`+TypingL2.v+` are all `+admit.+`-free.

==== Idris2 side (proof carriers, not Coq mechanisation)

[width="100%",cols="34%,33%,33%",options="header",]
|===
|Concern |File(s) |Status
|Region linearity |`+src/formal/Ephapax/Formal/RegionLinear.idr+`
|working — explicitly "`REAL proof — not believe_me, not assert_total`"

|ABI surface (17 files) |`+src/abi/Ephapax/…+` |working — clean of
`+believe_me+` / `+sorry+`
|===

==== Tools

* *Coq 8.18+* for `+formal/*.v+` — primary mechanisation.
* *Idris2 0.8.0* (needs `+IDRIS2_PREFIX+` pointing at a prefix with
TTCs) for `+src/abi/Ephapax/…+`.
* *Just* as the build orchestrator (`+just proofs+`,
`+just idris-build+`, `+just golden+`).

==== Build oracles

* `+coqc 8.18.0+` is the *only authoritative answer* to "`is this
proved?`" for `+.v+` files. Comments in source claiming `+Qed+` without
`+coqc+` acceptance are not evidence.
* `+idris2 --check+` is the same for `+.idr+` files.
* Both are wired into `+rust-ci.yml+`’s "`Coq proofs`" and "`Idris2
build`" jobs.

'''''

=== §5. Archived closure-plan snapshots + foundation audit (2026-06-16 onward)

____
This section preserves dated historical snapshots for traceability; it is
not current status and is superseded by §1–§4 and the current preservation
boundary at the start of this document. In particular, later Coq
counterexamples refuted `+step_pop_disjoint_from_type_l1+` and
`+preservation_l1+`; old “open closure route” language below must not be
read as a plan to prove those unrestricted statements. The foundation-repo
audit is separate and cannot discharge Ephapax's local soundness obligations.

*Companion design docs* `+L1-REGION-REFOUNDATION-PLAN.md+` and
`+L1-ELIMINATOR-FORK.md+` (referenced below) live in *PR #299* (branch
`+docs/l1-closure-research+`), pending merge to `+formal/+`. The
tropical applicability case study is `+tropical-resource-typing+` PR #21
(`+docs/applications/ephapax-l1-regions.adoc+`).
____

==== 5.1 Archived proof-branch snapshot (superseded)

Branch `+proofs/l1-effect-typing-Aprime+` (A′ effect-typed-only
lambdas). *A′ closes 0 of 4 L1 admits* — the open obligations are
region/eliminator cases, not lambda-rigidity cases — so its
adoption-vs-revert disposition is still open (it is groundwork for the
choreographic `+S_App_Step2+` case, not a closure).

All four L1 lemmas (`+region_shrink+`, `+region_liveness+`,
`+step_pop+`, `+preservation_l1+`) each carry an outer `+Admitted.+` on
*both* this branch *and `+main+`* (`+step_pop_disjoint_from_type_l1+` is
present on `+main+` too, at `+Semantics_L1.v:3178+`/`+:3433+`). So
`+formal/+` holds *5 outer `+Admitted.+`* (1 legacy + 4 L1) on main —
*but the §4 `+status-gate+` marker reads `+4+` and the §4 prose says "`3
outer `+Admitted.+` in `+Semantics_L1.v+``": both are stale by one* (the
true `+Semantics_L1.v+` count is 4 outer markers, → 5 with the legacy).
This is a real *`+main+`-wide* drift, not branch-local — and exactly the
drift the *broken + unwired* `+status-gate+` (see §5.7) was supposed to
catch but couldn’t. §4’s marker is corrected to `+5+` in this PR; the
companion `+fix/proof-gates+` PR repairs the script (`+//+`→`+#+`) and
wires it into CI so future drift is flagged. (A′ shifts the line numbers
but not the count.)

==== 5.2 Archived L1-admit table (not authoritative; later counterexamples supersede)

[width="99%",cols="20%,16%,16%,16%,16%,16%",options="header",]
|===
|# |Lemma |Site (this branch) |Internal admits |Class |Closes via
|1 |`+region_shrink_preserves_typing_l1_gen_m+` |`+Semantics_L1.v:441+`
|`+:572+`, `+:642+` |*live structural* (list-vs-multiset tear)
|*Dissolves* — carrier refactor `+region_env : list+` → count-map.
`+L1-REGION-REFOUNDATION-PLAN.md+`

|2 |`+region_liveness_at_split_l1_gen+` |`+Semantics_L1.v:1904+`
|`+:1956+`, `+:1976+` |*provably FALSE* as written (witness
`+ERegion rv (EI32 5)+` at `+R=[rv]+`) |*Repaired* — restate as graded
`+live R rv ∧ no-exit-of-rv ⇒ live R' rv+`; prove from
`+count_occ_le_l1_m+` monotonicity + ~13-site call audit.
`+L1-REGION-REFOUNDATION-PLAN.md §5+`

|3 |`+step_pop_disjoint_from_type_l1+` |`+Semantics_L1.v+` |*1* (reduced
from ~9–11 in 2026 via the `+step_R_change_shape+` rewrite — see
`+L1-ELIMINATOR-FORK.md+` §8). The single residual obligation is
`+step exits r0 ∧ r0 ∈ free_regions(T) ⟹ cnt r0 R ≥ 2+`; its direct-exit
sub-case is vacuous, the residue is congruence-exit count-coherence.
Diagnosis corrected: *not* §4.8 lambda-rigidity (the witness has no
lambda) but region-count coherence at a region exit. *⚠️ 2026-07-07
(experiment 3): provably FALSE AS STATED* —
`+formal/Counterexample_StepPop.v+` (Qed, zero axioms) exhibits
`+EPair (ERegion rv (EI32 5)) (EVar 0)+` at `+R=[rv]+`: it types
(`+T_Var_Lin_L1+` has no `+In rv R+` premise), steps (`+S_Region_Exit+`
under `+S_Pair_Step1+`), and lands at `+R'=[]+` with
`+rv ∈ free_regions(T)+`. Same class as admit #2’s history: the
`+Admitted.+` hides a falsehood, not a gap. |*the eliminator fork* — now
with a Qed forcing argument that typing ⇏ trace coherence. The initial
value-anchored restriction proposal is superseded: the later witness in
`+Counterexample_PreservationL1.v+` refutes the `+S_StringConcat_Step2+`
case with an `+ELoc+` anchor. The current unrestricted lemma must not be
proved; a replacement requires an explicitly different judgment or
premise, owner-approved and independently proved.
`+Counterexample_StepPop.v+` header + `+L1-ELIMINATOR-FORK.md+` §3–§8

|4 |`+preservation_l1+` (capstone) |`+Semantics_L1.v:3367+` |`+:3379+`
|*⚠️ provably FALSE AS STATED (2026-07-07, experiment 3b)* —
`+formal/Counterexample_PreservationL1.v+` (Qed, zero axioms):
`+EStringConcat (ELoc 0 rv) (ESnd (EPair (ERegion rv (EI32 0)) (EVar 0)))+`
at `+R=[rv]+` types in both modalities and steps (the sibling’s region-exit
pops the only `+rv+`). In the Linear instance the post-state is untypable —
the `+ELoc+` anchor’s `+T_Loc_L1+` demands `+In rv []+`. The value-anchored escape
hatch suggested by `+Counterexample_StepPop.v+` is closed: the dangling
dependence here IS a value. |*NOT closable by lemmas* — the judgment
needs a temporal invariant such as region-liveness-through-reduction,
encoded in the judgment or enforced by strengthened leaf rules that reject
the witness. These are redesign directions, not established proofs; owner
decision required and to be recorded in `+PRESERVATION-DESIGN.adoc+`.
|===

`+preservation_l3+` (`+Semantics_L1.v+`, *Qed*) is scoped to the
matching echo-emitting rule pairs; it does not depend on the removed
unrestricted region-shrink helper and does not establish general L1/L2
preservation. `+L4.v+` is a scaffold (`+ProgramMode+` + round-trip
mapping; definitions only, no theorems). The marker inventory above is
not evidence that a refuted theorem should be closed.

==== 5.3 Idris2 ABI proof needs (a separate axis from the Coq L1 admits)

`+src/abi/Ephapax/ABI/Invariants.idr+` states six compiler-correctness
invariants as *erased (0-quantity) postulates*, each an explicit _owed_
forward to a discharging proof:

[width="100%",cols="34%,33%,33%",options="header",]
|===
|ID |Invariant |Status
|E1 |Type preservation (operational) |*owed* — legacy `+preservation+`
is false and current unrestricted `+preservation_l1+` is refuted. This
requires a separately stated, sound replacement theorem in Coq.

|E2 |Linear consumption across control flow |E2a position-form
*DISCHARGED* (`+splitLinearCoverage+`, Qed, `+Formal/Qualifier.idr+`);
E2b control-flow form *owed*

|E3 |No region escape |static/type-level *DISCHARGED*
(`+noEscapeTheorem+`, Qed, `+Formal/RegionLinear.idr+`); operational
form *owed*

|E4 |No runtime GC |*owed + flagged* — `+noGCExtract+` is a
*tautological/vacuous wrapper* (returns inputs unchanged), not a proof

|E5 |WASM compilation correctness |*owed — no formalisation exists*
(Rust backend only). Highest-leverage compiler-correctness gap; enables
`+compileOkImpliesWasmTyped+` in `+Foreign.idr+`

|E6 |IR (S-expr) lowering correctness |*owed — no formalisation*
|===

Real Idris Qed proofs verified clean (no
`+believe_me+`/`+assert_total+`/holes): `+splitLinearCoverage+`,
`+noEscapeTheorem+`, `+orthogonalityLemma+`, `+compileResultRoundTrip+`,
`+outlivesTransitive+`. Both `+abi-verify.yml+` and `+coq-build.yml+`
are hard CI gates (`+idris2 --build+`; `+coq_makefile+` +
`+Print Assumptions+` on the Phase-D top-level results).

==== 5.4 Committed closure route (owner-committed 2026-06-16)

[arabic]
. *Clean win (deterministic):* tropical carrier refactor → dissolves #1,
repairs the false #2, then flips `+preservation_l3+` unconditional. *Net
4 → 2 admits, 0 false lemmas.* (`+L1-REGION-REFOUNDATION-PLAN.md+`.)
. *Deciding experiment (cheap, do before the general theory):* the
minimal `+EDrop (EVar j : TString rv)+` choreography over two segments —
does subject reduction carry liveness through `+S_Region_Exit rv+`
coherently, or relocate it into a projection-coherence side-condition?
(`+L1-ELIMINATOR-FORK.md §6+`.) *DONE*
(`+formal/L1ChoreoExperiment.v+`): verdict *relocates* — and it
sharpened _why_ (the naive model collapses projection onto the scalar
predicate, which is false at re-entry; the real fork lives in the
*congruence* cases, not the clean `+ERegion+` exit). 2b. *Congruence
experiment (non-collapsed model):* *DONE*
(`+formal/L1ChoreoExperiment2.v+`, `+L1-ELIMINATOR-FORK.md §9+`). A
trace model that keeps subterm-relative *order* (not just the scalar
balance) *closes — in the model* — the obligation `+step_pop+` relocates
to: `+sibling_use_keeps_region_live+` is `+Qed+`, axiom-free,
non-circular, and unprovable from the snapshot alone. The congruence
verdict is upgraded from "`relocates`" to "`closes in the trace model,
reduced to **one wiring lemma**`" (`+wiring_obligation+`: typing ⇒
`+valid+` trace at `+k = cnt rv R+`). Experiment 1’s re-entry failure
mode provably does not recur. *Closes no admit yet* (honest count still
3); it is the consolidation step that names the precise next target.
. *If green → choreographic-foundational re-derivation:* region liveness
as a tropically-graded choreography across time segments (regions =
session- typed resources, scopes = segments, preservation = subject
reduction). Closes #3 → *2 → 0*, and likely gives *L4* its dyadic
(2-party choreography) structure for free — one foundation, all four
layers. *Next concrete step:* discharge `+wiring_obligation+` (plausibly
a structural induction on the typing derivation — each trace
`+Close+`/`+Use+` `+>= 1+` premise mirrors a local `+In r R+` premise in
`+T_Region_Active_L1+` / `+T_Loc_L1+`).

==== 5.5 Foundation trust audit (2026-06-16) — GO

The route reuses proofs from three sibling repos. An independent
ground-truth audit (cold rebuilds + kernel/flag probes, not doc-trust)
cleared all three — the owner’s "`did an LLM let a blank/sorry
through?`" concern *did not materialise*:

* *`+epistemic-types+`* (Agda 2.8.0) — *trustworthy/GO.*
`+agda   --no-libraries … All.agda+` exit 0; `+-W error+` still exit 0;
`+--safe+` _proven enforced_ (postulate-injection probe rejected, exit
42); zero escape hatches; zero orphans. Caveat: its `+EchoBridge+` is a
deliberate scaffold (grade plumbing, no proven graded-loss laws).
* *`+tropical-resource-typing+`* (Lean 4.13.0) — *trustworthy/GO
(strongest).* Cold `+lake build+` exit 0 ×2; kernel `+#print axioms+` on
all 17 load-bearing results → only `+propext+`/`+Quot.sound+` or none
(*no `+sorryAx+`, no `+Classical.choice+`*). Every lemma the route
reuses is non-vacuous.
* *`+echo-types+`* (Agda 2.8.0) — *trustworthy/GO, build on the WIRED
layer only.* 164 wired files (`+--safe --without-K+`, exit 0, zero
postulates) vs 15 orphaned (~8%). Three caveats: (a) the *one* real
postulate lives in the orphaned, exempted exploratory
`+EchoImageFactorizationPropPostulated.agda+` (honest quarantine,
imported by nothing); (b) the experimental `+echo-additive+` *variance*
suite is *orphaned + RETRACTED (R-2026-05-18)* and `+VarianceGate.agda+`
self-declares "`NO proven theorems`" — *do not cite variance as proven*;
(c) two dangling `+libraries+` configs cause false "`name not found`"
failures — fix before handing off.

==== 5.7 Gate integrity — threatened (surfaced 2026-06-16, NOT yet fixed)

Two CI-gate findings threaten the "`is it proved?`" guarantee and are
recorded here so they are not lost (no fix applied — surfaced for
decision):

* *`+coq-build-gate+` is implemented but NOT a _required_ status check.*
`+.github/settings.yml:113-118+` requires only `+hypatia-scan+` +
`+codeql+`; the always-on `+coq-build-gate+` aggregator (PR #254) is not
in `+required_status_checks+`. *Consequence: a new
`+Admitted.+`/`+Axiom+`, or a proof that fails `+coqc+`, could merge to
`+main+` undetected.* This is the single highest-priority gate fix.
* *`+scripts/status-gate.sh+` is doubly dead:* (a) line 3 is a `+//+`
C-style comment (should be `+#+`) → the script is syntactically invalid
and aborts immediately (a delimiter bug, fixable without touching the
owner string);
[loweralpha, start=2]
. it is wired into no CI workflow (only `+just status-gate+`). So the
"`Coq admitted proofs remaining: N`" drift check in §4 never runs in CI
— which is also why the §5.1 count drift (4 vs 5 on this branch) was
never flagged automatically.

(Lower-severity: `+scorecard-enforcer+` defaults the parsed score to
`+0+` on a malformed SARIF → possible false-fail; `+boj-build.yml+`
`+continue-on-error+` is acceptable for an external service.)

==== 5.6 Bottom line

ephapax’s remaining proof work = the 4 L1 admits (→ 2 by the
deterministic clean win, → 0 if the eliminator-fork experiment goes
green) + the unbuilt L4 + the owed Idris ABI obligations (E1, E2b,
E3-operational, E4, E5, E6, with E5 the highest leverage). The legacy
`+Semantics.v preservation+` is *not debt* — it is a deliberate,
witnessed false result. The plan is staged, ground-truthed, and the
foundation it builds on is independently verified.

'''''

=== Cross-references

* link:STATUS.adoc[`+STATUS.adoc+`] — past / present / future temporal
map.
* link:formal/PRESERVATION-DESIGN.adoc[`+formal/PRESERVATION-DESIGN.adoc+`]
— canonical four-layer design doctrine.
* link:CLAUDE.md[`+CLAUDE.md+`] — agent guidance; owner directive
2026-05-27.
* link:formal/Counterexample.v[`+formal/Counterexample.v+`] — the 5 Qed
lemmas that pin the soundness gap.
* https://github.com/hyperpolymath/echo-types[`+https://github.com/hyperpolymath/echo-types+`]
— upstream Agda foundation for L3.
* https://github.com/hyperpolymath/nextgen-languages/blob/main/docs/disambiguation/ephapax-vs-affinescript.md[Disambiguation:
ephapax vs AffineScript] — canonical side-by-side table.