Examples and Boundaries

Canonical examples

The coupon feature extension is the running minimal example. A good extension routes coupon calculation through the declared interface and keeps interaction with the payment core inside an explicit boundary. A bad extension bypasses that boundary by reaching into payment adapters, hidden caches, or implicit rounding order.

• Static witness A hidden direct dependency from the coupon service into payment internals.
• Semantic witness An observation difference caused by rounding or discount application order.

Example template

Each canonical example should expose the same proof-relevant structure. The example is not merely a story about a system; it is a bounded object, a selected operation, a witness universe, a signature reading, and a list of conclusions that do not follow.

Example
  = selected architecture object
  + selected operation or extension
  + invariant family under test
  + witness universe
  + measured signature axes
  + theorem boundary
  + counterexample or non-conclusion

This template is why the coupon example can carry static, semantic, and runtime readings without collapsing them into a single quality judgment.

Coupon case study

The coupon example is the smallest useful running case because it exposes the separation between static structure, semantic behavior, runtime behavior, and measurement boundary.

CheckoutService
  -> CouponService
  -> PaymentPort
  -> PaymentAdapter

bad static edge:
  CouponService -> PaymentAdapter

semantic diagram:
  apply coupon ; round
    ?= round ; apply coupon

runtime exposure:
  retry / cache / callback crosses selected boundary

• Object A selected checkout universe containing coupon code, a declared payment interface, payment core components, and selected relations among them.
• Good extension Coupon computation is added through the declared interface, with a feature view and selected section laws recording how the feature is observed.
• Static obstruction A direct dependency from coupon code into payment adapters, caches, or private payment internals violates the selected static split or boundary policy.
• Semantic obstruction Two implementation paths produce different totals, rounding traces, error observations, or discount ordering observations under the selected client context.
• Runtime obstruction A retry, callback, cache invalidation, or protection failure crosses a runtime boundary not represented by the static dependency graph.
• Non-conclusion A static split report does not prove semantic commutativity, runtime protection, product outcome improvement, or complete extraction of the real repository.

Counterexamples

Static repair can satisfy selected static split while a semantic diagram still fails to commute. A repair can reduce a selected static obstruction while transferring risk to runtime or semantic axes. SOLID-style local contracts can hold without implying global decomposability or acyclicity.

StaticFlatWithin X U
  does not imply
SemanticFlatWithin X

selected obstruction decreases
  does not imply
all axes are non-increasing

AAT boundary

AAT is a local algebra for software architecture. It does not claim complete extraction from real codebases, automatic runtime or semantic flatness from static split, a single architecture quality score, safety of unmeasured axes, full formalization of every natural-language design principle, or that empirical cost correlation is a Lean theorem.

Coupon reading

The coupon example is intentionally small enough to expose the theorem boundary. A static report can measure whether coupon code bypasses a declared payment interface. A semantic report can measure whether discount and rounding observations commute. A runtime report can measure retry, cache, or callback exposure. These are connected readings, not one measurement.

static direct adapter call
  -> static obstruction witness

different rounding trace
  -> semantic obstruction witness

retry leaks across boundary
  -> runtime obstruction witness

SOLID boundary

SOLID-style contracts are useful local law packages, but they are not a complete architecture theory. A component can satisfy selected substitution tests and interface separation checks while the abstract dependency layer is cyclic. Conversely, a layered graph can be acyclic while selected LSP observations still fail.

• Local success A selected client context or interface contract satisfies its observation law.
• Global failure Layering, decomposition, acyclicity, or boundary preservation fails outside the local contract.
• Cross-layer caution One law family cannot be promoted into another without a theorem boundary.

Lean status

The theorem index records proved SOLID-style counterexamples, static / semantic counterexamples, flatness packages, and coupon-oriented bridge APIs. Their purpose on this page is to fix non-implications, not to claim that every real repository example has been extracted completely.