bposit: encoding + spec (bound the taper, prove TwoSum/TwoProduct exactness)

[Ravenwater]

Part of Epic #1250 (bposit). First sub-issue: nail down the encoding and prove the EFT-exactness property before any implementation, since that property is the entire reason bposit exists (see #1247 / #1249 for why tapered posit fails it).

Goal

Specify how bposit bounds the posit taper so the fraction field is never empty, and establish the exact condition under which TwoSum and TwoProduct are exact for the format. Deliver a written spec + a reference encoding + an exhaustive validation for a small config.

Encoding -- decisions to resolve

Starting from modern posit (posit<nbits, es, bt>: sign / variable-length regime / up-to-es exponent / remaining fraction), where near maxpos/minpos the regime consumes the field and the fraction (and exponent) bits vanish:

1. How is the taper bounded?
   • (a) Regime cap: limit the regime run length to R_max = nbits - 1 - es - F_min, guaranteeing at least F_min fraction bits and the full es exponent at every magnitude. Values beyond the cap saturate to maxpos/minpos.
   • (b) Reserve a fixed minimum fraction field another way.
   • Pick one and justify; (a) is the leading candidate.
2. F_min: how many fraction bits are guaranteed minimum? This is the core precision-vs-range dial. Tabulate the dynamic-range / guaranteed-precision trade for a few (nbits, es, F_min).
3. Saturation vs overflow at the bounded extremes (interaction with NaR; does bposit keep posit's single NaR, or gain a saturating maxpos like a clamped format?).
4. Template signature: bposit<nbits, es, bt> with F_min as a 4th parameter, or F_min derived from (nbits, es)?
5. numeric_limits: min / max / lowest / epsilon / round_style / the (now bounded) dynamic range; radix.

bposits do not have TwoSum/TwoProd attributes

For any two representable bposit values a, b, the exact roundoff of a+b (TwoSum) and a*b (TwoProduct) is representable in the EFT residual's domain, making s = RN(a op b); e = (a op b) - s an exact split.

Using b-posits does not help with the TwoSum property, even when there are always fraction bits.

Take the example of 8-bit b-posits with maximum regime size rS = 4 and no exponent bits, eS = 0. The smallest positive value is 9/128 = minPos.

Now suppose x = 9/128 and y = 5/64, both exactly representable as posits. Their exact sum is 19/128, which rounds to 5/32. The error is e = 1/128, but there is no posit value 1/128. So it fails the "two sum" property that the exact sum of two real numbers is always exactly as the sum of two real numbers in the format.

This is why the quire is important and maybe essential. Compensated summation is not the way to go since it does not always work (for floats), whereas quire summation always works.

bposit's precision still varies with magnitude within the bounded band (it is taper-bounded, not fixed-precision), so exactness is not automatic the way it is for IEEE fixed-precision + subnormals -- it must be established, not assumed. Determine the minimum-fraction-bits / regime-cap condition that is actually sufficient, and document any residual-domain requirement (e.g. whether e must be representable as a bposit or in a wider companion domain).

Deliverables

• docs/number-systems/bposit.md: encoding spec, field layout, the bounding rule, dynamic-range/precision profile, numeric_limits, and the EFT-exactness argument. ASCII-only.
• A worked reference encoding table for one small config (e.g. bposit<8,1,F_min=...>): every code point -> value, showing the fraction field is always non-empty.
• Exhaustive EFT validation for a small config: brute-force all a,b pairs of bposit<8,es> (and <10,es>) and confirm twosum/twoprod reconstruct a op b exactly (long-double / dyadic oracle). This is the empirical proof of the property before the full type is built.
• Decision recorded on the template signature and saturation/NaR behavior.

Acceptance

Spec doc merged, small-config encoding table + exhaustive TwoSum/TwoProduct exactness check pass, and the (nbits, es, F_min) -> range/precision trade documented -- enough that the core-type sub-issue can be implemented against a settled encoding.

Part of #1250. Relates to #1247, #1249.