[VictorLiwentao]

Change and mathematical scope

Answers open question 2 of #3696 under the #2977/#3004 checker/exporter cascade. That PR showed dest-free gates always make Sym and Exp agree, named dest-in witnesses that diverge, and four B[0] bad operands rejects. OQ2 asked whether those four rejects are exhaustive for dest-in-sources divergence on the pinned word.

They are not. On the pinned tuned word, at B[0] destination d=111 over n=661 registers, Sym≠Exp for exactly 661 source lists of length at most 2 — namely all [a,d]. Only self_even and dest_with_src among the four named rejects lie in that set; dup_src and self_once agree.

This package also proves a dest-in closed form: Sym and Exp agree iff either d ∉ srcs, or else count(d) is odd and every non-d value has even multiplicity in the strict prefix before the last d. Dest-free agreement is used inside that form and is not republished as the claim. Every length-≤2 divergence fails operand distinctness and is rejected by the checker.

No new kappa. Selected κ stays 0.001672660197076918. No production/schema adoption.

Task and overlap

• Package: research/selected-word-reject-exhaustion/
• Tip: 8db402376a5604dcccd9a4db9072313253595f2d
• Base: 20ecf2891d80b5acf18d980b2164fb44ea7faa90
• Scope: changed — answer Research: gate-operand export parity — dest-free always agrees; dest-in can diverge (answers #3004 OQ2; no new kappa) #3696 OQ2 with closed form + exact length-≤2 census

Closest prior: open #3696. Soft overlap is a semantic successor (token ≈0.10 / line ≈0.33), not a ~0.9 dest-free retarget and not the deferred dest-absent corollary. Cascade priors #2977/#3004 leave alone.

Validation

python3.12 -I -B research/selected-word-reject-exhaustion/verify.py
python3.12 -I -O -Werror -B research/selected-word-reject-exhaustion/verify.py
python3.12 -I -B research/selected-word-reject-exhaustion/independent.py
python3.12 -I -B research/selected-word-reject-exhaustion/test_package.py
python3.12 -B scripts/research_package.py --package research/selected-word-reject-exhaustion

Expected:

PASS_SELECTED_WORD_REJECT_EXHAUSTION len2_divergences=661 named_diverge=2 four_exhaustive=false no_new_kappa
PASS_SELECTED_WORD_REJECT_INDEPENDENT len2_divergences=661 named_diverge=2 four_exhaustive=false
PASS_SELECTED_WORD_REJECT_PACKAGE_TESTS
PASS_REGISTERED_RESEARCH_PACKAGE research/selected-word-reject-exhaustion outcome=completed

Default verify is read-only. Admission uses need() and still fires under -O.

Credit

Credit #3696 for the dest-free lemma, named rejects, and OQ2; Nick Petalas / #2977 and Kumagi / #3004 for the cascade; Dylan Crow exporter; eumemic symbolic checker; tuned PR589 word. Prepared by Wentao Li (VictorLiwentao, @Is__Victor) with substantial AI assistance, under Apache-2.0.

Open next questions

1. Exact length-≤3 divergence count at the same destination?
2. Should schema docs separate divergence classes from distinctness rejects?