Commit 2025-07-11 15:12 c9ce0e86

refactor(Order/Concept): rename intentClosure → lowerPolar (#26976) The former name was being misused; the intent closure of a set s is actually lowerPolar r (upperPolar r s). The name "polar" can be found in the reference. Although the two types of polars don't have separate names, we choose lower and upper in analogy to lowerBounds and upperBounds; in fact, lowerPolar (· ≤ ·) s is def-eq to lowerBounds s, and likewise for upperPolar. While we're at it, we also get rid of the Concept.toProd projection, in favor of giving more informative names to its fields. This PR contains no mathematics, it's just renaming.