…no admit removed yet)

Replaces the soundness SMELL of the false region_liveness_at_split_l1_gen
(In rv R -> In rv R'; witness ERegion rv (EI32 5) at R=[rv]) with TRUE,
axiom-free counterparts proven beside it (build green, Print Assumptions clean):
  - expr_no_exit_of_region rv e          (honest side condition)
  - cnt_preserved_no_exit_l1_gen  (Qed): no exit of rv => cnt rv invariant
  - region_liveness_no_exit_l1_gen (Qed): the honest In rv R -> In rv R'

13-site call-site audit (subst_typing_gen_l1_m): ALL 13 are class-3. The only
local hypothesis is In rv R (outer); output_shape_at_l1 carries no region info;
the no-exit side condition is not locally dischargeable (e1 is an opaque
induction var). The obligation they smuggle IS the dangling-region /
eliminator-fork problem: the 4 L1 admits are 4 faces of ONE
region-liveness-through-reduction invariant. ADMIT 2 is NOT independently
closable.

Net: 4+1 admits UNCHANGED (false lemma retained, still used by 13 sites).
Honest 4->3 path documented inline + plan doc: thread expr_no_exit_of_region
through subst_typing_gen_l1_m, discharge the 13 sites via the TRUE lemma,
delete the false lemma, relocate the obligation to preservation_l1 (capstone).
Staged as a follow-on (signature change through a ~30-case induction).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…hine-checked, no admit closed)

Minimal 2-segment EDrop(EVar j)/ERegion choreography experiment for the
region-liveness eliminator fork. A 3-lens adversarial verify (wf_300a9737)
sharpened the verdict: subject reduction RELOCATES region-liveness into a
projection-coherence side condition (= expr_no_exit_of_region promoted to a
foundational invariant) — it does NOT carry coherently.

- formal/L1ChoreoExperiment.v: 5 Qed lemmas, axiom-free (Print Assumptions
  clean), wired into the build. EDrop(EVar j) is the wrong probe (reduces by
  S_Drop with R unchanged, never crosses S_Region_Exit; carried
  unconditionally). The only boundary-crossing term ERegion rv _ fails the
  relocated coherence condition (region_frame_breaks_no_exit). The
  apparatus-level obligation close_derives_coherence is named honestly (bare
  Definition, never proved) and proved incompatible with any inner
  same-region re-frame (close_derives_coherence_needs_no_inner_exit).
- formal/L1-CHOREO-EXPERIMENT.md: the decisive finding + corrected next
  experiment — target the congruence cases (S_Let/App/Pair/Case
  Semantics_L1.v:3271-3284), NOT the already-Qed'd clean region exit. Routes
  for admits 1/2 (deterministic carrier refactor) vs 3/4 (choreographic)
  stay independent.

Closes no admit, adds no axiom. Semantics_L1 admits unchanged (4); legacy
preservation untouched (1).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…ation — axiom-free

The general region_shrink statement was FALSE-as-stated: the witness
ERegion r (ERegion r EUnit) consumes two ambient copies of r (nested
T_Region_Active_L1) yet is expr_strictly_free_of_region r (that
predicate descends through ERegion unconditionally); it types at
[r;r] -> [] but not at remove_first r [r;r] = [r]. So the admitted
region_shrink_preserves_typing_l1_gen_m could never close.

Replace it with region_shrink_msperm: region-shrink holds whenever the
OUTPUT env is a multiset-permutation of the input. This threads through
every compound rule via the monotonicity squeeze (count_occ_le_l1_m in
both directions) — no list (order) equality needed, so the feared
list-vs-multiset wall never bites — and makes the T_Region_Active_L1
(+ _Echo) shadowed sub-case VACUOUS: an active region strictly drops
its r-count, so its output can never be a multiset-perm of its input.
region_shrink_{neutral,value} follow as axiom-free corollaries; the
value form (via value_R_G_preserving_l1) is exactly what the
preservation_l3 / S_Region_Exit call sites need.

- Semantics_L1.v: + multiset_perm + region_shrink_msperm (all 36 cases,
  Qed) + region_shrink_{neutral,value}; rewire preservation_l3 and the
  value wrapper region_shrink_preserves_typing_l1; remove the false
  _gen_m / _gen lemmas; honesty pass on the status comments.
- Counterexample_RegionShrink.v (NEW): pins region_shrink_is_FALSE
  (6 Qed lemmas) — the regression witness motivating the restriction.
  Sibling to Counterexample.v / Counterexample_L2.v.
- _CoqProject: register Counterexample_RegionShrink.v.

Print Assumptions region_shrink_{msperm,neutral,value} = "Closed under
the global context". preservation_l3 is now UNCONDITIONALLY axiom-free.
Semantics_L1 admit inventory 4 -> 3 (region_liveness_at_split_l1_gen,
step_pop_disjoint_from_type_l1, preservation_l1 remain). Clean
from-scratch `make` green (15 files). Independently recompiled; validated
by four adversarial coqc probes.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Route C (count-map carrier migration) is moot: ADMIT 1 was closed via the
multiset-perm generalisation (region_shrink_msperm, 0acd7d8) on the existing
list carrier instead. Kept banner-marked SUPERSEDED as the record of the
explored-and-abandoned migration design + the A'/_Eff decouple analysis.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…vernance

…vernance

…vernance