Skip to content

Bound distinct adjacent pairs of a length-28 universal word (no kappa change) - #7321

Open
petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w4-1111f-length28-adjacency-bound
Open

petalas wants to merge 2 commits into
CrocSwap:mainfrom
petalas:research/w4-1111f-length28-adjacency-bound

Conversation

@petalas

@petalas petalas commented Nov 11, 2026 •

Copy link
Copy Markdown
Contributor

Result and claim type

Scoped written proof with exhaustive finite corroboration and an explicit sharp example. No new κ. Selected κ stays 363005817/100000000000.

For a closed cyclic word of length 28 over the eight coordinate directions of F_2^8 with letter multiplicities (4,4,4,4,4,4,2,2) — the profile #5234 shows is necessary at length 28 — let D(w) be the number of distinct unordered pairs of cyclically consecutive letters. Then

D(w) <= 23, and 23 is attained.

Equivalently, at least 5 of the 28 adjacent-pair slots repeat an earlier unordered pair. A two-letter arc contributes e_i + e_j, so at least 5 of the 28 weight-2 basis sums cannot come from two-letter arcs and must come from arcs of even length at least 4.

The proof is a degree count. Each occurrence of a letter lies in exactly two adjacent pairs, so its number of distinct partners is at most twice its multiplicity. The two letters of multiplicity 2 have at most four partners out of seven, so each misses at least three edges of K_8; their missing sets share at most the single edge between them, leaving at most 28 - 5 = 23 distinct pairs. Sharpness is an explicit loop-free connected multigraph with degree sequence (8,8,8,8,8,8,4,4), 28 edges and 23 distinct edges; its Euler circuit is the word 0107547156453236250432413021.

A corollary excludes the most natural construction: all 28 adjacent pairs distinct would force every letter count to be 7/2, so no such word exists and no census of simple-graph Euler circuits is complete.

Evidence and reproduction

From the repository root:

~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/length28-adjacent-pair-degree-obstruction/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/length28-adjacent-pair-degree-obstruction/verify.py
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/length28-adjacent-pair-degree-obstruction
~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/length28-adjacent-pair-degree-obstruction --check-source-history

Expected marker: PASS_LENGTH28_ADJACENCY_DEGREE words=484417 D_max=23 sharp_D=23. The verifier runs in about 1.5 seconds under CPython 3.12.3 on macOS.

It checks exactly:

  • the incidence identity 2 m_i = sum_{j != i} mult(i,j) + 2 loops_i and the bound deg_G(i) <= min(2 m_i, n-1) on all 484,417 words over at most five letters with the lengths listed in the script (exhaustive, including loops);
  • the complement arithmetic 3 + 3 - 1 = 5 and 28 - 5 = 23;
  • the sharp multigraph, its degree sequence, its Euler circuit, the resulting letter counts (4,4,4,4,4,4,2,2), the 23 distinct pairs, the three repeated pairs and the 5 repeated slots, and that the sharp word has only 156 distinct arc sums;
  • the all-distinct contradiction 2 m_i = 7.

check_research_commit.py --check-source-history passed locally at commit e53e88a44b4543768e498c81964f8d96cfeb4a2e (source history e54523517d0f03e58352e647c403a5af3e525a57).

Limitations and unrun obligations

  • No universal length-28 word is constructed or excluded. 28 <= f(8) <= 32 is unchanged.
  • The bound 23 is sharp for the multiplicity profile, not for universality; the sharp word has 156 arc sums.
  • The count uses only two-letter arcs and gives no bound on longer arcs.
  • No replay of the cited Prove an eight-source singleton floor of 28 calls (no new κ) #5234 floor or Research: exact seven-source singleton minimum f(7) = 24 #3058 f(7) = 24.
  • No selected cold replay, Lean, Docker, supplier admission or κ change.
  • The verifier is not a proof kernel. Independent human and formal proof-kernel review are unclaimed.
  • A search I ran for a universal length-28 word did not find one; a failed search is not a proof of nonexistence and is not used as evidence here.

Open next questions

  1. Does a universal length-28 word with multiplicities (4,4,4,4,4,4,2,2) exist? A census can now restrict to words with at most 23 distinct adjacent pairs and at least five repeated slots.
  2. Can the same degree count be repeated on length-4 arcs to sharpen the bound? Length-4 arcs are not determined by adjacent pairs, so the incidence identity needs a new carrier.
  3. Do the 23-pair bound and the Prove length-28 double sojourns use at least four sources. #6966 arc-rank constraint jointly exclude the rank-4 arcs that Prove length-28 double sojourns use at least four sources. #6966 leaves open?

Related open work

CI notes

CI did not certify this package. At head e53e88a44b4543768e498c81964f8d96cfeb4a2e, run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/43105694304 (job 130808332826) failed the plan job in its Onboarding helper tests step: 760 tests ran, one failed and 24 were skipped. The single failure is test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, an AssertionError: 'make frontier7000-verify' not found in ... on docs/ci-verification.md. The replay job was skipped because plan failed.

The failure is repository-level and unrelated to this package. On base e54523517d0f03e58352e647c403a5af3e525a57, certificates/selected-result.json names make frontier7000-verify while docs/ci-verification.md still describes #6030 and contains zero occurrences of the required command, so the test fails on main's own files. The identical single test and assertion appear in runs 42905094314, 43030419612, 43105433200 and 43105506939 (other contributors' and this account's PRs).

Local evidence at this head: both VERIFY.json commands pass with PASS_LENGTH28_ADJACENCY_DEGREE words=484417 D_max=23 sharp_D=23, scripts/research_package.py --package research/length28-adjacent-pair-degree-obstruction passes, and scripts/check_research_commit.py --package research/length28-adjacent-pair-degree-obstruction --check-source-history passes with source history e54523517d0f03e58352e647c403a5af3e525a57.

Every closed length-28 word over eight letters with multiplicities
(4,4,4,4,4,4,2,2) has at most 23 distinct unordered adjacent pairs. The bound
is attained by an explicit Eulerian multigraph. Consequently at least five
weight-2 basis sums need arcs of length at least four, and no word has 28
distinct adjacent pairs.
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.

1 participant