Algebraic Architecture Theory.

Abstract

Algebraic Architecture Theory formalizes software architecture as a bounded mathematical object equipped with operations, invariant families, obstruction witnesses, signature axes, and theorem boundaries. Its basic claim is that architectural quality should be read through preserved invariants and explicit witnesses of failure, not through slogans, framework names, or a single scalar score.

The theory is local by design. Every claim is relative to a selected universe, observation context, coverage boundary, and exactness assumption. This makes AAT useful for precise design review: it can say what is preserved, what is broken, what was measured, what was not measured, and which theorem package licenses the conclusion.

Main contributions

• Architecture as bounded algebra AAT treats architecture objects and operations as typed, evidence-bounded mathematical data rather than as informal descriptions of whole codebases.
• Obstruction-first quality Quality failure is represented by selected obstruction witnesses: forbidden edges, boundary violations, projection failures, semantic non-commutativity, runtime exposure, lifting failure, and residual coverage gaps.
• Multi-axis signature Architecture Signature records measured coordinates and measurement status per axis, keeping unmeasured, out-of-scope, private, and zero evidence distinct.
• Theorem-boundary discipline Every theorem candidate records assumptions, coverage, exactness, conclusion, and non-conclusions so static, runtime, semantic, tooling, and empirical readings are not collapsed.

Publication purpose

This website is the canonical public reading surface for AAT: a web-native theory text that sits between outreach posts and a future conventional paper. Blog platforms are useful for motivation, but AAT needs a stable place for definitions, assumptions, theorem boundaries, examples, counterexamples, Lean status, and non-conclusions to remain together.

• Not a blog summary The pages preserve formal distinctions instead of compressing them into general software advice.
• Not a product landing page The primary object is the theory: its vocabulary, theorem shape, examples, and boundaries.
• Preprint-style surface The site makes AAT readable before a slower arXiv-style paper is prepared, while keeping claim discipline explicit.

Reading order

The repository keeps AAT as one first-class mathematical text. The website splits that text into chapter clusters so readers can keep their current position and move through the theory in a stable order.

• Foundations Central proposition, ArchitectureObject, ArchitectureCore, ComponentUniverse.
• Laws and Witnesses Invariant families, LawUniverse, ObstructionWitness, zero-curvature reading.
• Signature and Theorem Boundary ArchitectureSignature, MeasurementStatus, theorem boundary, non-conclusions.
• Local Law Packages Projection, observation, LSP, DIP, and three-layer flatness.
• Calculus and Extensions ArchitectureOperation, operation laws, FeatureExtension, extension obstruction.
• Repair and Dynamics Repair, synthesis, complexity transfer, paths, homotopy, diagram filling.
• Representations and Effects Graph, matrix, analytic representation, state-transition algebra, effect boundary.
• Examples and Boundaries Coupon extension, semantic counterexample, repair transfer, SOLID boundaries.
• Status How to read Lean status, proof obligations, and implemented theorem packages.

Claim discipline

AAT does not identify architecture quality with a slogan, a framework name, or a scalar score. It asks which invariant is required, which universe is being observed, which witness shows a failure, and which theorem boundary permits the conclusion.

software architecture
  = ArchitectureObject
  + ArchitectureOperation
  + InvariantFamily
  + ObstructionWitness
  + ArchitectureSignature
  + theorem boundary / non-conclusions

Canonical sources

The mathematical source of truth is the repository document. Lean theorem status is intentionally separated into the theorem index and proof-obligation ledger so public prose does not turn a theorem candidate into a proved Lean claim.

• Mathematical text `docs/aat/mathematical_theory.md` defines the AAT theory surface.
• Lean status `docs/aat/lean_theorem_index.md` lists implemented definitions and theorems.
• Proof obligations `docs/aat/proof_obligations.md` separates proved, defined only, future proof obligation, and empirical hypothesis.