File size: 1,386 Bytes
224e773 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 | import Lake
open Lake DSL
package «sovMonster» where
require mathlib from git
"https://github.com/leanprover-community/mathlib4" @ "v4.14.0"
lean_lib «SovMonster» where
roots := #[`SovMonster]
-- Matrix-level Jordan commutativity proof (requires Mathlib)
lean_lib «JordanMatrixProof» where
roots := #[`JordanMatrixProof]
-- Full matrix-level formalization (Ahmad Ali Parr, PAR-011)
lean_lib «SovMonster_Matrix» where
roots := #[`SovMonster_Matrix]
-- Closed formalization — Ahmad's systematic sorry audit
lean_lib «SovMonster_Matrix_Closed» where
roots := #[`SovMonster_Matrix_Closed]
-- Gap analysis + implementation strategies for remaining sorries
lean_lib «SovMonster_Gaps» where
roots := #[`SovMonster_Gaps]
-- Bridge: sovereign-calculus ↔ sov-kernel-monster (Ω, φ⁻¹, AToKio, WORM)
lean_lib «SovereignCalculusBridge» where
roots := #[`SovereignCalculusBridge]
-- Gap 2 closed: MOC 108-dim ↔ Jordan 10×10 roundtrip, zero sorry
lean_lib «MOCJordanRoundtrip» where
roots := #[`MOCJordanRoundtrip]
-- Link against the Fortran object (built by build_monster.sh)
-- Run `build_monster.sh` first, then `lake build`
lean_exe «sov-monster» where
root := `SovMonster
moreLinkArgs := #[
"-L./build",
"-Wl,-rpath,./build",
"./build/sov_arm64.o" -- or sov_x86.o on x86_64
]
|