AAT Part VII

Representations and Effects

Graph, matrix, analytic, and state-transition views are different representations of selected architecture structure. The strength of a representation depends on whether it preserves or reflects zeros and obstructions under stated assumptions.

Canonical source

Chapters 13-14 in the AAT text

AAT release snapshot

Updated: 2026-05-15
Docs source commit: e4a27d9
Lean status: `lake build` passed for this snapshot; see local status notes and Status page.

Boundary note

Analytic values alone do not prove structural flatness. The reflecting direction needs coverage, witness completeness, and semantic contract coverage assumptions.

Graph and matrix

On a finite unweighted universe, acyclicity, absence of closed walks, and nilpotence of the adjacency matrix can express the same static structure. Finite propagation is not baked into that structural theorem; it depends on a walk universe and a propagation model.

Finite unweighted bridge

acyclic
  <-> no closed walk
  <-> nilpotent adjacency matrix

Graph theorem schema

The graph and matrix bridge is a representation theorem for a finite unweighted static universe. It connects several views of the same structural condition without redefining `Decomposable` and without importing runtime propagation into the static theorem.

Finite static bridge

finite measured static universe
  + coverage assumptions
  ->
  Acyclic
    <-> no nonempty closed walk
    <-> adjacency nilpotence

Cost, latency, propagation, and operational risk require separate observation models or analytic representations. They are not consequences of this static bridge alone.

Boundary diagram

Decomposable = StrictLayered
  separate from
acyclicity
  <-> closed-walk absence
  <-> adjacency nilpotence
  -> spectral radius zero under finite matrix assumptions

runtime propagation
  requires runtime graph / propagation model
  and is not built into Decomposable

Claim	Current Lean status	Boundary	Non-conclusion	Source
Finite graph / matrix bridge	`proved`	Finite unweighted static universe with coverage assumptions.	Not the definition of `Decomposable` and not a runtime theorem.	Lean theorem index, matrix bridge entries.
Spectral bridge	`proved` for finite complex adjacency matrices	mathlib-backed finite matrix representation.	Does not turn cost, risk, or latency into theorem-level signature axes.	Lean theorem index, spectral radius entries.
Runtime propagation bridge	`defined only` / `proved` for selected 0/1 runtime graph zero bridges	Separate runtime universe and propagation model.	Does not follow from static acyclicity alone.	Lean theorem index and proof obligations.

Analytic representation

`AnalyticRepresentation` maps a structural architecture object into an analytic domain. The representation can be zero-preserving, zero-reflecting, obstruction-preserving, or obstruction-reflecting. These are different strengths, and the reflecting directions are the ones that need stronger evidence.

ZeroPreserving Structural zero implies analytic zero.
ZeroReflecting Analytic zero plus assumptions implies structural zero.
ObstructionReflecting An analytic obstruction can be read back as structural only with explicit assumptions.

Representation pattern

A representation theorem has two directions that must not be conflated. Preserving sends a structural zero or witness into the representation. Reflecting reads a represented zero or obstruction back into the structural world, and therefore needs stronger assumptions.

Preserve versus reflect

structural zero
  -[preserving]->
analytic zero

analytic zero
  + coverage
  + witness completeness
  + semantic contract coverage
  -[reflecting]->
structural zero

This pattern also explains why dashboards and numerical summaries are useful but insufficient: an aggregate can guide attention without by itself proving structural flatness.

State transitions and effects

The state-transition layer treats commands, events, retries, compensations, snapshots, CRUD overwrites, and migrations as generators, with laws expressed as relations. Event Sourcing, Saga, CRUD, retry safety, snapshot consistency, and migration naturality are projections of this algebra.

The effect boundary captures obstruction that a dependency graph alone may miss: cross-boundary effects, implicit authority, missing handlers, and non-commuting effect pairs.

Example relations

f ; f = f
compensate ; action ~= id
decode ; encode ~= id

Circuit Breaker Runtime protection law: selected failures should not propagate beyond the protected boundary while the breaker is open.
Replicated Log Distributed ordering law: replicas converge only under the selected quorum, ordering, and failure-model assumptions.
CRUD Overwrite law: update and delete behavior must be read against the selected state and observation relation, not against event replay by default.

Valuation boundary

`ObstructionValuation` maps selected witnesses to numeric or ordered values. Aggregates can be useful for dashboards, but an aggregate zero reflects witness-level zero only when the value domain and aggregation are zero-reflecting under the selected assumptions.

Zero reflection guard

witnesses -> values -> aggregate

aggregate = 0
  + zero-reflecting valuation
  + complete selected witness coverage
  -> selected witnesses are zero

This is the same boundary discipline as matrix and analytic representations: preserving zero is weaker than reflecting zero, and reflecting an obstruction requires coverage and semantic contract assumptions.

Effect examples

A dependency graph may show that checkout depends only on a payment interface, while the effect layer reveals a hidden authority boundary: a retry command is not idempotent, a compensation does not undo the action, a snapshot omits a required event, or a migration fails to commute with the old projection.

Replay law Projection after appending events agrees with replaying the prior projection through those events.
Compensation law A compensation sequence is observationally equivalent to the relevant identity behavior.
Migration naturality Old and new projections commute with the migration relation under stated assumptions.

Lean status

Matrix bridges, finite-universe bridges, analytic representation strength APIs, and state-transition / effect boundary laws are indexed separately. Cost interpretation, runtime completeness, and empirical outcome claims remain outside the structural theorem package.

Acyclicity, closed-walk absence, and adjacency nilpotence are connected for finite unweighted structure. They are not the definition of `Decomposable`, and they do not by themselves settle finite propagation or runtime semantics.