Verified einsum scalar product generation

The scalar kernel compiler is organized as certified operand indexing, generated-term utilities, contraction-invariance analysis, and ordered product assembly; this module is the final assembly stage and is what importers of the kernel compiler name.

This module assembles direct operand reads into the ordered scalar product used by a checked einsum. It also extracts semiring factors that are invariant across the contraction while retaining a pointwise semantic certificate.

def TorchLean.Tensor.Internal.Elab.Impl.compileEinsumInputProduct (checked inputTensorFamily scalarType : Lean.Expr) (inputTensors : List Lean.Expr) (inputViews : List (Option (Lean.Expr × Lean.Expr × Lean.Expr))) (inputDimensions : List (List Lean.Expr)) (inputAxes : List (List Check.EinsumAxis)) (outputAxes semanticContractedAxes contractedAxes : List Check.EinsumAxis) (outputLengths semanticContractedLengths contractedLengths : List Lean.Expr) (contractionCoordinateMap? : Option Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr × Option (Lean.Expr × Lean.Expr × Lean.Expr × Lean.Expr))

Generate the direct scalar product used by a literal einsum and an erased pointwise proof that it equals the generic verified implementation.

Output coordinates are computed before the contraction lambda. Eligible multi-term output-index bases are hoisted from the contraction loop. With multiple contracted axes, every operand's outer-axis contributions are combined into a base that the loop compiler floats outside the innermost contraction loop. Over a semiring, maximal source-order prefixes and suffixes that do not use a contracted axis are also returned as optional factors.