The Braid as a Fourth Sheaf

The categorical arc on this site has carried one algebraic substrate outward a step at a time, and every step so far has stayed abelian. Kennedy’s units of measure fixed the starting point: dimensional consistency is unification over a finitely-generated free abelian group, decided in polynomial time and free of any annotation the engineer has to write. The dimensional type system reads that group as a Tier 1 sheaf, a triangle without mystery reads each such discipline as a functor from the compilation poset to a target category of values, and the negative and fractional types add a duality dimension to the same abelian substrate, promoting our symmetric-monoidal semantics to compact closed while every group in view stays commutative. The exchange of two objects has been symmetric throughout: swap twice and the arrangement returns to where it started.

The braid is the next step, and it is where that symmetry breaks. Two pieces of concurrent work that cross in an order the runtime can observe do not commute; swapping them twice does not return the identity, and the group governing their rearrangement is the non-abelian braid group $B_n$. This is the principled boundary of the abelian gradient, and this page is the design orientation for it: a proposed non-abelian sheaf over the same compilation poset our other sheaves already sit over. It is a placeholder written with integrity, so the heavy formalization stays honestly ahead. The composition lemma and the full assembly proof named below are future work; this entry fixes the slot they would attach to and leaves the proof itself open.

A reader can reasonably worry that the framework just got more expensive, that a non-abelian solver at the narrow end drags every ordinary parallel loop onto a heavier verification path. The abelian guarantees the earlier steps established survive the non-abelian step intact, and the section that follows shows how before it turns to the categorical framing.

The Tiering Guarantee

Proof-for-free is protected by construction.

Free projection: the writhe. Every region has a braid word that records how its concurrent strands cross. Abelianizing that word, forgetting the order and keeping only the signed count of crossings, is the group homomorphism $B_n \to \mathbb{Z}$, and the image is the writhe: a single-generator abelian quantity. The writhe rides the same finitely-generated free abelian group the dimensional type system already unifies over, one more generator alongside the units, so it is a Tier 1 quantity carried at zero annotation cost and decided by the same integer linear algebra that decides dimensional consistency. Ordinary reorder-free parallelism, the map and fold and scan and stencil and the independent loop, is licensed at Tier 1 by strong confluence and referential transparency, the way the DCont/INet duality licenses the interaction-net breakout. A region in that class has writhe zero and reorders freely, and it never reaches a non-abelian solver, because it presents no observable crossing for a solver to reason about. The abelian projection is what the wide end of the gradient sees, and for the wide end it settles the question.

Assembled, not solved. Where crossing order is observable, the braid word over a region is a global section: an assignment of one stalk value to each node of the base poset, compatible across every edge. It is assembled from the tier-appropriate per-site proofs already discharged at each crossing, dimensional and grade facts at Tier 1, QF_LIA bounds at Tier 2, and it is witnessed by the same edge-check the compilation sheaf already describes: the structure-map equations checked on the edges of the Hasse diagram, with cost proportional to the number of lowering passes, not to the number of stage-pairs. The braid word is a composite of witnesses the compiler has in hand, not a fresh theorem the parallelism path stops to prove. Nothing new is proved on the ordinary parallelism path, because assembly consults proofs that already exist.

Scoped, graceful residue. A region whose crossing structure is covered by an already-discharged composable set is assembled and done. The case that remains is a region whose crossings fall outside that set. There the design degrades to an explicit obligation, scoped to a declared region boundary and live-only, in the same posture Weaving the Braid sets for a dynamic actor callee: the boundary is visible, the developer sees it and steers it, and the fallback is supervised. The composition lemma that would let per-crossing witnesses assemble into a region witness across a wider class of crossings is future work, not a present claim. Full braid unification, solving braid equations with metavariables during inference, is a further step out and is not known to be unitary; it is an open research obligation, and this page states it as one. The abelian projection and the assembled section keep the ordinary and the observable cases from blurring together, and the residue marks the honest edge of the design as it stands today.

A Fourth Sheaf Over the Same Base

The compilation sheaf leaves the door open by construction. Its base is the poset of compilation stages, source through PSG through the MLIR levels to the binary, and its closing observation is that any number of compatible sheaves can live over that one base. The document already names three siblings: the four-tier functional sheaf whose stalks range from $\mathbb{Z}^n$ at Tier 1 to relational pRHL judgments at Tier 4, the access Hoare sheaf whose stalks are capability lattices, and the symmetry Hoare sheaf whose stalks carry group actions. Each has its own stalk category, its own global-section problem, and its own dual-pass discharge, and all three are checked at the same edges of the same poset without interfering with one another.

The braid enters as a fourth sibling. Its stalks carry crossing structure: at each node of the base poset, the braid word that records how a region’s concurrent strands cross at that stage of lowering. The structure maps are the lowering passes, required to preserve the crossing structure the way the functional sheaf’s structure maps preserve dimensional annotations. A global section of this sheaf is a crossing assignment consistent across every lowering edge, and the dual-pass architecture witnesses it by the mechanism it already runs for the other sheaves: local structure-map equations at the Hasse edges, with compositionality propagating the check through the rest. The braid sheaf adds a stalk category to the base poset; it does not add a tier, and it does not change the poset the sheaves are built over.

This is a concrete inhabitant of a slot the dimensional type system already reserved. That document draws the boundary of the abelian fragment and points past it: properties involving non-abelian group actions are equivariance properties, silent to parametricity over the abelian dimensional group, and their natural assertional layer is a symmetry Hoare logic that reuses the same dual-pass discharge with a different stalk category. The braid is one of the concrete cases that live one step out from the abelian corner. Where the negative and fractional types stay abelian, promoting our symmetric-monoidal semantics to compact closed while the group stays commutative, the braid is the case where the substrate itself goes non-abelian: the group is $B_n$, and the order of composition is the content.

The Writhe and the Non-Abelian Residue

The braid word factors into an abelian image and a non-abelian remainder, and the two land on different tiers. Three readings make the object concrete, in the shape the negative and fractional types use for their own duals.

The categorical structure. The braid group $B_n$ is the group of $n$-strand braids under stacking, generated by the elementary crossings $\sigma_1, \dots, \sigma_{n-1}$ subject to the braid relations. It is non-abelian for $n \ge 3$: $\sigma_1 \sigma_2 \ne \sigma_2 \sigma_1$, because crossing strand one over two and then two over three is a different braid from doing them in the other order. Abelianization sends every generator to the same element and forgets which strands crossed, collapsing $B_n$ onto $\mathbb{Z}$, and the image of a braid word is its writhe, the signed crossing count. What abelianization discards is the order-sensitive content: the record of which strand crossed which, in what sequence.

What the value is. The writhe is a single-generator abelian quantity, one more generator alongside the units the dimensional unifier already carries, and it is decided for free at Tier 1. It is the coarse invariant the wide end of the gradient sees, and for a region whose strands do not observably cross it is zero, so reorder is licensed with nothing further to check. The non-abelian residue is what remains when the writhe alone does not settle the question, and it is a structured word over the crossing generators, not a number. That word is where an obligation can live when one is needed, and it is empty for the ordinary parallel region.

The operational reading. A crossing in a running Clef program is the return point Weaving the Braid names: the place where parallel work spawned from sequential control comes back and threads its result through what follows. The abelian projection records how many such return points a region has and with what sign; the non-abelian word records the order in which they resolve, and it carries weight exactly when two crossings share state, so that resolving them in a different order would compute a different result. When the strands are separable, the word is trivial and the region reorders. When they are not, the word carries the sequence, and the assembled section certifies that the sequence the compiler lowers is the sequence the source meant.

Weaving the Braid draws the line this page depends on, so it is enough to point at it. Categorical braiding, the monoidal law $a \otimes b \equiv b \otimes a$ that lets the compiler reorder two independent operations for locality, marks a strand as separable: reorder-freedom inside one strand. The braid is the non-separable weave of two strands together, the crossing between them that must not come apart. This sheaf is about the second thing. The writhe is what survives when separability holds everywhere; the non-abelian word is what appears when it does not.

Where the Live Braid Appears

A braid that has to be assembled, one the writhe alone does not settle, has its operational setting on the monad/applicative axis of the DCont/INet duality. The applicative side, pair, composes computations that are complete before either runs, with nothing passing between them; that is the separable strand, writhe zero, reorderable, lowered to the tensor path or to interaction nets under a confluence theorem discharged once over the rule system. The monadic side, bind, writes the crossing into its type: the second computation is a function of the first computation’s value, so what runs next depends on what just arrived. A region whose crossings are observable is one where bind is doing genuine work that pair cannot absorb, and the containment runs one way, pair derivable from bind and not the reverse, which is the asymmetry that orders the duality. The live braid is the DCont side of that boundary, where delimited control suspends a computation and resumes it with the spawned result threaded back through what follows.

Delimited control here is the established Danvy-Filinski shift/reset discipline, not a Clef invention; the mechanism and its lowering are the subject of the DCont representation work, which this page relies on without restating. The braid has no surface keyword. It is inferred from a region’s dependency structure the way every other region classification is, off the graph and not off a marker the developer writes, and the source spelling of a region that carries an observable crossing is unspecified. In Clef source, a region that crosses looks like ordinary sequential code with parallel work spawned inside it, plain identifiers and a computation expression, with the crossing structure a fact the analysis derives.

Where a region’s crossings are covered by an already-discharged composable set, the assembled section certifies the lowering and no obligation surfaces. Where they are not, the residue is a scoped, live-only obligation at a declared boundary, and the region runs under supervision the way a dynamic callee does in Weaving the Braid: the boundary is visible, the fallback is bounded, and the diagnostic names the site. The braid word itself, the generators $\sigma_i$ and the writhe, stays in prose and in the typing judgment, in the discipline the sibling documents keep for their own metatheory notation.

Where This Sits, and What Remains Open

The portable middle end emits func, cf, scf, arith, memref, and index, and the target legs, CIRCT for FPGA and LLVM for CPU among them, carry the crossing structure into target dialects at the backend handoff. The braid sheaf adds no middle-end operation; emitting a target-specific op inside the portable middle end would be a category error against the backend lowering architecture, so the crossing structure rides the existing structure maps as annotation, discharged at the same edges as every other sheaf. The demonstrated evidence for crossing-structure lowering is narrower than the braid it points toward: width inference has been taken through Vivado place-and-route on a compiled HelloArty design, the same design a triangle without mystery walks to an Artix-7 bitstream with the dimensional and coeffect guarantees intact into hardware. The end-to-end braid demonstration is planned, and the assembled-section machinery is design direction held apart from any claim of a shipping capability.

Three things are open, and we would rather name them than paper over them. The composition lemma, the statement that per-crossing witnesses assemble into a region witness across a stated class of crossings, is future work. The full assembly proof, that a global section of the braid sheaf exists whenever the composable set covers the region, is future work. Full braid unification, inference over braid equations with metavariables, is not known to be unitary and is an open research obligation, the case that someday earns its own pre-print, well past what a paragraph here can carry. The proposed capsule in terms and definitions records the braid type as non-normative for this reason: it reserves the term without asserting the theorem.

The gradient the framework holds everywhere is the shape this design keeps, broadest at ordinary concurrent programming and narrowing to the depth a given domain requires. The braid marks its non-abelian edge and leaves the wide end untouched, and the depth beyond that edge is depth a domain asks for, never a cost the everyday surface imposes.