proofs(lean4): promote ET-2 to main — L1 conversion is decidable - #27

Merged

hyperpolymath merged 8 commits into

mainfrom

proofs/lean4-l1-l2

Jul 27, 2026

Commits on Jul 21, 2026

proofs(lean4): mechanize the L1/L2 core — hereditary substitution, grade algebras, hard gates

hyperpolymath
and
claude
committed
0eb7afe
ci(proofs): enforce https-only redirects on the elan download (Sonar S6506)

hyperpolymath
and
claude
committed
1f2a81a

Commits on Jul 22, 2026

proofs(lean4): close ET-2 — L1 conversion is decidable

hyperpolymath
and
claude
committed
7dc7cd7
proofs(lean4): close ET-2 — L1 conversion is decidable (#24)
hyperpolymath
authored
7599b7b

Commits on Jul 27, 2026

Merge origin/main into proofs/lean4-l1-l2 (pre-PR sync)

hyperpolymath
and
claude
committed
0104c9c
fix(ci): make the Lean toolchain install idempotent

hyperpolymath
and
claude
committed
14ebfe8
fix(ci): drop policy-violating flake.nix; unblock the trusted-base check

hyperpolymath
and
claude
committed
0ba3aec
chore(estate): delete the corrupted anti-Zig check (owner ruling)

hyperpolymath
and
claude
committed
0ade7de