Skip to content

Prove sharp c=6 endpoint chain windows (no κ) #7176

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
petalas wants to merge 1 commit into
base: main
Choose a base branch
from
+899 −0
Open

Prove sharp c=6 endpoint chain windows (no κ) #7176

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
183 changes: 183 additions & 0 deletions research/six-source-c6-chain-windows/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
154 changes: 154 additions & 0 deletions research/six-source-c6-chain-windows/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
24 changes: 24 additions & 0 deletions research/six-source-c6-chain-windows/SOURCES.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
]
}
Loading
Loading