The setting is exact-arrival multi-agent path finding: every agent has a pinned departure place and time and a pinned arrival place and time, and the agents are coupled by vertex conflicts. The output is distributed rather than centrally decoded, so each cell must emit whether it belongs to a valid joint path-support mask. The machine is cellular and nonuniform: topology and slot information may be compiled into per-cell transition rules, each cell has finite state for the fixed topology, communication follows a fixed local fabric, computation proceeds in synchronous rounds, and the output round is independent of the query. The central difficulty is that a branch can be legal for an agent in isolation but become invalid because a different agent makes a later conflicting choice.
The main result gives an explicit two-agent, twelve-cell, depth-three topology on which no forward-only machine with no global channel is correct for two feasible queries, regardless of how many local rounds it uses. Reversing time yields the corresponding obstruction for backward-only machines, and taking the disjoint union of the two constructions rules out renouncing either orientation across the composite family. The paper then places multiple selector copies side by side and derives a bandwidth-round trade-off for forward-only machines: at constant depth, the information reaching target cones plus the information carried by global one-bit flags must scale with the number of copies. Matching-order upper bounds are described using a backward-capable machine and a flag-streaming construction.
The machine receives, at each cell, its own cavity bit, meaning the maximum individual path-support available to that agent. This concession makes the single-agent problem trivial in zero rounds, so the lower bound must come from inter-agent conflicts rather than from missing individual reachability information. In the crossed-conflict selector, the query changes a forcing bit on the other agent while leaving the target cell’s own local cache unchanged; one branch is fully compatible with a joint support in one query and the other branch is fully compatible in the other query. Locality and cone invariance imply that the target sees the same relevant state in both cases, while the forced-output property requires different output bits, producing a contradiction. For repeated copies, transcript counting measures how much query information can reach target cones and how much can be carried through the global flags.
The finite gadget lemmas and the pair-invariance contradictions are checked in Lean 4. The semantic bridge from the machine to the path-support task, the cone lemma, and the counting argument are presented as paper proofs. The single-agent consequence is also said to be confirmed by exhaustive enumeration. The paper reports no benchmarks, standard MAPF datasets, baseline algorithm comparisons, runtime measurements, success-rate measurements, or other conventional empirical evaluation.
The theorem should not be read as saying that every forward-only algorithm fails on every instance. Because the topology is known offline, a forward-only machine with enough time and suitable global signaling can gather endpoint and cavity bits, enumerate candidate joint masks, check local path, pin, and conflict conditions, and eventually make every cell output the retained valid candidate. A flooding machine also solves every instance in a number of rounds equal to the diameter of the local fabric, so the architecture class is not inherently too weak. The result instead says that one-directional local causality cannot handle the stated query families at the claimed constant-depth and narrow-channel resource regime without another payment, such as longer runs, wider channels, external advice, sequential enumeration, or shared memory. The excerpt does not establish hardware-level performance or a universal optimal upper bound for bidirectional machines; it indicates that the exact-arrival, free-arrival, and deadline variants are not separated by the proofs described.
Exact-arrival routing differs from ordinary reachability because both ends of every agent’s schedule are pinned. A cell that looks harmless when considering only its own agent may be ruled out by a collision with another agent whose endpoints constrain its available choices. This makes endpoint information and cross-agent conflict information jointly relevant even when individual reachability has already been supplied.
The paper asks whether a cellular machine can produce a valid joint path-support mask for every feasible query while using only local communication in one temporal direction. The topology is fixed and known, the state is factored over cells, communication is synchronous, and the output time cannot depend on the query. The studied task is not deciding only global feasibility, selecting one centrally decoded path, or computing an exact maximal joint support; it is distributed production of any valid support mask.
A cavity is the maximum individual path-support for one agent, and giving every cell its cavity bit eliminates the easy single-agent direction argument. The multi-agent construction keeps the target’s own cavity fixed while changing a query-dependent condition on the collision partner, so the correct target output changes without a corresponding local causal change. In the replicated family, the forward-only lower bound is expressed as J_R+kR≥p, where J_R measures information reaching target cones, k is the number of one-bit global flags, R is the number of rounds, and p is the number of copies; in the stated family J_R is zero. A backward-only machine handles that family in constant rounds, while streaming one-bit flags requires on the order of the number of copies divided by the number of flags, plus a constant overhead.
The evidence is primarily theorem-level rather than benchmark-level. It includes machine-checked finite lemmas, a checked finite enumeration for the single-agent consequence, and paper proofs for the semantic and counting components. A later section is described as containing finite enumerations and simulations, but the supplied excerpt does not provide their datasets, exact conditions, numerical outputs, or comparison baselines. Accordingly, no empirical performance claim beyond the stated finite verification should be inferred.
On the twelve-cell, two-agent, depth-three gadget, a forward-only machine with no global flags fails on two feasible queries for every number of rounds. The time-reversed gadget gives the analogous failure for backward-only machines, and the composite family requires both orientations at the architecture level. For repeated copies at constant depth, the forward-only information requirement grows with the number of copies, while a backward-only construction solves the family in constant rounds and a flag-streaming construction uses roughly the copy count divided by the flag count, plus constant overhead. The paper characterizes this as tight in order, not as a conventional runtime benchmark.
An early commitment in exact-arrival routing can be invalidated by a later decision made by another agent. Supplying complete individual reachability caches and allowing a few global aggregate bits removes two obvious objections but does not remove the multi-agent obstruction. The paper therefore identifies bidirectional local propagation as necessary for the explicit constant-depth families, unless the design instead pays with communication bandwidth, rounds, external advice, enumeration, or shared memory. The necessity is an architectural and resource statement, not a claim that one-way machines lack all expressive power.
The conclusions rely on a narrow model: ranked directed acyclic graphs, vertex conflicts, feasible queries, fixed local wiring, synchronous rounds, and nonuniform transition rules compiled from the known topology. The supplied text does not establish results for edge conflicts, capacities, kinematics, dynamic topologies, or a complete general-topology upper bound for bidirectional machines. It indicates that the proofs do not separate exact-arrival from free-arrival or deadline variants, rather than proving a broader equivalence of all such models. It also explicitly says that the literature search is a first pass over bibliographic records and abstracts rather than an exhaustive priority survey. Since no benchmarks are reported, the paper does not show how the lower bound predicts practical performance on standard MAPF instances.
The work isolates a specific information-flow obstruction in distributed MAPF: preprocessing each agent’s individual options does not resolve dependencies created by collisions with other agents. For cellular or hardware-inspired solvers, it provides a way to account for the choice between bidirectional wiring and alternative resources such as global bandwidth, execution time, or shared memory. The small, parameterized, and partly formally checked families may be useful as future stress tests, although the paper does not itself exercise them as a benchmark suite.
This paper is most relevant to researchers in MAPF under exact timing constraints, distributed computation, cellular automata, causal-cone lower bounds, and communication complexity. It is useful for readers designing local hardware or analyzing what global signaling can buy under narrow bandwidth. It is not a substitute for an empirical survey of MAPF solvers, because the supplied paper reports no standard datasets, baseline comparisons, or conventional performance evaluation.