diff --git a/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean b/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean
index 2afe5b62..50f08a26 100644
--- a/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean
+++ b/0-Core-Formalism/lean/SilverSight/SilverSight/HardwareContentionMarkov.lean
@@ -53,23 +53,29 @@ def measuredRingRate : Q16_16 := Q16_16.ofRatio 105127 100
 
 /-- Self-loop ordering: SUBLEQ has more contention than ring. -/
 theorem subleq_contention_gt_ring : subleqSelfLoop.val >= ringSelfLoop.val := by
-  native_decide
+  unfold subleqSelfLoop ringSelfLoop Q16_16.ofRatio Q16_16.zero
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 /-- Self-loop ordering: CL has more contention than SUBLEQ. -/
 theorem cl_contention_gt_subleq : clSelfLoop.val >= subleqSelfLoop.val := by
-  native_decide
+  unfold clSelfLoop subleqSelfLoop Q16_16.ofRatio
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 /-- Mixing model: ringRate equals measuredRingRate exactly. -/
 theorem ring_rate_match : ringRate.val = measuredRingRate.val := by
-  native_decide
+  unfold ringRate measuredRingRate baseRate mixingRate ringSelfLoop
+  unfold Q16_16.ofRatio Q16_16.zero Q16_16.one Q16_16.sub Q16_16.mul
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 /-- Throughput ordering: ring is fastest. -/
 theorem ring_fastest : measuredRingRate.val >= measuredWordRate.val := by
-  native_decide
+  unfold measuredRingRate measuredWordRate Q16_16.ofRatio
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 /-- Throughput ordering: word is faster than CL. -/
 theorem word_faster_than_cl : measuredWordRate.val >= measuredClRate.val := by
-  native_decide
+  unfold measuredWordRate measuredClRate Q16_16.ofRatio
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 /--
 Cache tunnel miss probability per instruction.
@@ -96,10 +102,14 @@ Applying throughput_antitone to our three chains:
   ringRate >= wordRate >= clRate
 -/
 theorem ring_rate_gte_word : ringRate.val >= wordRate.val := by
-  native_decide
+  unfold ringRate wordRate baseRate mixingRate ringSelfLoop subleqSelfLoop
+  unfold Q16_16.ofRatio Q16_16.zero Q16_16.one Q16_16.sub Q16_16.mul
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 theorem word_rate_gte_cl : wordRate.val >= clRate.val := by
-  native_decide
+  unfold wordRate clRate baseRate mixingRate subleqSelfLoop clSelfLoop
+  unfold Q16_16.ofRatio Q16_16.one Q16_16.sub Q16_16.mul
+  simp [Q16_16.scale, q16Scale, Q16_16.toInt, q16Clamp, q16MaxRaw, q16MinRaw]
 
 #eval subleqSelfLoop
 #eval mixingRate baseRate subleqSelfLoop