From ca5d947a295f09f06af4900048a1b5f6fa0a9247 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 23:34:55 -0500 Subject: [PATCH] refactor(lean): replace native_decide with decide in PIST.Repair invariants MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit All 8 invariant theorems in Semantics.PIST.Repair now use decide instead of native_decide. The kernel reducer handles the Q16_16 subtype arithmetic (ofRatio, mul, sub, add) without timeout — build time drops from 2.0s to 1.0s. Compiler boundary (RRC/Emit, AVMIsa/Emit, RRC/Corpus278) had zero native_decide calls already; this cleans up the PIST workspace modules to match. Generated with [Devin](https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- .../lean/Semantics/Semantics/PIST/Repair.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/PIST/Repair.lean b/0-Core-Formalism/lean/Semantics/Semantics/PIST/Repair.lean index 8b44345e..23484e01 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/PIST/Repair.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/PIST/Repair.lean @@ -183,7 +183,7 @@ def rankPatchesDefault (patches : List Patch) : List Patch := theorem defaultWeights_sum : defaultWeights.α.toInt + defaultWeights.β.toInt + defaultWeights.γ.toInt + defaultWeights.δ.toInt = 65534 := by - native_decide + decide -- §6.2 Every weight is strictly positive theorem defaultWeights_pos : @@ -191,7 +191,7 @@ theorem defaultWeights_pos : 0 < defaultWeights.β.toInt ∧ 0 < defaultWeights.γ.toInt ∧ 0 < defaultWeights.δ.toInt := by - native_decide + decide -- §6.3 α is the dominant weight (α > β > γ > δ) -- This is what the Python comment implies: specificity matters most. @@ -199,7 +199,7 @@ theorem defaultWeights_ordered : defaultWeights.δ.toInt < defaultWeights.γ.toInt ∧ defaultWeights.γ.toInt < defaultWeights.β.toInt ∧ defaultWeights.β.toInt < defaultWeights.α.toInt := by - native_decide + decide -- §6.4 rankScore with defaultWeights on the all-zero input is negative. -- Note: mkInputs zero zero zero derives residual_risk = 1 - 0 = 1 (= one). @@ -207,15 +207,15 @@ theorem defaultWeights_ordered : -- The score is strictly negative, confirming δ > 0. theorem rankScore_zero_inputs_negative : (rankScoreDefault (mkInputs zero zero zero)).toInt < 0 := by - native_decide + decide -- §6.5 residualRisk complement: embedResidualRisk(1) = 0 (exact on Q16_16.one) theorem embedResidualRisk_one : embedResidualRisk one = zero := by - native_decide + decide -- §6.6 residualRisk complement: embedResidualRisk(0) = 1 theorem embedResidualRisk_zero : embedResidualRisk zero = one := by - native_decide + decide -- §6.7 Monotonicity of score in specificity (all else equal): -- Higher specificity → higher score (net coefficient α − δ > 0). @@ -223,7 +223,7 @@ theorem embedResidualRisk_zero : embedResidualRisk zero = one := by theorem rankScore_monotone_specificity_witness : (rankScoreDefault (mkInputs (ofRatio 91 100) (ofRatio 12 100) (ofRatio 67 100))).toInt > (rankScoreDefault (mkInputs (ofRatio 50 100) (ofRatio 12 100) (ofRatio 67 100))).toInt := by - native_decide + decide -- §6.8 No-promotion theorem: a zero-specificity/zero-prior patch never outscores -- a maximum-specificity/maximum-prior patch (same cost). @@ -231,6 +231,6 @@ theorem rankScore_monotone_specificity_witness : theorem rankScore_zero_lt_full : (rankScoreDefault (mkInputs zero zero zero)).toInt < (rankScoreDefault (mkInputs one zero one)).toInt := by - native_decide + decide end Semantics.PIST.Repair