Exact Action Depth in a Two-Probe Partition Planner: An n + 1 Diameter Law on Partition Lattices
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.
Authors
- benjamin lenoir
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-09-05
- DOI
- https://doi.org/10.5281/zenodo.22394897
- Primary Topic
- DNA and Biological Computing
- Type
- preprint