Add emptyScan to the Lean Phase 1 plan model

[Copilot]

This extends the formal Phase 1 model to cover one more concrete optimizer primitive from the Python plan tree: LogicalEmptyScan. It closes a gap in the formal TODO list by modeling empty scans explicitly instead of encoding them indirectly as scan [].

• Lean plan model

  • Added Plan.emptyScan to formal/Py3plex/DSL/Syntax.lean
  • Mapped it directly to Python's LogicalEmptyScan

• Lean semantics

  • Added Plan.eval_emptyScan
  • Updated Plan.filter_empty_scan to state the ShortCircuitEmptyLayer behavior in terms of emptyScan

• Formal docs / roadmap

  • Marked Plan.emptyScan as completed in formal/README.md
  • Updated the Phase 1 proof table and Python↔Lean mapping to include emptyScan
  • Clarified the ShortCircuitEmptyLayer correspondence around emptyScan.eval = []

• Alignment guardrails

  • Extended tests/test_formal_phase1_alignment.py to enforce:
    • Plan.emptyScan is documented
    • the Python↔Lean mapping stays present
    • Plan.eval_emptyScan remains part of the Lean semantics surface

inductive Plan (α : Type) where
  | scan : List α → Plan α
  | emptyScan : Plan α
  | filter : (α → Bool) → Plan α → Plan α

theorem Plan.eval_emptyScan :
    ((Plan.emptyScan : Plan α)).eval = [] := rfl