Einsum contraction-invariance analysis

This module recognizes operands whose physical reads are constant across all contracted coordinates, including singleton-broadcast axes.

def TorchLean.Tensor.Internal.Elab.Impl.operandIsContractionInvariant (axes : List Check.EinsumAxis) (dimensions : List Lean.Expr) (outputAxes : List Check.EinsumAxis) : Lean.MetaM Bool

Report whether an operand is constant across every contracted coordinate.

Output axes never vary inside the contraction. A contracted physical axis is also constant when its dimension reduces to one, because broadcasting always reads its sole entry.