Module coalgebra 

The coalgebraic / Poly view, made into checked code rather than narration.

A certified refutation is a discrete dynamical system — a coalgebra S → p(S) for a polynomial functor p (positions = states, directions = the certified moves available there), exactly Spivak’s model of dynamical systems in Poly. A Lyapunov measure is then a coalgebra morphism to the countdown coalgebra (ℕ, n ↦ n-1) — the canonical well-founded object: it intertwines the system’s dynamics with the countdown’s, i.e. every transition strictly decreases it.

The load-bearing theorem (Taylor; Adámek–Milius–Moss on well-founded coalgebras): a finite system is well-founded (terminating — no infinite forward trajectory) iff it admits a morphism to a well-founded object. That equivalence is the synthesis–impossibility duality at the categorical level: a collapsing measure is a countdown morphism, and its non-existence is the presence of a cycle. We make both directions constructive and machine-checked here, and connect it back: every Lyapunov trajectory this crate produces is a countdown morphism on its path system.

Structs

TransitionSystem

A finite transition system: a coalgebra S → 𝒫(S) for the finite-powerset polynomial functor. successors[s] lists the states reachable from s in one step.

Functions

canonical_countdown_morphism

The canonical countdown morphism of a well-founded system: the longest forward path from each state (sinks = 0). This is the terminal such morphism — the existence half of the theorem made constructive. Returns None if the system is not well-founded (no morphism exists).

is_countdown_morphism

Is measure a coalgebra morphism to the countdown coalgebra? Every transition s → t must strictly decrease it (measure[t] < measure[s]) — the morphism square commuting with n ↦ n-1. Because the countdown is well-founded, a true here witnesses that the system is well-founded.

is_well_founded

Is the system well-founded (acyclic — no infinite forward trajectory)? Equivalent, for a finite system, to “is a DAG”. Computed by Kahn’s algorithm: a full topological order exists iff there is no cycle.