ci(lean): add Lean proof gate (lake build) guarding the metatheory

[hyperpolymath]

Summary

Adds the Lean proof CI gate — the capstone that guards every mechanized proof landed this session against regression. There was no Lean CI anywhere in the estate, so the proofs (now all in main) were unguarded; a future refactor could silently break one.

What it does

.github/workflows/lean.yml runs lake build over academic/formal-verification/lean4/ on every push/PR, via leanprover/lean-action (SHA-pinned 38fbc41…, v1.5.0). lake build typechecks the whole development, so a broken proof fails CI. Guarded theorems:

• type safety — progress / preservation / determinism
• Sandbox Isolation (Theorem 1)
• Capability Soundness (Theorem 2) + Ethical Verdict Consistency
• BFT quorum-intersection safety (Theorem 3)

Core Lean only — no Mathlib, no test/lint targets — so test/lint/use-mathlib-cache are off; the toolchain pinned in lean-toolchain (v4.12.0) is all CI needs.

Notes

• Estate-consistent: reuses the vetted actions/checkout pin and SHA-pins lean-action (satisfies the scorecard/Hypatia "pin actions" policy).
• YAML validated locally; lake build itself verified locally via the cached toolchain (exit 0, no warnings) across all of this session's proof work.
• Possible follow-up: also assert sorry-freedom in CI (a naive grep false-positives on the docstrings that mention "sorry-free", so it'd need a #print axioms-based step) — local #print axioms already confirms only Lean's standard propext/Quot.sound/Classical.choice.

With this merged, the Phronesis proof suite is both complete and CI-protected going forward.

https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS

---

Generated by Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 30 issues detected

Severity	Count
🔴 Critical	0
🟠 High	7
🟡 Medium	23

View findings

[
  {
    "reason": "Action trufflesecurity/trufflehog@main needs attention",
    "type": "unpinned_action",
    "file": "secret-scanner.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_timeout_minutes",
    "file": "secret-scanner.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in scorecard-enforcer.yml",
    "type": "scorecard_publish_with_run_step",
    "file": "scorecard-enforcer.yml",
    "action": "split_scorecard_publish_job",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "binary_to_term without :safe option -- deserialization attack (1 occurrences, CWE-502)",
    "type": "elixir_send_unsanitised",
    "file": "/home/runner/work/phronesis/phronesis/lib/phronesis/compiler.ex",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  },
  {
    "reason": "Nominal-only SAST in phronesis: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/phronesis/phronesis",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "Repository has 3 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  },
  {
    "reason": "Code scanning (Hypatia): hypatia/structural_drift/SD007 -- Hypatia structural_drift: SD007 -- 2 day(s) old",
    "type": "CSA001",
    "file": ".claude/CLAUDE.md",
    "action": "review",
    "rule_module": "code_scanning_alerts",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence