Axiom Dynamics 6: Between Sequential and Batch—Execution Equivalence Criteria for Axiom Transitions and the Normal Form of Replay Verdicts

This paper closes two still-open problems in the criterion system of axiom transitions on finite Horn deductive systems. On the execution problem: can a candidatebatch that passes the holistic transition-legitimacy biconditional be implemented asa sequential execution that is legal at every step? We prove a deadlock criterion:a pure expansion batch has a step-ignition-legal sequential implementation if andonly if the batch contains no deadlock subset, that is, no proper subset that, after activation, has already generated the entire closure of the batch. The criterionyields a counting necessary condition, namely that batch gain is no less than thenumber of candidates, and proves a strict separation of three tiers: holistic legalitydoes not imply step-ignition reachability; step-ignition reachability does not implythat all orderings are step-ignition legal; and the counting condition is necessarybut not sufficient. On the verdict problem: what is the canonical record of a replayverdict? We prove a verdict normal form: under the replay protocol in which theprotected core is fixed throughout registration and the archive is append-complete,every history uniquely decomposes, up to adjacent-compression congruence, into analternating sequence of maximal clean blocks and non-clean segments; the normalform is a complete invariant of the verdict, the comparison object for verdict equality is the normal-form structure rather than the number of raw segment records,and it is finitely decidable. An insertion-sensitivity counterexample proves that thiscongruence is an exact boundary and cannot be coarsened; bleach impossibility isa definitional corollary of archive appendability. All readings are recomputed by asingle self-contained script in exact integer arithmetic; the subset-criterion engineand the ordering depth-first engine agree in two routes with zero conflicts; all inputs are hardcoded, with no external data source and no random source. The aboveconclusions hold within the fragment of finite Horn systems, no negation, no quantifiers, and no self-referential encoding; minimal interleaved implementation withcontraction batches, the complexity classification of the deadlock criterion, and therefinement direction of the congruence are registered as open problems.