mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
7faed2de0e
FixedPoint.lean — two new theorems:
ofRawInt_monotone (a b : Int) (h : a ≤ b) :
(ofRawInt a).toInt ≤ (ofRawInt b).toInt
— proved by explicit by_cases on all four guard combinations
(a/b each: above max, below min, in range), closing each branch
with simp + dsimp [q16MinRaw/q16MaxRaw] + omega/exact.
add_nonneg_monotone (a b : Q16_16) (hb : 0 ≤ b.toInt) :
a.toInt ≤ (add a b).toInt
— follows from ofRawInt_monotone + ofRawInt_toInt (one rewrite).
Semantics.PIST.Motif §6.2 — upgraded from concrete witness to general theorem:
motifScore_match_ge_base (x : MotifInputs) :
(motifScore {x with familyMatch := true}).toInt ≥
(motifScore {x with familyMatch := false}).toInt
— now proved for all MotifInputs using add_nonneg_monotone,
replacing the earlier TODO(lean-port) placeholder.
Full workspace build: 3570 jobs, 0 errors.
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
|
||
|---|---|---|
| .. | ||
| conversions/hardware | ||
| external/OTOM | ||
| LeanGPT | ||
| Semantics | ||
| CHAIN_ALL_REVIEW_REPORT.md | ||