Positive level-two shapes are explicit permutations of 112
Provedmme_more_asymmetry_positive_level2_shape_explicitfinite-combinatoricsmore-asymmetryrecursive-extraction
If three positive natural coordinates sum to four, then the shape is one of the three permutations of (1,1,2), stated without a local preamble definition so the worker can package the theorem directly.
Preamble
import Mathlib.Tactic set_option autoImplicit false
Formal statement
theorem mme_more_asymmetry_positive_level2_shape_explicit
(a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c)
(hsum : a + b + c = 4) :
(a = 1 ∧ b = 1 ∧ c = 2) ∨
(a = 1 ∧ b = 2 ∧ c = 1) ∨
(a = 2 ∧ b = 1 ∧ c = 1) := by sorrySource
Alman, Duan, Vassilevska Williams, Xu, Xu, Zhou, More Asymmetry Yields Faster Matrix Multiplication, arXiv:2404.16349v2, Definitions 3.5–3.6 and Theorem 6.4, pp. 14–15 and 28–31.