diff --git a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md
index 8f7b3505c..ecc009c64 100644
--- a/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md
+++ b/kmir/src/kmir/kdist/mir-semantics/symbolic/spl-token.md
@@ -533,6 +533,22 @@ The `#initBorrow` helper resets borrow counters to 0 and sets the correct dynami
     [preserves-definedness]
 ```
 
+## Rent minimum_balance calculation simplification
+
+The rent exemption check involves: `(int)((float)(data_len * lamports_per_byte_year) * 2.0)`
+Since float casts create thunks, we simplify this pattern directly to `PRODUCT * 2`.
+
+```k
+  // Simplify: (int)((float)PRODUCT * 2.0) => PRODUCT * 2
+  rule #cast(
+         thunk(#applyBinOp(binOpMul,
+           thunk(#cast(Integer(PRODUCT:Int, 64, false), castKindIntToFloat, INT_TY, FLOAT_TY)),
+           Float(0.20000000000000000e1, 64),
+           false)),
+         castKindFloatToInt, FLOAT_TY, INT_TY)
+    => Integer(PRODUCT *Int 2, 64, false)
+```
+
 ```k
 endmodule
 ```