Item 62: The inertness dichotomy in Lean

The dichotomy is three lines and uses only convexity: if every stage-consistent world satisfies a finite system of half-space rows, then the convex hull of those worlds lies inside the region the rows cut, so the intersection is the hull. Stated over the repository's own objects it says ConstraintSchedule's hadm implies regionPred contains DeductiveRegion's hull, hence that the enforced region equals the deductive one.

It is currently a paper derivation checked on finite instances, and it is the premise item 61 exists to answer.

Deliverable shape: lean-proved — one theorem in a contribution namespace, with an inhabitation witness. Acceptance check: the lean job, and #print axioms clean. Context: projects/normativity/legitimacy/rounds/2026-08-25-end-to-end-vertical-slice/VERTICAL_SLICE.md §11 (T2); lean/Workspace/Normativity/Contrib/{ConstraintSchedule,DeductiveRegion}.lean. Consumed by: item 61, which needs the dichotomy to be a statement of record before its own negative half means anything.