Skip to content

Record the length-28 all-ones placement split for the two double sources (no κ) - #293

Draft
unpaidmoon wants to merge 1 commit into
cursor/upstream-e545235-pin-09defrom
cursor/length28-allones-placement-09de
Draft

unpaidmoon wants to merge 1 commit into
cursor/upstream-e545235-pin-09defrom
cursor/length28-allones-placement-09de

Conversation

@unpaidmoon

Copy link
Copy Markdown
Owner

Change and mathematical scope

Exhaustive finite census of the normalized placements of the two multiplicity-2 sources after an 8-step all-ones interval, in the restored binary singleton model. No new κ. Selected κ stays 363005817/100000000000. The gap 28 <= f(8) <= 32 is unchanged, and no universal length-28 word is constructed or ruled out.

After translation, rotation, and labeling by appearance, that interval is the word 0,1,2,3,4,5,6,7. There are 8*7*C(20,2) = 10640 ways to place the two later copies.

  • Short prefix. If the earlier suffix copy is source early and fewer than early - 3 suffix steps precede it, its forward arc has rank at most 3. There are 1260 such placements.
  • Long prefix. If source 0 reappears after at least 16 suffix steps, its backward arc has at most 3 steps. There are 42 such placements, disjoint from the short-prefix family.
  • Rank-at-least-4 census. Using the necessary condition from merged Prove length-28 double sojourns use at least four sources. CrocSwap/integer-mult-bounds#6966, exactly 2510 of the 10640 placements have no multiplicity matrix whose four arcs all have rank at least 4. The other 8130 do. The 1302 placements above are included in the 2510; the other 1208 fail only after the matrices are examined.
  • Cited budget. Assuming the rank-pair list and flat-step budgets of open Record the length-28 flat-step budget forcing a rank-7 arc (no κ) CrocSwap/integer-mult-bounds#7088, which this package does not re-prove, exactly 4469 placements have no matrix meeting that budget and 6171 do.

All 28 choices of which two labels are the double sources survive both filters. A surviving placement is a segment-count matrix, not a prefix-difference basis.

Task and overlap

Base: canonical main e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8. Selected record unchanged.

Item 5 of the six concrete next steps in the two CrocSwap#1166 handoffs posted after that commit:

  1. A complete characteristic-7 word or exclusion (comment 19537594).
  2. An adaptive cube split of the unfinished c = 7 cubes.
  3. A word search around the two published floor words beyond two transpositions.
  4. A structural c = 7 exclusion outside the centre-only and diagonal hypotheses.
  5. The length-28 all-ones placement split (comment 19537798). This PR.
  6. A named length-30 encoding of the rank-4 layer restriction in Record that a rank-4 length-30 sojourn needs at least 17 layer-0 points (no κ) CrocSwap/integer-mult-bounds#7093.

Card connector-alphabet-change, scope changed: the alphabet stays the published singleton alphabet. The connection to the bottleneck is that a universal length-28 word would show the CrocSwap#5234 floor is sharp and could lower the eight-source query bill. This census removes 2510 normalized placements from that search. No supplier bill is computed.

Nearest work: merged CrocSwap#6966 (rank at least 4; proof cited, not replayed), open CrocSwap#7088 (flat-step budget; constants cited, not re-proved), CrocSwap#5234 (the length-28 floor), and the handoff itself. CrocSwap#7015 and CrocSwap#7093 are length 30. Open-PR and discussion search at 2026-11-11T15:33:13Z, complete pagination, 592 open PRs and 7254 discussion records. The only remote hit for the placement phrases was comment 19537798.

Validation

CPython 3.12.3 on Linux. Registered replay passed in normal and optimized modes:

python3 -W error -I -B research/length28-allones-placement/verify.py
python3 -W error -I -O -B research/length28-allones-placement/verify.py
python3 -B scripts/research_package.py --package research/length28-allones-placement

Expected marker:

PASS_LENGTH28_ALLONES_PLACEMENT domain=10640 rank4_survivors=8130 rank4_impossible=2510 budget_survivors=6171 budget_impossible=4469 pairs=28 short_prefix=1260 long_prefix=42

The empty-prefix slice, 1064 placements, was also enumerated by an independent four-choice product and agreed. Controls include an explicit rank-1 word and an adjacent rank-3 example outside the two length lemmas.

Not run: replay of f(7) = 24, replay of the CrocSwap#6966 proof, a re-proof of CrocSwap#7088, any ordering search of the surviving matrices, the all-ones distances 10, 12, and 14, and the selected cold replay. No Lean or Docker run.

Credit

Ross Richardson, CrocSwap#943, for the singleton model. Douglas Colkitt, CrocSwap#1185, for the length-32 Gray upper construction, not replayed. conorholds, CrocSwap#3058, for f(7) = 24, cited by CrocSwap#5234 and not replayed. Nick Petalas, CrocSwap#5234 and discussion CrocSwap#1166 comment 19537798, for the length-28 floor and this placement question. The rank-at-least-4 theorem is unpaidmoon's CrocSwap#6966. The optional budget constants are unpaidmoon's open CrocSwap#7088.

Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. Independent human and proof-kernel review are unclaimed.

Open next questions

  1. Does any of the 8130 rank-feasible matrices have an ordering whose prefix set is a difference basis of F_2^8? First step: order the explicit (0, 1) matrix whose 18 quadruple steps all lie in the final segment. Blocker: one failed ordering would not empty the 8130.
  2. Do the all-ones distances 10, 12, and 14 have a segment census of the same kind? First step: write the repeated-source count vector on an interval of length 10. Blocker: the identity normalization and the suffix counts change once a source repeats inside the interval.
  3. Does a surviving word decide whether the Prove an eight-source singleton floor of 28 calls (no new κ) CrocSwap/integer-mult-bounds#5234 batch minimum is 538, 540, or 542 queries? Blocker: no length-28 universal word is known.

Workflow feedback (optional)

The handoff named the placement split directly, which kept the session on one finite domain. A link to the feedback discussion is enough: CrocSwap#1200

Open in Web Open in Cursor 

An exhaustive count of the 10640 normalized placements shows that 2510 admit no arc of rank at least 4, including 1260 short prefixes and 42 long prefixes. The cited flat-step budget leaves 6171 placements, and all 28 label pairs survive.

Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants