[petalas]

Result

Exact shortest unsigned word for a dirty connector chained through two dirty intermediates, over every coefficient characteristic. The calls are z1 += B1 x, z2 += B2 z1 and y += B3 z2. The source x is immutable, z1, z2 and y start dirty, and the maps are arbitrary. Coefficients lie in a nonzero unital ring of characteristic m. The word must restore z1 and z2 and add c B3 B2 B1 x to y:

shortest length = 3m  for every m >= 2 and c != 0 (mod m),
                        except (m, c) = (2, 1), (3, 2), (4, 3): 4m.

Claim type: scoped proof for all m, with a finite certificate for characteristics 2 to 4 and for one sporadic witness at (6, 5). The depth-four table is a finite certificate only. No new κ, supplier admission or selected-frontier change.

• Lemma 1 reduces correctness to interval subword counts N[i..j] mod m. Equivalently, the positive-generator product in UT4(Z/m) must equal I + c e_{1,4}.
• Lemma 2: each call count is a positive multiple of m, so the floor is 3m and every length is a multiple of m.
• Lemma 3 gives an explicit 3m word for every m >= 5 except (6, 5): 1^a 2 3^t 1^(m-2a) 2 1^a 2^(m-t-2) 3 2^t 3^(m-t-1) with ta ≡ c. The proof is a written all-m computation.
• Lemma 4: at m = 2, 3, 4 an exhaustive census of balanced words shows that c ≡ -1 is unreachable in 3m calls. Explicit 4m words attain it.
• Depth four: the per-call floor 4m fails. The exact minima are 12, 18 and 20 calls at m = 2, 3, 4 (registered), and 25 at m = 5 (opt-in local run).

Only research/depth3-chain-connector/ is added, on base 12fa8c5c844be21bfefb38a19503fbd867a11244 (priority revision 7, card connector-alphabet-change, scope explicitly changed in TASK.json).

Evidence and reproduction

From the repository root:

/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 -O -W error -B research/depth3-chain-connector/verify.py
/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
# opt-in, not registered:
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth3-chain-connector/verify.py --depth4-m5

Locally, on CPython 3.12.15 / macOS arm64, both registered commands print PASS_DEPTH3_CHAIN_CONNECTOR depth4_moduli=3 constructed=32634 with a generated receipt bound to every package/input SHA-256. Each takes about 12 s of CPU. PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES pass. The checks cover:

• exact BFS minima over all of UT4(Z/m) for 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;
• the explicit word for all 32,634 pairs (m, c) with 5 <= m <= 256;
• literal noncommuting dirty replay, 1,972 cases;
• exact depth-four BFS minima at m = 2, 3, 4;
• six rejection controls.

The opt-in --depth4-m5 verifier run passed locally (PASS_DEPTH3_CHAIN_CONNECTOR depth4_moduli=4, depth-four minima [25,25,25,25] at m = 5, 202 s wall, 88 s CPU). It runs an exhaustive BFS over all 9,765,625 states of UT5(Z/5). CI does not run it.

Limitations and unrun obligations

The all-m statement is a written proof. The verifier checks the construction only through m = 256 and the floor/exceptions by exhaustive search for m <= 8. Independent human and formal proof-kernel review are unclaimed. No depth-four all-m law is claimed. All calls carry complete implementation prices. Admission, dispatch, routing of the two intermediates, precision, supplier caller and the outer multiplication theorem are not supplied.

Open next questions

1. What is the exact depth-four minimum in every characteristic? The floor 4m fails for m <= 5. Plain search has m^10 states, so m >= 6 needs a quotient or meet-in-the-middle search, or a three-slope extension of Lemma 3.
2. Does any concrete recursive caller route through two dirty intermediates with a favorable complete invoice for these 3m calls?

Related open work

• Count optimal unsigned one-source connector words in every characteristic #4236 counts optimal words for the depth-two (one-source) chain. That chain is this one with one call fewer. Its 2m floor is consistent with Lemma 2 at depth two, and no identical quantity is shared.
• Classify the unsigned five-source connector in every characteristic (36c for c ≥ 3; no new κ) #4231 classifies the unsigned five-source connector by characteristic and gives the one-source 2m floor. It has a different target, and no overlapping number.
• Construction: three-stage persistent prefix shear chain (no new kappa) #1930 builds a three-stage chain with clean targets and no dirty restoration. It is a different contract: it calls each map once and no restoration count applies.
• Bound the unsigned F3 connector floor for every source count: attained for n ≤ 6, impossible for n ≥ 14 (no new κ) #4232, Prove the exact 744-call F3 optimum for full ternary five-source demand #4238 and Prove the exact signed connector tariff with sign-dependent prices (no new κ) #4241 study unsigned F3 multi-source and signed connectors. They have different interfaces, and no overlapping quantity.
• Merged Research: UT4 central-target tariff bound with arbitrary dirty workspace #1662 (research/ut4-central-tariff-relaxation) prices the binary UT4 one-target case at exactly eight calls in a broader workspace model. This agrees numerically with the m = 2 exception here (8 = 4m).

CI notes

Hosted CI is green on head 03b8a19d7442edebb3565064631f6ca2408d731e: run 39494609297. plan passed in 3m10s and the package replay passed in 2m37s. No check failed.

Produced by Nick Petalas. Predecessor credit: Ross Richardson's #943/#934 connector lineage, the #1662 UT4 lineage, and #4231/#4236. Apache-2.0.

[rcfc-jreed]

Independent scoped audit of #4249 depth-3 chain connector at 03b8a19d: 9/9

Code-disjoint local fork. Head 03b8a19d7442edebb3565064631f6ca2408d731e. CLAIM.

No packaging defect. PASS_DEPTH3_CHAIN_CONNECTOR. Pins + SOURCES digests; fork rc=0.

Finite replay ≠ formal proof. James Reed (@rcfc-jreed), with substantial AI assistance (Claude, in Cursor).