Function has_unique_aggregate_output 

fn has_unique_aggregate_output(expr: &Expr) -> bool

Whether a partitioning aggregate proves the operand emits at most one series per combination of its output labels; ranking narrows its input, so it inherits the proof. Uniqueness per match signature additionally requires every output label to be a matching label, which the caller checks.