docs: Phase 3b 4-stage staged resolution plan (#235 → #239 / #240 / #241 / #242)

[hyperpolymath]

Summary

Phase D slice 4 Phase 3b — design-gap finding (#235) + 4-stage staged resolution plan owner-approved 2026-05-30 PM. Stages tracked at #239 / #240 / #241 / #242.

No formal/*.v changes. No CI changes (the parallel-session PR #236 owns the Coq EACCES fix).

4-stage staged resolution plan

The original three-option framing in #235 is superseded by a staged plan that captures all three "Interesting" values without committing to any single option's downsides.

Stage	Issue	Scope	Captures value of
Stage 1 — IMMEDIATE	#239	Leaf-only Phase 3b via tfuneff_lambda_free + Counterexample_L2_nested.v + 2-condition preservation_l2.	Option (3) — principled deferral, honest 2-condition statement.
Stage 2 — parallel L4 track	#240	ELam T_param R_in R_out body annotation extension. AST + typing rule + cascading.	Option (1) — L4 "type-level → program-level commitments".
Stage 3 — post-Stage-2	#241	Relaxed Phase 3b via declared_lambda_r_ins ⊆ R_in_v + CPS v-typing argument. Nested-condition collapses.	Option (2) — higher-order proof style enters codebase.
Stage 4 — Phase 5	#242	Compound non-linear + region-substitution machinery + unconditional preservation_l2.	The final destination.

Why staging beats single-option commitments

• (1) alone: forces AST migration before unblocking preservation_l2.
• (2) alone: introduces inductive-over-derivations predicate with no other use in the codebase.
• (3) alone: ends with conditional preservation_l2 forever (no path to unconditional).

The staged plan: (3) ships today's value at Stage 1, (1) lands L4's value at L4's timeline (Stage 2), (2)'s value is harvested at exactly the point CPS is necessary not over-engineered (Stage 3), (4) reaches unconditional preservation_l2 as the natural sum.

Stage 1's correctness is delivered, not provisional

Each of the 2 conditions on Stage 1's preservation_l2 has a mechanised counterexample:

• Counterexample_L2.v (already on main, PR docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234) — fresh-region gap.
• Counterexample_L2_nested.v (new in Stage 1) — nested-lambda gap.

Programs outside the conditional form a precisely-documented soundness class.

Sequencing

• Stage 1 green-lit (Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239). Implementation ships next session.
• Stages 2-4 tracked but NOT actioned this session.
• Stage 3 blocked on Stage 2; Stage 4 blocked on Stage 3; Stage 2 independent of Stage 1.

Changes

• formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md — Phase 3b addendum (gap finding + 3-options framing) + Phase 3b resolution addendum (4-stage staged plan).
• .machine_readable/6a2/STATE.a2ml — phase = implementation; next_action = Stage 1 (Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239) implementation.

No formal/*.v changes; Coqc 8.18.0 unaffected.

Predecessor PRs

• Phase 4a (feat(L2): Phase D slice 4 Phase 4a — preservation_l2_app_eff_beta_linear + hotfix duplicate tfuneff_lambda_retype_l1_m #228) MERGED — preservation_l2_app_eff_beta_linear.
• Phase 4b (feat(L2): Phase D slice 4 Phase 4b — preservation_l2 β for ground-non-linear T1 #233) MERGED — preservation_l2_app_eff_beta_ground_nonlinear_l1.
• Phase 4c (docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β #234) MERGED — Counterexample_L2.v 3-Qed soundness-gap witness.

Owner-directive compliance (across all 4 stages)

• ✅ No Semantics.v / Typing.v / Counterexample.v (legacy) touch.
• ✅ No new Axiom / Admitted markers.
• ✅ No closure of residual Semantics_L1.v admits — strictly NEW infrastructure under the four-layer redesign.
• ✅ Per-layer derivation: preservation_l2 closes via L2 infra; legacy preservation remains Admitted (PROVABLY FALSE) per 2026-05-27 directive.

Test plan

• CI green (no code changes; Coq oracle should pass unchanged — pending PR ci(coq-build): run coqorg/coq container as root to fix actions/checkout EACCES #236's EACCES fix landing).
• Issues Phase 3b design gap: option (a) precondition insufficient for T_Lam_L1_*_Eff body cases #235 / Phase 3b Stage 1: leaf-only substitution lemma + 2-condition preservation_l2 + Counterexample_L2_nested #239 / Phase 3b Stage 2 (L4 track): ELam annotation extension — R_in / R_out as program-level commitments #240 / Phase 3b Stage 3: relaxed restriction via declared_lambda_r_ins + CPS substitution lemma signature #241 / Phase 3b Stage 4 (Phase 5): compound non-linear values + unconditional preservation_l2 #242 cross-referenced.

Refs: #225 (Phase 3b parking lot), #230 (regions_introduced_by), #233 (Phase 4b), #234 (Phase 4c), #235 (parent finding), #236 (parallel Coq EACCES fix), #239 (Stage 1), #240 (Stage 2), #241 (Stage 3), #242 (Stage 4).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 75 issues detected

Severity	Count
🔴 Critical	11
🟠 High	16
🟡 Medium	48

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in abi-verify.yml",
    "type": "missing_timeout_minutes",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "missing_timeout_minutes",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "missing_timeout_minutes",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "missing_timeout_minutes",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "missing_timeout_minutes",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "missing_timeout_minutes",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "missing_timeout_minutes",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "missing_timeout_minutes",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "missing_timeout_minutes",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence