mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
b8299e209f
FixedPoint.lean: - mul_mono_left: proved via Int.mul_le_mul_of_nonneg_right + Int.ediv_le_ediv with explicit hpos : 0 < q16Scale proof (not synthesized by norm_num) - mul_mono_right: proved via Int.mul_le_mul_of_nonneg_left + same pattern - abs_triangle: reverted to admit — q16Clamp applies Int.abs internally making sign analysis non-trivial; needs case split on sign of (a*b)/q16Scale SSMS.lean: - t2 (line 617): corrected first arg from cT i - cT j to Q16_16.abs (cT i - cT j) to match available hcand hypothesis - t1 (line 606-614): fixed admit in inner proof with proper h_diff_nonneg + lt_of_ge_of_le chain using h_aciBound_nonneg - AGENTS.md: updated status — mul_mono_left/right are proved, abs_triangle is the critical remaining blocker for aciPreservedByMlgruStep Build: 3313 jobs, 0 errors (lake build) |
||
|---|---|---|
| .. | ||
| conversions/hardware | ||
| external/OTOM | ||
| LeanGPT | ||
| Semantics | ||
| CHAIN_ALL_REVIEW_REPORT.md | ||