Foundations

Central proposition

AAT formalizes software architecture as a local algebra of objects, operations, invariant families, obstruction witnesses, signatures, and theorem boundaries. The review question is not "is this design good?" but "which invariant is being required, under which observation boundary, and which witness or theorem package supports the claim?"

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

Architecture object

An `ArchitectureObject` is a bounded mathematical object cut out from code, specifications, review evidence, or operational observations. `ArchitectureCore` is a structured, evidence-aware presentation of that object. It can include static and runtime graphs, boundary policy, abstraction policy, semantic diagrams, decidability assumptions, and a selected measurement universe.

• ArchitectureCarrier Components plus static and runtime dependency relations.
• ArchitecturePolicy Boundary and abstraction policies used to read lawfulness.
• ArchitectureObservationContext Observation model, semantic diagram universe, and selected measurement universe.

Definition spine

The foundational record is deliberately small. AAT does not begin with every fact about a repository; it begins with the selected carrier, the policies used to read that carrier, and the observation context that states what evidence is in scope.

ArchitectureCarrier
  = components
  + static dependency relation
  + runtime dependency relation

ArchitecturePolicy
  = boundary policy
  + abstraction policy

ArchitectureObservationContext
  = observation model
  + semantic diagram universe
  + selected measurement universe

ArchitectureObject
  = ArchitectureCarrier
  + ArchitecturePolicy
  + ArchitectureObservationContext

This schema is the first theorem-boundary guard. A claim about the object is never stronger than the carrier, policy, and observation context that presented it.

Foundational claims

The first layer of the theory establishes a disciplined replacement for the phrase "the architecture." The object of reasoning is not an entire repository, but a selected presentation with explicit evidence and scope.

• Definition An `ArchitectureObject` is a carrier plus policy plus observation context.
• Interpretation An `ArchitectureCore` presents the object through evidence, but presentation is not assumed complete or injective.
• Boundary A `ComponentUniverse` is a selected measurement universe; outside it, zero and absence are not inferred.
• Non-conclusion No theorem here states that a real-code extractor has found every relevant component, relation, runtime effect, or semantic diagram.

selected carrier
  + selected policy
  + selected observation context
  + coverage / exactness boundary
  -> bounded ArchitectureObject claim

Universe boundary

`ComponentUniverse` records selected components, selected relations, coverage boundary, and exactness boundary. Outside that universe, AAT does not infer zero, absence, flatness, split, or lawfulness.

`ComponentCategory` is thin: it remembers whether a reachability morphism exists and intentionally forgets path count and walk length. Quantitative data belongs to `Walk`, `Path`, adjacency matrix, finite metrics, or future free-category constructions.

Formal reading

The foundational move is to replace an unbounded repository question with a typed object plus explicit evidence scope. A static dependency graph, a runtime graph, an abstraction policy, and a semantic observation model may all present the same bounded `ArchitectureObject`, but none of those presentations is automatically complete.

This is why `ArchitectureCore` is read as an evidence-aware carrier rather than as the architecture itself. The map from a core presentation to the object it presents is not assumed to be injective or complete: two presentations can be equivalent under the selected observation, and either presentation can omit relations outside its coverage boundary.

ArchitectureObject claim
  = selected carrier
  + selected policy
  + selected observation context
  + coverage and exactness boundary

Example boundary

A repository slice containing a coupon service, a payment interface, and a payment adapter can be a valid component universe for a static split theorem. That same slice is not, by itself, evidence about runtime retries, cache invalidation, rounding order, or operational incidents. Those require their own observation contexts.

• Measured zero No selected violating relation was found inside the chosen universe and exactness boundary.
• Unmeasured outside No claim is made about components, relations, effects, or observations outside that boundary.
• Presentation equivalence Different carriers can present the same object only relative to the selected observation model.

Lean status

The Lean side already fixes the static graph, reachability, layering, decomposability, thin-category, finite-universe, and bridge vocabulary used by this page. The important boundary is that these declarations do not certify complete extraction from a real repository.