docs: Phase C deferred (2026-05-28) — option (c) analytical infeasibility

[hyperpolymath]

Summary

• Records the 2026-05-28 finding that Phase C's structural admits at Semantics_L1.v:553/621 are not closeable via any of the four design paths surfaced in the prior session.
• Option (c) rule redesign was attempted in-flight on the prior proof/phase-c-l1-multiset-bridge branch — TypingL1.v rules + Counterexample.v regression + count_occ_le_l1_m Permutation-bridged — but proven analytically to close only sub-sub-case (ii) (R has exactly 1 rr via count-vacuity) while leaving sub-sub-case (i) (R has ≥2 rr) requiring body-input-shrinkage which is NOT a theorem (T_Loc_L1 counterexample at count=1; T_Let composition unstable for count-≥-2 precondition).
• The (c) changes are NOT in this PR — only the docs are. The (c) in-flight code was reverted; 10/10 .v rebuild clean against the original rules with the 2 documented admits still at 553/621.

What changed

• PROOF-NEEDS.md — adds a near-term deferral row for Phase C alongside the existing Phase B Slice 1 row.
• .machine_readable/6a2/STATE.a2ml — next_action moves to Phase D (L2 effect-typed TFun) with cross-references to both Phase B + Phase C deferrals.

Why option (d) defer was selected

• Most mathematically safe + elegant per owner directive 2026-05-28.
• Phase D introduces effect-typed lambdas, which gives the structural invariant that lets body-input-shrinkage discharge naturally.
• Preserves all current Qed lemmas; no regression-to-Admitted artifacts.
• The 2 admits at 553/621 + outer Admitted. at 653 + preservation_l3 cross-layer annotation continue to attribute the gap correctly to a pre-existing L1 obligation.

Test plan

• coqc 8.18.0 rebuild — 10/10 .v files clean (no new admits/axioms)
• No code changes (docs-only)
• Both deferral rows reference Phase D as the natural closure setting (consistent with formal/PRESERVATION-DESIGN.md §5.1)

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 67 issues detected

Severity	Count
🔴 Critical	10
🟠 High	10
🟡 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