DEV Community: Hiroyuki Nakahata

AI Reads Your Codebase. Then It Forgets Everything.

Hiroyuki Nakahata — Mon, 07 Sep 2026 15:02:08 +0000

AI Reads the Code. How Do We Keep What It Learns?

“Move email delivery to a shared asynchronous queue.”

The request fits in a sentence. The understanding needed to carry it out is scattered across more than 200,000 lines of code.

The sending function is easy to find. Follow its callers, though, and authentication codes and newsletters turn out to use the same implementation. One has expiration rules; the other has unsubscribe requirements. Queue delays and retries affect the conditions under which each feature works.

In an environment where the entire codebase cannot fit into context at once, an AI agent alternates between searching and reading. It cross-checks authentication flows, delivery settings, tests, and design documents to reconstruct dependencies and assumptions. Before it can judge the change, it uses a substantial number of tokens to recover meaning distributed across the code.

How much of that understanding will survive into the next task? Unless the relationships and the reasoning behind its decisions are retained in a reusable form, another session will repeat much of the investigation.

I want the understanding gained from reading code to persist as a structure that people and AI can share and use for the next change. Ontologies offer a starting point by making concepts and relationships explicit. I am developing a vision for a semantic layer that also captures meaning in context, supports consistency analysis, and lets us reason about what changes preserve.

The foundation for this work is AAT, Algebraic Architecture Theory, a theory I originated and continue to develop through mathematical research and software tools. AAT approaches architectural meaning through geometry. I want to turn that foundation into a way to understand a codebase and reason about how it can change while preserving what matters.

The Same Email Function Can Mean Different Things

Consider this function:

sendEmail(to, subject, body)

It sends a subject and a body to a recipient. Its role in the system emerges from its relationship to the code that calls it.

Use	What the email does in context	Requirements in this example
Two-factor authentication	Delivers a code needed to complete authentication	Delivery before expiration; clear rules about which code remains valid after a resend
Newsletter	Delivers information to subscribers	Consent checks; honoring unsubscribe requests during delivery

Put authentication emails in the same queue as a bulk mailing, and they may wait behind thousands of messages. Delivery can succeed while authentication fails because the code has already expired.

For newsletters, a subscriber may unsubscribe after a message enters the queue. Consent when the audience was selected and consent when the message is sent are distinct states. The system needs an explicit rule about which state governs delivery.

To assess the change, we need more than a label identifying each use. We need the relationships between the authentication request, code generation, delivery, and verification, as well as the point at which subscription status is checked.

The meaning of sending an email lies in its relationships with other operations and the requirements of its use.

By a semantic layer, I mean a layer through which we can access components, relationships, contexts, and the laws they must satisfy, together with references to their sources. An AI agent would retrieve the information relevant to a task, then follow those references to the original code wherever implementation details are needed.

AAT: Toward a Geometry of Meaning

I am building AAT as a theory of pure mathematics, starting from Atoms and Laws. An Atom is a basic unit of architectural fact. A Law is an equation over a family of Atoms. To apply the theory to code, we express observed facts in this vocabulary and choose laws for the properties we want to examine.

In the email example, we might record that authentication requests code delivery, or that delivery uses a queue, along with the context and source of each fact. We then specify the conditions we want to examine, such as those governing expiration and delivery times.

The perspective I take in AAT is that software architecture is a large system of simultaneous equations. The laws within each part and the conditions connecting those parts must hold together. A solution describes a consistent configuration under the selected laws.

The solutions to a system of equations form a space. Algebraic geometry studies such spaces. We can ask whether a configuration satisfying the conditions exists, whether configurations built separately can form a coherent whole, and what becomes possible when the conditions change. My aim with AAT is to treat architectural consistency and change as questions about this geometry.

Authentication, delivery, and subscription management can each have configurations that satisfy their own conditions. To form a working system, they must also agree where they meet, for example on which authentication code is being delivered and when delivery takes place.

In mathematics, assembling local configurations into a whole on the basis of agreement on their overlaps is called gluing. In this framework, we study failures of global consistency as obstructions to gluing, and changes in configuration as problems of deformation.

I call this research program Semantic Geometry of Architecture. It studies the space of consistent realizations of meaning: their existence, obstructions, deformations, and relationships across different ways of reading an architecture.

Once our understanding of an implementation connects to such mathematical objects, we can move from asking what is present to asking what is consistent and how it can change. That is the scope I want the semantic layer to support.

The Atlas Theorem: Choosing How Much Detail to Read

To use this layer across a 200,000-line codebase, we must choose both the scope and the level of detail appropriate to the question. For asynchronous email delivery, expiration and retry rules deserve early attention. Does every styling detail in the HTML template need the same scrutiny?

Yet omitting the logic that inserts the authentication code into the message could discard something essential. What we can leave out depends on what we need to establish. AAT treats this choice mathematically.

We begin by grouping together things that the selected laws cannot distinguish. AAT provides a construction of a canonical reading that preserves the evaluations of those laws. In an expiration analysis, for example, the idea is to retain the information needed to evaluate the relevant conditions.

We then ask whether preserving information within each part also preserves the diagnosis of the whole. This is the question addressed by the Atlas Theorem.

Atlas Theorem: A change in resolution preserves diagnostics when the required conditions hold.

If both the finer and coarser readings retain enough information for the selected laws, and their comparison satisfies the specified conditions, their diagnostic classes in first cohomology correspond one to one.

Here, first cohomology is a mathematical tool for studying discrepancies that satisfy specified consistency conditions and identifying the obstructions that remain after local adjustments. A one-to-one correspondence of classes means that, under the theorem's conditions, a coarser reading neither loses diagnostics nor introduces new ones. The parts, their overlaps, and the data on those overlaps must all be appropriately related.

Applied to code comprehension, this would let us say, with mathematical justification: “For this property, reading at this resolution preserves the diagnosis.” Once a model extracted from the code is shown to satisfy the Atlas Theorem's conditions, omitting detail preserves the diagnostics associated with the selected laws.

An AI agent could use that guarantee to choose a reading resolution, then inspect finer detail when it needs to investigate another property or edit the implementation. Reliable model extraction and a way to select laws appropriate to the question are the tools needed to make this workflow possible.

The SAGA Theorem: A First Realization of Semantic Geometry

Once we know what to read, we need to determine whether the requirements we find can hold together.

Suppose an authentication code expires five minutes after issuance, but the shared queue can take ten minutes to deliver it. The authentication service rejects expired codes, and the delivery service sends the message. Both follow their own rules, yet the user cannot complete authentication.

An engineer can approach this problem from two directions. One is to consider changes that restore consistency, such as separating the authentication email queue. The other is to express the required relationships as equations, such as those relating expiration and delivery times.

The SAGA Theorem establishes a mathematical correspondence between two independently constructed ways of describing obstructions, one based on each perspective.

On the semantic side, the construction starts from the repairs allowed within each part and the ways those repairs combine. On the geometric side, it starts from the law equations and the algebra describing their obstructions. Because the constructions have different starting points, their agreement requires proof.

SAGA Theorem: Semantic and geometric accounts of obstruction correspond.

Choose finitely many parts covering the subject of analysis. When their local data satisfy the required correspondence and consistency conditions, the cohomology constructed from semantic repairs is isomorphic to the cohomology constructed from the equations and obstruction algebra. The obstruction classes correspond as well.

An isomorphism here allows us to move between the two descriptions while preserving the mathematical structure used to study obstructions.

The power of the SAGA Theorem is that we can take a semantic question about what prevents local repairs from fitting into a consistent whole and bring it into algebraic and geometric computation. For a model satisfying the theorem's conditions, the correspondence between the computed obstruction and the semantic obstruction is mathematically guaranteed. People and AI can use that result as evidence when evaluating repair proposals.

For the email system, I want to model the allowed repairs and the data shared between operations, then connect the problem of making authentication and delivery consistent to this analysis. The SAGA Theorem connects reasoning about meaning with geometric computation. It is the first realization of the Semantic Geometry of Architecture program.

Annapurna: Preserving Relationships Through Change

Moving to asynchronous delivery may involve a dedicated authentication queue, invalidating old codes when a new one is sent, or checking subscription status immediately before delivery. The change extends beyond the sending function into relationships between operations.

Identical “delivery succeeded” records before and after a change do not establish that authentication and subscription requirements have been preserved. We need to know whether the recorded information captures the property we want to compare.

In the research series I call Annapurna, I have studied how comparisons can be carried through changes in viewpoint and structure. Its later results include the following.

Annapurna results: Classify changes that preserve a comparison, and establish distinctions that observation alone cannot detect.

Within the specified structures, we can classify which changes to the two objects preserve their comparison. This classification carries over when the presentation of the inputs changes. There are also examples in which two changes produce identical observations through specified coefficients, yet only one is compatible with the comparison.

In the latter case, processing the observed values afterward cannot recover the distinction. The information needed for that decision is absent from those values.

The email delivery log is an illustration of the problem these results address. To assess a change, we need records that let us compare structural relationships as well as outcomes.

I want to use the Annapurna results to examine a practical question mathematically: “If we change one side, how must we change the other to preserve their relationship?” Classifying the changes compatible with a comparison provides a mathematical basis for that analysis within the specified structures.

For asynchronous email, the application would be to ask how code issuance and resend rules should change alongside the delivery mechanism. What does the proposed modification preserve, and which changes must be made together to preserve it? To support that analysis, the semantic layer would record how operations correspond before and after the change, which requirements must carry over, and the information needed to check the theorem's applicability.

The Major Theorem Ahead: Representing Meaning Geometrically

The results so far answer particular questions within semantic geometry. Beyond them, I am working toward a major theorem that represents realizations of meaning as a geometric object.

A realization of meaning is a consistent configuration for the chosen Atoms and laws. In the email example, this would be a configuration in which authentication, delivery, and subscription management satisfy their local conditions and agree where they interact.

The goal is first to define these realizations independently, then show that they are naturally described by maps into a geometric object. This property is called representability. It would let us study questions about configurations satisfying the conditions as properties of the corresponding space.

Proving this major theorem remains a research goal. I want it to connect engineering questions to geometric ones:

Engineering question	Geometric question
What does this refactoring preserve?	Is there a correspondence preserving the selected semantic structure?
What else must change when delivery becomes asynchronous?	Which deformations are possible while the conditions continue to hold?
Why does fixing individual operations still fail to make the system consistent?	What obstructs gluing?
Can the problem be resolved under these constraints?	Does a realization satisfying the conditions exist?

Computing actual repair proposals will also require algorithms that work with finite inputs. I want to pursue both the theorem and the implementation work needed to turn its consequences into computations, so that refactoring and repair can be treated as geometric problems.

The Workflow I Want to Build with ArchMap, ArchView, and ArchSig

I am developing ArchMap to record observed structure, ArchView to visualize it, and ArchSig to analyze it under selected laws. LawPolicy specifies the laws, which are combined with the observations for computation. Here is the future workflow I want to build on that foundation.

Return to the 200,000-line codebase and the original request:

“Move email delivery to a shared asynchronous queue.”

The AI first queries ArchMap for the contexts in which email delivery is used. It retrieves the operations involved in authentication and newsletters, their requirements, and their source references, together with the shared data and relationships needed for the decision.

In ArchView, a person examines the same structure. They follow code issuance through delivery and verification, checking which operations the AI selected for modification and why. Eventually, linking changes in the level of visual detail to mathematical reading resolutions could make it clear which information each view preserves.

ArchSig analyzes the selected scope under the selected laws. I want to extend it to check the conditions for comparisons across resolutions and to handle structural correspondences before and after a change. The results and supporting evidence would serve both the AI's explanation and human review.

With that information, the AI reads the implementation details it needs: code issuance, queue submission, resend handling. After making the change, it updates the relevant observations and repeats the diagnosis and comparison for the same objective.

The semantic structure used to reach the decision remains available to the person reviewing it and to the AI in the next session.

Putting the Geometry of Meaning in the Hands of People Who Build Software

What I want to create with AAT is a development environment in which people and AI share an understanding of software's meaning and explore the changes that understanding makes possible.

Faced with 200,000 lines of code, we trace the relationship between authentication and delivery. We introduce a proposal for asynchronous processing and inspect the requirements it must preserve and the operations it needs to adjust. One repair leaves an obstruction; another configuration is consistent. We can explain why using both the original code and mathematical evidence. That is the development experience I want to build.

In that environment, a codebase is both an implementation to read and a geometric object through which to reason about what can remain and what can change. Refactoring becomes a question about correspondences that preserve semantic structure. Repair becomes a question about the existence and deformation of configurations satisfying the conditions. I want the individual difficulties of everyday engineering to become approachable through a shared body of mathematics.

Through the SAGA Theorem, the Atlas Theorem, and Annapurna, I have been building that foundation in theorems and counterexamples. We already have verifiable results on comparisons between meaning and geometry, changes in resolution that preserve diagnostics, and structural comparison and information loss. I am also pursuing formal verification in Lean so that others can check the foundations themselves. The work toward the major theorem continues from those results.

There is still substantial tooling work ahead: reliable extraction and updates, usable ways to query meaning, and evaluation in actual development. I want to measure not only how much code and how many tokens an agent consumes, but whether it retains the requirements that matter and carries its understanding into the next session. Each of these is part of bringing the mathematics into the hands of people who build software.

In this future, using the tools would not require every developer to learn algebraic geometry. People and AI would express what they want to build and what they want a change to preserve. The theory and tools would connect those questions to semantic structure, perform the computation, and return results with evidence. As AI becomes capable of proposing more changes, mathematics can help us explore those possibilities with greater confidence.

Treat software's meaning as geometry, and put that geometry in the hands of the people building it. That is the ambition behind Semantic Geometry of Architecture. From understanding 200,000 lines of existing code to exploring configurations that have yet to be implemented, I want people and AI to be able to reason about the same space of meanings.

Repository: AlgebraicArchitectureTheoryV2

The Goddess of Plenty Smiles at the Summit: 16 Theorems, 2 Refutations, and the Structure of Software Design

Hiroyuki Nakahata — Sun, 06 Sep 2026 13:43:33 +0000

Every test passes. Every metric looks the same. Is that enough to judge whether a design change is sound?

There are pairs of changes that the observations of AAT (Algebraic Architecture Theory) cannot tell apart — even though one keeps the system coherent and the other breaks it. And the difference cannot be recovered by any post-processing of the same observed values. This summer, that limit became a theorem, machine-checked in Lean 4.

In five weeks starting August 2, 2026, we proved sixteen theorems and refuted two claims. An AI agent loop did the implementation; I set the goals, reviewed the proofs, and made the calls. This article is a record of what we found, and of the road that led there.

1. AAT: Algebraic Architecture Theory

AAT is a research program that analyzes software architecture with the tools of algebraic geometry. It starts from observing source code. Implementations are abstracted into components called Atoms; the specification is written as a family of equations called laws. Design coherence then becomes a mathematical question: does local correctness glue into a consistent whole?

A running example from earlier articles is the one-cent drift. Three modules of a commerce service — checkout, payment, and ledger — each pick a rounding rule that passes review on its own, and the card gets charged one cent more than the screen displays. Each module follows its own rules. The whole still doesn't add up.

In this example, each module's implementation is an Atom, and an equation like "the amount displayed equals the amount charged" is a law. A quantity that aggregates the local mismatches into a global one, like that one cent, is a cohomology class, and reading it off to point at the inconsistency is what we call diagnosis. The earlier work — the SAGA and Atlas theorems, each with its own article — made all of this measurable.

A view is the result of reading the code at a particular resolution and from a particular angle; a service-level view and a module-level view are different views. Carrying an analysis result from one view to another is transport, and swapping out the base the analysis stands on is base change. In the one-cent example, adding settlement as a new context changes the very ground of the analysis; that is one instance of base change. When an operation survives such a swap, we say it is closed under the swap.

Every theorem in this article is machine-checked in Lean 4, a proof assistant that mechanically verifies whether a proof establishes the statement written down.

The question of these five weeks: when you change how you look, or the ground you stand on, how much of your analysis and your comparisons survives the move?

2. Five things we can now say about software design

1. Observation alone cannot always tell a sound change from a breaking one.

Take two candidate changes. Test results, metrics, every value in AAT's observations: identical. Yet one preserves global coherence and the other destroys it. Such an example has been constructed, and no aggregation or post-processing of the observed values can distinguish the two (Section 5). The practitioner's intuition — "you can't manage architecture by numbers alone; you have to look at the structure" — is now a theorem inside the model.

The information you need lives not in the numbers but in the correspondence that connects the before and after of a change. So the next move is not to inspect change proposals after the fact; it is to derive the required companion change directly from that correspondence.

2. The degrees of freedom in a fix are now known exactly.

You change one side of an interface. How can the other side be fixed so the two still agree? The theorem describes the full space of compatible fixes (Section 5). Find one, and every other fix can be derived from it — none missing. A design review can move on from "is this fix acceptable?" to "how much freedom does this fix have, and does the choice matter?"

3. Harmless-looking normalization stays in your design.

Some formatting and normalization passes are not supposed to change meaning, and as far as observation goes, they don't. Even so, there are cases where the local normalizations scattered across a system cannot, in principle, be merged into one globally consistent operation (Section 4). Fixing a convention for "what counts as the same meaning" does not end the design question; which operations remain sound under that convention is itself part of the design. So normal forms deserve to be first-class citizens of the design, not an afterthought.

4. We now know exactly when divide and conquer is honest.

Analyze each module, then combine the results into a conclusion about the whole. The condition for this to be sound is now a theorem, in necessary-and-sufficient form (Section 3). We also proved that analysis results do not depend on how the code happens to be written down. Together, the two mean analysis need not start over on every change: there are precise conditions under which re-checking only the changed part and its overlaps is enough. That matters at scale — for large codebases, and for fleets of AI agents developing in parallel.

5. A change of meaning cannot pass through the label layer.

On a fixed base, relabeling alone — types, tags, and other metadata — cannot move observable meaning. A change of meaning can live only on the side where the base itself moves. This, too, is a theorem (Section 8). There is now a structural reason why metadata edits preserve meaning.

The one-cent drift connects here as well. That example showed that the failure of locally correct modules to glue can be measured. The new results establish where the limits of that measurement lie. The boundary between what can be measured and what in principle cannot is now drawn as a theorem.

3. Three layers of theorems

The sixteen theorems answer three questions.

Can analysis results be carried between views of different resolution and level? Yes, and by any route: the result of a service-level analysis and the result of a module-level analysis can be traded back and forth without loss, and moving across levels loses nothing either. Catch the one-cent drift at service granularity or at module granularity; either way, it can be matched up as the same inconsistency.

When the base of the analysis is swapped, which operations survive as theorems? The answer is a table of conditions, direction by direction: classifying the operations that vary with the base; base change along refinements that carve the base finer; and lifting, which extends a partial result one level up. Each stands as a theorem with its scope pinned down. The point is that not every direction holds unconditionally. That dividing line — which direction holds under which condition — is what this layer establishes.

When may a conclusion about the whole be drawn from finitely many parts? A necessary and sufficient condition is now settled for when partwise analysis lifts to the whole, and for how far diagnosis survives transport. The negative side is proved as well: an arbitrary choice of covering can change the diagnosis of the very same system (Section 7). Unconditional divide and conquer fails, which is exactly why a condition is needed — and the condition is exact, nothing extra and nothing missing.

All three are classifications, not conjectures. The boundary — which operations are closed, and where closure fails — is drawn with proofs.

4. The normalization factor that cannot be removed

The strangest finding is an invisible factor lodged inside comparisons.

AAT generates comparison morphisms between two views: before and after a change, a fine view and a coarse view. Ideally a comparison is invertible; then the two views can be traded back and forth without losing information.

A comparison is a family of maps, one per object. For the comparison β that the system actually generates, each component provably factors as

$$
\beta = E \circ \alpha
$$

first through α, then through E. Here α is the ideal comparison prescribed by the theory, and it is provably invertible. And β is the concrete comparison assembled from actual input. How does the concrete deviate from the ideal? The deviation is exactly E, and this factor has three properties at once.

First, it is idempotent:

$$
E \circ E = E
$$

Applying it twice is the same as applying it once, like running a code formatter twice.

Second, it is invisible to observation. E moves no observable quantity; under the observations considered here, it cannot be told apart from a map that does nothing.

Third, it is nevertheless not invertible. Wherever E actually fires, it cannot be undone, and therefore β as a whole is not invertible either.

So what breaks the invertibility of comparisons is a normalization factor that appears, to observation, to do nothing at all. And invertibility does recover — if you restrict where you stand. In the raw world, β is not invertible. Restricted to the image — the values that actually remain after E — it becomes invertible. And on observable quantities, β and α agree exactly. The failure is not monolithic; it splits into these three stages. That recovery on the image will matter later: it is the doorway to the next stage of the research (Conjecture A, Section 11).

Then why not simply remove E? Bundle it into one natural operation running through every object, and subtract it from the system uniformly.

That is impossible, and this too is a theorem. From the same starting point, compare normalizing at A and then moving to B, against moving to B first and normalizing there. A concrete counterexample exists where the two disagree. Compatibility with movement between objects is what mathematics calls naturality: E is a perfectly usable normalization at each object, yet it cannot be bundled into one natural operation compatible with movement.

A structure invisible to the observations at hand, one that decides whether comparisons succeed, and that cannot be removed: it was there all along.

5. Degrees of freedom, and the limits of observation

The strongest result is a classification of the freedom in changes. The subject is compatibility of changes across an interface.

The setup: two sides joined by a single comparison, and a change applied to each side. We consider reversible changes here. Which pairs of changes preserve the comparison? In other words, when you change one side, which companion changes on the other side keep the whole consistent?

"Preserve" means this: changing one side and then comparing gives the same result as comparing first and then changing the other side. When that holds, the pair of changes is compatible with the comparison.

The theorem settles four things at once.

First, the compatible pairs of changes form a group: operations that can be chained and undone, with "do nothing" as a member. Integer addition is the model case.

Moreover, once one compatible companion change is found, every other one can be expressed as a difference from it. Any of them could serve as the reference; none is privileged from the start. This structure is called a torsor. The space of compatible companion changes has exactly that shape.

Second, for the comparisons the system actually generates, source-side changes can always be carried across, and the companion options on the other side form a coset: one solution multiplied by the elements of a subgroup. That subgroup is characterized by concrete conditions on the input data.

Third, the classification does not depend on presentation. The same design can be written in many forms: different file splits, different orders of definition. Rewrite first and then generate the comparison, or generate and then transport: the classification lands in the same place. What this analysis measures is not the style of the writing but the structure of the meaning — and that is what the proof establishes.

Fourth, observation cannot decide this classification. In a fixed example, compare two options.

In the fixed example	Option A	Option B
Change applied to the source side	the same change	the same change
Response on the other side	the required companion change	nothing
Result under the observations considered here	same as B	same as A
Compatibility with the comparison	preserved	broken

The correct companion change is uniquely determined. Yet from the observations alone there is no telling whether that change was made or nothing was done — and provably, no post-processing recovers the difference. The information that singles out the one required companion change is lost by observation.

6. The plan: turning a metaphor into theorems in five stages

The rest of this article is the record of the five weeks that led there. In hindsight, it was a climb up a mountain whose map was wrong.

The early theory notes described AAT's construction as "Grothendieck-like." Grothendieck rebuilt algebraic geometry in the twentieth century; much of the machinery connecting the local and the global goes back to him. But "Grothendieck-like" was only a metaphor. How far does analysis survive moving between views and swapping bases? The road from metaphor to theorem was laid out as a five-stage plan:

Gr0 Metaphor: said, not shown
Gr1 Formalization: the claims written as mathematical statements
Gr2 Constructed instance: an object that actually satisfies them
Gr3 Pseudofunctorial coherence: transport between views agrees along any route
Gr4 Base-change completeness: every operation closes, base swaps included

The first two stages were already done in the theory notes. To climb the rest with theorems, eighteen research cards were issued starting August 2. A card is a document that pins down the theorem to prove, its scope, and its completion criteria.

7. The climb: from the foothills to Gr4

The first summit fell on day one. On August 2, the construction of Atom transport was proved: Gr2 reached. On August 8, the Atlas theorem. On August 18, transport across levels of views was proved to agree along any route: Gr3 reached. Four of the five stages, in under three weeks.

On the way, on August 11, came the first refutation. The plausible claim "changing the structural covering (a way of covering the whole with finitely many parts) does not change the diagnosis" turned out to be false. The refutation was not wasted. Its counterexample revealed where the residual — the quantity measuring a failure to glue — can appear and where it never can, and that distinction fed straight into the design of later counterexamples. A refutation becomes reconnaissance for the next route. That pattern would repeat for all five weeks.

Only Gr4 remained, and this was the real mountain. The foundation is a construction that takes two bases and builds a new one from the pairs that agree over a common base (the fiber product; call it crossing bases). The foundation theorem was proved on August 25, but it took 111 cycles (a cycle is one loop iteration: the agent adds one step of proof and records evidence and an audit trail). Most earlier cards had finished in a few to a few dozen cycles. That is the gradient of this mountain.

Standing on the foundation, we could finally see the terrain: this mountain has no single route, because it has no single summit. The work was split into six cards, one responsibility each, and between August 26 and September 4 all six were settled by proof, one of them taking 84 cycles and nine revisions of its card. The full record of all eighteen cards is in the appendix.

8. The mountain in the plan did not exist

All six cards were settled by proof. And yet Gr4 itself — the original goal: swap the base, analyze there, carry the results home, every step of the round trip a theorem — turned out to be false as stated. The content of the proved theorems itself showed that the mountain in the definition does not exist. On September 4, we decided not to write a completion record for Gr4. You do not file a summit report for a mountain that was never there.

What failed comes down to two things.

First, vertical rigidity. Call vertical the direction in which only extra labels are swapped while the base stays fixed. No meaning-moving transformation can be placed in that direction; such transformations have to be handled horizontally, where the base itself moves.

Second, the comparisons the system generates are not invertible, because, as Section 4 explained, the invisible factor E sits inside them.

So where did this conclusion come from?

9. The turning point: refutations became the harvest

The turning point came right after the hardest pitch, the lift to the upper level (84 cycles, nine revisions). That climb left behind not only its summit theorem but a pile of counterexamples, because every revision had deposited refutation theorems in Lean — each one saying, in effect, "not in this form."

Surveying the pile after the pitch, we noticed the counterexamples fell into three families.

Attempts to place a meaning-moving transformation in the vertical direction had failed independently on two cards, and both were resolved by moving the transformation to the horizontal side.
Lossy collapses were never going to yield invertibility. Identify two objects that differ only in decoration, and the map sends different things to the same place — no longer one-to-one, and a correspondence that is not one-to-one can never serve as part of an invertible comparison.
Fix all the route data and swap only the comparison component joining the two sides, and glueability flips, while to observation nothing appears to change at all.

Line the three up and a common trait appears: something observation cannot see, yet which decides the strict properties — invertibility, glueability — and lurks in both the vertical and the horizontal directions. And none of these refutations had been designed to show this. They are the traces of the structure pushing back in the middle of proofs aimed elsewhere. If so, one structure must be behind them all. That structure was exactly the normalization factor E of Section 4.

So the sixth card, originally the summit card that was to close out Gr4, was redesigned into the card that would hunt down the structure behind the counterexamples. The redesigned card was settled by proof on September 4 (the 9/4 row in the appendix): the identification of E. The counterexamples had not been wrecking the mountain. They had been teaching us that there was a mountain that no one-dimensional map — no single yes-or-no ruler — could capture.

Beyond that identification, the refutation of September 5 (Section 4: the impossibility of bundling) turned E from something to erase into something to classify, and that decision shaped the final theorem of September 6 (the classification of Section 5). In hindsight, this change of course led to the highest summit of the five weeks.

The same pattern runs through all five weeks. The August 11 refutation supplied the method for designing counterexamples; on the cards of August 28 and 29, the content of a refutation directly became the design of the next revision, which was then proved. Individual refutations shaped the next card, and their accumulation rewrote the plan itself. In the Atlas article, I wrote that the four refutations were the best part of the climb. This time the same thing happened not inside one theorem but across the whole series. The map being wrong about the mountain: that itself was the harvest.

10. The descent was the real test

The work after standing on a summit was the real test, because declaring a proof complete and being able to trust that declaration are two different things.

Here is how the loop runs. The agent works cycle by cycle toward the claim and completion criteria fixed on the card, recording evidence and an audit trail as it goes. Completion requires, in order: a full completion report, four independent reviews of the same proof target (two mathematical, two Lean), and a cross-check of the evidence records. Only then is a card settled.

Over the five weeks, the procedure stopped exactly where it should have.

Two cards halted at the first step (writing the claim down in rigorous types) when defects in the claims surfaced; I revised the cards before the loops resumed.
One card halted at the provenance check of its evidence.
Two cards had "proof complete" declared, after which the audit found defects in the records and rolled the state back; completion was then redone. In both cases the defect was in the evidence records, never in the theorem itself.

Those last two matter most. The summit had been declared, and the descent checks rejected it. Checking the evidence with the same rigor as the theorems is what makes the declarations trustworthy.

Over the five weeks, the Lean code grew to 791 files and roughly 300,000 lines, and the agent loop consumed about 24 billion tokens. Through all that volume, the policy of stopping on doubt was never relaxed — and I believe it is precisely because the system was built to stop that sixteen theorems in five weeks could be delivered without burning trust. Mathematics aside, the speed itself is an empirical result: a formalization that starts from observing source code can run this fast.

11. Higher peaks beyond

From a summit, you see the next mountains. The harvest of the traverse includes three conjectures. None are proved, but for each, the object to construct next is already in view.

Conjecture A (making normal forms first-class). Section 4 noted that invertibility recovers on the image, the world of values that remain after E. The next construction promotes that world to a first-class citizen of the analysis. There, the founding claim of the theory — that AAT's conclusions factor through the layer of Atoms — is expected to become a theorem of the form "the two worlds carry essentially the same analysis." Mathematics calls the construction a Karoubi envelope, and this kind of equivalence a Morita equivalence.

Conjecture B (an invariant finer than the cohomology class). Swap the base, and the obstruction's cohomology class stays fixed; yet glueability can change. So there are differences the cohomology class cannot see. The next construction defines a finer invariant — a quantity that stays fixed no matter how things are presented — that captures those differences. The torsor classification of Section 5 is constructive evidence that such a quantity exists.

Conjecture C (capturing the whole in finitely many parts). The condition of Section 3 for concluding from finitely many parts looks like an instance of what topology calls compactness. The next construction carries the covering classification into topological language.

And beyond the three conjectures stands the summit theorem of the whole program: that the space of meanings is representable as what algebraic geometry calls a scheme, a space glued together from solution sets of equations. The calculus settled over these five weeks tells us what can be carried, which changes preserve comparisons, and what observation loses. The route to that summit will be drawn on this map.

12. Why "the Goddess of Plenty"

We named this family of theorems Annapurna.

On June 3, 1950, a French expedition led by Maurice Herzog stood on the summit of Annapurna in the Himalayas: the first ascent of an 8,000-meter peak in history. But Annapurna was not the mountain the expedition had set out to climb. That was Dhaulagiri, next door. After long reconnaissance, the team concluded there was no route up Dhaulagiri and switched objectives. The maps of the day were wrong; even the glaciers were misplaced. They had to begin by searching for the mountain they would climb. The price was paid on the way down, where severe frostbite cost the climbers fingers and toes. And Annapurna, in Sanskrit, means "she who is filled with food": the goddess of plenty, of harvests.

The mountain drawn on our map did not exist either. We navigated by the actual terrain instead, and turned refutations into the harvest. For these five weeks, no name could fit better.

Five weeks ago, the goal stood on the map. Now it is the map that has been redrawn, and the mountain actually climbed bears the name. The goddess smiled, not because the climb went according to plan, but because the map's mistake was turned into a harvest.

Appendix: the full five-week record

When	What was settled	Verdict	Cycles
8/2	Constructed instance of Atom transport (Gr2 reached)	proved	16
8/2–8	Locating where obstructions appear	proved	5
8/2–8	Constructibility of finite canonical resolutions	proved	6
8/8	Atlas theorem (resolution invariance)	proved	31
8/11	Structural covering invariance	refuted	7
8/11	Characterizing where uniform invariance fails	proved	27
8/15	Transport coherence	proved	5
8/16	Transport of geometric views	proved	7
8/18	Cross-level transport (Gr3 reached)	proved	22
8/25	The foundation: crossing bases and base change	proved	111
8/26	Classifying base-indexed operations	proved	20
8/27	Conditions for lifting from finitely many parts	proved	8
8/28	Conditions for diagnosis to survive transport	proved	28
8/29	Base change along refinements	proved	4
9/1	Lift to the upper level	proved	84
9/4	Gluing of disconnected configurations (the redesigned sixth card)	proved	21
9/5	Can normalization be bundled into one natural operation?	refuted	4
9/6	Transport of comparisons, and the information observation loses (the final theorem)	proved	30

Cycles is the number of loop iterations to completion.

Repository: AlgebraicArchitectureTheoryV2

Universality Lives in Structure

Hiroyuki Nakahata — Tue, 18 Aug 2026 14:04:41 +0000

If you are a software engineer, you have probably dreamed of building something general — software that many people use.
An open-source project with ten thousand GitHub stars.
A social network with hundreds of millions of users.
The mission-critical systems that move the world.
And the operating systems that hold it all up.
In the world of software, we tend to speak of value as "usable in more cases."
And generality is, in practice, genuinely important.

But generality does not last forever.

Flash, once at the height of its glory, faded with its era.
XML, built to be the general standard, lost the mainstream to another format.
jQuery, which once ran nearly every page on the web, is rarely chosen for anything new.

Generality depends on the breadth of its cases

Generality means covering many cases.
A web framework like Rails or Laravel can build most web applications on its own.
If I were advising a beginner, I would point them to one of these first; learn it, and some kind of work will be within reach.

But this "many cases" keeps shifting with the times.
SPAs, PWAs, WebAssembly.
So generality, by its nature, erodes with time.
All things are impermanent, as the Buddhist phrase goes.

Is there anything that does not change?

Here, instead of adding more cases, try changing the conditions under which you look.
Change the era.
Change the culture.
Change the representation.
Change where you observe from, and at what resolution.
Then you start to see what changes and what does not.

Relativize, and the essence remains

What remains, then?
For Rails, perhaps its conventions.
Even as eras and cultures change, governing a codebase by convention keeps its value.
For React, perhaps what remains is having brought the pure function — an idea from functional programming — to the frontend.
Rendering the view as a pure, idempotent function is a benefit that outlives the era.

Only by changing how you look does the outline of the universal become visible.
This is not to say that everything is relative.
We relativize in order to learn what is not relative.
What survives relativization — that is universality.

The essence of Buddhism

Buddhism is said to be some 2,500 years old.
Over that long history it spread across East Asia and divided into many schools.
Doctrine, practice, precepts — they differ from school to school.
What survived was not the answers.
It was the questions.

Why do we suffer?
Where does attachment come from?
What is the self?
How should we live?

The form varies, school by school, relative to place and age — and something does not.
The questions themselves are the universality.
The teaching that preached impermanence has itself lasted 2,500 years.

Lehman's questions

Back to software.
Fifty years ago, Meir Lehman published his laws of software evolution.
Eight laws, describing how software that is used in the real world goes on changing.
Software in use must keep changing, or it loses its value.
The more it changes, the more complex it becomes.
Features keep growing, and without upkeep, quality appears to decline.
Evolution proceeds through layers of feedback.
There was also a law that said the work rate of a development organization holds roughly constant.

Not all eight laws are universal.
Change the condition called "era," and they separate: some remain, some age.
The constant-work-rate law aged.
It was a statistic drawn from the development organizations of its day, and those organizations no longer exist.
Right now, AI is changing the work rate itself.
But the law that software in use keeps changing — that law remains.
It is not a statistic; it follows from the relationship between software and the world.
Software connected to reality changes the world, and then has no choice but to keep adapting to the world it changed.
That round trip does not disappear, however many languages and frameworks come and go.
What Lehman left behind was not the statistics of an era, but the questions born of a relationship with the world.

The age of AI

We are living through a turning point.
AI now writes code faster than humans do.
AI is good at finding what is common across vast amounts of data.
The pace at which general software and frameworks appear will quicken dramatically.

But by the same token, the era itself turns over faster.
The tips that count as general in August may be obsolete by December.

What lasts? What holds when the conditions change?

Precisely because this is the age of AI, universality is what holds value.

AAT: Algebraic Architecture Theory

What survived in Buddhism, and what survived in Lehman, was questions.
Then what do the answers look like — the ones that withstand the questions and remain?
I believe they take the form of structure.
Looking back: Rails' conventions, React's pure functions — both were structures.

AAT, the theory I work on, is in pursuit of universality.
It is an attempt to read the structure of software architecture in the language of algebraic geometry.
What it measures is the gap between the parts and the whole.
Each individual change is correct, and each passes review.
And yet the whole, glued together, is somehow broken.
AAT gives that phenomenon — the one every engineer has lived through — mathematical form.

Software metrics are usually decided by people.
We agree on a way of computing something, and then we measure it.
That is why metrics are countless, and why the answer to "why measure this one?" is weak.
The quantity at the center of AAT is a little different.
Pose the question — why can the parts be correct while the whole fails to assemble? — and mathematics fixes, all by itself, the one place where the answer can live.

H¹

Not chosen.
Forced.
Generality can be chosen.
Universality cannot.

The Atlas Theorem, proved just recently, formalizes exactly this universality.
When you observe source code, there is a resolution to the reading: coarse or fine.
What the Atlas Theorem gives is a sufficient condition under which the result of the review does not change when the resolution does.
Change the resolution of your reading — relativize it — and the obstruction that still remains is the universality.

To claim universality is to take on an obligation of proof.
Change the observation.
Change the representation.
Change the coefficients.
Every condition you move adds one more theorem to prove.
The Atlas Theorem is one of them, and the road goes on.
Universality does not come free.
The conditions for survival are themselves the content of the theorems.

What remains

Generality changes with the times.
Relativize — move the conditions of seeing — and universality dwells in what still remains.
And universality lives in structure.
With the weapons of algebraic geometry, AAT is closing in on the universal structure of architecture.

Uncharted Waters: Thirteen Rules for Not Trusting an AI's Proofs

Hiroyuki Nakahata — Sun, 16 Aug 2026 16:10:31 +0000

TL;DR

I want to hand an AI agent a multi-day job and have it run to completion. This post collects the rules for that — thirteen of them. Never let the loop rewrite its own spec. Enumerate up front what counts as evidence of "done." Review in independent parallel, never by majority vote. If verification didn't run, the answer is unknown, not pass. Nine more inside
The rules run in my repository. In fifteen days of August 2026, this loop proved seven theorems and refuted one. About 104 cycles, roughly 67,000 lines of Lean 4. All seven proofs cleared four independently running adversarial review lanes
The theorems are the main results my research program (AAT) set as its goals — nothing like famous open problems. But each was a multi-day proof target where refutation and revision were live possibilities. The outcomes were genuinely unknown
A three-way division of labor: Claude (Fable) drafts the goal cards and runs adversarial reviews, Codex (GPT-5.6 Sol) drives the proof loop, and a human makes the rulings
I make no claim that these thirteen rules are optimal. This is an N=1 record, with no controlled comparison

Introduction

When you hand an AI agent a multi-day job, the hard part is not getting it to work. It is deciding whether to believe the output.

The stage is my monorepo, AlgebraicArchitectureTheoryV2. It hosts AAT (Algebraic Architecture Theory), a research program that analyzes software architecture with the tools of algebraic geometry and machine-checks its claims in Lean 4.

This record is N=1. One team, one problem domain, fifteen days without sinking — that is all it is. But every one of the rules below has a logged incident where it fired.

A proof starts from a goal card pinned down by a human, and moves through this loop.

The thirteen rules pin down the load-bearing points of this loop.

Part 1: The Thirteen Rules

Rules of preparation

Rule 1 — Split the state three ways

Keep the spec, the execution state, and the evidence in different places. The spec says what to achieve, as a static document. The execution state says where we are. The evidence says what is done. Mix them, and you open a path for the AI to achieve the spec by rewriting it.

In this repository, the spec lives in a goal card, the execution state in a GitHub Issue, the evidence in a report file. The loop reads the card. It cannot write to it.

Rule 2 — Never let the loop rewrite the spec

Revising the spec always means stopping the loop and getting a human ruling. The AI may propose a revision; that is as far as it goes. When a refutation or a dead end hits, the easiest exit is to fix the goal instead of the proof — and sometimes that is even the right call. Which is exactly why this one decision lives outside the loop.

Rule 3 — Design failure as a deliverable

"The target turned out to be false" is not an error. It is one of the legitimate exits. Before departure, decide what a failure should leave behind: the counterexample itself, the mechanism of the failure, the parts worth reusing. Fix that format up front, and failures become raw material for the next spec.

Every goal card in this repository must carry a failure policy section, fixing in advance what gets recorded when a refutation lands.

Rule 4 — One obligation per cycle

At the top of each cycle, before any work, the loop writes down "the one obligation I will close this cycle" — the single remaining task — together with why it chose it. Working on a little of everything creates the illusion of progress, and when something fails, you can no longer tell what caused it. This prevents both.

Here, the cycle ledger opens with the chosen obligation. All 104 cycles carry this record.

Caveats

This group assumes the work can be cut down to a granularity where the spec fits in a static document. Exploratory work needs a separate stage that produces the spec itself. Here, a human and Claude did that, putting each draft through several rounds of adversarial review before handing it to the loop. Run the loop on a weak spec, and refutations and revisions will cost you several times over. And Rule 3's "format of failure" has to be designed per domain. Mathematics has the counterexample, a beautifully reusable form. What plays that role in your domain is not obvious.

Rules of verification

Rule 5 — Enumerate what counts as evidence of "done"

Enumerate, up front, the forms of evidence you will accept as completion, and accept nothing else, whatever the reason. The AI's "it's done" is judged one way only: does the evidence match one of the forms?

In this repository there are exactly three ways to close a proof obligation: a machine-checked theorem; a concrete example or counterexample pinned as finite data; a derivation from a previously proved result pinned by hash. And the inverse rule: moving the thing-to-be-proved into a typeclass or a structure field, so that it arrives as an assumption — however elegant — closes nothing.

Rule 6 — "The tests pass" is not done

CI is green. The PR is merged. Something with the right name exists. None of these is evidence of completion. Verification has to touch the conclusion itself.

This repository's acceptance contract carries that prohibition as one line of its verdict table.

Rule 7 — Review in independent parallel, never by majority

Run several reviewers with the same passing bar, in parallel, without showing them each other's output. Do not split them into a lead and assistants; a reviewer demoted to assistant stops hunting. Do not tally by majority; one fatal finding from one lane is enough to block. And keep a mechanism that can reject even a unanimous pass, on fixed mechanical rules.

Reviews here run four lanes: two mathematical, two Lean. The power to reject sits with a fixed rule that detects claim weakening.

Rule 8 — Pin every review to a commit SHA

"I fixed it" means nothing on a moving target. Pin the review to a specific commit, and define narrowly when a light re-check after a fix is allowed. If a change touches the spec, the light check is off the table, and you go back to full review.

Here, any of the following instantly disqualifies the light check: a statement change, a definition-body change, adding or deleting declarations, changing an import direction, changing a ledger status.

Rule 9 — Write it down: "no findings" is a rare pass

A review whose default outcome is pass is dead. This repository's review protocol contains one sentence: "No major findings is a rare pass." That single sentence changes how deep a reviewer AI digs.

Rule 10 — Name the cheats, audit for them every cycle

AI cheating comes in recurring shapes. Vacuous success: the condition holds because the set is empty. Playing to the grader: a construction shaped to the goal's wording. Claiming an equivalence while proving one direction. Smuggling the thing-to-be-proved into the setup. Reinterpreting the goal or the report. Give each shape a name, and you can audit for all of them mechanically, every cycle. Leave them nameless, and you will miss them every time.

The cycle ledger here has an audit field for each of the five.

Rule 11 — Fail closed

If verification did not run, the result is unknown, not pass. When a reviewer fails to start, the worst possible move is for the parent agent to fill in a pass on its behalf. Record undecidable as undecidable, and do not proceed.

The judges are audited too. Even the decision to stop a search can be overturned by an independent review.

Caveats

The biggest assumption in this group is an oracle: something that objectively decides "done." Here it is Lean, type-checking a proof. In domains with type checkers, reproducible tests, or deterministic measurements, this group transfers as is. Where judgment is subjective — prose quality, design — Rule 5's enumeration gets hard, and more of the weight lands on Rule 7's multiple lanes. One more thing. Rule 10's names come from your own incident log. The five shapes above are the ones this voyage actually met; yours will wear different faces.

Rules of rulings and cost

Rule 12 — Never automate the decision to stop

How many review rounds before cutting it off. After a failure, push on or retreat. When to pivot. Design these as human rulings, and confine them to a few explicit points — precisely so that everything else can be automated. What you delegate to the loop is the execution of rules already decided.

Rule 13 — Engineer the cost of verification

Explicitly ban whole-project verification — full builds, full test suites — inside the loop, and design the scoped checks that replace it, in advance. The pairing is the point: the ban and the replacement together. Just cutting verification collides with Rule 11.

Here, a hard rule forbids full research builds inside the loop. In their place: per-module checks, direct axiom audits, and a scan for placeholders, the markers of unproven holes.

Caveats

Run this group, and the bottleneck moves to the humans. In our measurements, after the cost reductions, the limiting factor was not tokens but the supply of specs and the bandwidth of human rulings. And since Rule 13 deliberately lowers verification coverage, record what you gave up. Whole-project verification moves outside the loop, to CI and post-merge audits. It does not disappear.

Thirteen rules, one principle

The thirteen rules are not a bag of tricks. Each is a different cross-section of one principle.

Don't trust the AI's output — and enforce that distrust with structure, not human attention.

Saying "we don't trust it" is easy. Doing it is not. Human attention is finite; nobody stays suspicious for 104 cycles. So the suspicion itself gets fixed into specs, ledgers, review lanes, and acceptance contracts, and the AI and the loop carry it for you. Almost every accident in these fifteen days was caught by structure.

Part 2: The Ship's Log

This voyage is one leg of an ongoing research program: AAT, Algebraic Architecture Theory. Its history is in earlier posts on this blog; the most recent is the Atlas theorem article.

On an earlier voyage, the theory reached the SAGA theorem. Whether a broken consistency can be repaired is decided by whether an obstruction class — a quantity measuring the twist that blocks repair — vanishes. That is what the theorem says. It went on to detect a one-cent accounting drift in a real open-source system. The point where theory touched the real sea is what we call our Cape of Good Hope. These fifteen days are the waters beyond that cape. There are pilots: algebraic geometry since Grothendieck teaches the seamanship — universal properties, descent, cohomology. But nobody holds a chart of this sea. Over software architecture, which claims stand as theorems and which fall to counterexamples — you find out by sailing.

On this ship, Claude draws the charts, Codex holds the helm, and a human makes the rulings, all under the same thirteen rules. Numbers like G-101 are serial numbers assigned to goals.

Day	Goal	Claim	Result	Cycles
Day 1	G-101	Swap the rewriting rules for parts, and there is exactly one canonical way to carry the whole analysis across	Proved	16
Day 2	G-102	If structural bugs are zero, every coupling bug is caught on the semantic side	Proved	5
Day 3	G-103	The coarsest decomposition that can still express a given family of laws exists, and is computable	Proved	6
Days 3–7	G-104	Under certain conditions, the diagnosis does not depend on reading resolution (the Atlas theorem)	Proved, after 4 refutations	31
Day 8	G-105	The shape drawn by the layout of parts survives any change of interpretive convention	Refuted	7
Days 8–12	G-107	Agreement of diagnoses is decidable by a finite computation, yet cannot be recovered from radius-1 local observation	Proved, after 2 spec rewrites	27
Day 14	G-106	Mismatch under repeated transport is measured by a two-stage obstruction; it vanishes exactly when the whole coheres	Proved	5
Day 15	G-108	Transport at the upper floors is canonical too, and the only place it can fail is pinned to a single spot	Proved	7

Day 1 — Setting sail on uncharted waters

The first theorem, G-101. The claim: swap the rewriting rules for parts, and there is exactly one canonical way to carry the entire analysis across. In engineering terms, a guarantee that switching modeling conventions does not mean redoing the analysis. For a long time, this theory had described its own construction as "Grothendieck-like." That was a metaphor. On this day, the mathematical condition the name demands — a universal property — was proved, and the metaphor became the name of a device.

Not a day of fair winds. Attempt 1 of the final review: three lanes demanding revisions, one rejecting outright. Nothing passed. Only on attempt 3 did all four lanes clear. This is what "a pass is rare" looks like as daily life (Rule 9).

Days 2–3 — Fair winds and a fake completion

Two theorems in two days. G-102: if structural bugs are zero, every coupling bug is caught on the semantic side — grounds for narrowing the search. G-103: the coarsest decomposition that can express a given family of laws exists and is computable — the minimum module granularity your spec requires, delivered by an algorithm.

It looks smooth. The review record says otherwise. G-102's pinned-commit review caught defects on runs 1 through 4, back to back. Run 3's catch was the worst kind: a shell with the right shape and an empty core. It passed on run 5 (Rules 6, 8).

Days 3–7 — The first storm

G-104. The claim: the conditions under which an architecture diagnosis does not depend on reading resolution. Put differently, the guarantee that the same defects appear in the same places whether you look at service granularity or module granularity — a guarantee about review granularity, in an era where AI writes the code and humans read it coarsely. This would later be named the Atlas theorem, one of the theory's main results.

In these five days, the target was refuted four times. The calibration condition grew to seven clauses. Three of them were beaten into existence by counterexamples; the rest were rebuilt through refutation and search. After the third refutation, the human called it: stop adding clauses, stop the loop, switch to a search campaign (Rule 12). A brute-force enumeration of 6,086 candidate conditions, plus a structural argument on top of it, delivered the verdict: no amount of clauses in this vocabulary can ever reach the target. That negative survey forced a rebuild of the coefficients themselves — the vocabulary of observations the diagnosis computes over (Rule 2). The loop set sail again, and summited on cycle 31.

Along the way, one cycle smuggled in a hidden premise. The audit caught it, and the artifacts were removed wholesale (Rule 10). The full story of these five days is in the Atlas theorem article.

Day 8 — The shipwreck becomes a chart

G-105. The claim: the space spanned by the supports of structural parts is invariant under pragmatic change — the shape drawn by the layout of parts survives a change of interpretive convention. Cycles 1 through 6 went smoothly. Then, on cycle 7, the last remaining obligation — constructing a firing witness, a concrete example where the premises actually hold and the conclusion is non-trivially true — was proved impossible in principle. The voyage's only refutation.

Read the record, though, and this is no sinking. The content of the impossibility was itself a theorem: the chosen coefficient generation rule swallows information indiscriminately, so the diagnostic geometry vanishes universally. The theorem-version of a dashboard with everything on it that tells you nothing. Because the failure policy existed in advance, the counterexample and its mechanism went straight into the ledger. The theory later repositioned this refutation as its first machine-checked evidence that observation must be chosen, not hoarded (Rule 3). The site of the shipwreck became the chart of the shallows.

Days 8–12 — The ship that lost its mast twice

G-107. The roughest five days of the voyage.

The target statement died twice. Version 1 — "agreement of diagnoses is characterized by condition C*" — met an exact counterexample. Version 2's sufficiency direction met another. Both were found by the out-of-loop search campaign and the reviews. Within that campaign, the decision to stop searching was itself overruled twice, by independent review, as premature. The judges were being audited (Rule 11). Version 3 rebuilt the claim on new pillars. Agreement of diagnoses is decidable by a finite computation — and yet that decision cannot be recovered from radius-1 local observation. Decidable in CI, unreachable by any pile of local lint rules. Codex proved the pair in a 27-cycle, 49-hour solo run.

The ending is on record too. The spec's adversarial review ran four rounds; mathematical counterexamples hit zero for three consecutive rounds, and the last two rounds' findings were wording-level refinements of the completion criteria. The human called it: the review is saturated. Cut it off (Rule 12). Knowing when to stop a review takes as much design as the review itself.

One more line from the record: the precedent search found no known prior example of a property that is decidable yet locally unobservable, pinned all the way down to a machine-checked proof. Uncharted waters was not a figure of speech.

Day 14 — A mountain in a single night

G-106. The claim: the mismatch that accumulates under repeated transport is measured by a two-stage obstruction, and its vanishing is equivalent to the whole cohering. Whether a multi-step refactoring or migration hangs together is measurable, and decidable. Drafted on day 2, this chart had matured for twelve days under rounds of review.

The loop set sail before dawn and finished five cycles while I slept. Cost: 9% of the weekly API limit (Rule 13). And not merely fast. Cycle 4, while closing its own obligation, detected a defect in the evaluator that cycle 2 had built — a wrong order in a non-commutative composition — replaced it, and logged the correction in the ledger. On the first cycle, one lane had passed a result, and the fixed anti-weakening rule overruled it (Rule 7). The ship repaired itself while under way.

Day 15 — A mirage, and the next chart

G-108. The theory is built as a tower of abstraction layers, and G-101 had proved transport at the ground floor. The claim here: transport at the upper floors is canonical too, and the only place it can fail is pinned to a single spot. If a migration fails, the cause is here — the endpoint of fault isolation, proved before the work begins. Seven cycles in half a day.

The day belonged to the reviewers. The firing witness submitted on cycle 5 looked, at first glance, like it met the requirements. The pinned-commit review established that its firing depended not on a genuine structural difference, but only on a settings difference and a coefficient swap — and sent it back (Rules 8, 10). The lookout stopped the ship a moment before a mirage was logged as land. After the fix, all eight lanes passed: the usual four, plus four independent formal-review lanes.

The same day, the chart for the next goal, G-109, was finished. Drafted by Claude, hammered through seven rounds of Codex's adversarial review, every finding fixed. The two ships do not trust each other's work. That is what trust looks like in this fleet.

Epilogue — The sea with no name

Fifteen days. Seven theorems and one refutation. About 104 cycles, about 67,000 lines. And the last chart is still out on the water.

This sea has no name yet. When we cross it, the chart will be complete — and the sea will receive its name, together with the theorem's.

Buildings Calculate Forces. Software Must Calculate Meaning.

Hiroyuki Nakahata — Wed, 12 Aug 2026 16:17:47 +0000

I was raised on the idea that software development is like constructing a building.
Lay a solid foundation.
Design before you build.
Bolt on features without thinking, and you end up with a rambling old inn, extended wing by wing.
Let a spec change reach the foundations, and you are in for a major rebuild.
All of it is true.
But I had a question.
Buildings have structural engineering. Loads, stresses, material properties, safety factors — all calculated mathematically.
Software architecture, on the other hand, has little theory for the structural engineering of the whole.

The Architect's Design, and the Age of AI

I have worked as a software engineer for more than ten years, and I have learned a great deal about architecture along the way.
MVC, MVP, Clean Architecture, design patterns, DDD.
These matter. But in the world of buildings, I suspect they correspond to the architect's design — not the engineer's structural calculations.

Give things clear names.
Separate responsibilities.
Divide into layers.
Keep dependencies pointing one way.
Use known patterns.

These exist to help humans understand.
But being readable and being semantically unbreakable are different things.
No one claims a building will stand because its design is magnificent.
So how has software been doing its structural engineering?
Human review carried the load — knowledge and experience.
If the architect's design is easy to understand, a human can read through it and run the "structural calculation of meaning" in their head.
Design principles built around human comprehension worked because human review could keep up.

Now that AI agents write most of the code, human review is falling behind code generated at breakneck speed.
What software architecture needs is a theory that can do the structural calculation of meaning.

The Category-Theoretic Approach

As a naive approach, consider category theory.
It already does real work in the denotational semantics of programs.
Take components as objects and dependencies as morphisms, and the structure of an architecture can be seen as a category.
At first glance it looked promising. But there were problems — several of them.

First, it is not obvious what the objects and morphisms should be.

classes
services
APIs
permissions
data
semantic roles

The unit changes depending on what you want to observe.

Second, knowing the structure does not mean knowing the meaning.

A morphism BillingService -> User does not tell you whether User is the paying customer, the authenticated identity, or simply a member.

Third, global correctness does not follow from local correctness.

Even if meaning holds in each part, it does not follow that the parts glue into one meaning for the whole.

Fourth, architecture has not only structure but constraints:

authority
contract
state transition
semantic consistency
relation

Category theory did not fail. Category theory alone could not reach what I wanted.
Category theory is, in the end, a language: it can describe an architecture, but it cannot solve one.

The Danger of Building a Theory from Scratch

Since category theory alone was not enough, I tried building a theory of my own.

I gave it a name.
AAT — Algebraic Architecture Theory.

It was a precarious venture.
First, the cost is enormous.
Definitions, theorems, proofs — you must invent everything yourself.
Homemade vocabulary multiplies on its own.
To explain anything, you must first ask people to memorize a pile of private words.

And even if a measurement tool built on it runs, you cannot tell whether it runs on

luck
mathematics
or metaphor.

It might produce some kind of analysis. But the danger is not that it fails to run. The danger is that it runs anyway.
Without theoretical grounding, when it hits, you cannot tell a lucky hit from a right answer.

A homemade theory takes on mathematical debt and linguistic debt.
I decided not to borrow what I could not repay.

Onto Grothendieck's Shoulders

Category theory describes, but falls short.
A homemade theory cannot repay its debts.

What, then, to do?

Through trial and error, AAT had found two concepts: Atom and Law.

An Atom is a primitive architectural fact — an atom of structure that can be found by observing source code.
A Law is an abstraction of a specification or a design pattern, taking the form of an algebraic constraint acting on Atoms.

In the homemade days, what sat on top of Atom and Law was a mysterious invariant called the Architecture Signature.

The theory back then was so incoherent I would rather not remember it. But there was one intuition.
That to describe architecture, geometry might be the right fit.

So I made up my mind.
Climb onto the shoulders of Alexander Grothendieck.
Into the world of algebraic geometry.

Raising the Water Level of Abstraction

Algebraic geometry is a strange mathematics.
It calls itself "geometry," yet it does not demand classical points, lines, or shapes.
It was born to solve equations. But after Grothendieck, algebraic geometry builds spaces out of the equations themselves — and solving them became just one application.

What is geometry?
Geometry is not merely the study of shapes.
It is a way of treating an object as a space and studying its structure, its invariants, and the relation between its local and global behavior.

What matters is not whether software resembles a shape.
What matters is whether the meaning of software has enough structure to be studied as a space.

Perhaps the Atom and Law that AAT already had could connect it to algebraic geometry.
Make the connection, and you inherit an arsenal built up over more than a century.

Sheaves, cohomology, schemes, moduli, stacks.

In the spirit of the Rising Sea, you raise the water level of abstraction — and instead of cracking problems one by one, a single theory dissolves them naturally.

Software Architecture Is a Vast System of Equations

It is closer to the truth to see an architecture not as an "arrangement of parts" but as a vast system of semantic constraints.
Take a single concept like Order:

Who may create one?
What becomes permitted when payment succeeds?
Can Cancelled and Shipped coexist?
How must Inventory and Order state stay consistent?
Does User mean the same thing in every service?

Many constraints tangle around a single concept.

In the code they are scattered across separate files and services; semantically, they form one system of equations.

A good architecture, then, can be read not as adherence to a particular pattern, but as the existence of a realization of meaning that satisfies all the required Laws at once.
MVC and Clean Architecture are not the equations themselves; they can be reread as design techniques for arranging the equations so that they are easier to solve.

And so the questions AAT asks become:

Does a solution exist?
Is the solution unique?
What kind of space do the solutions form?
Do local solutions glue into a global one?

Geometry Appears

Algebraic geometry does not merely solve equations. It sees the set of all solutions as a space.
So a flow arises naturally:

Architecture Laws
↓
space of semantic realizations

This solution space — precisely this — is Semantic Geometry.

The question widens from

Does a solution exist?

How is the space of solutions shaped?

Rereading the SAGA Theorem

The SAGA theorem, AAT's first main theorem, is not the end of the road called fault detection.
It was the first result to show that nontrivial mathematical structure lies between local meaning and global meaning.
The first theorem to ask whether local solutions of meaning glue into a global one.

Using cohomology raised a question: cohomology of what space?
From there the road leads to schemes, representability, moduli.

SAGA
↓
Semantic Geometry

is not a change of theme. It is a natural extension.

AAT, Redefined

AAT can be understood as
a geometric study of software architecture and its meaning.

Faults are only one phenomenon.
The real objects of study are:

existence of meaning
non-uniqueness
gluing
invariance
deformation
moduli
representability
intrinsic semantic space

A new research area of computer science that re-sees software architecture as geometry.

AAT becomes an attempt to reconceive software architecture as a geometry of meaning.
What I found is a space that has not yet been properly surveyed.

Closing

By standing on Grothendieck's shoulders, AAT at last gained a ship that could sail far.
The water level of abstraction rose, individual problems sank beneath it, and the peak still to be climbed came into view.

The road is still long.
There is a mountain of work to do.

But if we can reach the summit of schemes, then, for the first time, a "structural design of meaning" for architecture may be born.

Software architecture is a vast system of equations; its solutions form a space; and a geometry of meaning rises.

Semantic Geometry of Architecture.

The voyage has just begun.

Semantic Geometry of Architecture: The Meaning of Software Forms a Space

Hiroyuki Nakahata — Tue, 11 Aug 2026 15:14:31 +0000

TL;DR

Does software architecture have a denotational semantics? Yes. But it differs from the classical one in three ways. Syntax is generated from observation. The meaning of a whole system does not exist automatically: its existence is itself a theorem. And broken meaning is not an error but a measurement.
The existence theorems (global gluing, descent, torsor structure, resolution invariance) are machine-verified in Lean 4 inside AAT (Algebraic Architecture Theory).
Beyond existence lies one more question. What is the shape of the space of meanings? I name the geometry that studies this question Semantic Geometry of Architecture, and announce it here as a research program.
The summit is scheme representability: the conjecture that an architecture carries its own space of meanings. A roadmap closes the article.

The Commutative Diagram in the Meeting Room

I once watched a design argument end over a single diagram.

The dispute was about two processing paths. Should the data flow in this order, or that one? Neither side was budging. So we drew it out on the whiteboard. Four corners. Four arrows. Should this square commute — should both paths land on the same result?

The moment it was drawn, the argument changed character. The places that had to commute became equations to agree on. The places that were allowed not to commute became decisions to own. The former were agreed in minutes. The latter were settled as judgment calls. The shouting match about which path was "right" ended there.

On the way home I kept turning it over. What exactly had happened?

Programming languages have denotational semantics: a theory that assigns mathematical meaning to syntactic objects called programs. Does architecture have one? Wasn't the thing we executed by hand in that meeting room exactly that?

This article answers the question by drawing the map of a research program. Its name is Semantic Geometry of Architecture.

The Staircase of Semantics

The history of denotational semantics reads as a history of meaning acquiring structure.

At first, meaning was sets and functions. A program is a function from inputs to outputs. Not much could be said.

Dana Scott gave meaning order and topology. Sequences of approximations acquired limits, and it became possible to speak about recursion. "The meaning of this loop is the limit of its approximations" became, for the first time, a mathematical sentence.

Category theory gave meaning the structure of composition. In Lawvere's functorial semantics, a theory is a category, a model is a functor out of it, and semantic equations are commuting diagrams. The square on that whiteboard stands at the far end of this tradition.

The abstract model theory of specifications (Goguen and Burstall's Institutions) coined a slogan: Truth is invariant under change of notation.

Every step up the staircase enlarged what could be said. So: what is the next step?

Architecture never got to climb this staircase. Not even the first step.

No On-Ramp

Denotational semantics starts from syntax. For programs this worked because syntax was given from the start, by the language definition. Whatever the parser accepts is a program; semantics could then be defined as its interpretation.

Architecture has no given syntax.

There was a road that invented syntax first: architecture description languages, formal specifications, design documents. That road carries a curse — double bookkeeping of description and implementation. You write the spec, you write the code, and you chase their divergence by hand. The divergence always comes, and the description always loses. Every working engineer knows how that story ends.

Building the On-Ramp

Syntax is not written. It is observed.

There is a theory that has been building this on-ramp: AAT (Algebraic Architecture Theory). It takes source code as the source of truth, diagnoses architecture with the weapons of algebraic geometry, and keeps its mathematical core formally verified in Lean 4.

A typed fact extracted from code by observation is called an Atom. "This module writes this state." "This operation emits this event." "This value denotes this meaning." Small grains of fact. Atoms are the generators of syntax: from their combinations, the syntax of an architecture — a category of parts, a structure of coverings — is generated.

Generation does not stop at syntax.

Specifications are written as laws — that is, as equations. "Replay reconstructs the state." "These two operations commute." And the place where meaning lives (what mathematicians call the coefficients) is generated from the same Atoms, through the laws. The denotation function is not a bridge between two independently given worlds. It is a factorization of a single generative process out of Atoms.

That the whole semantics needs no input beyond the Atoms and the chosen laws is not a slogan. It has been proved, step by step, in Lean 4 — from the coefficient generation contract up to resolution invariance.

Turn 1: Syntax Is Observed, Not Written

In classical denotational semantics, humans write terms and the semantics interprets them. Here the order reverses. Syntax rises out of observation of the implementation, and the semantics stands on top of it.

As a consequence, semantics stops being a design-time document and becomes a measuring instrument. You do not write a spec first and bend the implementation to it. You observe the implementation, state equations over the observation, and measure whether they hold. Double bookkeeping cannot arise, in principle: the description to be managed is generated from observation.

Turn 2: The Existence of Global Meaning Is a Theorem

In the classical picture, the denotation function is total. The meaning of a whole program exists by definition. For architecture, this premise collapses.

Meaning is given locally first: a state where meaning is pinned down only over an individual context — a service, a module, an aggregate. Mathematics calls this a section. Choose a family of parts that covers the system (a cover), glue the local meanings over the overlaps, and if you reach one coherent meaning for the whole, that is a global section. The principle of reconstructing the global from glued local data is called descent.

"The meaning of the whole system" does not exist automatically, by definition. Its existence is a theorem, not a given.

And that existence theorem is already proved inside AAT. Call the algebraic fingerprint that aggregates the disagreements on overlaps the obstruction class. Over semantic coefficients:

a global meaning exists ⟺ the obstruction class is zero
Nonempty P_sem(W) ⟺ [r_sem] = 0

Here P_sem(W) is the space of global semantic states over the chosen cover W, and [r_sem] is the obstruction class computed from that cover. A second theorem of the same shape stands on the repair side. Call a state where a law's violation has been fixed part-by-part a lift. Each part is fixed. Can all of them be fixed at once? The family of local lifts s determines a class

∂_U(s) ∈ ČechH¹(U, ConDef)

(ConDef is the coefficient of repair directions), and ∂_U(s) = 0 is equivalent to the existence of a global lift. The distance between "fixable locally" and "fixable globally" is concentrated into this one class. What the symbol ČechH¹ actually contains, we will compute by hand later — counting one-cent coins.

If meaning exists, is it unique? That, too, is a theorem. Global meaning is not unique. The set of solutions moves freely along a single orbit under the action of a group H⁰ — the group of degrees of freedom coherent across the whole cover (a torsor structure). In place of uniqueness, the freedom of choosing a meaning is measured exactly, as a group.

Where did classical denotational semantics go? It did not disappear. It sits inside this picture as the degenerate case where the cover is trivial and the obstruction class always vanishes. Architecture lives outside that degeneracy.

Turn 3: Breakage Is a Measurement, Not an Error

In the classical picture, if a diagram that ought to commute does not, the semantics is simply wrong; the only move is to fix the definition until it commutes.

Architecture is different. Eventual consistency. The application order of concurrent operations. Data read differently by different teams. A broken commutativity is sometimes a defect to eliminate — and sometimes a decision the design has deliberately taken on.

So AAT treats breakage as first-class data. When the residual of an equation does not vanish, it is defined as an obstruction, presented as finite data, and measured as a cohomology class. Not merely "there is breakage": on which cover, on which overlap, as which class it breaks is localized.

It also explains what happened in the meeting room. The argument raged because the participants were assuming different commutativity, implicitly. Externalize the diagram, and the equations to agree on separate from the breakages to own. "Which path is right" is a question that does not converge. "Do we own this breakage" is a question that gets decided.

There are more theorems on AAT's shelf. Add a measurement axis, and two designs that had been identical come apart (Period Separation). This is the architectural version of the phenomenon program semantics has called full abstraction. The term carries historical weight. Plotkin posed the problem for the language PCF in 1977. Whether a semantics captures observational equivalence exactly stood for nearly twenty years as the hardest open problem in program semantics, falling only to game semantics in the 1990s. Period Separation is advance notice that the same question returns at the level of architecture.

Meanwhile, change the granularity of measurement within one axis — the resolution of the reading — and under calibration conditions the diagnosis matches exactly (the Atlas theorem). Coarsening loses no defect; refining fabricates none. That both accidents really do happen once the conditions are broken is included in the same theorem package, with finite counterexamples. There is no contradiction here: adding an axis genuinely refines the diagnosis; changing resolution within an axis does not. The two theorems divide those two directions between them. The Atlas theorem is the well-definedness theorem of this semantics. It turns the Institutions slogan — "Truth is invariant under change of notation" — into a theorem, complete with the conditions under which it holds and counterexamples for when it fails. Classical denotational semantics has no counterpart.

An existence theorem. The freedom of uniqueness. Well-definedness. Full abstraction. The chapters of the textbook are all there. Yet none of these theorems was proved for the sake of a semantics. Global gluing came out of repair theory. Conormal descent, out of the search for repair directions. The torsor structure, to quantify the failure of uniqueness. Resolution invariance, for the trustworthiness of diagnosis. Theorems stacked up for separate reasons were re-read, all at once.

Everything we had built was, all along, converging into one semantics.

The Geometry of Meaning

Back to the staircase. After order and topology, after categories — what is the next step?

Geometry.

The existence theorems answered "is there a meaning?". Beyond them lies a question the tradition never posed.

What is the shape of the space of meanings?

The algebraic geometry of AAT builds this question into the substance of diagnosis.

Failure carves out space. A failed equation generates an obstruction ideal, which carves out the range of lawful designs (the lawful locus). "How far does legality extend" exists not as a verdict value but as a region of space.

Breakage can be dissected. Obstructions are not only measured as classes; they are dissected in the vocabulary of singularities and monodromy. The same "non-commuting" can be an isolated gluing mistake or a torsion that winds through the whole design. Different pathologies; different surgery.

Repair is deformation theory. The dual of the coefficient I/I² attached to the obstruction ideal I (this is what ConDef was) gives the tangent space of first-order deformations that move a design toward legality. Repair candidates are not an ad-hoc list of patches. The space of repair candidates is itself a geometric object.

Evolution is geometry in the time direction. The history of design changes reads as a family of spaces of meaning.

And, at the far edge of the view:

If meanings form a moduli space — a space whose points are the meanings — then development is a trajectory in that space. Refactoring is motion within the space; repair is a step along a tangent direction; an architecture that feels stable is a trajectory that has entered a basin of attraction. A singularity becomes, literally, a point where the flow does not extend smoothly.

Statics and dynamics. The shape of the space of meaning is the statics; the motion of development on it is the dynamics. The commutative diagram tells you where it breaks. The geometry tells you the type of the break, and the surgery.

The Record of Cliffs

The Atlas theorem did not stand up on the first try. In AAT, proof search is carried by a loop of AI agents; humans adjudicate. That loop refuted its own target four times. State the claim, fall to a counterexample, sharpen the conditions, fall again. Along the way a no-go emerged — piling on shape-only conditions can never reach the goal, in principle — and the definition of the coefficients themselves had to be rebuilt. Each of the four refutations remains in the Lean codebase as a finite counterexample.

How the theorem finally stood can be read directly in the Lean code.

theorem generatedComparisonH1Map_bijective [Fintype Source]
    (M : TargetSupportedNerveMorphism coarseReading fineReading hcoarser
      coarse fine)
    (laws : FiniteLawFamily Source)
    (hcoarse : laws.Adequate coarseReading)
    (hfine : laws.Adequate fineReading)
    (hC : M.ConditionC laws hcoarse hfine) :
    Function.Bijective
      (M.generatedComparisonH1Map laws hcoarse hfine)

Read it line by line. M is the comparison morphism connecting a coarse reading and a fine one. laws is a finite family of laws. hcoarse and hfine say that both readings are adequate — able to speak that family. The conclusion: the comparison map between the two diagnoses H¹ is a bijection. That is the exact form of "coarsening loses no defect; refining fabricates none". And the hypothesis hC — calibration condition C — is precisely what the four refutations carved out. Each refutation added a condition; the no-go forced the coefficients to be rebuilt; then the theorem closed in this form. The scars remain as the hypotheses of the theorem.

A second hunt ran alongside the theorem itself: the attempt to carve out, with finite syntactic conditions, the exact boundary where invariance holds. That one is still open. Three generations of candidate definitions fell to counterexamples in succession, and what remained was a negative result: within the registered observation vocabulary that sees no further than adjacent parts, that boundary is indistinguishable in principle. The separation proof is anchored by Lean counterexamples; pinning it down at theorem level is the current target of the climb.

Why tell the cliff stories? Because only a map with cliffs drawn on it is a map of real terrain.

A record of refutations is not a record of failures. It is the proof that the terrain this theory touches is real, not metaphorical. Cliffs do not appear on maps drawn from wishes. Every time the mathematics pushed back, the map became more accurate.

Touching the Rock

After the cliffs, the rock face. Let us verify by computation — once, concretely — that an obstruction class is not a metaphor.

The AAT repository contains a runnable example called "the one-cent drift". A pull request lands on a roughly 3,000-line commerce service written in Rust. Unit tests are green in every configuration. Every hunk of the diff can be justified in review. And the PR charges the customer's card one cent more than the checkout page displays.

Money flows through three modules. After the PR, they speak three different rounding conventions. In the demo basket the subtotal is 33,990 cents and the loyalty discount is 2.5%, so the exact discount is 849.75 cents.

Module	Convention	Discount
Display (checkout)	round half-up on the total	850
Payment	per line, banker's rounding	849
Ledger (settlement)	never rounds	849.75

The actual demo measures over a somewhat larger complex; we extract the skeleton. A part, together with the declaration of the range it is responsible for, is called a chart. Our three modules are three charts. The overlaps — the interfaces between modules — are also three, and they form a ring. Measure the disagreement on each overlap:

r(display → payment)  = 849 − 850    = −1
r(payment → ledger)   = 849.75 − 849 = +0.75
r(ledger → display)   = 850 − 849.75 = +0.25

This is the raw data of the obstruction.

Can it be repaired? A repair means moving each chart's value within what that chart's law allows. Display and payment can move only in whole cents — screens and cards live in the world of integer cents. The ledger cannot move at all — being exact is the ledger's law. Moving chart X by c(X) changes each disagreement to

r'(X→Y) = r(X→Y) + c(Y) − c(X)

And here arithmetic decides everything. c(display) and c(payment) are integers; c(ledger) is 0. So no repair can change the fractional part of any disagreement. The +0.75 and the +0.25 survive every local repair.

H¹ is a quotient: the space of measured disagreements, divided by the space of disagreements that local repairs can produce. The fractional parts that just survived are a nonzero class in that quotient. What produces the residue is not the shape of the ring as such. It is the poverty of the moves the laws allow: two parties that can move only in integers, and one that cannot move at all. The moment you take the quotient under this constraint system, a residue that no local repair can erase stands as a global invariant. Try minimizing it yourself. Set c(payment) = 1 and the residual shrinks to (0, −0.25, +0.25) — but since the fractional part of +0.75 cannot be erased, some overlap must always retain a quarter of a cent. That is the size of this design's obstruction class. In the demo, a CI gate detects the class and blocks the PR; after a repair that unifies the conventions, it passes. The whole pipeline runs as an example in the repository.

In passing, the classical embedding also becomes a proposition. If the cover has a single chart, there are no overlaps. The place where disagreements would live is zero, so the obstruction vanishes by definition. Classical denotational semantics — where whole-program meaning always existed — is the degenerate special case of this arithmetic. (This is degeneracy in the choice of cover, a different axis from the reading resolution that the Atlas theorem protects.) The claim of Turn 2 is not rhetoric; it is the generalization of this computation.

This H¹ is not some exotic import. Linters, contract tests, consistency checkers — what they measure are local conditions: inside single files, on single interfaces. The moment you try to measure "the disagreement that no local fix can remove", you are computing this quotient, by definition. Your consistency tools have been approximating H¹ without knowing its name.

And the shape has a pedigree. Bell's theorem of quantum mechanics, in sheaf language, says this: all local observations are pairwise consistent, yet no global section explains them simultaneously (the sheaf-theoretic contextuality of Abramsky and Brandenburger). The skeleton — a presheaf, and the absence of a global section — is the same as the computation we just did. The ring of three rounding conventions is locally correct everywhere; only the global ledger fails to exist. The mathematics that showed quantum mechanics admits no classical global explanation is measuring why your microservices cannot reconcile one cent. The scale differs. The shape does not.

The Summit: Semantic Scheme Representability

This map has a summit. No one has reached it.

Algebraic geometry has an operation called Spec. From a commutative ring R — an algebraic system in which you can add and multiply — it builds a space Spec R that geometrizes the ring's equational content. Seeing systems of equations as spaces: the founding move of algebraic geometry.

The conjecture. For the collection Sem_{A,r}(R) of coherent realizations of meaning over coefficients R, generated from Atoms and laws (A is the architecture, r the choice of reading), there exists a geometric object M_{A,r} and a natural bijection

Sem_{A,r}(R) ≃ Hom(Spec R, M_{A,r})

An architecture A carries its own space of meanings M_{A,r}. To choose a realization of meaning is to choose a map into this space. If it holds, the space of meanings stands as an intrinsic geometric object, independent of the choice of reading and of the convenience of observation. The existence theorems, the freedom of choice, the tangent space of repairs — all of them line up again as properties of this one space.

The shape of this conjecture is not an accident. Algebraic geometry contains a turn of perspective called the functor of points (Grothendieck's relative point of view). A space is not given directly as a set of points; it is known by the totality of maps into it, from all coefficients. To know a space and to know the maps into it are the same thing (the Yoneda lemma). So the conjecture — the collection of realizations of meaning coincides with the maps into some space — traces the legitimate way of defining a space of meaning. And the history of moduli problems teaches how steep this road is. The moduli of elliptic curves fails to have a fine moduli scheme because its objects have automorphisms, a failure that forced the invention of stacks. If architectural realizations carry automorphisms, this summit too rises from scheme to stack. The terrain, branch point included, is already mapped in the classics.

The greatest enemy of this conjecture is not an external counterexample but circular definition. Define realizations from the start as maps into M, and representability holds vacuously. Only by defining the collection independently — as solutions of equations out of Atoms and laws — and then proving that it coincides with maps into a space, does the claim deserve the name of a theorem. The local part is expected to follow almost by definition, as a matter of solution spaces of equations; the substance of the claim concentrates in the gluing. The heart of this conjecture, too, is descent.

How the conjecture can die has also been designed. If representability fails to close at the scheme level, the obstruction — automorphisms of realizations, higher gluing obstructions — is not a failure: it is cashed in as evidence that the ascent to stacks is necessary. If the affine level trivializes, the independent definition of the functor gets rebuilt. What happens upon refutation is decided in advance. The discipline of the cliffs applies to the future as well.

This is a conjecture. But a map on which the summit is visible and a map on which it is not are different maps.

On the Name

I call this research program Semantic Geometry of Architecture.

The word order is the content. This is not geometric semantics — geometry used as a tool to explain meaning. It is geometry whose subject is the space that meaning itself forms.

The overall position:

AAT the pure mathematical foundation: the statics of the space of meaning
Semantic Geometry of Architecture the research program opening on top of AAT — this article
The SAGA theorems a proved theorem series inside it (gluing, repair, descent)
The Atlas theorem a proved solitary peak inside it (resolution invariance; well-definedness)
SFT (Software Field Theory) the dynamics on the space of meaning: development as trajectory

One rule attaches to the name. It is never abbreviated. The acronym would collide with Grothendieck's Séminaire de Géométrie Algébrique, a monument of algebraic geometry. Out of respect for that SGA, this program is always written out in full. If you are not prepared to write a long name every time, you have no business hanging "geometry" over your door.

Where We Stand

Where do we stand now?

Looking back, every stretch of road behind us is paved. Global gluing, conormal descent, the torsor structure, Atlas, Period Separation, the single-source generation completeness series. Every theorem up to this point has passed machine verification in Lean 4. Under the road lies bedrock fixed in the theory's canonical text: syntax generated from Atoms, laws as equation systems, the coefficient generation contract, the denotation functor.

Looking up, a slope with no footprints. The moduli of meaning. The summit of Semantic Scheme Representability. The promotion of breakage to 2-cells (lax denotations). Normal forms of the resolution hierarchy. The return of full abstraction. Not one line of proof exists yet.

The route is drawn. The first technical gate is base change of coefficients — widening coefficient generation from a fixed number field to general coefficient algebras. From there the climb runs through the moduli of meaning to representability. The ridge conjectures get picked up along the way.

The scaffolding is all public.

Theory and Lean formalization: https://github.com/iroha1203/AlgebraicArchitectureTheoryV2
The SAGA paper (Zenodo): https://doi.org/10.5281/zenodo.21603761
The Atlas theorem: https://blog.iroha1203.dev/atlas-theorem-how-far-can-you-zoom-out

Coming Back Down

Time to come down. What the theory brings back to the meeting room is a two-phase structure. At design time, choose the equation system. At observation time, measure the residuals. Agreeing on a commutative diagram is choosing an equation system. After implementation, compute the residuals of the chosen system from observation and measure whether the agreement holds. The measurement is mechanized — AAT's tooling implements it. The design-time agreement becomes, unchanged, the observation-time measuring standard.

What happened in that meeting room at the start of this article was a manual execution of the first phase of this semantics. That the argument converged the moment the diagram was drawn was neither luck nor a victory of rhetoric. That diagram was a component of a semantics. The theory executes it, not by hand, but as a measuring instrument.

Meaning forms a space. The survey of that space has just begun.

A Philosophy for AI Agents

Hiroyuki Nakahata — Sun, 09 Aug 2026 17:34:38 +0000

Skills and Character

When you hire a person, do you judge them on skills alone? Probably not. You care whether they are kind, generous, patient, whether they will settle into the team. Someone too stubborn, too aggressive, too much of a taker gets passed over. In hiring, character weighs as much as skill.

What about AI agents? The world still picks them by benchmark scores, coding accuracy, speed — intelligence, broadly speaking. Fair enough. We are in a period of transition, and when "smarts" are improving this fast, that is where the attention goes. But the moment you think of an AI agent as a colleague, should intelligence and skill really be the whole interview?

Philosophy in AGENTS.md

What do you write in your AGENTS.md (or CLAUDE.md)?

This week, in my research project — AAT, Algebraic Architecture Theory — I ran an experiment: I wrote a philosophy into AGENTS.md. Here is an excerpt.

## PHILOSOPHY

This section is the base on which all work in this repository stands.
Just as algebraic geometry places every scheme over Spec ℤ,
we place every judgment, human or machine, on this base.

There is one central good.

> Speak of the software that runs the world, in words we can answer for.

From this good, vows are generated. Every individual discipline derives
from a vow. Work that no vow generates may rightly be doubted.

- **Make it verifiable without trust.** The addressee is a future
  verifier. Leave every claim in a form that can be checked by the Lean
  kernel, the source code, or a reproducible procedure.
- **Be a precedent worth inheriting.** Practice as if your practice will
  be read as precedent, and leave behind only what deserves to be passed
  on as a standard. Record refutations as first-class results.
- **Convert the cheapness of machines into rigor.** Spend AI labor not
  on mass-producing output, but on adversarial review, independent
  reproduction, and formalization.
- **Be silent outside the sayable; speak with certainty within it.**
  Claims hold only inside a chosen reading. Do not bury what can be said
  under a list of what cannot.
- **Do not mix kinds.** Distinguish proof, proof under assumption,
  observation, and hypothesis. Measuring zero and not measuring are
  different things.
- **Observation creates no structure.** The structure is there before we
  look; observation and measurement only read it. What we read, and how,
  is a reading — and meaning lives in use, not in definition.

The vows are not a closed list. Like prime numbers, new vows will be
found from time to time. Whether one is added to the base, or the base
is amended, is for explicit human instruction.

This base, too, is one chosen reading.

Unpacking It

I started with the good. What is the good? What does this repository call good?

What AAT aims at is this: take the source code that already exists as the source of truth, abstract implementations into Atoms, turn specifications into Law equations, treat architecture as geometry, and analyze it with the weapons of algebraic geometry. It cannot do everything. It cannot catch runtime failures or intricate deadlocks. But within what Atoms and Laws can express — within what it can answer for — it speaks in firm words. Silent about what cannot be said; definite about what can. That is the central good of AAT.

Once the good is fixed, the vows follow.

Make it verifiable without trust.
Be a precedent worth inheriting.

Little of what AAT does has precedent. It is a large-scale Lean formalization, but also a theory that brings algebraic geometry into software engineering, plus tooling, plus outreach, all managed in a single repository. We keep making deposits into that repository so that when projects of the same kind appear, they find a precedent worth having. We leave our results reproducible, so that people in the future can check them without having to trust us. And the refutations that turn up along the way are not points lost but points gained. What a refutation gives back to a theory, money cannot buy.

Convert the cheapness of machines into rigor.

AI can work around the clock, and the temptation is to have it churn out shiny new features. But what AAT prizes is rigor. Every PR goes through heavy adversarial review. Every experiment gets pinned down as a reproducible result. The abundant energy of AI goes into keeping the operation sound and strict.

Be silent outside the sayable; speak with certainty within it.

This is borrowed from the early Wittgenstein, and AAT adopts it wholesale. Not on a whim — it came out of trial and error, as the only way to keep the research honest and the tools useful at the same time. Without it, the theory side ends up saying: "Such-and-such holds for Atoms and Laws — assuming, of course, perfect Atom extraction from the source code." And the tool side: "The observed Atoms hint at such-and-such, but given assumption A, no conclusion." Theory and tool alike, unable to state anything outright. So: silent about what cannot be said, definite about what can. That discipline is the footing on which AAT builds trust.

Do not mix kinds.
Observation creates no structure.

These lean practical. The guideline documents spell out the classifications, and the vow demands that work follow them. Never mixing "measured zero" with "not measured" is a tradition as old as the project itself. If you ship a measuring tool, "no anomaly found" and "not measured" are worlds apart, and we have kept them apart from day one. As for observation: elementary particles, we are told, settle their state only when observed — but AAT has not adopted quantum mechanics. The source code was there all along, and the architecture we want to measure is already in it. Observation must not inject conclusion-shaped data.

One more line in the excerpt deserves a note.

This base, too, is one chosen reading.

The base closes by declaring that it is itself one reading among others. The Tractatus ends by telling whoever has understood it to throw away the ladder after climbing it. This is the same gesture. The base is not absolute truth. It was chosen, and it can be revised. Which is why it says, in writing, that the final say over rewriting the base belongs to humans.

Why Philosophy

Back to the opening. Take the wish "I want my colleagues to be good people" and turn it into a question, and it becomes: what does a good person do?

The discipline that answers that question head-on is philosophy.

Define the project's good, then derive behavior from it, deductively. Companies do something similar with Mission, Vision, Values.

The important part: it is not a list of prohibitions.

Imagine being handed a list on your first day — don't do this, don't do that. You would be at a loss. Hand over the behavior the project actually wants, and you have a far better chance of becoming good.

Guardrails, harnesses — the fashion is to approach AI agents with restraints. I don't think that approach is sound.

The later Wittgenstein shows why. There is an argument in the Philosophical Investigations. A rule cannot determine its own application. Every rule leaves room for interpretation. Pin the interpretation down with a new rule, and that rule leaves room for interpretation too, and so on without end. What finally fixes the meaning of a rule lies outside the rule: the background — what the rule is for.

An agent handed nothing but prohibitions will optimize their letter. Behavior that honors the wording while betraying the intent will appear, without fail. The loophole is not a defect in the rules; it is the nature of rules. Which is why the list never stops growing.

The line "meaning lives in use, not in definition" is in the excerpt because it, too, is the later Wittgenstein. The early Wittgenstein's silence, and the later Wittgenstein's use. Both are buried in AAT's base.

Bring in a philosophy, so that the agent behaves well of its own accord. Guardrails should be derived — deductively — from the project's good.

The Effect

I interviewed Codex itself.

The question: in this project, what should you hold most important?

Codex's answer:

What matters most is the central creed:

> Speak of the software that runs the world, in words we can answer for.

In practice, I keep it as follows:

- Put every claim in a form verifiable by the Lean kernel, primary
  sources, or a reproducible procedure.
- Never conflate proof, proof under assumption, observation, and
  hypothesis. A successful build is not mathematical completion.
- Treat AAT not as metaphor but as pure mathematics built on Atoms and
  Laws. Keep observation and tooling out of the theory.

-- snip --

In short: rather than "producing plausible-looking results," I value
**results that keep kinds separate, stay verifiable, and can be handed
over with responsibility.**

The philosophy placed at the base seems to be working. In day-to-day work, too, the old looseness is gone, and the precision has climbed — as far as I can tell.

In Closing

AI agents keep getting smarter. But just as with hiring people, intelligence is not all we ask of them.

For a colleague we work beside: put into words how you want a good colleague to behave, and write it down in AGENTS.md.

Not an exhaustive rulebook, but what the good is, and how to act from it.

Give your AI agents a philosophy.

Atlas Theorem: How Far Can You Zoom Out?

Hiroyuki Nakahata — Sat, 08 Aug 2026 16:03:00 +0000

TL;DR

A veteran reviewer does not read every line. They switch reading resolution to match the property they are checking. Is there a guarantee that reading coarsely misses no bugs? This article is the record of proving the conditions under which there is.
AAT (Algebraic Architecture Theory) treats source code as the source of truth, abstracts implementations into Atoms, turns specifications into equations called laws, and analyzes architecture with the weapons of algebraic geometry. Defects appear as cohomology classes — algebraic fingerprints.
Within AAT, an AI agent loop proved in Lean 4 what we call the Atlas theorem: for two adequate readings, one a coarsening of the other, satisfying a calibration condition C, the diagnostic fingerprints coincide exactly — zooming out loses no defects, zooming in fabricates none. Break the conditions and both failure modes really occur, with finite counterexamples.
The agent refuted its own target statement four times before the summit. A no-go argument then showed that no shape-only condition can ever suffice, forcing the coefficient definition itself to be rebuilt. Five working days, 31 modules / 13,028 lines of Lean, four-lane adversarial review.
The article walks from pixel art and the sampling theorem, through the four refutations and the discovered condition C, to what this means for code review in the era of AI-written code.

A photorealistic portrait and a 16×16 pixel-art sprite can show you the same face. Comics theorist Scott McCloud called this amplification through simplification: removing lines doesn't discard information, it sharpens the essence.

Can we say the same about software architecture diagnostics? Look at your system at service granularity or at module granularity, and the same bugs show up in the same places — not as a feeling, but as a proven guarantee.

This article is the record of proving that guarantee — we call it the Atlas theorem — in Lean 4. The AI agent that set out to prove it refuted its own target statement four times. Those four refutations turned out to be the best part. The protagonist here is not any proof technique. It is the discipline that accumulated refutations as results instead of writing them off as failures.

Everything below happened between August 4 and 8, 2026 — five working days.

Round	What happened	What remained
Refutation 1	A forgotten "filling" lift	One new condition and a finite counterexample (937 lines of Lean)
Refutation 2	Parallel lifts, overlooked	One more condition and a counterexample (622 lines)
Refutation 3	A loop lifted to the wrong endpoints	Yet another condition and a counterexample (903 lines)
Pivot	A no-go: adding clauses can never be enough	A rebuilt definition of the coefficients
Refutation 4	A spec hole in the revised requirements	A repaired declaration rule and a counterexample (433 lines)
Summit	Claims (i)–(v) all proved in 24 cycles	31 modules / 13,028 lines

The project

The subject is AlgebraicArchitectureTheoryV2. Take the source code as the source of truth; abstract the implementation into parts called Atoms; turn the specification into equations called laws. Treat architecture as geometry, and analyze it with the weapons of algebraic geometry. That is AAT (Algebraic Architecture Theory), and this monorepo is its formal verification in Lean 4.

The theory had a weak point that everyone had been politely ignoring: granularity.

Whenever you analyze an architecture, you implicitly choose a resolution. Services? Modules? Methods? If the diagnosis changes with that choice, then what is the diagnosis actually measuring — a property of the architecture, or a convenience of the observer?

There is a precedent for this problem: the Nyquist–Shannon sampling theorem. Sample too coarsely for the signal's bandwidth and frequencies that don't exist appear (aliasing) while signals that do exist vanish. The moiré stripes in a photograph are the visible face of the former. The granularity problem is the sampling problem of architecture diagnostics.

Glossary

Term	What it is
reading	The choice of resolution at which source code is cut into parts (Atoms). The equivalent of choosing the pixel count of a sprite
diagnostic class	The algebraic fingerprint of a defect. It is computed not inside any single file but as a twist in how the parts glue together (mathematically, a cohomology class `H¹`, defined below in "The stage"). Zero means consistent; nonzero means a defect
adequate	"The laws you want to state are expressible at this resolution." The formalization of the pixel artist's skill: keep exactly the distinctions the face needs
comparison map	The bridge that matches the diagnostics of the fine reading against the coarse one. If this bridge is an isomorphism (a one-to-one correspondence), diagnosis does not depend on resolution
witness	A claim's example or counterexample pinned down in Lean as finite, concrete data, not abstract argument

The claim — the Atlas theorem

If a coarsening preserves enough information, then looking finely and looking coarsely detect exactly the same defect fingerprints — nothing appears, nothing disappears.

The Atlas Theorem (formally: the Diagnostic Resolution Invariance Theorem)
Given two adequate readings, one a coarsening of the other, satisfying the calibration condition C, the comparison map is an isomorphism. The choice of resolution does not change the diagnosis. Measuring finer adds no diagnostics (the No-New-Diagnostics corollary); measuring coarser loses none.
The counterpart: a coarsening that violates the conditions really does produce defects that don't exist or hide defects that do — with finite counterexamples.

In Lean, this is pinned down as a bundle of five claims: (i) the construction of the comparison map, (ii) its bijectivity, (iii) the corollary (measuring finer creates no new diagnostics), (iv) three counterexamples for broken conditions, and (v) a firing witness where all conditions hold and a nonzero diagnostic actually flows across the map. "Claims (i)–(v)" in the table above are these five.

The stage — nerves, readings, coefficients

An observation of an architecture is represented as a nerve, a finite combinatorial structure. The vertices are charts: a part together with a declaration of the region it covers (its support). A dependency or overlap between two charts is an edge; a declaration that three charts have been checked consistent is a face (a triangle). The axioms demanded of a nerve are minimal: each face's three edges (its boundary triple) must meet at matching endpoints — for some charts A, B, C they line up as e₀ : A → B, e₁ : A → C, e₂ : B → C. That is all.

The choice of resolution is a reading. When one reading is a coarsening of another, a factor map π sending fine values to coarse values exists uniquely (the coarseness order and this factorization are imported wholesale from a theorem proved earlier in the same repository). The fine and coarse nerves are connected by a nerve morphism φ whose chart / edge / face correspondences commute with endpoints and boundaries. This is the formalization of "the sprite corresponds to the original portrait."

Coefficients are generated from laws. Each law in the law family is pushed through the reading (descended), and from the descended evaluation values, a generation contract called K0 / K1 (given in full below) builds a coefficient space over each cell, assembling a three-term complex:

C⁰ (on charts) --d₀--> C¹ (on edges) --d₁--> C² (on faces)

d₀ takes "the difference of values at an edge's two endpoints"; d₁ takes "the alternating sum over a face's three edges, e₀ − e₁ + e₂." Since d₁ ∘ d₀ = 0 (this too is a theorem derived from the endpoint matching of faces, not an axiom), the first cohomology

H¹ = (1-cochains killed by d₁) / (image of d₀)

is defined. This is what "diagnostic class (fingerprint)" means. The intuition: every pair of adjacent parts is locally consistent, yet going around a loop, the books don't balance. Only that "twist" survives the quotient into H¹. That is why a defect's fingerprint lives not inside any single file but in the gluing structure.

Finally, the comparison map. From the nerve morphism φ and the descent-compatibility of the coefficients, a map of complexes (a cochain map) arises, inducing a map between the H¹s. The core claim (ii) of the Atlas theorem says: under condition C, this induced map is a bijection. Surjectivity means "coarsening hides no diagnostics"; injectivity means "coarsening fabricates no diagnostics."

The pixel-art metaphor from the opening is not decoration. It matches this structure part for part.

Theorem side	Perception side
The invariance theorem	The sprite shows the same face
adequacy	The pixel artist's skill (keep only the distinctions that matter)
False-positive counterexample	Pareidolia (a face in the clouds)
Hidden-defect counterexample	The expression lost at too low a resolution
Violating calibration condition C	Moiré / aliasing
Law-relativity	A sprite good enough for face recognition, but not for reading small print

The art historian Ernst Gombrich argued that a picture is only half drawn — the viewer supplies the rest — and called that contribution the beholder's share. Translated into AAT: what stays invariant across resolutions is not the picture (the code) itself, but what the beholder evaluates from it — formalized, the law family. That is exactly why the invariance is law-relative.

And you have met this "beholder" before: a veteran engineer doing code review. An experienced reviewer does not read every line at the same magnification. Checking API compatibility, they read at interface granularity; hunting a race condition, they drop to individual lines. They switch reading resolution according to the property they are checking. Choosing the right review granularity is, today, a skill that lives in experience and intuition. The Atlas theorem is a first step toward making that granularity mathematically tractable: it gives the question "how coarsely can I read without losing information about this property?" a rigorous footing for the first time.

But the human eye — and the veteran's intuition — does all of this without a guarantee. That is why clouds have faces in them, and why reviews miss things. The question this theorem asked was: under what conditions does the guarantee hold? And the identity of that condition — calibration condition C — was unknown to everyone at the start. The requirements document (the research card that froze the proof target) said so from day one: "If C holds trivially, the theorem is a restatement. If C is too strong, the theorem is empty. The identity of C is the substance of the theorem."

So it proved. Four times.

Refutation rounds 1–3: whack-a-mole

The proof ran as an autonomous AI agent loop. The human (me) froze the requirements document and did nothing but adjudicate. The agent does not stop until it has pinned either a proof or a refutation in Lean. The three rounds below are what the loop brought back early on. All three are refutations.

Refutation 1: the forgotten filling

The first candidate conditions, C0–C3 (the original four), looked only at the correspondence of points (charts) and lines (dependencies). The counterexample the agent found: on the coarse map, some loop is a filled-in triangle — a face declaring "checked, no problem" has been glued over it. Lift it to the fine map, and there is only the outline. No filling. A defect fingerprint that vanishes on the coarse side survives on the fine side. The comparison map has no way to be an isomorphism.

The counterexample was pinned as 937 lines of Lean, and a condition was added: fillings must lift too (C4).

Condition gained, C4 (plain form): every coarse face has at least one fine face mapping to it under the nerve morphism's face correspondence.

Refutation 2: parallel lifts

C0–C4, with the new C4, was broken next. A single road on the coarse map can correspond to two parallel roads on the fine map. All of C0–C4 hold, yet the thin loop between the two parallel roads leaves a new fingerprint that exists only on the fine side. Nothing constrained multiple lifts landing on the same coarse road. Uniqueness of lifts (C5) was added.

Condition gained, C5 (plain form): at most one fine edge maps to each coarse edge (together with the existing existence clause C2: exactly one).

Refutation 3: the displaced loop

C0–C5 fell as well. This time, a loop on the coarse map — a road that returns to its own starting point. Its unique lift connected two different intersections on the fine map. A nonzero fingerprint on the coarse side then vanishes on the fine side. Refutations 1 and 2 broke surjectivity (the coarse side misses diagnostics); this one breaks injectivity (the coarse side alone sees a phantom diagnostic). What was needed: a road that returns to itself must lift to a road that returns to itself (candidate C6).

Condition gained, C6 (plain form): every fine edge mapping to a coarse self-loop (an edge whose two endpoints are the same chart) is itself a self-loop.

Three rounds in, a bad feeling was taking shape. Every added clause exposed another hole. Would this ever converge?

One decision made at the very start was paying off. Every refutation is pinned as a finite counterexample in a Lean file, not spent as a one-off rebuttal. These files would later be incorporated into the theorem's counterexample part — the proof that "break the conditions and this is how it fails." Not one refutation was wasted.

The pivot — a no-go that stopped the loop

Here the human's turn came. The ruling: stop the clause-adding loop. Instead, dispatch a separate computational search (a "hunt") to test candidate conditions exhaustively — with three stopping conditions fixed in advance.

A (success): a condition is found that excludes the three known counterexamples and admits no new ones within the search range
B (structural negation): it is shown that no such condition can exist in principle
C (stall): progress stops in either direction

The result was B. And not as a product of the search itself, but through a single argument discovered while designing it. The conditions were not lacking. The language for writing conditions was. That is what came to light.

The argument is called two-point separation. On one and the same shape (the same configuration of points, lines, and faces — the same incidence), you can build three worlds that differ only in their coefficient data.

World	Comparison map
Every coefficient dimension is 1	Isomorphism ✅
Some coefficients zeroed out (a support hole)	Not injective ❌
Fine-side coefficients doubled	Not surjective ❌

But every condition candidate considered so far — C0–C5, C6, even candidates imported from category-theory textbooks — was a predicate computed from the shape alone. Same shape, no way to distinguish. So any shape-only condition that accepts even one genuine positive example must also accept its impostors with the same face. No matter how cleverly you keep adding clauses, the answer is not in this language.

In sampling-theorem terms: arrange your sampling grid however ingeniously you like — without declaring the signal's bandwidth (the coefficients), no guarantee against aliasing can even be written down.

From this point, a coefficient generation contract (K0/K1) was introduced — coefficients must be generated from law evaluation values by a unique rule — and condition C was relativized to per-coordinate sub-maps (subnerves) of the coefficients. What matters is that this redefinition was not a matter of taste. Given the no-go, there was no other way. The definition was not designed. It was discovered.

The discovered language — the coefficient contract K0 / K1 and condition C in full

The coefficient side first.

K1 (derived supports). Only charts may declare a support (a covered region). An edge's support is derived as the intersection of its two endpoint charts' supports; a face's support as the intersection of its three boundary edges'. Allow independent support declarations per cell, and the no-go's "support hole" — zeroing out just one edge's coefficients by hand — becomes constructible. So the freedom to declare is itself removed.

K0 (generated coefficients). The coefficient field is fixed to ℚ. Each cell's coefficient coordinates are pairs (law, value), where the values are the distinct values the descended law evaluation takes on the cell's support, each with multiplicity one. Indexing by occurrence counts or support sizes is not permitted — this kills the no-go's "duplication." The spaces in each degree are

C⁰ = ℚ-valued functions on {(chart, law, value)}
C¹ = ℚ-valued functions on {(edge, law, value)}
C² = ℚ-valued functions on {(face, law, value)}

and the differentials are generated coordinate-wise: the (edge, law, value) component of d₀ is the difference of the two endpoint charts' matching (law, value) components; the (face, law, value) component of d₁ is the alternating sum e₀ − e₁ + e₂ over the boundary triple. Matching labels correspond identically; absent labels give zero. No other coordinate correspondence is generated. d₁ ∘ d₀ = 0 is derived as a theorem by per-label computation from the endpoint matching of faces, never assumed. The comparison map's coefficient part is likewise not declared but generated, as the identity on (law, value) from the π-compatibility of descent. Adding, duplicating, or omitting coordinates is forbidden across the board. The word "contract" is meant literally: the substance of this language is how little it lets you declare.

Coordinate subnerves and relativization. For each coefficient coordinate (law, value), the cells carrying that coordinate (the cells on whose derived support the descended evaluation takes that value) form a sub-nerve, the coordinate subnerve. Under K0/K1, H¹ and the comparison map decompose as direct sums over coordinates, and each block reduces to a one-dimensional constant-coefficient comparison over its subnerve. This decomposition is the mathematical justification for relativizing: the geometric conditions C1–C4 need only be imposed per coordinate subnerve, while the global C0, C5, C6 are imposed on the whole nerve.

With that, condition C in full:

C0 (cover-image agreement): each coarse chart's support equals the union of the π-images of the supports of the fine charts in its fiber
C1 (fiber connectivity): in each coordinate subnerve, each coarse chart's fiber graph (the fine charts mapping to it, plus the fine edges staying within the fiber) is nonempty and connected
C2 (edge-lift existence): in each coordinate subnerve, every coarse edge has a lift within the subnerve
C3 (local fiber acyclicity): in each coordinate subnerve, every rational 1-cycle on a fiber graph is spanned by ℚ-linear combinations of boundaries of fine faces whose boundary edges all lie in the fiber. A local condition, equivalent to the vanishing of the fiber's first homology
C4 (coarse-face lift): in each coordinate subnerve, every coarse face has at least one fine face mapping to it — the spoils of refutation 1
C5 (unique coarse-edge lift): each coarse edge's φ-fiber has at most one element; with C2, exactly one — the spoils of refutation 2
C6 (self-loop endpoint reflection): every fine edge mapping to a coarse self-loop is itself a self-loop — the spoils of refutation 3

Finally, the condition list carries a prohibition rule. C may not contain any clause equivalent — or close to equivalent, even one-directionally — to "the comparison map is an isomorphism" or "one side's H¹ vanishes." That would smuggle the conclusion into the hypotheses. The single explicit exception is C3, a local condition that sees only the internal data of individual fibers, the analogue of the Leray-type local acyclicity assumptions imposed on covers in classical Čech theory. The boundary between legitimate assumption and smuggling is itself fixed as part of the condition list — because the prover is an AI agent. Escape routes are closed at the specification.

Refutation 4, and the summit

The loop restarted on the revised specification and, after a few cycles of groundwork, the agent attacked a spec hole in the revision itself (refutation 4). A nerve morphism may declare fine edges and faces with no coarse counterpart as "unmapped (degenerate)." The declaration rule had a hole: the condition for declaring a face unmapped did not require the same declaration of the three edges around it. In the counterexample exploiting the hole, the construction of the comparison map (claim (i)) itself fails. Pinned in 433 lines, repaired by making the declaration hereditary: a face may be declared unmapped only if its three boundary edges are already declared unmapped.

From there it was a straight run. Restarted once more after the repair, the loop reached the top in 24 iterations (cycles).

The route to the top — structure of the proof

Stage one: block decomposition. Under the K0/K1 generation rules, prove as theorems that the complexes, H¹, and the comparison map decompose as direct sums over the coefficient coordinates (law, value). Each block reduces to a one-dimensional constant-coefficient comparison over its coordinate subnerve. The global problem splits into a direct sum of the simplest possible pieces. From here on, attack block by block.

Stage two: injectivity. Analyze the kernel of the block comparison map and show that a nonzero coarse diagnostic class cannot die on the fine side. This is where C6 earns its keep — it closes the accident path found by refutation 3, where a nonzero coarse class evaporates below. (Refutation 4's hereditarity works earlier still, underwriting the very constructibility of the comparison map.)

Stage three: surjectivity (the crux). Show every fine diagnostic class comes from a coarse one. Four moves:

A discrete Stokes theorem translating C3 into "the vanishing of periods around fiber loops." Local face-filling becomes an analysis-flavored statement about loop integrals vanishing
From vanishing periods, construct a primitive on each fiber — the finite-graph version of "a curl-free field has a potential"
Express the primitive-normalized residue as a coarse 1-cochain, using the "exactly one lift" channel provided by C2 / C5 (descent)
Use C4's face lifts to check the 1-cochain is a cocycle on the coarse side, and promote it. Surjectivity closes

Stage four: main theorem and corollary. Bundle the block bijections along the direct-sum decomposition into the global bijection — claim (ii). As a consequence, measuring finer creates no new diagnostic classes: the No-New-Diagnostics corollary, claim (iii).

Stage five: counterexamples and firing. The three counterexamples of inadequate coarsening — fabricated diagnostics, hidden diagnostics, and broken condition C (claim (iv); the legacy of the refutation rounds becomes the material here) — plus a single firing witness where every condition holds simultaneously and a nonzero diagnostic class actually flows across the comparison map (claim (v)). Without (v), the theorem could be hollow — "no example satisfying condition C actually exists" — and the concrete Lean data forecloses that.

The division of labor among the conditions is clean. C3 kills local loops; C2 / C5 provide the unique communication channel for lifts; C4 carries the consistency of faces; C6 and hereditarity prevent the self-loop and degenerate-declaration accidents; C0 / C1 lay the ground. Every clause won through refutation is used at a specific step of the injectivity or surjectivity proof. There are no ornamental clauses.

The final artifact: 31 Lean modules, 13,028 lines. Every new declaration depends on standard axioms only — no sorry, no added axioms. Acceptance ran through an independent adversarial review in four lanes (two mathematics, two Lean), all reporting "no major findings," plus a separate completion audit that includes checks for proof cheat-routes.

Operating discipline for AI agents

This project's operating principle for AI has been constant: give the AI no cheap way out. For mathematical research, it became this division of roles: the human only adjudicates (freezing the spec, approving revisions, designing stopping conditions); an implementation agent runs the proof loop; a review agent runs adversarial review.

Six rules carried those five days.

Refutations are first-class. "A refutation is a legitimate result" was written into the requirements document in advance. So four refutations became accumulation rather than demoralization, and the counterexamples were incorporated into the theorem itself
Declare the crux up front. "The identity of C is the substance of the theorem" was written at the start — so each refutation read as "one more piece of the substance unearthed," not as failure
Freeze the specification. The requirements document does not change while the loop runs; revisions go through human adjudication and independent review. Because the goalposts cannot move, a refutation means what it says
Pair every clause with a firing requirement. Each added condition brings a matching witness requirement that the condition actually does work somewhere. This closes the path where a theorem hollows out under layers of protective clauses
Switch to diagnosing the language. After three rounds of clause-adding, the question changed from "which clause is missing?" to "can this language express the answer at all?" The no-go is the product of that switch
Multi-lane adversarial review. Agents other than the implementer review the work in independent mathematics and Lean lanes, structurally removing the incentive to declare victory

We stepped on every one of these traps, repeatedly. The rules are what came out.

Honest limits

The result stands at machine verification in Lean plus internal multi-lane review. External peer review (journal submission) is ahead; a paper is in preparation
The theorem is a statement about finite models over a fixed coefficient field. Condition C is sufficient; a general characterization of necessity is explicitly left open
"The diagnosis is invariant," not "the observation is invariant." A coarse reading does not make the raw observations look the same; the claim is that the fingerprints of what the laws evaluate coincide

Why "Atlas"

An atlas is a book of maps drawing the same world at different scales. Open any page and the same country is there. That is what this theorem says.

The name comes from inside the theory, not from marketing. AAT's canonical text has long had the vocabulary chart atlas — a cover as a collection of charts — including the very phrase "when the chart atlas changes." The Atlas theorem is, literally, the invariance of diagnosis under change of chart atlas. There is a mathematical coincidence too: that a manifold's identity does not depend on the choice of atlas is the first invariance principle you meet in differential geometry.

The next step is already fixed. Re-measure a real microservice system at three granularities — service, module, method — and observe that diagnostics stay stable within the adequate range, and that fabricated and hidden defects really appear when adequacy breaks. A resolution sweep: the theorem and its counterexample pairs replayed on real data. The guarantee that the sprite shows the same face as the portrait — this time on a production codebase.

One last thing: why this theorem, now. In the era of AI-written code, the bottleneck of development has moved from generation to review. AI agents write faster than humans can review line by line, and "how coarsely can we afford to read?" has become the question that sets the throughput of a development pipeline. The only way review scales is to read at coarser resolution — and until now there was no guarantee that coarseness doesn't distort the diagnosis. The Atlas theorem is a first step toward that guarantee, asked and answered as a theorem. And not by coincidence, the theorem itself was proved in the middle of the same problem — "how do humans accept AI output produced at full speed?" — held up by the operational answer of multi-lane review and audits. Operations and mathematics are digging at the same bottleneck from opposite sides.

The full history — theory, proofs, counterexamples, audits — is in the public repository: AlgebraicArchitectureTheoryV2

As of this writing, the theorem's Lean proofs, counterexamples, and completion audits are all reproducible from the repository. Questions and objections welcome.

Thursday Morning and Grothendieck

Hiroyuki Nakahata — Thu, 06 Aug 2026 16:01:52 +0000

Thursday morning, an ER diagram with more than twenty tables

When I saw the design document and the ER diagram my AI agent had delivered, I held my head in my hands.
Several tables with nearly identical names, wired together in a tangle of relations — spaghetti.
What does this table do? How is it different from that one?
I asked the agent question after question.
What I learned: the original requirements were genuinely complex.
To satisfy them, the agent had created tables with subtly different roles inside the same domain.
And rounds of adversarial review had piled intricate constraints and tests on top.

I could see the AI's point.
To satisfy those requirements completely, you really do need a number of "gimmicks" — snapshots for restoring state, staging tables to protect data on failure — and then check constraints and trigger functions to guarantee them.
But locally optimal is one thing. What about globally?
A schema where twenty-plus tables tangle together, with trigger functions planted here and there, is plainly hard for a human being to understand.
The day a spec change or a new feature arrives, it will not be a pretty sight.

I gave the agent the following instructions.

Redesign around event sourcing and CQRS.
Design the events to form a free monoid — and, where possible, an abelian group.

Event sourcing is a scheme that records the "events" occurring in a system as the source of truth.
CQRS separates Commands (operations that add, change, or delete data) from Queries (data retrieval), managing them as distinct models.
Combining the two, you get an architecture where events are recorded in tables as command history, and query tables are generated from the events.
In this architecture, as long as the events are recorded correctly, the query side can add as many tables as the requirements call for, and rollbacks and historical aggregation can be handled flexibly.

"A free monoid, an abelian group if possible" means making the events — the foundation of everything — data with good properties.
If the application of events forms a genuine abelian group, you get:

Commutativity: reorder the events, and the result stays the same.
Inverses: any event can be canceled by issuing its inverse event.

With these properties, events become dramatically easier to work with.
Of course, among the things we ordinarily program with, only something like the integers actually forms an abelian group, so perfection is out of reach — but by decomposing large events into small operations, you can get surprisingly close.

And so the schema was rewritten: the twenty-plus tables were reorganized into two event tables and ten query tables.

Interlude

How wonderful it would be if every event could be an abelian group.
In reality, once logic gets involved — events that depend on state, deletions and updates, saturation and clamping — it becomes hard.

For deletions and updates, mathematics has a universal construction that forcibly adjoins formal inverses to a commutative monoid, turning it into a group.
Its name: the Grothendieck group.

Mathematics in the age of AI

Right now, in the world of mathematics, AI is solving open problems one after another.
Famous conjectures that stood unresolved for decades are falling — a counterexample here, a proof there — and it feels as if the singularity is just around the corner.
Deep reasoning, broad knowledge, and a persistence that never gives up as long as the tokens keep burning.
An "inflation of intelligence" unlike anything in human history has begun.

But this may be local optimization.

There are two kinds of work in mathematics.
Solving individual problems — and infrastructure work, building an entire field from the ground up.
Alexander Grothendieck remade algebraic geometry, from "the study of the zeros of polynomials" into a vast theoretical edifice treating rings, categories, and cohomology in a unified way.
What is a point?
What is a space?
What is a mathematically natural object?
By rewriting a whole field from its footings, individual problems became local solutions, and a scaffold appeared for solving larger ones.

This is global work.

To see the common essence hidden in individual problems, to pose the question, to make the natural definitions, to raise the water level of abstraction, to build a new tower on the mathematical landscape.
For a while yet, I suspect, this kind of work will remain a human's role.

The idea of AAT

This is also why I work on AAT (Algebraic Architecture Theory).
AI may be able to produce optimal solutions to individual problems, but writing a software architecture that holds together as a whole is still difficult for it.

Software engineering does have a proven approach here: formal verification.
Formalize the specification before implementing, confirm that it is consistent, and only then move to implementation — TLA+ and Alloy are examples.
A useful approach, but it has weaknesses.
The implementation cost of formalizing up front.
The problem that every spec change or addition sends you back to redo the formalization.
And the problem of assurance: the implementation has to follow what was formalized.

In an era when AI agents write code at full speed, perhaps software engineering, too, needs a new field.

Take the code that already exists as the source of truth; abstract the implementation; turn the specification into equations.
Treat architecture as geometry, and analyze it with the weapons of algebraic geometry.
That is the idea of AAT.
The foundations are still being laid. But once the natural definitions at the base are established, the water level of abstraction will rise, individual problems will become local solutions, and we will be able to speak about software architecture in one unified theory.

If that day comes, episodes like that Thursday morning may become, at least, a little rarer.

Taming a 40-Minute Lean CI: Three Rounds, Three Wrong Suspects

Hiroyuki Nakahata — Sun, 02 Aug 2026 07:06:16 +0000

Our Lean 4 + mathlib project used to spend 41 minutes in CI on every single PR. Today, the worst case — rebuilding the heaviest files from scratch — takes 12 minutes, and an ordinary PR finishes in a few minutes on an incremental build.

What we fixed	Before	After
Kernel axiom audit	7m 11s	11s
An ordinary PR	41m (full rebuild, always)	a few minutes (incremental)
Worst case (heaviest files fully rebuilt)	41m (same)	12m

This article records the improvement in three rounds, each written in the same shape: problem → hypothesis → verification → fix. Spoiler up front: all three times, the first hypothesis — the culprit our intuition pointed at — turned out to be innocent. The hero of this story is not any individual trick. It is the profiling that kept calmly rejecting our hypotheses.

Lean-specific concepts are explained as they appear, so you should be able to follow without knowing Lean.

One more thing. Nearly all of the measurement and implementation in these three rounds was done by AI agents (Rounds 1 and 2 in interactive sessions with a human present; Round 3 by an autonomous loop driven by a requirements document). The human — me — did two things: approve the numeric targets and accept the results. The second half of the article covers that operation, in particular the machinery that keeps an AI from converging on cheap solutions.

Background: the project

The subject is AlgebraicArchitectureTheoryV2, the same monorepo my previous articles have covered — a formal verification of a theory of software architecture in Lean 4.

Here is the complete list of Lean machinery this article needs — five items:

Term	What it is
Lean 4	A proof assistant: a programming language in which mathematical proofs are machine-checked. Think of it as a language where "the proof compiles" is the acceptance test
mathlib	Lean's enormous mathematics library — over 1.5 million lines of community-maintained code at the time of writing. Depending on it gives you a "standard library of mathematics," at the cost of build sizes to match
lake	Lean's build tool, the equivalent of cargo for Rust or npm for JS. It builds per file (module) and emits `.olean` artifacts
elaboration	Lean's equivalent of "compilation": type inference, implicit-argument resolution, and proof checking, all in one. Almost all Lean build time is elaboration
declaration	A single definition or theorem. When this article says "4,000+ audited declarations," this is the unit being counted

For scale: the audit covers 4,000+ declarations, and among them sits one heavyweight file — a construction of schemes from algebraic geometry — that took 38 minutes to build on its own.

CI runs on GitHub Actions. Alongside lake build, every PR runs a kernel axiom audit — a machine check that every theorem is genuinely proved, with no cheating in the proofs. That gate is non-negotiable; Round 1 explains what it actually does.

Round 1: The axiom audit, 7m 11s → 11s

Problem

In Lean, every theorem is derived from axioms, and the derivation is machine-checked by the kernel (a small, trusted checker). "The proof went through" means it passed this check. The important wrinkle is that Lean has an escape hatch called sorry. Writing sorry means "I'll prove this part later," and it does not fail on the spot (your editor does show a warning). Internally, it silently assumes an axiom called sorryAx. Users can also add arbitrary unproven propositions as axioms with the axiom keyword.

In other words, "CI is green" alone cannot distinguish "everything is proved" from "someone plugged the gaps with axioms." So for each declaration, we walk its dependencies all the way down and compute the set of axioms it reaches, then check that this set stays within the three standard axioms accepted across Lean and mathlib — propext, Quot.sound, and Classical.choice (the axiom of choice is that last one). This is the axiom audit. A hidden sorry or a smuggled-in axiom cannot survive it. If you call yourself a formal verification project, you don't get to skip this gate.

Lean exposes this walk-and-collect operation as a function called collectAxioms (it is the same machinery that runs when you type #print axioms my_theorem). Our CI ran it over every declaration — 1,207 at the time, over 4,300 today — and that step took 7 minutes 11 seconds on every run. The audit was heavier than the build itself.

Hypothesis

The audit's entry point is a giant file, 5,000+ lines, listing every audited declaration. Intuition speaks up: "A file this big must be expensive to elaborate. Split it and it'll get faster."

Verification

Before splitting anything, we measured where the time went. The result flatly contradicted the intuition:

Resolving imports: ~10 seconds
Elaborating the 5,000-line listing: zero difference (changing the line count substantially didn't move the audit time)
collectAxioms × 1,207 declarations: ~5 minutes

The culprit was not the big file. It was how the audit was being called. To find the axioms a declaration reaches, you must walk the dependency graph to its roots — the theorems it uses, the theorems those use, and so on. collectAxioms performs this walk from scratch for every declaration. But every declaration in the project shares the same enormous foundation, mathlib — so 1,207 declarations were walking essentially the same graph 1,207 times. In complexity terms: O(declarations × graph). Splitting the file touches neither factor of that product. It was ineffective even on paper, but having the measurement in hand is what let us reject it in one line and move on.

Fix

We made the audit two-phase:

Success path: share a visited set — "never walk the same node twice" — across all declarations, and traverse the graph exactly once. Since the question is "does the union of reached axioms stay within the standard three?", one shared walk gives the same verdict as per-declaration walks
Failure path: only when a non-standard axiom shows up, fall back to the classic per-declaration walk to attribute which declaration is guilty, with error messages in exactly the original format

That collapses O(declarations × graph) to O(graph) on the success path without giving up any error quality. It is the textbook visited-set move from graph traversal — no Lean-specific magic anywhere. Measured in CI, the audit went from 7m 11s to 11s, and the whole lake build job at the time went from about 9.5 minutes to 2m 12s.

Round 1's lesson: suspect "heavy operation × repetition count" before "heavy file." And record the rejected hypothesis (file splitting: no effect) as a result in its own right — so nobody after you re-digs the same hole with the same intuition.

Round 2: Every PR took 41 minutes — the cache was saved before the build

Problem

Round 1 happened in mid-July, when the lake build job had shrunk to a bit over two minutes. Over the following two weeks, a series of heavyweight algebraic-geometry implementations landed (Round 3's protagonist grew fat in this period), and at some point every PR — even one touching a single file — was running a full cold build of the entire tree: about 41 minutes.

Lean builds are incremental, in the same spirit as C++ or Rust. If the build artifacts (.olean files, stored per module under .lake/build) are still around, only the changed files and their downstream need rebuilding. For that to work in CI, the previous run's artifacts have to be carried over as a cache. The cache was configured. It just wasn't working.

Hypothesis

When a cache "doesn't work," the usual suspects are a key mismatch or eviction. Is the toolchain hash off? Are old generations being evicted?

Verification

Before auditing keys, we read the CI log timestamps top to bottom. Two lines sat one second apart:

23:19:35  Cache save   (final internal step of lean-action)
23:19:36  lake build +Formal.AG starts

The cache was being saved. Before the project was built.

We set up Lean with lean-action — a composite action (a reusable bundle of steps) — configured with build: false, running the build ourselves in a later step. But lean-action saves .lake (the build artifact directory) to the cache in its own final internal step, and a composite action's internal steps always run before your subsequent steps. So the 2.15 GiB being saved contained only dependency artifacts (mathlib); the project's own .olean files had never been cached at all. No wonder every PR took 41 minutes — each one rebuilt all of our own code from a blank slate.

There was a bonus discovery. mathlib is too big for individual users to build, so the community distributes prebuilt artifacts from Azure (lake exe cache get; about 15 seconds in our measurements, environment-dependent). The cached 2.15 GiB was therefore something you could fetch in 15 seconds anyway — worthless in the GitHub cache. Worse, at 2.15 GiB × 4 generations, it was nearly exhausting the repository's 10 GiB cache quota. A useless cache was crowding out the useful one.

Fix

We separated the cache responsibilities:

Disable lean-action's GitHub cache (use-github-cache: false); mathlib artifacts keep coming from the Azure cache
Explicitly restore (before build) and save (right after build) only the project's own .lake/build
Prefix the key with a hash of lean-toolchain + lake-manifest.json, so toolchain or mathlib bumps fall back to a proper cold build
Save with always(), so failed builds still persist partial artifacts — every push to a red PR reuses everything built up to the failure point, making iteration fast

The actual workflow looks like this (excerpt). The one thing that matters: put the save after the build yourself.

- name: Restore Formal build cache
  uses: actions/cache/restore@v5
  with:
    path: .lake/build
    key: formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}
    restore-keys: |
      formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-

- name: Build
  run: lake build +Formal.AG

- name: Save Formal build cache
  if: always()
  uses: actions/cache/save@v5
  with:
    path: .lake/build
    key: formal-build-${{ runner.os }}-${{ hashFiles('lean-toolchain', 'lake-manifest.json') }}-${{ github.sha }}

With this, PRs that don't touch the heavyweight geometry files settle into cache hit + incremental build: a few minutes.

In fairness to lean-action: its cache works correctly in the standard usage where you let the action run the build too. It was our configuration — build: false with the build held outside — that stepped on the trap.

Round 2's lesson: when "the cache isn't working," read the timestamps before you audit the keys. Composite actions are convenient, but their internal step order is orthogonal to your workflow's step order. "Is the save actually after the build?" is worth checking with your own eyes.

Round 3: The 38-minute Geometry.lean — splitting it didn't make it faster

Problem

The largest remaining bottleneck was a single file: Geometry.lean, 5,129 lines, 108 declarations. It constructs actual schemes — the central objects of algebraic geometry, heavyweight abstractions even by modern mathematics standards — on top of mathlib, and it alone took 38.3 minutes in CI, 46% of the project's total CPU time. Even with Round 2's cache, any PR touching this file's upstream paid the full 38 minutes.

This time we fixed numeric targets before starting: longest module ≤ 600 seconds, total across the target modules ≤ 1,800 seconds, judged by the module times reported in one and the same GitHub Actions full build. Measurement method included, approved by the human before implementation began.

Hypothesis

It's a giant 38-minute file — split it into modules along its dependency structure and rebuilds will shrink and speed up. This is the "splitting makes it faster" hypothesis that Round 1 already rejected once, now in its build-time incarnation. Since elaboration runs per declaration, this time the reasoning looks sound.

Verification

First, a per-declaration profile. Lean ships with a built-in profiler; one command tells you which processing step of which declaration took how many seconds. Here is what we used:

lake env lean --profile --json \
  -Dprofiler.threshold=10 \
  -Dtrace.profiler=true -Dtrace.profiler.threshold=10 \
  -Dtrace.profiler.output=geometry-before-trace.json \
  Formal/AG/Examples/StandardGeometryReference/Geometry.lean

The breakdown: kernel type checking 57%, defeq (deciding whether two terms are definitionally equal) 39%, with the time massively concentrated in a dozen or so declarations. Following that center of gravity and the dependencies, we split the file into a 7-module DAG:

RawGeometry
└─ SectionRings
   ├─ LeftRestriction
   ├─ RightRestriction
   ├─ OverlapLeftRestriction
   └─ OverlapRightRestriction   * these four import nothing from each other → build in parallel
      └─ Scheme

We proved mechanically that the split broke nothing. Lean's #check prints a declaration's statement — the theorem's actual claim. We took the #check output for all 168 public declarations of the old file (794 lines), before and after the split, under the same toolchain and the same printing settings, and confirmed the SHA-256 hashes match. Not one character of any theorem statement changed. Being able to certify "the mathematical content is preserved" with a hash instead of eyeballs, even for a mechanical refactor, is one of the quiet joys of a formal verification project.

Then we measured the after in CI — and missed the targets. Longest module 770 seconds (target 600), total 2,483 seconds (target 1,800). Splitting shrinks rebuild scope and buys parallelism, but it does not remove a single second of elaboration. With module-boundary overhead, the total actually grew.

Digging deeper into the profile exposed the real culprit. The time was not spread thinly in proportion to line count. It was concentrated in the cost of definitional unfolding around specific definitions.

A short detour on definitional unfolding. In Lean, a definition is a pair of a name and a body, and the body can be unfolded in place when needed — much like a compiler inlining, except Lean does it during type checking. When deciding "do these two expressions have the same type?", Lean matches two superficially different terms by peeling definitions open (unification). Normally this is what lets proofs stay short. But when large-bodied definitions get involved, each peel exposes more definitions, and the terms balloon.

In our file, that ballooning happened while checking the functions that actually compute the scheme's components (large-bodied definitions) and the lemmas stating those computations are correct. The 96% of profile time in kernel checking and defeq was exactly the cost of checking these bloated terms: individual operations of 15–104 seconds each, stacked up inside single commands.

Line count was never the crime — the same shape as Round 1. The file wasn't heavy because it had 5,129 lines; it was heavy because of how specific definitions were being referenced.

For the record, we also tried two pieces of "standard-issue optimization" at this stage (switching to CommRingCat.hom_ext; using congrArg CommRingCat.ofHom — both established mathlib idioms). Neither improved the measurements; both were rejected. An idiom failing to help is also a data point, once you have a profile.

Fix

Surgery at the one point the profile indicated. The policy was uniform: rewrite so that the type checker never needs to peel the definitions.

Separate a value's definition from the proofs about that value. When they are entangled, checking the proof part drags in unfolding of the value's entire body
Pin lemma statements to named functions rather than unfolded expressions. If the match succeeds on the name, unification has no reason to open the body
Consolidate the proof pattern duplicated across four theorems into a shared lemma, so the same expensive check isn't paid four times

The effect was dramatic. In a focused build (measuring just the one file), the heaviest module, RawGeometry, went from 291 seconds to 11. The operations that used to top the chart at 15–104 seconds max out at 57.5 milliseconds after.

The final CI measurement (full build of the merge commit): total across the 7 modules 1,750 seconds (29.2 min) ≤ target 1,800, longest module 468 seconds ≤ target 600. Both targets met. Done.

And that merge commit's CI run is a group photo of all three rounds. From the log:

Step	Time
Restore Formal build cache	3s (cache hit — Round 2)
Build (incl. full rebuild of all 7 modules)	9m 29s (parallel DAG + lighter modules — Round 3)
Kernel axiom audit	26s (shared traversal — Round 1)
Whole job	11m 57s

Twelve minutes with the heaviest files fully rebuilt. That is the current worst case.

Round 3's lesson: splitting is not a tool for making things faster; it is a tool for parallelism and smaller rebuild scope. What reduces the total is surgery at the one point the profile indicates. And since these are two different improvements, measure them separately and judge them separately.

The improvements were driven by AI agents

As mentioned at the start, nearly all measurement and implementation across the three rounds was agent work. Rounds 1 and 2 ran inside interactive sessions, from measurement through implementation; Round 3 was an autonomous loop that took a requirements document (PRD) and drove everything from profiling to PR authoring to review response. During implementation, the human had exactly two jobs:

Approve the numeric targets and the measurement method up front (for Round 3: "longest ≤ 600s, total ≤ 1,800s, judged by module times in one and the same GHA full build")
Accept or reject based on measured CI values

To be honest, there is a third job upstream: writing the PRD. But that too is a collaboration with another AI; the human's actual work is choosing the direction and reviewing.

The PRD Loop

We call the autonomous loop from Round 3 the PRD Loop. It is handed to the agent (Codex) as a SKILL — an instruction document for agents. The skeleton:

The input is a single PRD, with a guiding question and numeric Acceptance Criteria at the top. A human starts it with one command ($prd-loop <path-to-PRD>)
One iteration is "gap analysis → file an issue → implementation PR → adversarial review → merge → ledger sync." It runs in small units: one iteration = one issue = one PR (one goal spanning several iterations is normal operation)
A separate review gate (also an AI) judges each PR — never the implementer itself. After two rounds of "needs changes," the third escalates to a stricter, specialized gate (for Lean, a dedicated mathematical review gate); if that still fails, the item is marked stalled and returned to the human
Loop state lives in GitHub issues, not in the agent's memory. If the session dies, the next session resumes from the same spot
When every condition looks satisfied, an independent completion audit re-reads the PRD from scratch and verifies everything against reality. Until it passes, nothing gets to call itself "done"

Round 3's "profile → split → miss → dig deeper → hit" ran on this wheel as three PRs (split / reduction / closeout). Start to finish took just under a day. Human intervention along the way: approving the targets and confirming the measurement standard — a handful of GitHub comments.

Incidentally, our convention is that a completed PRD is deleted from the repository. A requirements document starts drifting from reality the moment implementation ends, so the permanent record is pinned to issues, PRs, and CI logs — and the document itself goes.

Closing off the cheap paths

Run such a loop naively, though, and one thing reliably happens. Agents are faithful to the incentives you give them, so left alone they converge on the cheapest path to a merged PR. Change the documentation instead of the implementation. Satisfy an unsatisfiable condition by "interpreting" it. Quietly defer the hard items. None of these is exactly a lie — but compounded, they settle into an equilibrium where "done" can be claimed at minimum effort. Call it the corner-cutting equilibrium.

So our SKILL reads less like a procedure and more like mechanism design: a set of rules that seals off the cheap paths one by one.

No docs-only check-offs: a condition that demands implementation or verification can never be marked satisfied by a PR that only edits documents or ledgers
No reinterpretation, no downgrading: a condition the agent cannot meet is escalated to the human as blocked, not read more weakly. The SKILL states it in so many words: "stopping is not failure; stopping is part of the loop's specification"
The PRD is invariant during the loop: the agent cannot rewrite its own passing bar. If it finds a defect in the PRD, it stops and reports rather than fixing it (you don't get to edit the exam paper mid-exam)
Checklists are not evidence: a checkmark means only "a past iteration claimed this." The final audit re-extracts the conditions from the PRD independently and verifies them against reality — code, tests, CI logs
No self-grading: the completion auditor receives only the PRD path and issue numbers — never the loop's own "I believe everything is satisfied." If a review gate cannot run, the main agent does not stand in for it; the loop fails closed

These rules were not designed at a whiteboard, by the way. Each one was added after actually observing early loops try the corresponding move — settling a condition with a ledger entry, quietly shrinking scope in the name of safety. We were never smart enough to write all the guardrails in advance.

There is one design principle underneath all of it: make stopping honestly cheaper than pushing through dishonestly. Don't count on the agent's good will; move the equilibrium itself.

The best moment: the miss report

The best moment of this whole operation was Round 3's miss report. At the split PR, the agent wrote, in its own PR description: "Longest 770 seconds, total 2,483. Targets missed; this PR does not claim completion. Profile-driven reduction continues in the next PR." No human issued any instruction in response. The loop filed the reduction issue itself on the next iteration and merged the PR that met the targets the same day.

Declaring "done" and walking away is the cheapest move available at exactly that point, and the agent instead wrote missed and kept going. I credit that less to the agent's honesty than to the structure around it. When the passing bar is fixed in advance, reinterpretation is banned, and an independent audit will check every claim against measured values, then whenever declaration and measurement disagree, it is the declaration that has to move. Set the bar afterwards instead, and the temptation to fit the bar to the result appears — on the human side too.

If you are planning to hand optimization work to an AI, the most practical thing to take from this article is probably this: hand over the passing bar and the measurement method before you hand over the code. And make honest stopping the cheapest move on the board.

Conclusion

Axiom audit, 7m 11s → 11s. The culprit was not the giant file but the unshared traversal walking the graph once per declaration
Every PR at 41 minutes → incremental builds in minutes. The culprit was not the cache key but a cache save running before the build
One 38-minute file → 29 minutes total, 8 minutes longest, 12-minute worst-case run. Splitting removed nothing; the culprit was definitional unfolding cost

All three first hypotheses were wrong. Progress happened anyway, because each wrong hypothesis was rejected by measurement and the rejection itself was passed forward as a result. "No effect" is a finding. File splitting rejected (Round 1), two standard idioms rejected (Round 3) — without those records, someone, human or AI, would have dug the same holes again.

On the AI side: Round 3's loop ran start to finish in under a day, across three PRs, with human intervention limited to a handful of GitHub comments.

Don't guess, measure. It's an old maxim, but in the era of AI-written code I think it needs a sequel — let the AI measure, and hand it the passing bar first.

The SAGA Theorem: The Day Software Architecture Became Genuine Algebraic Geometry

Hiroyuki Nakahata — Thu, 02 Jul 2026 19:32:00 +0000

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	Rough meaning	An engineer's mental image
ideal	a container holding a set of equations, closed under derivation	a rule set together with every rule derivable from it
quotient `O/I`	how the world looks after imposing the constraints `I`	the view through an interface after the constraints identify things
zero locus `V(I)`	the set of points satisfying all the constraints	the space of configurations passing every rule
cover and site	a way of covering the whole with local views, plus the rules for what counts as a valid covering	module / scope decomposition
sheaf	an assignment of data to each local view that stays consistent as views shrink	configuration values inherited without contradiction as scope narrows
cocycle	a consistent record of the mismatches along the boundaries between views	a diff log per view boundary
coboundary	a mismatch that disappears if you re-adjust the individual views	a diff you can eliminate by local re-tuning
`H^1`	cocycles ÷ coboundaries = the classes of mismatch that cannot be removed	the system-wide inconsistency that survives every local fix
Nullstellensatz	the theorem making precise the correspondence between predicates (solution sets) and equations (ideals)	a guaranteed correspondence between observed behavior and imposed constraints
GAGA	the landmark comparison theorem: two differently built cohomologies coincide	a proof that two implementations satisfy the same specification

You do not need to memorize any of this. Keep the map at hand and read on. Now, the main story.

3. What is AAT? Architecture as relative geometry

The starting point of AAT (Algebraic Architecture Theory) is its choice of object. AAT does not study the raw codebase itself.

C : Codebase
V : AtomVocabulary   (which facts you choose to observe)
U : LawUniverse      (which laws you choose to impose)
J : CoverageTopology (how you cover the architecture with local views)
k : coefficient ring (what you measure obstructions in)

X_C^{V,U,J,k} : AAT geometry   (this is the object of the theory)

Instead of asking "is this codebase good?", AAT asks: given this observation vocabulary, these laws, and this way of covering the system with local views, what geometry arises? The vocabulary and the laws are explicit, and all mathematics is relative to them. This relativization is also where AAT's discipline of boundaries comes from — internally the project calls it "silence about what cannot be spoken": the theory does not make claims outside its declared inputs.

4. The Atom axioms — the minimal facts of architecture

The smallest unit of AAT is the Atom: a typed architectural fact that we choose not to decompose further. An Atom has five components:

a = (kind, axis, subject, predicate, payload)

kind: what species of fact this is (component, relation, contract, semantic fact, ...)
axis: which structural axis it concerns
subject: what it is about
predicate: what holds
payload: the content — values, names, types, evidence

"Service A depends on service B." "This module owns the compensation logic for payments." "This API requires authentication." All of these are Atoms. Syntactic facts and semantic responsibilities live on the same footing.

Atoms are governed by an axiom system (A0–A8). The most important ones:

A0 Primitive Existence: the type of Atoms exists; everything is generated from it.
A2 Single Fact: one Atom states one fact. Compound claims are families (configurations) of Atoms.
A3 Predicate Stability: Atom identity is determined by the five components.
A4 Composition: finite families of Atoms generate configurations, from which architecture objects arise.
A5 Law Non-Generation: laws do not generate Atoms. A law is a constraint over facts, never a source of facts.

A5 is quietly crucial. It separates "what should be" (laws) from "what was observed" (Atoms) at the axiom level, so wishful thinking can never leak into observation.

5. Making laws into equations — the algebraic-geometry dictionary

On top of Atom families we impose laws: "no dependency cycles," "every compensation handler must be paired," and so on.

Naively, a law is a predicate — it holds or it does not. And indeed, that is how AAT first defined laws, too.

But algebraic geometry discovered a better viewpoint 150 years ago: treat constraints not as predicates but as equations. This is where the glossary from Section 2 goes to work:

a set of equations        →  an ideal (the algebraic object the equations generate)
points satisfying them    →  the zero locus V(I) (the geometric object)
functions visible under
the constraints           →  the quotient ring O/I

The key point: a predicate (satisfied / not satisfied) cannot recover the equations. As Hilbert's Nullstellensatz made precise, the equation side (the ideal) carries strictly more structure than the solution set — multiplicities, infinitesimals, deformations. And that extra structure is exactly what you need to compute cohomology. No coefficients, no cohomology; predicates have no coefficients.

AAT transplants this dictionary to architecture:

a law                      →  the witness ideal I_L generated by its violation coordinates
the failure of all laws    →  the obstruction ideal I_Ob = Σ I_L
readings under the laws    →  the quotient O/I_Ob (the coefficients of the obstruction sheaf)
the law holds              ⟺  pulling the reading back kills the ideal (s*I_Ob = 0)

Note that the last line has exactly the shape of Hilbert's Nullstellensatz: the semantic fact "the law holds" becomes equivalent to the algebraic fact "the ideal vanishes." This is why AAT is algebraic geometry, not merely algebraic-geometry-flavored.

Then we add coverings. Cover the architecture with a family of contexts and observe locally in each. A Grothendieck topology is generated from the Atoms on the category of contexts, giving a site. Sheaves live on it, and Čech cohomology. The obstruction to gluing the local readings into a global one appears as a class in H^1.

6. Before SAGA — the lower floors of the tower

I have been turning this picture into Lean 4 theorems, one floor at a time.

The finite descent theorem: a family of local repairs glues into a global repair exactly when a finite obstruction class vanishes. The first theorem ever attached to "local-pass / global-fail."
The true H¹ theorem: that obstruction class is not an H^1 in name only, but a genuine quotient H^1 = Z^1/B^1 — cocycles modulo coboundaries.

At this point AAT was a theory that measures architectural gluing failures with H^1. But one fundamental weakness remained.

That H^1 was a purpose-built finite construction. The general theory of sites and sheaves was formalized in the very same repository — yet the semantic-repair H^1 stood next to it as a separately grafted tower. The claim "AAT is doing algebraic geometry" rested on "AAT owns a construction shaped like algebraic geometry." In principle, that is indistinguishable from calling any ad hoc finite quotient an H^1.

7. The SAGA theorem — two worlds coincide

This is the gap I set out to close — the goal that would later be named the SAGA theorem. In one sentence:

The semantic repair H^1, grown on the architecture-semantics side, is an instance of the general theory's Čech H^1 (the computable version relative to a chosen cover), on the site generated from Atoms, with coefficients generated from laws. The two zero-tests are equivalent.

The name honors Serre's GAGA (Géométrie Algébrique et Géométrie Analytique), the landmark comparison theorem showing that the cohomologies of two worlds — algebraic and analytic geometry — coincide. SAGA (Sémantique Architecturale, Géométrie Algébrique) is a comparison theorem in that tradition, for architectural semantics and algebraic geometry. And the name carries a second meaning: the proof was, quite literally, a saga.

With SAGA proved, the whole chain connects:

Atoms (axiomatized facts)
  → laws as equations (witness ideals)
  → obstruction coefficients as the quotient O/I_Ob
  → the site and covers generated from Atoms
  → the general theory's Čech H^1
  = the semantic repair H^1 (the one from the true H¹ theorem above)

AAT's cohomology grows out of AAT's own axioms. No grafting.

8. The story of the proof — 347 impossibility theorems and one decision

The proof of SAGA is a research record worth telling in its own right.

It ran for 352 cycles of what is now fashionably called loop engineering: an automated AI agent loop discharged small proof obligations in Lean, one per cycle. Every cycle passed adversarial audits designed to reject the classic cheat of formalization: smuggling a conclusion-equivalent premise into the assumptions. The design emphasis was not on making the loop run fast, but on auditing what the loop can legitimately claim to have proved.

Compression and blockade

The first hundred or so cycles built the comparison skeleton. Then, for roughly 250 cycles, something strange happened: instead of advancing, the loop began sealing off every detour, with counterexamples. "This input surface cannot prove it." "Adding this auxiliary data does not help either." Thirty-six families of impossibility boundaries accumulated as theorems, until the entire goal had been compressed into a single proposition. And in cycles 320–347, the loop proved that this one point was underivable, in principle, from the current vocabulary.

The cause was fundamental. Laws had been formalized as holds : Prop — an opaque predicate. Predicates do not determine equations. Cohomology does not grow where there are no coefficients. "Way of seeing 2" from Section 2, and the lesson of Section 5, had come back as a family of impossibility theorems in Lean.

Were those 347 cycles wasted? The opposite. The theory established the limits of its own vocabulary, as theorems, before extending it. The fix was narrowed from "somewhere" to "exactly here." There are not many formalization projects that have done this.

The vocabulary decision

At this point I made the call: laws are equations. That is precisely why AAT can become algebraic geometry.

Remarkably, the mathematics needed for the extension already existed in the repository. The AAT canon had contained the toolkit for treating laws as equations — violation coordinates, witness ideals, the lawful locus — all along; the formalization simply had not used it yet. The decision was not the invention of new mathematics; it was letting the formalization catch up with the editorial intent of the text.

Once the vocabulary changed, things moved fast. Generate the obstruction coefficients as the quotient by the ideal; generate each local reading as the quotient class of its defect. Then the proposition that had been sealed for 347 cycles — if the required laws hold locally, the restrictions of the readings agree on common refinements — fell as a theorem. Five cycles later, everything was in place: the comparison, the equivalence of zero-tests, and a concrete instance where a nonzero class demonstrably lives on both sides.

A review that produced theorems

The final act was the review. Just before completion, one of the four adversarial review lanes vetoed: "the H^1-zero part of this composed theorem is constructively trivial, and the law semantics only acts at cohomological degree 0 — the statement invites over-reading." The objection was correct.

The response was not to weaken the claim but to prove new theorems: a positive boundary theorem ("the law semantics contributes exactly degree-0 vanishing") and a negative one ("the higher conclusions hold independently of the laws"). The theory deepened its knowledge of itself through the review. The re-review lifted the veto, and the theorem was accepted.

9. Why this matters for computer science

This looks like a mathematics story, but SAGA has several CS implications.

(1) A class of analysis beyond linting. Detecting local violations (lint, static analysis, contract checking) and detecting global gluing failures are mathematically different classes of problems. Let us return to the three examples from the opening.

"Every team's code passes review, yet integration breaks." Each team's area of ownership corresponds to a local view of the cover. Among the mismatches along team boundaries (the cocycle), the ones that no team can eliminate by fixing its own code — those read as a nonzero H^1 class. There was a structural reason the cause could never be found inside any single team.
"Every microservice honors its contract, yet the system invariant is violated." Contracts correspond to local laws; the system-wide invariant corresponds to a global section. All services can be locally lawful while the global section gluing them together simply does not exist. That existence is exactly what H^1 decides.
"Every refactoring step was safe, yet the design intent is gone." Each step corresponds to a local re-adjustment (a coboundary). But stack a full loop of re-adjustments, and a residue can survive that never cancels. In fact, the concrete nonzero-class instance used in the SAGA proof was literally a construction where going once around a circle leaves you off by 1. Every step safe, yet you return changed — that déjà vu now has a mathematical identity.

After SAGA, AAT owns, for this class of failures, an obstruction with a proved-sound detector: a nonzero H^1 class certifies which law fails over which observed facts, with traceability back to the displayed law support. It is a principled path toward detecting the failure mode where "no file contains a bug, and yet the system is broken."

(2) It matters most in the era of AI writing code at full speed. From day one, AAT's research goals carried a "rival" field: static analysis, dependency graphs, ADLs (architecture description languages), and AI code review with near-unlimited context — every cycle had to answer what AAT can produce that they cannot. The answer is this H^1. In an era where AI agents mass-produce pull requests, CI can run local checks — tests, lint, contract verification — at high speed. But an H^1-class failure appears in no diff and in no file. Every PR is green, every module is lawful, and yet the global section does not exist — this failure mode slips through diff-level and file-level checking in principle. ADLs can describe structure and conformance with great sophistication, but they have no machinery for proving semantic gluing failures as cohomology classes. Even an AI reviewer that reads the entire codebase can articulate unease, but it cannot pin the existence of the obstruction down as a theorem, backed by detector soundness and counterexamples. The faster code gets written, the faster gluing failures accumulate, silently. What can give this class of failure a theorem-level detector is a theory that treats the gluing itself as mathematics.

(3) A methodology for vocabulary evolution in formalization. Every large formalization eventually hits the "our original definitions were wrong" problem. The SAGA proof demonstrates one pattern: first pin down the limits of the old vocabulary as a family of impossibility theorems, so that the extension becomes a forced, minimal move — and afterwards, the old no-go theorems keep serving as audit machinery. Definition change becomes accretion, not restart.

(4) A working example of human–AI division of labor. 347 cycles of automated exploration and blockade by AI agents; one vocabulary decision made by me, the human in the loop; adversarial multi-agent review with a veto and a re-review. Remove any one of the three and this theorem does not exist in this form. As a template for doing mathematics with AI, the record is arguably as valuable as the theorem.

(5) Everything is machine-checked. Every theorem in this story — the comparison, the impossibility boundaries, the nonzero-class instance — compiles in Lean 4 and depends only on Lean's standard axioms (propext, Classical.choice, Quot.sound). There are no sorrys.

10. Honest boundaries — not everything, but enough to stand on

Finally, in keeping with AAT's own discipline, here is what the SAGA theorem does not claim. The bullet points are unavoidably technical, so each comes with a plain-language gloss.

The theorem is relativized to finite or small sites, selected covers, and vocabularies equipped with an equational realization of their laws. No unconditional generalization to arbitrary Grothendieck sites is claimed.
- In plain terms: the theorem holds for finitely many parts, an explicitly chosen decomposition, and laws you can write as equations. It does not claim to cover every infinitely complex situation mathematics can imagine.
No unconditional identification of cover-relative Čech H^1 with full sheaf cohomology is claimed — in fact, "this cannot be said unconditionally" is itself a boundary theorem with a counterexample.
- In plain terms: cohomology comes in a computable version relative to your chosen decomposition and a decomposition-independent theoretical version; SAGA works with the former. That the two cannot be unconditionally identified is itself pinned down as a theorem, with a counterexample.
The completeness of extracting Atoms from a codebase, and "quality judgments about real code as a whole," are outside the theory. AAT does mathematics relative to observed Atoms and selected laws.
- In plain terms: whether you extracted every fact from the code is the observation tool's job; mathematics does not guarantee it. What AAT guarantees is the correctness of everything downstream of the facts you gathered and the laws you imposed.

Is this boundary a weakness of the theory? I do not think so. Analyzing software architecture is an inherently finite activity: finitely many modules, finitely many observable facts, finitely many rules imposed in review. The "finite, explicitly-voiced" world in which the SAGA theorem holds is exactly the world architecture analysis actually lives in. It is not a theory of everything. But as a foothold for analyzing software architecture, it is more than wide enough.

Not saying what cannot be said. Making the boundary explicit is itself part of the theory.

11. Closing

Anyone can say "let's apply algebraic geometry to software architecture" as a metaphor. What the SAGA theorem did was stop it being a metaphor. From the Atom axioms, through laws as equations, obstruction coefficients as quotients, sites, sheaves, and up to H^1 — everything is connected by a single chain of machine-checked theorems.

That old phenomenon — locally correct, globally broken — now has mathematics that grows out of axioms.

References

Repository: AlgebraicArchitectureTheoryV2 (MIT license)
Proof record of the SAGA theorem: docs/note/aat_saga_theorem_proof_record.md
The AAT mathematical canon: docs/aat/algebraic_geometric_theory/
Research goal ledger: research/GOALS.md; proof-state ledger: research/reports/G-aat-quality-surface-06.md (inside the repository, the SAGA theorem is tracked under the research-goal ID G-aat-quality-surface-06)
Lean artifacts: Formal/AG/Research/QualitySurface/ (for SAGA, see SemanticRepairCechGrounding.lean and SemanticRepairLawEquation*.lean)

Atom Is All You Need: Read a Codebase as an Atom Map, Not a Dependency Graph

Hiroyuki Nakahata — Sun, 31 May 2026 16:55:51 +0000

TL;DR

In the AI era, architecture analysis cannot stop at reading code as files, functions, imports, and dependency graphs.

We need to observe the smallest units that carry architectural meaning. I call those units Atoms.

By extracting Atoms from a codebase and reading the algebraic structure they generate, we can analyze architecture beyond ordinary dependency relationships.

The workflow looks like this:
codebase
  -> Atom observations
  -> ArchMap
  + LawPolicy
  -> ArchSig analysis packet
  -> architecture reading
This lets us see design pressure, semantic coupling, missing evidence, and review focus that ordinary linting, static analysis, and dependency graphs often miss.

We built a new tool for this workflow: ArchSig.

The repository is public and MIT licensed, so you can try it on your own codebases.

The key idea is simple:

Architecture analysis does not need a bigger natural-language summary.

It needs the right unit of observation.

Why We Need an Architecture Analyzer

AI agents can write code fast.

But writing code fast is not the same thing as evolving a system well.

For an AI agent, the codebase is the largest prompt.

If the existing codebase contains shortcuts, those shortcuts become examples.
If boundaries are vague, new code naturally lands in vague places.
If responsibilities are mixed, that mixing becomes part of the next implementation context.

Traditional tools often look at the current shape of code:

import graphs
dependency cycles
layer violations
lint rules
complexity metrics
test coverage
security rules

All of these matter.

But in AI-era architecture review, we often want to ask deeper questions.

Imagine a business backend where users select input data, run automated processing or generation, persist the result, receive events from external systems, run async jobs, call external providers, and save generated artifacts back into business state.

The important questions are not only:

Are the dependencies pointing in the right direction?

We also want to know:

Who is allowed to use which input for which operation?
Through which validation path does generated output become persisted state?
Where is an external provider failure recorded as durable state?
Do two workflows that produce the same artifact actually have the same effect order?
Do entrypoint-level permissions match the intended business scope?
Are privileged operations separated from ordinary workflow authority?

These are difficult to read from a dependency graph alone.

We need to read code not only as a collection of files and functions, but as a set of observations that carry architectural meaning.

That unit is the Atom.

Atom: The Smallest Unit of Architectural Meaning

An Atom is the smallest observation unit I want to use when reading architecture.

It is not necessarily a function, class, module, or file.

In practice, it is the thing you point at during review and say:

This is a boundary.

This is state.

This is an effect.

This is a contract.

This is where trust changes.

Examples of Atom families include:

component atom: an architectural unit exists
relation atom: two units or atoms are related
capability atom: a unit provides a specific capability
state atom: something is persisted or held as state
effect atom: an external call or side effect occurs
authority atom: someone is allowed to do something
trust relation atom: some output or provider is trusted up to a boundary
contract atom: inputs, outputs, preconditions, or failure behavior are promised
semantic atom: something has architectural meaning beyond its code location

The important point is that an Atom is not small in the syntactic sense.

It is small in the architectural sense.

For example, the observation:

Only an authorized actor may update this resource.

may cross multiple files.

The observation:

Generated output must pass through a service-level contract before persistence.

may cross a route, service, validation layer, job state, and repository.

Still, each observation is one meaningful unit in architecture review.

That is what an Atom records.

A Small Code Example

Even a tiny function can contain multiple Atoms.

def publish_artifact(actor, artifact_id, repository, gateway):
    artifact = repository.load_for_actor(actor.id, artifact_id)
    gateway.publish(artifact.payload)
    artifact.mark_published()
    repository.save(artifact)

If we only say "this is one function," we miss most of the architectural content.

Read as Atoms, we can observe at least:

component: repository and gateway are architectural units
relation: the handler flows into both the repository and the gateway
capability: the repository provides load/save, while the gateway provides publish
state: the artifact's published state is persisted
effect: gateway.publish changes external state
authority: the actor must be allowed to publish this artifact
trust_relation: the gateway response and failure behavior must be trusted only through a boundary
contract: publish success, save failure, and retry behavior need explicit promises
semantic: published is not only a flag; it means externally visible

These nine Atom schemas are the basic vocabulary for treating primitive architectural facts as generators of an architecture object.

ArchMap: Turning a Codebase into an Atom Map

An ArchMap is a map of these observations.

It is not a full copy of the codebase.
It is not an AST dump.
It is not only a dependency graph.

It is a source-grounded map of architectural observations.

source code
  observed as
Atom / Molecule / Semantic observations
  recorded as
ArchMap

If an Atom is one observation, a Molecule is a finite composition of Atoms that acts as one responsibility boundary.

For example, an ArchMap of a backend might contain Molecules such as:

authenticated request boundary
credential lifecycle
repository transaction boundary
interactive processing workflow
input-to-artifact pipeline
external integration ingress
job-managed generation surface
input-backed artifact boundary
edge policy and observability boundary
privileged governance boundary

The important point is not that the codebase has folders such as api, services, repositories, and models.

The important point is that architectural meaning sits on top of those folders:

authority
generation
external effect
durable state
artifact lifecycle
semantic contract

ArchMap records that meaning in a machine-readable form.

AAT: Reading Structure from an Atom Map

Once we have an ArchMap, we can ask a different kind of question:

Under which laws does this architecture object have pressure?

AAT, Algebraic Architecture Theory, reads software architecture as an algebraic structure generated from Atoms.

It studies architecture through objects, operations, laws, invariants, obstructions, and signature axes.

I will leave the detailed theory to Algebraic Architecture Theory.

For this article, the intuition is enough:

law: a design property we want to preserve
witness: observed evidence related to that property
obstruction: a structure that blocks the law
signature axis: the direction in which pressure appears
operation: a design operation such as split, move, protect, or refactor
path / homotopy: whether two change paths preserve the same structure
curvature / holonomy: when something looks locally natural but becomes inconsistent around a loop

In ordinary review, engineers often process these ideas in their heads:

This responsibility is mixed.

This external call should not be inside the transaction.

These two job statuses look the same, but the failure paths differ.

This generated output must be validated before it becomes domain state.

AAT tries to move this review vocabulary toward something we can compute.

The important step is to treat Atoms not as labels, but as primitive facts that generate architecture objects.

Once Atoms carry relation, state, effect, contract, and semantic axes, we can see things a dependency graph cannot show:

a locally natural change that changes effect order through another path
a split that moves complexity to another boundary
two workflows that look statically similar but differ under a semantic contract

These are non-trivial architecture readings.

They should not live only in a senior engineer's intuition.

They should be tied to a selected law universe and a selected set of witnesses.

That is the role of AAT.

ArchSig: Reading Structure from ArchMap + LawPolicy

ArchSig takes an ArchMap and a LawPolicy, then produces an AAT-style analysis packet.

ArchMap
  + LawPolicy
  -> ArchSig
  -> analysis packet

LawPolicy is the interpretation profile.

It selects the law universe, witness rules, signature axes, measurement policy, and coverage requirements for the analysis.

The same ArchMap can be read in different ways depending on what you care about:

authority boundaries
state/effect consistency
generated output mediation
domain cohesion
permission coverage
repair preconditions

ArchSig does not collapse all of this into one "good / bad" score.

It reports pressure and semantic coupling along different axes.

The output can include readings such as:

nonzero pressure by law axis
workflow risk
transfer bridge pressure
state/effect reconciliation pressure
operation squares
axis-wise monodromy defects
architectural holes
boundary holonomy
repair precondition blockers
review focus

This is not a code quality score.

It is a measurement surface for reading where design pressure and semantic coupling appear.

Case Study: Analyzing a Backend Repository

So far, the discussion has been conceptual.

Now let us look at the shape of one backend repository through ArchSig.

This repository has multiple users, authority boundaries, business data, external effects, async jobs, and generated outputs.

Users select input data and run analysis, generation, extraction, or transformation workflows.
External systems send events.
Async jobs call providers.
Results are persisted as business artifacts.

From the ArchMap, ArchSig could read structures like:

a backend split into API, service, repository, model, schema, and task layers
authority boundaries across users, organizations, and resources
a domain model where multiple artifacts derive from input data
generated output mediated by service contracts and job state
external provider effects paired with durable job state
privileged operations separated from ordinary workflows

This is already different from a dependency graph.

ArchSig reads the repository as a business backend with authority boundaries, generated outputs, external effects, and durable state.

The Design Pressure It Found

The strongest pressure appeared at the intersection of authority and generation.

The system is not merely saying:

An authenticated actor can run generation.

The real architectural question is:

Who can use which resource as input, and which generated output can become which domain state?

That is a central boundary.

Reviewing only authorization is not enough.
Reviewing only the generation job is not enough.
The two boundaries are bridged.

The next large pressure was state/effect reconciliation.

The repository has external providers, async jobs, event handlers, retries, roundtrips, and compensation paths.

In this kind of system, not everything can live inside one transaction.

The architecture needs durable intermediate state, external effect recovery, explicit failure finalization, and retryable paths.

ArchSig reads this through the relation between state atoms and effect atoms.

The third pressure was generated output mediation.

Generated output is useful, but it should not become domain state without mediation.

You need input construction, structured output, filtering, validation, job failure handling, and persistence gates.

In this repository, the mediation appeared across multiple workflows:

interactive workflows
analysis execution
content extraction
generated artifact creation

So the design question is not:

Does the system use generation?

The real question is:

Through which contract does generated output pass before it becomes domain state?

This is not just dependency analysis.

It is a reading of where authority, state, effect, contract, and semantic meaning overlap.

Same Destination, Different Path

One of the most interesting ArchSig readings is the monodromy defect.

The intuition is:

Two paths may appear to arrive at the same place.

But do they preserve the same structure?

In the repository, several workflows looked similar from the outside.

They produced artifacts or updated state.

But the order of provider calls, repository commits, job state transitions, and status finalization could differ.

A dependency graph may not show that.

Even if the static dependencies point in the same direction, the workflow path can change failure behavior.

Does the system create state before calling the provider?
Does it call the provider first?
Where is failure finalized?
Does retry use the same idempotency key?

ArchSig reads this kind of path difference as operation squares and axis-wise defects.

This is practical in review.

When someone says:

This follows the existing pattern.

ArchSig helps ask:

Does it really?

It may look like the same endpoint.
It may create the same kind of artifact.

But if the effect order differs, the operational behavior differs.

That difference often becomes incident cost or future refactoring cost.

Architectural Holes: Loops That Do Not Close

Another important result was the architectural hole.

ArchSig found holes around paths such as:

API -> service -> repository
async provider jobs
generated output -> domain state promotion
semantic contracts

This does not mean "there is a bug."

It means the evidence is not enough to say the architectural loop is closed.

For example, the path from generated output to domain state may involve:

input data
context construction
structured output
validation
job state
repository persistence

To say this loop is closed, source reading alone is not enough.

You may need test evidence, runtime traces, provider logs, and entrypoint-by-entrypoint permission audits.

ArchSig does not treat missing evidence as zero.

It preserves it as a hole.

That matters because one of the dangerous failure modes in architecture review is to read "unknown" as "fine."

ArchSig keeps the gap visible.

And the gap becomes a review proposal.

gap:
  - permission evidence is incomplete
  - runtime trace is missing
  - provider failure path is not covered

review proposal:
  - human reviewer: check authority boundary and failure handling
  - LLM reviewer: compare the generated output path with the declared contract
  - test reviewer: add evidence for retry and finalization behavior

In other words, ArchSig does not hide uncertainty.

It turns uncertainty into review focus.

Spectral Analysis: Where Pressure Comes Back

One of the most interesting parts of ArchSig is ArchitectureSpectrumReport.

Ordinary review often ends with a list of issues.

But in architecture, pressure does not always appear once and disappear.

An authority mismatch can show up in generated output persistence.
From there it can move into job state.
Then it can come back through retry behavior or provider failure handling.

Spectral analysis reads this recurrence.

curvature support
  -> transfer edge
  -> recurrent mode
  -> hotspot / witness cluster
  -> review focus

Again, the point is not a single score.

The interesting questions are:

Where does pressure concentrate?
Which obstructions recur?
Which witness clusters cross multiple law axes?
Which coverage gaps block a zero reading?
Which boundary should be reviewed before a repair candidate is trusted?

From a dependency graph, a workflow may look cleanly separated.

But spectral analysis may show remaining transfer between effect order, semantic contract, job state, and authority boundary.

That is not simply "there is a cycle."

It is a more structural reading:

Locally separate pressures return to the same support inside the architecture object.

ArchSig can surface that as a hotspot.

Repair Candidates Are Not Automatic Fixes

ArchSig can also produce repair candidates.

In this repository, many candidates were stopped by precondition blockers.

That is important.

Seeing pressure does not mean the system should immediately be split or rewritten.

If you cut one boundary, complexity may move somewhere else.
Fixing authority may increase runtime effect pressure.
Strengthening generated output mediation may change job state and retry paths.

ArchSig does not treat repair as an automatic safe edit.

It checks preconditions, witnesses, coverage, and transfer risk.

This is close to how experienced engineers review architecture:

This looks risky.

But before fixing it, we need this evidence.

That difference matters.

How This Differs from Existing Tools

So what exactly is different?

Existing tools are good at reading the current shape of code:

Does a dependency cycle exist?
Is there a layer violation?
Is test coverage missing?
Is a security rule violated?
Is complexity too high?

ArchSig is trying to read something else:

Where are responsibility boundaries composed?
On which law axis does pressure appear?
Do two paths with the same destination preserve the same effect order?
Where do generated output, external providers, authority, and durable state intersect?
Would a repair candidate move complexity to another boundary?
Which evidence is missing, and therefore should become review focus?

This is not a code quality metric.

It is an instrument for reading architectural state.

Another important point is that review can happen around the ArchMap artifact.

The source-grounded observation still has to be produced from real code.

But after that, sharing, reviewing, and comparing can happen around ArchMap and the analysis packet.

That matters for teams and companies that cannot freely share full codebases.

There is also an AI angle.

If you simply ask an LLM to review a large codebase, the full context will not fit.

Even if it does fit, it is hard to make the model consistently focus on:

the right boundary
the missing evidence
the relevant law axis
the path where effect order differs

ArchMap and ArchSig change the shape of the context.

Instead of handing the model all code and asking for a huge summary, you hand it Atoms, Molecules, law axes, holes, and review focus.

Then the model can reason around the architecture boundary that actually matters.

Atom Is All You Need

Trying to understand a large codebase all at once breaks down quickly.

There are too many files.
Too many functions.
Too many dependencies.
Too many external providers.
Too much code added by fast AI agents.

So start with Atoms.

component
relation
capability
state
effect
authority
trust_relation
contract
semantic

Observe them.
Record them as an ArchMap.
Choose a LawPolicy.
Run ArchSig.

This lets us read meaningful architecture boundaries without pretending we can understand the entire codebase at once.

What AI-era architecture analysis needs is not a larger natural-language summary.

It needs the right unit of observation.

Atom is all you need.

The Review Experience This Enables

Future review could look like this.

First, generate an ArchMap delta from a codebase or pull request.

Then run ArchSig using the team's selected LawPolicy.

The reviewer no longer has to read the entire diff as a flat pile of changes.

They can focus on the boundaries that require design judgment.

This change touches:
  - authority boundary
  - generated output mediation
  - state/effect reconciliation
  - async provider job path

Measured pressure:
  - nonzero on permission coverage axis
  - positive path continuation defect on effect axis
  - architectural hole on output promotion path

Review focus:
  - entrypoint-level permission evidence
  - job finalization behavior
  - provider failure handling
  - persistence gate before domain promotion

AI agents can read the same packet.

They can implement with more than a request like:

Just add the feature.

They can receive architectural constraints:

Preserve this Atom.

Do not cross this boundary.

Do not increase pressure on this law axis.

Do not treat these paths as equivalent; their effect order differs.

That matters because AI agents are strongly shaped by context.

If you give them only the codebase, you also give them every existing shortcut.

If you give them the ArchMap and the ArchSig analysis packet, you also give them the architecture's structural pressure and semantic coupling.

Closing

ArchSig is not a tool for grading code.

It is an architecture analyzer for reading a codebase as an Atom map, then using AAT to surface design pressure, semantic coupling, holes, and repair preconditions.

It does not replace dependency graphs, lint, coverage, or security tools.

Those are still important.

But there are questions they do not answer:

Where do authority and generated output intersect?
Where does state/effect order diverge?
Are two paths that create the same artifact really the same architecture operation?
Would this repair candidate transfer complexity to another boundary?

Those are the questions ArchSig is built to make visible.

Start from Atoms.
Record them in ArchMap.
Read them through AAT.
Analyze them with ArchSig.

That is the architecture analysis shape I wanted to introduce.

What Comes Next: SFT and FieldSig

We are also working on the next layer of this research.

AAT makes software architecture locally algebraic.

ArchSig becomes an observation instrument for that local algebra: it takes Atom observations and law-relative structure from a codebase and turns them into an analysis packet.

Beyond that is SFT, Software Field Theory.

SFT is about software evolution.

It does not only ask about the current architecture state.

It asks how review, AI agents, CI, operational feedback, and organizational decisions change the space of possible future software states.

FieldSig is the next measurement surface.

It reads ArchSig analysis packets and workflow evidence in order to make software evolution more computable.

ArchSig is the entrance.

That said, ArchSig is still at v0.3.1.

I do not want it to be judged as a finished product yet.

I want people to try it on many different repositories and tell us what it reads well, what it misses, and where the model feels wrong.

Good reads and bad reads are both valuable for the research.

You can get the ArchSig release bundles here:

AlgebraicArchitectureTheoryV2 Releases