[Lean Squad] feat: formal verification infrastructure — research & CI automation

[Evangelink]

• Add formal-verification/ directory with research docs, targets list,
  correspondence and critique placeholders, and project report
• Identify 5 FV targets in the command-line infrastructure:
  • ArgumentArity (priority 1, decidable properties)
  • CommandLineParser.TryUnescape (priority 2, pure string unescaping)
  • CommandLineParser.ParseOptionAndSeparators (priority 3, pure splitting)
  • CommandLineOptionsValidator arity validation (priority 4)
  • CommandLineParseResult.Equals (priority 5, structural equality laws)
• Add formal-verification/lean/ directory with Lake build config (lakefile.toml)
• Add .github/workflows/lean-proofs.yml CI workflow for lake build

🔬 Lean Squad — automated FV infrastructure setup.

Co-authored-by: Copilot 223556219+Copilot@users.noreply.github.com

[Copilot]

Pull request overview

Introduces an initial Lean 4 formal-verification workspace and documentation for tracking verification targets in the command-line infrastructure, plus CI automation to run lake build when the Lean project changes.

Changes:

• Add formal-verification/ documentation (research notes, target list, placeholders, and report).
• Add a Lean 4 project scaffold under formal-verification/lean/ with Mathlib dependency.
• Add a GitHub Actions workflow to build Lean proofs on relevant PRs/pushes.

Show a summary per file

File	Description
formal-verification/lean/lakefile.toml	Defines the Lean/Lake project and pins Mathlib revision.
formal-verification/lean/README.md	Documents project structure, local build steps, and CI behavior.
formal-verification/TARGETS.md	Lists and prioritizes initial FV targets and phases.
formal-verification/RESEARCH.md	Captures research rationale and candidate properties to verify.
formal-verification/REPORT.md	Summarizes current status and run history.
formal-verification/CRITIQUE.md	Placeholder for ongoing critique of FV utility/coverage.
formal-verification/CORRESPONDENCE.md	Placeholder for Lean↔C# correspondence notes.
.github/workflows/lean-proofs.yml	Adds CI job that installs Lean tooling and runs lake build.

Copilot's findings

• Files reviewed: 8/8 changed files
• Comments generated: 6

[github-actions]

Commit pushed: b69b49f

Generated by 📐 Lean Squad, see workflow run.

[Copilot]

Copilot's findings

Comments suppressed due to low confidence (1)

.markdownlint-cli2.jsonc:156

• This change excludes formal-verification/**/*.md from markdownlint entirely. Since these documents are part of the repo and currently look markdownlint-compliant, ignoring the whole directory reduces lint coverage and can allow regressions. Consider removing this ignore entry (or narrowing it to truly generated artifacts) and fixing any rule violations inline if they arise.

  // Ignore patterns - files we are not in control of or auto-generated
  "ignores": [
    "SECURITY.md",
    "artifacts/tmp/**/*.md",
    "eng/**/*.md",
    "tools/**/*.md",
    "formal-verification/**/*.md",
    ".dotnet/**/*.md",
    ".github/ISSUE_TEMPLATE/**/*.md",
    ".github/skills/**/*.md",
    ".github/agents/**/*.md",

• Files reviewed: 13/14 changed files
• Comments generated: 5