Lean 4 kernel check of six published matrix-multiplication tensor decompositions

Lean 4 kernel checks (decide +kernel, no native_decide, Lean core only) that six matrix-multiplication tensor decompositions published in google-deepmind/alphaevolve_results (mathematical_results.ipynb, commit 4226acbf) satisfy the tensor identity: <3,3,3> 23 terms, <2,4,5> 32, <4,4,4> 48, <3,4,7> 63, <4,5,6> 90 and <5,5,5> 93. Every identity depends only on the axioms [propext, Quot.sound]. Nothing here concerns optimality; the <3,3,3> case is Laderman's (1976) baseline. Decomposition coefficients: © 2025 Google LLC, CC-BY-4.0 (materials) / Apache-2.0 (software); changes: transcribed into Lean, half-integer entries doubled, complex entries as integer pairs. Lean projects, generator and checksums are in certificates_tensors.zip. The archive's Final theorems state the listed term count together with the identity.