allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/0-Core-Formalism/lean
History
Brandon Schneider 1a407b51de fix(FixedPoint): revert abs_triangle to admit — q16Clamp sign analysis still blocked 
abs_triangle: reverted to admit. The q16Clamp applies Int.abs internally, making
sign analysis after division non-trivial. Attempted proofs using Int.sign,
Int.sign_mul_abs, Int.ediv_neg_pos_of_neg, Int.mul_ediv_le all failed (missing
theorems in this Mathlib version).

Key theorem: mul_mono_left and mul_mono_right are proved and working.

Build: 3313 jobs, 0 errors (lake build)
2026-05-27 17:15:52 -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 fix(FixedPoint): revert abs_triangle to admit — q16Clamp sign analysis still blocked 2026-05-27 17:15:52 -05:00
CHAIN_ALL_REVIEW_REPORT.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00