C-D25-CLOSURE

Full within-caps closure OPEN: the projection is favorable but not certified. The greedy hitting set left a few survivors on the sample (the finite denominator pool does not cut every branch; the rest need a larger pool or the D23 arithmetic cuts), and the multi-modulus master's SAT / decision-diagram cost at full clause count is not yet measured within caps. D25-PARTIAL: the direction is validated, full closure is not proven

In plain language

The math points the right way, but closing the whole search within the limits is still open: some states survive and the cost of all the clauses together is unmeasured.

Exact statement

Full within-caps closure OPEN: the projection is favorable but not certified. The greedy hitting set left a few survivors on the sample (the finite denominator pool does not cut every branch; the rest need a larger pool or the D23 arithmetic cuts), and the multi-modulus master's SAT / decision-diagram cost at full clause count is not yet measured within caps. D25-PARTIAL: the direction is validated, full closure is not proven