[petalas]

Result

Exact call-count classification and unequal-price tariff for the unsigned depth-four dirty chain connector in characteristics 2 to 5, for every nonzero target residue and for words of any length.

The calls are z_l += B_l z_{l-1} for l = 1..4. The source x = z_0 is immutable, z_1..z_3 and y = z_4 start dirty, and the maps are arbitrary. A correct word restores z_1..z_3 and adds c B4B3B2B1 x to y. A count vector (n1,n2,n3,n4) is feasible if and only if every n_l is a multiple of m and it dominates a member of

m = 2:  {(2,4,4,2)}
m = 3:  {(3,3,9,3), (3,6,6,3), (3,9,3,3)}
m = 4:  {(4,4,8,4), (4,8,4,4)}
m = 5:  {(10,5,5,5), (5,10,5,5), (5,5,10,5), (5,5,5,10)}

The set does not depend on c. With positive complete-call prices and S = p1+p2+p3+p4, the cheapest bill is

m = 2:  2S + 2(p2 + p3)
m = 3:  3S + 6 min(p2, p3)
m = 4:  4S + 4 min(p2, p3)
m = 5:  5S + 5 min(p1, p2, p3, p4)

At unit prices these are #4249's lengths 12, 18, 20, 25. What is new is where the premium sits. At m = 2, 3, 4 it falls only on the two middle operations: no minimal word doubles the first or last call, however cheap those calls are. At m = 5 any one call can be doubled. For 6 <= m <= 32 the bill is mS, a corollary of #4263's balanced witnesses (cited, not rechecked).

Claim type: scoped proof whose completeness step is a finite reduction checked by computer, plus a finite certificate for each witness. No new κ, no supplier admission and no selected-frontier change.

The key step: a 1 matters only through which 2s follow it, and a 4 only through which 3s precede it. So every interval count is a function of the order of the 2s and 3s, the prefix counts u of 1s and the suffix counts r of 4s, with N14 = u'Ar for the precedence matrix A. Leaving n1 and n4 free lets u and r range over all residue vectors. At m = 3, 4 that relaxation reaches no nonzero target on any middle pair the Pareto set misses. This covers words of every length. m = 2 has a short hand proof (two 2s force N14 = u1·N24 = 0), and m = 5 needs only the exact exclusion of (5,5,5,5).

Only research/depth4-chain-tariff/ 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/depth4-chain-tariff/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/depth4-chain-tariff/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth4-chain-tariff
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth4-chain-tariff --check-source-history

Locally (CPython 3.12, macOS arm64), both registered commands print PASS_DEPTH4_CHAIN_TARIFF witnesses=29 replays=87 box_comparisons=125 cross_checks=116 receipt_sha256=42f5bef2… in about 57 s each. The receipt is generated and bound to every package file and source input hash. PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES pass.

The verifier is standard-library only. It checks:

• all 29 witnesses (one per m, c and Pareto vector): counts, the ten interval conditions, an independent UT5(Z/m) product, and three literal dirty replays each with random noncommuting 2x2 maps;
• the relaxed engine on every missed middle pair at m = 3, 4, with positive controls on the adjacent feasible pairs;
• the exact engine at (5,5,5,5), plus a control showing why the relaxation is not enough at m = 5;
• the m = 2 lemma on a box, and the mirror symmetry;
• a second engine (direct DP over interval residues), which matches the claimed cone in all 125 box cases and matches the reduction engine in the 116 cases with every count at most 6;
• five negative or positive controls.

The witnesses came from a seeded local annealing search that is not packaged. The verifier checks the words themselves.

Limitations and unrun obligations

Only m = 2..5 is proved. The mS corollary for larger m is a cited statement: #4263 (open, not rechecked) covers 6 <= m <= 32 and #4280 (open, not rechecked) covers 33 <= m <= 64, so it extends to 6 <= m <= 64. m >= 65 remains open. Word multiplicities at the Pareto vectors are not counted. Independent human and formal proof-kernel review are unclaimed. Every call carries its complete price. Admission, dispatch, routing of the three dirty intermediates, precision, stock, supplier caller and the outer multiplication theorem are not supplied.

Open next questions

1. What is the Pareto set for m >= 33? It is {(m,m,m,m)} exactly when the balanced vector is feasible.
2. How many words attain each Pareto vector? A counting DP at length 25 needs a sparser state encoding to fit CI.
3. Which operations carry the premium at depth five? The same middle-letter reduction applies with three inner letters bounded.
4. Can a concrete recursive caller with three dirty intermediates use one of these profiles at a favorable complete physical cost?

Related open work

• Prove the shortest unsigned depth-three chain connector in every characteristic (3m; 4m at c ≡ -1 for m ≤ 4; no new κ) #4249 is the depth-three chain law and the source of the model and of the depth-four minimum lengths. Overlap checked: the unit-price tariffs here give 12, 18, 20, 25 at m = 2..5, matching Prove the shortest unsigned depth-three chain connector in every characteristic (3m; 4m at c ≡ -1 for m ≤ 4; no new κ) #4249's table for every c.
• Classify all depth-three connector count vectors and unequal-price optima #4257 is the depth-three count classification. Its divisibility and padding arguments are reused. It is one level shorter and shares no number.
• Attain the depth-four chain connector floor 4m for every 6 ≤ m ≤ 32 (no new κ) #4263 attains 4m at depth four for 6 <= m <= 32. It is used only for the cited mS corollary; its m range does not overlap the m = 2..5 proved here.
• Attain the depth-four chain connector floor 4m for every 33 ≤ m ≤ 64, via an exact row model (no new κ) #4280 attains 4m at depth four for every 33 <= m <= 64 (1,520 witnesses) and adds a row-model lemma. Same object. Its enumeration of every row-model record at m = 2..5 finds no balanced word with nonzero c, which agrees with the minimum lengths 12, 18, 20, 25 and with the exclusion of (m,m,m,m) here. With Attain the depth-four chain connector floor 4m for every 6 ≤ m ≤ 32 (no new κ) #4263 it extends the cited mS corollary to 6 <= m <= 64; not rechecked here.

CI notes

Hosted CI is green on head bb56c7c1681a743acb6eeb9057563211a8498905: run 39525253988. plan passed in 2m43s and the package replay in 7m12s. No check failed. Locally each registered command takes about 1 minute.

Produced by Nick Petalas. Predecessor credit: #4249, #4257, #4263 and Ross Richardson's #943/#934 connector lineage. Apache-2.0.