Elaboration of einsum #
This module implements arbitrary positive-arity einsum over heterogeneous
tensor shapes. Concrete shapes use the executable checker; symbolic shapes
retain their original Nat expressions while proving repeated-label,
broadcasting, source-occurrence, and output-shape invariants.
Elaborate positive-arity einsum syntax to a specialized output with certificates relating it to the general executor. Empty concrete output uses that executor directly. Concrete checks give source diagnostics; symbolic certificates preserve dimension expressions in either path.