InfoView reports for verified tensor transformations

einops? inspects the current target without changing it. Recognized operations appear in a compact InfoView panel. Checked types and the principal shape transformation remain visible. Independent disclosure sections expose the checked axes, proof obligations, lowering stages, generated execution, static work estimates, and correctness theorems on demand.

The tactic inspects expressions and reduces shape metadata; it does not execute tensor kernels or run benchmarks. Optimization estimates are reconstructed by the report analyzer, not extracted from an execution trace. A checked semantic result does not certify those estimates.

def TorchLean.Tensor.Internal.einopsSuggestionTactic : Lean.ParserDescr

Report checked types and shapes, verified lowering stages, generated execution, static work estimates, and compiler-correctness theorems found in the current target.

The tactic is observational: it does not change the target or add local facts. It reduces reflected metadata without executing tensor kernels or running benchmarks. Symbolic certificates retain their dimensions. Optimization descriptions are planner estimates, not observed execution.