TorchLean tactics

• autograd proves derivative formulas and registered autograd certificates.
• converges proves supported convergence and rate bounds from their hypotheses.
• einops proves supported tensor transformation identities.
• except_cases extracts successful steps from checked computations.
• verify combines registered soundness theorems with kernel-checked evidence.

The ? variants explain the proof or tensor transformation. Import individual tactic modules when the other domains are not needed. NN.Tactic.Verify.Lowering separately loads einsum-lowering correctness rules. Executable regression checks are separate from this proof collection.