From af3647d85d6f52956b1423ec8b22646f0deac196 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 08:05:59 +0000 Subject: [PATCH] feat(research): prove sharp c6 endpoint chain windows --- research/six-source-c6-chain-windows/PROOF.md | 183 ++++++++ .../six-source-c6-chain-windows/README.md | 154 +++++++ .../six-source-c6-chain-windows/SOURCES.json | 24 ++ .../six-source-c6-chain-windows/TASK.json | 108 +++++ .../six-source-c6-chain-windows/VERIFY.json | 36 ++ .../six-source-c6-chain-windows/verify.py | 394 ++++++++++++++++++ 6 files changed, 899 insertions(+) create mode 100644 research/six-source-c6-chain-windows/PROOF.md create mode 100644 research/six-source-c6-chain-windows/README.md create mode 100644 research/six-source-c6-chain-windows/SOURCES.json create mode 100644 research/six-source-c6-chain-windows/TASK.json create mode 100644 research/six-source-c6-chain-windows/VERIFY.json create mode 100644 research/six-source-c6-chain-windows/verify.py diff --git a/research/six-source-c6-chain-windows/PROOF.md b/research/six-source-c6-chain-windows/PROOF.md new file mode 100644 index 0000000000..e5829cba99 --- /dev/null +++ b/research/six-source-c6-chain-windows/PROOF.md @@ -0,0 +1,183 @@ +# Chain windows on the c=6 diagonal: proofs + +Scoped written proofs for a fixed finite model, with an exhaustive finite +certificate in `verify.py`. This is not a statement about the unrestricted +six-source depth-two exclusion at characteristic 6, which remains the solver +verdict of PR6141. + +## 0. Setting (cited, not re-proved) + +The interface is the one restated in the merged package +`research/six-source-c6-centre-classification` (pinned in `SOURCES.json`), +which credits Nick Petalas's PR4231, PR4248 and PR6107. + +A **floor word** is a word `w_0 ... w_35` on the sources `0,...,5` calling each +source exactly six times. `q_t` counts the letters among `w_0 ... w_{t-1}`, so +`q_36 = (6,...,6)`. For `4 <= s <= 18` write + +```text +S(s) = q_s + q_{39-s}, 0 <= S(s)_j <= 12, sum_j S(s)_j = 39. +``` + +`S(s)` is **weight-3** when every coordinate lies in `{0,1,6,7,12}` and exactly +three coordinates lie in `{1,7}`. (An integer in `0..12` is congruent to 0 or 1 +modulo 6 exactly for those five values.) A **chain on `[s0,18]`**, for +`4 <= s0 <= 18`, is a floor word whose `S(s)` is weight-3 for every +`s0 <= s <= 18`. Its **family** is the sorted multiset `S(18)`. The weight-3 +condition at the pair `(0,9)` is the same condition on `q_0 + q_9 = q_9`. +Only the endpoint family is fixed: intermediate multisets may differ from it. +The longest window of a constant-multiset chain is a separate question. + +The step identity (also used in open PR #7099) follows from `q_{s+1} = q_s + e_{w_s}` +and `q_{38-s} = q_{39-s} - e_{w_{38-s}}`: + +```text +S(s+1) = S(s) + e_{w_s} - e_{w_{38-s}}. (0) +``` + +Call coordinate `j` **low** at `s` if `S(s)_j <= 1` (base 0), **base 6** if +`S(s)_j in {6,7}`, and **high** if `S(s)_j = 12`. Write `L(s)` for the number +of low coordinates. + +## 1. Lemma A: bases are frozen along a chain + +*If `S(s)` and `S(s+1)` are both weight-3, every coordinate keeps its base.* + +By (0) each coordinate changes by `-1`, `0` or `+1`. Inside `{0,1,6,7,12}` the +only unit steps are `0 <-> 1` and `6 <-> 7`. The values `1,6,7,12` have the +neighbours `2,5,8,11,13` outside the set, so no unit step joins two bases. Hence +the vector of bases `6*floor(S_j/6)` is constant on a chain, and so are the +numbers of low, base-6 and high coordinates. `verify.py` also checks the lemma +on all 644,820 legal steps between weight-3 states with `4 <= s <= 17`. + +## 2. Lemma B: as many highs as lows + +*A weight-3 `S(s)` has exactly `L(s)` high coordinates.* + +The coordinate sum is 39 and exactly three coordinates are `1 mod 6`, so the +bases sum to 36. Let `n0, n6, n12` count the coordinates of each base. Then +`n0 + n6 + n12 = 6` and `6 n6 + 12 n12 = 36`, so `n6 + 2 n12 = 6` and +`n12 = n0`. + +## 3. Lemma C: a counting bound + +*If `S(s)` is weight-3 with `L` low coordinates, then `5L <= s - 3` and `6L <= s`.* + +A low coordinate `j` has `q_{39-s}[j] <= S(s)_j <= 1`, so at most one of the six +copies of `j` lies in the first `39-s` letters. At least five lie in the last +`s-3` letters, positions `39-s,...,35`. Distinct low coordinates are distinct +letters, so `5L <= s - 3`. A high coordinate has `S_j = 12`, hence +`q_s[j] = 6` and all six of its copies lie in the first `s` letters. By +Lemma B there are `L` highs, so `6L <= s`. (The second bound is no stronger than +the first for `L <= 3`, the only possible values since `L + L <= 6`.) + +## 4. Theorem 1: the window of each family + +*Let `F` be one of the six families at `(18,21)` and let `L` be its number of +low coordinates (entries `0` or `1`). For `4 <= s0 <= 18` a chain on `[s0,18]` +with family `F` exists if and only if `s0 >= max(4, 3 + 5L)`.* + +| family `F` | `L` | least `s0` | +| --- | ---: | ---: | +| `(6,6,6,7,7,7)` | 0 | 4 | +| `(0,6,7,7,7,12)`, `(1,6,6,7,7,12)` | 1 | 8 | +| `(0,1,7,7,12,12)`, `(1,1,6,7,12,12)` | 2 | 13 | +| `(1,1,1,12,12,12)` | 3 | 18 | + +*Only if.* The family at `s = 18` has `L` lows. By Lemma A, `S(s0)` has `L` lows +as well. Lemma C at `s = s0` gives `s0 >= 3 + 5L`. + +*If.* The README lists one floor word per family. Each is a chain on +`[max(4,3+5L), 18]` with the stated family, checked literally by +`verify.py` from the word alone. Restricting a chain to `[s0,18]` with a larger +`s0` leaves a chain. + +The finite certificate is independent of the argument above. The 77,220 +weight-3 states `(q_s, q_{39-s})`, `4 <= s <= 18`, are enumerated exhaustively +(counts `120, 420, 1060, 2100, 3600, 5520, 7740, 9900, 11220, 11280, 9780, +7240, 4500, 2040, 700` for `s = 4,...,18`). The least `s` at which a state with +`L = 0,1,2,3` lows occurs is `4, 8, 13, 18`. A layered search from the 700 end +states at `s = 18` and a second, forward search from the start states agree on +every count in the next section. + +Here is why this state graph captures words exactly. A state at index `s` +is any pair `(q,t)` with coordinatewise `0 <= q <= t <= 6`, sums `s` and +`39-s`, and weight-3 sum `q+t`. It is realizable by concatenating blocks with +letter multiplicities `q`, `t-q` and `6-t`. An edge to index `s+1` adds one +letter to `q` and removes one from `t`, recording the letters at positions +`s` and `38-s`. For a whole path, these positions are disjoint. Fill the +first `s0` positions with its initial `q`, the three positions `18,19,20` +with its final `t-q`, and the last `s0-3` positions with `6-t` from its +initial state. All multiplicities are nonnegative and their sums match the +available positions. This constructs a floor word for every graph path. +Conversely, taking these prefixes of any word gives precisely such a path. +Thus graph reachability is equivalent to existence of a word, rather than +only a necessary relaxation. + +## 5. Corollary: the T2 question of PR #7099 has no solution on `s = 4,...,18` + +Open PR #7099 asks which endpoint pairs of the multiset `(0,6,7,7,7,12)` are +joined by a monotone chain on `s = 4,...,18`. + +*Answer: none, and the same holds for all five families other than +`(6,6,6,7,7,7)`.* A chain on `[4,18]` has `L = 0` by Lemma C at `s = 4`, since +`5L <= 1`. Directly: `S(4) = q_4 + (6,...,6) - e_{w_35}` has every coordinate in +`5..10`, and only 6 and 7 are allowed there. By Lemma A every `S(s)` stays in +`{6,7}^6`, so the family is `(6,6,6,7,7,7)`. The question as posed has the empty +answer, because the multiset cannot occur at `s = 4`. + +The nonvacuous version asks about the longest window of the family. Take the +start state `(q_{s0}, q_{39-s0})` and the end state `(q_18, q_21)` as the +endpoint pair, which for `(6,6,6,7,7,7)` and `s0 = 4` is the pair +`(M_4, D, M_18)` of PR #7099. A pair is **joined** if some chain on `[s0,18]` +passes through both. At the least window start of each family: + +| family | `s0` | start states | end states | joined pairs | +| --- | ---: | ---: | ---: | ---: | +| `(6,6,6,7,7,7)` | 4 | 120 | 20 | 2400 | +| `(0,6,7,7,7,12)` | 8 | 180 | 120 | 720 | +| `(1,6,6,7,7,12)` | 8 | 180 | 180 | 1080 | +| `(0,1,7,7,12,12)` | 13 | 180 | 180 | 360 | +| `(1,1,6,7,12,12)` | 13 | 180 | 180 | 360 | +| `(1,1,1,12,12,12)` | 18 | 20 | 20 | 20 | + +So on its longest window `[8,18]` the T2 relation joins 720 of the 21,600 pairs. +The counts for `(6,6,6,7,7,7)` and the sizes of +the six end families (20, 120, 180, 180, 180, 20; 700 in all) agree with the +numbers reported in open PRs #7099 and #7029. They are by-products of this +computation, not a replay of those packages. The other joined-pair counts have +no closed form here. + +## 6. Theorem 2: how far down the (0,9) hypothesis needs the chain + +*For `4 <= s0 <= 18` there is a floor word that is weight-3 at `(0,9)` and at +every `s` in `[s0,18]` if and only if `s0 >= 8`.* + +A weight-3 `q_9` has entries in `{0,1,6}` (7 exceeds the cap), three entries +equal to 1 and coordinate sum 9, so the other three entries sum to 6 from +`{0,6}`. Hence `q_9` is a permutation of `(1,1,1,6,0,0)`; there are 60 of them. + +*Only if.* Let `s0 <= 9`, so that `s = 9` lies in the chain. The coordinate `f` +with `q_9[f] = 6` has `q_30[f] >= q_9[f] = 6`, so `S(9)_f = 12` and `f` is high. +Then `L >= 1` by Lemma B, and Lemma A with Lemma C at `s0` give +`s0 >= 3 + 5 = 8`. + +*If.* The word `345555552443322111234111223344000000` is a floor word with +`q_9 = (0,0,1,1,1,6)`, weight-3 at `(0,9)`, and weight-3 at every `s` in +`[8,18]`; its family is `(0,6,7,7,7,12)`. It also serves every larger `s0`. + +The consequence is for the conditional exclusion stated in open PR #7029 +(no floor word is weight-3 at `(0,9)` and at every `s = 4,...,18`). Its +chain hypothesis is needed only from `s = 7`: the pair of hypotheses +`(0,9)` and `[7,18]` is already contradictory, while `(0,9)` and `[8,18]` are +jointly satisfiable. The exclusion in #7029 is cited and not replayed; this +theorem is proved from the definitions above. + +## 7. What is and is not established + +Established, in the stated model: Lemmas A to C; Theorem 1; the empty answer of +Section 5 and its joined-pair counts; Theorem 2. The witnesses are checked for +weight-3 at the listed pairs; no claim is made that any of them realizes any other mask +of the depth-two interface. The characteristic-6 six-source depth-two exclusion, +other characteristics and source counts, and every pair other than +`(s,39-s)` for `4 <= s <= 18` and `(0,9)` are outside this result. diff --git a/research/six-source-c6-chain-windows/README.md b/research/six-source-c6-chain-windows/README.md new file mode 100644 index 0000000000..08d7fe8ba7 --- /dev/null +++ b/research/six-source-c6-chain-windows/README.md @@ -0,0 +1,154 @@ +# Chain windows for the six c=6 separation-3 families + +**Scoped written proof with an exact finite certificate. No new κ, supplier or +frontier change.** In the unchanged unsigned dirty connector at six sources and +characteristic 6, a floor word is weight-3 on the diagonal `s + t = 39` at `s` +when `S(s) = q_s + q_{39-s}` has every coordinate in `{0,1,6,7,12}` and exactly +three in `{1,7}`. This package answers the open question of unpaidmoon's open +[PR #7099](https://github.com/CrocSwap/integer-mult-bounds/pull/7099): which +endpoint pairs of the type-T2 multiset `(0,6,7,7,7,12)` are joined by a monotone +chain on `s = 4,...,18`. + +**Answer: none.** A chain that reaches `s = 4` has `S(4)` in `{6,7}^6`, and every +step between weight-3 states keeps each coordinate in its block `{0,1}`, +`{6,7}` or `{12}`. So every chain on `[4,18]` has the multiset +`(6,6,6,7,7,7)`, and no other family of the six at `(18,21)` occurs there. +Each other family has a longest window `[s0,18]` and the start is exactly +`s0 = 3 + 5L`, where `L` is its number of entries `0` or `1`: + +Here a family's window fixes the multiset at `(18,21)`. Earlier indices need +only be weight-3; their multisets may differ. The window table therefore +concerns endpoint families. It does not determine the longest windows on which +a specified multiset stays constant at every index. + +| family at `(18,21)` | `L` | least `s0` | start states | end states | joined pairs | +| --- | ---: | ---: | ---: | ---: | ---: | +| `(6,6,6,7,7,7)` | 0 | 4 | 120 | 20 | 2400 | +| `(0,6,7,7,7,12)` (T2) | 1 | 8 | 180 | 120 | 720 | +| `(1,6,6,7,7,12)` | 1 | 8 | 180 | 180 | 1080 | +| `(0,1,7,7,12,12)` | 2 | 13 | 180 | 180 | 360 | +| `(1,1,6,7,12,12)` | 2 | 13 | 180 | 180 | 360 | +| `(1,1,1,12,12,12)` | 3 | 18 | 20 | 20 | 20 | + +A start state is `(q_{s0}, q_{39-s0})`, an end state is `(q_18, q_21)`, and a pair +is joined when one weight-3 chain passes through both. On its longest window +`[8,18]` the T2 relation joins 720 of 21,600 pairs. The proof is two lemmas and a +counting bound: bases are frozen along a chain, a family with `L` entries at most +1 also has `L` entries equal to 12, and each low source keeps at least five of +its six copies in the last `s - 3` letters. [Proofs](PROOF.md) + +## How far down the (0,9) hypothesis needs the chain + +Open [PR #7029](https://github.com/CrocSwap/integer-mult-bounds/pull/7029) states +a conditional exclusion: no floor word is weight-3 at the pair `(0,9)` and at +every `s = 4,...,18`. The same two lemmas give an exact threshold. A floor word +that is weight-3 at `(0,9)` and on `[s0,18]` exists if and only if `s0 >= 8`. +Weight-3 at `(0,9)` forces `q_9` to be a permutation of `(1,1,1,6,0,0)`, whose +6-coordinate is high at `s = 9`, so a chain through `s = 9` needs `L >= 1` and +hence `s0 >= 8`. This package proves that from the definitions; #7029's own proof +is not replayed. So the chain hypothesis is needed only from `s = 7`, and +`(0,9)` together with `[8,18]` is satisfiable. + +## Witness words + +Each word is a floor word and weight-3 on its window; the five words with `L >= 1` +fail at `s0 - 1`. `verify.py` checks each from the string alone. + +| family | window | word | +| --- | --- | --- | +| `(6,6,6,7,7,7)` | `[4,18]` | `345554433222111000345000111222334455` | +| `(0,6,7,7,7,12)` | `[8,18]` | `345555554433222111234111220334400000` | +| `(1,6,6,7,7,12)` | `[8,18]` | `345555554433222111034111222334400000` | +| `(0,1,7,7,12,12)` | `[13,18]` | `344444455555533222123220330000011111` | +| `(1,1,6,7,12,12)` | `[13,18]` | `344444455555533222013222330000011111` | +| `(1,1,1,12,12,12)` | `[18,18]` | `333333444444555555012000001111122222` | + +The word `345555552443322111234111223344000000` is weight-3 at `(0,9)` and on +`[8,18]`; its family is `(0,6,7,7,7,12)`. The last window word above is the +separation-3 word printed in the merged centre-classification package. +None of these words is claimed to realize any other mask of the depth-two +interface. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/six-source-c6-chain-windows/verify.py +python3.12 -I -O -W error -B research/six-source-c6-chain-windows/verify.py +python3.12 -B scripts/research_package.py --package research/six-source-c6-chain-windows +``` + +Expected marker: + +```text +PASS_SIX_SOURCE_C6_CHAIN_WINDOWS states=77220 steps=644820 first=[(0, 4), (1, 8), (2, 13), (3, 18)] joined=[360, 720, 20, 360, 1080, 2400] forward=6 starts09=[0, 0, 0, 0, 180, 480] witnesses=7 controls=7 inputs=1 +``` + +`verify.py` enumerates all 77,220 weight-3 diagonal states with `4 <= s <= 18` and +checks the frozen-base lemma on all 644,820 legal steps between them. It counts +joined pairs by a backward search and by a second forward search that agree, and +it reproduces the least window start for each family. It then re-derives the +60 weight-3 shapes at `(0,9)`, finds the empty start sets for `s0 <= 7` and the +nonempty ones at 8 and 9, and checks the stored words literally. Seven controls +accept the cited words of #7099 and the centre package, and reject a 35-letter +word, a seventh copy of a letter, and a word without a weight-3 `(0,9)`. +`verify.py --print-witnesses` regenerates the stored words; they must match. + +## Verifier limits + +All search bounds are fixed in `verify.py`. Each state has six coordinates, +each layer tests at most 36 next-letter pairs per state, and each reachability +mask has at most 700 bits. Partial coordinate enumeration has at most `10^6` +entries. The graph has 15 layers, 77,220 states and 644,820 edges. Every function +is below 60 lines, and scientific checks raise even with optimized Python. +The registered commands enable warnings as errors. No solver or child process +is started. + +Power-of-Ten rule 3 has a managed-runtime deviation in `verify.py`: Python +allocates tuples, dictionaries and integer masks during enumeration. The fixed +domains above bound live collections; replacing those containers with fixed +storage would require a different runtime. Normal and optimized registered +runs exercise the complete domains. A port to a runtime with controllable +allocation should preallocate these capacities before enumeration. + +## Scope and limits + +The model is fixed: six sources, characteristic 6, floor words of length 36, the +pairs `(s, 39-s)` for `4 <= s <= 18` and the early pair `(0,9)`. The interface is +cited from the merged `six-source-c6-centre-classification` package and pinned in +[SOURCES.json](SOURCES.json); nothing in it is re-proved. The unrestricted +depth-two exclusion at c=6 stays the solver verdict of PR6141. The joined-pair +counts other than the T1 row are census values with no closed form. Independent +human and proof-kernel review are unclaimed. Hosted CI is separate from the +local runs. + +## Open next questions + +1. Which further weight-3 pairs `(s,t)` with `s + t = 3 mod 6`, for example + `(0,3)`, can hold together with `(0,9)` and a window `[8,18]`? *Why:* the pair + `(0,9)` with `[8,18]` is satisfiable, so excluding words on that shorter + window needs further pairs. *First step:* take the 180 start states at `s = 8` and add + one pair that constrains only the prefix counts, with the prefix arrangement as + extra state. *Blocked by:* the diagonal state does not record the order inside + the first `s0` letters, which this package fixes in ascending order. +2. Does `s0 >= 3 + (c-1) L` hold at other characteristics and source counts? *Why:* + the lemmas use only the allowed set `{0,1,c,c+1,2c}` and the suffix length. + *First step:* rerun `verify.py` with the constants changed to the c=7 diagonal + `s + t = 45` and compare the first-appearance table with `3 + 6L`. *Blocked by:* + the constants are hard-coded for c=6; the c=7 existence question belongs to + another contributor's claim and is not addressed. + +The structured copies are in [TASK.json](TASK.json). + +## Credit + +The window theorem, the `(0,9)` threshold and the verifier were produced by Nick +Petalas. unpaidmoon's [PR #7099](https://github.com/CrocSwap/integer-mult-bounds/pull/7099) +poses the T2 question and the endpoint-pair terminology, and supplies the cited T1 +control word; neighbours [#7029](https://github.com/CrocSwap/integer-mult-bounds/pull/7029) +and [#7042](https://github.com/CrocSwap/integer-mult-bounds/pull/7042) supply the +six-family census and the T1 chains. The interface is restated in unpaidmoon's +merged `six-source-c6-centre-classification` package, which credits Nick Petalas's +PR4231, PR4248 and PR6107, the Ross Richardson PR934/PR943 lineage and +JosieElliston's PR6141. No predecessor credit is changed. Apache-2.0. diff --git a/research/six-source-c6-chain-windows/SOURCES.json b/research/six-source-c6-chain-windows/SOURCES.json new file mode 100644 index 0000000000..ef9ddc2171 --- /dev/null +++ b/research/six-source-c6-chain-windows/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/six-source-c6-centre-classification/README.md", + "usage": "input", + "git_blob": "3e6b3c225c15b081f2b66dd16c97118e3b8c494b", + "sha256": "0d86c0d2524036b1fe36bc4217a935b97160f8155b810bb0010a3130d97f3dcf" + } + ] +} diff --git a/research/six-source-c6-chain-windows/TASK.json b/research/six-source-c6-chain-windows/TASK.json new file mode 100644 index 0000000000..9263fb1a15 --- /dev/null +++ b/research/six-source-c6-chain-windows/TASK.json @@ -0,0 +1,108 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Answer the open question of open PR #7099 on type T2 of the six-source c=6 diagonal s+t=39: which endpoint pairs are joined by a monotone chain on s=4..18. Determine exactly, for each of the six separation-3 families at (18,21), the windows [s0,18] on which a floor word with weight-3 at every s realizes it, with explicit words, and the least start index for which weight-3 at (0,9) and on [s0,18] can hold together.", + "scope_change_reason": "The card asks for one new connector operation. This package keeps the published alphabet and the interface of #4231/#4248 unchanged and answers an open question of unpaidmoon's open #7099 about the six-source c=6 diagonal chain, as that package and its neighbours #7029 and #7042 do. A new operation is not the missing step.", + "bottleneck_link": "Side result on the connector-alphabet interface schedule at six sources and characteristic 6: it shows which hypotheses of a conditional diagonal argument carry the weight. It supplies no supplier, consumer, selected-record change or kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact window theorem with the T2 answer and the (0,9) threshold; leave every other pair, source count and characteristic open.", + "outcome": "completed", + "evidence": "PROOF.md (frozen-base and balance lemmas, the counting bound, the window theorem, the T2 corollary, graph-to-word equivalence and the (0,9) threshold) and verify.py: exhaustive census of 77,220 weight-3 diagonal states with 4<=s<=18, backward and forward joined-pair counts, seven literal witness words and cited controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which further weight-3 pairs (s,t) with s+t = 3 mod 6, for example (0,3), can hold together with weight-3 at (0,9) and on a window [8,18]?", + "why_it_matters": "Weight-3 at (0,9) with s0 = 8 is satisfiable, so these two hypotheses alone do not exclude words on [8,18]; further pairs are needed to obstruct them.", + "first_step": "Take the 180 start states at s = 8 of the (0,9) witness class and add one early or off-diagonal pair that constrains only the prefix counts, then re-run the layered search with the prefix arrangement as extra state.", + "blocked_by": "Pairs inside the first s0 letters constrain the order of that prefix, which the diagonal state does not record; this package fixes the prefix in ascending order." + }, + { + "question": "Does the window bound s0 >= 3 + (c-1) L hold at other characteristics and source counts, with the same frozen-base lemma?", + "why_it_matters": "The lemma and the counting bound use only the allowed set {0,1,c,c+1,2c} and the suffix length, so they may transfer to the c = 7 diagonal and to five- or seven-source blocks.", + "first_step": "Re-run verify.py with C, K, LENGTH, PAIR_SUM, TOP changed to the c = 7 diagonal s+t = 45 and compare the first-appearance table with 3 + 6L.", + "blocked_by": "The constants and the allowed set are hard-coded for c = 6 here; the c = 7 existence question is a separate claim by another contributor and is not addressed." + } + ], + "claim_type": "scoped written mathematical proof with exact finite certificate", + "predecessor": { + "pr": 7099, + "author": "unpaidmoon", + "head": "123e6808f2d1381e5ab07d128e69c52a98ef0a1a", + "question": "README Open next questions 1 (type T2)", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/7099", + "role": "Source of the T2 question, the endpoint-pair terminology and the cited T1 control word; cited and restated, not audited or replayed." + }, + "coordination_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19529842", + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library only" + }, + "overlap": { + "checked_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "open_prs": { + "fetched_at": "2026-11-11T07:54:25Z", + "records": 466, + "complete_pagination": true + }, + "targeted_merged_searches": [ + "0,6,7,7,7,12", + "six-source c6 monotone chain", + "separation-3 T2 chain", + "c6 floor word diagonal weight-3 window", + "six-source separation-3 families" + ], + "live_handoff": "Latest 30 comments of #1166 read on 2026-11-11; refreshed paginated Discussion snapshot contains 7,089 records. No competing claim on this target found within that coverage.", + "limits": "Non-atomic open-PR and Discussion snapshots; sparse working-tree note coverage. No diff-level or unpublished-work completeness claim.", + "local_note_coverage": { + "searched_records": 178, + "head_records": 10178, + "complete_head_inventory": false, + "compensation": "Targeted git grep over origin/main research READMEs, plus merged-PR searches for the exact T2 multiset, monotone chains and floor words, including general-characteristic results." + } + }, + "coordination_progress": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19537481", + "scope_addition_to_claim": "The CLAIM explicitly excluded the (0,9) hypothesis. The progress update records the additional exact coexistence threshold obtained from the same counting bound and one literal witness.", + "window_convention": "The family is the multiset at (18,21). Earlier diagonal sums need only be weight-3 and may have different multisets. Constant-multiset windows are not classified." +} diff --git a/research/six-source-c6-chain-windows/VERIFY.json b/research/six-source-c6-chain-windows/VERIFY.json new file mode 100644 index 0000000000..e8c2cb4653 --- /dev/null +++ b/research/six-source-c6-chain-windows/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/six-source-c6-centre-classification/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 400, + "checks": "Exhaustive weight-3 diagonal census, frozen-base lemma on every legal step, backward and forward joined-pair counts, window starts, (0,9) threshold, literal witness words and cited controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 400, + "checks": "The same gates under optimized Python; every gate raises SystemExit, none uses assert." + } + ] +} diff --git a/research/six-source-c6-chain-windows/verify.py b/research/six-source-c6-chain-windows/verify.py new file mode 100644 index 0000000000..3d2df0fdf7 --- /dev/null +++ b/research/six-source-c6-chain-windows/verify.py @@ -0,0 +1,394 @@ +#!/usr/bin/env python3 +"""Exact chain windows for the c=6 six-source diagonal s + t = 39. + +Standard library only. Every scientific gate raises SystemExit, so running +with -O cannot silence a failure. Loop bounds: every loop ranges over a +constant-size range or over a finite set built from constants. The census has +77,220 weight-3 states with 4 <= s <= 18; partial coordinate enumeration has +at most 10**6 entries because column_options() has ten choices. No recursion. + +Interface (cited, not re-proved): the merged package +research/six-source-c6-centre-classification defines floor words on k = 6 +sources at c = 6, the prefix counts q_t, and the weight-3 mask condition. +Usage: verify.py [--print-witnesses] +""" + +import hashlib +import itertools +import json +import sys +from pathlib import Path + +C = 6 +K = 6 +LENGTH = 36 +PAIR_SUM = 39 +TOP = 18 +LOW = 4 +MID = 9 +ALLOWED = (0, 1, 6, 7, 12) +PKG = Path(__file__).resolve().parent +ROOT = PKG.parents[1] + +# Cited words. CONTROL_T1 is printed in open PR #7099; the two CENTRE words +# are printed in the merged centre-classification README. +CONTROL_T1 = "012334500112234455345554432211002103" +CENTRE_SEP3 = "333333444444555555012000001111122222" +CENTRE_09 = "333333012000001111122222444444555555" + +# Witnesses generated by witness_words() and re-checked literally from the +# strings alone. Key: sorted S(18). Value: (first window index s0, word). +WITNESS = { + (0, 1, 7, 7, 12, 12): (13, '344444455555533222123220330000011111'), + (0, 6, 7, 7, 7, 12): (8, '345555554433222111234111220334400000'), + (1, 1, 1, 12, 12, 12): (18, '333333444444555555012000001111122222'), + (1, 1, 6, 7, 12, 12): (13, '344444455555533222013222330000011111'), + (1, 6, 6, 7, 7, 12): (8, '345555554433222111034111222334400000'), + (6, 6, 6, 7, 7, 7): (4, '345554433222111000345000111222334455'), +} +# Word with weight-3 at (0,9) and at every s in [8, 18]. +WITNESS_09 = '345555552443322111234111223344000000' + + +def require(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +def weight3(sv): + """Weight-3 mask: all entries in {0,1,6,7,12}, exactly three in {1,7}.""" + return all(x in ALLOWED for x in sv) and sum(1 for x in sv if x % C == 1) == 3 + + +def column_options(): + """(q_j, t_j) pairs with q <= t <= 6 and q + t in ALLOWED.""" + return [(q, t) for t in range(C + 1) for q in range(t + 1) if q + t in ALLOWED] + + +def static_states(s): + """All weight-3 diagonal states (q_s, q_{39-s}) with q_s <= q_{39-s} <= 6.""" + opts = column_options() + parts = [((), 0, 0, 0)] + for _ in range(K): + grown = [] + for cols, sq, st, ones in parts: + for q, t in opts: + nsq, nst = sq + q, st + t + nones = ones + ((q + t) % C == 1) + if nsq <= s and nst <= PAIR_SUM - s and nones <= 3: + grown.append((cols + ((q, t),), nsq, nst, nones)) + parts = grown + out = [] + for cols, sq, st, ones in parts: + if sq == s and st == PAIR_SUM - s and ones == 3: + out.append((tuple(c[0] for c in cols), tuple(c[1] for c in cols))) + return sorted(out) + + +def diag_sum(state): + return tuple(a + b for a, b in zip(state[0], state[1])) + + +def lows(state): + return sum(1 for x in diag_sum(state) if x <= 1) + + +def highs(state): + return sum(1 for x in diag_sum(state) if x == 12) + + +def base_vector(state): + return tuple(C * (x // C) for x in diag_sum(state)) + + +def successors(state, next_layer): + """States at s+1 reached by early letter w_s = a and late letter w_{38-s} = b.""" + q, t = state + found = [] + for a in range(K): + qa = q[:a] + (q[a] + 1,) + q[a + 1:] + for b in range(K): + if t[b] == 0: + continue + tb = t[:b] + (t[b] - 1,) + t[b + 1:] + if (qa, tb) in next_layer: + found.append((qa, tb)) + return sorted(found) + + +def build_layers(): + return {s: static_states(s) for s in range(LOW, TOP + 1)} + + +def build_successors(layers): + sets = {s: set(v) for s, v in layers.items()} + return {s: {x: successors(x, sets[s + 1]) for x in layers[s]} for s in range(LOW, TOP)} + + +def reach_masks(layers, succ, require_09=False): + """reach[s][x]: bit i set iff top state i is joined to x by weight-3 steps. + + With require_09, states at s = 9 whose q_9 is not weight-3 reach nothing. + """ + top_index = {x: i for i, x in enumerate(layers[TOP])} + reach = {TOP: {x: 1 << i for x, i in top_index.items()}} + for s in range(TOP - 1, LOW - 1, -1): + layer = {} + for x in layers[s]: + mask = 0 + for y in succ[s][x]: + mask |= reach[s + 1][y] + if require_09 and s == MID and not weight3(x[0]): + mask = 0 + layer[x] = mask + reach[s] = layer + return reach, top_index + + +def check_lemma_a(layers, succ): + """Every legal step between weight-3 states keeps all bases 6*floor(S/6).""" + steps = 0 + for s in range(LOW, TOP): + for x in layers[s]: + for y in succ[s][x]: + require(base_vector(x) == base_vector(y), "base changed at s=%d" % s) + steps += 1 + return steps + + +def check_static_bound(layers): + """5*lows <= s-3, highs == lows, and the first s carrying L lows is 3+5L.""" + first = {} + for s in range(LOW, TOP + 1): + for x in layers[s]: + low = lows(x) + require(highs(x) == low, "highs != lows at s=%d" % s) + require(C * low <= s and 5 * low <= s - 3, "bound violated at s=%d" % s) + first[low] = min(first.get(low, s), s) + require(first == {0: 4, 1: 8, 2: 13, 3: 18}, "first appearance %r" % (first,)) + return first + + +def popcount(n): + return bin(n).count("1") + + +def family_masks(layers, top_index): + groups = {} + for x in layers[TOP]: + groups.setdefault(tuple(sorted(diag_sum(x))), []).append(top_index[x]) + masks = {f: sum(1 << i for i in idx) for f, idx in groups.items()} + return masks, {f: len(idx) for f, idx in groups.items()} + + +def window_table(layers, reach, masks): + """Per family: lows, first window start, start/end/joined counts there.""" + table = {} + for fam, mask in sorted(masks.items()): + low = sum(1 for v in fam if v <= 1) + per_s0 = {} + for s0 in range(LOW, TOP + 1): + joined = sum(popcount(reach[s0][x] & mask) for x in layers[s0]) + starts = sum(1 for x in layers[s0] if reach[s0][x] & mask) + per_s0[s0] = (starts, joined) + first = min(s for s, v in per_s0.items() if v[1] > 0) + require(first == max(LOW, 3 + 5 * low), "window start %r %d" % (fam, first)) + require(all(per_s0[s][1] == 0 for s in range(LOW, first)), "gap %r" % (fam,)) + require(all(per_s0[s][1] > 0 for s in range(first, TOP + 1)), "hole %r" % (fam,)) + table[fam] = (low, first, per_s0[first][0], popcount(mask), per_s0[first][1]) + return table + + +def forward_joined(layers, succ, s0, top_index): + """Second method: forward closure from each start; end-index sets per start.""" + result = {} + for x in layers[s0]: + frontier = {x} + for s in range(s0, TOP): + frontier = {y for z in frontier for y in succ[s][z]} + result[x] = {top_index[y] for y in frontier} + return result + + +def check_forward(layers, succ, top_index, masks, table): + """The forward closure reproduces every joined-pair count at the first window.""" + for fam, row in table.items(): + s0 = row[1] + ends = forward_joined(layers, succ, s0, top_index) + bits = {i for i in range(len(layers[TOP])) if masks[fam] >> i & 1} + joined = sum(len(e & bits) for e in ends.values()) + starts = sum(1 for e in ends.values() if e & bits) + require((starts, joined) == (row[2], row[4]), "forward mismatch %r" % (fam,)) + return len(table) + + +def pick_chain(layers, succ, reach, s0, mask): + """Lexicographically first chain of states from s0 to s = 18 inside `mask`.""" + starts = [x for x in layers[s0] if reach[s0][x] & mask] + require(bool(starts), "no start state at s0=%d" % s0) + chain = [starts[0]] + for s in range(s0, TOP): + nxt = [y for y in succ[s][chain[-1]] if reach[s + 1][y] & mask] + require(bool(nxt), "chain stuck at s=%d" % s) + chain.append(nxt[0]) + return chain + + +def chain_to_word(chain, s0): + """Lift a state chain to a 36-letter floor word (ascending order outside it).""" + word = [None] * LENGTH + q0, t0 = chain[0] + pos = 0 + for letter in range(K): + for _ in range(q0[letter]): + word[pos] = letter + pos += 1 + for i in range(len(chain) - 1): + s = s0 + i + (q, t), (q2, t2) = chain[i], chain[i + 1] + word[s] = [j for j in range(K) if q2[j] != q[j]][0] + word[38 - s] = [j for j in range(K) if t2[j] != t[j]][0] + qt, tt = chain[-1] + pos = TOP + for letter in range(K): + for _ in range(tt[letter] - qt[letter]): + word[pos] = letter + pos += 1 + pos = PAIR_SUM - s0 + for letter in range(K): + for _ in range(C - t0[letter]): + word[pos] = letter + pos += 1 + require(all(x is not None for x in word), "word has holes") + return "".join(str(x) for x in word) + + +def counts(word, n): + return tuple(word[:n].count(j) for j in range(K)) + + +def check_word(text, s0, want_09=False): + """Literal check of a floor word; returns the sorted diagonal sum at s = 18.""" + require(len(text) == LENGTH, "length %d" % len(text)) + word = [int(ch) for ch in text] + require(all(0 <= x < K for x in word), "letter out of range") + require(all(word.count(j) == C for j in range(K)), "not a floor word") + for s in range(s0, TOP + 1): + sv = tuple(a + b for a, b in zip(counts(word, s), counts(word, PAIR_SUM - s))) + require(weight3(sv), "not weight-3 at s=%d" % s) + if want_09: + require(weight3(counts(word, MID)), "(0,9) is not weight-3") + top = tuple(a + b for a, b in zip(counts(word, TOP), counts(word, PAIR_SUM - TOP))) + return tuple(sorted(top)) + + +def rejects(text, s0, want_09=False): + try: + check_word(text, s0, want_09) + except SystemExit: + return True + return False + + +def witness_words(layers, succ, reach, masks, table): + """Deterministic witnesses: one per family, plus one with (0,9) weight-3.""" + words = {} + for fam, row in sorted(table.items()): + chain = pick_chain(layers, succ, reach, row[1], masks[fam]) + words[fam] = (row[1], chain_to_word(chain, row[1])) + everything = (1 << len(layers[TOP])) - 1 + filtered, _ = reach_masks(layers, succ, require_09=True) + return words, chain_to_word(pick_chain(layers, succ, filtered, 8, everything), 8), filtered + + +def check_threshold(layers, filtered): + """(0,9) weight-3 together with weight-3 on [s0,18] needs s0 >= 8.""" + nine = {v for v in itertools.product(range(C + 1), repeat=K) if sum(v) == MID and weight3(v)} + require(len(nine) == 60 and nine == set(itertools.permutations((1, 1, 1, 6, 0, 0))), "(0,9) shapes") + for x in layers[MID]: + if x[0] in nine: + require(lows(x) == 1, "(0,9)-shaped state with lows != 1") + starts = {s0: sum(1 for x in layers[s0] if filtered[s0][x]) for s0 in range(LOW, MID + 1)} + require(all(starts[s0] == 0 for s0 in range(LOW, 8)), "threshold: chain below 8") + require(starts[8] > 0 and starts[9] > 0, "threshold: no chain at 8 and 9") + return starts + + +def check_witnesses(generated, generated_09): + """Stored witnesses equal the generated ones and pass the literal checks.""" + require(WITNESS == generated and WITNESS_09 == generated_09, "stored witnesses differ") + for fam, (s0, word) in WITNESS.items(): + require(check_word(word, s0) == fam, "witness family %r" % (fam,)) + if s0 > LOW: + require(rejects(word, s0 - 1), "witness extends below window %r" % (fam,)) + for s0 in range(8, TOP + 1): + check_word(WITNESS_09, s0, want_09=True) + require(rejects(WITNESS_09, 7, want_09=True), "(0,9) witness must fail at s=7") + readme = (PKG / "README.md").read_text(encoding="utf-8") + for fam, (s0, word) in WITNESS.items(): + require(word in readme, "README lacks witness %r" % (fam,)) + require(WITNESS_09 in readme, "README lacks the (0,9) witness") + return len(WITNESS) + 1 + + +def check_sources(): + sources = json.loads((PKG / "SOURCES.json").read_text(encoding="utf-8")) + checked = 0 + for row in sources["files"]: + if row["usage"] != "input": + continue + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "pin " + row["path"]) + text = data.decode("utf-8") + for anchor in ("{0,1,6,7,12}", "weight-3 mask", CENTRE_SEP3, CENTRE_09): + require(anchor in text, "anchor %r missing in %s" % (anchor, row["path"])) + checked += 1 + require(checked == 1, "expected exactly one live input") + return checked + + +def check_controls(layers): + require(check_word(CONTROL_T1, LOW) == (6, 6, 6, 7, 7, 7), "cited T1 word") + require(check_word(CENTRE_SEP3, TOP) == (1, 1, 1, 12, 12, 12), "cited separation-3 word") + require(rejects(CENTRE_SEP3, TOP - 1), "separation-3 word must fail at s=17") + require(weight3(counts([int(c) for c in CENTRE_09], MID)), "cited (0,9) word") + require(rejects(CONTROL_T1[:-1], LOW), "35 letters must be rejected") + require(rejects(CONTROL_T1[:-1] + "4", LOW), "a seventh copy must be rejected") + require(rejects(CONTROL_T1, LOW, want_09=True), "T1 word has no weight-3 (0,9)") + require(len(layers[TOP]) == 700, "top layer size") + return 7 + + +def run(print_witnesses): + inputs = check_sources() + layers = build_layers() + total = sum(len(v) for v in layers.values()) + succ = build_successors(layers) + steps = check_lemma_a(layers, succ) + first = check_static_bound(layers) + reach, top_index = reach_masks(layers, succ) + masks, sizes = family_masks(layers, top_index) + require(sorted(sizes.values()) == [20, 20, 120, 180, 180, 180], "family sizes") + table = window_table(layers, reach, masks) + forward = check_forward(layers, succ, top_index, masks, table) + words, word_09, filtered = witness_words(layers, succ, reach, masks, table) + starts = check_threshold(layers, filtered) + if print_witnesses: + print("WITNESS = {") + for fam, value in sorted(words.items()): + print(" %r: %r," % (fam, value)) + print("}") + print("WITNESS_09 = %r" % word_09) + return 0 + stored = check_witnesses(words, word_09) + controls = check_controls(layers) + joined = [table[f][4] for f in sorted(table)] + print("PASS_SIX_SOURCE_C6_CHAIN_WINDOWS states=%d steps=%d first=%s joined=%s forward=%d " + "starts09=%s witnesses=%d controls=%d inputs=%d" % ( + total, steps, sorted(first.items()), joined, forward, + [starts[s] for s in range(LOW, MID + 1)], stored, controls, inputs)) + return 0 + + +if __name__ == "__main__": + sys.exit(run("--print-witnesses" in sys.argv))