Normalization is the guarantee that every Term reaches a ValueReduction always terminates.

Normalization guarantees that the evaluation of any well-typed Term halts — it does not loop or diverge but arrives at an irreducible Value. Together with Soundness (evaluation does not go wrong) and Confluence (evaluation does not branch), Normalization ensures that evaluation is total: every Term has exactly one Value.

The semantics stratum establishes Normalization through strong normalization — not just that some reduction path terminates, but that every reduction path terminates. No matter how you choose to reduce, you reach the same Value in finitely many steps.

Normalization is what makes Observation possible: the observation stratum witnesses Values, and witnessing requires that Terms can actually be evaluated to Values. Without Normalization, some Terms would never settle, and Observation would have gaps — unwitnessable positions in the syntax.