ch:coercive-subtyping: coherent path comparison

Problem and invariant. Enumerate simple paths in a finite coercion graph and compare the symbolic cast programs of every parallel pair. A path is accepted only when its endpoints and complete edge sequence are preserved by normalization.

Representation and construction. Store types as vertices, primitive casts as labeled edges, and cast programs as lists of labels after identity removal and composition flattening. Use a visited set for path enumeration. Report unique path, coherent parallel paths, and an explicit incoherent pair as distinct results.

Observable result and mutation. Require unique, coherent, the rejected-parallel-casts line, and the summary shown in Appendix E. Comparing programs only by length still checks but accepts the bad diamond.

Acceptance and boundary. Match the accepted source record in Appendix E. Restore and rerun after mutation. Finite enumeration proves neither path coherence nor completion for a general dependent coercion calculus.