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 open question is whether this generalizes beyond Petri nets. Does the comonad W = UF from any free SMC adjunction produce a tropical left context? Does the convergence of continuous, algebraic, and cryptographic analysis hold for arbitrary morphism structures, or is it specific to the incidence matrix? If the tropical characterization and the convergence result survive generalization, the pflow square isn't a Petri net result — it's a result about computation.
Related: The Zipper Whose Hole Is a Universe · Symmetric Monoidal Categories · Tropical Petri Nets · Earned Compression · ZK Petri Nets · The Incidence Reduction