FiniteConvexSplit.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The finite convex separation used in path-law fusion. A convex family of vectors missing the strict upper orthant has a nonnegative normalized separator. No closedness of the vector family is required.

theorem OAI.CircleDomainRigidity.finite_nonnegative_separator line 18