Atlas Theorem: How Far Can You Zoom Out?

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