WIP: Import Beyond Bethe permanent approximation - #500

Open

Vilin97 wants to merge 62 commits into

mainfrom

codex/import42-formalization-beyond-bethe

Commits on Sep 21, 2026

Import complete Beyond Bethe permanent development and complexity dependency
Vilin97
committed
0f7f1d8
Port complete upstream content to current Mathlib and improve lint compliance
Vilin97
committed
de91481

Commits on Sep 22, 2026

Port foundational permanent, computation, and ellipsoid modules
Vilin97
committed
30b9984
Port cluster product bounds and machine combinator step proofs
Vilin97
committed
5f7bda4
Port Turing subroutine proofs and RAM configuration support
Vilin97
committed
d6b5fe7
Complete second compiler frontier across affine and machine proofs
Vilin97
committed
9fe8aa5
Port Turing composition and structured RAM proof dependencies
Vilin97
committed
2a27421
Port Bethe certificates and remaining machine transition proofs
Vilin97
committed
b65cd7f
Update word encoding and configuration simulation proofs
Vilin97
committed
c13d301
Port retargeted and register-store machine simulation proofs
Vilin97
committed
e8ac1f1
Adapt composed machine runs and sparse ABI resource proofs
Vilin97
committed
9924cb3
Resolve machine composition and entry-update type aliases
Vilin97
committed
963903d
Port Cobham closure and register instruction simulation proofs
Vilin97
committed
503be74
Port final approximation assembly and numerical cost estimates
Vilin97
committed
184bb53
Update certified pair accuracy and directed objective proofs
Vilin97
committed
1f78390
Port matrix epigraph identities and instruction execution bounds
Vilin97
committed
356089b
Port certificate bounds and remaining machine carrier equalities
Vilin97
committed
963f509
Port epigraph geometry and dense RAM initialization bounds
Vilin97
committed
8cdc018
Port machine computations and certificate bounds to current Lean
Vilin97
committed
33f57fa
Merge remote-tracking branch 'origin/main' into pr-500
github-actions[bot]
committed
7b5af6a

Commits on Sep 23, 2026

Commits on Sep 24, 2026

Merge remote-tracking branch 'origin/main' into pr-500
github-actions[bot]
committed
31e7b44

Commits on Sep 25, 2026

Commits on Sep 26, 2026