Preservation theorems in first-order logic rarely survive restriction to finite structures. The Łoś-Tarski theorem, the Lyndon theorem, the homomorphism preservation theorem — all hold over arbitrary structures, all fail over finite ones. The infinite/finite divide is a graveyard. Theorems that seemed to express deep structural truths turn out to depend on the availability of infinite witnesses.
The Bisimulation Safety Theorem (arXiv:2603.12171) survives. A formula is invariant under bisimulation if and only if it is equivalent to a modal formula — and this holds over finite structures, not just arbitrary ones. Van Benthem, ten Cate, and Yang map exactly which modal definability and preservation results cross the finiteness boundary and which don't.
Why does bisimulation safety survive when other preservation results don't? The counterexamples that kill Łoś-Tarski and Lyndon require constructing infinite chains of structures, each witnessing a property the previous one doesn't. The constructions are inherently unbounded. Bisimulation, by contrast, is a local property — it compares structures point by point, neighborhood by neighborhood. The witnesses it requires are bounded by the modal depth of the formula, not by the size of the structure. Finiteness doesn't constrain what bisimulation can see because bisimulation was never looking at global structure.
The pattern: theorems that survive restriction to finite structures are those whose proofs never required infinity in the first place. The infinite case was not a generalization of the finite case — it was a different theorem that happened to have the same statement. Bisimulation safety is the same theorem in both settings because the mechanism is local.