diff --git a/research/c5-mask-centre-nondetermination/README.md b/research/c5-mask-centre-nondetermination/README.md new file mode 100644 index 0000000000..e0a0e44ae4 --- /dev/null +++ b/research/c5-mask-centre-nondetermination/README.md @@ -0,0 +1,352 @@ +# Separate c=5 weight-2-family and all-ones-window centre counterexamples + +**Two separate counterexamples. No new κ.** In the unchanged unsigned dirty +connector, the following are established separately. They do not combine. + +1. No individual all-ones window forces `S(16) = q_16 + q_17` to be legal. + Every admissible window has a floor word with that window and an illegal + centre. Some windows also have a legal-centre word. None forces the legal + polarity. +2. The fifteen weight-2 masks, as a family and without the weight-6 mask, + admit both polarities. One floor word realizes all fifteen with an illegal + centre, and another realizes all fifteen with a legal centre. + +No conclusion is established about a word that realizes all fifteen weight-2 +masks and the weight-6 mask together. That conjunction is not shown to force +a legal centre, and it is not shown to admit an illegal centre. This holds +whether or not such a word exists. The selected conditional κ stays +`781451/250000000`. Hypothesis (H) of the centre-freeze is not proved. + +## Proved statement + +Let a floor word of length 30 call each of six sources exactly five times. +Write `q_t` for the count vector of the first `t` letters. Letters are +`w_0,...,w_29`, with `q_{t+1} = q_t + e_{w_t}`. For the adjacent pair at +the middle of `s + t = 33`, + +```text +S(16) = q_16 + q_17 = 2 q_16 + e_{w_16}. +``` + +Let `A = {0,1,5,6,10}`. Call `S(16)` **legal** when every coordinate lies in +`A`, and **illegal** otherwise. The same reading as PR #7038: a coordinate +sum in `{0,...,10}` lies in `A` exactly when it is congruent to 0 or 1 +modulo 5, and the mask bit is 1 exactly on `{1,6}`. + +**Result A.** No individual all-ones window forces a legal centre. There +are 4095 admissible ways to assign coordinate types to one all-ones window. +For every one of them there is a length-30 floor word that realizes that +window and has illegal `S(16)`. For 1731 of them there is also a floor word +with the same window and legal `S(16)`. No window forces `S(16)` to be +legal. Of the 2364 windows that force it to be illegal, 1573 do so because +`q_16` cannot contain a coordinate 0, by the three human classes below. The +other 791 admit a coordinate 0, but none of their feasible vectors `q_16` +is a legal centre; that last split is the exhaustive comparison in +`verify.py`. Each of these words is a witness for one window. A window +witness does not realize every weight-2 mask, and Result A does not quantify +over words that realize the weight-6 mask together with all fifteen weight-2 +masks. + +**Result B.** The fifteen weight-2 masks admit both centre polarities. The +sorted floor word realizes all fifteen and has illegal `S(16)`. The explicit +word `001211112322203343354444555500` realizes all fifteen and has legal +`S(16)`. Neither word realizes the weight-6 mask. Result B is a statement +about that family alone. + +The weight identity is rechecked and is not a third result about the +conjunction. Every 6-tuple with coordinates in `A` has coordinate sum +congruent to its mask weight modulo 5. A tuple of sum 33 therefore has +weight 3. A single pair with `s + t = 33` cannot realize a weight-2 mask or +the weight-6 mask. That says where one mask can sit. It does not say whether +realizing every weight-2 mask and the weight-6 mask on other pairs forces +`S(16)` to be legal. + +The evidence class is an exhaustive finite census. The domains are finite: +the 36 ordered pairs of counts in `{0,...,5}`, the centre vectors of sum 16, +the 4095 type assignments, the bounded compositions for `q_16`, and the 465 +pairs of each explicit word. The completeness argument is the case split +below. The checker does not call a SAT solver. Two of the explicit words +were first found by a local CaDiCaL search; the census then checks those +words directly. A failed search is not used as evidence. + +## Interface, unchanged + +This is the depth-two interface of PR #4231 and PR #4248, as used by +PR #6141 and by the centre classification in PR #7038. A pair +`0 ≤ s ≤ t ≤ 29` realizes a binary mask when `q_s + q_t` has every +coordinate in `A`. The coordinate sum is `s + t`, so a realized mask of +weight `w` has `s + t ≡ w (mod 5)`. Nothing here adds a connector operation. +Boundary 30 is not a second endpoint: `q_30` is the all-fives vector. + +Hypothesis (H) from PR #7038 asks every `S(s) = q_s + q_{33-s}`, for +`s = 4,...,16`, to be legal. That note proves (H) is empty for every floor +word, because a legal `S(16)` freezes a coordinate at 10 and the diagonal +step cannot move 10 inside `A`. It leaves open whether every depth-two +floor word satisfies (H). One proposed route was to derive a legal `S(16)` +from the sixteen masks of weights 2 and 6. This note does not decide that +route. Result A is about one all-ones window at a time. Result B is about +the weight-2 masks without the weight-6 mask. A word that realizes both at +once is not covered by either result. + +## Coordinate types of an all-ones window + +The weight-6 mask is the all-ones vector. A realizing pair has every +coordinate sum in `{1,6}`. Since `q_t ≥ q_s` coordinatewise and both counts +lie in `{0,...,5}`, the only possibilities are: + +| type | `q_s` | `q_t` | letters in the window | +|---|---:|---:|---:| +| A | 0 | 1 | 1 | +| B | 1 | 5 | 4 | +| C | 2 | 4 | 2 | +| D | 3 | 3 | 0 | + +Sum 1 is only `0+1`. Sum 6 with the first count at most the second is +`1+5`, `2+4`, or `3+3`. The pairs `0+6` and `6+0` use a count 6, which a +single prefix does not have. The checker scans all `6 × 6` ordered pairs +and finds these four. + +An assignment of types to the six sources determines + +```text +s = n_B + 2 n_C + 3 n_D, t - s = n_A + 4 n_B + 2 n_C. +``` + +The assignment is admissible when `0 ≤ s ≤ t ≤ 29`. There are 4095 such +assignments. The same count is the sum of the multinomial coefficients +`6! / (n_A! n_B! n_C! n_D!)` over the admissible multiplicity vectors, so +the distinct permutations were not under-counted. Every floor word that +realizes the all-ones mask has one of these 4095 windows: its prefixes at +the realizing boundaries are one of the four types in each coordinate. + +## Which vectors `q_16` a window allows + +Fix an admissible window, and write `δ` for the letter counts between `s` +and `t`. The position of 16 relative to the window puts `q_16` in exactly +one of three finite sets. + +- If `t ≤ 16`, then `q_16 = q_t + e` where `e` sums to `16 - t` and + `0 ≤ e_j ≤ 5 - q_t[j]`. +- If `s ≥ 16`, then `q_16 = q_s - d` where `d` sums to `s - 16` and + `0 ≤ d_j ≤ q_s[j]`. +- If `s < 16 < t`, then `q_16 = q_s + c` where `c` sums to `16 - s` and + `0 ≤ c_j ≤ δ_j`. + +Each set is a set of bounded compositions. Any such vector extends to a +floor word with the prescribed window: place the determined multiset on +each block, and append the missing copies so that every source ends at 5. +The centre letter `w_16` has to lie in the block that contains position 16. +In every one of the 4095 windows, every feasible vector that the centre +test accepts or rejects has such a letter available. The constructions +below use one explicit letter and are checked as floor words. + +A centre is legal only for the two shapes already classified in PR #7038. +The checker does not trust that classification for the zero lemma: it +enumerates every `q_16 ∈ {0,...,5}^6` of sum 16 and every centre letter +used at most four times, and it finds 300 legal pairs. The count vector of +every one of those pairs contains a coordinate 0. The short reason is the same two-row +arithmetic. A non-centre coordinate of a legal centre lies in `{0,3,5}`, +and the centre letter lies in `{0,2}`. + +- Centre letter 0. The count equation is `3 n_3 + 5 n_5 = 16` on the other + five coordinates. The only solution in range is two 3s, two 5s and a 0. +- Centre letter 2. The equation is `3 n_3 + 5 n_5 = 14`. The only solution + is three 3s, one 5 and a 0. + +Both rows contain a 0. A vector with no coordinate 0 is not a legal centre, +whatever letter follows it. + +## Three classes in which `q_16` has no zero + +These classes are disjoint, and every window outside them has at least one +feasible `q_16` that does contain a 0. The checker compares the class +predicate with the enumerated vectors on all 4095 assignments. + +**Early, 845 windows.** The window ends at `t ≤ 16`. Every type has +`q_t ∈ {1,3,4,5}`, so `q_16 ≥ q_t` has no coordinate 0. + +**Covering and not of type A, 721 windows.** There is no type-A source, and +`s ≤ 16 ≤ t`. Then `q_s` lies in `{1,2,3}^6`, and inside the window +`q_16 ≥ q_s`. + +**Tight drop, 7 windows.** There is no type A or B. + +- One C and five D: `s = 17`, `t = 19`, and `q_17` is a 2 and five 3s. + The single letter in position 16 reduces one coordinate by 1, which + cannot produce a 0. There are 6 places for the C. +- Six D: `s = t = 18`, and `q_18 = (3,3,3,3,3,3)`. The two letters in + positions 16 and 17 reduce the all-threes vector by one or two. The + resulting 21 vectors are fifteen with two 2s and six with a single 1. + The minimum coordinate is 1. + +That is `845 + 721 + 7 = 1573` windows. Each forces `S(16)` illegal, and +each has a constructed floor word realizing the window. + +## The other windows + +The remaining `4095 - 1573 = 2522` windows each have at least one feasible +`q_16` containing a 0. Comparing those vectors with the 300 legal centres +splits them in two. + +- **1731 windows admit both polarities.** For each, the checker builds one + floor word with legal `S(16)` and one with illegal `S(16)`, both + realizing the same window. +- **791 windows admit a zero but no legal centre.** Every feasible vector + was compared with the centre test. This comparison is the exhaustive + census. It is not a second closed-form classification of those 791 + multiplicity vectors. + +No window lands in a third bin. In particular, **no all-ones window forces +`S(16)` to be legal.** The checker builds 5826 floor words: +`2364` illegal-only windows, plus two words for each of the 1731 flexible +windows. Each constructed word is checked to be a floor word, to reproduce +the prescribed prefixes at `s`, `t` and 16, to realize all-ones on that +window, and to have the claimed centre polarity. + +One flexible window is visible by hand. The word + +```text +012300333300112241122545545544 +``` + +has `q_4 = (1,1,1,1,0,0)` and `q_22 = (5,5,5,5,1,1)`. The sum is +`(6,6,6,6,1,1)`, all-ones, at `s + t = 26`. Its centre is + +```text +q_16 = (5,3,3,5,0,0), w_16 = 4, S(16) = (10,6,6,10,1,0), +``` + +which is legal. The same prefixes are realized by + +```text +012311222233334500001144445555 +``` + +with `q_16 = (1,3,5,5,1,1)`, `w_16 = 0` and +`S(16) = (3,6,10,10,2,2)`, which is illegal. The two words share the +window and differ on the centre. This is one of the 1731, not a substitute +for the census. + +## The fifteen weight-2 masks + +The sorted word `00000 11111 22222 33333 44444 55555`, written without +spaces as `000001111122222333334444455555`, realizes every weight-2 mask. +For `0 ≤ a < b ≤ 5` take the boundaries `s = 5a + 1` and `t = 5b + 1`. +The prefix `q_{5a+1}` is ones on sources `0,...,a-1`, a single `a`, and +zeros after that, and likewise for `b`. Their sum is 10 on sources before +`a`, 6 on `a`, 5 on the sources strictly between `a` and `b`, 1 on `b`, +and 0 after `b`. The mask bits are exactly `{a,b}`. There are +`C(6,2) = 15` such pairs, and `s + t = 5(a+b) + 2 ≡ 2 (mod 5)`. The full +scan of the 465 pairs finds no further weight-2 mask and no weight-6 mask. +The centre is `q_16 = (5,5,5,1,0,0)`, `w_16 = 3`, +`S(16) = (10,10,10,3,0,0)`. The coordinate 3 is outside `A`. + +Swapping positions 0 and 5 drops four of those fifteen masks. The checker +rejects that swap as a control. + +The word + +```text +001211112322203343354444555500 +``` + +also realizes all fifteen weight-2 masks, and no weight-6 mask. Its centre +is `q_16 = (3,5,5,3,0,0)`, `w_16 = 4`, +`S(16) = (6,10,10,6,1,0)`, which is legal of weight 3. The checker scans +all 465 pairs. This word was found by a local solver and is checked here +as a literal; the solver is not part of the replay. + +Thus the fifteen weight-2 masks, without the weight-6 mask, occur with both +centre polarities. That is Result B. It does not restrict the centre of a +word that also realizes the weight-6 mask. + +## One six-D window that also meets thirteen weight-2 masks + +The word + +```text +102431540325045231253054314120 +``` + +has `q_18 = (3,3,3,3,3,3)`, so `(18, 18)` is the six-D window in the tight +class above, and `S(16) = (6,4,6,5,6,6)` is illegal for that window reason. +The same word also realizes 13 of the 15 weight-2 masks. The two it misses +are `(0,0,1,0,1,0)` and `(0,1,0,0,0,1)`. This is one checked example inside +Result A. It is not a classification of those thirteen masks together with +weight 6, and it is not a statement about the conjunction of all fifteen +weight-2 masks with the weight-6 mask. + +## What these two results do not say + +Result A and Result B are separate. A counterexample to one all-ones window, +and a pair of counterexamples to the weight-2 family alone, do not imply a +counterexample to their conjunction. No conclusion about that conjunction is +established here, including in the case where a word realizing all fifteen +weight-2 masks and the weight-6 mask exists. + +PR #7038 asked whether those sixteen masks force a legal `S(16)`, which with +the centre-freeze would empty (H). This package does not answer that +question. + +Merged PR #6216 asserts that no floor word realizes all sixteen masks. This +package does not replay that certificate and does not use the asserted empty +fibre as a reason to call the centre legal or illegal. Emptiness, if +granted, would make both polarities vacuous; that is #6216's claim, not a +result of this census. + +No supplier, consumer, or selected frontier changes. The live selected +record at the base commit is κ `= 781451/250000000 = 0.003125804`. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/c5-mask-centre-nondetermination/verify.py +python3.12 -I -O -W error -B research/c5-mask-centre-nondetermination/verify.py +python3.12 -B scripts/research_package.py --package research/c5-mask-centre-nondetermination --check-only +``` + +The marker token is the package id. Its counts are the two separate checks: +`legal_only=0` and `weight6_forces_legal=0` are Result A, and +`weight2_polarities=2` is Result B. The fields `joint_weight2=13` and +`joint_missing=2` count masks on the single six-D example above. They are +not a result about the conjunction of all fifteen weight-2 masks with the +weight-6 mask. + +```text +PASS_C5_MASK_CENTRE_NONDETERMINATION assignments=4095 illegal_only=2364 both=1731 legal_only=0 no_zero=1573 zero_but_illegal=791 classes=845+721+7 constructed=5826 midpoint_q16=21 weight2_polarities=2 weight6_forces_legal=0 joint_weight2=13 joint_missing=2 controls=9 +``` + +The nine controls are the near-miss centre `(3,3,3,3,3,1)`, the agreement of +the human no-zero classes with the enumerated vectors, the 21 midpoint +vectors, the weight identity on every allowed 6-tuple, the sorted staircase +and its centre, the swapped sorted word, the legal weight-2 witness, the +flexible all-ones pair and its illegal twin, and the six-D example that +meets 13 weight-2 masks. +Failures raise `SystemExit`. Optimized mode cannot silence them. No Lean, +Docker, or historical suite was run. + +## Open next questions + +1. For a floor word that realizes all fifteen weight-2 masks and the + weight-6 mask together, what is the status of `S(16)`? + *Why:* Result A and Result B do not apply to that word. PR #7038 still + lacks a derivation of a legal centre from that conjunction, and this + package does not provide one. + *First step:* state the conjunction as its own hypothesis, separate from + the one-window census and from the weight-2 family. This package does not + take that step. + *Blocked by:* no joint word is constructed or excluded here. PR #6216's + empty-fibre assertion is not an input to this census. + +## 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 is the solver exclusion. queelius's merged +PR #6216 is the characteristic-5 DRAT certificate; it is not replayed here. +The centre-freeze and the statement of (H) are PR #7038. The sorted word is +the weight-two control of `research/connector-six-source-small-char`. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/c5-mask-centre-nondetermination/SOURCES.json b/research/c5-mask-centre-nondetermination/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/c5-mask-centre-nondetermination/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/c5-mask-centre-nondetermination/TASK.json b/research/c5-mask-centre-nondetermination/TASK.json new file mode 100644 index 0000000000..d073809a19 --- /dev/null +++ b/research/c5-mask-centre-nondetermination/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": "Characteristic 5 only, six sources, unchanged unsigned dirty connector. Two separate results: no individual all-ones window forces a legal S(16), and the fifteen weight-2 masks admit both centre polarities. No conclusion about the conjunction of all fifteen weight-2 masks with the weight-6 mask, including when that conjunction is satisfiable. No kappa change.", + "scope_change_reason": "The catalogue card asks for one new connector operation. This package keeps the alphabet fixed and records two separate centre counterexamples toward the first open question of open PR 7038. It does not decide whether the sixteen masks together determine the sum-33 centre. A new operation is not the missing step. The adjacent-centre question, the c=6 and c=7 remainders, and the merged DRAT certificate in PR 6216 are other questions.", + "bottleneck_link": "Side result on the recursive-interface schedule. It does not change a supplier, a consumer, or kappa. One all-ones window at a time, and the weight-2 family without the weight-6 mask, each fail to force a legal sum-33 centre. Those two facts do not speak to a word that realizes both together.", + "budget_minutes": 60, + "stop_rule": "Stop when every admissible all-ones window is classified against S(16) and the fifteen weight-2 masks are realized at both centre polarities, or when a window that forces a legal centre appears.", + "outcome": "partial", + "evidence": "Two separate exhaustive checks. Result A: 4095 all-ones type assignments, of which 2364 force an illegal centre (1573 because q_16 cannot contain a 0, by three human classes 845+721+7, and 791 by comparing every feasible vector with the 300 legal centres) and 1731 admit both polarities, with 5826 constructed floor words; no individual window forces a legal centre. Result B: the sorted staircase realizes all 15 weight-2 masks with an illegal centre, and one explicit word realizes them with a legal centre; neither word realizes weight 6. Rechecked, not a conjunction claim: no allowed 6-tuple of sum 33 has weight 2 or 6. No conclusion is established about a word that realizes all fifteen weight-2 masks and the weight-6 mask together.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: census design, verifier, and packaging. Two witness words were first found with a local CaDiCaL search through python-sat and are checked in the standard-library verifier; the replay does not call a solver.", + "open_questions": [ + { + "question": "For a floor word that realizes all fifteen weight-2 masks and the weight-6 mask together, what is the status of S(16)?", + "why_it_matters": "Result A and Result B do not apply to that word. PR 7038 still lacks a derivation of a legal centre from that conjunction, and this package does not provide one.", + "first_step": "State the conjunction as its own hypothesis, separate from the one-window census and from the weight-2 family. This package does not take that step.", + "blocked_by": "No joint word is constructed or excluded here. The PR 6216 empty-fibre assertion is not an input to this census." + } + ] +} diff --git a/research/c5-mask-centre-nondetermination/VERIFY.json b/research/c5-mask-centre-nondetermination/VERIFY.json new file mode 100644 index 0000000000..21d02ec62a --- /dev/null +++ b/research/c5-mask-centre-nondetermination/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": "Two separate checks. Result A: exhaustive census of all 4095 admissible all-ones windows at c=5. Expect 2364 illegal-only windows, 1731 windows with both centre polarities, and 0 windows that force a legal centre. The 1573 no-zero windows split as the human classes 845+721+7. Build 5826 floor words. Result B: the sorted weight-2 staircase and one legal weight-2 witness. Also check one flexible all-ones pair and its illegal twin, one six-D window that meets 13 weight-2 masks (not a conjunction-16 result), the weight identity, and the near-miss centre." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same census under optimized Python. Failures are explicit SystemExit calls, not assertions." + } + ] +} diff --git a/research/c5-mask-centre-nondetermination/verify.py b/research/c5-mask-centre-nondetermination/verify.py new file mode 100644 index 0000000000..f324c92d0a --- /dev/null +++ b/research/c5-mask-centre-nondetermination/verify.py @@ -0,0 +1,490 @@ +#!/usr/bin/env python3 +"""Two separate c=5 centre counterexamples. + +Result A: no individual all-ones window forces a legal sum-33 centre. +Result B: the fifteen weight-2 masks admit both centre polarities. +No conclusion is drawn about a word that realizes both together. + +Evidence class: exhaustive finite census. The human completeness argument +is in README.md. This program enumerates every admissible all-ones window, +builds a floor word for every window with an illegal centre, and checks the +explicit weight-2 witnesses. It does not call a SAT solver and it does not +search words that realize all fifteen weight-2 masks and the weight-6 mask. +""" + +import itertools +import math + +K = 6 +C = 5 +LENGTH = K * C +ALLOWED = (0, 1, C, C + 1, 2 * C) +MASK_BIT = {0: 0, 1: 1, 5: 0, 6: 1, 10: 0} +# (q_s, q_t, delta) for a coordinate whose sum is 1 or 6. +TYPES = { + 'A': (0, 1, 1), + 'B': (1, 5, 4), + 'C': (2, 4, 2), + 'D': (3, 3, 0), +} + +# Discovery of the two legal-centre words used a local CaDiCaL search. +# The checks below do not call that solver. +SORTED = '000001111122222333334444455555' +WEIGHT2_LEGAL = '001211112322203343354444555500' +WEIGHT6_LEGAL = '012300333300112241122545545544' +# Weight 6 at the repeated boundary (18, 18), plus 13 weight-2 masks. +JOINT = '102431540325045231253054314120' +# Same all-ones window as WEIGHT6_LEGAL, with an illegal centre. +WEIGHT6_TWIN = '012311222233334500001144445555' +JOINT_MISSING = ((0, 0, 1, 0, 1, 0), (0, 1, 0, 0, 0, 1)) + + +def fail(msg): + raise SystemExit('FAIL: ' + msg) + + +def prefixes(word): + counts = [0] * K + out = [tuple(counts)] + for letter in word: + counts[letter] += 1 + out.append(tuple(counts)) + return out + + +def mask_of(sum_vec): + bits = [] + for value in sum_vec: + bit = MASK_BIT.get(value) + if bit is None: + return None + bits.append(bit) + return tuple(bits) + + +def centre_sum(q16, letter): + return tuple(2 * q16[j] + (1 if j == letter else 0) for j in range(K)) + + +def legal_letters(q16): + if sum(q16) != 16: + return [] + letters = [] + for letter in range(K): + if q16[letter] >= C: + continue + if mask_of(centre_sum(q16, letter)) is not None: + letters.append(letter) + return letters + + +def expand(counts): + return [j for j in range(K) for _ in range(counts[j])] + + +def build_word(qs, delta, s, t, q16, letter): + """Schedule one all-ones window with a prescribed q_16 and centre letter.""" + qt = tuple(qs[j] + delta[j] for j in range(K)) + if t <= 16: + extras = tuple(q16[j] - qt[j] for j in range(K)) + rest = expand(tuple(5 - q16[j] for j in range(K))) + rest.remove(letter) + return expand(qs) + expand(delta) + expand(extras) + [letter] + rest + if s >= 16: + rest = expand(tuple(5 - qt[j] for j in range(K))) + if s > 16: + drop = expand(tuple(qs[j] - q16[j] for j in range(K))) + drop.remove(letter) + return expand(q16) + [letter] + drop + expand(delta) + rest + window = expand(delta) + window.remove(letter) + return expand(q16) + [letter] + window + rest + consumed = tuple(q16[j] - qs[j] for j in range(K)) + if t > 16: + remaining = expand(tuple(delta[j] - consumed[j] for j in range(K))) + remaining.remove(letter) + after = expand(tuple(5 - qt[j] for j in range(K))) + return expand(qs) + expand(consumed) + [letter] + remaining + after + after = expand(tuple(5 - q16[j] for j in range(K))) + after.remove(letter) + return expand(qs) + expand(consumed) + [letter] + after + + +def feasible_centres(qs, delta, s, t): + """Count vectors q_16 compatible with the window, and letters available at 16.""" + qt = tuple(qs[j] + delta[j] for j in range(K)) + found = {} + + def add(q16, available): + if sum(q16) != 16 or any(value < 0 or value > 5 for value in q16): + fail(f'feasible vector left the cube: {q16}') + found.setdefault(q16, set()).update(available) + + if t <= 16: + need = 16 - t + rooms = [5 - qt[j] for j in range(K)] + + def rec(i, left, acc): + if i == K - 1: + if 0 <= left <= rooms[i]: + acc[i] = left + q16 = tuple(qt[j] + acc[j] for j in range(K)) + add(q16, [j for j in range(K) if q16[j] < 5]) + return + for value in range(min(rooms[i], left) + 1): + acc[i] = value + rec(i + 1, left - value, acc) + + rec(0, need, [0] * K) + return found + if s >= 16: + need = s - 16 + + def rec(i, left, acc): + if i == K - 1: + if 0 <= left <= qs[i]: + acc[i] = qs[i] - left + q16 = tuple(acc) + if s > 16: + available = [j for j in range(K) if qs[j] - q16[j] > 0] + else: + available = [j for j in range(K) if delta[j] > 0] + add(q16, available) + return + for drop in range(min(qs[i], left) + 1): + acc[i] = qs[i] - drop + rec(i + 1, left - drop, acc) + + rec(0, need, [0] * K) + return found + need = 16 - s + + def rec(i, left, acc): + if i == K - 1: + if 0 <= left <= delta[i]: + acc[i] = left + consumed = tuple(acc) + q16 = tuple(qs[j] + consumed[j] for j in range(K)) + if t > 16: + available = [j for j in range(K) if delta[j] - consumed[j] > 0] + else: + available = [j for j in range(K) if q16[j] < 5] + add(q16, available) + return + for value in range(min(delta[i], left) + 1): + acc[i] = value + rec(i + 1, left - value, acc) + + rec(0, need, [0] * K) + return found + + +def extensions(options): + legal = [] + illegal = [] + for q16, available in options.items(): + good = [letter for letter in available if letter in legal_letters(q16)] + if good: + legal.append((q16, min(good))) + if not legal_letters(q16): + if available: + illegal.append((q16, min(available))) + else: + bad = [letter for letter in available if letter not in legal_letters(q16)] + if bad: + illegal.append((q16, min(bad))) + return legal, illegal + + +def weight_masks(word): + pref = prefixes(word) + found = set() + for s in range(LENGTH): + for t in range(s, LENGTH): + mask = mask_of(tuple(pref[s][j] + pref[t][j] for j in range(K))) + if mask is not None and sum(mask) in (2, 6): + found.add(mask) + return found + + +def main(): + # The four types are every pair of counts in 0..5 that sums to 1 or 6. + found_types = [] + for x in range(C + 1): + for y in range(x, C + 1): + if x + y in (1, 6): + found_types.append((x, y, y - x)) + expected_types = sorted(TYPES.values()) + if sorted(found_types) != expected_types: + fail(f'coordinate types changed: {found_types}') + + legal_pairs = [] + for counts in itertools.product(range(C + 1), repeat=K): + if sum(counts) != 16: + continue + for letter in legal_letters(counts): + legal_pairs.append((counts, letter)) + if len(legal_pairs) != 300: + fail(f'legal centre count changed: {len(legal_pairs)}') + if any(0 not in counts for counts, _letter in legal_pairs): + fail('a legal centre has no coordinate 0') + controls = 0 + + near = (3, 3, 3, 3, 3, 1) + if legal_letters(near): + fail('near-miss centre was accepted') + controls += 1 + + assignments = 0 + multinomial_total = 0 + class_early = 0 + class_cover = 0 + class_tight = 0 + illegal_only = 0 + both = 0 + legal_only = 0 + no_zero = 0 + zero_but_illegal = 0 + constructed = 0 + for counts in itertools.product(range(7), repeat=4): + if sum(counts) != K: + continue + n_a, n_b, n_c, n_d = counts + s = n_b + 2 * n_c + 3 * n_d + d = n_a + 4 * n_b + 2 * n_c + t = s + d + if not (0 <= s <= t <= LENGTH - 1) or s + t != 36 - 5 * n_a: + continue + ways = math.factorial(K) // ( + math.factorial(n_a) * math.factorial(n_b) + * math.factorial(n_c) * math.factorial(n_d) + ) + multinomial_total += ways + # Human no-zero classes. They are disjoint: a window counted here + # cannot place a coordinate 0 in q_16, for the reason in README.md. + if t <= 16: + class_early += ways + elif n_a == 0 and s <= 16 <= t: + class_cover += ways + elif n_a == n_b == 0 and (n_c, n_d) in ((1, 5), (0, 6)): + class_tight += ways + labels = ('A',) * n_a + ('B',) * n_b + ('C',) * n_c + ('D',) * n_d + for perm in set(itertools.permutations(labels)): + assignments += 1 + qs = tuple(TYPES[perm[j]][0] for j in range(K)) + delta = tuple(TYPES[perm[j]][2] for j in range(K)) + qt = tuple(qs[j] + delta[j] for j in range(K)) + if any(value > 5 for value in qt): + fail(f'type assignment exceeded 5: {perm}') + options = feasible_centres(qs, delta, s, t) + if not options: + fail(f'window has no q_16: s={s} t={t} {perm}') + if any(not available for available in options.values()): + fail(f'a feasible q_16 has no letter at position 16: s={s} t={t}') + legal_ext, illegal_ext = extensions(options) + human_no_zero = ( + t <= 16 + or (n_a == 0 and s <= 16 <= t) + or (n_a == n_b == 0 and (n_c, n_d) in ((1, 5), (0, 6))) + ) + enumeration_no_zero = all(0 not in q16 for q16 in options) + if human_no_zero != enumeration_no_zero: + fail(f'no-zero class disagreed with the vectors at s={s} t={t} {perm}') + if enumeration_no_zero: + no_zero += 1 + if legal_ext: + fail('a window with no zero coordinate was called legal') + if legal_ext and illegal_ext: + both += 1 + kind = 'both' + elif illegal_ext and not legal_ext: + illegal_only += 1 + kind = 'illegal' + if not enumeration_no_zero: + zero_but_illegal += 1 + elif legal_ext: + legal_only += 1 + kind = 'legal' + else: + fail(f'window has no placeable centre letter: s={s} t={t} {perm}') + for want_legal, choices in ((False, illegal_ext), (True, legal_ext)): + if not choices: + continue + q16, letter = min(choices) + word = build_word(qs, delta, s, t, q16, letter) + pref = prefixes(word) + if ( + len(word) != LENGTH + or any(word.count(source) != C for source in range(K)) + or pref[s] != qs + or pref[t] != qt + or pref[16] != q16 + or word[16] != letter + ): + fail(f'construction failed for s={s} t={t} {perm}') + summed = tuple(pref[s][j] + pref[t][j] for j in range(K)) + if summed != tuple(TYPES[perm[j]][0] + TYPES[perm[j]][1] for j in range(K)): + fail('all-ones sum drifted') + if any(value not in (1, 6) for value in summed): + fail(f'constructed window is not all-ones: {summed}') + legal = mask_of(centre_sum(q16, letter)) is not None + if legal != want_legal: + fail(f'polarity failed on a {kind} window') + constructed += 1 + + if assignments != 4095 or multinomial_total != 4095: + fail(f'assignment count changed: loop {assignments}, multinomial {multinomial_total}') + if (class_early, class_cover, class_tight) != (845, 721, 7): + fail(f'human no-zero classes changed: {class_early}, {class_cover}, {class_tight}') + if (illegal_only, both, legal_only, no_zero, zero_but_illegal, constructed) != ( + 2364, 1731, 0, 1573, 791, 5826 + ): + fail( + 'census counts changed: ' + f'illegal_only={illegal_only} both={both} legal_only={legal_only} ' + f'no_zero={no_zero} zero_but_illegal={zero_but_illegal} ' + f'constructed={constructed}' + ) + if no_zero != class_early + class_cover + class_tight: + fail('the enumeration and the human classes count different windows') + if illegal_only != no_zero + zero_but_illegal: + fail('illegal windows were not partitioned') + controls += 1 + + # Midpoint all-ones: q_18 is all threes, so q_16 cannot contain a zero. + midpoint_q = [] + for first in range(K): + for second in range(first, K): + q16 = [3] * K + q16[first] -= 1 + q16[second] -= 1 + midpoint_q.append(tuple(q16)) + if len(midpoint_q) != 21 or any(legal_letters(q16) for q16 in midpoint_q): + fail('midpoint all-ones no longer forces an illegal centre') + if any(min(q16) < 1 for q16 in midpoint_q): + fail('midpoint q_16 acquired a zero') + controls += 1 + + # Weight identity: sum 33 admits only weight 3 inside the allowed alphabet. + for values in itertools.product(ALLOWED, repeat=K): + weight = sum(MASK_BIT[value] for value in values) + if sum(values) % C != weight % C: + fail(f'weight identity failed on {values}') + if any(weight % C == 3 for weight in (0, 1, 2, 4, 5, 6)): + fail('another weight in 0..6 is congruent to 3') + controls += 1 + + def require_floor(text): + word = [int(ch) for ch in text] + if len(word) != LENGTH or any(word.count(source) != C for source in range(K)): + fail(f'witness is not a floor word: {text}') + return word + + # Sorted staircase: every pair of blocks realizes one weight-2 mask. + sorted_word = require_floor(SORTED) + sorted_pref = prefixes(sorted_word) + staircase = set() + for left in range(K): + for right in range(left + 1, K): + s = 5 * left + 1 + t = 5 * right + 1 + summed = tuple(sorted_pref[s][j] + sorted_pref[t][j] for j in range(K)) + mask = mask_of(summed) + if mask is None or sum(mask) != 2 or mask[left] != 1 or mask[right] != 1: + fail(f'staircase missed {(left, right)} at {(s, t)} sum {summed}') + staircase.add(mask) + if len(staircase) != 15: + fail(f'staircase realized {len(staircase)} masks') + sorted_centre = centre_sum(sorted_pref[16], sorted_word[16]) + if sorted_pref[16] != (5, 5, 5, 1, 0, 0) or sorted_centre != (10, 10, 10, 3, 0, 0): + fail(f'sorted centre changed: {sorted_pref[16]} {sorted_centre}') + if mask_of(sorted_centre) is not None: + fail('sorted centre became legal') + if weight_masks(sorted_word) != staircase: + fail('sorted word realizes a weight-2 or weight-6 mask outside the staircase') + controls += 1 + + swapped = sorted_word[:] + swapped[0], swapped[5] = swapped[5], swapped[0] + swapped_masks = weight_masks(swapped) + if len([mask for mask in swapped_masks if sum(mask) == 2]) >= 15: + fail('swapping the sorted word kept every weight-2 mask') + controls += 1 + + legal_word = require_floor(WEIGHT2_LEGAL) + legal_pref = prefixes(legal_word) + legal_found = weight_masks(legal_word) + if sum(1 for mask in legal_found if sum(mask) == 2) != 15: + fail('legal-centre weight-2 witness missed a mask') + if any(sum(mask) == 6 for mask in legal_found): + fail('legal-centre weight-2 witness realized weight 6') + legal_centre = centre_sum(legal_pref[16], legal_word[16]) + if legal_pref[16] != (3, 5, 5, 3, 0, 0) or legal_word[16] != 4: + fail(f'weight-2 legal prefixes changed: {legal_pref[16]} letter {legal_word[16]}') + legal_mask = mask_of(legal_centre) + if legal_centre != (6, 10, 10, 6, 1, 0) or legal_mask is None or sum(legal_mask) != 3: + fail(f'weight-2 legal centre changed: {legal_centre}') + controls += 1 + + weight6 = require_floor(WEIGHT6_LEGAL) + weight6_pref = prefixes(weight6) + pair = tuple(weight6_pref[4][j] + weight6_pref[22][j] for j in range(K)) + if pair != (6, 6, 6, 6, 1, 1) or any(value not in (1, 6) for value in pair): + fail(f'weight-6 legal window changed: {pair}') + weight6_centre = centre_sum(weight6_pref[16], weight6[16]) + if weight6_pref[16] != (5, 3, 3, 5, 0, 0) or weight6[16] != 4: + fail(f'weight-6 legal prefixes changed: {weight6_pref[16]}') + if weight6_centre != (10, 6, 6, 10, 1, 0) or mask_of(weight6_centre) is None: + fail(f'weight-6 legal centre changed: {weight6_centre}') + # Same window, opposite centre. Types are read off the witness prefixes. + qs = weight6_pref[4] + qt = weight6_pref[22] + delta = tuple(qt[j] - qs[j] for j in range(K)) + _legal_ext, illegal_ext = extensions(feasible_centres(qs, delta, 4, 22)) + if not illegal_ext: + fail('the exhibited flexible window has no illegal extension') + q16, letter = min(illegal_ext) + twin = build_word(qs, delta, 4, 22, q16, letter) + if ''.join(str(letter) for letter in twin) != WEIGHT6_TWIN: + fail('illegal twin of the flexible window changed') + twin_pref = prefixes(twin) + if twin_pref[4] != qs or twin_pref[22] != qt: + fail('illegal twin lost the flexible all-ones window') + if mask_of(centre_sum(twin_pref[16], twin[16])) is not None: + fail('illegal twin centre became legal') + controls += 1 + + joint = require_floor(JOINT) + joint_pref = prefixes(joint) + joint_pair = tuple(2 * joint_pref[18][j] for j in range(K)) + if joint_pref[18] != (3, 3, 3, 3, 3, 3) or joint_pair != (6, 6, 6, 6, 6, 6): + fail(f'joint witness is not all-ones at (18, 18): {joint_pref[18]}') + joint_centre = centre_sum(joint_pref[16], joint[16]) + if joint_centre != (6, 4, 6, 5, 6, 6) or mask_of(joint_centre) is not None: + fail(f'joint centre changed: {joint_centre}') + joint_found = weight_masks(joint) + missing = tuple(sorted( + mask for mask in itertools.product((0, 1), repeat=K) + if sum(mask) in (2, 6) and mask not in joint_found + )) + if missing != JOINT_MISSING: + fail(f'joint missing masks changed: {missing}') + if sum(1 for mask in joint_found if sum(mask) == 2) != 13: + fail('joint witness no longer realizes 13 weight-2 masks') + controls += 1 + + print( + 'PASS_C5_MASK_CENTRE_NONDETERMINATION ' + f'assignments=4095 illegal_only={illegal_only} both={both} ' + f'legal_only={legal_only} no_zero={no_zero} ' + f'zero_but_illegal={zero_but_illegal} ' + f'classes={class_early}+{class_cover}+{class_tight} ' + f'constructed={constructed} midpoint_q16=21 ' + f'weight2_polarities=2 weight6_forces_legal=0 ' + f'joint_weight2=13 joint_missing=2 controls={controls}' + ) + + +if __name__ == '__main__': + main()