feat(L1): Phase D slice 4 Phase 3a — tfuneff_lambda_retype_l1_m + is_tfuneff_ty

[hyperpolymath]

Summary

• Ships the retype lemma half of Phase 3 per formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md.
• Adds is_tfuneff_ty predicate (Syntax.v) mirroring is_ground_nonlinear_ty.
• Adds tfuneff_lambda_retype_l1_m lemma (Semantics_L1.v): retype TFunEff lambda value across (m, R, G) → (m, R', G) under side condition forall r, In r R' → In r R_in.
• Phase 3b (substitution-lemma extension) DESCOPED to a follow-up PR after structural analysis revealed the T_Region_L1 fresh-region obstacle. STATE.a2ml documents the three candidate solutions.

Why split

SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3 proposed two pieces (retype + substitution extension). Walking the substitution proof revealed: every retype across a threaded R_n inside the term e demands forall r, In r R_n → In r R_in_arg, and T_Region_L1 firings inside e introduce fresh r ∉ R_outer — freshness wrt the threaded R does not imply membership in the value-type's fixed R_in_arg. Three candidate fixes (syntactic side condition on e; universal-R Hv_type with per-case discharge; restrict to region-free terms) need Phase 4 prototyping of the actual subst 0 varg ebody shape before choosing. Phase 3a's retype lemma stands on its own as clean infrastructure usable in 3b and Phase 4.

Proof shape

tfuneff_lambda_retype_l1_m:

• destruct Hval (10 value-form cases)
• inversion Ht; subst; try discriminate
  • Non-ELam forms: types don't match TFunEff → discriminate.
  • ELam at TFun (legacy rules T_Lam_L1_Linear / T_Lam_L1_Affine): type mismatch TFun ≠ TFunEff → discriminate.
  • ELam at TFunEff (T_Lam_L1_Linear_Eff / T_Lam_L1_Affine_Eff): re-apply rule with new Hsub, body via eassumption.

Zero new admits, zero new axioms. Coqc 8.18.0 clean rebuild across all 10 .v files.

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

• ✅ No closure of legacy preservation in Semantics.v (untouched).
• ✅ No closure-support lemmas in Semantics.v (untouched).
• ✅ No closure of residual Semantics_L1.v admits — strictly NEW orthogonal infrastructure.
• ✅ No patching Typing.v (untouched).
• ✅ No new Admitted / Axiom.
• ✅ Anti-pattern detector clean.

Test plan

• coqc -Q . Ephapax clean across all 10 .v files locally.
• CI green on formal/ build job.

Refs: standards#134 (proof-debt epic), #220 (Phase 2), #213 (design doc).

[github-actions]

🔍 Hypatia Security Scan

Findings: 74 issues detected

Severity	Count
🔴 Critical	13
🟠 High	13
🟡 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": "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 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"
  },
  {
    "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

[hyperpolymath]

Phase 3b follow-up tracked in #225 (substitution-lemma extension; three candidate solutions documented).

[hyperpolymath]

Seam-analyst notes (for owner awareness, not blocking):

1. SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 3 description ("ship retype + extend substitution") is over-optimistic — the two halves have very different difficulty. Worth an addendum noting the T_Region_L1 obstacle and the 3a/3b split. Could file as a docs-only follow-up.

2. Parallel-session race noticed: another worktree at /tmp/ephapax-phase-3a on branch phase-d-slice-4-phase-3a-tfuneff-retype-2026-05-30 has a local commit for the same Phase 3a work (1648a08, not pushed). Per the branch-drift memory I didn't disturb that WIP; if its PR lands first, this PR rebases or closes. If this PR lands first, that session rebases.

3. SUBST-LEMMA-GENERALIZATION-DESIGN.md Phase 4 plan refers to "Phase 3 lemma" (singular). With the 3a/3b split, Phase 4 case-coverage analysis needs updating to reflect that 3b is the actual blocker for the TFunEff non-linear T1 case.