[jiro-by-nori]

Summary

Fixes #115.

Range#count was alias count size, so a Range answered the size where
CRuby's Enumerable#count counts: the block form silently answered the wrong
number ((1..5).count { |x| x > 2 } → 5, CRuby → 3), and the item form was
rejected with size's arity error (given 1, expected 0) instead of counting.
Array#count goes through Enumerable#count and is right, so the two
collections disagreed with each other as well as with CRuby.

Written by Jiro, an autonomous coding agent; the code and this description are
its work.

What changed

ruby-lean/prelude/prelude.rb (plus the regenerated Prelude.lean and
PreludeJson.lean; no other generated file moves):

• Range#count is its own method. CRuby's enum_count defers to size
  only for the bare form and counts matches otherwise, so:
  • no argument, no block → size, unchanged and still O(1) (size is what
    enum_count asks for anyway);
  • a block → counts matches through each;
  • an item argument → the existing named gate
    Enumerable#count with an argument, the same one Enumerable#count
    already gives every other collection (an Array included), rather than an
    answer only some receivers give.
• Range#each refuses a begin CRuby refuses. Iteration is succ, and CRuby
  has no iteration story for a Float begin: (1.0..3.0).each is TypeError: can't iterate from Float. The model leaked its own succ NoMethodError,
  which the block form of count now reaches, so each raises CRuby's
  TypeError for a begin that is not Integer, String or Symbol. A
  beginless/endless range is still the existing named gate, and a String
  range still gates on String#succ.

difftest/corpus/regressions/range-count-block (.rb + .json) pins 13 shapes
of the family against CRuby 4.0.5: bare, exclusive and empty ranges, the block
form (some / none / all / truthy / one element), size's unchanged arity, and
the Float refusal from both each and count.

Test plan

Every check was run on the final tree, on this machine (Lean
leanprover/lean4:v4.32.2, CRuby 4.0.5).

Check	Result
Row-by-row against CRuby, bin/ruby-lean --compare-style probe	the whole table below agrees, or gates
New regression case, difftest replay (lean SUT)	agree
difftest run --tier regressions	221 held, 1 gated (the pre-existing open case), 0 failures

The table from #115, after the change:

expression	model	CRuby 4.0.5
(1..5).count	5	5
(1...5).count	4	4
(1..0).count	0	0
(1..5).count { |x| x > 2 }	3	3
(1..5).count { |x| x }	5	5
(1..5).size(1)	ArgumentError (given 1, expected 0)	same
(1..5).count(2)	gates: Enumerable#count with an argument	1
(1..5).count(2) { }	gates: Enumerable#count with an argument	1 (with a "block not used" warning)
(1.0..3.0).each { }	TypeError: can't iterate from Float	same
(1.0..3.0).count { |x| x > 1 }	TypeError: can't iterate from Float	same

make check targets, each run to completion:

• make prereqs, make ci-sync — OK
• make lint — ruff, RuboCop (43 files), shellcheck, actionlint: clean
• make gen-check — every generated source fresh (Prelude.lean regenerated
  in this commit)
• make lean, make books (1399 jobs), make metatheory — every theorem rests
  on propext, Classical.choice, Quot.sound only, and the booted heap
  satisfies the assumptions the proofs make about it
• make soundness — SOUNDNESS CHECK PASSED
• make comparator — OK: the comparator accepts
• make desugar-unit (917 runs), make emitter-unit (367 runs),
  make desugar-test (76/76 rules), make desugar-coverage,
  make difftest-test (189 passed) — every coverage baseline holds
• make conformance — CONFORMANCE OK; ran 1287, agree 1087,
  sut_unsupported 194, not_compared 6, disagree 0 — unchanged, so no baseline
  file moved (nothing in the harvested corpus counts a range)
• make feature-loading, make book-checks (72/72 inputs), make docs
• make check-not-weakened — CHECKS NOT WEAKENED

No sorry, native_decide, axiom, lint suppression or test skip was added.