Exact Action Depth in a Two-Probe Partition Planner: An n + 1 Diameter Law on Partition Lattices

Abstract

We prove the exact worst-case action depth of a two-probe planner on the partition lattice: [ D_2(n)=n+1 \qquad (n\ge5). ] The result is achieved by matching structural upper and lower bounds, with explicit extremal families, mechanical certificates, and a source-level Lean 4 formalization.