Re-normalize round53's rounded mantissa back into 53 bits - #1524

Approving. The fix is correct, and I verified it by exhaustive/differential sweep rather than by re-running the examples in the proof.

What the change actually does

The two return sites in round53 collapse into one up expression plus a
decreaseMantissa(...)(twoPow53) on the result. I checked the collapse is
semantically identical to the old branches: up = cond ? m53 & 1n : o54 is
exactly odd on the tie path and o54 otherwise. So the only behavioural
delta is the re-normalization.

The carry case is m53 + up === 2^53 exactly, which decreaseMantissa shifts
once to 2^52 with e + 1. The dropped bit is 0, so no second rounding
decision — the JSDoc's argument holds.

Boundary inputs, derived independently

I constructed the all-ones and just-below cases myself rather than trusting the
proof's choices. Mantissa bit-widths in brackets:

The just-below case does not carry on either side, which is the control I
wanted: the fix is not shifting unconditionally.

Exhaustive / systematic verification

Two sweeps, both against a trusted oracle.

Oracle sweep — 5,228,298 inputs (every mantissa 1..200000 at
e ∈ {0,±1,±2,±3,-5,-10}, the top 4096 and the ±2048 neighbourhood of every
power of two up to 2^70, plus 300k pseudo-random (m, e) with |m| up to 90
bits and e ∈ [-20, 20], both signs throughout). For each I asserted
abs(m) < 2^53 and that m · 2^e equals Number("<m>e<e>") — JS
string-to-number is correctly rounded half-to-even, so it is a genuine
independent oracle for this function.

main:    {checked: 5228298, widthFails: 77828, valueFails: 0}
this PR: {checked: 5228298, widthFails: 0,     valueFails: 0}

Exact differential, main vs this head — 7,989,926 inputs (top-8192 band of
every bit-width up to 80; every mantissa 1..120000 at 12 exponents; a carry hunt
over bit-widths 40..90 at 13 exponents from -40 to 40). Outputs compared as
exact rationals, not through Number:

{n: 7989926, reprDiff: 404024, valDiff: 0, wideMain: 404024, widePr: 0}

So: 404,024 inputs get a different (mantissa, exponent) pair than main, and
every one of them is one of main's oversized results — reprDiff and
wideMain are the same set. Zero inputs change numeric value. Nothing outside
the carry case moved.

Mutation testing

Reverted just the fix in place (return [m53 + up, e53]) and ran the bigfloat
proof groups individually:

decToBin:         0/19 killed
roundingPositive: 0/7  killed
roundingNegative: 0/7  killed
roundingCarry:    4/4  killed

All four new cases are load-bearing, and the 33 pre-existing cases detect
nothing — which is the same statement as "this mutation kills nothing on
main", since main's round53 is the mutation and its suite is green
(2531/2531).

Worth noting alongside that: npm run cov reports bigfloat/module.f.mjs at
100.00 / 100.00 / 100.00 on main and on this head. The bug lived under
full line and branch coverage, so the four new value assertions are the only
thing that could have caught it.

Rest of the battery

• npx tsc --noEmit → 0.
• npm run prepack from a clean tree → 0.
• npm test: 2535 pass / 0 fail, vs 2531 on main — exactly the four new cases.
• Public surface: type-alias extract is byte-identical to main (526 entries);
  normalized const-signature diff is 0 deltas over 898 entries. decToBin's
  emitted signature is unchanged; the only .d.mts delta is the new JSDoc prose
  and proof.roundingCarry. No elided / any anywhere in bigfloat.
• No in-repo consumer of decToBin outside its own proof, so the representation
  change is unobservable today — consistent with what the todo said.

CHANGELOG

§8.3 clean: entry present for a code change, links only /pull/1524, in
Unreleased, no released section touched, ~200 chars.

It characterises the change correctly — "no longer returns a 54-bit mantissa …
always a binary64 significand" is exactly what my differential measured, and it
does state plainly that the returned pair is different for those inputs. I
considered whether §8.4 applies and concluded it does not: the numeric value is
unchanged (valDiff: 0 over 8M inputs), there is no consumer, and the published
type surface is identical. That matches how #1522 and #1514 — both
output-correcting fixes — are worded in the same section, while #1516 took the
prefix because serialized data had to be regenerated.

If you want one more half-sentence, "the value is unchanged; only the
representation moves one bit right" would save a reader the derivation, but the
entry is fine as it stands.

One nit, non-blocking

Deleting fjs/types/bigfloat/todo/round53-overflow.md strands the link to it in
its sibling:

fjs/types/bigfloat/todo/from-decimal.md:39
- [round53-overflow](round53-overflow.md) — `decToBin`, the next stage of the
  same pipeline

Broken relative markdown links go 140 → 141, and diffing the sets shows that
one entry as the only addition. The Related bullet is also stale in substance
now that the work is done, so it wants deleting rather than repointing. Tiny,
and against a 140-link baseline, but it is the one thing this PR introduces.

Everything else checks out. The todo's four tasks are all done, including the
magnitude-based assertion it specifically warned about (m < 2^53 would have
been vacuous for the negative cases — the proof uses abs(m)).

Re-reviewed at 8f359a3. I approved this at e3f47fb; the delta since then is two commits — dropping the stale round53-overflow link and the decToBin JSDoc/postcondition correction. Still clean, and the open nit from last time is fixed.

The delta is not logic

git diff e3f47fb..8f359a3 touches four files: module.f.mjs (JSDoc only — no
statement changed), proof.f.mjs (+2 cases), a new
todo/binary64-exponent-range.md, and the two stale link lines removed from
todo/from-decimal.md. Since round53/decToBin behaviour is untouched I did
not re-run the exhaustive differential from the previous review; I did re-run the
rest of the battery.

Verified

• npx tsc --noEmit — 0. npm run prepack from a clean tree — 0.
• npm test — 2537 pass / 0 fail, vs 2531 on origin/main (28a2e99).
  +6 = the 4 cases from the first round plus the 2 new farExponent ones.
• Public surface diff (extract.mjs + consts.mjs, both trees after prepack;
  46 KB / 65 KB of output, so not a vacuous empty compare) — byte-identical
  to main. No new export type, prefixed or otherwise.
• Broken-link sets — 140 on both trees, and diff of the sorted sets is
  empty. That closes the nit from the last review: deleting
  todo/round53-overflow.md had stranded the link in from-decimal.md:39 and
  taken the set 140 → 141; feaf7e3 removes the reference and the set is back to
  exactly main's.
• npm run cov — fjs/types/bigfloat/module.f.mjs at 100.00 / 100.00 /
  100.00 (line/branch/function); repo total 99.94 / 98.17 / 99.73.

The two new proof cases are correct, and so is the todo

I re-derived both farExponent expectations independently (exact BigInt
scaling of 10^±n, then a half-to-even round to 53 bits written from scratch,
not the module's):

• [1n, -320] → 0x1f_a017_12e8_f047n, -1116 ✔
• [1n, 400] → 0x1b_4ec7_f919_73ffn, 1276 ✔ — both exactly 53 bits.

Worth stating plainly, since it is easy to assume otherwise: these two also
pass on origin/main. They do not discriminate the round53 fix — they pin
the newly documented "width holds at every scale" contract, which is what the
comment above them says they do. The fix's discriminating cases are still the
four from the first round.

I also spot-checked binary64-exponent-range.md rather than taking it on faith,
and every checkable claim in it holds: all five rows of the table reproduce
exactly, and the double-rounding counter-example is real — with q = 2^44 + 1
and the input just below the subnormal tie point, the correctly-rounded double
is 0x100000000001, decToBin lands exactly on the tie [0x10_0000_0000_0180n, -1082], and grid-rounding that half-to-even goes to 0x100000000002, one ulp
off. The JSDoc's retraction of the binary64-exponent-range claim is therefore an
accuracy fix, not a hedge.

Conventions

CHANGELOG entry is present, links only /pull/1524, sits in Unreleased, and
describes the code change (the docs-only commits correctly get none). The new
todo/ file gets no entry, per §8.3.

Approving.