DEV Community: Hiroyuki Nakahata

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

I Open-Sourced the AAT / SFT Research Repository

Hiroyuki Nakahata — Sun, 24 May 2026 05:13:39 +0000

I open-sourced the AAT / SFT research repository.

Repository:

https://github.com/iroha1203/AlgebraicArchitectureTheoryV2

This repository is for building theory and tools that treat software architecture not only as a blueprint or a list of best practices, but as something that keeps evolving through changes, reviews, CI, operations, and proposals from AI agents.

The larger goal is to make the evolution of software and computers something we can measure, compare, and reason about, instead of only looking back after the fact.

What This Research Is About

The repository is organized around three ideas.

AAT makes architecture locally algebraic.
ArchSig makes architecture observable.
SFT makes software evolution computable.

AAT stands for Algebraic Architecture Theory.

It treats software architecture as a local algebraic structure.

In more practical terms, it asks questions like these:

Did this design change preserve dependency direction?
Did it cross a layer boundary?
Does it still depend on abstractions instead of concrete details?
Did it make failures easier to spread?

ArchSig is a set of tools for extracting architecture signals from real codebases and pull requests.

It is not meant to produce one big "good / bad" score. Instead, it separates different kinds of risk: dependency cycles, boundary violations, abstraction leaks, unmeasured parts of the system, and other signals that should be read separately.

SFT stands for Software Field Theory.

It treats software evolution as a sequence of changes and tries to make that evolution computable.

PRDs, issues, pull requests, reviews, CI, organizations, and AI agents do not only affect the current change. They also shape what kind of change is likely to happen next.

For example, a vague PRD can invite an ad hoc implementation. A codebase with clear boundaries tends to make the next change easier to place cleanly. SFT develops concepts for reasoning about what futures become easier to reach after a change.

Why I Am Building This

AI can generate working code very quickly.

But whether a fast diff makes future changes easier, or instead adds more ad hoc implementation, is a different question.

The question is not only:

Do the tests pass?

I also want to ask:

Did this change preserve the design properties we care about?
If not, what code or dependency shows the problem?
Is the problem a dependency cycle, a boundary violation, or an abstraction leak?
Does this PRD, issue, or pull request make the next change easier to move in a good direction?
Can review and CI stop risky change patterns early?

The motivation behind this repository is to turn those questions into something we can formalize, observe, and eventually support with tools.

What Is In The Repository

The repository currently contains:

Lean formalization for AAT
Research notes for AAT and SFT
Rust implementation of the ArchSig tools
Open proof tasks and a Lean theorem index
A static website for reading AAT, SFT, and ArchSig

On the Lean side, I am building small theorem packages with explicit assumptions.

On the Rust tooling side, I am working toward reports that extract design signals from codebases and pull requests, then make them readable in review and CI.

On the website side, I am preparing public-facing research notes and manuals for AAT, SFT, and ArchSig.

This Is Still Research

This repository is a working research space, not a finished product.

I separate different kinds of claims:

what has been proved mathematically,
what has only been defined so far,
what I want to prove later,
and what should be checked against real development data.

For example, a theorem proved in Lean does not automatically predict the future of a real project.

There is a difference between a tool saying "this dependency was observed," Lean proving "this property follows under these assumptions," and empirical work saying "this trend seems to appear in real development data."

The repository keeps those claims separate.

Where To Start

The README is the best entry point.

https://github.com/iroha1203/AlgebraicArchitectureTheoryV2

If you want to go deeper, I recommend this order:

Research goal
AAT mathematical theory
AAT / SFT interface
Software Field Theory
Lean definitions and theorem index
ArchSig tooling documentation

Website

There is also a website for reading AAT, SFT, and ArchSig as connected research notes.

https://iroha1203.dev

If you want the big picture before reading code or proof details, the website is the easier place to start.

Closing

The short version is:

I want to treat software architecture and software evolution as things we can observe, diagnose, and compute.

I do not want design principles to remain slogans.

I want to ask what properties they preserve, what failures they reveal, and what futures they make easier to reach.

This repository is where I am building the theory, formalization, tools, and public notes for that direction.

Forecast Cone: A Grand Theorem for Computable Software Evolution

Hiroyuki Nakahata — Fri, 22 May 2026 17:50:41 +0000

TL;DR

This article starts from the ForecastCone in Software Field Theory (SFT), then reads modularity, technical debt, review, governance, and learning as parts of one research program.

The goal is simple to state:

Make it possible to see what futures a change opens, close dangerous futures early, and shape the development environment so good futures become easier to reach.

If this theorem-shaped program works, architecture, technical debt, review, governance, and AI coding safety can all be reread around the same object: the ForecastCone.

We are also formalizing this direction in Lean by breaking concepts such as ForecastCone and ConsequenceEnvelope into small records and theorem packages.

For the Bigger AAT / SFT Picture

I introduced the broader AAT / SFT framing here:

The Problem: Fast Code Is Not the Same as Healthy Evolution

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

If the existing code contains many shortcuts, the agent can easily learn those patterns.
If boundaries are vague, the agent will naturally add the next change in the vague place.
A good structure attracts good changes. A bad structure repeatedly makes bad shortcuts look natural.

PRDs, issues, review policies, and CI rules do not only decide "this change."
They shape what the next PR tends to look like, which modules feel natural to touch, which boundaries are easy to miss, and which shortcuts are likely to pass.

In vibe coding, for example, an AI agent can quickly produce a plausible implementation from an underspecified PRD.

A PRD that only says "make coupons usable" may turn into a small if inside the checkout flow.
The first demo works.
But if that change leaves pricing policy, refunds, usage limits, and audit logs as vague boundaries, the next PR will often build on the same shortcut.

The problem is not that AI writes bad code.
The problem is that vague artifacts plus fast generation can open bad future paths very quickly.
A bad field can be amplified by AI into larger technical debt.

Traditional review, CI, and metrics often look at the current diff or at outcomes that already happened.
In the AI era, that is not enough.

The question is no longer only:

Does this PR pass right now?

The deeper question is:

What future does this PRD, this agent, this codebase, and this review rule open next?

SFT needs ForecastCone in order to ask that question.
It gives us an object for making software evolution computable, not as a mere sequence of changes, but as a space of reachable futures.

The Grand Theorem: A Fundamental Theorem of Software Evolution

Modularity
  = ForecastCone descent

Technical debt
  = descent obstruction

Review
  = minimal decision-preserving envelope

Governance
  = desired-cone-preserving obstruction cutting

Learning
  = closed-loop boundary-explicit fixed point

In this article, I will call this theorem-shaped picture the Fundamental Theorem of Software Evolution.

In everyday engineering language, it says something like this:

A good architecture boundary lets teams and AI agents work separately, then combine their changes safely later.

Technical debt is the ability to explain, with a concrete cause, why integration keeps breaking at the same place.

In review, we do not want every diff line or every possible future. We want the dangerous futures that matter for the decision.

Governance should not just add rules that stop development. It should close bad shortcuts and make good implementation paths easier to choose.

Learning means using actual PRs, incidents, and review outcomes to update the next forecast and the next rule.

In more mathematical language:

A good architecture boundary is not merely a static dependency cut. It is a boundary across which future evolution paths can be computed locally and glued into a global future under compatibility conditions.

Technical debt is an obstruction that appears when that gluing fails.

Review is not the act of seeing the entire ForecastCone. It is the act of seeing an envelope that preserves the distinctions needed for a decision.

Governance is a support transformation that removes bad futures while preserving desired futures.

Learning is a closed-loop update that moves a field estimate toward a boundary-explicit fixed point using PRs, incidents, reviews, and operational outcomes.

If such a theorem can be proved, the way we reason about software evolution changes.

Whether an architecture is good, where technical debt sits, what a reviewer needs to see, which governance rule is effective, and how the field model should be updated next can be studied over the same computational object.

That object is the ForecastCone.

ForecastCone: The Range of Reachable Futures

SFT reads the development environment as a field.

codebase
  + artifacts
  + practices
  + agents
  + governance
  + feedback
  -> reachable software futures

The range of futures reachable under that field is what SFT calls a ForecastCone.

A ForecastCone is not a prophecy.

SFT does not say:

This PRD will definitely produce this PR.

Instead, it asks:

Under this field model, operation support, policy, observation boundary, and horizon, which future paths are reachable?

Imagine an e-commerce service receives a PRD: "Add limited-time coupons."

That PRD does not open just one future.

One future adds a small branch to the checkout flow.
One future adds a discount policy to the pricing service.
One future introduces an independent coupon domain.
One future expands into campaign rules and audit logs.
One future adds a database column for now and leaves cleanup for later.

All of these are, in some sense, "coupon support."
But they open very different next futures.

The ForecastCone is the object that lets us look at that difference.
The same PRD can make different futures easy or hard to reach depending on the current codebase, module boundaries, past workarounds, review rules, CI, and AI agent behavior.

Modularity = ForecastCone Descent

Modularity
  = ForecastCone descent

The intuition is:

The global future of a software system can be computed by gluing compatible local futures.

Traditional modularity is often described in terms of APIs, dependency direction, and responsibility separation.
SOLID, Layered Architecture, Clean Architecture, and Design Patterns have often been used as ways to help humans understand responsibilities, localize change, and control dependencies.

SFT extends that line of thought by asking:

Do the futures glue?

If a boundary is truly modular, we should be able to reason about the future of Pricing and the future of Checkout locally, then glue them into one checkout future under the right compatibility conditions.

The boundary is not just a line. It is a place where future evolution should cross without breaking.

In practice, following SOLID and Layered Architecture already gets us a lot of the way toward this kind of modularity.

Technical Debt = Descent Obstruction

Technical debt
  = descent obstruction

The intuition is that technical debt can be read as a failure of futures to glue.

local tests pass.
local reviews pass.
the AI proposal looks reasonable.
then integration breaks.

SFT does not want to stop at "the design is bad."
It wants to record the failure as an obstruction.

DescentFailure:
  missing interface invariant

Witness:
  Pricing returns a discounted total,
  but Checkout treats it as a tax-included final charge.

Now technical debt is no longer just a feeling.

Each team-local change looks reasonable, but the whole system cannot combine them into a valid global future.
The reason is that the boundary rule that should have been preserved was never defined.

That is the role of the Descent Obstruction Theorem.

Review = Minimal Decision-Preserving Envelope

Review
  = minimal decision-preserving envelope

A ForecastCone can be large.
A reviewer cannot look at every future path.
But a diff alone is often too small.

Suppose an AI agent produces a PR like this:

if coupon_code.present?
  total = total - discount
end

The diff is small.
But the reviewer does not only care about these three lines.

Will this add an unobserved branch to the refund path?
Will usage limits collide with retry behavior?
Is the tax boundary between Pricing and Checkout still undefined?

What we need is not the whole ForecastCone, but the part needed for a review decision.
SFT calls this a ConsequenceEnvelope.

The goal for review tooling is not to show everything.
It is to show the future-relevant differences needed for the decision, no more and no less.

Governance = Desired-Cone-Preserving Obstruction Cutting

Governance
  = desired-cone-preserving obstruction cutting

When a risky future appears, the simplest response is to add another rule.

Anything coupon-related must be reviewed by a senior engineer.

That is a guardrail.
But it is often heavy, and it may not say what future it is actually closing.

The kind of governance SFT wants is more specific: close bad futures while preserving desired ones.

Introduce separate DiscountedTotal and FinalCharge types across the Pricing / Checkout boundary.
Make coupon usage updates idempotent.
Require coupon invariant checks when touching the refund path.
Guide AI agents away from ad hoc discount branches under checkout and toward policy objects.

We want to close the future where discount logic spreads across checkout.
We still want to preserve the future where coupon policy can evolve independently.

That difference is what the Governance Synthesis Theorem is about.
It is not just about adding guardrails. It is about shaping the field.

Learning = Closed-Loop Boundary-Explicit Fixed Point

Learning
  = closed-loop boundary-explicit fixed point

SFT is not a theory where we compute one ForecastCone and stop.

Predicted future paths are compared with actual PRs, incidents, review comments, CI failures, and runtime observations.
When the forecast is wrong, that is not just a failure.
It becomes evidence for updating the model.

Was the field estimate too coarse?
Was the observation boundary too narrow?
Did the policy model fail to represent actual review behavior?
Should the unknown remainder have been made explicit?

As this closed loop progresses, an SFT workbench becomes more than an analyzer.
It becomes a system for continuously calibrating the field model of software evolution.

Attractor Engineering and ArchSig

This grand theorem becomes practical only when it connects to AAT and ArchSig.

AAT gives us a local theory for reading what a change preserves and what it breaks.
ArchSig gives us a signature layer for observing preservation and breakage from repositories, PRs, reviews, CI, and incidents.
SFT uses those observations to compute reachable futures and connect them to governance and learning.

AAT
  -> local laws / invariants / obstruction witnesses

ArchSig
  -> observed signatures / measured axes / evidence boundaries

SFT
  -> ForecastCone / ConsequenceEnvelope / governance update

Attractor Engineering fits here as well.

A good architecture attracts good changes.
A bad architecture repeatedly makes the same shortcut look natural.

In SFT language, this means the shape of reachable futures changes.
Governance interventions close bad future paths, type boundaries make good local evolution more natural, and review rules make risky paths observable.

Attractor Engineering is the practice of shaping the ForecastCone.
ArchSig is a tool for observing that change.
SFT connects those observations back to the theorem family.

A Sketch of a Future Development Workflow

SFT is not trying to build a system that decides the future instead of developers.
It is trying to make a development environment where developers, AI agents, reviews, and CI can see the future opened by a change on the same map.

An ambiguous PRD arrives.
An AI agent quickly proposes an implementation.
At the same time, a workbench sketches the futures that change seems to open and shows only the differences needed for review.

PRD
  -> implementation candidates
  -> reachable future range
  -> review-relevant differences
  -> review / CI / governance
  -> observed outcome
  -> next forecast update

Before reading every line of the diff, the reviewer sees which futures look risky.
CI checks not only whether tests pass, but whether a risk we wanted to close is still present.
The AI agent prioritizes implementation candidates that open better futures instead of copying the nearest shortcut.

Actual PRs, incidents, and review comments then become evidence for the next forecast.

That is the development workflow SFT is aiming toward.

Impact on Computer Science and Software Engineering

Lehman raised a core question of software evolution: long-lived software keeps changing as it adapts to its environment, and that change tends to increase complexity.

SFT revisits that question in the age of AI-assisted development.

Software engineering has long developed design and architecture theory around human cognition.

That makes sense.
Software is complex, and if humans cannot read it, they cannot maintain it.
So we developed ideas such as separation of concerns, information hiding, cohesion, coupling, layering, Clean Architecture, and bounded contexts to make complexity manageable for people.

That axis remains important.

But once AI coding agents enter the loop, the bottleneck shifts.
When code can be produced faster, the question is no longer only:

Can humans understand the current structure?

The next question is:

What futures does this structure make reachable?

A good design is not only one that makes the current code easier to read.
It is also one that makes good futures easier to reach and bad futures harder to reach.

From this point of view, architecture expands from human comprehensibility to future reachability.

Can this boundary glue future paths locally?
Which direction does this PR make the next change more likely to take?
Does this metric preserve distinctions that matter for future evolution?
Does this review rule close bad futures while preserving good ones?
Which gluing failure does this technical debt represent?

These questions already exist in practice.
They are just scattered across experience, intuition, review comments, incident memory, and organizational culture.

SFT tries to move them toward computable theory.

If this direction works, software engineering moves from:

techniques for making complexity understandable to humans

toward:

a science for observing, computing, and governing software evolution

The central concepts begin to look different:

architecture
  -> shape of reachable futures

modularity
  -> descent of future paths

technical debt
  -> obstruction to future gluing

review
  -> minimal consequence envelope

metrics
  -> cone-conservative observations

governance
  -> support transformation

refactoring
  -> evolutionary invariance

AI coordination
  -> agentic confluence

lifecycle
  -> bifurcation of repair feasibility

Lean Formalization

We are also formalizing this research program in Lean.

The point is to keep SFT vocabulary from remaining only a metaphor.

Terms such as field, ForecastCone, ConsequenceEnvelope, and governance update are being broken into small objects that can become records, types, and theorem packages.
The big research picture gradually becomes something we can touch formally.

Current formalization work includes:

SoftwareFieldEstimate
OperationSupport / StepRelation
ForecastCone / ClockedForecastCone
ConsequenceEnvelope
FieldUpdate

For example, ForecastCone is treated as a supported path within a finite horizon.
ClockedForecastCone introduces a shared clock and idle / stutter steps for descent.
ConsequenceEnvelope treats review output as a projection from a cone family.

The final grand theorem is also being assembled from components: descent, obstruction, review, governance, calibration, and agentic confluence.
Under those explicit components, the Lean-side assembly has the shape:

computably governed
  or
typed boundary failure

This formalization makes SFT a research program where we can track what is a theorem, what belongs to modeling, and what remains on the tooling or empirical side.

Closing

ForecastCone is not a tool for predicting the future.

It is a way to make reachable software futures computable under explicit modeling boundaries, operation support, policies, observation boundaries, and horizons.

SFT's bet is that we can rebuild central software engineering concepts from there.

Architecture is not only the shape of present code.
It is the shape of reachable futures.

Architecture is not only the shape of the code we have now.

It is also the shape of the futures that codebase makes reachable.