rule 23: a live-verified module can still be wrong - thin coverage is how; float literals are widened floats

guides/method-rules.md

@@ -270,3 +270,22 @@ shim cross-build failed**, which is exactly the gap rule 13 exists for.
 When both sides add a *member of a construct*, the resolution is to merge them **into that
 construct** — one list, one chain — not to paste one after the other. Read the resolved region
 before committing, and let the cross-build be the judge.
+
+## 23. A live-verified module can still be wrong — thin coverage is how
+
+`ComputeBudget` was compared against the original on **4,437 live calls with 0 divergences** and was
+still wrong: its interest literals are **widened floats** in the image (`(double)0.01f`,
+`(double)0.15f`) and then truncated, so a treasury of exactly 50,000 earns **499, not 500**. Our code
+used exact decimals. Sixteen hand-computed test expectations moved by one when it was fixed.
+
+It survived because those 4,437 calls presented only **20 distinct states, none of them on a
+boundary** — the exact thin-coverage caveat recorded against that lane at the time, later vindicated
+by a different lane doing arithmetic the compare never exercised.
+
+So "live-verified, 0 divergences" is a statement about **the states that occurred**, never about the
+function. Two defences, both cheap: report the distinct-state count next to the call count (rule 15),
+and test the boundaries by hand — a value that lands exactly on a cap, a treasury that divides
+exactly, an empty container.
+
+**A float literal in this image is a widened `float`, not a `double`.** It has now bitten the money
+chain, the bankruptcy divisor and the gate constant. Read the four bytes; do not assume the decimal.