[unpaidmoon]

Change and mathematical scope

Scoped exchange obstruction. No new κ, and the selected frontier is unchanged.

In the unchanged unsigned dirty connector, let a floor word on six sources in characteristic 7 call each source seven times. Suppose exactly one index s in 4..22 fails to make q_s + q_{45-s} a weight-3 mask. Adding the early pair (0, 3) and any one pair off s + t = 45 still leaves at least one of the C(6, 3) = 20 weight-3 masks unrealized. The cover has size at most 19. The word

023514103524310254054123145203452034213150

attains 19: its diagonal image has 18 masks, (0, 3) supplies (0, 2, 3), no off-diagonal pair is weight 3, and (1, 3, 5) is missing.

The only index that can be the single failure is the centre s = 22. Every weight-3 centre freezes a coordinate at 14, a step inside {0, 1, 7, 8, 14} cannot move 14, and two steps from a 14-free sum-45 vector stay inside {5, ..., 10}. A prefix shorter than 7 cannot meet a 14. Thus s = 4..21 stay free of 14, and the free-type chain is an exact layered graph, stays included.

Of the 108 off-diagonal slots, 82 are killed by those coordinate bounds. The 25 slots with both indices in 4..21 realize a weight-3 sum only at (12, 12) (20 times, and the mask is already the diagonal mask), (11, 13) (180), (10, 14) (180) and (9, 15) (20). The last three have equal endpoint masks, so the diagonal image has size at most 17. The remaining slot (33, 33) repeats a mask on s = 4..12 (at most 8 distinct masks there), so that image also has size at most 17. One new mask plus (0, 3) is therefore at most 17 + 1 + 1 = 19. A mask already on the diagonal adds nothing, and 18 + 1 = 19.

This does not decide whether a six-source depth-two block exists at c = 7. A word whose diagonal image has size 18 has no off-diagonal weight-3 mask outside that image. A word that does realize a new off-diagonal mask has image size at most 17, so two such masks could still have room to reach 20. Masks of every weight other than 3, and two or more failed diagonal indices, stay open. No supplier, consumer, or selected conditional κ changes. The selected record remains 781451/250000000 from PR #6030.

Task and overlap

Base commit 7c49fe32c55de02c2c873655c804b16e4c3fef0a (upstream main at submission; re-fetched, unchanged). This fork's main is older, so the PR base is the pin branch cursor/upstream-7c49fe32-pin-bae7 at that same commit. The diff is only research/six-source-c7-one-index-exchange/.

Task card connector-alphabet-change, priority revision 8. Scope status: changed. The card asks for one new connector operation. This package keeps the alphabet fixed and answers the released one-index exchange: Nick Petalas's handoff in discussion comment 19384981, left open as question 1 of the equality-case note. A new operation is not the missing step.

Overlap checked 2026-11-10 against open upstream PRs through #6949 and open fork PRs through #177. The nearest result is upstream #6941 / fork #156, which proves the diagonal equality case empty and explicitly leaves this replacement open. This package starts there: it rechecks the centre count and does not repeat the induction down to q_4. Merged #6141 excluded c = 5 and c = 6 by local SAT and left c = 7 open. Open #6216 certifies only the c = 5 exclusion. Fork #160 and #161 are the separate c = 5 / c = 6 human-proof remainder and are not used here. zxv's #6057 and JosieElliston's #6061 supply the c ≥ 8 words. No open PR settles the one-index replacement.

Validation

Python 3.12, standard library only, from the repository root:

python3.12 -I -W error -B research/six-source-c7-one-index-exchange/verify.py
python3.12 -I -O -W error -B research/six-source-c7-one-index-exchange/verify.py
python3.12 -B scripts/research_package.py --package research/six-source-c7-one-index-exchange --check-only

Both replay commands print:

PASS_SIX_SOURCE_C7_ONE_INDEX_EXCHANGE only_failure=22 centres_with_14=300/300 free_vectors=20 slots_blocked=82 graph_slots=25 block_slots=1 graph_internal=20 graph_novel=380 block33_max_distinct=8 cover_at_most=19 witness_cover=19 missing=(1,3,5) census=12/12:20,11/13:180,10/14:180,9/15:20 controls=6

The metadata check prints PASS_PACKAGE_METADATA_AND_PINS (not a mathematical acceptance check).

The six controls are the inherited centre count (300 realizations, 480 coordinates equal to 14), the move table that keeps 14 fixed, the two-step and short-prefix bounds, the absence of an in-type step at s = 21, the witness chain lying on that graph, and a rejected one-letter mutation. The slot census is exhaustive on the free-type graph. It is not a SAT certificate and not a search-failure claim. No Lean, Docker, or unrestricted word search was run.

Credit

The depth-two interface and the weight identity are Nick Petalas's (PR #4231, PR #4248, PR #6107), with the Ross Richardson PR #934 / PR #943 lineage. JosieElliston's PR #6141 leaves c = 7 open. The empty equality case is upstream PR #6941 / fork PR #156. Its centre fact is rechecked here.

Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

Open next questions

1. Can two off-diagonal weight-3 pairs finish the count when the diagonal image has size at most 17? One new pair plus (0, 3) stops at 19, while two new pairs have room to reach 20. On an image of size 18 there is nothing for them to add. First step: keep the centre as the only failed index and ask whether the (9, 15) complement and one other new pair, from (10, 14), (11, 13), or (33, 33), can be new at the same time and disjoint from (0, 3). Blocked because those pairs constrain the same suffix, and this package does not enumerate their joint realizations.
2. Which non-weight-3 masks does the witness above miss? A depth-two block needs every nonzero mask, so a completed weight-3 count would still not be a block. First step: evaluate q_s + q_t on this one word for weights other than 3 and list the missing masks. Blocked because the state graph here tracks only weight-3 diagonal sums. The c = 5 / c = 6 human-proof question is a different remainder and is not taken here.

Workflow feedback (optional)

The free-type graph has to include stays. A first enumeration that omitted them reported no joint hits and would have been a false emptiness. Linking this once to the feedback discussion is enough: #1200