ch:sort-polymorphism: bounded sort constraints

Problem and invariant. Enumerate assignments of sort variables to Type, Prop, and SProp, retaining exactly those that satisfy every equation and declared elimination edge.

Representation and construction. Store the ground elimination table explicitly. Enumerate the finite Cartesian power of ground sorts, then filter it by equality and edge membership. Keep the empty-solution case distinct from a unique or multiple-solution result.

Observable result and mutation. Require two accepted lines, one rejected-elimination line, and the summary shown in Appendix E. Making the table predicate always true still checks but changes the negative line to accepted.

Acceptance and boundary. Match the accepted source record in Appendix E. Restore after the failing mutation, and rerun all four commands. This is a finite solver, not a proof of monomorphization, equiconsistency, or principal inference.