AI 中文总结
本文确定了八元数乘法的实张量秩的界为18至25，还推导了偶数维实赋范可除代数的通用下界，并验证了相关张量的秩，结果由Lean 4内核和脚本确认。
AI 中文摘要
双线性映射的张量秩是计算它所需的任何双线性算法的最少乘法次数；对于代数的乘法而言，它衡量了该代数进行乘法运算的成本高低。对于偶数维的实赋范可除代数，复数的张量秩为3，四元数的为8，均为经典结论；而八元数（$\boldsymbol{\text{O}}$）的张量秩此前仅知一个范围：至少15（Fiduccia和Zalcstein，1977年），至多30（Cariow和Cariowa）。本文证明了 $18 \boldsymbol{\text{≤ R}}_{\boldsymbol{\text{R}}}(\boldsymbol{T}_{\boldsymbol{\text{O}}}) \boldsymbol{\text{≤ 25}}$。下界的推导是将八元数乘法张量 $\boldsymbol{T}_{\boldsymbol{\text{O}}}}$ 的八个切片缩减为两个，并通过八元数范数对剩余的 pencil 的秩进行界定；该推导并非仅适用于8维，相同步骤可对每个偶数维 $n$ 的实赋范可除代数 $A$，得到 $\boldsymbol{\text{R}}_{\boldsymbol{\text{R}}}(\boldsymbol{T}_A) \boldsymbol{\text{≥}} \boldsymbol{\frac{5}{2}} \boldsymbol{n} \boldsymbol{-} \boldsymbol{2}$，该下界对复数和四元数是紧的，也是目前针对八元数已知的最佳下界。上界则是通过独立构造得到的，即一个显式的秩-25分解，该分解通过Krawczyk论证在精确有理算术下被验证与精确分解的误差在 $10^{-6}$ 以内。上述两个论证还确定了一个更小的三切片四元数张量 $\tau$ 的秩为7。Lean 4内核验证了下界和Krawczyk存在性原理，附带的脚本则验证了证书有限个精确有理不等式。
英文摘要
The tensor rank of a bilinear map is the least number of multiplications any bilinear algorithm needs to compute it; for the multiplication of an algebra it measures how cheaply the algebra can be multiplied at all. For the even-dimensional real normed division algebras it is $3$ for the complex numbers and $8$ for the quaternions, both classical, while for the octonions $\mathbb{O}$ only a range was known: at least $15$ (Fiduccia and Zalcstein, 1977) and at most $30$ (Cariow and Cariowa). We prove $$18 \le \operatorname{R}_{\mathbb{R}}(T_{\mathbb{O}}) \le 25.$$ The lower bound peels the eight slices of $T_{\mathbb{O}}$ down to two and bounds the rank of the surviving pencil through the octonion norm. Nothing in it is special to dimension $8$: the same steps give $\operatorname{R}_{\mathbb{R}}(T_A) \ge \frac{5}{2}n - 2$ for every real normed division algebra $A$ of even dimension $n$, sharp for $\mathbb{C}$ and $\mathbb{H}$ and the best bound we know for $\mathbb{O}$. The upper bound is a separate construction, an explicit rank-$25$ decomposition certified by a Krawczyk argument, in exact rational arithmetic, to sit within $10^{-6}$ of an exact one. The same two arguments pin down the rank of a smaller three-slice quaternion tensor $τ$, giving $\operatorname{R}_{\mathbb{R}}(τ) = 7$. The Lean 4 kernel checks the lower bounds and the Krawczyk existence principle; the accompanying scripts check the certificate's finitely many exact-rational inequalities.
CommentsCode at https://github.com/hxrdxkxvxd/octonion-rank
