Covers word_source/mixed_arithmetic_words.c. Two genuine findings recorded
in comments rather than fixed:
- register_mixed_arithmetic_words registers MOD and /MOD a second time,
after arithmetic_words.c's own registrations; vm_create_word links new
entries at the head of vm->latest and FIND scans from vm->latest forward,
so arithmetic_words.c's MOD//MOD are permanently shadowed, unreachable
dead code once bootstrap completes (verified against
dictionary_management.c and the module order in word_registry.c).
- M*, M/MOD, and the "avoids intermediate overflow" claim on */ and */MOD
are false on 64-bit builds: cell_t and "long long" are the same width
there, so the long-long intermediate does not actually widen the
product -- it wraps mod 2^64 like plain cell multiplication before the
32-bit-style split/reconstruction runs. M*/M/MOD are left undefined
here (oops-equivalent: documented as not modelled, since formalizing
"the wrong thing, faithfully" adds no proof value) rather than fixed.
MOD//MOD/*//*/MOD reuse cell_sdiv/cell_smod from the arithmetic-words
migration; M+/M- transcribe the C's hand-rolled signed carry/borrow
detection literally, proving only stack-level plumbing (not double-
precision correctness, which needs an interpretation function this
suite doesn't build).
All 24 theory files verify with zero errors.
Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
