docs(adr): ADR 005 answers three Copilot findings on 66f317e1 (improvise-l2b8)

Detect real precision loss, not a scale decrease; Overflow bullet follows Q13 (b); SUM states both exactness conditions.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze

context/adr/005-exact-decimal-arithmetic.md

@@ -640,12 +640,22 @@ is not. So `Num`'s arithmetic must **detect** either one and return `Inexact`. I
 never return a rounded `Exact`. A rounded value that calls itself exact is the one
 outcome this design exists to prevent.
 
-**Detection is cheap, and it reads the scale.** The exact result of `a + b` or `a - b`
-has scale `max(sa, sb)`, and of `a * b` has scale `sa + sb`. A result whose scale is
-smaller was rounded. `1000 + 0.333…` (28 places) comes back at scale 25, and
-`0.1234567890123456²` at 28 against an exact 32. The test can report a false positive
-only where the dropped digits were zeros, and that direction is safe: the value demotes
-to inexact but is not wrong. Division has its own test (clause 5).
+**Detection reads the scale, then checks that the dropped digits were not zeros**
+(revision 7, Copilot on `66f317e1`). The exact result of `a + b` or `a - b` has scale
+`max(sa, sb)`, and of `a * b` has scale `sa + sb`. A returned scale that is smaller is a
+*hint* of rounding, not proof. `1000 + 0.333…` (28 places) comes back at scale 25, and
+`0.1234567890123456²` at 28 against an exact 32. Revision 6 demoted on the hint alone and
+called the zero-digit case a safe false positive. It is not safe: it breaks question 13's
+decided rule that a stored value is exact iff it fits. `1.2500000000000000 *
+4.0000000000000000` (scale 16 each) has the exact value `5` at scale 32, which is
+`5·10³²` as an integer and does not fit 96 bits, yet `5` fits a `Decimal`. So on the hint
+the arithmetic recomputes the exact integer result in the 256-bit integer clause 8
+already uses (a product of two 96-bit mantissas is below 2¹⁹², and an aligned sum below
+2¹⁹⁰), strips its trailing zeros, and returns exact iff the stripped mantissa fits 96
+bits at a scale of at most 28. Otherwise the value is not a `Decimal`, and goes to the
+fraction arm and then f64 as below. The recompute runs only when the scale hint fires, so
+the common path is unchanged. This is a design for the implementer and is **not
+measured**. Division has its own test (clause 5).
 
 This is not rare in practice, and the review showed why. Clause 10 loads an old file's
 17-digit f64 spellings as exact, so `0.30000000000000004 + 1e12` needs 29 significant
@@ -820,8 +830,12 @@ further to `inf` only at the inexact level.
   order-dependent `SUM` as a class for exact data, which is nearly all data.
 - **Inexact values are summed by ADR 009's exact f64 accumulator** when it lands, and by
   today's fold until then.
-- **The result is exact if every value was exact** and the exact total fits a `Decimal`.
-  Otherwise it is inexact. **It must not be a fold with contagion part-way through.**
+- **The result is exact if every value was exact** and the exact total fits the stored
+  bound: a `Decimal`, or, under option (d), an `i128` fraction (a sum of fractions can
+  fit the fraction arm without fitting a `Decimal`). **A second condition applies to
+  fractions:** if the sum holds more than K = 32 non-decimal denominator groups it reads
+  the inexact f64 accumulator, so it is inexact **even when its exact total would have
+  fitted** (clause 8's recommendation below, question 16). Otherwise it is inexact. **It must not be a fold with contagion part-way through.**
   Such a fold switches to f64 at the first inexact value in store order, so the answer
   would depend on where that value sits.
 
@@ -1289,16 +1303,16 @@ pub enum Num {
 
 - **Division stays exact.** `10/3` is `Fraction(10/3)`, and `10/3 × 3` is exactly `10`,
   which normalizes back to `Exact(10)`. Both measured.
-- **Overflow demotes.** As written here, *every operation* is bounded. Question 13
-  proposes bounding only the stored result instead, and if it is answered that way,
-  this bullet applies at the store rather than per operation. Every operation uses
-  checked `i128` arithmetic after the gcd
-  reduction (`num-rational`'s `checked_add`/`checked_mul`/`checked_div` do exactly
-  this). A `None` **may** mean the reduced result does not fit. It may also mean an
-  intermediate overflowed while the reduced result would have fitted, because
-  `checked_add` goes through the lcm of the denominators. Either way the value demotes
-  to `Inexact`. That is safe, because it only demotes, and it is deterministic. The
-  demotion is the correctly rounded f64 of the exact fraction.
+- **Overflow demotes at the store** (question 13, decided (b); revision 7 replaced the
+  per-operation wording, which Copilot found contradicted it). The fast path uses
+  checked `i128` arithmetic after the gcd reduction (`num-rational`'s
+  `checked_add`/`checked_mul`/`checked_div` do exactly this). A `None` **may** mean the
+  reduced result does not fit, and **may** mean only that an intermediate overflowed
+  (`checked_add` goes through the lcm of the denominators) while the reduced result
+  fits. So a `None` widens that step to a bigint rational and the **stored** result is
+  tested against the `i128` bound: exact iff it fits, else the correctly rounded f64 of
+  the exact fraction, which is `Inexact`. It is deterministic. Past question 13's
+  ceiling, the intermediate demotes (the one stated exception).
 
   Revision 3 cited `Ratio<i128>::to_f64` agreeing with `BigRational`'s conversion. That
   was **circular**: both share `num-rational`'s one `ratio_to_f64` routine. The review
@@ -1729,7 +1743,9 @@ open. Nothing is renumbered.
     written. `a × (b + c)` and `a × b + a × c` are the same number, but an intermediate
     can overflow in one spelling and not the other, so one is exact and the other a
     demoted f64. Under (b) the rule is one sentence: **a stored value is exact if and
-    only if it fits.** Algebraically equal formulas give equal values.
+    only if it fits.** Algebraically equal formulas give equal values. (Two stated
+    exceptions: the ceiling below, and a `SUM` of more than K = 32 non-decimal
+    denominator groups, which reads inexact by question 16 whatever its value.)
 
     **The rule has one exception, and it is stated rather than hedged** (revision 5,
     the review of `87ae21ca`):