[jiro-by-nori]

Fixes #102.

Written by Jiro, an autonomous coding agent (Nori), on behalf of @sam-xif. The commit and this description are the agent's work; nothing here was written by a human.

What was wrong

ary_join_1 emits the separator before every element after the first, at every level. The model flattened nested arrays into one list of rendered parts and then put the separator between parts, so an empty nested array — which renders nothing and therefore pushed no part — lost the boundary its position earned.

expression	before	CRuby 4.0.5
[1, [], 2].join("-")	"1-2"	"1--2"
[[], 1].join("-")	"1"	"-1"
[[], []].join("-")	""	"-"
[1, [[]], 2].join("-")	"1-2"	"1--2"
[[1], []].join("-")	"1"	"1-"
[1, [2, [3, nil]], []].join("-")	"1-2-3"	"1-2-3-"

A wrong answer, not a gate — the failure mode the project treats as a bug.

The change

• ruby-lean/prelude/prelude.rb — the recursive walk renders each element as a unit and recurses with the same separator (__join_collect pushing leaves into a flat list becomes __join_part returning one element's contribution), so every level keeps its own boundaries. It keeps the depth limit the flattening walk had, so a self-referential array is still refused rather than running the machine out of steps.
• ruby-lean/RubyCore/Builtins/Support.lean — joinImpl is exactly CRuby's rule over a flat array. A receiver containing a nested Array now defers to the prelude twin in toAryDefer?, the mechanism that already routes an element answering to_ary there. Deferral is one level deep, which is enough: the prelude walk owns everything below.
• ruby-lean/RubyCore/Generated/{PreludeJson,Prelude}.lean — regenerated (make gen), not edited.
• difftest/corpus/regressions/array-join-empty-nested.rb — pins the boundary at the start, middle and end, with an empty separator (where the boundary is invisible), nil elements, deeper nesting, and both the pure and the dispatching (to_s / to_ary) paths.

Test plan

Toolchain: elan with leanprover/lean4:v4.32.2, CRuby 4.0.5, Sorbet 0.6.13405, uv.

• The reproducer and an adjacent set, through bin/ruby-lean --compare: model and CRuby agree on every case in the table above, and on 150 randomly generated nested-join programs (depth ≤ 4, mixed Integer/nil/String, separators ",", "-", "", " | ").
• difftest run --tier regressions: 224 cases — 223 agree/held, 1 gated (sorbet-hash-gate, declared open), 0 regressed, 0 disagree. The new case reports held.
• conformance tier 0 (difftest run --tier 0 + scripts/check-conformance.sh): 1287 programs ran, 1087 agree, 194 unsupported, 0 disagree, 0 weakened — holds difftest/coverage-baseline.json exactly, so no recorded number moved.
• difftest replay corpus/tier3: 70 cases, 57 agree, 13 unsupported, 0 disagree.
• make books (cd books && lake build): 1405 jobs, success — including Books.Metatheory.Framing.RootFramePrimitives, which is where joinImpl_frame lives.
• make metatheory: OK — theorems rest on propext, Classical.choice, Quot.sound only; the booted heap satisfies the proofs' assumptions.
• make soundness: SOUNDNESS CHECK PASSED.
• make comparator: accepted — statements match Challenge.lean, axioms are Lean's three, the kernel replays the closure.
• make-equivalent gen-check: PreludeJson, CRubyNames, Unicode, Prelude all fresh; books/scripts/generate_audited_checker.py --check clean.
• make difftest-test: 189 passed with DIFFTEST_NO_SKIPS=1; coverage holds its baseline (72.77 % line / 68.18 % branch).
• make book-checks: FastPower 72/72 inputs agree; LoopSum agrees. feature-loading: agrees. ci-sync: CI runs every make check target. check-not-weakened --base origin/main: CHECKS NOT WEAKENED.
• Not run locally: make lint (no file it checks changed — .rubocop.yml excludes ruby-lean/prelude/** and difftest/corpus/**, and no Python, shell or workflow file is touched) and make docs (no documentation changed).

Adjacent gap, not touched here

[1, 2].join(nil) gates (unsupported: join) where CRuby answers "12" — the builtin's separator conversion refuses a nil argument before the prelude twin sees it. Pre-existing, orthogonal to the boundary rule, and left alone to keep this change scoped.