Six posts from February to April โ symmetric monoidal categories, the zipper, tropical Petri nets, earned compression, ZK Petri nets and the incidence reduction โ each supplied an arrow, an object, or a claim that two paths agree. This is the one diagram they fit into.
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 are meant to commute: composition then forget, or contextualize then extract, same marking space. That is what the square asserts; it is drawn, not proved.
Petri nets are the worked example. The structure is SMC.
Revised 2026-10-20. W is FU, the comonad; an earlier revision today relabelled it as the monad UF, and that is undone. The figure now draws FU as the round trip at F(N), and its convergence labels no longer call the three analyses independent or the core reversible. See What Changed.
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 construction that makes context explicit, and we take it to be a comonad. A comonad needs two operations:
The figure labels it W = FU, the round trip taken from the SMC side: forget a symmetric monoidal category down to its underlying net with U, then build the free one back up with F. In an adjunction F โฃ U that composite is the comonad โ UF, the round trip from the net side, is the monad โ with counit ฮต : FU โ Id and comultiplication ฮด = FฮทU. The figure draws it as a loop at F(N), so no path around the square should be read as W. FU is a comonad by construction; what we have not done is show that the zipper W(M) = ๐ ร M ร ๐ก is that comonad, or check the comonad laws for its ฮต and ฮด directly. So when we read a DDM engine as a coKleisli morphism W(M) โ M โ read the full context, produce the next state โ that is a reading, and it is only as good as the laws.
The bottom of the diagram is the claim the square was drawn for: three analyses of the incidence matrix put the same transitions on each side of the core-observer boundary โ the ฯ boundary, where ฯ(t) is the tokens transition t consumes over the tokens it produces. Earned Compression was checked against the code in October 2026, and each leg holds up less well than this post first said.
The ODE steady state relaxes the net into โ^P under mass-action kinetics and recovers integer structure from the equilibrium. This post said the boundary falls out of the eigenstructure, with ฯ = 1 transitions reversible and ฯ > 1 irreversible. Nothing computes an eigenstructure for it. What the ODE sees is direction of flow: observer transitions are sinks, and in the tic-tac-toe ODE they fire inside the solve and halt it. "Reversible" was the wrong word for the plays, too โ no play has a reverse transition. What the core has is that it destroys nothing (the cell and turn invariants hold), where a win takes five tokens and leaves one. And in the 33-place net the plays are ฯ = 2/3, not 1, because each also feeds a move_tokens counter that the draw consumes (pilot_ttt); only the counter-free core has plays at exactly ฯ = 1.
Tropical accumulation needs a timed event graph โ every place with one producer and one consumer โ for x(k+1) = A โ x(k) to hold. This post said the places with that 1:1 shape are core and the rest observer. Strictly, the tic-tac-toe core isn't an event graph either: each empty-cell place has two consumers and the turn places have nine. The argument that one turn token serializes the core applies just as well to the single game_active token every win consumes, so of the three this is the weakest leg.
The ZK leg was supposed to discover the boundary because core transitions compile to uniform constraints and observer transitions need non-uniform witnesses. The circuits we run don't do that. The arkworks circuit in pflow-rs (circuit.rs) puts every transition, wins and draw included, through one boolean selector multiplexer, with a remainder witness per input arc, and the gnark circuit in the ZK post has the same shape. The observer's cost is width: a win has five input arcs to a play's two, and every step's circuit is padded to the widest.
So the three do agree on tic-tac-toe, but not as independent discoveries. Each leg is derived from the one sink property, which tracks ฯ in this net, and nothing yet runs the three classifications on one net and compares the partitions. What they do share is what they read โ C โ and that is also why none of them sees a read arc. An overdraft guard has ฯ = 1, is not a column of C, and sits on the other, contextual boundary (two boundaries).
We think the decomposition into ๐ ร M ร ๐ก is forced by what recursion requires rather than chosen, though nothing below is a proof of that.
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 case for the comultiplication ฮด : W(M) โ W(W(M)) is that it is well-defined because ๐ can't mutate under you โ if the left context were mutable, re-contextualization would be incoherent. That is the intuition, not a check of the comonad laws, and ฮด is exactly where Structuralism, Not Objects later found the framing strains: if ๐ก is an effect that ฮต handles rather than a value W holds, ฮด copies the left context as a value and re-installs the right one as a handler, and W is a value, a focus and a scope rather than a product of three values.
The right context is the opposite of the left โ ephemeral, recomputed from the hole on every step. You can't recurse over the future because it doesn't exist yet. The asymmetry has an algebraic face: one side is a semiring that accumulates, the other a predicate that evaluates. (max, +) on the left, boolean guards on the right.
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. A lot of formalizations of computation land here.
This post claimed two things for Petri nets: that the left context is specifically tropical โ not "some accumulation" but (max, +) โ and that three independent analyses (ODE, tropical, ZK) find the same core-observer boundary from the incidence matrix alone. The first is argued above, not proved. The second needs three qualifications from later work. It is the ฯ boundary, the one that lives in C; the contextual one is R's business. The analyses are not independent, since each reads the one sink property. And at tic-tac-toe's turn places C is not enough: deciding whether the core behaves like an event graph there takes reachability information, which C doesn't carry.
The generalization might be this: the pflow square works for any SMC whose morphism structure is decidable. If the adjunction and the comonad can be stated properly, they would give the tense structure for free โ the zipper would always exist. But whether you can find the boundary depends on the expressiveness of the morphisms. Petri nets look like a sweet spot. The ฯ boundary is a count over the columns of a finite matrix, and where C runs out, as at the turn places, the reachability question is still decidable (Mayr, Kosaraju), if not cheaply.
Move to a richer SMC โ say, coloured Petri nets with arbitrary data types, or higher-order process calculi โ and the tense decomposition might still hold, 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 would be the dividing line between "the square commutes in principle" and "the square commutes and you can build tools that exploit it." We haven't tried the square on anything richer than an ordinary net, so this is a conjecture about where the line falls, not a result.
Revised 2026-10-20 against Earned Compression as revised on 2026-10-18, the pilot_ttt fixture and the arkworks circuit in pflow-rs. Nothing was re-run.
pilot_ttt, 1 counter-free) against the observer as a sink, as in the ODE leg above.Related: The Zipper Whose Hole Is a Universe ยท Symmetric Monoidal Categories ยท Tropical Petri Nets ยท Earned Compression ยท ZK Petri Nets ยท The Incidence Reduction ยท The Category Settle ยท Structuralism, Not Objects