Local Law Packages

Projection and observation

A projection maps concrete structure to abstract structure. An observation maps concrete structure or operation results to selected observations. They are related by the claim that equal abstractions should have equivalent observations in the selected context.

F : Concrete -> Abstract
Obs : Concrete -> Observation

F(x) = F(y) -> Obs(x) ~= Obs(y)

ker(F) <= ker(Obs)

Projection theorem schema

Projection claims become architecture claims only after the strength of the projection is stated. Soundness, completeness, exactness, and representative stability support different conclusions.

ProjectionSound F
  -> concrete dependency evidence is represented abstractly

ProjectionComplete F
  -> abstract dependency evidence has concrete representatives

ProjectionExact F + RepresentativeStable F
  -> quotient-style or replacement-style readings may be stated

For LSP-style claims, the same discipline appears as selected client contexts and selected observations. Equal abstractions must preserve observations only for the contexts and equivalence relation named in the theorem boundary.

LSP and DIP

LSP-style substitutability is read through a selected client context universe. DIP and Clean Architecture style abstraction soundness are read as concrete dependencies mapping soundly to abstract dependencies, with stronger claims requiring completeness, exactness, and representative stability.

• ProjectionSound Concrete dependency evidence is represented in the abstract graph.
• ProjectionComplete Abstract dependencies have concrete representatives under stated assumptions.
• RepresentativeStable Chosen representatives remain stable for the claim being made.

Three-layer flatness

AAT separates static flatness, runtime flatness, and semantic flatness. Static flatness handles dependency direction, boundary, and abstraction violations. Runtime flatness handles protection, propagation, and exposure. Semantic flatness handles observation-level commutativity, diagram filling, and contract preservation.

ArchitectureFlatWithin
  = StaticFlatWithin
  + RuntimeFlatWithin
  + SemanticFlatWithin
  + no unmeasured required axis
  + coverage / exactness boundary

Assumption strength

Projection claims come in different strengths. `ProjectionSound` says concrete dependency evidence is represented abstractly. `ProjectionComplete` says abstract dependencies have concrete representatives. `ProjectionExact` and `RepresentativeStable` add stronger assumptions needed for quotient-style or replacement-style readings.

The page therefore separates local abstraction soundness from global layering. A DIP-style statement may be true because concrete calls depend on declared interfaces, while the interface layer itself still contains a cycle or a semantic mismatch outside the local contract.

ProjectionSound
  does not imply
ProjectionComplete
  does not imply
ProjectionExact + RepresentativeStable

Non-implication map

Local law packages are useful because they make a precise claim small enough to prove. They are dangerous only when their conclusion is promoted into a different invariant family without a bridge theorem.

LSP-compatible selected contexts
  does not imply
global decomposability

DIP-compatible dependency direction
  does not imply
abstract layer acyclicity

StaticFlatWithin X U
  does not imply
RuntimeFlatWithin X or SemanticFlatWithin X

AAT keeps these failures as theory content. The point is not to weaken design principles, but to place each principle in the invariant family where it can be stated and checked correctly.

Contract example

In a coupon extension, replacing a discount implementation by another implementation can be LSP-sound for selected checkout clients if the observed totals, rounding trace, and error behavior remain equivalent. That does not prove that the coupon service respects a global dependency ranking, nor that background jobs, caches, or payment callbacks preserve the same observations.

• Client context universe The selected callers and call shapes for which substitutability is checked.
• Observation equivalence The chosen equality or tolerance on visible behavior.
• Missing layer claim Runtime and semantic flatness require separate evidence packages.

Lean status

Projection / DIP bridges and finite observation / LSP violation-count bridges are tracked as Lean APIs and theorem packages. Three-layer flatness is a boundary discipline: static flatness, runtime flatness, and semantic flatness remain separate claims unless a theorem boundary explicitly connects them.