Lower the characteristic-four connector floor bound to N(4) ≤ 20; the known nine-source walk does not extend (no new κ)

research/connector-char4-floor-bounds/CERTIFICATE.json

@@ -0,0 +1,6 @@
+{
+  "schema_version": 1,
+  "characteristic": 4,
+  "source": "nine-source floor walk of PR4248 (CERTIFICATE.json floor_walks[\"9\"], head e7df122403cfc2febfb6799abb821487d8d1ee49)",
+  "walk9": [4, 2, 6, 4, 0, 8, 1, 7, 3, 2, 5, 2, 1, 7, 4, 3, 0, 2, 5, 8, 6, 5, 6, 4, 8, 3, 1, 0, 5, 7, 8, 7, 0, 3, 6, 1]
+}

research/connector-char4-floor-bounds/README.md

@@ -0,0 +1,156 @@
+# Unsigned connector in characteristic four: 9 ≤ N(4) ≤ 20
+
+Take the unsigned dirty connector of
+[#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231) over a ring
+of characteristic c, with k immutable sources and all 2^k − 1 nonzero
+binary-mask outputs. Every legal word needs at least c(k + 2^k − 1) complete
+calls. Let N(c) be the largest k at which that floor is attained.
+[#4248](https://github.com/CrocSwap/integer-mult-bounds/pull/4248) proved
+9 ≤ N(4) ≤ 21 and asked for the exact value. This package shows:
+
+- **Theorem P** (proof, instance-checked): for every even c, a floor walk on k
+  sources needs 2^k − 1 ≤ P(c, k), where P counts parity sums of at most c
+  boundaries after collapsing adjacent pairs. P(4, 21) = 1,743,531 <
+  2,097,151, so **N(4) ≤ 20**. The bound also gives N(8) ≤ 54 (was 55) and
+  N(2) ≤ 5; for c = 6, 10 and 12 it gives no gain.
+- **No extension** (exhaustive finite check): none of the C(40, 4) = 91,390
+  ways to insert four events of a tenth source into #4248's nine-source walk
+  reaches all 1,023 masks. So a ten-source floor walk, if one exists, deletes
+  to no relabelling of that walk.
+
+The claims are a scoped proof plus an exhaustive finite check. There is no new
+κ, no selected-frontier change and no multiplication theorem. N(4) is still
+open in 9 ≤ N(4) ≤ 20.
+
+## 1. Interface and prefix criterion
+
+The interface and criterion are #4248's. A floor word has a source walk w of
+length ck that uses each source exactly c times. Let q_t ∈ (Z/c)^k count
+source events modulo c after t steps, for boundaries t = 0, …, ck. The word is
+correct exactly when every nonzero mask m has readout boundaries
+t_1 ≤ … ≤ t_c with
+
+```text
+q_(t_1) + ... + q_(t_c) = m   in (Z/c)^k.
+```
+
+The deletion lemma (#4232, extended by #4248 to every c) makes the set of
+attaining k an initial segment. #4248's counting bound uses the
+C(ck + c − 1, c) multisets of c boundaries and excludes k ≥ 22 at c = 4.
+
+## 2. Theorem P: a parity count for even characteristic
+
+Let c be even. Reduction Z/c → Z/2 is a ring map, so the parity vectors
+u_t = q_t mod 2 ∈ F_2^k satisfy u_(t_1) + … + u_(t_c) = m, because m is binary.
+Along the walk, u_t = u_(t−1) + e_(w_t): each step flips one bit. Also
+u_0 = u_(ck) = 0.
+
+Let T be the set of boundaries that occur an odd number of times among
+t_1, …, t_c, with 0 and ck removed. Then |T| ≤ c, T is nonempty, T lies in
+the n = ck − 1 inner boundaries, and m is the sum of u_t over T.
+
+- If T contains no two consecutive boundaries, it is one of at most
+  Σ_(i=1..c) C(n − i + 1, i) such subsets.
+- If T contains t − 1 and t, then u_(t−1) + u_t = e_(w_t), so
+  m = e_(w_t) + Σ_(r∈R) u_r with R = T \ {t − 1, t} and |R| ≤ c − 2. There are
+  at most k · Σ_(i=0..c−2) C(n, i) such values.
+
+Every nonzero mask needs a readout, so
+
+```text
+2^k − 1 ≤ P(c, k) = Σ_(i=1..c) C(ck − i, i) + k · Σ_(i=0..c−2) C(ck − 1, i).
+```
+
+At c = 4, P(4, 20) = 1,422,427 ≥ 1,048,575 but P(4, 21) = 1,743,531 <
+2,097,151. With the deletion lemma, every k ≥ 21 fails. So N(4) ≤ 20.
+
+| c | #4248 multiset bound: first excluded k | Theorem P: first excluded k |
+|---:|---:|---:|
+| 2 | 7 | 6 |
+| 4 | 22 | **21** |
+| 6 | 38 | 38 |
+| 8 | 56 | 55 |
+| 10 | 74 | 74 |
+| 12 | 93 | 93 |
+
+At c = 2 the bound is consistent with N(2) = 4, which
+[#943](../universal-connector-boundary/README.md) established. For odd c the
+reduction mod 2 is unavailable and #4248's bound stands.
+
+**Instance check.** On #4248's nine-source walk, the verifier enumerates all
+59,535 inner subsets of size at most four. Each one that contains an adjacent
+pair has a sum in the e_j-plus-two family. It then reduces all 91,390 boundary
+4-multisets mod 2 and checks that each lands in the two counted families.
+
+## 3. The nine-source walk does not extend
+
+[CERTIFICATE.json](CERTIFICATE.json) copies #4248's walk:
+
+```text
+4 2 6 4 0 8 1 7 3 2 5 2 1 7 4 3 0 2 5 8 6 5 6 4 8 3 1 0 5 7 8 7 0 3 6 1
+```
+
+The verifier re-checks all 511 masks. It then places four events of a tenth
+source at every 4-subset of the 40 positions, keeping the other events in
+order. For each of the 91,390 walks it finds a nonzero mask that no boundary
+4-multiset reaches. The sweep uses 32 distinct witness masks.
+
+Coverage is invariant under relabelling sources. If deleting some source from
+a ten-source floor walk gave a relabelling of this walk, relabelling back
+would give one of the checked insertions. So no ten-source floor walk restricts
+to this walk. This is an exhaustive check of one family, not an exclusion of
+k = 10. Insertions into other nine-source floor walks are unchecked.
+
+## 4. Reproduction
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/connector-char4-floor-bounds/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/connector-char4-floor-bounds/verify.py --skip-insertions
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-char4-floor-bounds
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-char4-floor-bounds --check-source-history
+```
+
+Expected marker:
+`PASS_CONNECTOR_CHAR4_FLOOR_BOUNDS c4_excludes_k>=21 walk9_has_no_ten_source_extension`.
+The verifier uses only the standard library. The full run takes about 25 s
+locally; `--skip-insertions` takes under a second. It prints a receipt hash
+bound to all six package files. Three mutation controls must be rejected: the
+walk with its first two events swapped, the sorted run walk, and a comparison
+that requires Theorem P to be strictly tighter than the multiset count at
+k = 22.
+
+## 5. Limitations
+
+The result covers only the unsigned, immutable-source, complete-call interface
+of #4231. Theorem P is proved for every even c and checked numerically for
+c ≤ 12, k ≤ 200. The extension check covers one nine-source walk. Input
+admission, coefficient preparation, dispatch and physical costs are unknown.
+No consumer is instantiated. Proof-kernel checks and independent human review
+are not claimed.
+
+## Open next questions
+
+These are recorded with first steps in [TASK.json](TASK.json).
+
+1. What is N(4) exactly, within 9 ≤ N(4) ≤ 20? A ten-source floor walk
+   restricts to ten nine-source floor walks, none a relabelling of the known
+   one. Generating inequivalent nine-source walks and running the same sweep is
+   the natural next step.
+2. Can the carry condition give a much smaller bound? Write each stage as
+   u + 2h with u, h ∈ {0, 1}. A mask also needs Σh + e_2(u) = 0 over F_2 in
+   every coordinate, where e_2 is the second elementary symmetric function of
+   the four parity bits. Heuristically this removes a 2^−k fraction of
+   multisets, but the k conditions are not independent.
+3. Does any concrete consumer use a characteristic-four batch of more than four
+   sources at a favourable complete invoice?
+
+## Credit
+
+Produced by Nick Petalas. The interface and the floor c(k + 2^k − 1) are
+#4231's. The nine-source walk, the every-c deletion lemma and the multiset
+bound are #4248's; the deletion lemma and counting idea extend #4232's F3
+versions. The connector interface and prefix-boundary readout criterion come
+from Ross Richardson's [#943](../universal-connector-boundary/README.md).
+Apache-2.0.

research/connector-char4-floor-bounds/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}

research/connector-char4-floor-bounds/TASK.json

@@ -0,0 +1,86 @@
+{
+  "schema_version": 1,
+  "task_id": "connector-alphabet-change",
+  "priority_revision": 7,
+  "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+  "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": "For the unsigned dirty connector of PR4231 over a ring of characteristic four (k immutable sources, all 2^k-1 nonzero binary-mask outputs, calls B_j: z += B_j x_j and A_m: y_m += A_m z), bound N(4), the largest k at which the floor 4(k+2^k-1) is attained. Lowers PR4248's upper bound 21 to 20 by a parity counting argument valid for every even characteristic, and shows that PR4248's nine-source walk has no ten-source extension.",
+  "scope_change_reason": "Keeps the PR4231 alphabet and studies the source count, which the card lists as a scope-change trigger. PR4248 left N(4) open between 9 and 21; the floor is the premise any larger-batch consumer of that alphabet would rely on.",
+  "bottleneck_link": "Side result: bounds the batch size at which a characteristic-four connector consumer can pay exactly four calls per operator. No physical consumer, admission or transfer is supplied, so no kappa change follows.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the parity counting bound, its instance check and the exhaustive extension check of the certified nine-source walk. Do not start an unbounded search for other nine-source walks.",
+  "outcome": "completed",
+  "evidence": "verify.py re-checks all 511 masks of the PR4248 nine-source walk, checks the parity collapse lemma on all 59,535 inner boundary subsets of size at most four of that walk and all 91,390 boundary 4-multisets, tabulates both counting thresholds for c <= 12 and k <= 200, and checks all C(40,4) = 91,390 insertions of a tenth source, each with an explicit uncovered mask. Three mutation controls must be rejected.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is N(4) exactly, now known to satisfy 9 <= N(4) <= 20?",
+      "why_it_matters": "It is the largest batch on which the characteristic-four connector pays exactly four calls per operator.",
+      "first_step": "A ten-source floor walk restricts to ten nine-source floor walks, none equal to the PR4248 walk up to relabelling. Generate many inequivalent nine-source floor walks and run the same insertion check on each.",
+      "blocked_by": "Only one nine-source floor walk is known; the space of 36-event walks is too large to enumerate."
+    },
+    {
+      "question": "Can the quadratic carry condition give a counting bound far below 20?",
+      "why_it_matters": "Parity uses only the low bit of each coordinate. Writing each stage as u + 2h, a mask also needs sum(h) + e2(u) = 0 over F2 in every coordinate, which heuristically removes a 2^-k fraction of multisets.",
+      "first_step": "Bound the number of 4-subsets of the parity path satisfying the carry condition for one fixed coordinate, then combine coordinates.",
+      "blocked_by": "The k carry conditions are not independent; no rigorous bound is proved."
+    },
+    {
+      "question": "Does any concrete consumer use a characteristic-four batch of more than four sources at a favorable complete invoice?",
+      "why_it_matters": "The abstract call counts change no recursive supplier or kappa by themselves.",
+      "first_step": "Identify an immutable-source, unobserved-output caller with coefficients of characteristic four and price every primitive, admission and dispatch.",
+      "blocked_by": "No selected-supplier consumer is instantiated."
+    }
+  ],
+  "predecessor_handoff": {
+    "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4248",
+    "head": "e7df122403cfc2febfb6799abb821487d8d1ee49",
+    "author": "Nick Petalas",
+    "usage": "Nine-source walk, prefix criterion, deletion lemma and the multiset bound N(4) <= 21; open question 1 is narrowed here. The walk is copied into CERTIFICATE.json; no executable dependency."
+  },
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19082839",
+    "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244",
+    "overlap_scope": "100 live open PR titles, 60 recent account PRs, last 30 handoff comments, merged PR search for characteristic-four connector terms, merged README grep. PR4248, PR4231, PR4232 and PR4250 are the related packages. Closed work and arbitrary diffs are incompletely covered.",
+    "family_decision": "Local interface result; stop. No construction round is justified without a consumer."
+  }
+}

research/connector-char4-floor-bounds/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "Nine-source walk coverage; parity collapse lemma on that walk; counting thresholds for c<=12; all 91,390 tenth-source insertions each with an uncovered mask; three rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py",
+        "--skip-insertions"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat every check except the insertion sweep under optimized Python; checks use explicit exceptions."
+    }
+  ]
+}