The formal folder TODO list had reachable Phase-1 items left open. This change advances the Lean model and README alignment by implementing project/limit semantics and checking off the corresponding redundant-project optimizer theorem.

• Lean Plan extension (reachable Group 1 TODOs)

  • Added Plan.project and Plan.limit to formal/Py3plex/DSL/Syntax.lean.
  • Updated Python mapping table in the same file to include LogicalProject and LogicalLimit.

• Executable semantics and core theorems

  • Extended Plan.eval in formal/Py3plex/DSL/Semantics.lean:
    • project evaluates via List.map
    • limit evaluates via List.take
  • Added:
    • Plan.eval_project
    • Plan.eval_limit
    • Plan.project_id

• Optimizer theorem for redundant project

  • Added formal/Py3plex/Optimizer/ProjectIdentity.lean with:
    • Py3plex.Optimizer.remove_redundant_project
  • Imported into root formal entrypoint (formal/Py3plex.lean).

• Formal README TODO/proof inventory alignment

  • Updated theorem inventory and Python↔Lean mapping.
  • Marked as done:
    • Plan.project
    • Plan.limit
    • remove_redundant_project ↔ RemoveRedundantProject

• Alignment test updates

  • Extended tests/test_formal_phase1_alignment.py to assert:
    • new constructors are present in Lean syntax
    • new semantics theorems are listed and defined
    • new optimizer theorem file/theorem is present
    • README checklist reflects completed items.

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

def Plan.eval : Plan α → List α
  | .scan rows => rows
  | .emptyScan => []
  | .filter p child => child.eval.filter p
  | .project f child => child.eval.map f
  | .limit n child => child.eval.take n