state: shift next_action to Phase 1 (ground_nonlinear_retype_l1_m)

[hyperpolymath]

Summary

Reflect the deeper analysis from PR #213's design doc: the non-linear substitution generalisation is a 5-phase plan, not a single sibling lemma. Phase 1 (the simplest ~10-line building block) is the right next-session scope.

Changes

• `next_action`: shift from "generalise subst_typing_gen_l1_m (full scope)" → "Phase 1: `ground_nonlinear_retype_l1_m`". Cites the design doc + identifies the two file touchpoints (`Syntax.v` predicate, `Semantics_L1.v` lemma).
• `last_action`: record PR docs: SUBST-LEMMA-GENERALIZATION-DESIGN — Phase D slice 4 plan #213 design doc merge.
• `@artifacts`: extend to list `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`.

Anti-pattern list updated to include design-doc-specific guardrails: no folding case-split into existing lemma, no closing TFun retype (legacy slice 4b gap, out of scope), etc.

Refs

• PR docs: SUBST-LEMMA-GENERALIZATION-DESIGN — Phase D slice 4 plan #213 — design doc (merged)
• PR feat(L2): preservation_l2_via_l1 — Phase D slice 4 partial landing #211 — preservation_l2_via_l1 (merged)
• `formal/SUBST-LEMMA-GENERALIZATION-DESIGN.md`

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 73 issues detected

Severity	Count
🔴 Critical	13
🟠 High	13
🟡 Medium	47

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "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"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "unknown",
    "file": "scorecard-enforcer.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence