Theorem: Direct excess-route audit

For the selected route of Definition def:route:

1. the six regular base constraints are available;

2. the full selected conormal matching is not clean;

3. the rank-two transverse object is a tangent-defect bundle;

4. the covector-sum projection has one-dimensional, not two-dimensional, local fibers;

5. the stated projected image is not a Lagrangian relation on the named ambient space.

Therefore the direct application of a clean excess-two composition formula to this fiber product is not justified. The selected route stops at F2.

Proof. Proposition prop:regular gives (i). Theorem thm:nonclean gives (ii). Proposition prop:defect gives (iii). Theorem thm:projection gives (iv) and (v). The required clean and Lagrangian hypotheses of the direct route are consequently absent. Lemma lem:persistence shows that the proposed frequency reduction does not remove the failed tangent equality.