Automatic einsum contraction planning

The planner chooses a nesting order for contracted logical axes from the physical row-major strides of every operand. High-stride axes remain outside low-stride axes, improving locality without specializing to a tensor rank or named operation.

Planning is enabled only when the scalar type has lawful commutative addition. The returned permutation proof is consumed by the lowering correctness theorem; ordered scalar types retain the source contraction order.

def TorchLean.Tensor.Internal.Elab.Impl.contractionAxisOrder (inputAxes : List (List Check.EinsumAxis)) (inputShapes : List (List ℕ)) (contractedAxes : List Check.EinsumAxis) : List Check.EinsumAxis

Order contracted axes by descending aggregate physical row-major stride.

The function is pure cost analysis: it does not grant permission to use the order. planContraction? separately requires lawful commutative addition and constructs the permutation certificate.

def TorchLean.Tensor.Internal.Elab.Impl.planContraction? (checked scalarType : Lean.Expr) (inputDimensions : List (List Lean.Expr)) (inputAxes : List (List Check.EinsumAxis)) (contractedAxes : List Check.EinsumAxis) (contractedLengths : List Lean.Expr) : Lean.Elab.TermElabM (Option (List Check.EinsumAxis × List Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Choose a certified contraction-axis order when exact algebra permits it.

The result contains the planned axes and lengths, their coordinate equivalence to the checked source order, and the permutation certificate used by the final coordinate-sum theorem.