diff --git a/research/six-source-c7-two-pair-count/README.md b/research/six-source-c7-two-pair-count/README.md new file mode 100644 index 0000000000..b5b1dd018b --- /dev/null +++ b/research/six-source-c7-two-pair-count/README.md @@ -0,0 +1,199 @@ +# Two off-diagonal pairs do not finish the six-source c=7 weight-3 count + +**Scoped exchange obstruction. No new κ.** In the unchanged unsigned dirty +connector, keep the centre as the only failed diagonal index. Then the pair +`(9, 15)` and one other pair from `(10, 14)`, `(11, 13)`, and `(33, 33)` +cannot finish the `C(6, 3) = 20` weight-3 masks. Every such chain has +weight-3 cover at most 7. The value 7 is attained, but only when `(9, 15)` +is the single new mask. Two or three of the masks can be new at the same +time, and different from the mask of `(0, 3)`; the cover is then at most 6. + +This does not decide whether a six-source depth-two block exists at `c = 7`. +Masks of every weight other than 3, and chains with two or more failed +diagonal indices, stay open. The selected conditional κ remains +`781451/250000000`. + +## Hypothesis, inherited + +A floor word has length 42 and calls each of six sources seven times. `q_t` +counts the first `t` letters. A pair realizes a weight-3 mask when every +coordinate of `q_s + q_t` lies in `{0, 1, 7, 8, 14}` and exactly three lie +in `{1, 8}`. The coordinate sum is then `s + t = 3 + 7λ`. + +The one-index exchange, open upstream PR #7016, proves that if exactly one +index in `4..22` fails, that index is the centre `s = 22`, and that one +off-diagonal pair still leaves the cover at most 19. This package does not +repeat that argument. It takes the resulting free-type chains as the +hypothesis: `S(s) = q_s + q_{45-s}` is a permutation of `(8, 8, 8, 7, 7, 7)` +for every `s = 4..21`. The state at index `s` is the suffix usage on +`[45-s, 42)` together with the mask of `S(s)`. The prefix is usage plus one +on the mask, and the only in-type steps are a stay or a Johnson swap, as in +that exchange. The checker rebuilds the layered graph and compares two +writings of the step. It has the same layer sizes, ending at one saturated +state per mask. + +## The only `(9, 15)` shape + +Among all free-type states at `s = 9` and `s = 15`, exactly 20 pairs have +prefixes that sum to a weight-3 vector. There is one pair for each mask +`M`. Both endpoints carry `M`, and the sum is `7` on `M` and `1` on the +complement `M^c`. Thus `(9, 15)` realizes `M^c`. The usages are `2` on `M` +and `0` off `M` at `s = 9`, and `3` on `M` and `1` off `M` at `s = 15`. +No other free-type pair sums to weight 3. The scan is exhaustive: every +centre-only chain meets the forward closure, and every sum-24 weight-3 +vector is tested against those prefixes. There are 700 such vectors and +20 hits. + +## Support collapse + +Counts are monotone, so `q_9` supported on `M` forces every earlier prefix +to be supported on `M`. A free-type mask is a 3-subset of the positive +coordinates, so `s = 4..9` all carry `M`. The checker also walks every +graph ancestor back to `s = 4` and finds the same mask. + +At `s = 15` every source in `M` already has suffix usage 3, so it cannot be +the letter added to the suffix. A swap would require that, and a stay on +`M` would too. The only remaining steps are stays on `M^c`. They preserve +the mask. Six stays saturate the usage, and `s = 16..21` all carry `M`. + +The only indices that can carry a mask other than `M` are therefore +`s = 10, 11, 12, 13, 14`. The diagonal image has size at most 6. + +The first nine letters use only `M`. If `(0, 3)` is weight 3, its three +letters are three distinct sources in `M`, so its mask is `M`, already in +the image. + +The suffix usage at `s = 12` is three steps beyond the `s = 9` usage. The +pair `(33, 33)` is weight 3 only when that usage lies in `{0, 3}` with +exactly three 3s: `q_33 = 7` minus the usage, and twice that value lies in +`{0, 1, 7, 8, 14}` only for usage 0 or 3, with the 3s as the mask. A +complement source starts at usage 0 and would need all three steps to reach +3, leaving the other coordinates at 2 or 0. That is not a legal support. +The only remaining usage is 3 on `M` and 0 off `M`, and `(33, 33)` realizes +`M`. + +The diagonal image, `(0, 3)`, and `(33, 33)` therefore contribute at most +six masks. The three pairs `(9, 15)`, `(10, 14)`, and `(11, 13)` add at +most one mask each. The cover is at most `6 + 3 = 9`, which is less than +20. + +## The walks sharpen 9 to 7 + +Each complement shape has one state at `s = 9` and one at `s = 15`. Every +in-type walk of length 6 between them was enumerated. A forward count and +a classifying recursion agree: 31,788 walks for each of the 20 masks. +On these walks the five intermediate masks and the three pair-sums were +read directly. No sum at `(10, 14)` or `(11, 13)` is weight 3 unless the +endpoints agree, and `(33, 33)` never leaves the image. + +For each mask the cover is at most 7. The 3,276 walks of cover 7 all have +image size 6 and exactly one new mask, the complement. Another 1,044 walks +per mask have two or more new masks, and 72 of those have all three of +`(9, 15)`, `(10, 14)`, and `(11, 13)` outside the image. Whenever two or +more are new, the image has shrunk enough that the cover is at most 6. +Joint newness occurs, and it does not finish the count. + +A new mask is one outside the diagonal image of `s = 4..21`. It is +disjoint from `(0, 3)` when it differs from the mask `(0, 3)` realizes. +On these chains that mask is `M` or `(0, 3)` is not weight 3, and `M` is +already in the image, so every new mask is disjoint from `(0, 3)`. The +complement is also disjoint from `M` as a 3-subset. The masks of `(10, 14)` +and `(11, 13)` need not be: on the word below they meet `M`. + +## Two words + +Both words call each source seven times. The only failed diagonal index in +`4..22` is the centre. The checker reads every pair whose index sum is +congruent to 3 modulo 7, which is every pair that can realize a weight-3 +mask, because a weight-3 vector sums to `3 + 7λ`. + +```text +012001122012345334455345554433543210221100 +``` + +The first nine letters are three copies of `(0, 1, 2)`, and positions +`9..14` are `012345`. The diagonal image is `{(0, 1, 2)}`. The pair +`(0, 3)` realizes `(0, 1, 2)`. The only other weight-3 masks are + +| pair | sum | mask | +|---|---|---| +| `(9, 15)` | `(7, 7, 7, 1, 1, 1)` | `(3, 4, 5)` | +| `(10, 14)` | `(8, 7, 7, 1, 1, 0)` | `(0, 3, 4)` | +| `(11, 13)` | `(8, 8, 7, 1, 0, 0)` | `(0, 1, 3)` | + +and `(33, 33)` repeats `(0, 1, 2)`. The cover is 4. All three new masks +differ from `(0, 3)`. A one-letter change of the first letter is rejected. + +```text +012001122301452554433345334455543210221100 +``` + +The same `(0, 3)` mask sits in a diagonal image of size 6, + +```text +(0,1,2), (1,2,3), (0,2,3), (0,1,3), (0,1,4), (0,1,5), +``` + +and `(9, 15)` supplies the seventh mask `(3, 4, 5)`. The pairs `(10, 14)` +and `(11, 13)` are not weight 3, and `(33, 33)` repeats `(0, 1, 2)`. The +cover is 7, so the census ceiling is sharp. It is still not 20. + +## What this does not say + +The bound applies only to centre-only free-type chains on which `(9, 15)` +is weight 3. A chain whose `(9, 15)` sum is not weight 3 is not classified. +Two or more failed diagonal indices are not classified. Masks of weight +other than 3 are not listed; a completed weight-3 count would still not be +a depth-two block. The slot bounds that kill the other off-diagonal sums +in PR #7016 are used only as the reason this package does not search them +again. On the two words above, the exhaustive residue scan finds no further +weight-3 mask, but that is a check of those words, not a new proof of the +82-slot obstruction. No supplier, consumer, or selected frontier changes. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/six-source-c7-two-pair-count/verify.py +python3.12 -I -O -W error -B research/six-source-c7-two-pair-count/verify.py +python3.12 -B scripts/research_package.py --package research/six-source-c7-two-pair-count --check-only +``` + +The marker is `PASS_SIX_SOURCE_C7_TWO_PAIR_COUNT endpoint_pairs=20/20 walks_per_mask=31788 image_at_most=6 structural_cover_at_most=9 census_cover_at_most=7 several_walks=1044 several_cover_at_most=6 three_new_walks=72 cover7_walks=3276 three_word_cover=4 sharp_word_cover=7 block33_outside=0 unclassified=0 controls=12`. + +The twelve controls are the agreement of the two step generators, the +terminal layer, the 20 complement pairs, the forward stays, the ancestors +back to `s = 4`, the agreement of the two walk counts, the absence of an +unclassified sum, the absence of a new `(33, 33)` mask, the cover ceilings +together with the attained cover-7 and three-new cases, the three-new word, +the sharp word, and the rejected one-letter mutation. No SAT solver, Lean, +or Docker replay is used. + +## Open next questions + +1. On a centre-only chain whose `(9, 15)` sum is not weight 3, can + `(10, 14)` and `(11, 13)` be new at the same time and push the weight-3 + cover to 20? *Why:* the collapse above uses the complement shape, so it + says nothing about a chain that misses `(9, 15)`. Separate endpoint + equalities would suggest an image of size at most 16 and a cover of at + most 19, but that counting is not proved here. *First step:* enumerate + the joint walks on which `s = 10` and `s = 14` share a mask, `s = 11` + and `s = 13` share a mask, and the states at `s = 9` and `s = 15` are + not a complement pair; record the image size and whether `(0, 3)` is + outside it. *Blocked by:* those walks are outside the 31,788 complement + windows classified here. + +## 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 diagonal +equality case is upstream PR #6941. The one-index exchange and the released +question answered here are upstream PR #7016, head +`3a89abb195ec9a63476c12042df5fbb0760e3534`; its centre reduction and its +one-pair ceiling are not repeated. zxv's PR #6057 and JosieElliston's +PR #6061 supply the `c ≥ 8` words. queelius's open PR #6216 is a `c = 5` +certificate only. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/six-source-c7-two-pair-count/SOURCES.json b/research/six-source-c7-two-pair-count/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/six-source-c7-two-pair-count/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/six-source-c7-two-pair-count/TASK.json b/research/six-source-c7-two-pair-count/TASK.json new file mode 100644 index 0000000000..70708d1f11 --- /dev/null +++ b/research/six-source-c7-two-pair-count/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "17469fff78c22941280f04d39dc5a1faee09c840", + "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": "The two-pair off-diagonal exchange for the six-source weight-3 count at characteristic 7, under the inherited centre-only free-type hypothesis. The question is whether (9, 15) and one of (10, 14), (11, 13), or (33, 33) can be new at the same time, disjoint from (0, 3), and finish the 20 weight-3 masks. This package shows joint newness occurs and that the cover is still at most 7. Unrestricted c=7 existence stays open.", + "scope_change_reason": "The catalogue card asks for one new connector operation. This package keeps the unsigned dirty connector alphabet fixed and answers open question 1 of the one-index exchange: whether two off-diagonal weight-3 pairs can finish the count when the diagonal image is small. A new operation is not the missing step.", + "bottleneck_link": "Side result on the recursive-interface schedule. It does not change a supplier, a consumer, or kappa. It bounds the two-pair replacement inside the weight-3 count at c=7 and leaves the full depth-two question open.", + "budget_minutes": 60, + "stop_rule": "Stop once every centre-only chain with a weight-3 (9, 15) sum is classified, or stop if one such chain and the named pairs cover all 20 weight-3 masks.", + "outcome": "negative-result", + "evidence": "Exhaustive free-type census: the only weight-3 (9, 15) pairs are the 20 complement shapes. The diagonal image then has size at most 6, (0, 3) and (33, 33) add nothing, and the structural cover is at most 9. The 31788 walks per mask tighten this to 7, attained by 3276 walks with only the complement new. 1044 walks have two or more new masks and cover at most 6; 72 of them have all three of (9, 15), (10, 14), and (11, 13) new. Two explicit words realize covers 4 and 7. A one-letter mutation is rejected.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: the collapse argument, the exhaustive checker, and the package text.", + "open_questions": [ + { + "question": "On a centre-only chain whose (9, 15) sum is not weight 3, can (10, 14) and (11, 13) be new at the same time and push the weight-3 cover to 20?", + "why_it_matters": "The collapse proved here uses the complement shape, so a chain that misses (9, 15) could still be the route to 20 masks. Separate endpoint equalities suggest an image of size at most 16 and a cover of at most 19, but that counting is not proved in this package.", + "first_step": "Enumerate the joint walks on which s=10 and s=14 share a mask, s=11 and s=13 share a mask, and the states at s=9 and s=15 are not a complement pair. Record the image size and whether (0, 3) lies outside it.", + "blocked_by": "Those walks are outside the 31788 complement windows classified here." + } + ] +} diff --git a/research/six-source-c7-two-pair-count/VERIFY.json b/research/six-source-c7-two-pair-count/VERIFY.json new file mode 100644 index 0000000000..77aafb1c13 --- /dev/null +++ b/research/six-source-c7-two-pair-count/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive free-type census of centre-only chains whose (9, 15) sum is weight 3: 20 complement shapes, image size at most 6, structural cover at most 9, and 31788 walks per mask with cover at most 7. Two explicit words realize covers 4 and 7. Twelve controls cover the step generators, the terminal layer, the complement pairs, the forward stays, the ancestors, the two walk counts, unclassified sums, a new (33, 33) mask, the ceilings and attained cases, both words, and a rejected one-letter mutation." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same two-pair census under optimized Python. Failures are explicit exceptions, not assertions." + } + ] +} diff --git a/research/six-source-c7-two-pair-count/verify.py b/research/six-source-c7-two-pair-count/verify.py new file mode 100644 index 0000000000..398b9675cf --- /dev/null +++ b/research/six-source-c7-two-pair-count/verify.py @@ -0,0 +1,581 @@ +#!/usr/bin/env python3 +"""Joint off-diagonal pairs for the six-source c=7 weight-3 count. + +Hypothesis, inherited from the one-index exchange and not re-proved here: +the only failed diagonal index in 4..22 is the centre, so s=4..21 are +free-type weight-3 masks. This program exhausts that finite graph. + +It does not decide unrestricted c=7 existence, and it does not inventory +masks of any weight other than 3. +""" + +import itertools + +K = 6 +SOURCES = range(K) +ALLOWED = (0, 1, 7, 8, 14) +MASK_VALUES = (1, 8) +LAYER_SIZES = ( + 120, 420, 1120, 2400, 4320, 6720, 9120, 10920, 11600, + 10920, 9120, 6720, 4320, 2400, 1120, 420, 120, 20, +) +# Image of size 1, three masks outside it, and (0, 3) equal to the image. +THREE_WORD = "012001122012345334455345554433543210221100" +# Image of size 6 plus the single complement. Ceiling 7, attained. +SHARP_WORD = "012001122301452554433345334455543210221100" +MASK_M = frozenset((0, 1, 2)) +MASK_COMPLEMENT = frozenset((3, 4, 5)) +MASK_1014 = frozenset((0, 3, 4)) +MASK_1113 = frozenset((0, 1, 3)) + + +def fail(message): + raise SystemExit("FAIL: " + message) + + +def weight3_mask(vector): + """The weight-3 support, or None when the vector is not a realization.""" + support = [] + for source, value in enumerate(vector): + if value not in ALLOWED: + return None + if value in MASK_VALUES: + support.append(source) + if len(support) != 3: + return None + return frozenset(support) + + +def middle(usage, mask): + return tuple( + 7 - 2 * usage[source] - (1 if source in mask else 0) for source in SOURCES + ) + + +def prefix_of(usage, mask): + return tuple(usage[source] + (1 if source in mask else 0) for source in SOURCES) + + +def letter_moves(usage, mask): + """In-type steps from the letter recurrence. + + A step reads a prefix letter p at position s and a suffix letter x at + position 44-s. The free-type sum stays a permutation of (8, 8, 8, 7, 7, 7) + only for a stay p=x, or for a swap that moves the 8 from x onto p. + Usage records the growing suffix and is already 3 at the terminal layer. + """ + counts = middle(usage, mask) + if min(counts) < 0: + return [] + moves = [] + for source in SOURCES: + if usage[source] >= 3 or counts[source] < 2: + continue + updated = list(usage) + updated[source] += 1 + moves.append((tuple(updated), mask)) + for removed in mask: + if usage[removed] >= 3 or counts[removed] < 1: + continue + for added in SOURCES: + if added in mask or counts[added] < 1: + continue + updated = list(usage) + updated[removed] += 1 + moved = frozenset((set(mask) - {removed}) | {added}) + moves.append((tuple(updated), moved)) + return moves + + +def johnson_moves(usage, mask): + """The same steps, written as a Johnson swap or a stay on the mask.""" + counts = middle(usage, mask) + if min(counts) < 0: + return [] + moves = [] + current = list(usage) + for removed in mask: + if usage[removed] >= 3 or counts[removed] < 1: + continue + for added in SOURCES: + if added in mask or counts[added] < 1: + continue + current[removed] += 1 + moved = frozenset((set(mask) - {removed}) | {added}) + moves.append((tuple(current), moved)) + current[removed] -= 1 + for source in SOURCES: + if usage[source] >= 3 or counts[source] < 2: + continue + current[source] += 1 + moves.append((tuple(current), mask)) + current[source] -= 1 + return moves + + +def start_states(): + """Every free-type state at s=4. The partner is one final letter.""" + found = [] + seen = set() + for last in SOURCES: + for counts in itertools.product(range(5), repeat=K): + if sum(counts) != 4: + continue + suffix = tuple(6 if source == last else 7 for source in SOURCES) + summed = tuple(counts[source] + suffix[source] for source in SOURCES) + mask = weight3_mask(summed) + if mask is None: + continue + if sorted(summed) != [7, 7, 7, 8, 8, 8]: + fail("s=4 weight-3 vector is not free type: " + str(summed)) + usage = tuple(1 if source == last else 0 for source in SOURCES) + if prefix_of(usage, mask) != counts: + fail("s=4 prefix formula missed " + str(counts)) + state = (usage, mask) + if state in seen: + fail("duplicate s=4 state " + str(state)) + seen.add(state) + found.append(state) + if len(found) != 120: + fail("expected 120 states at s=4, found %s" % len(found)) + return found + + +def build_layers(): + """Forward closure of the free-type steps from s=4 through s=21.""" + layers = [start_states()] + successors = [] + for _ in range(17): + index = {} + states = [] + edges = [] + for usage, mask in layers[-1]: + letter = letter_moves(usage, mask) + johnson = johnson_moves(usage, mask) + if set(letter) != set(johnson) or len(letter) != len(set(letter)): + fail("move generators diverged at usage %s mask %s" % (usage, mask)) + targets = [] + for new_usage, new_mask in letter: + key = (new_usage, new_mask) + if key not in index: + index[key] = len(states) + states.append(key) + targets.append(index[key]) + edges.append(targets) + layers.append(states) + successors.append(edges) + sizes = tuple(len(layer) for layer in layers) + if sizes != LAYER_SIZES: + fail("free-type layer sizes changed: " + str(sizes)) + if any(len(targets) != len(set(targets)) for edges in successors for targets in edges): + fail("a free-type state has a repeated successor") + return layers, successors + + +def check_terminal(layers): + masks = [] + for usage, mask in layers[-1]: + if usage != (3, 3, 3, 3, 3, 3): + fail("s=21 usage is not saturated: " + str(usage)) + if letter_moves(usage, mask): + fail("s=21 still has an in-type step") + masks.append(mask) + if len(masks) != 20 or len(set(masks)) != 20: + fail("s=21 is not one state per mask") + + +def complement_pairs(layers): + """Every free-type pair at s=9 and s=15 whose prefixes sum to weight 3. + + Connectivity is not required for this list. A centre-only chain meets + one of these pairs if its (9, 15) sum is weight 3, because both states + lie in the forward closure. + """ + right_by_prefix = {} + for index, (usage, mask) in enumerate(layers[11]): + right_by_prefix.setdefault(prefix_of(usage, mask), []).append((index, mask)) + vectors = [] + for mask in itertools.combinations(SOURCES, 3): + others = [source for source in SOURCES if source not in mask] + for mask_values in itertools.product(MASK_VALUES, repeat=3): + for other_values in itertools.product((0, 7, 14), repeat=3): + vector = [0] * K + for position, source in enumerate(mask): + vector[source] = mask_values[position] + for position, source in enumerate(others): + vector[source] = other_values[position] + if sum(vector) == 24: + vectors.append(tuple(vector)) + if len(vectors) != 700: + fail("expected 700 sum-24 weight-3 vectors, found %s" % len(vectors)) + found = [] + for left_index, (usage, mask) in enumerate(layers[5]): + left_prefix = prefix_of(usage, mask) + for vector in vectors: + needed = tuple(vector[source] - left_prefix[source] for source in SOURCES) + if min(needed) < 0 or needed not in right_by_prefix: + continue + for right_index, right_mask in right_by_prefix[needed]: + found.append((left_index, right_index, mask, right_mask, vector)) + if len(found) != 20: + fail("expected 20 free-type (9, 15) pairs, found %s" % len(found)) + by_mask = {} + for left_index, right_index, mask, right_mask, vector in found: + if mask != right_mask: + fail("(9, 15) endpoints differ: %s %s" % (mask, right_mask)) + realized = weight3_mask(vector) + complement = frozenset(SOURCES) - mask + if realized != complement: + fail("(9, 15) mask is not the complement of " + str(sorted(mask))) + left_usage = layers[5][left_index][0] + right_usage = layers[11][right_index][0] + expect_left = tuple(2 if source in mask else 0 for source in SOURCES) + expect_right = tuple(3 if source in mask else 1 for source in SOURCES) + if left_usage != expect_left or right_usage != expect_right: + fail("complement usage changed for " + str(sorted(mask))) + if prefix_of(left_usage, mask) != tuple(3 if source in mask else 0 for source in SOURCES): + fail("q9 is not 3 on the mask and 0 off it") + by_mask[mask] = (left_index, right_index) + if len(by_mask) != 20: + fail("complement pairs are not one per mask") + return by_mask + + +def check_forward(layers, successors, pairs): + """From each complement state at s=15, only stays on the complement remain.""" + for mask, (_, right_index) in pairs.items(): + complement = frozenset(SOURCES) - mask + seen = {11: {right_index}} + frontier = [right_index] + for layer in range(11, 17): + nxt = [] + for state in frontier: + usage, state_mask = layers[layer][state] + if state_mask != mask: + fail("forward mask left %s at s=%s" % (sorted(mask), layer + 4)) + for source in mask: + if usage[source] != 3: + fail("mask source is not saturated on the complement tail") + moves = letter_moves(usage, state_mask) + for target in successors[layer][state]: + new_usage, new_mask = layers[layer + 1][target] + increased = [ + source for source in SOURCES if new_usage[source] != usage[source] + ] + if new_mask != mask or len(increased) != 1 or increased[0] not in complement: + fail("forward step is not a stay on the complement") + nxt.append(target) + if not moves: + fail("complement tail died before s=21") + frontier = nxt + seen[layer + 1] = set(frontier) + if len(seen[17]) != 1: + fail("complement tail does not end at one s=21 state") + usage, state_mask = layers[17][next(iter(seen[17]))] + if usage != (3, 3, 3, 3, 3, 3) or state_mask != mask: + fail("complement tail does not saturate on the same mask") + + +def reverse_edges(successors, layer, width): + reverse = [[] for _ in range(width)] + for source, targets in enumerate(successors[layer]): + for target in targets: + reverse[target].append(source) + return reverse + + +def check_ancestors(layers, successors, pairs): + """Every free-type state from s=4 through s=9 on a complement chain carries M.""" + for mask, (left_index, _) in pairs.items(): + frontier = {left_index} + for layer in range(5, 0, -1): + reverse = reverse_edges(successors, layer - 1, len(layers[layer])) + previous = set() + for state in frontier: + previous.update(reverse[state]) + if not previous: + fail("complement state at s=9 has no ancestor at s=%s" % (layer + 3)) + for state in previous: + usage, state_mask = layers[layer - 1][state] + if state_mask != mask: + fail("ancestor mask left %s" % sorted(mask)) + prefix = prefix_of(usage, state_mask) + if any(prefix[source] for source in SOURCES if source not in mask): + fail("ancestor prefix uses the complement of %s" % sorted(mask)) + frontier = previous + if not frontier: + fail("no s=4 ancestor") + + +def walk_census(layers, successors, pairs): + """Every in-type walk from the s=9 complement state to s=15. + + The diagonal image outside s=10..14 is exactly {M}, by the ancestor and + forward checks. A walk therefore determines the image and the three + off-diagonal masks. + """ + mask_bit = { + frozenset(choice): 1 << position + for position, choice in enumerate(itertools.combinations(SOURCES, 3)) + } + summary = [] + for mask, (left_index, right_index) in sorted(pairs.items(), key=lambda item: sorted(item[0])): + complement = frozenset(SOURCES) - mask + allowed = [None] * 7 + allowed[6] = {right_index} + for depth in range(6): + reverse = reverse_edges(successors, 10 - depth, len(layers[11 - depth])) + previous = set() + for state in allowed[6 - depth]: + previous.update(reverse[state]) + allowed[5 - depth] = previous + if left_index not in allowed[0]: + fail("complement endpoints are not joined for " + str(sorted(mask))) + counts = [0] * len(layers[5]) + counts[left_index] = 1 + for step in range(6): + layer = 5 + step + nxt = [0] * len(layers[layer + 1]) + for state, count in enumerate(counts): + if not count: + continue + for target in successors[layer][state]: + if target in allowed[step + 1]: + nxt[target] += count + counts = nxt + dynamic = counts[right_index] + stats = { + "walks": 0, + "outside33": 0, + "unclassified": 0, + "max_cover": 0, + "max_cover_several": 0, + "several": 0, + "three": 0, + "cover7": 0, + } + + def visit(step, state, path): + if step == 6: + stats["walks"] += 1 + image = mask_bit[mask] + for offset, layer in ((1, 6), (2, 7), (3, 8), (4, 9), (5, 10)): + image |= mask_bit[layers[layer][path[offset]][1]] + outside = [] + if mask_bit[complement] & image == 0: + outside.append(complement) + for left_layer, left_at, right_layer, right_at in ( + (6, path[1], 10, path[5]), + (7, path[2], 9, path[4]), + ): + left_usage, left_mask = layers[left_layer][left_at] + right_usage, right_mask = layers[right_layer][right_at] + vector = tuple( + prefix_of(left_usage, left_mask)[source] + + prefix_of(right_usage, right_mask)[source] + for source in SOURCES + ) + realized = weight3_mask(vector) + if realized is None: + continue + if realized == left_mask or realized == right_mask: + continue + if left_mask != right_mask: + stats["unclassified"] += 1 + continue + if mask_bit[realized] & image == 0 and realized not in outside: + outside.append(realized) + usage12 = layers[8][path[3]][0] + if all(value in (0, 3) for value in usage12): + support = frozenset( + source for source, value in enumerate(usage12) if value == 3 + ) + if len(support) == 3 and mask_bit[support] & image == 0: + stats["outside33"] += 1 + if support not in outside: + outside.append(support) + image_size = image.bit_count() + cover = image_size + len(outside) + stats["max_cover"] = max(stats["max_cover"], cover) + if len(outside) >= 2: + stats["several"] += 1 + stats["max_cover_several"] = max(stats["max_cover_several"], cover) + if len(outside) == 3: + stats["three"] += 1 + if cover == 7: + stats["cover7"] += 1 + if image_size > 6: + fail("image exceeded the five variable indices") + return + layer = 5 + step + for target in successors[layer][state]: + if target in allowed[step + 1]: + path.append(target) + visit(step + 1, target, path) + path.pop() + + visit(0, left_index, [left_index]) + if stats["walks"] != dynamic: + fail( + "walk count diverged for %s: recursion %s dynamic %s" + % (sorted(mask), stats["walks"], dynamic) + ) + if stats["unclassified"] or stats["outside33"]: + fail("unexpected joint hit for %s: %s" % (sorted(mask), stats)) + if stats["max_cover"] != 7 or stats["max_cover_several"] != 6: + fail("cover bound changed for %s: %s" % (sorted(mask), stats)) + if stats["three"] != 72 or stats["several"] != 1044 or stats["cover7"] != 3276: + fail("joint histogram changed for %s: %s" % (sorted(mask), stats)) + if stats["walks"] != 31788: + fail("walk total changed for %s: %s" % (sorted(mask), stats["walks"])) + summary.append(stats) + if len(summary) != 20: + fail("census did not cover every mask") + return summary[0] + + +def prefixes(word): + if len(word) != 42 or any(character not in "012345" for character in word): + fail("word is not a length-42 word on six sources") + letters = [int(character) for character in word] + if any(letters.count(source) != 7 for source in SOURCES): + fail("word does not call every source seven times") + running = [0] * K + found = [tuple(running)] + for letter in letters: + running[letter] += 1 + found.append(tuple(running)) + return found + + +def pair_mask(found, left, right): + return weight3_mask( + tuple(found[left][source] + found[right][source] for source in SOURCES) + ) + + +def weight3_inventory(found): + """Every pair whose index sum can be a weight-3 coordinate sum.""" + realized = {} + for left in range(42): + for right in range(left, 42): + if (left + right - 3) % 7: + continue + mask = pair_mask(found, left, right) + if mask is not None: + realized.setdefault(mask, []).append((left, right)) + return realized + + +def diagonal_image(found): + masks = [] + for index in range(4, 23): + masks.append(pair_mask(found, index, 45 - index)) + return masks + + +def audit_three(word): + found = prefixes(word) + diagonal = diagonal_image(found) + if diagonal[:18] != [MASK_M] * 18 or diagonal[18] is not None: + fail("three-new word does not have image {(0,1,2)} and a failed centre") + if pair_mask(found, 0, 3) != MASK_M: + fail("three-new word does not realize (0, 3) as (0, 1, 2)") + inventory = weight3_inventory(found) + expected = { + MASK_M: "diagonal and (0, 3) and (33, 33)", + MASK_COMPLEMENT: (9, 15), + MASK_1014: (10, 14), + MASK_1113: (11, 13), + } + if set(inventory) != set(expected): + fail("three-new inventory changed: " + str(sorted(tuple(sorted(m)) for m in inventory))) + for mask, slot in ( + (MASK_COMPLEMENT, (9, 15)), + (MASK_1014, (10, 14)), + (MASK_1113, (11, 13)), + ): + if inventory[mask] != [slot]: + fail("three-new mask %s is not only %s" % (sorted(mask), slot)) + if (33, 33) not in inventory[MASK_M] or (0, 3) not in inventory[MASK_M]: + fail("three-new word lost (0, 3) or (33, 33) inside the image") + # The three new masks differ from the mask of (0, 3). The complement is + # also disjoint from that mask as a 3-subset. + if MASK_M & MASK_COMPLEMENT: + fail("complement meets (0, 1, 2)") + for mask in (MASK_1014, MASK_1113, MASK_COMPLEMENT): + if mask == MASK_M: + fail("a new mask equals (0, 3)") + + +def audit_sharp(word): + found = prefixes(word) + diagonal = diagonal_image(found) + if any(mask is None for mask in diagonal[:18]) or diagonal[18] is not None: + fail("sharp word is not centre-only") + image = set(diagonal[:18]) + if len(image) != 6 or MASK_M not in image or MASK_COMPLEMENT in image: + fail("sharp diagonal image is not six masks excluding the complement") + if pair_mask(found, 0, 3) != MASK_M: + fail("sharp word does not realize (0, 3) as (0, 1, 2)") + if pair_mask(found, 9, 15) != MASK_COMPLEMENT: + fail("sharp word lost the complement") + if pair_mask(found, 10, 14) is not None or pair_mask(found, 11, 13) is not None: + fail("sharp word realized a second named pair") + if pair_mask(found, 33, 33) != MASK_M: + fail("sharp (33, 33) is not the diagonal mask") + inventory = weight3_inventory(found) + if set(inventory) != image | {MASK_COMPLEMENT}: + fail("sharp inventory is not the image plus the complement") + if len(inventory) != 7: + fail("sharp cover is not 7") + + +def mutated_three_fails(): + letters = list(THREE_WORD) + letters[0] = "1" if letters[0] == "0" else "0" + try: + audit_three("".join(letters)) + except SystemExit as error: + if str(error).startswith("FAIL:"): + return + raise + fail("mutated three-new word was accepted") + + +def main(): + layers, successors = build_layers() + check_terminal(layers) + pairs = complement_pairs(layers) + check_forward(layers, successors, pairs) + check_ancestors(layers, successors, pairs) + census = walk_census(layers, successors, pairs) + audit_three(THREE_WORD) + audit_sharp(SHARP_WORD) + mutated_three_fails() + # Short proof, before the sharp census: image size <= 6, (0, 3) and + # (33, 33) add nothing, and the three named pairs add at most one mask + # each. 6 + 3 = 9 < 20. The walk census tightens 9 to 7. + if 6 + 3 >= 20 or census["max_cover"] >= 20 or census["max_cover_several"] >= 20: + fail("cover reached 20") + print( + "PASS_SIX_SOURCE_C7_TWO_PAIR_COUNT " + "endpoint_pairs=20/20 walks_per_mask=%s " + "image_at_most=6 structural_cover_at_most=9 " + "census_cover_at_most=%s several_walks=%s several_cover_at_most=%s " + "three_new_walks=%s cover7_walks=%s " + "three_word_cover=4 sharp_word_cover=7 " + "block33_outside=0 unclassified=0 controls=12" + % ( + census["walks"], + census["max_cover"], + census["several"], + census["max_cover_several"], + census["three"], + census["cover7"], + ) + ) + + +if __name__ == "__main__": + main()