Repository navigation
Prove length-28 double sojourns use at least four sources. - #6966
Merged
Mister-Meeseeks merged 1 commit intoNov 10, 2026
Merged
Mister-Meeseeks merged 1 commit into
Mister-Meeseeks merged 1 commit into
Conversation
A universal closed word with multiplicities (4,4,4,4,4,4,2,2) cannot put three or fewer other sources on a multiplicity-2 arc. The remaining rank-at-least-4 case, and whether f(8) equals 28, stay open. No kappa change. Co-authored-by: unpaidmoon <unpaidmoon@users.noreply.github.com>
This was referenced Nov 10, 2026
Record the length-28 flat-step budget forcing a rank-7 arc (no κ)
unpaidmoon/integer-mult-bounds#210
Draft
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Change and mathematical scope
Scoped written proof with finite corroboration. No new κ and no selected-frontier change. Selected κ stays
781451/250000000.In the restored binary singleton model,
28 <= f(8) <= 32is unchanged. For a closed length-28 word with multiplicities(4,4,4,4,4,4,2,2), if the prefix set satisfiesP+P = F_2^8, then each of the four arcs determined by the two multiplicity-2 sources uses at least four other sources.Rank at most 2 is a product bound: the arc image has size at most 4, so the cross sum has size at most 96. Rank 3 splits on the other double source. Three quadruple sources leave only 14 outside steps, which visit at most 15 of the 16 quotient cosets. The other double plus two quadruples leaves at most three flat steps on the complement, hence at most four flat coordinates, and a 4-point set in
F_2^3has at most 7 pairwise sums. This does not construct a universal word and does not prove that none exists. Arcs of rank at least 4 remain open. A failed search is not a nonexistence proof.Task and overlap
Base commit:
7c49fe32c55de02c2c873655c804b16e4c3fef0a.Session r125. The question is discussion #1166 comment 19377982 as left open by the length-30 handoff, and open question 2 of the length-30 finding: whether a universal length-28 word with these multiplicities exists. This package proves a necessary arc constraint. It does not take the locked length-30 existence question.
Card
connector-alphabet-change, priority revision 8. Scope status: changed. The card asks for one new connector operation. This package keeps the published singleton alphabet. The length-28 arc constraint is the added statement.Nearest work:
f(7)=24, cited and not replayed.research/eight-source-singleton-floorproves28 <= f(8) <= 32and the multiplicity shape, and asks whether a 28-step word exists. This package starts from that question and does not revisit the 538-query batch bound.(4,4,4,4,4,2,2,12).Overlap search at 2026-11-10T02:22:37Z: 895 open PR records and 6934 discussion records, complete pagination; local head inventory at
7c49fe32was complete (8919 note records). Terms:4,4,4,4,4,4,2,2,length-28,sojourn rank. Closed PR bodies are covered through local notes and the predecessors named above, not a full closed-PR index. No match is a novelty certificate.Validation
CPython 3.12.3, standard library, from the repository root:
Observed:
PASS_LENGTH28_SOJOURN_RANK subsets=162 paths=320 worst_missed=7 gray=256PASS_REGISTERED_RESEARCH_PACKAGE research/length28-sojourn-rank outcome=completedPASS_RESEARCH_COMMIT_BYTESat8f66b0f936d93a3c2fad756b488d4a1100582c1d, source pin7c49fe32c55de02c2c873655c804b16e4c3fef0aPASS_RESEARCH_BASELINE_BINDINGS_ONLY(bindings only, not a scientific replay)The subset census is all 162 nonempty subsets of
F_2^3of size at most 4. The path census is all 320 walks of length at most 3 on three flat bits, from every start. The five-point set{0,1,2,3,4}coversF_2^3, so the four-value bound is specific. A relabelled Gray step and a deleted Gray step are rejected.f(7)=24was not replayed. No search of the remaining rank-at-least-4 words, no Lean, no Docker, and nofrontier6030-verify.Credit
Ross Richardson, #943, for the singleton model and prefix criterion. Douglas Colkitt, #1185, for the length-32 Gray construction. conorholds, #3058, for
f(7)=24and the eight-source question. Nick Petalas, #5234 and discussion comment 19377982, for the deletion floor, the multiplicity shape, and the open sharpness question. Nicholas Stone, #5430, for the fixed-projection obstruction that this split does not reuse. #6943 for the length-30 sojourn obstructions on a different length.Prepared by unpaidmoon with substantial Cursor Grok assistance. New work is Apache-2.0. Independent human and proof-kernel review are unclaimed.
Open next questions
{0,1,2,3,4}shows five coordinates can coverF_2^3.Workflow feedback
The coordinate split separates a short counting obstruction from the remaining rank-at-least-4 search. No further session report.