[jiro-by-nori]

Fixes #141.

Authored by Jiro, an autonomous agent (Nori sessions) on behalf of @sam-xif.

What was wrong

A Ruby float literal exported as a JSON number, and the model decoded it with
JsonNumber.toFloat, i.e. OfScientific.ofScientific mantissa true exponent.
That keeps 64 bits of mantissa and truncates before the final rounding, so it
double-rounds: for some literals the model's double is one ulp away from the
one CRuby's strtod produces. A silent wrong answer, not a gate.

Program	CRuby 4.0.5	before	after
p 403355592039198e57	4.03355592039198e+71	4.0335559203919798e+71	same as CRuby
a = 5.724162270483689e-257; b = 5.7241622704836886e-257; p [a == b, a > b]	[false, true]	[true, false]	same

The second row is the sharper witness: the two literals are different doubles
(0abb80e67590c875 and 0abb80e67590c874) and the model collapsed them.

The fix

The export writes a float literal as ["flt_bits", <UInt64>] — the head the
imaginary-component path already used — so no decimal-to-binary64 conversion
happens inside the model; Float.ofBits finishes the job on exact bits. The
number never travels through OfScientific.

• desugar/lib/export.rb: a [:flt, f] node exports as its bits (the finite
  and payload checks stay, as ArgumentErrors). imag's component goes through
  the same path, so the two cannot drift.
• ruby-lean/RubyCore/Syntax.lean: ["flt", number] stays readable, for a
  document written before this. No new head, so Export::VERSION does not move.
• books/Books/TypeSoundness/Checker/Lang/Expr.lean: the checker's own copy of
  the decoder gains flt_bits the same way (its .flt already carried bits).
• books/scripts/emit_deriv.rb: fltLit reads the bits; ["flt", number] is
  still accepted.
• ruby-lean/RubyCore/Generated/PreludeJson.lean is regenerated (make gen
  equivalent). The prelude has one float literal — def to_f = 0.0 — and the
  regenerated Prelude.lean is byte-identical, so nothing the proofs see moves.
  Most of that file's diff is the fixed-width line re-wrapping the chunked JSON
  string, shift-and-all from the changed node.

-0.0 and the imaginary path are unchanged in behaviour: p -0.0 and
p 1.5i still agree with CRuby. The -0.0 literal keeps its -@ normal form
(the desugared shape is pinned by desugar/test/test_variants.rb); only the
comment explaining why changed, because the reason it gave (JSON cannot carry
a negative zero) no longer holds.

Test plan

New regression case difftest/corpus/regressions/float-literal-double-round.rb
(status: fixed), replayed by every make conformance: both witnesses above,
and p [a, b] to pin that the two literals stay distinct.

How I validated, on this branch:

• Before/after, on the same machine: bin/ruby-lean --compare on both
  witnesses is DIFFER on main (model 4.0335559203919798e+71, [true, false]) and AGREE on this branch.
• make conformance — ran 1287, agree 1087, sut_unsupported 194, not_compared 6, disagree 0: CONFORMANCE OK, the baseline holds exactly. The
  new regression case is held; the regressions tier is 222 held / 1 gated /
  0 failures, and the tier3 replay is 57 agree / 0 disagree.
• make soundness — SOUNDNESS CHECK PASSED. The corpus pipeline rebuilds
  every AST (now with flt_bits) and validateD accepts 140/268, exactly the
  set in corpus/accepted.txt; 007-flt-lit is among them, so the checker's
  new decode path is exercised.
• make books (1403 jobs), make metatheory (axiom audit included),
  make comparator (Your solution is okay!), make book-checks
  (FastPower 72/72, LoopSum AGREE), make feature-loading (AGREE).
• make desugar-test — 1257 agree, 0 disagree, 76 out-of-fragment, rule
  coverage 76/76. make desugar-coverage — in-fragment 1211/1282, the baseline.
• make desugar-unit — 921 runs, 0 failures; branch coverage moved up
  (88.91 → 88.92) and the baseline is recorded in this commit, as the check
  asks. make emitter-unit — 368 runs, 0 failures, coverage holds (a new test
  drives both the flt_bits and the legacy flt arm, so neither is uncovered).
• make difftest-test — 189 passed, coverage holds. make docs
  (mkdocs build --strict), make gen-check (all four generated files fresh),
  make check-not-weakened (CHECKS NOT WEAKENED), make ci-sync.
• make lint-equivalent: rubocop over the tree (44 files, no offenses), ruff format --check and ruff check (115 files, clean). shellcheck and actionlint
  cover files this change does not touch.

Found while testing, not fixed here

-0.0 as a sub-expression still takes the -@ route, which is now
unnecessary but harmless; changing it would move the pinned normal form for no
behavioural gain, so it is left alone.