diff --git a/research/c5-sum13-adjacent-centre/README.md b/research/c5-sum13-adjacent-centre/README.md new file mode 100644 index 0000000000..fde31093b2 --- /dev/null +++ b/research/c5-sum13-adjacent-centre/README.md @@ -0,0 +1,334 @@ +# The characteristic-5 adjacent centre on `s + t = 13` freezes no coordinate + +**Classification. No new κ.** In the unchanged unsigned dirty connector, the +only adjacent pair on the sum `σ = 13` is `(6, 7)`. Every legal value of +`q_6 + q_7` is a weight-3 mask with coordinates in `{0, 1, 6}`. The only +immovable value in the allowed set is `10`, so this centre freezes no +coordinate. It therefore does not freeze a coordinate that meets a positive +share of the twenty weight-3 masks. + +The selected conditional κ stays `781451/250000000`. This note does not rerun +a SAT solver, does not touch the DRAT certificate in open PR #6216, and does +not replace the sum-33 chain argument in open PR #7038. + +## Definitions + +The interface is the depth-two interface of PR #4231 and PR #4248, as used by +PR #6141 and PR #7038. A floor word of length 30 calls each of six sources +exactly five times. Write `q_t` for the count of the first `t` letters, so +`q_0 = 0` and `q_30 = (5, 5, 5, 5, 5, 5)`. Each coordinate of a prefix lies in +`{0, ..., 5}`. + +A pair `(s, t)` with `0 ≤ s ≤ t ≤ 29` is **legal** when every coordinate of +`q_s + q_t` lies in + +```text +A = {0, 1, 5, 6, 10}. +``` + +The mask bit of a value in `A` is `1` for `{1, 6}` and `0` for `{0, 5, 10}`. +The coordinate sum of a legal pair is `s + t`, and its mask weight `w` +satisfies `s + t ≡ w (mod 5)`. + +A value `v ∈ A` is **immovable** when neither `v - 1` nor `v + 1` lies in `A`. +A coordinate of a legal sum is **frozen** when its value is immovable. This is +the meaning of the frozen coordinate `10` in PR #7038. The move table on `A` is + +| move | values | +|---|---| +| `+1` stays in `A` | `0 → 1`, `5 → 6` | +| `-1` stays in `A` | `1 → 0`, `6 → 5` | +| immovable | `10` only | + +There are `C(6, 3) = 20` weight-3 masks. Coordinate `j` **meets** a mask `m` +when `m_j = 1`. Each coordinate meets `C(5, 2) = 10` of the twenty masks, a +share of `1/2`. + +The pair `(s, s + 1)` is the **adjacent centre** on the odd sum `2s + 1`. +On `σ = 13` that pair is `(6, 7)`, and it is the only pair of indices on this +sum that differ by 1. Sum `28` is even, so it has no such pair. The repeated +index `(14, 14)` is a different centre and is not classified here. + +## Proved statement + +**Theorem.** Every legal adjacent centre on `s + t = 13` has centre letter +`w` satisfying `q_6[w] = 0`, exactly two other coordinates equal to `3`, and +the remaining three coordinates equal to `0`. The centre sum is `1` at `w`, +`6` at the two sources counted three times, and `0` elsewhere. There are +`6 · C(5, 2) = 60` such count vectors. Every one is a weight-3 mask, every +one is the prefix of a floor word, and none has a coordinate equal to `10`. + +In particular the adjacent centre freezes no coordinate. Since every +coordinate meets ten of the twenty weight-3 masks, the centre does not freeze +a coordinate that meets a positive share of those masks. + +The type split is the case analysis below. The checker exhausts every vector +in `{0, ..., 5}^6` of sum `6` and every centre letter with a remaining call. +That enumeration is an exhaustive finite census of a finite domain. It checks +the case split. It is not a heuristic search and not a solver verdict. + +## Case split + +Let `r = q_6` and let `w = w_6`, so `q_7 = r + e_w`, `∑ r_j = 6`, and +`r_w ≤ 4`. The centre sum is `2r + e_w`. + +A non-centre coordinate is legal only for `r_j ∈ {0, 3, 5}`: + +| `r_j` | `2 r_j` | in `A` | +|---:|---:|---| +| 0 | 0 | yes, mask bit 0 | +| 1 | 2 | no | +| 2 | 4 | no | +| 3 | 6 | yes, mask bit 1 | +| 4 | 8 | no | +| 5 | 10 | yes, mask bit 0 | + +The centre letter is legal only for `r_w ∈ {0, 2}`: + +| `r_w` | `2 r_w + 1` | in `A` | +|---:|---:|---| +| 0 | 1 | yes, mask bit 1 | +| 1 | 3 | no | +| 2 | 5 | yes, mask bit 0 | +| 3 | 7 | no | +| 4 | 9 | no | + +Let `n_0, n_3, n_5` count the five non-centre coordinates, so +`n_0 + n_3 + n_5 = 5`. + +**Centre count `0`.** The count equation is `3 n_3 + 5 n_5 = 6`. + +| `n_5` | equation | solution | +|---:|---|---| +| 0 | `3 n_3 = 6` | `n_3 = 2`, so `n_0 = 3` | +| 1 | `3 n_3 = 1` | not an integer solution | +| `≥ 2` | at least `10` | above `6` | + +The only solution has mask weight `n_3 + 1 = 3`. Its values are one `1`, two +`6`s and three `0`s. It contains no `10`. + +**Centre count `2`.** The centre contributes `2`, so +`3 n_3 + 5 n_5 = 4`. The case `n_5 = 0` gives `3 n_3 = 4`, which is not an +integer solution. The case `n_5 ≥ 1` is at least `5`, which is above `4`. +This case is empty. + +These rows are the whole legal centre. The sixty realizations come from +choosing the centre coordinate in `6` ways and the two coordinates equal to +`3` in `C(5, 2) = 10` ways. + +Each of those sixty vectors extends to a floor word. After the centre letter, +`q_7` still has coordinates in `{0, 1, 3}` and the residual quotas `5 - q_7[j]` +sum to `23`, which is the number of letters left. The checker builds one such +word for every vector and recomputes the centre sum. + +## The one-step neighborhood is not a freeze + +The diagonal step on this sum is + +```text +S(s - 1) = S(s) - e_{w_{s-1}} + e_{w_{13-s}}, +``` + +where `S(s) = q_s + q_{13-s}`. At the adjacent centre, `S(6) = q_6 + q_7`. +A subtraction letter is realizable only when it occurs in `q_6`. On the legal +shape those letters are the two sources of count `3`. Every one of the six +possible added letters keeps `q_8` inside `{0, ..., 5}`, because `q_7` is +coordinatewise at most `3`. + +That is `60 · 2 · 6 = 720` realizable steps. Exactly eight per centre are +legal: + +- the two steps that add the same triple source they subtract, which leave + the sum unchanged; +- the six steps that subtract a triple source and add a source of count `0`, + sending `6 → 5` and `0 → 1`. + +All `480` legal steps keep the centre coordinate equal to `1`. The `360` +steps of the second kind show that a coordinate equal to `6`, and a +coordinate equal to `0`, can both move inside `A`. This census is exhaustive +for the one-step neighborhood of every legal adjacent centre. + +The same arithmetic explains the centre coordinate without listing the steps. +Its value is `1`. The only in-`A` neighbor of `1` is `0`, and reaching `0` +requires subtracting the centre letter. That letter does not occur in `q_6`, +so the subtraction is not realizable. Adding the centre letter sends `1` to +`2`, which is outside `A`. A legal step therefore leaves the coordinate at +`1`. The value `1` itself is movable inside `A`; what is unavailable is the +letter that would move it. + +## Invariance along a legal diagonal + +**Lemma.** Suppose `S(6)` is a legal adjacent centre with centre letter `w`, +and suppose `S(s)` is legal for every `s = 0, ..., 6`. Then `S(s)_w = 1` for +every such `s`. + +The classification gives `S(6)_w = 1`. Proceed downward. The step from `s` to +`s - 1`, for `s = 6, ..., 1`, subtracts `w_{s-1}`. The index `s - 1` lies in +`{0, ..., 5}`, and `q_6[w] = 0`, so the subtracted letter is not `w`. Once the +coordinate equals `1`, adding `w` would replace `1` by `2`, which is outside +`A`. A legal image therefore leaves the coordinate equal to `1`, and the next +step starts from that same value. The coordinate stays `1` at every slot, +including `S(0) = q_13`. + +This hypothesis is realizable. The floor word + +```text +111222022311400003333444455555 +``` + +has centre letter `0` and the seven sums + +| `s` | partner | `q_s + q_{13-s}` | mask | +|---:|---:|---|---| +| 6 | 7 | `(1, 6, 6, 0, 0, 0)` | `(1, 1, 1, 0, 0, 0)` | +| 5 | 8 | `(1, 6, 6, 0, 0, 0)` | `(1, 1, 1, 0, 0, 0)` | +| 4 | 9 | `(1, 6, 6, 0, 0, 0)` | `(1, 1, 1, 0, 0, 0)` | +| 3 | 10 | `(1, 6, 5, 1, 0, 0)` | `(1, 1, 0, 1, 0, 0)` | +| 2 | 11 | `(1, 6, 5, 1, 0, 0)` | `(1, 1, 0, 1, 0, 0)` | +| 1 | 12 | `(1, 6, 5, 1, 0, 0)` | `(1, 1, 0, 1, 0, 0)` | +| 0 | 13 | `(1, 5, 5, 1, 1, 0)` | `(1, 0, 0, 1, 1, 0)` | + +Every entry lies in `A`, every mask has weight `3`, and coordinate `0` stays +equal to `1`. The three distinct masks all meet coordinate `0`. That +coordinate meets ten of the twenty weight-3 masks. The lemma fixes it on this +diagonal only. Masks may still be realized on another sum, and this word does +not realize the other seven masks that also have a `1` in coordinate `0`. + +The invariance is not the freeze in the theorem. It uses the missing letter +in the prefix. It does not make `1` immovable, and it does not force a `5` +into `q_4`. A coordinate equal to `1` splits as `0 + 1` or `1 + 0`, and a +length-`4` count can hold either part. + +The other coordinates are not invariant. The floor word + +```text +111222030000112233334444455555 +``` + +has the same legal centre `(1, 6, 6, 0, 0, 0)` and a legal image + +```text +S(5) = (1, 6, 5, 1, 0, 0). +``` + +Coordinate `2` moves from `6` to `5`, and coordinate `3` moves from `0` to +`1`. Replacing the added letter `3` by the centre letter `0` produces a `2`, +which leaves `A`. + +## What remains outside this pair + +The published floor word of PR #7038, + +```text +000001231234512345123451234545 +``` + +has adjacent sum `(10, 2, 1, 0, 0, 0)`, which is illegal, and realizes the +weight-3 mask `(10, 1, 1, 1, 0, 0)` at the non-adjacent pair `(5, 8)`. A +weight-3 mask on sum `13` does not make the adjacent centre legal. A `10` can +occur on this sum, on a pair this note does not classify. On a legal pair the +value `10` is a mask bit `0`, so an immovable coordinate is a `0`-bit of the +mask that contains it. + +PR #7038 proves that every legal centre on `s + t = 33` freezes a `10`, and +that the chain hypothesis (H) on that one diagonal is empty. This note does +not rerun that argument. Question 1 of that PR, whether every depth-two floor +word satisfies (H), is untouched. The characteristic-6 centre and the +characteristic-7 diagonal are untouched. Open PR #6216 is untouched. + +No supplier, consumer, or selected frontier changes. The live selected record +at the base commit is κ `= 781451/250000000 = 0.003125804`. The priority note +on this same commit still quotes the older selected figure from PR #5599; +this package follows the selected record. + +## Evidence class + +1. **Proof.** The case split enumerates every nonnegative integer solution of + `n_0 + n_3 + n_5 = 5` against the two count equations. One solution + survives. The move table on the five-element set `A` shows that `10` is + the only immovable value, and the surviving solution does not use it. +2. **Exhaustive finite census.** Every sum-`6` vector in `{0, ..., 5}^6`, + every legal centre letter, and all `720` realizable one-step letter pairs + were enumerated. The counts agree with the proof: `60` centres, `0` + coordinates equal to `10`, `480` legal steps, all of them preserving the + centre coordinate. +3. **Witnesses.** Two explicit floor words realize the legal centre. One + keeps all seven diagonal slots legal. The other moves a `6` in one legal + step. The published word shows an illegal adjacent centre beside a legal + pair that contains a `10`. These words are witnesses. They are not a + census of floor words, and a witness is not an unrestricted exclusion. + +A classification of this one pair is not an unrestricted characteristic-5 +exclusion, not a proof that no depth-two word exists, and not a change to κ. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -W error -B research/c5-sum13-adjacent-centre/verify.py +python3.12 -I -O -W error -B research/c5-sum13-adjacent-centre/verify.py +python3.12 -B scripts/research_package.py --package research/c5-sum13-adjacent-centre --check-only +``` + +The marker is + +```text +PASS_C5_SUM13_ADJACENT_CENTRE centres=60 weight3=60 frozen10=0 immovable=[10] mask_bit10=0 share=10/20 adjacent_pair=(6,7) sum28_adjacent_pairs=0 legal_steps=480 moving_steps=360 diagonal_slots=7 centre_bit=1 published_adjacent=illegal controls=6 +``` + +The six controls are the near-miss centre `(2, 2, 2, 0, 0, 0)`, the pair +geometry on sums `13` and `28`, the fully legal diagonal word, the one-step +word that moves a `6`, the centre-letter increase that leaves `A`, and the +published word above. No Lean, Docker, or historical suite was run. + +Overlap was checked with `scripts/find_overlap.py` on 2026-11-10 at base +`17469fff78c22941280f04d39dc5a1faee09c840` (339 open PRs, complete pagination; +7013 discussion records, complete pagination; local note inventory complete, +10178 head records). The query matches open PR #7038, which asks this +question and does not answer it, plus the characteristic-6 and +characteristic-7 centre notes and unrelated centre-path discussions. No match +classifies `(6, 7)`. + +## Open next questions + +1. Does the adjacent centre on one of `σ ∈ {3, 23, 43, 53}` contain a + coordinate equal to `10`? + *Why:* those are the other adjacent sums congruent to `3` modulo `5`. + A `10` there would be the immovable freeze already proved for sum `33`, + on a diagonal the sum-33 walk does not see. + *First step:* repeat the count equation at `s = (σ - 1) / 2` for one named + sum, at characteristic `5` only. + *Blocked by:* each adjacent sum has a different prefix total, so the + sum-`13` row does not decide it. +2. Which legal values can the repeated centre `2 q_14` take on `s + t = 28`? + *Why:* sum `28` is the other sum named beside `13`, and it has fifteen + pairs, none of them adjacent. The doubled prefix has no centre letter, so + it can still contain a `10`. + *First step:* enumerate `r ∈ {0, ..., 5}^6` with `∑ r_j = 14` and + `2 r ∈ A^6`. + *Blocked by:* there is no centre-letter equation on a repeated index. The + split used here does not apply. +3. How many distinct weight-3 masks can one fully legal sum-`13` diagonal + realize under the centre-bit lemma? + *Why:* the lemma leaves at most the ten masks that meet the centre + letter, and the explicit word realizes three. A sharp count would say + whether this diagonal alone can hold a positive share of the twenty masks. + *First step:* classify one non-adjacent pair on sum `13`, for example + `(5, 8)`, at characteristic `5` only. + *Blocked by:* the two prefixes differ by more than one letter, so the + adjacent-centre equation does not determine that pair. + +## Credit + +The depth-two interface is Nick Petalas's (PR #4231, PR #4248), with the Ross +Richardson PR #934 / PR #943 lineage. PR #6107 supplies the weight identity. +JosieElliston's PR #6141 is the solver exclusion at characteristics 5 and 6. +queelius's open PR #6216 is the characteristic-5 DRAT certificate; it is not +replayed here. The sum-33 centre freeze, the published witness word, and the +question answered here are open PR #7038, head +`3240f7d58d608a97449d4c07f04e8995b9761c15`, from the same account. The +characteristic-7 chain is discussion comment 19493159. The characteristic-6 +centre classification is separate and is not used. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/c5-sum13-adjacent-centre/SOURCES.json b/research/c5-sum13-adjacent-centre/SOURCES.json new file mode 100644 index 0000000000..41a0d8e4ed --- /dev/null +++ b/research/c5-sum13-adjacent-centre/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-sum13-adjacent-centre/TASK.json b/research/c5-sum13-adjacent-centre/TASK.json new file mode 100644 index 0000000000..132de59cdc --- /dev/null +++ b/research/c5-sum13-adjacent-centre/TASK.json @@ -0,0 +1,74 @@ +{ + "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. Classify the adjacent centre (6, 7) on s+t=13 and decide whether it freezes a coordinate that meets a positive share of the twenty weight-3 masks. The proved statement is that every legal centre sum lies in {0,1,6}^6, so it freezes no coordinate. Sum 28 is not classified.", + "scope_change_reason": "The catalogue card asks for one new connector operation. This package keeps the alphabet fixed and answers open question 2 of PR #7038 at the single adjacent pair on sigma=13. A new operation is not the missing step. The sum-33 chain hypothesis, the characteristic-6 centre, and the characteristic-7 diagonal are other questions.", + "bottleneck_link": "Side result on the recursive-interface schedule. It does not change a supplier, a consumer, or kappa. The sum-13 adjacent centre was the named obstruction to carrying the sum-33 freeze onto the weight-3 masks realized off that diagonal.", + "budget_minutes": 60, + "stop_rule": "Stop after the adjacent pair (6, 7) is classified and the freeze question is answered under written hypotheses. Do not classify another sum or another pair.", + "outcome": "negative-result", + "evidence": "Proof: the only nonnegative solution of the centre equations is (r_w, n0, n3, n5)=(0, 3, 2, 0). The centre sum is a permutation of (1, 6, 6, 0, 0, 0). The only immovable value in {0,1,5,6,10} is 10, which does not occur, so the centre freezes no coordinate. Each coordinate meets 10 of the 20 weight-3 masks. Exhaustive census: 60 legal centres, 0 coordinates equal to 10, all 60 realizable by floor words, 720 realizable one-step pairs, 480 legal steps, every legal step preserving the centre coordinate, 360 of them moving a 6 to a 5. Companion lemma, not a freeze: if all seven sum-13 pairs are legal, the centre letter stays equal to 1. The floor word 111222022311400003333444455555 realizes that hypothesis. The published #7038 word has an illegal adjacent centre and a 10 at pair (5, 8). No SAT run.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance: the case split, the one-step census, the diagonal lemma, the witness words, the checker, and the package text.", + "open_questions": [ + { + "question": "Does the adjacent centre on one of sigma in {3, 23, 43, 53} contain a coordinate equal to 10?", + "why_it_matters": "Those are the other adjacent sums congruent to 3 modulo 5. A 10 there would be the immovable freeze already proved for sum 33, on a diagonal the sum-33 walk does not see.", + "first_step": "Repeat the count equation at s=(sigma-1)/2 for one named sum, at characteristic 5 only.", + "blocked_by": "Each adjacent sum has a different prefix total, so the sum-13 row does not decide it." + }, + { + "question": "Which legal values can the repeated centre 2 q_14 take on s+t=28?", + "why_it_matters": "Sum 28 is the other sum named beside 13, and it has fifteen pairs, none of them adjacent. The doubled prefix has no centre letter, so it can still contain a 10.", + "first_step": "Enumerate r in {0,...,5}^6 with coordinate sum 14 and 2r in {0,1,5,6,10}^6.", + "blocked_by": "There is no centre-letter equation on a repeated index. The split used here does not apply." + }, + { + "question": "How many distinct weight-3 masks can one fully legal sum-13 diagonal realize under the centre-bit lemma?", + "why_it_matters": "The lemma leaves at most the ten masks that meet the centre letter, and the explicit word realizes three. A sharp count would say whether this diagonal alone can hold a positive share of the twenty masks.", + "first_step": "Classify one non-adjacent pair on sum 13, for example (5, 8), at characteristic 5 only.", + "blocked_by": "The two prefixes differ by more than one letter, so the adjacent-centre equation does not determine that pair." + } + ] +} diff --git a/research/c5-sum13-adjacent-centre/VERIFY.json b/research/c5-sum13-adjacent-centre/VERIFY.json new file mode 100644 index 0000000000..c957eef797 --- /dev/null +++ b/research/c5-sum13-adjacent-centre/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exhaustive census of every q_6 in {0,...,5}^6 summing to 6 and every centre letter with room for one more call. Expect 60 legal centres, all weight 3, of shape (1,6,6,0,0,0) up to permutation, and zero coordinates equal to 10. The nonnegative case split has the single solution (n0,n3,n5)=(3,2,0) at centre count 0. Each of the 60 vectors extends to a floor word. The one-step neighborhood has 480 legal realizable steps and 360 steps that move a 6 to a 5; every legal step keeps the centre coordinate equal to 1. Controls: a sum-6 near miss, the unique adjacent pair (6,7) and the absence of an adjacent pair on sum 28, one floor word with all seven sum-13 pairs legal, one floor word whose legal step moves a 6, the centre-letter increase exiting A, and the published word whose adjacent centre is illegal while pair (5,8) contains a 10." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same census under optimized Python. Failures are explicit exceptions, not assertions." + } + ] +} diff --git a/research/c5-sum13-adjacent-centre/verify.py b/research/c5-sum13-adjacent-centre/verify.py new file mode 100644 index 0000000000..7ad00b71f9 --- /dev/null +++ b/research/c5-sum13-adjacent-centre/verify.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Classification of the characteristic-5 adjacent centre on s + t = 13. + +The argument is in README.md. This program exhausts the finite centre domain +and the finite one-step neighborhood, and it checks three explicit words. +It does not search for a depth-two word and it does not call a SAT solver. +""" + +import itertools +import math + +K = 6 +C = 5 +LENGTH = K * C +SIGMA = 13 +CENTRE_S = 6 # partner 7; 6 + 7 = 13 +ALLOWED = (0, 1, C, C + 1, 2 * C) +MASK_BIT = {0: 0, 1: 1, C: 0, C + 1: 1, 2 * C: 0} +# Floor word whose seven sum-13 pairs are all legal. The centre letter is 0. +DIAGONAL = (1, 1, 1, 2, 2, 2, 0, 2, 2, 3, 1, 1, 4, 0, 0, 0, 0, + 3, 3, 3, 3, 4, 4, 4, 4, 5, 5, 5, 5, 5) +# Same centre, with the next letter moving a 6 down to 5. +STEP = (1, 1, 1, 2, 2, 2, 0, 3, 0, 0, 0, 0, 1, 1, 2, 2, + 3, 3, 3, 3, 4, 4, 4, 4, 4, 5, 5, 5, 5, 5) +PUBLISHED = (0, 0, 0, 0, 0, 1, 2, 3, 1, 2, 3, 4, 5, 1, 2, 3, 4, 5, + 1, 2, 3, 4, 5, 1, 2, 3, 4, 5, 4, 5) +DIAGONAL_SUMS = { + 0: (1, 5, 5, 1, 1, 0), + 1: (1, 6, 5, 1, 0, 0), + 2: (1, 6, 5, 1, 0, 0), + 3: (1, 6, 5, 1, 0, 0), + 4: (1, 6, 6, 0, 0, 0), + 5: (1, 6, 6, 0, 0, 0), + 6: (1, 6, 6, 0, 0, 0), +} + + +def fail(msg): + raise SystemExit('FAIL: ' + msg) + + +def mask_weight(sum_vec): + bits = 0 + for value in sum_vec: + bit = MASK_BIT.get(value) + if bit is None: + return None + bits += bit + return bits + + +def mask_of(sum_vec): + if mask_weight(sum_vec) is None: + return None + return tuple(MASK_BIT[value] for value in sum_vec) + + +def prefixes(word): + counts = [0] * K + out = [tuple(counts)] + for letter in word: + counts[letter] += 1 + out.append(tuple(counts)) + return out + + +def require_floor(word, label): + if len(word) != LENGTH: + fail(label + ' length is not 30') + counts = [0] * K + for letter in word: + if not 0 <= letter < K: + fail(label + ' letter out of range') + counts[letter] += 1 + if counts[letter] > C: + fail(label + ' exceeds five calls of one source') + if counts != [C] * K: + fail(label + ' is not a floor word: ' + str(counts)) + + +def centre_sum(counts, centre): + return tuple(2 * counts[j] + (1 if j == centre else 0) for j in range(K)) + + +def main(): + if (K, C, SIGMA, CENTRE_S) != (6, 5, 13, 6) or ALLOWED != (0, 1, 5, 6, 10): + fail('pinned characteristic-5 constants changed') + if 2 * CENTRE_S + 1 != SIGMA: + fail('the adjacent sum is not 13') + + non_centre = [r for r in range(C + 1) if 2 * r in MASK_BIT] + centre_types = [r for r in range(C) if 2 * r + 1 in MASK_BIT] + if non_centre != [0, 3, 5] or centre_types != [0, 2]: + fail('local types changed: non-centre %s, centre %s' % (non_centre, centre_types)) + + # Finite case split: n0 + n3 + n5 = 5 and the count equation. + solutions = [] + for centre_count, remainder in ((0, 6), (2, 4)): + for n5 in range(6): + for n3 in range(6): + n0 = 5 - n3 - n5 + if n0 < 0: + continue + if 3 * n3 + 5 * n5 == remainder: + solutions.append((centre_count, n0, n3, n5)) + if solutions != [(0, 3, 2, 0)]: + fail('case split changed: ' + str(solutions)) + predicted = K * math.comb(5, 2) + if predicted != 60: + fail('multinomial prediction changed: %s' % predicted) + + found = [] + weights = {} + frozen = 0 + for counts in itertools.product(range(C + 1), repeat=K): + if sum(counts) != CENTRE_S: + continue + for centre in range(K): + if counts[centre] >= C: + continue + summed = centre_sum(counts, centre) + weight = mask_weight(summed) + if weight is None: + continue + weights[weight] = weights.get(weight, 0) + 1 + frozen += sum(1 for value in summed if value == 10) + others = tuple(sorted(counts[j] for j in range(K) if j != centre)) + values = tuple(sorted(summed)) + if counts[centre] != 0 or others != (0, 0, 0, 3, 3) or values != (0, 0, 0, 1, 6, 6): + fail('legal centre outside the unique shape: q=%s centre=%s sum=%s' % (counts, centre, summed)) + if summed[centre] != 1 or weight != 3: + fail('centre letter is not the unique 1 of a weight-3 mask') + found.append((counts, centre, summed)) + + if weights != {3: predicted} or len(found) != predicted or frozen != 0: + fail('census mismatch: weights %s found %s frozen %s' % (weights, len(found), frozen)) + + immovable = [v for v in ALLOWED if v + 1 not in MASK_BIT and v - 1 not in MASK_BIT] + increments = [v for v in ALLOWED if v + 1 in MASK_BIT] + decrements = [v for v in ALLOWED if v - 1 in MASK_BIT] + if immovable != [10] or increments != [0, 5] or decrements != [1, 6]: + fail('move table changed: immovable %s +%s -%s' % (immovable, increments, decrements)) + if MASK_BIT[10] != 0 or 1 not in decrements: + fail('10 is not a 0-bit, or 1 cannot decrease inside A') + share_total = math.comb(K, 3) + share_hit = math.comb(K - 1, 2) + if share_total != 20 or share_hit != 10: + fail('weight-3 share changed: %s of %s' % (share_hit, share_total)) + + # Every one of the 60 count vectors is a prefix of a floor word. + for counts, centre, summed in found: + order = [] + for source, count in enumerate(counts): + order.extend([source] * count) + if len(order) != CENTRE_S or centre in order: + fail('centre letter already occurs in q_6') + q7 = list(counts) + q7[centre] += 1 + if any(value > C for value in q7): + fail('q_7 exceeds five') + rest = [] + for source, count in enumerate(q7): + rest.extend([source] * (C - count)) + if sum(C - count for count in q7) != LENGTH - (CENTRE_S + 1): + fail('residual quota does not fill the word') + word = tuple(order + [centre] + rest) + require_floor(word, 'realized centre') + pref = prefixes(word) + if pref[CENTRE_S] != counts or pref[CENTRE_S + 1][centre] != 1: + fail('realized prefix left the centre shape') + if centre_sum(pref[CENTRE_S], centre) != summed: + fail('realized centre sum changed') + + # Exhaustive one-step neighborhood. A subtraction is realizable only when + # that source occurs in q_6. Every addition is count-feasible on this shape. + legal_steps = 0 + moving_steps = 0 + for counts, centre, summed in found: + q7 = list(counts) + q7[centre] += 1 + local_legal = 0 + local_moving = 0 + realizable_subs = [source for source in range(K) if counts[source] >= 1] + if realizable_subs != [source for source in range(K) if counts[source] == 3]: + fail('realizable subtraction letters are not the two triple sources') + for sub in realizable_subs: + for add in range(K): + if q7[add] >= C: + fail('a count-feasible addition was rejected by the shape') + image = list(summed) + image[sub] -= 1 + image[add] += 1 + if mask_weight(image) is None: + continue + if image[centre] != 1: + fail('legal one-step image moved the centre coordinate: %s' % image) + local_legal += 1 + if any(summed[j] == 6 and image[j] == 5 for j in range(K)): + local_moving += 1 + if local_legal != 8 or local_moving != 6: + fail('one-step counts changed: legal %s moving %s' % (local_legal, local_moving)) + legal_steps += local_legal + moving_steps += local_moving + if legal_steps != 480 or moving_steps != 360: + fail('neighborhood totals changed: %s %s' % (legal_steps, moving_steps)) + + controls = 0 + + # Sum 6 can still leave A. Three 2s with centre letter 0 is one example. + near = (2, 2, 2, 0, 0, 0) + if sum(near) != CENTRE_S or mask_weight(centre_sum(near, 0)) is not None: + fail('near-miss centre was accepted') + controls += 1 + + # Pair geometry: (6, 7) is the only adjacent pair on sum 13, and sum 28 + # has none. This package does not classify the repeated index (14, 14). + adjacent_13 = [] + adjacent_28 = [] + slots_13 = 0 + slots_28 = 0 + for left in range(LENGTH): + for right in range(left, LENGTH): + if left + right == 13: + slots_13 += 1 + if right - left == 1: + adjacent_13.append((left, right)) + if left + right == 28: + slots_28 += 1 + if right - left == 1: + adjacent_28.append((left, right)) + if slots_13 != 7 or adjacent_13 != [(6, 7)] or slots_28 != 15 or adjacent_28 != []: + fail('adjacent-pair geometry changed: %s %s %s %s' % (slots_13, adjacent_13, slots_28, adjacent_28)) + controls += 1 + + # Full diagonal: every sum-13 pair is legal and the centre coordinate stays 1. + require_floor(DIAGONAL, 'diagonal witness') + pref = prefixes(DIAGONAL) + if pref[6] != (0, 3, 3, 0, 0, 0) or pref[7] != (1, 3, 3, 0, 0, 0): + fail('diagonal witness left the centre shape') + seen = set() + for slot in range(7): + summed = tuple(pref[slot][j] + pref[13 - slot][j] for j in range(K)) + if summed != DIAGONAL_SUMS[slot] or mask_weight(summed) != 3 or summed[0] != 1: + fail('diagonal slot %s changed: %s' % (slot, summed)) + seen.add(mask_of(summed)) + for slot in range(1, 7): + current = tuple(pref[slot][j] + pref[13 - slot][j] for j in range(K)) + previous = tuple(pref[slot - 1][j] + pref[14 - slot][j] for j in range(K)) + sub = DIAGONAL[slot - 1] + add = DIAGONAL[13 - slot] + if sub == 0: + fail('a downward step subtracted the centre letter') + expected = list(current) + expected[sub] -= 1 + expected[add] += 1 + if tuple(expected) != previous or previous[0] != 1: + fail('diagonal recurrence broke at slot %s' % slot) + if seen != {(1, 1, 1, 0, 0, 0), (1, 1, 0, 1, 0, 0), (1, 0, 0, 1, 1, 0)}: + fail('diagonal masks changed: %s' % (seen,)) + controls += 1 + + # One legal step can move a 6 to a 5 and a 0 to a 1. The centre bit stays 1. + require_floor(STEP, 'step witness') + pref = prefixes(STEP) + top = tuple(pref[6][j] + pref[7][j] for j in range(K)) + nxt = tuple(pref[5][j] + pref[8][j] for j in range(K)) + if top != (1, 6, 6, 0, 0, 0) or nxt != (1, 6, 5, 1, 0, 0): + fail('step witness sums changed: %s -> %s' % (top, nxt)) + if mask_weight(top) != 3 or mask_weight(nxt) != 3 or nxt[0] != 1: + fail('step witness left A or moved the centre bit') + if not any(top[j] == 6 and nxt[j] == 5 for j in range(K)): + fail('step witness did not move a 6') + if not any(top[j] == 0 and nxt[j] == 1 for j in range(K)): + fail('step witness did not move a 0') + controls += 1 + + # Replacing that added letter by the centre letter sends 1 to 2. + bumped = list(top) + bumped[STEP[5]] -= 1 # undo w_5, which is not the centre letter + bumped[0] += 1 + if STEP[5] == 0 or mask_weight(bumped) is not None or bumped[0] != 2: + fail('adding the centre letter did not exit A') + controls += 1 + + # The published sum-13 witness realizes a 10 off the adjacent pair. + # Its own adjacent centre is illegal, so a weight-3 mask at sum 13 does + # not make (6, 7) legal. + require_floor(PUBLISHED, 'published witness') + pref = prefixes(PUBLISHED) + adjacent = tuple(pref[6][j] + pref[7][j] for j in range(K)) + off = tuple(pref[5][j] + pref[8][j] for j in range(K)) + if adjacent != (10, 2, 1, 0, 0, 0) or mask_weight(adjacent) is not None: + fail('published adjacent centre became legal: %s' % (adjacent,)) + if off != (10, 1, 1, 1, 0, 0) or mask_weight(off) != 3 or 5 + 8 != 13: + fail('published off-adjacent pair changed: %s' % (off,)) + if off[0] != 10: + fail('published off-adjacent pair lost its 10') + controls += 1 + + if controls != 6: + fail('control count changed: %s' % controls) + + print( + 'PASS_C5_SUM13_ADJACENT_CENTRE ' + 'centres=60 weight3=60 frozen10=0 immovable=[10] mask_bit10=0 ' + 'share=10/20 adjacent_pair=(6,7) sum28_adjacent_pairs=0 ' + 'legal_steps=480 moving_steps=360 diagonal_slots=7 centre_bit=1 ' + 'published_adjacent=illegal controls=6' + ) + + +if __name__ == '__main__': + main()