Research-Stack/0-Core-Formalism/lean
Brandon Schneider efe8c14973 refactor(ssms): clean f_eps/omf_eps proof; restructure ko_preserves_hyperbola_approx
- SSMS: remove redundant conflicting sub-proofs in f_eps/omf_eps; streamline
  with single H2 + h2 + omega chain
- HyperbolicStateSurface: replace trivial identity ko_preserves_hyperbola_approx
  with proper TODO(lean-port) admitting the full bound-propagation chain for
  sqrt error; AGENTS.md updated accordingly
- AGENTS.md: update aciPreservedByMlgruStep status to reflect mul_mono_left
  as critical remaining blocker

Build: 3313 jobs, 0 errors (lake build)
2026-05-27 16:49:05 -05:00
..
conversions/hardware WIP: accumulated changes 2026-05-25 16:24:21 -05:00
external/OTOM WIP: accumulated changes 2026-05-25 16:24:21 -05:00
LeanGPT Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
Semantics refactor(ssms): clean f_eps/omf_eps proof; restructure ko_preserves_hyperbola_approx 2026-05-27 16:49:05 -05:00
CHAIN_ALL_REVIEW_REPORT.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00