A Typed Certification Protocol for Finite-State Causal Abstractions
Description
Coarse-grained dynamics can be well defined while failing to preserve the targets or persistence events that motivate a model. This paper presents a typed certification protocol for finite-state, discrete-time controlled Markov systems. The protocol separates state aggregation, action implementation, history-response equivalence, and event-order quotients, and records their assumptions within a fixed task contract. For exact state abstractions, action-wise strong lumpability and implementation invariance yield well-defined macro kernels and finite-horizon state-path consistency under compatible control protocols. Probabilities of persistence events are preserved only when the events are measurable through the aggregated paths. For approximate abstractions, standard total-variation contraction and perturbation arguments provide a finite-horizon error budget with a separate term for target approximation. Finite examples and counterexamples distinguish dynamical closure from implementation consistency, target measurability, and preservation of identity-dependent events. The contribution is an explicit organization of these certification obligations and their failure witnesses, rather than new foundations for lumpability or Markov contraction. The results concern specified finite models and do not establish empirical validity in natural systems or general compositional guarantees for open systems. The protocol forms a bounded mathematical component of the DCS research program.