A mechanized calculus for index notation with automatic contraction
Abstract
Tensor expressions in index notation, where a repeated index name denotes a summation, are ubiquitous in physics software, but the elaboration of such expressions into explicit sums is rarely verified. We present a small calculus for index notation over a finite index range, with named, variance-tagged indices, and prove in Lean 4 that every well-typed expression transforms covariantly under a change of basis. On top of this core we define a surface language in which a product contracts its repeated names automatically, a translation into the core that introduces explicit contractions and fresh renamings, and an algorithm that infers the set of contracted names from the free indices of the factors. We prove that the translation preserves typing and denotation, that the algorithm is sound and complete with respect to the typing discipline (the contracted set is unique), and that covariance holds for surface expressions. The development is about 1450 lines, uses only the Lean core library, and is intended as the formal core of the tensor fragment of the language PyAct-tensor; the implementation of that language is not itself verified.
Related
- Compiling index notation to sums of products: a verified functional pearl
- Shape calculus and automatic differentiation for multi-phase level-set topology optimisation with unfitted finite elements
- Tensor Contraction with ZX Calculus, a Graph-Theoretic Approach
- A k-Fractional Calculus with Mittag-Leffler Resolvents: Existence Theory and Closed-Form Contraction Thresholds for Singular Boundary-Value Problems
- Harnessing large language models for reliable automatic Charlson Comorbidity Index scoring: a validation study
BibTeX
@misc{pavesi2026mechanized,
title = {{A mechanized calculus for index notation with automatic contraction}},
author = {Luca Eliseo Pavesi},
howpublished = {Submitted to Annals of Formalized Mathematics},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23533336},
url = {https://zenodo.org/records/23533336},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - A mechanized calculus for index notation with automatic contraction
AU - Luca Eliseo Pavesi
PY - 2026
DA - 2026/10/21
PB - Submitted to Annals of Formalized Mathematics
DO - 10.5281/zenodo.23533336
UR - https://zenodo.org/records/23533336
AB - Tensor expressions in index notation, where a repeated index name denotes a summation, are ubiquitous in physics software, but the elaboration of such expressions into explicit sums is rarely verified. We present a small calculus for index notation over a finite index range, with named, variance-tagged indices, and prove in Lean 4 that every well-typed expression transforms covariantly under a change of basis. On top of this core we define a surface language in which a product contracts its repeated names automatically, a translation into the core that introduces explicit contractions and fresh renamings, and an algorithm that infers the set of contracted names from the free indices of the factors. We prove that the translation preserves typing and denotation, that the algorithm is sound and complete with respect to the typing discipline (the contracted set is unique), and that covariance holds for surface expressions. The development is about 1450 lines, uses only the Lean core library, and is intended as the formal core of the tensor fragment of the language PyAct-tensor; the implementation of that language is not itself verified.
ER -