[petalas]

Result

The shortest unsigned depth-four dirty chain connector has exactly 4m calls for every characteristic 33 <= m <= 64 and every nonzero c. This extends open question 1 of #4263, which covered 6 <= m <= 32.

• Finite certificate: one witness for each of the 1,520 pairs (m, c), 33 <= m <= 64, 1 <= c < m. Each uses every call exactly m times, which meets the floor of Prove the shortest unsigned depth-three chain connector in every characteristic (3m; 4m at c ≡ -1 for m ≤ 4; no new κ) #4249.
• Scoped proof (README Lemma 2), all m: a balanced word is fixed by a partition λ in the m × m box (from the 2/3 subword) and two monotone profiles ρ, β (from the levels of calls 1 and 4). The word is correct for c iff five sums vanish mod m and Σ_q ρ(q) B(ℓ(q)) ≡ −c. Full rows drop out, so each witness is a short record: one full row and three to five short rows.
• Scoped proof (README Lemma 3): for prime m, two short rows force c ≡ 0, so at least three are needed.

With #4249 (m <= 5) and #4263 (6..32), both open and not rechecked here, the depth-four minimum is known for 2 <= m <= 64. No all-m theorem, no new κ, no supplier admission and no change to the selected frontier.

Evidence and reproduction

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/depth4-chain-rowmodel/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/depth4-chain-rowmodel/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/depth4-chain-rowmodel
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/depth4-chain-rowmodel --check-source-history

Any CPython 3.12 works. Local results at cf55a41: both verifier modes print PASS_DEPTH4_CHAIN_ROWMODEL moduli=32 witnesses=1520 in about 0.5 s each; PASS_REGISTERED_RESEARCH_PACKAGE; PASS_RESEARCH_COMMIT_BYTES.

For every record the verifier checks the Lemma 2 sums, then builds the word and checks it independently: exactly m copies of each call, the interval subword counts, the UT5(Z/m) product, and one literal replay with dirty registers in (Z/m)^2 and random noncommuting 2x2 maps. It also checks Lemma 2 against direct counting on 4,000 random records (691 of them correct words), Lemma 3 on 173 non-vacuous random records, and five rejection controls.

Limitations

• A finite certificate for 33 <= m <= 64 only. A uniform all-m family was searched for and not found; the README records the designs that failed.
• Lemmas 2 and 3 are proved in the README and spot-checked by the verifier; independent human and formal proof-kernel review are unclaimed.
• Admission, dispatch, routing of the three intermediates and physical costs are unpriced. No caller, precision analysis or κ change.

Open next questions

1. Is the depth-four minimum 4m for every m >= 6? Lemma 2 reduces this to choosing one partition and two profiles; the blocking constraint is the budget ρ(1) <= m and at most m calls 4.
2. Are three short rows enough for every prime m >= 7? (436 of the 1,520 witnesses use three.)
3. Does a row model of the same kind give the floor 5m at depth five?

Related open work

• Attain the depth-four chain connector floor 4m for every 6 ≤ m ≤ 32 (no new κ) #4263: same object, 6 <= m <= 32. Disjoint m range, same 4m law; this package continues its open question 1. No overlapping number to compare.
• Prove the shortest unsigned depth-three chain connector in every characteristic (3m; 4m at c ≡ -1 for m ≤ 4; no new κ) #4249: depth-three law and depth-four m <= 5 minima. Disjoint m range; this package uses its floor lemma only.
• Classify all depth-three connector count vectors and unequal-price optima #4257: depth-three count vectors and unequal prices. Different depth; no overlapping number.
• Classify depth-four chain connector count vectors and unequal-price tariffs for m = 2..5 (no new κ) #4279: same depth-four object, exact count vectors and unequal-price tariffs for m = 2..5. Disjoint m range from this certificate. Its open question 1 (Pareto set for m >= 33) is answered here for 33 <= m <= 64: since every count is a positive multiple of m (Lemma 1) and (m,m,m,m) is feasible, the Pareto set is {(m,m,m,m)} and the tariff is mS. Overlap checked numerically: enumerating all 216, 8000, 343000 and 16,003,008 row-model records (λ, ρ, β) at m = 2, 3, 4, 5, Lemma 2 admits no balanced word for any nonzero c. This agrees with Classify depth-four chain connector count vectors and unequal-price tariffs for m = 2..5 (no new κ) #4279's Pareto sets, none of which contains (m,m,m,m), and with its unit-price minima 12, 18, 20, 25, each above 4m. This local check is not packaged.

Credit

Produced by Nick Petalas. The chain model, floor and m <= 5 minima are from #4249; the 6..32 witnesses and three-interleaving lemma are from #4263; the complete-call interface is from Ross Richardson's #943/#934 lineage.

CI notes

Both checks passed on head cf55a41: plan and replay (research/depth4-chain-rowmodel), run https://github.com/CrocSwap/integer-mult-bounds/actions/runs/39525299145 (replay job 1m18s).