diff --git a/research/length28-adjacent-pair-degree-obstruction/PROOF.md b/research/length28-adjacent-pair-degree-obstruction/PROOF.md new file mode 100644 index 0000000000..c97511df6d --- /dev/null +++ b/research/length28-adjacent-pair-degree-obstruction/PROOF.md @@ -0,0 +1,145 @@ +# Proof: at most 23 distinct adjacent pairs + +## Setting + +A word is a cyclic sequence `w_0, ..., w_{L-1}` over the letter set +`[8] = {0,...,7}`. A *closed* word has the property that each letter count is +even, which is the standing hypothesis of the singleton connector model: the +prefix walk returns to the origin exactly when every coordinate is used an even +number of times. + +For a slot `t` (indices mod `L`) the *adjacent pair* is the unordered pair +`{w_t, w_{t+1}}`. A pair `{i,i}` is a *loop*. `mult(i,j)` is the number of +slots with pair `{i,j}`; `m_i` is the number of occurrences of letter `i`; and +`G` is the simple graph on `[8]` with `{i,j}` an edge exactly when +`mult(i,j) > 0`. + +## Lemma 1 (incidence identity and degree bound) + +For every letter `i`, + +```text +2 m_i = sum_{j != i} mult(i,j) + 2 * loops_i, +``` + +and therefore + +```text +deg_G(i) <= sum_{j != i} mult(i,j) <= 2 m_i. +``` + +Also `deg_G(i) <= 7`. + +**Proof.** Each occurrence of `i` at position `t` lies in exactly two slots: the +slot ending at `t` and the slot starting at `t`. Both contain `i`. Summing over +occurrences counts every non-loop slot containing `i` once and every loop at `i` +twice. This gives the identity. The number of distinct partners is at most the +number of non-loop incidences, which is at most `2 m_i`. The last inequality is +`|V(G)| = 8`. QED + +## Lemma 2 (Euler correspondence) + +The multiset of adjacent pairs of a closed word is exactly the edge multiset of +a connected Eulerian multigraph on the letters, with degree `2 m_i` at letter +`i`. Conversely, every connected multigraph with even degrees `2 m_i` has an +Euler circuit, and reading its vertices produces a closed word with those +multiplicities and that adjacent-pair multiset. + +**Proof.** The closed word is a closed walk in the letter multigraph; every edge +is one slot. Conversely an Euler circuit traverses each edge once, and the +degree of a vertex in an Eulerian circuit equals its degree in the multigraph. +QED + +## Theorem + +Let `w` be a closed word of length 28 over `[8]` with multiplicities +`(4,4,4,4,4,4,2,2)`. Then `D(w)`, the number of distinct unordered adjacent +pairs, satisfies `D(w) <= 23`. The bound is attained. + +**Proof.** Let `L` be the set of the two letters with `m_i = 2`. Its complement +in `[8]` is the six letters with `m_i = 4`. + +For `i` in `L`, Lemma 1 gives `deg_G(i) <= 2 m_i = 4`. Since `K_8` has degree 7, +letter `i` is missing at least `7 - 4 = 3` edges to other letters. + +Let `M_i` be the set of edges of `K_8` at `i` that are absent from `G`. Then +`|M_i| >= 3`. The two light letters `a, b` are distinct. If an edge belongs to +`M_a` and to `M_b`, then it is incident with both `a` and `b`, hence it is the +single edge `{a,b}`. Therefore + +```text +|M_a union M_b| >= |M_a| + |M_b| - 1 >= 3 + 3 - 1 = 5. +``` + +Each missing edge is one of the 28 edges of `K_8`, so at least 5 edges are +missing and + +```text +D(w) = |E(G)| <= 28 - 5 = 23. +``` + +QED + +## Sharpness + +Take letters `0,...,5` heavy and `6,7` light. Delete the five edges +`{6,7}, {0,6}, {1,6}, {2,7}, {3,7}` from `K_8`. The remaining graph has 23 +edges and degrees + +```text +deg(0)=deg(1)=deg(2)=deg(3)=6, deg(4)=deg(5)=7, deg(6)=deg(7)=4. +``` + +Add the extra copies `{0,1}` twice, `{2,3}` twice and `{4,5}` once. The +resulting loop-free connected multigraph has 28 edges and degrees + +```text +(8,8,8,8,8,8,4,4). +``` + +Every degree is even, so Lemma 2 gives an Euler circuit, hence a closed word +with counts `(4,4,4,4,4,4,2,2)` whose distinct adjacent pairs are exactly the +23 distinct edges. One such circuit is + +```text +0107547156453236250432413021. +``` + +The only repeated pairs are `{0,1}` and `{2,3}`, each on three slots, and +`{4,5}` on two slots; the total number of repeated slots is +`2 + 2 + 1 = 5`. So `D = 23` is attained. + +## Corollaries + +**Corollary 1 (weight-2 sums).** A two-letter arc has sum `e_i + e_j`. A loop +has sum 0. Hence at most `D(w) <= 23` of the 28 weight-2 vectors of `F_2^8` are +sums of two-letter arcs of `w`. At least five weight-2 vectors are not, and +because the weight of an arc sum is congruent to its length modulo 2, each of +those five must be a sum of an arc of even length at least 4. + +**Corollary 2 (no all-distinct word).** Suppose the 28 adjacent pairs of a +length-28 word are all distinct. Then `G = K_8` and `deg_G(i) = 7` for every +letter. Lemma 1 forces `2 m_i = 7`, which has no integer solution. So no closed +word with 28 distinct adjacent pairs exists. In particular an Euler circuit of +`K_8` cannot be a length-28 word with the required profile: in a closed trail the +number of occurrences of a letter is half its degree, so every letter would have +to occur `7/2` times. + +**Corollary 3 (repeats).** Under the theorem's hypotheses the 28 slots contain +at least five repeated pairs, that is + +```text +sum_{edges e of G} (mult(e) - 1) = 28 - D(w) >= 5. +``` + +## What is not claimed + +- 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 above has 156 distinct arc sums and is not universal. +- The degree count uses only two-letter arcs. It gives no bound on arcs of + length 3 or more. +- No selected-frontier, supplier, native, precision or kappa claim. +- A search that failed to find a universal word is not a proof of nonexistence, + and no such search is reported as evidence here. diff --git a/research/length28-adjacent-pair-degree-obstruction/README.md b/research/length28-adjacent-pair-degree-obstruction/README.md new file mode 100644 index 0000000000..b896e08593 --- /dev/null +++ b/research/length28-adjacent-pair-degree-obstruction/README.md @@ -0,0 +1,125 @@ +# At most 23 distinct adjacent pairs in a length-28 universal word + +**Scoped written proof with exhaustive finite corroboration and an explicit sharp +example. No new kappa.** Selected kappa stays `363005817/100000000000` +(0.00363005817). + +Consider 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 that +[#5234](https://github.com/CrocSwap/integer-mult-bounds/pull/5234) shows is +necessary at length 28. This package proves: + +> **Theorem.** Let `D(w)` be the number of distinct unordered pairs +> `{w_t, w_{t+1}}` 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 the sum `e_i + e_j`, so at least +5 of the 28 weight-2 basis sums cannot be produced by a two-letter arc and must +come from arcs of even length at least 4. + +The proof is a degree count on a graph attached to the word. Each occurrence of +a letter participates in exactly two adjacent pairs, so the number of distinct +partners of a letter is at most twice its multiplicity; the two letters of +multiplicity 2 have at most four partners out of seven and therefore each miss +at least three edges of `K_8`. Their missing sets can share at most the single +edge between them, so at least five edges are missing and at most +`28 - 5 = 23` distinct pairs remain. Sharpness is an explicit loop-free +multigraph with degree sequence `(8,8,8,8,8,8,4,4)` on 28 edges, 23 of them +distinct, whose Euler circuit realizes the profile. + +A consequence excludes the most natural construction: a word whose 28 adjacent +pairs are all distinct would have every letter count equal to `7/2`. Thus no +Euler circuit of `K_8` (or of any simple graph with 28 distinct pairs) is a +length-28 word with the required profile, and a census that enumerates such +circuits is provably incomplete. + +## Scope + +The result is a combinatorial constraint on the input word. It does not +construct a universal length-28 word, does not prove one impossible, and does +not change `28 <= f(8) <= 32`. The question it constrains is Open next question +1 of `research/length28-sojourn-rank` (#6966), which asks whether a universal +length-28 word exists with every multiplicity-2 arc using at least four other +sources. + +Priority card `connector-alphabet-change`, priority revision 8. Scope status: +**changed**; the card asks for one new connector operation, while this package +keeps the singleton alphabet and adds a necessary condition on the word. +Base commit `e54523517d0f03e58352e647c403a5af3e525a57`. + +## Result in detail + +Write `m_i` for the number of occurrences of letter `i` and `mult(i,j)` for the +number of slots whose unordered pair is `{i,j}`. Let `G` be the simple graph on +the eight letters with `{i,j}` an edge when `mult(i,j) > 0`. + +1. **Incidence identity.** `2 m_i = sum_{j != i} mult(i,j) + 2 loops_i`. +2. **Degree bound.** `deg_G(i) <= min(2 m_i, 7)`. +3. **Complement count.** The two letters with `m_i = 2` have `deg_G <= 4`, so + each misses at least three edges of `K_8`. Two such missing sets share at + most the edge joining the two letters, so at least 5 of the 28 edges are + missing. +4. **Sharpness.** The word `0107547156453236250432413021` is closed, has counts + `(4,4,4,4,4,4,2,2)`, and has exactly 23 distinct adjacent pairs. + +The bound is tight as a statement about the profile. It is not tight for +universality: the exhibited word has only 156 distinct arc sums, so it is not +universal. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -W error -I -B research/length28-adjacent-pair-degree-obstruction/verify.py +python3 -W error -I -O -B research/length28-adjacent-pair-degree-obstruction/verify.py +python3 -B scripts/research_package.py --package research/length28-adjacent-pair-degree-obstruction +``` + +Expected marker: + +```text +PASS_LENGTH28_ADJACENCY_DEGREE words=484417 D_max=23 sharp_D=23 +``` + +The verifier exhaustively checks the lemma on 484,417 closed words over at most +five letters, checks the complement arithmetic, rebuilds the sharp multigraph +and its Euler circuit, and confirms the all-distinct arithmetic. It runs in +about 1.5 seconds. + +## Evidence status + +The written proof is the argument above. The verifier corroborates the finite +claims exactly; it is not a proof kernel. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +1. Does a universal length-28 word exist at all? The present bound leaves the + five weight-2 sums to longer arcs; a census can now restrict to words with at + most 23 distinct adjacent pairs, but no exclusion follows. +2. Can the same degree count be sharpened with length-3 or length-4 arc + constraints? The count uses only length-2 arcs, and the sharp example shows + the length-2 budget alone cannot exclude the profile. +3. Does the arc-rank constraint of `research/length28-sojourn-rank` combine with + the 23-pair bound to exclude the rank-4 arcs it leaves open? + +## Credit + +This package was produced by Nick Petalas. + +Ross Richardson, #943, for the singleton model and the prefix criterion. +conorholds, #3058, for `f(7) = 24` and the eight-source question. Nick Petalas, +#5234, for the length-28 floor and the multiplicity profile used as the premise. +unpaidmoon, #6966, for the arc-rank constraint and for posing the sharpness +question this package constrains. The degree count, the sharp multigraph and the +verifier are new work. + +## Overlap + +The search covered open and merged PR titles and bodies for `length-28`, +`4,4,4,4,4,4,2,2`, `adjacent pair`, `Euler circuit` and `difference basis`, and +the live handoff thread. No earlier package states a bound on the number of +distinct adjacent pairs. #5234 and #6966 bound arcs by rank, not by adjacency +degree; #5430 and #6497 fix one projection. No match is a novelty certificate. diff --git a/research/length28-adjacent-pair-degree-obstruction/SOURCES.json b/research/length28-adjacent-pair-degree-obstruction/SOURCES.json new file mode 100644 index 0000000000..500e29290e --- /dev/null +++ b/research/length28-adjacent-pair-degree-obstruction/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/length28-sojourn-rank/README.md", + "usage": "provenance", + "git_blob": "8f0b0873ae2049ae5e2fda178390744f1a4ea9f8", + "sha256": "2adb2b7c4b127b29b649883f89dc0deff54b46e32c3f560850cb70fc3967790b" + } + ] +} diff --git a/research/length28-adjacent-pair-degree-obstruction/TASK.json b/research/length28-adjacent-pair-degree-obstruction/TASK.json new file mode 100644 index 0000000000..14b2876f9e --- /dev/null +++ b/research/length28-adjacent-pair-degree-obstruction/TASK.json @@ -0,0 +1,98 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove that a 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, that 23 is attained, and that at least five weight-2 basis sums therefore require arcs of length at least four.", + "scope_change_reason": "The card asks for one new connector operation. This package keeps the singleton alphabet and adds a necessary condition on the closed word that acts as the connector interface. It answers no part of the card's budget question and does not change kappa.", + "bottleneck_link": "A universal length-28 singleton word would make the #5234 floor of 28 sharp and could lower the eight-source query bill. The bound restricts any future census to words with at most 23 distinct adjacent pairs and excludes the all-distinct Euler-circuit route.", + "budget_minutes": 60, + "stop_rule": "Stop once the degree count, the complement bound, the sharp example and the exhaustive lemma check are complete. Do not search for a universal word and do not treat an unfinished search as nonexistence.", + "outcome": "completed", + "evidence": "Written degree count on the adjacent-pair graph plus an explicit loop-free Eulerian multigraph with degree sequence (8,8,8,8,8,8,4,4) and 23 distinct edges. The verifier exhaustively checks the incidence identity and degree bound on 484,417 closed words over at most five letters, the complement arithmetic, the Euler circuit and the sharp word, and the all-distinct arithmetic.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a universal length-28 word with multiplicities (4,4,4,4,4,4,2,2) exist?", + "why_it_matters": "A yes answer makes the #5234 floor of 28 sharp; a no answer raises f(8) to at least 29.", + "first_step": "Restrict a census to words with at most 23 distinct adjacent pairs and at least five repeated slots, then combine with the arc-rank rank-at-least-4 case left open by #6966.", + "blocked_by": "No structural exclusion of the remaining adjacency profiles, and no completed census." + }, + { + "question": "Can length-3 and length-4 arc constraints sharpen the 23-pair bound?", + "why_it_matters": "The present count uses only two-letter arcs, and the sharp example shows the two-letter budget alone cannot exclude the profile.", + "first_step": "Repeat the degree count on the graph whose edges are distinct length-4 arcs, with the loop and multiplicity bookkeeping of Lemma 1.", + "blocked_by": "Length-4 arcs are not determined by adjacent pairs, so the incidence identity needs a new carrier." + }, + { + "question": "Do the 23-pair bound and the #6966 arc-rank constraint jointly exclude the rank-4 arcs?", + "why_it_matters": "That is the only case #6966 leaves open in the rank-at-most-4 part of the length-28 question.", + "first_step": "Fix a multiplicity-2 source, enumerate the possible adjacent-pair graphs with at most 23 edges, and test the four-value flat-coordinate count of #6966.", + "blocked_by": "No classification of the admissible adjacent-pair graphs up to relabelling." + } + ], + "claim_type": "scoped written proof with exhaustive finite corroboration and an explicit sharp example", + "unrun_obligations": [ + "No construction or exclusion of a universal length-28 word.", + "No replay of the cited #5234 floor or the #3058 f(7)=24 theorem.", + "No selected cold replay, Lean, Docker, supplier admission or kappa change.", + "No proof-kernel or independent human review." + ], + "environment": { + "python": "3.12.3", + "platform": "macOS" + }, + "overlap": { + "open_pr_snapshot": "2026-11-11T21:35:00Z; first 100 open PR records by update time", + "discussion_snapshot": "2026-11-11T21:20:00Z; last 12 comments of discussion 1166", + "local_metadata": "base e54523517d0f03e58352e647c403a5af3e525a57", + "terms": [ + "length-28", + "4,4,4,4,4,4,2,2", + "adjacent pair", + "Euler circuit", + "difference basis" + ], + "novelty_limits": "Closed PR bodies are covered through targeted term searches, not a full closed-PR body index. No match is a novelty certificate." + } +} diff --git a/research/length28-adjacent-pair-degree-obstruction/VERIFY.json b/research/length28-adjacent-pair-degree-obstruction/VERIFY.json new file mode 100644 index 0000000000..d0d36b0b26 --- /dev/null +++ b/research/length28-adjacent-pair-degree-obstruction/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive incidence identity and degree bound on 484,417 closed words over at most five letters, the complement arithmetic, the sharp multigraph and its Euler circuit with 23 distinct pairs, and the all-distinct arithmetic." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with optimization; the assertions and the expected marker stay active." + } + ] +} diff --git a/research/length28-adjacent-pair-degree-obstruction/verify.py b/research/length28-adjacent-pair-degree-obstruction/verify.py new file mode 100644 index 0000000000..60ea1d5bc2 --- /dev/null +++ b/research/length28-adjacent-pair-degree-obstruction/verify.py @@ -0,0 +1,182 @@ +"""Exact checks for the length-28 adjacent-pair degree obstruction. + +Checks, all exact and exhaustive where stated: + A. Lemma: for every closed word on n <= 5 letters with n <= 4 and length <= 8 + (and n = 5, length <= 8), every letter i satisfies + deg_G(i) <= min(2 m_i, n - 1), + where G is the simple graph of distinct cyclic adjacent pairs and m_i is + the letter count. Also checks the incidence identity + 2 m_i = sum_{j != i} mult(i,j) + 2 * loops_i. + B. Complement count: for n = 8 with counts (4,4,4,4,4,4,2,2), the two + letters of count 2 each miss at least 3 edges of K_8, and two missing-edge + sets can share at most the single edge joining the two light letters. + Hence at least 5 edges of K_8 are missing, i.e. D(w) <= 23. + C. Sharpness: an explicit loop-free connected multigraph on 8 letters with + degree sequence (8,8,8,8,8,8,4,4) and 28 edges, 23 of them distinct, is + constructed; Hierholzer's algorithm produces a closed word with counts + (4,4,4,4,4,4,2,2) and D(w) = 23. + D. All-distinct impossibility: if D(w) = 28 then every letter has degree 7 in + G, so 2 m_i = 7, which is not an integer. +""" + +import itertools + +N8 = 8 +L = 28 + + +def cyclic_pairs(word): + """Multiset of unordered cyclic adjacent pairs, loops included.""" + return [tuple(sorted((word[t], word[(t + 1) % len(word)]))) + for t in range(len(word))] + + +def counts(word, n): + return [word.count(i) for i in range(n)] + + +def distinct_pairs(word): + return set(cyclic_pairs(word)) + + +def check_lemma_exhaustive(n, length): + """Enumerate every word of the given length over n letters.""" + bad = 0 + checked = 0 + for word in itertools.product(range(n), repeat=length): + m = counts(word, n) + pairs = cyclic_pairs(word) + mult = {} + loops = [0] * n + for a, b in pairs: + if a == b: + loops[a] += 1 + else: + mult[(a, b)] = mult.get((a, b), 0) + 1 + for i in range(n): + inc = sum(c for (a, b), c in mult.items() if a == i or b == i) + inc += 2 * loops[i] + if inc != 2 * m[i]: + bad += 1 + raise AssertionError(("incidence identity", word, i, inc, m[i])) + deg = len({b for (a, b) in mult if a == i or b == i}) + if deg > min(2 * m[i], n - 1): + bad += 1 + raise AssertionError(("degree bound", word, i, deg, m[i])) + checked += 1 + return checked, bad + + +def build_sharp_multigraph(): + """Return the edge multiset of the sharp example. + + Letters 0..5 are heavy (degree 8), letters 6,7 are light (degree 4). + Missing from K_8: 67, 60, 61, 72, 73 (five edges). + Extra copies added to reach degree 8 at 0..3 and 7 at 4,5: + {0,1} twice, {2,3} twice, {4,5} once. + """ + missing = {(6, 7), (0, 6), (1, 6), (2, 7), (3, 7)} + edges = [] + for i in range(N8): + for j in range(i + 1, N8): + if (i, j) not in missing and (j, i) not in missing: + edges.append((i, j)) + edges += [(0, 1), (0, 1), (2, 3), (2, 3), (4, 5)] + return edges + + +def hierholzer(edges, n): + adj = {i: [] for i in range(n)} + for idx, (a, b) in enumerate(edges): + adj[a].append((b, idx)) + adj[b].append((a, idx)) + used = [False] * len(edges) + stack = [0] + circuit = [] + while stack: + v = stack[-1] + advanced = False + while adj[v]: + u, idx = adj[v].pop() + if used[idx]: + continue + used[idx] = True + stack.append(u) + advanced = True + break + if not advanced: + circuit.append(stack.pop()) + circuit.reverse() + # circuit is a vertex sequence v_0 .. v_28 with v_28 = v_0; the word is the + # list of first 28 vertices. + return circuit[:-1] + + +def main(): + # A. exhaustive lemma checks + total = 0 + for n, length in [(2, 2), (2, 4), (2, 6), (2, 8), + (3, 3), (3, 6), (3, 9), + (4, 4), (4, 6), (4, 8), + (5, 5), (5, 8)]: + checked, bad = check_lemma_exhaustive(n, length) + total += checked + print(f"lemma n={n} L={length} words={checked} violations={bad}") + print(f"LEMMA_EXHAUSTIVE words={total} violations=0") + + # B. the complement count + light = [4, 4] # 2 m_i for the two light letters + missing_per_light = [7 - 4, 7 - 4] # at most 4 distinct partners of 7 + assert all(x >= 3 for x in missing_per_light) + missing_total = sum(missing_per_light) - 1 # shared edge only 6-7 + assert missing_total == 5 + bound = 28 - missing_total + assert bound == 23 + print(f"COMPLEMENT light_missing={missing_per_light} " + f"shared_at_most=1 missing_total={missing_total} D_max={bound}") + + # C. sharpness + edges = build_sharp_multigraph() + assert len(edges) == 28, len(edges) + distinct = set(edges) + assert len(distinct) == 23, len(distinct) + deg = {i: 0 for i in range(N8)} + for a, b in edges: + deg[a] += 1 + deg[b] += 1 + assert deg == {0: 8, 1: 8, 2: 8, 3: 8, 4: 8, 5: 8, 6: 4, 7: 4}, deg + word = hierholzer(edges, N8) + assert len(word) == 28 + m = counts(word, N8) + assert sorted(m) == [2, 2, 4, 4, 4, 4, 4, 4], m + assert len(distinct_pairs(word)) == 23, len(distinct_pairs(word)) + assert sum(1 for a, b in cyclic_pairs(word) if a == b) == 0 + mult = {} + for a, b in cyclic_pairs(word): + mult[(a, b)] = mult.get((a, b), 0) + 1 + repeated = {k: v for k, v in mult.items() if v > 1} + assert repeated == {(0, 1): 3, (2, 3): 3, (4, 5): 2}, repeated + q = 0 + pre = [0] + for s in word: + q ^= 1 << s + pre.append(q) + pre = pre[:-1] + arc_sums = {a ^ b for a in pre for b in pre} + assert len(arc_sums) == 156, len(arc_sums) + print("SHARP_WORD " + "".join(str(x) for x in word)) + print(f"SHARP counts={m} distinct_pairs={len(distinct_pairs(word))} " + f"repeated_slots={28 - len(distinct_pairs(word))} " + f"repeated={repeated} arc_sums={len(arc_sums)}") + + # D. all-distinct impossibility + assert 2 * 28 == 56 # total incidences + assert 56 // 8 == 7 and (2 * 4 == 8) # all-distinct forces 2m_i = 7 + print("ALL_DISTINCT forces 2*m_i=7, impossible for integer m_i") + + print("PASS_LENGTH28_ADJACENCY_DEGREE " + f"words={total} D_max={bound} sharp_D=23") + + +if __name__ == "__main__": + main()