From d722caee54e6481ce969891b3138c86e8cdd145f Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 23:51:18 -0500 Subject: [PATCH] =?UTF-8?q?feat(lean):=20add=20ofRawInt=5Fmonotone=20+=20a?= =?UTF-8?q?dd=5Fnonneg=5Fmonotone=20to=20FixedPoint;=20generalise=20Motif?= =?UTF-8?q?=20=C2=A76.2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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> --- .../lean/Semantics/Semantics/FixedPoint.lean | 48 +++++++++++++++++++ .../lean/Semantics/Semantics/PIST/Motif.lean | 20 ++++---- 2 files changed, 59 insertions(+), 9 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean index fe253c36..1db9574f 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean @@ -405,6 +405,54 @@ theorem ofRawInt_toInt_eq_general (i : Int) (h1 : i ≥ 0) : unfold ofRawInt toInt simp [h, hlo] +/-- `ofRawInt` is monotone: a ≤ b → (ofRawInt a).toInt ≤ (ofRawInt b).toInt. + The clamping constructor preserves order: both clamp endpoints are the same + fixed bound, and the in-range branch is identity. -/ +theorem ofRawInt_monotone (a b : Int) (h : a ≤ b) : + (ofRawInt a).toInt ≤ (ofRawInt b).toInt := by + unfold ofRawInt toInt + by_cases ha_hi : a > q16MaxRaw + · -- a clamped high → result_a = q16MaxRaw + simp only [ha_hi, ↓reduceIte] + by_cases hb_hi : b > q16MaxRaw + · -- b also clamped high → result_b = q16MaxRaw; q16MaxRaw ≤ q16MaxRaw + simp [hb_hi] + · by_cases hb_lo : b < q16MinRaw + · -- a ≤ b, a > max, b < min: impossible + simp [hb_hi, hb_lo]; dsimp [q16MinRaw, q16MaxRaw] at *; omega + · -- b in range → result_b = b; need q16MaxRaw ≤ b, but a > max and a ≤ b gives b > max: contradiction + simp [hb_hi, hb_lo]; dsimp [q16MaxRaw] at *; omega + · by_cases ha_lo : a < q16MinRaw + · -- a clamped low → result_a = q16MinRaw + simp only [ha_hi, ha_lo, ↓reduceIte] + by_cases hb_hi : b > q16MaxRaw + · -- result_b = q16MaxRaw; q16MinRaw ≤ q16MaxRaw + simp [hb_hi]; dsimp [q16MinRaw, q16MaxRaw] at *; omega + · by_cases hb_lo : b < q16MinRaw + · -- b also clamped low → result_b = q16MinRaw; q16MinRaw ≤ q16MinRaw + simp [hb_hi, hb_lo] + · -- b in range → result_b = b; q16MinRaw ≤ b + simp [hb_hi, hb_lo]; dsimp [q16MinRaw] at *; omega + · -- a in range → result_a = a + simp only [ha_hi, ha_lo, ↓reduceIte] + by_cases hb_hi : b > q16MaxRaw + · -- result_b = q16MaxRaw; a ≤ q16MaxRaw (from a's in-range bounds) + simp [hb_hi]; dsimp [q16MaxRaw] at *; omega + · by_cases hb_lo : b < q16MinRaw + · -- b < min but b ≥ a ≥ min: impossible + simp [hb_hi, hb_lo]; dsimp [q16MinRaw] at *; omega + · -- b in range → result_b = b; a ≤ b + simp [hb_hi, hb_lo]; exact h + +/-- Adding a nonnegative Q16_16 value cannot decrease the saturated result. + This is the general form of the motif-scoring monotonicity used in + Semantics.PIST.Motif §6.2: motifScore(match=true) ≥ motifScore(match=false). -/ +theorem add_nonneg_monotone (a b : Q16_16) (hb : 0 ≤ b.toInt) : + a.toInt ≤ (add a b).toInt := by + unfold add + have := ofRawInt_monotone a.toInt (a.toInt + b.toInt) (by omega) + rwa [ofRawInt_toInt] at this + /-- zero * a = zero. -/ theorem zero_mul (a : Q16_16) : mul zero a = zero := by unfold mul diff --git a/0-Core-Formalism/lean/Semantics/Semantics/PIST/Motif.lean b/0-Core-Formalism/lean/Semantics/Semantics/PIST/Motif.lean index 44596df8..d6cf9f0f 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/PIST/Motif.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/PIST/Motif.lean @@ -165,15 +165,17 @@ def topKMotifs (k : Nat) (candidates : List MotifCandidate) : List MotifCandidat -- §6.1 familyMatchBonus is strictly positive theorem motifScore_bonus_pos : 0 < familyMatchBonus.toInt := by decide --- §6.2 Concrete witness: matching score ≥ non-matching score at freq=3, lib=10. --- (A general proof over all MotifInputs requires reasoning about Q16_16.add --- clamping behaviour; deferred as TODO(lean-port).) --- TODO(lean-port): Generalise to all MotifInputs once Q16_16.add_nonneg_monotone --- is proved in FixedPoint.lean (i.e., 0 ≤ bonus → (base + bonus).toInt ≥ base.toInt). -theorem motifScore_match_ge_base_witness : - (motifScore { frequency := 3, librarySize := 10, familyMatch := true }).toInt ≥ - (motifScore { frequency := 3, librarySize := 10, familyMatch := false }).toInt := by - decide +-- §6.2 General theorem: matching score ≥ non-matching score for all MotifInputs. +-- Proof: motifScore(match=true) = base + familyMatchBonus; +-- motifScore(match=false) = base. +-- familyMatchBonus.toInt ≥ 0 (proved by decide below), so +-- Q16_16.add_nonneg_monotone gives base.toInt ≤ (base + bonus).toInt. +theorem motifScore_match_ge_base (x : MotifInputs) : + (motifScore { x with familyMatch := true }).toInt ≥ + (motifScore { x with familyMatch := false }).toInt := by + simp only [motifScore, baseScore] + have hbonus : 0 ≤ familyMatchBonus.toInt := by decide + exact Q16_16.add_nonneg_monotone _ _ hbonus -- §6.3 Zero frequency → base score is zero regardless of library size theorem motifScore_zero_freq_base (lib : Nat) (fm : Bool) :