Transform reports

This module reports concrete rearrange, repeat, and reduce certificates.

Work estimates count the generated traversal and calls to supplied reducers, fold steps, and finalizers. They exclude work and allocations performed inside those user functions.

def TorchLean.Tensor.Internal.Report.Impl.concreteTransformReport (operation : String) (checked inputScalarType outputScalarType : Lean.Expr) (supplementaryTypeEntries : List (String × String)) (nativeExecution correctnessTheorem denotation : String) (nonemptyReduction foldReduction : Bool := false) : Lean.MetaM (Option String)

Decode a concrete rearrange, repeat, or reduce certificate into its normalized axes, verified logical stages, and native execution strategy.