Patch Theory for Entities
Version control has been trying to acquire a theory for twenty years, and it keeps almost working. Darcs shipped one in 2005 and it was never proven sound. Jacobson later gave it an algebraic footing with inverse semigroups, and Mimram and Di Giusto gave the whole idea a category-theoretic treatment where a merge is a pushout, which is what Pijul is built on. The mathematics is good. The problem is what it has to be a theory of.
A patch to a sequence of lines is defined by position, so inserting a line silently shifts the meaning of every later patch that refers to anything below it. Two edits a human would call obviously independent do not commute, because both are stated in coordinates the other one moved. Every line-based patch theory spends most of its machinery reconstructing intent that the representation destroyed.
Git conflicts when two people change different functions that happen to sit near each other, even though nothing about the changes interacts. They were written close together, and closeness is the only thing git can see.
One change to the model
Let N be a set of stable entity names, meaning functions, classes and methods addressed by identity rather than position, and let C be their possible contents. A repository state becomes a finite partial map.
s : N ⇀ C
A patch is a set of primitive operations, each targeting one name.
add(n, c) applicable when n ∉ dom(s)
del(n) applicable when n ∈ dom(s)
mod(n, c → c') applicable when s(n) = c
Each is a partial invertible map on states, so patches form a groupoid, the same structure Jacobson found in Darcs. Nothing here is new mathematics. What is new is that operations are keyed by name instead of position, and that single change does the work, because two patches touching different names now commute by definition rather than after a normalization pass.
Conflicts become decidable
Given a base b and two patches out of it, the merge is the pushout of that span, meaning the smallest state containing both changes that commits to nothing neither side asked for.
That second one is the whole conflict condition. It is decidable, checkable in time linear in the size of the patches, and there is no heuristic and no threshold to tune. Unlike "the changed line ranges overlap", disjointness of names survives formatting, reordering and unrelated edits elsewhere in the file.
To make merge total rather than partial, extend contents with an explicit conflict value, C^ = C ∪ { conflict(base, ours, theirs) }. The merge then always exists and is computed key by key. Because each key is an independent bounded join relative to the base, and products of semilattices are semilattices, idempotence, commutativity and a unit all fall out of the structure instead of needing separate proofs.
The same shape buys something else. A finite map with a per-key join is a map-CRDT, so Shapiro's strong eventual consistency result applies directly, and there is already a machine-checked proof of exactly this shape in Isabelle by Gomes and Kleppmann. So a single three-way merge is correct by the pushout argument, and any number of agents editing concurrently converge by the semilattice one. The entity model is where both apply cleanly at once.
The honest boundary
None of this proves that merging two edits inside the same function body is correct. That residual is ordinary text merge and is not provable in general, so the real theorem is a reduction rather than a total result.
Entity theory reduces whole-repository merge to a provably sound, convergent, name-keyed algebra, plus a per-entity content merge left as an abstract parameter.
That is weaker than "we proved merge" and it is the claim that is actually true. It is also more useful than it sounds, because it confines everything unprovable to a single function body rather than letting it range over a whole file.
What this looks like in practice
The most interesting case turns out to be where the right answer is to refuse. When both sides add different decorators to the same Python or TypeScript function, decorator application is function composition, so the stacking order changes behaviour. Putting @cache outside @auth serves cached responses without ever running the authentication check. There is no correct order to pick, so weave conflicts rather than inventing one, and we changed our own benchmark to stop scoring that refusal as a failure. Annotations in Java and C# are unordered metadata, so those still merge by set union.
The part that has not worked is on the reading side. Per operation, asking sem for a function plus its callers costs far fewer tokens than grepping and reading files. That did not survive contact with an agent loop. In a small three-armed comparison on real tasks, the structural arm burned more tokens than plain file tools on one run, and solved fewer tasks on another. The sample is too small to conclude anything, but a per-operation reduction is plainly not the same as a session-level win, and we have measured one and not the other.
What is open
Formalizing the model and the two theorems in Lean or Isabelle, so the core is machine-checked rather than argued in prose. The CRDT half can be instantiated from existing work and the inner merge stays abstract.
The part we are most confident about is the smallest. Choosing names over positions as the unit of change turns merge from a heuristic into a structure where a conflict has a definition, and two independent proofs apply to the same object. Everything after that is implementation, and implementation is allowed to be wrong in ways the model is not.