Prove the shortest unsigned depth-three chain connector in every characteristic (3m; 4m at c ≡ -1 for m ≤ 4; no new κ)

research/depth3-chain-connector/PROOF.md

@@ -0,0 +1,107 @@
+# Proof: shortest unsigned depth-three chain connector
+
+## Setting
+
+Let R be a nonzero unital ring of exact characteristic m >= 2. Registers
+x = z_0 (immutable), z_1, z_2 and y = z_3 hold arbitrary initial (dirty)
+values z_j^0 in R-modules M_0, ..., M_3. The R-linear maps B_l: M_{l-1} -> M_l
+are arbitrary. The only operations are the complete calls
+
+```text
+l = 1, 2, 3:   z_l += B_l z_{l-1}
+```
+
+with no sign or inverse calls. A word w over {1, 2, 3} is *correct for c*
+when, for every choice of modules, maps and dirty data, it ends with z_1, z_2
+restored and y = y^0 + c B_3 B_2 B_1 x. For an interval 1 <= i <= j <= 3 let
+N_w[i..j] be the number of increasing position tuples p_i < ... < p_j with
+letter l at position p_l (scattered occurrences of the subword i(i+1)...j).
+
+**Lemma 1 (action).** After w,
+z_j = z_j^0 + sum_{i <= j} N_w[i..j] B_j ... B_i z_{i-1}^0.
+
+*Proof.* Induction on appending letter l. Only z_l changes, by
+B_l z_{l-1} = B_l z_{l-1}^0 + sum_{i < l} N[i..l-1] B_l ... B_i z_{i-1}^0.
+That is N[l..l] += 1 and N[i..l] += N[i..l-1], the recurrence for subword
+occurrences ending at the new letter. ∎
+
+**Corollary.** w is correct for c iff N_w[i..j] ≡ 0 (mod m) for every
+interval except N_w[1..3] ≡ c (mod m).
+
+Sufficiency is Lemma 1. For necessity take M_l = R and every B_l = 1. Put
+z_{i-1}^0 = 1 and every other initial value 0. Then z_j changes by N_w[i..j]·1,
+which is zero iff m divides N_w[i..j], because the characteristic is m. The
+same instance with x = 1 gives y - y^0 = N_w[1..3]·1 = c·1. ∎
+
+Equivalently, the product of the elementary unipotents I + e_{l,l+1} in
+UT_4(Z/m) must equal I + c e_{1,4}. This group form is also how the verifier
+runs its exact search.
+
+## Theorem
+
+For every m >= 2 and c ≢ 0 (mod m), the shortest correct word has length 3m,
+except (m, c) = (2, 1), (3, 2) and (4, 3), where it has length 4m. With no
+finite characteristic no unsigned word is correct for any nonzero c.
+
+**Lemma 2 (floor).** Each letter count n_l = N[l..l] is a positive multiple of
+m. Hence every correct word has length a multiple of m and at least 3m.
+
+*Proof.* n_l ≡ 0 by the Corollary. If some n_l = 0 then N[1..3] = 0 ≢ c. In
+characteristic zero n_l = 0 is forced, which is the last claim. ∎
+
+**Lemma 3 (construction).** Let m >= 5 with (m, c) ≠ (6, 5). Choose
+
+- a = 1, t = c if 1 <= c <= m - 2;
+- for c = m - 1, a unit a of Z/m in [2, floor(m/2)] and t = -a^{-1} mod m.
+
+Such a exists: a = 2 for odd m >= 5; a = m/2 - 1 when 4 | m and m >= 8 (odd,
+and gcd(a, m) divides m - 2a = 2); a = m/2 - 2 when m ≡ 2 (mod 4) and m >= 10
+(odd, and gcd(a, m) divides m - 2a = 4). Then t ≠ 0, and t ≠ m - 1 because
+a ≢ 1. So 1 <= t <= m - 2 and 1 <= a <= m/2 in both cases. The word
+
+```text
+W = 1^a 2 3^t 1^(m-2a) 2 1^a 2^(m-t-2) 3 2^t 3^(m-t-1)
+```
+
+has m copies of each letter and is correct for c ≡ ta.
+
+*Proof.* Track (N[1..2], N[2..3], N[1..3]) through the blocks. The first 2
+sees a ones: N12 = a. The block 3^t sees one 2 and N12 = a, adding t to N23 and
+ta to N123. The second 2 sees m - a ones: N12 = m. The block 2^(m-t-2) sees m
+ones: N12 = m(m - t - 1). The lone 3 sees m - t twos, so N23 = m, and adds
+N12, which is ≡ 0. The block 2^t adds mt, so N12 = m(m - 1). The final
+3^(m-t-1) sees m twos and N12 ≡ 0. The totals are N12 = m(m - 1) ≡ 0,
+N23 = m(m - t) ≡ 0 and N123 ≡ ta ≡ c. The letter counts are
+a + (m - 2a) + a, 1 + 1 + (m - t - 2) + t and t + 1 + (m - t - 1). ∎
+
+The remaining case (m, c) = (6, 5) uses the explicit 18-call word
+`111122133232123233`, checked by the verifier.
+
+**Lemma 4 (small characteristic).** For m in {2, 3, 4}, a 3m-letter correct
+word has n_1 = n_2 = n_3 = m by Lemma 2. The verifier enumerates all
+90, 1,680 and 34,650 such words. The attained N[1..3] residues among words
+whose other intervals vanish are {0}, {0, 1} and {0, 1, 2}. So 3m is attained
+for every c except c ≡ -1, and the next admissible length is 4m by Lemma 2.
+These explicit words attain it:
+
+```text
+m = 2, c = 1:  12321232
+m = 3, c = 2:  112113211323
+m = 4, c = 3:  1112111321213233
+```
+
+Lemmas 2 to 4 prove the Theorem. An exact breadth-first search over the
+whole of UT_4(Z/m), m = 2, ..., 8, confirms every minimum independently. ∎
+
+## Depth four (finite certificate only)
+
+The same Corollary holds for any chain depth k. Lemma 2 gives the floor km and
+lengths that are multiples of m. Exact breadth-first search over UT_5(Z/m)
+gives these minima, equal for every nonzero c:
+
+| m | 2 | 3 | 4 | 5 (opt-in run) |
+|---|---|---|---|---|
+| minimum | 12 = 6m | 18 = 6m | 20 = 5m | 25 = 5m |
+
+So the per-letter floor 4m fails at depth four for m <= 5. No all-m depth-four
+statement is claimed.

research/depth3-chain-connector/README.md

@@ -0,0 +1,106 @@
+# Shortest unsigned depth-three chain connector
+
+This scoped proof gives the exact shortest word for an unsigned dirty
+connector chained through two dirty intermediates, over every finite
+characteristic. The contribution was produced by Nick Petalas.
+
+The complete calls are `z1 += B1 x`, `z2 += B2 z1` and `y += B3 z2`. The source
+x is immutable, z1, z2 and y start with arbitrary dirty data, and the maps are
+arbitrary. Coefficients lie in a nonzero unital ring of exact characteristic m.
+For a nonzero residue c the word must restore z1 and z2 and add
+`c B3 B2 B1 x` to y.
+
+```text
+shortest length = 3m   for every m >= 2 and c != 0 (mod m),
+                         except (m, c) = (2, 1), (3, 2), (4, 3): 4m.
+```
+
+Each call is used a positive multiple of m times, so 3m is the per-call floor.
+For m >= 5 an explicit word attains it, with one exception handled by a checked
+witness at (m, c) = (6, 5):
+
+```text
+1^a 2 3^t 1^(m-2a) 2 1^a 2^(m-t-2) 3 2^t 3^(m-t-1),   ta ≡ c (mod m)
+```
+
+Here a = 1, t = c when c <= m - 2. For c = m - 1, a is a unit of Z/m in
+[2, m/2] and t = -1/a. In characteristic 2, 3 and 4 the target c ≡ -1 cannot
+be reached with m calls of each kind, and costs 4m. The binary case agrees with
+the eight-call one-target count in [#1662](../ut4-central-tariff-relaxation/README.md).
+That package uses a broader workspace model. Over characteristic zero, no
+unsigned word reaches any nonzero c.
+
+The per-call floor does **not** extend to depth four. Exact search over the
+four-call chain gives 12, 18, 20 and 25 calls at m = 2, 3, 4 and 5. The floor
+4m would give 8, 12, 16 and 20.
+
+[PROOF.md](PROOF.md) has the complete argument. Lemma 1 reduces correctness to
+interval subword counts mod m. Lemma 2 proves the floor, Lemma 3 is the
+all-m construction, and Lemma 4 settles characteristics 2 to 4 by finite
+enumeration. The depth-four table is a finite certificate only.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth3-chain-connector/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth3-chain-connector/verify.py --depth4-m5
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth3-chain-connector
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth3-chain-connector --check-source-history
+```
+
+Any CPython 3.12 can replace the local interpreter path. The default run
+prints a generated JSON receipt with every package and input SHA-256, then
+`PASS_DEPTH3_CHAIN_CONNECTOR depth4_moduli=3 constructed=32634`. It writes no
+files and takes about 12 seconds locally. The `--depth4-m5` flag adds the
+9,765,625-state depth-four search at m = 5. It is opt-in and not registered,
+because it takes much longer and needs more memory.
+
+The default checks:
+
+- Exact breadth-first minima over all of UT4(Z/m), m = 2 to 8, for every c.
+- An independent census of all 90, 1,680 and 34,650 balanced words at
+  m = 2, 3, 4, and the three 4m exception witnesses.
+- The explicit word for all 32,634 pairs (m, c) with 5 <= m <= 256, checked
+  for letter counts and every interval condition.
+- Literal replay with noncommuting 2x2 maps and dirty registers for every
+  constructed word through m = 32, and for the exception witnesses.
+- Exact depth-four minima at m = 2, 3, 4.
+- Six controls: an omitted readout, an adjacent transposition, a wrong
+  coefficient, a moved middle call, a reversed factor order and the
+  construction's domain guard.
+
+## Attribution and scope
+
+Ross Richardson's [#943/#934 lineage](../universal-connector-boundary/README.md)
+supplies the complete-call dirty-connector interface. The depth-two
+(one-source) chain and its 2m floor come from
+[#4231](https://github.com/CrocSwap/integer-mult-bounds/pull/4231) and
+[#4236](https://github.com/CrocSwap/integer-mult-bounds/pull/4236). The UT4
+central-target line, [#1662](../ut4-central-tariff-relaxation/README.md) and
+its credited lineage, already prices the binary case in a broader model. The
+new results here are the all-characteristic depth-three law, its construction,
+the c ≡ -1 exceptions and the depth-four table. Subword counts and unitriangular
+matrices are classical tools; no novelty is claimed for them. No pending
+executable or archived source is imported. Exact pins are in
+[SOURCES.json](SOURCES.json).
+
+The `connector-alphabet-change` card is explicitly changed to this side
+question. The chain gets one more complete call; the operations stay
+unsigned, and no new connector operation is added. All calls carry their
+complete implementation prices. Admission, dispatch, routing of the two
+intermediates and word-dependent physical costs are additional. No supplier
+caller, precision analysis, outer multiplication theorem, formal-kernel proof
+or new kappa is supplied. Independent human and formal proof-kernel review are
+unclaimed. Apache-2.0.
+
+## Open next questions
+
+The structured questions in [TASK.json](TASK.json) give first steps and blockers.
+
+1. What is the exact depth-four minimum in every characteristic? The floor 4m
+   fails for m <= 5. Whether it returns for large m is open, and plain search
+   has m^10 states.
+2. Does any concrete recursive caller route through two dirty intermediates
+   with a favorable complete invoice for these 3m calls?

research/depth3-chain-connector/SOURCES.json

@@ -0,0 +1,50 @@
+{
+  "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"
+    },
+    {
+      "path": "research/universal-connector-boundary/README.md",
+      "usage": "input",
+      "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f",
+      "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476"
+    },
+    {
+      "path": "research/ut4-central-tariff-relaxation/README.md",
+      "usage": "provenance",
+      "git_blob": "0aae28e488f3c78f3fe9c7396805eadec2726d64",
+      "sha256": "fac91d697e04ca63c0b3830bbe50fd61df7bc932ece12d22fe602647dfc6c7ca"
+    }
+  ],
+  "context_only": [
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4236",
+      "head_commit": "bd9b426837cddd37338dd284e49cc2303de57ca0",
+      "credit": "Nick Petalas",
+      "role": "Depth-two (one-source) unsigned connector: 2m floor and optimal-word counts. This package extends the chain by one call; no executable dependency."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4231",
+      "head_commit": "8a956cbc80dc55697fd3e214812ce567b5eca48f",
+      "credit": "Nick Petalas",
+      "role": "Unsigned connector over coefficient rings of every characteristic, including the one-source 2m floor; no executable dependency."
+    },
+    {
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1662",
+      "head_commit": "56210cdfdac844145b023a74e19663e757b915ff",
+      "credit": "ToikY and the lineage credited in research/ut4-central-tariff-relaxation",
+      "role": "Binary UT4 central-target tariff with arbitrary dirty workspace; one target needs exactly eight calls. Agrees with the m=2 exception here; no executable dependency."
+    }
+  ]
+}

research/depth3-chain-connector/TASK.json

@@ -0,0 +1,68 @@
+{
+  "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": "Prove the exact shortest unsigned word for the depth-three dirty chain connector z1 += B1 x, z2 += B2 z1, y += B3 z2 over every characteristic m >= 2 and every nonzero target residue c: 3m calls, except 4m at (m,c) = (2,1), (3,2), (4,3). Record exact depth-four minima for m = 2, 3, 4 (and m = 5 as an opt-in run).",
+  "scope_change_reason": "The live handoffs assign multi-source, F3 census and signed-ring connector questions elsewhere. This self-contained side question lengthens the one-source chain by one complete call instead of increasing the source count, and asks whether the per-letter floor km survives at depth three. It does not extend a source-count census or claim a supplier improvement.",
+  "bottleneck_link": "A recursive boundary that routes through two dirty intermediates pays this exact call count. The result shows when the naive per-call floor is attained and that it fails at depth four in small characteristic. No selected consumer is supplied; this is a scheduling side result, not a paid-profile or kappa gain.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish one uniform depth-three proof with exact finite exception certificates, bounded depth-four searches, literal dirty replay and source-bound publication checks; no depth-four all-m theorem or supplier construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the reduction to interval subword counts, the 3m floor, the explicit all-m construction and the finite exception argument. verify.py checks exact UT4(Z/m) breadth-first minima, an independent balanced-word census, every constructed word through m=256, literal noncommuting dirty replay and controls, with a generated source-hash receipt.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the exact depth-four minimum for every characteristic m?",
+      "why_it_matters": "The per-letter floor 4m fails for m = 2..5 (12, 18, 20, 25 calls). Whether it returns for large m decides whether deeper dirty chains pay a fixed or growing premium over one call per level per unit of characteristic.",
+      "first_step": "Extend the cut-point construction of Lemma 3 to a 1-2-3 skeleton with three slopes and test it against exact UT5(Z/m) search at m = 6 and 7.",
+      "blocked_by": "Plain breadth-first search over UT5(Z/m) has m^10 states; m >= 6 needs a quotient or meet-in-the-middle search."
+    },
+    {
+      "question": "Can a concrete recursive caller use a depth-three chain with a favorable complete invoice?",
+      "why_it_matters": "The call count is exact, but admission, dispatch and routing of two dirty intermediates are unpriced.",
+      "first_step": "Locate one pinned caller that composes three complete calls through dirty workspace and price all 3m calls plus its frame changes.",
+      "blocked_by": "No selected-supplier caller is bound here."
+    }
+  ]
+}

research/depth3-chain-connector/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/universal-connector-boundary/README.md"
+  ],
+  "commands": [
+    {
+      "argv": ["{python}", "-W", "error", "-B", "{package}/verify.py"],
+      "timeout_seconds": 240,
+      "checks": "Exact UT4(Z/m) BFS minima for m=2..8; independent balanced-word census for m=2,3,4; explicit 3m construction for every residue at m=5..256; exception witnesses; literal dirty noncommuting replay through m=32; exact depth-four BFS minima for m=2,3,4; six controls; source hashes."
+    },
+    {
+      "argv": ["{python}", "-O", "-W", "error", "-B", "{package}/verify.py"],
+      "timeout_seconds": 240,
+      "checks": "The same scientific checks with Python assertions disabled; all contracts use explicit exceptions."
+    }
+  ]
+}