The elementary Andrews–Curtis bottleneck of the Akbulut–Kirby presentation AK(2) is exactly 13

Abstract

For a balanced two-generator presentation R=⟨ x,y | r₀,r₁⟩ write E(R)=|r₀|+|r₁| for the total length of its freely reduced relators, and call a sequence of elementary Andrews–Curtis moves peak-bounded by B if every presentation it visits, endpoints included, has E ≤ B. We determine the least B for which the Akbulut–Kirby presentation AK(2), with relators xyxy⁻¹x⁻¹y⁻¹ and x²y⁻³, can be carried to ⟨ x,y | x,y⟩ by a peak-bounded sequence: it is exactly 13, against E(AK(2))=11. The upper half is a 32-move sequence. The lower half is a certificate of a different kind — a set of 1340 presentations that contains AK(2), contains no trivial presentation, and is closed under every elementary move whose result still has total relator length at most 12. Verifying such a set is a single pass with no queue, no visited-set bookkeeping and no termination argument, so a reachability lower bound of this shape is checkable, not merely computable. Read for its floor rather than its ceiling, the same set shows that inside budget 12 the presentation AK(2) cannot be shortened at all, not by a single letter; with the peak-13 sequence this pins the wall of its basin at height exactly 2. The quantity is the elementary analogue of a bottleneck distance defined by Carreras on a restricted substitution graph, whose scope paragraph explicitly excludes elementary-path peak bounds. Every theorem below is machine-checked in Lean 4 by kernel evaluation alone, and we say exactly which computations lie outside that guarantee. Nothing here is about AK(3) or about the Andrews–Curtis conjecture.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   dc2cbfebb6f95fb8d27aa024d389ece875d7e277435fb390311c62e65d0505c9