Add a Design notes section: why normalized reduces along the spine
instead of iterating single steps, why substitution computes the
replacement's free variables once (each was a measured order-of-
magnitude win), the Swift literal-coercion gotcha where Term("...")
with a bare literal traps instead of throwing, the by-notation (not
by-dependency) interchange with swift-combinators, and the 0/false
decoding ambiguity.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>