Rejection-based extractor from policyengine-us Python formulas to Lean 4, producing Lawlib.
Rejection-based: formulas are parsed by static AST inspection against a
whitelist IR (~20 node kinds). Anything outside the fragment — loops,
dynamic dispatch, astype tricks — is rejected loudly with file, line,
and reason into rejection_report.md. A wrong translation poisons every
downstream theorem; a rejection is actionable.
Pipeline: dependency-closure walk from eitc (static, never traced) →
typed IR with explicit bool→number coercions → Lean emission in
topological order with provenance docstrings. Parameters are read from
YAML decimal text (0.34 → 34/100), never through Python floats.
pip install -e .
pe2lean closure # print the classified dependency closure
pe2lean extract --lawlib .. # regenerate Lawlib/Gen, manifest, rejection report
pe2lean-spot --lawlib .. # parameter lookups vs PolicyEngine API
pe2lean-diff 10000 --lawlib .. # randomized differential test
policyengine-us is pinned exactly (pyproject.toml); bumping the pin is
a deliberate two-PR flow (pe2lean pin bump → re-extracted Lawlib), gated by
the differential suite.