Item 4: Higher-dimensional sharpness for the movement cap

Everything verified numerically in the joint layer is the one-coordinate fixture. The vertex formulation is stated for general finite regions but only the scalar case is exercised, and no claim is made that the corrected retention predicate is the weakest sound one.

Deliverable shape: witness-checked for the multi-coordinate instances; lean-proved for a sharpness result. Acceptance check: The witness checker accepts each instance; or the Lean gate is green.

Context: projects/normativity/consolidation-aug9/THEORY_10_JOINT_COMPOSITION.md §3, §6. A solution ships: the multi-coordinate instances with exact witnesses, and either a sharpness proof or a witness that the predicate is not weakest.