Definition: The selected route's contract

Before assigning a joint symbol to (eq:target), the route requires:

1. a named common ambient space and characteristic test locus;

2. valid individual relations, orders, and bundles for each factor used in the proposed composition;

3. proved internal composition maps for $K_5,K_8,K_9$;

4. a justified pullback or other operator composition for the complete grouped coefficient;

5. a common symbol identification and a uniform remainder theorem.

The ordinary pullback theorem is used only when its normal-set condition has been checked. If that condition fails, it supplies no automatic reference distribution.