すべての人に一次情報を
主発見。論文は、任意の(非可換を含む)環上で3×3行列の積を23回の乗算と55回の加減算で計算するスキームを示します。これは従来記録の56加算から1つ改善したものです(非可換かつ基底変換を行わない正確なスキームとしては初の55未満達成)。(F1,F3)
方法(要点)。入力側の加算最小化はチェーン被覆を用いる実装(sidemin.py)で厳密に求めます。sidemin.pyは閉包正規形を用い、導出可能な目標を貪欲に覆した後に補助値(helper)の挿入で分岐する反復深さ探索を行います。これにより各辺の最適加算数は「異なる多項目目標の数 + h*」という形で得られます。
出力側は転置原理(Tellegen)を適用して厳密に最小化します。加算のみの線形写像 W について、次が成り立ちます。 A(W) = A(W^T) + inputs(W) − outputs(W) この定数差により、9×23の出力側問題は9入力の問題に帰着し、入力側の最小化器で解けます。出力側最小化は構成的で、転置したチェーンから明示的な出力プログラムを得られます(tcmin.py)。(F4,F5,F18)
具体的結果。スキームはA側で13個、B側で14個の符号付き線形結合を作り、それら23組の積を取り、さらに28回の加算で再結合します(13+14+28=55)。Perminovのcn122代表(de Grooteクラス i19w225c4efh)に本手法を適用すると、入力側は13+14、出力側は28(貪欲法は29)となり合計55になります。sidemin.pyはSunの入力側最適値と不可能性証明(例:U: 12目標→h* =1で13加算等)を再現します。(F2,F6,F17)
実装と検証。提案スキームは実行可能なプログラム(src/mm55.rs および matmul/external/i19-55adds-slp.txt)として提供されます。その明示的な直線プログラムは、従来の27乗算三重ループと500,000件のランダム整数入力および50,000件の非可換2×2ブロック入力で照合され、操作計数が正確に23乗算・55加算であることが確認されています。スキームの正しさはLean 4で機械検証(sorry‑free proof)されています。成果物はDOI付きの記録庫とソースリポジトリにアーカイブされています。(F8,F9)
比較。従来の60→56の記録更新は貪欲な共通部分式消去(greedy CSE)に依存していました。greedy CSEは各辺を上から評価するため下界を見落とすことがあり、本稿の両側厳密最小化はPerminov代表で1加算の改善を発見しました。Sunの代表については出力側が30であり出力最適であることが本手法で確認されています。独立の再発見報告(Karunaratne & Idamekorala, arXiv:2607.28676)も同じテンソルと13+14+28分割・転置出力構成を報告しています。(F7,F10,F11)
最適性の範囲と制約。本稿の最適性主張は、直線プログラムにおける二項加減算の数を数えるコストモデルに依存します。一般の線形写像に対する最短直線プログラム問題はNP困難です。公表済みの17,376クラスを横断する計算では、レコードクラス(i19w225c4efh)のみが55を達成し、他クラスは少なくとも56以上でした。したがって、このカタログと本稿のコストモデル内では55が最小です。未収載のクラスや別のコストモデル(例えば真にdyadicな係数を許すモデル)が存在すれば、より小さい加算数の可能性は排除されません。(F13,F14,F12,F15)
再現性の注意。sidemin.py と tcmin.py は自己検査を備え、sidemin.py は Sun の入力側証明を再現します。実験の再現には kissat や Rust/Lean 等の環境が必要です。決定論的注意点として、kissat のバージョン差により返る符号モデルが変わることがあります(ただし各モデルは整数上で検証されます)。Lean の一部証明は文献に記載の公理に依存します。提供されたコミット済み代表と発行済み SLP により55加算の検証は決定論的に行えます。(F16)
総括。本稿は、任意の環上で動作する具体的な23×/55加算の3×3行列乗算スキームを提示します。左右両側を厳密に最小化する手法を示し、明示実装・試験・機械証明を添えた点が主な貢献です。(F1,F2,F3,F4,F5,F6,F8,F9)