Every post in this blog is an arrow, an object, or a commutativity proof inside a single diagram.
The square is symmetric monoidal categories all the way down. F builds the free SMC from a net. U extracts the universe — the marking space. Exec equips a marking with its execution context. ε extracts the focus. The two paths commute: composition then forget, or contextualize then extract, same marking space.
Petri nets are the worked example. The structure is SMC.
We don't need Petri nets to read the diagram. The zipper — Huet's 1997 decomposition of a data structure into a hole and two contexts — is universal. Undo/redo, cursor position, the call stack. Any computation that has a current state, an accumulated past, and a set of possible next steps already has this shape.
W(M) = 𝓛 × M × 𝓡 says: wrap a bare state with its tropical past and its predicate future. W is the world — the comonad that makes context explicit. Three operations:
Every DDM engine is a coKleisli morphism W(M) → M: read the full context, produce the next state.
The bottom of the diagram is the central result. Three independent analyses find the same core-observer boundary:
ODE steady state — relax the net into ℝ^P, solve for equilibrium, recover integer structure. This is mass action kinetics. Places with ρ = 1 are reversible (core). Places with ρ > 1 are irreversible (observer). The boundary falls out of the eigenstructure.
Tropical accumulation — timed event graphs are max-plus linear: x(k+1) = A ⊗ x(k). Places with 1:1 producer-consumer relationships are core. The rest are observer. Same boundary, discrete proof.
ZK witness structure — compile to R1CS. Core places produce uniform constraints. Observer places require non-uniform witnesses. The compiler discovers the boundary because uniform and non-uniform are fundamentally different proof objects.
They agree because they're all reading the same incidence matrix. The boundary is a property of the morphism structure — the SMC — not of any particular analysis. One net, one shape.
The decomposition into 𝓛 × M × 𝓡 isn't a design choice. It's forced by what recursion requires.
Tropical accumulation (max, +) is monotone — max is idempotent, values only grow, once a fact is absorbed it never changes. The left context is a value, not a mutable reference. That's referential transparency for the past, and it's what makes recursion safe. Event sourcing works because the log is immutable. ZK proofs work because the witness is fixed. Tropical matrix multiplication is fast-forward — A^n = A ⊗ A ⊗ ... ⊗ A — because you can skip ahead without replaying.
The comultiplication δ : W(M) → W(W(M)) is well-defined precisely because 𝓛 can't mutate under you. If the left context were mutable, re-contextualization would be incoherent. The comonad laws require immutability on the left.
The right context is the opposite — ephemeral, recomputed from the hole on every step. You can't recurse over the future because it doesn't exist yet. The asymmetry between 𝓛 and 𝓡 isn't arbitrary: one is a semiring that accumulates, the other is a predicate that evaluates. (max, +) on the left, boolean guards on the right. The algebra dictates the tense.
The three-part decomposition L × M × R is not new. Abstract machines (Felleisen's CEK, 1987), game semantics, Girard's geometry of interaction, and event sourcing all independently discover the same shape: accumulated past, current focus, constrained future. Every serious formalization of computation lands here.
What we've shown for Petri nets is: (1) the left context is specifically tropical — not "some accumulation" but (max, +), forced by what recursion requires, and (2) three independent analyses (ODE, tropical, ZK) find the same core-observer boundary from the incidence matrix alone.
The generalization is probably this: the pflow square works for any SMC whose morphism structure is decidable. The adjunction F ⊣ U guarantees the tense structure — the zipper always exists. But whether you can find the boundary depends on the expressiveness of the morphisms. Petri nets sit in the sweet spot: expressive enough to model interesting systems, constrained enough that the core-observer boundary is computable. The incidence matrix is finite, the reachability question is decidable (Mayr, Kosaraju), and the three analyses converge because they're all reading the same finite linear structure.
Move to a richer SMC — say, coloured Petri nets with arbitrary data types, or higher-order process calculi — and the tense decomposition still holds (it's forced by the adjunction), but the boundary may not be computable. The zipper exists; the question is whether you can compute where the hole is. Decidability of the morphism structure is the dividing line between "the square commutes in principle" and "the square commutes and you can build tools that exploit it."
That's why this is a Petri net result and a result about computation. The categorical structure is universal. The computability is not.
Related: The Zipper Whose Hole Is a Universe · Symmetric Monoidal Categories · Tropical Petri Nets · Earned Compression · ZK Petri Nets · The Incidence Reduction