proof(L3): preservation_l3 capstone — slice 4 (closes L3 wiring)

[hyperpolymath]

Summary

L3 wiring slice 4 — capstone. Per-layer preservation theorem for the two L3-specific echo-emitting step rules paired with their matching L3 typing rules. Closes the L3 wiring task in PROOF-NEEDS.md §2.

What's new

Three new Qed in formal/Semantics_L1.v:

Lemma	What it proves
preservation_l3_region_active_echo	(T_Region_Active_L1_Echo, S_Region_Exit_Echo) pair preserves typing at TEcho T
preservation_l3_drop_echo	(T_Drop_L1_Echo, S_Drop_Echo) pair preserves typing at TEcho T
preservation_l3 (umbrella)	Conjunction of the two — Qed by split; exact …

Per-case alignment is forced by T_Echo_L1's witness-type premise. The step rules are universally quantified over T (non-deterministic at the relation level); the typing derivation pins which T is in play. Non-deterministic crossover cases (e.g. legacy T_Region_Active_L1 + L3 S_Region_Exit_Echo) are non-preserving by design — not covered by this theorem and not well-typed at the umbrella's TEcho T output.

Seam audit (every admit/axiom classified)

The user asked to "make sure that all the seams and gaps are checked and secure." Two outcomes:

1. One avoidable parallel-rule admit closed

region_shrink_preserves_typing_l1_gen_m's T_Region_L1_Echo case admit (was a mirror of a fully-closed original) is now Qed-style — count-monotonicity for the shadowed sub-case, remove_first commutation for the descend sub-case. Same treatment for the descend sub-case of T_Region_Active_L1_Echo. Net debt: -1 internal admit.

2. Every remaining admit classified in PROOF-NEEDS.md §4

After this PR, the complete admit/axiom inventory of formal/*.v:

Location	Class
Semantics_L1.v:553 (admit.)	Pre-existing L1 structural (T_Region_Active_L1 shadowed)
Semantics_L1.v:621 (admit.)	True parallel mirror of :553
Semantics_L1.v:653 (Admitted.)	Outer marker over :553 + :621
Semantics_L1.v:1256 (admit.)	Pre-existing L1 structural (T_Region_Active_L1 r = rv)
Semantics_L1.v:1276 (admit.)	True parallel mirror of :1256
Semantics_L1.v:1290 (Admitted.)	Outer marker over :1256 + :1276
Semantics_L1.v:1694 (admit.)	Pre-existing — preservation_l1 lambda-rigidity gap
Semantics_L1.v:1695 (Admitted.)	Outer marker over :1694
Semantics.v:9257 (Admitted.)	🛑 Sacrosanct (provably false per Counterexample.v)

Zero Axiom declarations. TypingL1.v / Modality.v / Echo.v / Counterexample.v / TypingL2.v are all admit-free.

Per CLAUDE.md owner directive 2026-05-27

• ✅ Zero new Admitted. or Axiom. declarations
• ✅ No legacy Semantics.v patching
• ✅ No cross-layer reasoning to close L1 admits
• ✅ Re-uses pre-existing infrastructure only (value_R_G_preserving_l1 Qed + region_shrink_preserves_typing_l1_gen_m conditional)
• ✅ Cross-layer dependency on L1 structural admit annotated per PRESERVATION-DESIGN.md §5.1

Build oracle

coqc 8.18.0 clean rebuild of all 9 .v files in dependency order: PASS.

Test plan

• Slice 4 lemmas compile with zero warnings
• All 9 formal/*.v files compile (coqc -R . Ephapax)
• Zero new admit. or Admitted. introduced (verified via grep)
• One avoidable parallel-rule admit closed (line 574 was; gone now)
• Commit GPG-signed (G per git log --format=%G?)
• CI green
• Owner review

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 51 issues detected

Severity	Count
🔴 Critical	9
🟠 High	9
🟡 Medium	33

⚠️ 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