docs+test: Phase D slice 4 Phase 4c — mechanised soundness-gap counterexample for TFunEff β

[hyperpolymath]

Summary

Ships a mechanised proof that preservation_l2 fails for TFunEff substituends inside fresh-region scopes, plus a design-doc addendum prescribing the conditional Phase 4c closure path.

This is the L1/L2 analogue of `formal/Counterexample.v` (which witnesses the legacy preservation's soundness gap), providing rigorous justification for the conditional preservation_l2 statement that Phase 4c will ship.

What this PR ships

`formal/Counterexample_L2.v` (new)

Three Qed lemmas (zero axioms, zero admits) witnessing the soundness gap:

• `e_before_typed` — input `EApp outer v2` types via T_App_L2_Eff at `TFunEff TUnit TUnit [] []`.
• `e_step` — operational step S_App_Fun reduces to `ERegion r2 v2`.
• `e_after_untypable` — no L1 derivation exists for the β-result at the same outer type.

Configuration:

```coq
T1_inner = TFunEff TUnit TUnit [] [] (* R_in_v = [] )
outer = ELam T1_inner (ERegion r2 (EVar 0)) ( body introduces fresh r2 )
v2 = ELam TUnit EUnit ( a value of type T1_inner )
e_before = EApp outer v2 ( well-typed )
e_after = ERegion r2 v2 ( β-result, NOT well-typed *)
```

Structural mechanism: T_Region_L1's `~ In r (free_regions T)` premise prevents the fresh r from being in `R_in_v ⊆ free_regions(TFunEff)`, so the post-β term's inner TFunEff value cannot re-type at the new threaded R = `r :: R`.

`formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md` addendum

New §"Phase 4c addendum (2026-05-30) — conditional preservation_l2 for TFunEff β" documents the counterexample and prescribes three resolution paths:

1. Conditional preservation_l2 (recommended) — Phase 3b lemma takes the `regions_introduced_by(e) ⊆ R_in_v` precondition; Phase 4c β-case requires it; programs outside form a documented soundness-gap class. Aligns with the `Counterexample.v` precedent for legacy preservation.
2. Region-polymorphic TFunEff — type-system change deferred to a future redesign.
3. L2 region-transfer combinator — adds L2 expressiveness in a future PR.

`formal/_CoqProject`

Adds `Counterexample_L2.v` after `TypingL2.v` in the build order.

`.machine_readable/6a2/STATE.a2ml`

`next_action` shifted to Phase 3b implementation (option-(a) precondition codified by this PR's counterexample); `last_action` records the counterexample landing.

Build + assumption audit

• `coqc -R . Ephapax` clean rebuild across all 11 .v files.
• `Print Assumptions e_before_typed` / `e_step` / `e_after_untypable` → "Closed under the global context" for all three. Zero axioms, zero admits.

Owner-directive compliance (CLAUDE.md 2026-05-27)

• ✅ Does not modify `formal/Semantics.v` or `formal/Counterexample.v` (the legacy soundness-gap artifacts).
• ✅ Does not patch `formal/Typing.v` (legacy judgment).
• ✅ Does not close any residual `formal/Semantics_L1.v` admit.
• ✅ Adds NEW infrastructure (a new file) orthogonal to legacy admits, mirroring the precedent of `Counterexample.v` for the legacy preservation.
• ✅ No new `Axiom` or `Admitted` markers.

Why this matters

Before Phase 3b implementation (~400 lines per PR #230's analysis), this counterexample mechanically witnesses the structural constraint the lemma must satisfy. The conditional preservation_l2 design is now rigorously justified rather than asserted on paper.

Test plan

• `coqc -R . Ephapax` rebuild across all 11 .v files, zero errors / warnings.
• `Print Assumptions` audit shows zero axioms on all three counterexample lemmas.
• Configuration in `Counterexample_L2.v` matches the on-paper analysis in Phase D slice 4 Phase 3b — TFunEff substitution-lemma extension (deferred from #224) #225 comment 4583148707.
• First PR to be gated by the new CI Coq build oracle from PR ci: add Coq build oracle workflow (closes #227) #231.

Refs

• ephapax#225 — Phase 3b tracking issue (option (a) selected).
• ephapax#225 comment 4583148707 — on-paper prototype that motivated this mechanical formalisation.
• PR feat(syntax): regions_introduced_by helper — Phase 3b scaffolding (#225) #230 — `regions_introduced_by` scaffold (option (a)'s syntactic helper).
• PR feat(L2): Phase D slice 4 Phase 4a — preservation_l2_app_eff_beta_linear + hotfix duplicate tfuneff_lambda_retype_l1_m #228 — Phase 4a (linear T1, no soundness gap).
• PR feat(L2): Phase D slice 4 Phase 4b — preservation_l2 β for ground-non-linear T1 #233 — Phase 4b (ground-non-linear T1, no soundness gap).
• PR ci: add Coq build oracle workflow (closes #227) #231 — CI Coq build oracle (this PR is its first beneficiary).
• `formal/Counterexample.v` — legacy preservation counterexample (precedent for this file's structure).

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 78 issues detected

Severity	Count
🔴 Critical	15
🟠 High	13
🟡 Medium	50

⚠️ 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": "unknown",
    "file": "abi-verify.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in boj-build.yml",
    "type": "unknown",
    "file": "boj-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in codeql.yml",
    "type": "unknown",
    "file": "codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in coq-build.yml",
    "type": "unknown",
    "file": "coq-build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in governance.yml",
    "type": "unknown",
    "file": "governance.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in hypatia-scan.yml",
    "type": "unknown",
    "file": "hypatia-scan.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in instant-sync.yml",
    "type": "unknown",
    "file": "instant-sync.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in mirror.yml",
    "type": "unknown",
    "file": "mirror.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in rust-ci.yml",
    "type": "unknown",
    "file": "rust-ci.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence