Classify the six-source centre in every characteristic (no κ)

research/six-source-all-c-centre-emptiness/README.md

@@ -0,0 +1,177 @@
+# The centre of the six-source diagonal, in every characteristic
+
+**Scoped classification. No new κ.** On the six-source diagonal
+`s + t = 6c + 3`, the residue-legal centre pair of the frozen-coordinate
+argument is classified for every characteristic `c >= 2`:
+
+- even `c >= 4`: there is no residue-legal centre at all;
+- odd `c >= 5`: there are exactly **300** residue-legal centres, all of
+  weight 3, in exactly two count shapes (`180 + 120`);
+- `c = 3`: 366 residue-legal centres, 300 of weight 3;
+- `c = 2`: 450 residue-legal centres, none of weight 3.
+
+The c=6 emptiness of merged PR #6955 is therefore an even-characteristic
+phenomenon, not a property of the value six. Every odd characteristic at least
+three has weight-3 centres, and at odd `c >= 5` the weight-3 centre always
+carries the value `2c` that the frozen-coordinate step needs. The selected
+conditional κ stays `63005817/100000000000`.
+
+This package studies the residue-legal centre pair only. It does not search
+words, does not rerun the solver verdict of PR #6141, and does not claim a
+depth-two exclusion.
+
+## Interface, unchanged
+
+The interface is the one used by merged PR #6955, which follows PR #4231 and
+PR #4248. A floor word on `k = 6` sources in characteristic `c` has length
+`6c` and calls each source exactly `c` times. `q_t` counts the first `t`
+letters, so `q_0 = 0`, `q_{6c} = (c,...,c)`, each step adds one basis vector,
+and every count lies in `{0,...,c}`. Boundary `6c` is identified with `0`.
+
+On the diagonal `s + t = 6c + 3` the centre pair is
+
+    (3c+1, 3c+2),   q_{3c+2} = q_{3c+1} + e_j,
+
+so the centre sum is `2r + e_j` with `r = q_{3c+1}` and `r_j <= c-1`.
+
+A pair realizes a **weight-3 mask** when every coordinate of `q_s + q_t` lies
+in the residue set
+
+    A_c = {v in 0..2c : v = 0 or 1 (mod c)}
+
+and exactly three coordinates are `1 (mod c)`. The mask bit is the residue 1;
+this is the weight identity of PR #6107 as specialized in PR #6955. A sum of
+two counts in `{0,...,c}` lies in `{0,...,2c}`, so `A_c` is exactly the range
+of residue-legal values.
+
+## Even characteristic
+
+**Lemma 1.** For even `c >= 4` every residue-legal centre count is a multiple
+of `c/2`, while the centre length `3c+1` is not.
+
+*Proof.* Take a coordinate `j`. Off the centre the sum is `2r_j`, which is
+even; among the elements of `A_c` congruent to 1 modulo `c`, the odd ones are
+`1, c+1, ..., 2c+1`, so an even element is congruent to 0 and lies in
+`{0, c, 2c}`. Hence `r_j` is `0`, `c/2` or `c`. At the centre the sum is
+`2r_j + 1`, which is odd; the odd elements of `A_c` are `1` and `c+1`, so
+`r_j` is `0` or `c/2`. Every count is therefore a multiple of `c/2`. But
+`r` is a prefix count of length `3c+1`, and `3c+1 = 1 (mod c/2)` with
+`c/2 >= 2`. A multiple of `c/2` cannot equal `3c+1`. ∎
+
+So no residue-legal centre exists for any even `c >= 4`, and in particular no
+weight-3 centre does. The c=6 case of PR #6955 is the instance `c = 6`.
+
+## Odd characteristic
+
+**Lemma 2.** For odd `c >= 3`, off the centre `r_j` lies in `{0, h, c}` with
+`h = (c+1)/2`, and at the centre `r_j` lies in `{0, a}` with `a = (c-1)/2`.
+
+*Proof.* Off the centre `2r_j` is again even. The even elements of `A_c` are
+`0`, `c`, `c+1` and `2c`; `2r_j = c` has no integer solution because `c` is
+odd, so `2r_j` is `0`, `c+1` or `2c`. At the centre `2r_j + 1` is odd; the odd
+elements of `A_c` are `1` and `c`, giving `r_j = 0` or `a`. ∎
+
+Write `m` for the number of non-centre coordinates equal to `c` and `k` for
+the number equal to `h`; the remaining `5-m-k` non-centre coordinates are 0,
+and the centre count is `xi` in `{0, a}`. The prefix length gives
+
+    m c + k h + xi = 3c + 1.
+
+Substituting `2h = c+1`, `2a+1 = c` and checking every `m, k` in `0..5`:
+
+- `xi = 0` forces `(m,k) = (2,2)`;
+- `xi = a` forces `(m,k) = (1,3)`;
+- for `c = 3` only, two further solutions appear, `(m,k) = (3,0)` and
+  `(0,5)`.
+
+**Counts.** The `(2,2,0)` shape has count vector `{0,0,h,h,c,c}` with the
+centre on one of the two zero coordinates: `6!/(2!2!2!) · 2 = 180`
+realizations. The `(1,3,a)` shape has `{0,a,h,h,h,c}` with the centre forced
+at `a`: `6!/3! = 120` realizations. Both have exactly three coordinates
+`1 (mod c)`: in the first shape the centre contributes `1` and the two `h`
+coordinates contribute `2h = c+1`; in the second the centre contributes
+`2a+1 = c = 0 (mod c)` and the three `h` coordinates contribute. Hence, for
+odd `c >= 5`, there are exactly 300 residue-legal centres and all have
+weight 3.
+
+At `c = 3` the two extra families are `{0,0,a,c,c,c}` with the centre at `a`
+(60 realizations, weight 0) and `{0,h,h,h,h,h}` with the centre at `0`
+(6 realizations, weight 6). The census below confirms 366 legal centres, of
+which 300 have weight 3. At `c = 2` the step `c/2` is 1, every count is legal,
+and the centre is odd at exactly one coordinate, so the 450 legal centres all
+have weight 1.
+
+## What this changes
+
+The c=6 centre is empty because 6 is even, and the same holds for every even
+characteristic. The frozen-coordinate induction needs a weight-3 centre
+carrying `2c`; at odd `c >= 5` the `(2,2,0)` shape supplies two coordinates
+equal to `2c` and the `(1,3,a)` shape supplies one, so this residue count is
+not an obstruction there. Any claim that the centre route is universally dead
+would be wrong. The next step for odd characteristic is the induction itself,
+not another centre census.
+
+At even characteristic the centre slot is unavailable, so the induction has to
+start elsewhere or change mechanism. That is a statement about this centre
+pair only; it is not a depth-two exclusion.
+
+## Census
+
+`verify.py` enumerates every count vector with sum `3c+1` and every centre
+letter with `counts[centre] <= c-1`, and tests every coordinate of `2r + e_j`
+against `A_c`. Exact totals:
+
+| c | count vectors | centre letters | legal | weight-3 |
+|---:|---:|---:|---:|---:|
+| 2 | 126 | 450 | 450 | 0 |
+| 3 | 546 | 2346 | 366 | 300 |
+| 4 | 1686 | 7926 | 0 | 0 |
+| 5 | 4221 | 20916 | 300 | 300 |
+| 6 | 9156 | 46956 | 0 | 0 |
+| 7 | 17892 | 93996 | 300 | 300 |
+| 8 | 32292 | 172692 | 0 | 0 |
+| 9 | 54747 | 296802 | 300 | 300 |
+| 10 | 88242 | 483582 | 0 | 0 |
+
+The c=6 row reproduces the predecessor's `9156 / 46956 / 0` totals. Beyond the
+census range the two lemmas and the two linear equations are checked for every
+`c = 3, ..., 999` by integer arithmetic, so the classification is a written
+proof for all `c`, with the census as corroboration on a small range.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library only:
+
+```sh
+python3.12 -B -W error research/six-source-all-c-centre-emptiness/verify.py
+python3.12 -B -O -W error research/six-source-all-c-centre-emptiness/verify.py
+```
+
+The marker is `PASS_ALL_C_CENTRE_CLASSIFICATION`. Nothing here reads a live
+service or a frozen archive; the two hash-pinned provenance files are listed in
+[SOURCES.json](SOURCES.json).
+
+## Open next questions
+
+1. At odd `c >= 5`, does the `(2,2,0)` or the `(1,3,a)` centre actually extend
+   to the frozen-coordinate induction from `s = 3c+1` down to `s = 4`? The
+   residue count supplies the `2c` coordinate but not the intermediate
+   weight-3 indices.
+2. Which off-centre indices `s != 3c+1` carry residue-legal weight-3 masks at
+   even `c`? The c=6 examples in PR #6955 sit off the centre, and a complete
+   index classification is the natural replacement for the dead centre slot.
+3. Do the c=3 families of weight 0 and weight 6 interact with any mask
+   identity, or are they excluded by a different hypothesis?
+
+## Credit
+
+This package was produced by Nick Petalas.
+
+Merged PR #6955 by unpaidmoon supplies the six-source model, the residue set,
+the c=6 centre classification and the description of the c=7 frozen-14 step;
+this package generalizes its c=6 statement and does not replay it. The weight
+identity is PR #6107. The interface is PR #4231 / PR #4248. The solver verdict
+for the characteristic-six depth-two exclusion is PR #6141 and is cited, not
+rerun. The c=7 off-diagonal question is left open by discussion comment
+19493159 and fork PR #156. No characteristic polynomial, no word search and no
+supplier admission is claimed.

research/six-source-all-c-centre-emptiness/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"
+    }
+  ]
+}

research/six-source-all-c-centre-emptiness/TASK.json

@@ -0,0 +1,79 @@
+{
+  "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": "Exact centre classification of the six-source diagonal s+t=6c+3 for every characteristic c>=2: no residue-legal centre for even c>=4; exactly 300 weight-3 centres in two shapes for odd c>=5; the c=3 and c=2 censuses.",
+  "scope_change_reason": "The catalogue card asks for one new connector operation. Merged PR #6955 classifies only c=6 and leaves the general characteristic unclassified. This package keeps the alphabet fixed and supplies the missing general classification of the same centre pair. It does not add an operation and does not price a supplier.",
+  "bottleneck_link": "A scoped side result on the recursive-interface schedule. The c=6 centre emptiness is an even-characteristic phenomenon, so the frozen-coordinate induction is not obstructed by residue counting at odd characteristic. The selected conditional kappa stays 63005817/100000000000.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the even and odd count tables are proved, the two leading linear solutions and the two c=3 extras are enumerated, and the complete count-vector census for c=2..10 returns the stated totals. Do not search words, rerun PR #6141, or claim a depth-two exclusion.",
+  "outcome": "completed",
+  "evidence": "verify.py checks the even count restriction and the odd count tables for every c=3..999, solves the two linear equations for every odd c>=5, checks the 180+120 shape count, and enumerates the complete centre census for c=2..10. Marker PASS_ALL_C_CENTRE_CLASSIFICATION. The c=6 row reproduces the predecessor totals 9156/46956/0.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "At odd c>=5, does a residue-legal centre extend to the frozen-coordinate induction from s=3c+1 down to s=4?",
+      "why_it_matters": "The two centre shapes supply the 2c coordinate, but the induction also needs every intermediate index to be weight-3.",
+      "first_step": "Fix one c=7 centre shape and propagate the immovable coordinate down the diagonal.",
+      "blocked_by": "The intermediate weight-3 index set is not classified here."
+    },
+    {
+      "question": "Which off-centre indices s != 3c+1 carry residue-legal weight-3 masks at even c?",
+      "why_it_matters": "The centre slot is empty at even characteristic, so an off-centre start is the natural replacement.",
+      "first_step": "Classify residue-legal pairs on s+t=6c+3 with s<3c+1 for even c.",
+      "blocked_by": "Only the centre pair is enumerated here."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "platform": "darwin"
+  },
+  "overlap": {
+    "checked_at": "2026-11-11T21:34:00Z",
+    "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57",
+    "predecessor_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6955",
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19551775",
+    "limits": "Open PRs and merged packages were searched for the centre, the residue set and the formula 3c+1; no general-characteristic centre classification was found. The report is a lead, not a novelty certificate."
+  }
+}

research/six-source-all-c-centre-emptiness/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": 120,
+      "checks": "Even-characteristic count restriction for every c=4..999; odd count tables and linear solutions for every c=5..999; the 180+120 shape count with weight 3; complete count-vector census for c=2..10 with totals 450/366/0/300/0/300/0/300/0 legal centres and 0/300/0/300/0/300/0/300/0 of weight 3. The c=6 row reproduces the predecessor totals 9156 count vectors, 46956 centre letters and 0 legal sums. Controls cover the c=5, c=6 and c=7 residue sets and explicit shape witnesses at c=5 and c=7."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same classification and census under optimized Python. Failures are SystemExit, not assertions."
+    }
+  ]
+}