Faithful local dynamics on every finite acyclic graph

Give each vertex of a finite directed acyclic graph a finite set of states, and let updating a vertex overwrite its state with a function of the states at its outgoing neighbors. Collina and D'Andrea showed that such updates always satisfy the relations of the graph's Hecke–Kiselman monoid, introduced by Ganyushkin and Mazorchuk, and conjectured that some choice of states and functions satisfies no other relations. They proved this for complete acyclic graphs, and Forsberg's effective representations settle further special classes. We prove the conjecture for every finite directed acyclic graph: some such system represents the monoid faithfully, so two words act equally in every system exactly when they are equal in the monoid. Each update is recorded as a formal expression built from the expressions it reads. Aragona and D'Andrea's cancellation rules reduce every word to one of their normal forms. In a normal form, the expressions produced at each vertex grow strictly and all survive in the final state, so the final state determines the word up to swaps of adjacent commuting letters. Lean checks the full theorem. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.