The SAGA Theorem: Architecture as Algebraic Geometry<br>Command Palette<br>Search for a command to run...

HHiroyuki Nakahata<br>I’m a software engineer in Japan. Outside of work, I enjoy horse racing.

div>p:first-child]:mt-0 [&>div>p:first-child]:pt-0 min-w-0 wrap-break-word [&_a]:break-all **:max-w-full">TL;DR

Every module passes review, yet the system as a whole is broken. This "locally correct, globally inconsistent" phenomenon has a name in mathematics: cohomology, specifically H^1.

AAT (Algebraic Architecture Theory) treats software architecture as a geometric object: generated from axiomatized facts called Atoms, cut out by laws, with obstructions appearing as cohomology classes.

Within AAT, I proved in Lean 4 a theorem that I call the SAGA theorem (SAGA Grounding Theorem). It is a comparison theorem: the H^1 grown on the architecture-semantics side coincides with the genuine Čech H^1 of the site generated from Atoms.

The proof took 352 cycles. For 347 of them, an automated AI loop accumulated impossibility theorems saying "this vocabulary cannot prove it" — until a single vocabulary shift, laws are equations, not predicates , broke the rock face in the final 5 cycles.

This article starts from a minimal map of algebraic geometry, then explains what the SAGA theorem says and why it matters for computer science.

1. Locally correct, globally broken

You have probably seen this before.

Every team's code satisfies its own review standards. Integrated, the system fails.

Each microservice honors its contract. The system-wide invariant is still violated.

Every refactoring step was safe. Stacked together, the original design intent is gone.

Linters, static analysis, and dependency graphs are good at finding local violations. But none of the situations above contain one. The problem lives not in any individual part but in how the parts are glued together.

Mathematics has studied exactly this phenomenon — locally consistent data that fails to glue globally — for the better part of a century. The theory of sheaves and cohomology. The obstruction to gluing a family of local data into global data appears as an element of a cohomology group called H^1. If the class is zero, the pieces glue. If it is nonzero, you are facing the kind of failure whose cause cannot be found by inspecting any single part .

AAT is a theory that takes this mathematics and runs it, seriously, on software architecture.

2. A minimal map of algebraic geometry for engineers

Before the main story, let me lay out the algebraic-geometry ideas this article relies on. Algebraic geometry is advanced mathematics, but to read this article you do not need rigorous definitions — just three ways of seeing, and a small glossary .

Way of seeing 1: equations and shapes are two faces of the same thing

In one sentence, algebraic geometry is the study of the shapes formed by solutions of equations, through the algebra of the equations themselves . The equation x² + y² = 1 and the circle in the plane are two faces of one object. Operations on the equation side correspond to operations on the shape side — this "algebra ⇄ geometry" dictionary is the heart of the subject.

Way of seeing 2: not "is it satisfied?" but "how is it imposed?"

As solution sets, x = 0 and x² = 0 are indistinguishable — both are "just the origin." But as equations they differ: x² = 0 carries the extra information of being "zero twice over." Modern algebraic geometry took off precisely by studying not the predicate-level information (satisfied / not satisfied) but the structural information of the equations themselves. In engineering terms: instead of only checking whether the tests pass, you carry around by what margin and for what reason they pass. This distinction becomes decisive later in the article.

Way of seeing 3: study locally, then glue

You cannot map the whole Earth onto one flat sheet, but you can make an atlas — a family of local maps. Algebraic geometry covers a shape with a family of local views, studies each view, and glues the results back into a global understanding. And sometimes everything works locally, yet the gluing fails . The tool that measures that failure is cohomology.

A small glossary

Term<br>Rough meaning<br>An engineer's mental image

ideal<br>a container holding a set of equations, closed under derivation<br>a rule set together with every rule derivable from it

quotient O/I<br>how the world looks after imposing the constraints I<br>the view through an interface after the constraints identify things

zero locus V(I)<br>the set of points satisfying all the constraints<br>the space of configurations passing every rule

cover and site<br>a way of covering the whole with local views, plus the rules for what counts as a valid covering<br>module / scope decomposition

sheaf<br>an assignment of data to each local view that stays consistent as views shrink<br>configuration values inherited without contradiction as scope narrows

cocycle<br>a consistent record of the mismatches along the...