The crossed-wire puzzle

A useful diagram suppresses detail. A proof-bearing diagram suppresses only detail that the declared theory has proved irrelevant.

A picture of a process is not yet process syntax

A conventional architecture diagram may use arrows for data, control, dependency, time, trust or mere visual grouping. Two arrows may cross because the drawing tool needed space. A box may mean a function, a service, a team, a database, a policy or a whole organisation. Such pictures can be excellent communication devices. They are not automatically terms in a formal language.

It also helps to distinguish a string diagram from a commutative diagram. In a commutative diagram, points usually denote objects and arrows denote morphisms; the claim is that different paths with the same endpoints compose to the same morphism. A string diagram instead depicts the internal assembly of one composite morphism. Wires are more than arrows between labelled points. They are the typed systems that persist between process events. To prove two string diagrams equal is to show that two assemblies denote the same composite under the laws of the process theory.

This is why a diagram can be formal without being fully semantic. Start with a signature containing types and primitive boxes. Generate every well-typed diagram obtainable by sequence and tensor. That gives a free syntax in which no accidental domain equations have yet been imposed. Then quotient by declared equations such as a particular rewrite, a symmetry law or an algebraic identity. Finally, interpret the resulting theory in a target model. Keeping these stages separate prevents a property of one implementation from being mistaken for a universal law of composition.

A string diagram makes a sharper bargain. Wires denote systems or types. Boxes denote processes with ordered input and output boundaries. Joining a wire to a box is legal only when the types match. Placing one box after another denotes sequential composition. Placing boxes beside one another denotes parallel composition. A complete diagram denotes one composite process from its exposed input boundary to its exposed output boundary. This idea was formalised for monoidal categories by Joyal and Street, building on earlier graphical tensor notation, and developed into a hierarchy of graphical languages for different categorical structures [1] [2].

A string diagram is a typed term drawn spatially. The drawing is not a mnemonic pasted onto an equation. Its spatial operations are the language's constructors. This changes the burden of proof. We no longer ask whether two pictures look similar. We ask whether one well-typed term can be transformed into another by moves licensed by the theory.

The hidden contract beneath the page

Every proof-bearing diagram rests on four layers. The first is a signature: the available wire types and primitive boxes. The second is a composition grammar: how boxes connect sequentially and in parallel. The third is a structural regime: whether wires may cross, bend, copy or disappear. The fourth is an equational theory: named local patterns that may be replaced by other patterns. An interpretation then maps this syntax into actual functions, matrices, stochastic maps, circuits, protocols or other target processes.

Remove any layer and the visual argument weakens. Untyped wires permit impossible connections. An unspecified structural regime smuggles in swaps or feedback. Rewrite rules without semantics may manipulate marks consistently while saying nothing about the intended system. A semantic model without a proof calculus can show that two particular composites happen to agree, but not that the agreement follows from the general process laws.

flowchart TD
  A["The crossed-wire puzzle"] --> B["The proof surface"]
  B --> C["Four moves that are not free"]
  C --> D["From visual argument to<br/>checked artefact"]
  D -. "re-test" .-> A
  classDef first fill:#0a1424,stroke:#5B5CF6,stroke-width:2px,color:#e6f3ff
  classDef step fill:#0a1424,stroke:#3f7da0,stroke-width:1px,color:#e6f3ff
  class A first
  class B,C,D step

The proof surface

The core geometry is modest: processes can happen one after another or side by side. Its force comes from making those two forms of composition interact lawfully.

From two compositions to one process theory

Let A, B, C name system types. A process f : A → B transforms an input of type A into an output of type B. If g : B → C, then connecting the output of f to the input of g forms the sequential composite g ∘ f : A → C. The identity process 1_A leaves an A wire unchanged.

Now add a tensor product. If f : A → B and h : X → Y, their parallel composite is f ⊗ h : A ⊗ X → B ⊗ Y. The unit object I represents no exposed system. A state is a process I → A; an effect is A → I. These ingredients form a monoidal category, often called a process theory when read operationally [3] [4].

The smallest useful equation is the interchange law. Suppose f : A → B, f′ : B → C, h : X → Y and h′ : Y → Z. Then:

The left side says: perform two parallel processes, then another parallel pair. The right side says: compose the complete left lane and the complete right lane, then place those lane composites in parallel. Interchange is the first place where space becomes algebra. It licenses sliding independent boxes vertically past each other without changing the total process, provided their wires remain separate.

The proviso matters more than the equation's elegance. “Beside one another” is not a statement about screen coordinates. It asserts that the two components form a tensor product and that each box acts only on its own factor. A database write and a cache refresh drawn in separate columns are not thereby independent. A neural module and a monitoring hook on different lanes may still share parameters, randomness or clocks. Before interchange applies, the modeller must show that every relevant dependency is either absent or represented by a wire.

Why bending can replace parenthesising

Text forces choices that often have no operational content. Is (A ⊗ B) ⊗ C written before A ⊗ (B ⊗ C)? Is an identity wire inserted on the left or right? A general monoidal category carries associator and unitor isomorphisms that relate these presentations. Coherence results show that diagrams built from these structural isomorphisms agree whenever their formal shape requires them to agree. This is why string diagrams can usually omit a forest of parentheses and canonical reshufflings [5].

Joyal and Street's geometric account identifies morphisms in the freely generated monoidal setting with well-typed progressive plane graphs modulo the appropriate deformation. Modern work continues to refine this relation, including non-strict and effectful settings where apparently harmless spatial moves may cease to be valid [6] [7]. The practical lesson is not that topology magically proves algebra. It is that a coherence theorem has already paid for certain topological freedoms.

Soundness, completeness and scope

Suppose a signature and equation set generate a diagrammatic theory. An interpretation assigns each wire type to a target system and each primitive box to a target process, preserving identities, sequence and tensor. Categorically, this is a suitable monoidal functor from the syntactic process theory into the target category. Once the generators are interpreted, every composite diagram receives a compositional meaning.

A rewrite system is sound when every permitted diagram transformation preserves that meaning in every model satisfying the rules. If D_L rewrites to D_R, then:

Completeness asks the converse at a declared scope. If two diagrams have equal meaning in all relevant models, can the rules transform one into the other? A calculus can be sound but incomplete. Its derivations are trustworthy, yet some true equalities remain unreachable. Completeness results are therefore local achievements, not a generic property of visual reasoning. The ZX-calculus, for example, has completeness results for specified fragments of quantum theory, not a licence to treat every quantum-looking sketch as a proof [8].

Soundness and completeness answer different questions. Soundness protects every accepted move. Completeness measures whether the rule set can find every equality in the stated domain. A tool that evaluates two diagrams on a few examples supplies neither by itself. It may discover a counterexample, or increase confidence in a particular model, but sampled agreement is not a general derivation.

There is a third practical question: can the proof search be made usable? A rewrite system may be sound and complete yet still wander forever if rules can fire in cycles. Orienting equalities from complicated patterns towards simpler ones may create a terminating normalisation procedure, but termination alone does not guarantee that different rewrite choices meet at the same result. Confluence supplies that assurance. When both properties hold, equality can often be decided by reducing both diagrams to a common normal form. When they do not, an interactive prover may still be reliable because each local move is checked, even though search requires strategy or human guidance.

Target-specific equality sits beside, not above, this generic calculus. Two matrices can happen to be equal because their entries cancel, even if the equality is not derivable from bare monoidal laws. Conversely, a generic diagram equation may hold in every model of the theory without any numerical evaluation. A disciplined tool therefore reports which route established the result: coherence, a named rewrite theorem, exhaustive evaluation in a finite model, symbolic algebra in one interpretation or a proof-assistant derivation. Collapsing those routes into a single green tick hides the most important part of the evidence.

Four moves that are not free

Most invalid graphical arguments do not misuse composition. They import an extra capability by drawing it as if space itself supplied it.

The rows are not a single ladder of increasing realism. Cartesian structure and compact closure add different powers. A theory may support feedback without canonical copying, or copying without a trace. The right question is therefore not “which diagram language is strongest?” It is “which operations are justified by the target processes, and which equations follow from that choice?” Adding structure makes more pictures legal, but it also makes a stronger modelling claim.

Crossing: exchange is an operation

In a symmetric monoidal category, a symmetry morphism σ_A,B : A ⊗ B → B ⊗ A swaps adjacent systems. The graphical language allows wires to cross, and two consecutive crossings cancel. In a braided category, crossings retain over-under information and a braid need not equal its inverse. In a merely planar monoidal category, there may be no generic crossing at all. Selinger's survey catalogues how these different structures change the legal geometry and the equations it represents [2].

A crossing is a process, not empty decoration. This matters whenever order carries meaning: a tensor product of typed resources, a sequence of tokens, a queue of obligations or a spatial arrangement. A symmetric model declares that adjacent systems can be exchanged coherently. It does not say that the exchange is physically free, temporally instantaneous or authorised in a deployed system. Those are properties of the interpretation, not of symmetry alone.

Copying and discarding: classical convenience is not universal

Ordinary programming encourages a strong intuition: any value can be duplicated, ignored or logged. General monoidal process theories do not grant those operations automatically. A copying box would have type Δ_A : A → A ⊗ A. A discarding effect would have type !_A : A → I. They may be supplied as explicit processes or arise canonically in a cartesian category, where products support natural diagonals and terminal maps. Outside that setting, they are additional structure with equations of their own.

This restraint is not ceremonial. Copying an immutable classical record differs from cloning an unknown quantum state, duplicating a live database transaction or forking an agent whose future state will diverge. Discarding a local scratch value differs from deleting the only effect receipt after a consequential action. Copying is data-specific power. A diagram that forks a wire must state what can be copied, under which semantics and with which aliasing or conservation consequences.

Discarding deserves equal scrutiny. A terminal map in a cartesian theory says every value can be ignored in one canonical way. Operational systems often distinguish several forms of “not using” something: suppress a display, revoke access, erase storage, retain under legal hold or aggregate into an audit statistic. Those effects are not interchangeable. Drawing a wire into empty space can conceal a consequential process whose failure modes, permissions and receipts belong inside the model.

Feedback: a loop needs an equation, not just curvature

Bending an output wire back into an input suggests recurrence, iteration, a fixed point or a trace. These are related but not interchangeable notions. Traced monoidal categories provide an abstract trace operation satisfying specific axioms; compact closed categories support cups and caps that bend wire orientation in a stronger geometry [10] [9]. Other settings allow only guarded or delayed feedback because an instantaneous loop would be undefined.

A loop is not licensed by the fact that it fits on the page. In software, x = f(x) may have no solution, several solutions or a least fixed point under a chosen order. In control, feedback can stabilise or destabilise depending on gain and delay. In probabilistic models, cyclic dependencies require a defined semantics. The graphical curve hides all of these obligations unless the process theory exposes them.

Sliding effectful boxes: hidden state breaks interchange

The most dangerous false proof is often a legitimate monoidal move applied to processes that are not independent. Consider two operations that look as if they act on separate data wires. Operation A increments a hidden audit counter. Operation B reads that counter and appends its value to an output. Draw only the visible data and the boxes appear disjoint. Slide A past B, and the output changes.

Premonoidal and effectful categorical models exist precisely because arbitrary effectful computations need not interchange. Recent work gives a useful graphical discipline: add a runtime wire that passes through effectful boxes, making their shared dependency visible. Pure boxes can float around that wire; effectful boxes remain ordered along it [6]. Hidden state turns apparent parallelism into order dependence.

stateDiagram-v2
  [*] --> Claim
  state "A picture of a process is not<br/>yet process syntax" as Claim
  state "The hidden contract beneath<br/>the page" as Test
  state "From two compositions to one<br/>process theory" as Revision
  Claim --> Test: expose mechanism
  Test --> Decision: evidence survives
  Test --> Revision: rival survives
  Revision --> Claim: narrow or rebuild
  Decision --> [*]

From visual argument to checked artefact

The practical problem is not drawing diagrams. It is knowing what conclusion a proposed deformation is allowed to carry.

The Diagram Proof Contract

The following contract is a practitioner synthesis, not a new coherence theorem. It packages the minimum information needed to audit a visual process argument across mathematics, software architecture and AI system design. The contract makes the picture auditable.

Apply it in a fixed order. First compare the exposed boundaries, because different interfaces cannot denote the same typed process. Next expand hidden state, authority, randomness and environmental interaction until proposed independence is credible. Then select the least permissive structural regime that can express the system. List domain equations separately from coherence laws. Only after those steps should a reviewer attempt the deformation. The final receipt names each local move and the scope of the conclusion.

This order makes countermodel search cheap. Before investing in a polished derivation, try to construct one small interpretation in which the proposed equality fails. Finite functions, Boolean state machines and tiny matrices are often enough. A countermodel shows that the equality does not follow from the current axioms. It may reveal a missing premise, a hidden shared resource or an over-broad structural declaration. Failure to find a countermodel is not a proof, but finding one is decisive.

Executable lab: assess a proposed move

The lab below evaluates five common moves against five structural profiles. It does not solve arbitrary diagram equality. It makes hidden assumptions visible, returns a machine-readable deformation receipt and includes one semantic counterexample for shared-state commutation.

How to read the result

A positive result under generic scope permits the move only as a structural equality in every model of the selected theory. A positive configured result establishes equality only for the finite semantics implemented by the lab. A warning means that the move could be lawful after adding an explicit box or rule. A negative result means the current contract does not support the inference; it does not prove that the two real-world systems differ. A positive lab result licenses only the scope printed in its receipt.

The lab cannot establish that the selected category is an adequate model of an organisation, a biological system or a conscious process. It also does not prove completeness, termination or confluence of a rewrite system. Its job is narrower: catch category errors before visual confidence hardens into a design decision.

For a real review, replace the lab's assumed boundary with a typed manifest. Record port order, provenance, mutability, ownership and whether each wire denotes data, capability, world state or evidence. Attach side conditions to rewrites, such as “boxes touch disjoint state” or “swap is authorised for these record types”. A receipt should remain valid only against the versioned signature, equation set and interpretation that produced it. Change any of those inputs and the equality must be rechecked.

from __future__ import annotations

from dataclasses import asdict, dataclass
import json
import sys

PROFILES = {
    "planar": {"interchange"},
    "symmetric": {"interchange", "swap"},
    "cartesian": {"interchange", "swap", "copy", "discard"},
    "traced": {"interchange", "swap", "feedback"},
    "effectful": set(),
}

@dataclass(frozen=True)
class Receipt:
    profile: str
    move: str
    scope: str
    status: str
    warrant: str
    semantic_check: dict[str, object] | None = None


def shared_state_counterexample() -> dict[str, object]:
    # State is (audit_bit, output_bit).
    def a(state: tuple[int, int]) -> tuple[int, int]:
        s, x = state
        return 1 - s, x

    def b(state: tuple[int, int]) -> tuple[int, int]:
        s, x = state
        return s, x ^ s

    start = (0, 0)
    a_then_b = b(a(start))
    b_then_a = a(b(start))
    return {
        "start": start,
        "A_then_B": a_then_b,
        "B_then_A": b_then_a,
        "equal": a_then_b == b_then_a,
    }


def assess(profile: str, move: str, scope: str) -> Receipt:
    if profile not in PROFILES:
        raise ValueError(f"unknown profile: {profile}")

    if move == "effect-commute":
        check = shared_state_counterexample()
        return Receipt(
            profile, move, scope, "rejected",
            "Shared runtime orders the boxes; interchange is unavailable.",
            check,
        )

    if move in PROFILES[profile]:
        return Receipt(
            profile, move, scope, "permitted",
            f"The {profile} profile declares this structural operation.",
        )

    required = {
        "swap": "braiding or symmetry",
        "copy": "an explicit copier or cartesian diagonal",
        "feedback": "a trace, compact structure, or fixed-point operator",
        "interchange": "independence from shared runtime effects",
    }.get(move, "an explicit rule")
    return Receipt(
        profile, move, scope, "unsupported",
        f"Add {required}; the drawing alone is not a warrant.",
    )


if __name__ == "__main__":
    profile = sys.argv[1] if len(sys.argv) > 1 else "symmetric"
    move = sys.argv[2] if len(sys.argv) > 2 else "interchange"
    scope = sys.argv[3] if len(sys.argv) > 3 else "generic"
    print(json.dumps(asdict(assess(profile, move, scope)), indent=2))

A configured-system example: which refactor is actually safe?

Consider a synthetic AI action path. A model proposes an action. One branch checks evidence sufficiency; another formats a human-readable explanation. An authority kernel then decides whether the typed action may execute. The external system applies the action, and a readback produces an effect receipt.

The explanation formatter and an evidence-index formatter may commute if both are pure transformations on separate copies of already authorised input. The authority decision and the execution box do not commute: executing first changes the world before permission is established. Nor may the effect receipt be discarded merely because the diagram remains visually connected. Its presence changes recoverability and auditability.

Tooling, formalisation and the remaining human judgement

Diagrammatic proof can be mechanised at several levels. DisCoPy supplies Python data structures for constructing, composing, drawing, rewriting and interpreting string diagrams across multiple categorical structures [12] [13]. Hypergraph-based rewriting gives sound and complete correspondences for specified diagrammatic theories with Frobenius structure, supporting automated local transformations rather than freehand resemblance [11]. Recent Rocq work couples a graphical editor with formal tactics so graphical rewriting steps can be translated into textual proof objects checked by a proof assistant [14].

These tools reduce clerical error. They do not choose the right system boundary, decide whether two business operations are independent or justify treating a biological or phenomenological description as a monoidal process theory. The modelling decision remains a substantive claim. For convergence research, this is the crucial restraint: a string diagram can prove an equality inside a formal mapping, but it cannot by itself prove that machine attention is awareness, that a cognitive episode is a tensor network or that two traditions share an ontology.