Laws and Witnesses

Invariant families

An `Invariant` is a property an architecture object or operation is expected to preserve. Design principles induce families of operations that preserve, reflect, improve, localize, translate, or transfer invariants; the principle itself is not treated as one universal mathematical operation.

• Local contract layer SRP, OCP, LSP, ISP, and DIP organize contracts, abstraction, substitutability, and interface separation.
• Global structure layer Layered and Clean Architecture handle ranking, dependency direction, acyclicity, decomposition, and boundary preservation.
• State and runtime layers Event Sourcing, Saga, CRUD, Circuit Breaker, and Replicated Log carry replay, compensation, overwrite, protection, ordering, and convergence laws.

Obstruction witnesses

An `ObstructionWitness` structurally explains why a desired law does not hold. A forbidden static edge, hidden interaction, boundary policy violation, projection failure, LSP mismatch, non-commuting semantic diagram, runtime exposure, lifting failure, or residual coverage gap can all be witnesses when they live in the selected universe.

violatingWitnesses bad xs
  = xs filtered by bad

violationCount bad xs = 0
  <-> every measured witness is not bad

Zero-curvature reading

The central theorem package connects semantic lawfulness, selected required witness absence, and selected required signature axes being zero. The connection is nontrivial: it requires witness completeness, axis exactness, coverage completeness, and observation exactness.

finite law universe
  + theorem boundary B
  + complete witness coverage
  + required axis exactness
  ->
  ArchitectureLawfulWithin X B
    <-> no selected required obstruction witness
    <-> required signature axes are zero

Theorem pattern

The law-to-witness connection is not definitional. A finite witness report becomes a semantic lawfulness claim only after the theorem boundary supplies the missing exactness and coverage hypotheses.

• Semantic predicate `SemanticLawful X L` says the selected law universe is satisfied under the selected observation.
• Witness predicate `NoRequiredWitness X W` says no required bad witness appears in the selected finite witness family.
• Signature predicate `RequiredSignatureAxesZero X S` says the required measured axes are zero, not that every possible axis is safe.

WitnessComplete(L, W)
  + AxisExact(W, S)
  + CoverageComplete(boundary)
  + ObservationExact(context)
  ->
  SemanticLawful X L
    <-> NoRequiredWitness X W
    <-> RequiredSignatureAxesZero X S

Main theorem schema

The zero-curvature theorem is the central lawfulness bridge. It is stated as a schema because the law universe, witness family, signature axes, and observation model vary across structural, projection, semantic, runtime, and extension readings.

Given:
  finite law universe L
  selected witness family W
  selected signature axes S
  theorem boundary B

Assuming:
  WitnessComplete(L, W)
  AxisExact(W, S)
  CoverageComplete(B)
  ObservationExact(B)

Then, within B:
  SemanticLawful X L
    <-> NoRequiredWitness X W
    <-> RequiredSignatureAxesZero X S

This theorem shape is also the guardrail for readability. A dashboard zero, a passing local contract, or a missing witness list becomes a lawfulness statement only when the stated completeness and exactness assumptions are available.

Law universe

A `LawUniverse` collects required laws, optional laws, derived laws, witness families, and the observation boundary used to read them. AAT does not identify lawfulness with witness absence at the definition level; the equivalence is a theorem package that needs completeness and exactness assumptions.

ArchitectureLawfulWithin X B
  := SemanticLawful X B.lawUniverse
     under B.coverage / B.exactness / B.observation

This distinction prevents a finite report from silently turning into a global claim. The report may certify the absence of selected required witnesses; the theorem boundary states when that absence is enough to read semantic lawfulness inside the chosen universe.

Examples

A local LSP contract can be lawful for selected client contexts while the overall dependency graph remains cyclic. A layered ranking can be lawful for static dependencies while a runtime callback still crosses a protected boundary. A Saga law can hold for a compensation relation without proving anything about distributed convergence.

• Local contract witness An observation mismatch for a selected client context.
• Global structure witness A forbidden dependency direction, cycle, or boundary crossing in the selected static universe.
• Runtime witness A propagation, exposure, retry, or protection failure in a separate runtime observation layer.

Lean status

The generic witness-count kernel and required law / axis exactness bridge are part of the current proved static core. The broader design-principle classification remains a boundary discipline: SOLID, Layered, Clean Architecture, Event Sourcing, Saga, CRUD, Circuit Breaker, and Replicated Log are organized as different invariant families, not one Lean theorem scheme.