From 839f7e62bb9f7d5ee3cd10d3c7e953e7f835e1f1 Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 02:08:25 +0000 Subject: [PATCH] Classify the c=6 centre on s+t=39 as empty of weight-3 masks. Every residue-legal centre count is a multiple of 3, while the centre length 19 is not, so the frozen-14 step has no characteristic-six input. The depth-two exclusion remains the PR6141 solver verdict. No kappa change. Co-authored-by: unpaidmoon --- .../README.md | 198 ++++++++++++++++++ .../SOURCES.json | 18 ++ .../TASK.json | 62 ++++++ .../VERIFY.json | 34 +++ .../verify.py | 184 ++++++++++++++++ 5 files changed, 496 insertions(+) create mode 100644 research/six-source-c6-centre-classification/README.md create mode 100644 research/six-source-c6-centre-classification/SOURCES.json create mode 100644 research/six-source-c6-centre-classification/TASK.json create mode 100644 research/six-source-c6-centre-classification/VERIFY.json create mode 100644 research/six-source-c6-centre-classification/verify.py diff --git a/research/six-source-c6-centre-classification/README.md b/research/six-source-c6-centre-classification/README.md new file mode 100644 index 0000000000..3e6b3c225c --- /dev/null +++ b/research/six-source-c6-centre-classification/README.md @@ -0,0 +1,198 @@ +# The c=6 centre on s+t=39 carries no weight-3 mask + +**Scoped classification. No new κ.** In the unchanged unsigned dirty +connector, the centre pair of the diagonal `s + t = 39` never realizes a +weight-3 mask. The frozen-14 step, which starts from a weight-3 centre and +propagates a coordinate equal to `2c`, therefore has no c=6 input. The +six-source depth-two exclusion at characteristic 6 stays the solver verdict +of PR6141. + +The selected conditional κ remains `781451/250000000` in +`certificates/selected-result.json`. + +## Interface, unchanged + +A floor word on `k = 6` sources in characteristic `c = 6` has length 36 and +calls each source exactly six times. `q_t` counts the first `t` letters, so +`q_0 = 0`, `q_36 = (6,6,6,6,6,6)`, and each step adds one basis vector. +Counts stay in `{0,...,6}`. The word has depth two when every nonzero binary +mask is congruent modulo 6 to `q_s + q_t` for some `0 ≤ s ≤ t ≤ 35`. This is +the interface of PR4231/PR4248, as used by PR6141. Boundary 36 is identified +with 0 because `q_36 = 6·1 ≡ q_0`. + +A pair realizes a **weight-3 mask** when every coordinate of `q_s + q_t` +lies in `{0,1,6,7,12}` and exactly three coordinates lie in `{1,7}`. Every +sum of two counts in `{0,...,6}` is an integer in `{0,...,12}`, and the +members of that range congruent to 0 or 1 modulo 6 are exactly +`{0,1,6,7,12}`. The value 13 is outside the range. Mask bits are the +residues 1. This is the same reading of the weight identity (PR6107) that +the c=7 diagonal note uses, specialized to `c = 6`. + +## Centre classification + +The pairs with `s + t = 39` and `s ≤ t ≤ 35` are `(s, 39-s)` for +`s = 4,...,19`. The centre is the adjacent pair `(19, 20)`: +`q_20 = q_19 + e_j` for the single letter `j` in position 19, and +`q_19[j] ≤ 5`. Write `r` for `q_19`. The centre sum is `2r + e_j`. + +The coordinate types that land in `{0,1,6,7,12}` are: + +| role | count | sum | residue | mask bit | +|---|---:|---:|---:|---:| +| other | 0 | 0 | 0 | 0 | +| other | 3 | 6 | 0 | 0 | +| other | 6 | 12 | 0 | 2·`c` carries no mask bit | +| centre | 0 | 1 | 1 | 1 | +| centre | 3 | 7 | 1 | 1 | + +No other count in `{0,...,6}` works. In particular a non-centre coordinate +is even, and every even allowed value is a mask bit 0. A centre coordinate +is odd, so it is the only coordinate that can carry a mask bit. + +Every count in the table is a multiple of 3. A residue-legal centre would +therefore have coordinate sum divisible by 3. The centre length is 19, and +`19 ≡ 1 (mod 3)`. There is no residue-legal centre, and the weight-3 subset +is empty. + +The same arithmetic still forbids a centre if the unreachable value 13 is +added to the allowed set and the centre source is allowed to have count 6. +Those counts are `{0,3}` for a sum of 1 or 7, and `6` for a sum of 13. All +three are multiples of 3. + +`verify.py` exhausts the finite domain: all `7^6` vectors with coordinates +in `{0,...,6}`, the 9,156 of them that sum to 19, and the 46,956 choices of +centre letter that have not already been used six times. None of the 46,956 +sums is residue-legal. The widened domain, 54,936 pairs with 13 admitted and +the count-6 centre letter admitted, is empty as well. This census covers the +centre pair only. It is not a census of words, and it is not a SAT run. + +## Why the frozen-14 step has no c=6 input + +On the c=7 diagonal `s + t = 45`, the equality-case argument starts from a +weight-3 centre and a coordinate equal to 14, which is `2c` at `c = 7`. +Inside `{0,1,7,8,14}` a step can add 1 only from 0 or 7 and subtract 1 only +from 1 or 8, so 14 stays fixed. If every index `s = 4,...,22` is weight-3, +that coordinate is still 14 at `s = 4`, and both sides are 7, which a +length-4 prefix cannot hold. That is the frozen-14 step. It is an argument +about the equality case in which all 20 weight-3 masks sit on the 20 +diagonal slots. + +At `c = 6` the analogous allowed set is `{0,1,6,7,12}`. A step can add 1 +only from 0 or 6 and subtract 1 only from 1 or 7, so the immovable value is +12, which is `2c` at `c = 6`. The integer 14 is congruent to 2 modulo 6, so +it is not a weight-3 coordinate in this characteristic. The centre +classification supplies no residue-legal vector on which a 12 could sit. +The induction that keeps a frozen coordinate from the centre down to `s = 4` +therefore does not start. + +Nick Petalas's handoff of 2026-11-03 already records that the two-diagonal +model `s + t ∈ {3, 39}` has 17 slots against `C(6,3) = 20`, so that +restricted model is impossible by counting. The centre classification +removes the centre slot from those 17. The other early candidate `(1, 2)` +has sum `2e_a + e_b` or `3e_a`, and neither 2 nor 3 lies in +`{0,1,6,7,12}`. The only early pair left is `(0,3)`. At most the 15 indices +`s = 4,...,18`, plus that one early pair, remain: 16 slots. Sixteen is +still less than 20. The count, with or without the dead centre, is a human +proof of this restricted model only. PR6141's exclusion is the unrestricted +depth-two statement, in which a weight-3 mask may use any pair with +`s + t ≡ 3 (mod 6)`. + +## Weight-3 sums that sit off the centre + +The centre obstruction is local. Two explicit floor words realize a +weight-3 mask somewhere else. Both call each source six times. Neither is +claimed to have depth two. + +Separation 3 on the same diagonal. The word + +```text +333333444444555555012000001111122222 +``` + +has `q_18 = (0,0,0,6,6,6)` and `q_21 = (1,1,1,6,6,6)`. The sum is +`(1,1,1,12,12,12)`, a weight-3 mask, at `s + t = 39`. Its centre sum is +`(2,1,0,12,12,12)`, which contains a 2. The three coordinates equal to 12 +are immovable under the c=6 move table, and this one pair does not force +them down through `s = 4`, because the centre index between 18 and the +early indices is not weight-3. + +Off this diagonal, `s + t = 9`. The word + +```text +333333012000001111122222444444555555 +``` + +has `q_9 = (1,1,1,6,0,0)`, so `(0,9)` is a weight-3 mask. + +The handoff's c=7 prefix `jjjjabc` does not give a c=6 weight-3 mask. +`q_3 + q_7 = 7e_j + e_a + e_b + e_c`. At characteristic 7 the coefficient 7 +is a mask bit 0, and the sum realizes `{a,b,c}`. At characteristic 6 the +same coefficient is a mask bit 1, and four coordinates are mask bits. + +## What this establishes + +Under the hypotheses above, the centre of `s + t = kc + 3` at `c = 6` has +no weight-3 realization, and no residue-legal realization. The frozen-14 +step does not become a human proof of the c=6 depth-two exclusion: its +hypothesis, a weight-3 centre carrying the value `2c`, is empty here, while +the exclusion quantifies over pairs that are not that centre. PR6141's +CaDiCaL 1.9.5 and MapleChrono UNSAT verdicts remain solver evidence. This +package does not rerun them, does not emit a DRAT certificate, and does not +treat that UNSAT as a human proof. + +The c=5 centre is a different characteristic and is not classified here. +The c=7 question of replacing one diagonal index by an off-diagonal pair is +a different question. 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-c6-centre-classification/verify.py +python3.12 -I -O -W error -B research/six-source-c6-centre-classification/verify.py +python3.12 -B scripts/research_package.py --package research/six-source-c6-centre-classification --check-only +``` + +The marker is + +```text +PASS_SIX_SOURCE_C6_CENTRE_CLASSIFICATION sum19=9156 examined=46956 residue_legal=0 weight3=0 mod3_shapes=0 widened_legal=0 moves=+[0, 6]/-[1, 7] frozen_value=12 controls=8 +``` + +The eight controls accept two synthetic weight-3 sums, reject a centre sum +that contains a 2, record that the c=7 prefix has weight 4 at c=6, check +both explicit floor words, check that a multiple-of-3 vector can sum to 18, +and reject both integer shapes of the pair `(1,2)`. Failures raise +`SystemExit`. Optimized mode cannot silence them. + +## Open next questions + +1. Which human step, other than frozen-14, proves the c=6 depth-two + exclusion? *Why:* PR6141's c=6 verdict is still two solver runs, and the + centre classification gives that induction nothing to freeze. *First + step:* classify the separation-3 pairs on `s + t = 39`, starting from the + explicit type `q_18 = (0,0,0,6,6,6)` with three frozen coordinates equal + to 12, and price one mask realized at `s + t = 9` against those slots. + *Blocked by:* the centre index is empty, so a chain through every + diagonal index is unavailable, and the `s + t = 9` witness lies off the + diagonal the freeze follows. The c=6 DRAT certificate named in PR6216 is + a separate budget and is not this step. + +## Credit + +The depth-two interface and the weight identity are Nick Petalas's +(PR4231, PR4248, PR6107), with the Ross Richardson PR934/PR943 lineage. +JosieElliston's PR6141 records the c=6 solver verdict and leaves the human +proof open. Nick Petalas's handoff on 2026-11-03 +([discussion comment 19384981](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19384981)) +states the diagonal slot count, the centre shape at c=7, and the off-diagonal +prefix. The frozen-14 equality-case argument at c=7 is the fork draft +[PR156](https://github.com/unpaidmoon/integer-mult-bounds/pull/156), recorded +upstream as discussion comment 19493159. It is not an upstream merge. +queelius's open PR6216 certifies characteristic five and names a +characteristic-six certificate as later work; this package does not produce +that certificate. zxv's PR6057 and JosieElliston's PR6061 supply the +`c ≥ 8` words, which have spare diagonal slots. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/six-source-c6-centre-classification/SOURCES.json b/research/six-source-c6-centre-classification/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/six-source-c6-centre-classification/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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-c6-centre-classification/TASK.json b/research/six-source-c6-centre-classification/TASK.json new file mode 100644 index 0000000000..c5e22558c5 --- /dev/null +++ b/research/six-source-c6-centre-classification/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Classify the centre pair (19, 20) on s+t=39 for a six-source floor word in characteristic 6, and decide whether the frozen-14 step yields a human proof of the c=6 depth-two exclusion. The centre is empty of residue-legal sums, so the step has no c=6 input. The unrestricted exclusion remains PR6141's solver verdict.", + "scope_change_reason": "The catalogue card asks for one new connector operation. This package keeps the unsigned dirty connector alphabet fixed and answers the c=6 half of the released question in the c=7 diagonal note: whether the frozen-14 step becomes a human proof of the characteristic-six exclusion. The declared first step is the centre of s+t=kc+3 at c=6. 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. The centre classification records why the c=7 equality-case argument has no characteristic-six input.", + "budget_minutes": 60, + "stop_rule": "Stop after the centre classification and the decision on the frozen-14 step. Do not start a c=6 DRAT certificate, a c=5 centre classification, or a c=7 off-diagonal replacement.", + "outcome": "negative-result", + "evidence": "Written proof that every residue-legal centre count is a multiple of 3 while the centre length 19 is not, plus an exhaustive standard-library census of all 9156 length-19 count vectors and 46956 legal centre letters: 0 residue-legal sums and 0 weight-3 sums. The c=6 move table freezes 12, and no centre carries a 12. Two explicit floor words realize a weight-3 mask off the centre. Eight controls. No SAT solver was run.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: the classification, the exhaustive checker, and the package text.", + "open_questions": [ + { + "question": "Which human step, other than the frozen-14 centre induction, proves the six-source depth-two exclusion at c=6?", + "why_it_matters": "PR6141's c=6 verdict is a solver UNSAT. The centre of s+t=39 is empty, so that induction has no coordinate to freeze, and the exclusion remains open as a human proof.", + "first_step": "Classify separation-3 pairs on s+t=39, starting from q_18=(0,0,0,6,6,6) with three coordinates equal to 12, and price the explicit mask at s+t=9 against those slots.", + "blocked_by": "The centre index is empty, so the chain through every diagonal index is unavailable. The s+t=9 witness is off the diagonal the freeze follows. The c=6 DRAT certificate named in PR6216 is a separate budget." + } + ] +} diff --git a/research/six-source-c6-centre-classification/VERIFY.json b/research/six-source-c6-centre-classification/VERIFY.json new file mode 100644 index 0000000000..97145a8c81 --- /dev/null +++ b/research/six-source-c6-centre-classification/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": 60, + "checks": "Exhaustive centre census: 9156 length-19 count vectors, 46956 legal centre letters, 0 residue-legal sums and 0 weight-3 sums. Type table even counts {0,3,6} and centre counts {0,3}; no such 6-tuple sums to 19. Widened census admitting 13 and a count-6 centre letter has 0 legal sums. Move table freezes 12. Eight controls cover a synthetic weight-3 sum, the separation-3 sum, a rejected centre sum, the c=7 prefix at weight 4, both explicit floor words, a length-18 multiple of 3, and both shapes of the pair (1,2)." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same census and controls under optimized Python. Failures are SystemExit, not assertions." + } + ] +} diff --git a/research/six-source-c6-centre-classification/verify.py b/research/six-source-c6-centre-classification/verify.py new file mode 100644 index 0000000000..d02bc95c9a --- /dev/null +++ b/research/six-source-c6-centre-classification/verify.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Exhaustive centre census for the c=6 diagonal s+t=39. + +The written argument is in README.md. This program enumerates every length-19 +count vector and every legal centre letter. It does not search words and it +does not call a SAT solver. +""" +import itertools + +K = 6 +C = 6 +CENTRE_LENGTH = 19 +ALLOWED = (0, 1, 6, 7, 12) +ALLOWED_SET = set(ALLOWED) +# 13 would be 6+6+1. It is unreachable for two counts in 0..6, and it is +# kept here only as a widened control. +WIDENED = ALLOWED_SET | {13} +MASK_BIT = {0: 0, 1: 1, 6: 0, 7: 1, 12: 0, 13: 1} + + +def fail(msg): + raise SystemExit("FAIL: " + msg) + + +def mask_weight(sum_vec, allowed): + """Return the number of mask bits, or None if any coordinate is illegal.""" + bits = 0 + for value in sum_vec: + if value not in allowed: + return None + bits += MASK_BIT[value] + return bits + + +def weight3(sum_vec): + return mask_weight(sum_vec, ALLOWED_SET) == 3 + + +def prefix_counts(word, length): + counts = [0] * K + for source in word[:length]: + counts[source] += 1 + return counts + + +def centre_pair_sum(counts, centre): + return [2 * counts[j] + (1 if j == centre else 0) for j in range(K)] + + +def main(): + sum19 = 0 + examined = 0 + residue_legal = 0 + weight3_centres = 0 + for counts in itertools.product(range(C + 1), repeat=K): + if sum(counts) != CENTRE_LENGTH: + continue + sum19 += 1 + for centre in range(K): + # The centre letter is still ahead of q_19, so that source has + # at most five calls already. + if counts[centre] >= C: + continue + examined += 1 + summed = centre_pair_sum(counts, centre) + if mask_weight(summed, ALLOWED_SET) is None: + continue + residue_legal += 1 + if weight3(summed): + weight3_centres += 1 + fail(f"weight-3 centre exists: q={counts} centre={centre} sum={summed}") + if (sum19, examined, residue_legal, weight3_centres) != (9156, 46956, 0, 0): + fail( + "centre census changed: " + f"sum19={sum19} examined={examined} " + f"residue_legal={residue_legal} weight3={weight3_centres}" + ) + + # Type table: the only counts whose double, or double plus one, lands in + # the allowed set. Seven values, all checked. + even_counts = [r for r in range(C + 1) if 2 * r in ALLOWED_SET] + odd_counts = [r for r in range(C + 1) if 2 * r + 1 in ALLOWED_SET] + if even_counts != [0, 3, 6] or odd_counts != [0, 3]: + fail(f"type table changed: even={even_counts} odd={odd_counts}") + mod3_shapes = sum( + 1 + for counts in itertools.product((0, 3, 6), repeat=K) + if sum(counts) == CENTRE_LENGTH + ) + if mod3_shapes != 0: + fail(f"a multiple-of-3 count vector sums to 19: {mod3_shapes}") + + # Widened control: admitting the unreachable value 13, and admitting a + # centre source that has already been used six times, is still empty. + widened_trials = 0 + widened_legal = 0 + for counts in itertools.product(range(C + 1), repeat=K): + if sum(counts) != CENTRE_LENGTH: + continue + for centre in range(K): + widened_trials += 1 + summed = centre_pair_sum(counts, centre) + if mask_weight(summed, WIDENED) is not None: + widened_legal += 1 + if (widened_trials, widened_legal) != (54936, 0): + fail(f"widened census changed: trials={widened_trials} legal={widened_legal}") + + increments = [v for v in ALLOWED if v + 1 in ALLOWED_SET] + decrements = [v for v in ALLOWED if v - 1 in ALLOWED_SET] + if increments != [0, 6] or decrements != [1, 7]: + fail(f"move table changed: +{increments} -{decrements}") + if 12 in increments or 12 in decrements or 14 in ALLOWED_SET: + fail("12 is movable or 14 is an allowed c=6 coordinate") + + controls = 0 + if not weight3((1, 1, 1, 0, 6, 12)): + fail("predicate rejected a weight-3 sum") + controls += 1 + if not weight3((1, 1, 1, 12, 12, 12)): + fail("predicate rejected the separation-3 sum") + controls += 1 + if weight3((2, 1, 0, 12, 12, 12)): + fail("predicate accepted a centre sum with a 2") + controls += 1 + # The c=7 handoff prefix realizes weight 4 at c=6. + handoff = prefix_counts([3, 3, 3, 3, 0, 1, 2], 3) + handoff_late = prefix_counts([3, 3, 3, 3, 0, 1, 2], 7) + handoff_sum = [handoff[j] + handoff_late[j] for j in range(K)] + if handoff_sum != [1, 1, 1, 7, 0, 0] or mask_weight(handoff_sum, ALLOWED_SET) != 4: + fail(f"handoff prefix transferred incorrectly: {handoff_sum}") + controls += 1 + + diagonal = ( + [3] * 6 + [4] * 6 + [5] * 6 + [0, 1, 2] + [0] * 5 + [1] * 5 + [2] * 5 + ) + if len(diagonal) != K * C or sorted(diagonal) != sorted(source for source in range(K) for _ in range(C)): + fail("separation-3 witness is not a floor word") + q18 = prefix_counts(diagonal, 18) + q21 = prefix_counts(diagonal, 21) + q19 = prefix_counts(diagonal, 19) + sep_sum = [q18[j] + q21[j] for j in range(K)] + centre_sum = [q19[j] + prefix_counts(diagonal, 20)[j] for j in range(K)] + if sep_sum != [1, 1, 1, 12, 12, 12] or not weight3(sep_sum): + fail(f"separation-3 pair is not weight 3: {sep_sum}") + if centre_sum != [2, 1, 0, 12, 12, 12] or weight3(centre_sum): + fail(f"same word has a weight-3 centre: {centre_sum}") + if diagonal[19] != 1 or q19[1] != 0: + fail("centre letter of the witness moved") + controls += 1 + + off = [3] * 6 + [0, 1, 2] + [0] * 5 + [1] * 5 + [2] * 5 + [4] * 6 + [5] * 6 + if len(off) != K * C or sorted(off) != sorted(diagonal): + fail("s+t=9 witness is not a floor word") + q9 = prefix_counts(off, 9) + if q9 != [1, 1, 1, 6, 0, 0] or not weight3(q9): + fail(f"s+t=9 pair is not weight 3: {q9}") + controls += 1 + + # Multiples of 3 can sum to 18, so the obstruction is the length 19. + if sum((6, 6, 6, 0, 0, 0)) != 18: + fail("length-18 shape disappeared") + controls += 1 + + # s+t=3 has two candidate pairs. (1,2) is 2e_a+e_b or 3e_a. + for early in ((2, 1, 0, 0, 0, 0), (3, 0, 0, 0, 0, 0)): + if weight3(early): + fail(f"(1,2) was accepted: {early}") + controls += 1 + + if controls != 8: + fail(f"control count changed: {controls}") + + print( + "PASS_SIX_SOURCE_C6_CENTRE_CLASSIFICATION " + f"sum19={sum19} examined={examined} " + f"residue_legal={residue_legal} weight3={weight3_centres} " + f"mod3_shapes={mod3_shapes} widened_legal={widened_legal} " + f"moves=+{increments}/-{decrements} frozen_value=12 " + f"controls={controls}" + ) + + +if __name__ == "__main__": + main()