Skip to content

proof(L1): reduce step_pop's 11 eliminator admits to 1 via step_R_change_shape (§6 experiment) #330

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 27, 2026
Merged

proof(L1): reduce step_pop's 11 eliminator admits to 1 via step_R_change_shape (§6 experiment) #330

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion PROOF-NEEDS.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -385,7 +385,7 @@ future drift is flagged. (A′ shifts the line numbers but not the count.)
|---|---|---|---|---|---|
| 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:3106` | **~9–11** across every eliminator/erasing context (`S_App_Step2`, `S_Pair_Step2`, `S_Inl/Inr_Step`, `S_Case_Step`, `S_Let_Step`, `S_Region_Step`) — all blocked on the §4.8 lambda-rigidity gap | **the eliminator fork** | **Open research** — choreographic typing across time segments, used foundationally. `L1-ELIMINATOR-FORK.md` |
| 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. | **the eliminator fork** | **Open research** — the tropically-graded choreography over time segments. `L1-ELIMINATOR-FORK.md` §3–§8 |
| 4 | `preservation_l1` (capstone) | `Semantics_L1.v:3367` | `:3379` | **gated** on 1–3 | follows once 1–3 land |

`preservation_l3` (`Semantics_L1.v`, **Qed**) is real and depends on **only**
Expand Down
38 changes: 38 additions & 0 deletions formal/L1-ELIMINATOR-FORK.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,3 +153,41 @@ relocate the difficulty into projection coherence, and the sequential-language
foundation is non-standard. The §5/§6 experiment is the inexpensive way to
learn which — and it is the recommended next step on the eliminator fork, run in
parallel with (not blocking) the clean-win carrier refactor.

## 8. Result of the §6 experiment (2026 — run in Coq)

The §6 deciding experiment was run against the live judgment. Outcome: the
verdict is the predicted **"no" — it relocates** — but the experiment also
produced a concrete simplification worth keeping.

**(a) `step_pop_disjoint_from_type_l1` reduces from 11 admits to 1.** Driving
the proof by `step_R_change_shape` (every step leaves `R` fixed, prepends a
fresh region, or removes exactly one) makes all ten eliminator/erasing
congruences trivial — a region free in the result type survives unless the
step exits *that exact* region. The 255-line induction with eleven `admit`s
becomes ~15 lines with one. (Landed; `coqc 8.18.0` + `Print Assumptions`
verified; outer `Admitted` count unchanged.)

**(b) The single residual obligation, exactly:** the step exits `r0` while
`r0 ∈ free_regions(T)` ⟹ `cnt r0 R ≥ 2` (i.e. `In r0 (remove_first r0 R)`).
Its **direct-exit** sub-case is *vacuous* — a head redex `ERegion r0 v` is
typed by `T_Region_Active_L1`, whose `~In r0 (free_regions T)` premise
contradicts `r0 ∈ free_regions(T)`. The residue is the **congruence-exit**
case (`ERegion r0` under an eliminator; `r0` from a sibling's type — a
distinct occurrence).

**(c) Why it relocates (the §2 wall, mechanically reconfirmed).** Discharging
the congruence case needs the sibling's `r0` proved a *distinct* occurrence
from the exiting one — exactly the temporal/segment coherence the snapshot
env + result type cannot express. Every closure route tried
(`free_regions ⊆ R_out`, `count_occ_le_l1_m`, linking the dynamic exit to the
static output) collapses to connecting the dynamic step to the static typing
output, which *is* preservation. Circular.

**(d) The §4.8 framing was wrong** and is corrected in the source: the
obstruction is not lambda-rigidity (the witness has no lambda) but
region-count coherence at a region exit. **Net: ADMIT 3 stays open at the
honest count (still 2 outer `Admitted`), but is now ONE minimal, precisely
characterised obligation** — the cleanest possible target for the §3 / §5.1
tropically-graded choreography. That choreographic closure is the
unchanged recommended next step.
Loading
Loading