Import matrix multiplication exponent at most 9/4 over every field

LeanPool/MatrixMultiplicationAllFields.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 the original authors and Jeroen Zuiddam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: OpenAI, Jeroen Zuiddam
+-/
+module
+
+public import LeanPool.MatrixMultiplicationAllFields.LinearAlgebra.MatrixMultiplication.AllFields.Main
+
+/-!
+# Matrix multiplication exponent at most 9/4 over every field
+
+Source: url:https://github.com/jzuiddam/omega-nine-quarters-all-fields/tree/615b591cddd8792173c17b58558ef3b9f11a702c
+Authors: OpenAI, Jeroen Zuiddam
+Status: verified
+Main declarations: `MatrixMultiplicationAllFields.omega_le_nine_quarters_all_fields`
+Tags: matrix-multiplication, arithmetic-complexity, tensor-rank, field-extensions
+MSC: 68Q17, 15A69, 68Q25
+-/
+
+/-
+Preserved upstream attribution and Apache modification notice:
+
+omega-nine-quarters-all-fields
+Copyright 2026 Jeroen Zuiddam
+
+This product is a derived work of the Lean library in openai/math
+(https://github.com/openai/math), commit adc7f1241b42e322a6451854ab7e4b4c146bf78a, directory
+`lean/`, which is licensed under the Apache License, Version 2.0. The relevant upstream
+results are
+those of "family 107", the formalisation of OpenAI, "An Upper Bound of 9/4 for the Matrix
+Multiplication Exponent" (OpenAI Math Release preprint, 2026). Upstream ships no NOTICE
+file, and its
+LICENSE leaves the copyright line unfilled; the upstream files remain the work of their
+authors.
+
+The file `patches/fixed-point-theorems-lean4341.patch` is copied verbatim from
+openai/math. It
+patches the third-party package fixed-point-theorems
+(https://github.com/harfe/fixed-point-theorems-lean4, commit 770940ddf9878cf61952ed53d910b92bca841838)
+for Lean v4.34.1. That package is fetched by Lake and is not redistributed here.
+
+Contents and changes relative to upstream (paths are relative to upstream's `lean/`).
+This NOTICE
+summarizes the changes; each modified source file carries its own detailed change notice.
+
+* 99 modules under `OAI/` are copied unchanged.
+* 41 modules under `OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/` are
+modified. Each
+  begins with a comment "Modified from openai/math (adc7f1241) ... by Jeroen Zuiddam,
+  2026: ..."
+  stating what was changed. In summary:
+  - `ℂ` was replaced by an arbitrary algebraically closed field `K` throughout this
+  subtree;
+  - Proposition 3.1 (Fourier separation) uses a period L in {3M-2, 3M-1} that is nonzero
+  in `K`,
+    instead of L = 5M (Separation/{Fourier,NoWrap,FiniteProjection,Basic},
+    Character/FiniteSeparation);
+  - interpolation and convolution nodes come from an embedding of the natural numbers
+  into `K`
+    (Polynomial/Interpolation, Convolution/Rank);
+  - Arithmetic/Exponent was rewritten to pass from rank bounds to arithmetic cost over
+  an arbitrary
+    field;
+  - six ℂ-only lemmas whose removal does not affect the retained proof were removed
+    (Separation/Basic, Convolution/Rank, Polynomial/Interpolation, Sector/Degeneration);
+  - `[IsAlgClosed K]` is an explicit binder on the declarations that use it, not a
+  section variable;
+  - docstrings were updated and a few linter warnings were fixed.
+* New files, Copyright 2026 Jeroen Zuiddam:
+  - `OAI/LinearAlgebra/MatrixMultiplication/AuxiliarySeparation/Tensor/MatMul.lean`;
+  - `OAI/LinearAlgebra/MatrixMultiplication/AllFields/Descent.lean`;
+  - `OAI/LinearAlgebra/MatrixMultiplication/AllFields/Main.lean`;
+  - `Checks/Axioms.lean`;
+  - `README.md`, this `NOTICE`.
+* Files derived from upstream files (each carries a "Modified from openai/math ..."
+notice, except
+  as stated):
+  - `OAI.lean` is derived from upstream's `OAI.lean`, reduced to a single import of
+  `AllFields.Main`.
+  - `ComparatorChallenges/MatrixMultiplicationAllFields.lean` is derived from upstream's
+    `ComparatorChallenges/MatrixMultiplication.lean`. Its model definitions are
+    verbatim; only the
+    header comment and the theorem statement were changed.
+  - `ComparatorChallenges/MatrixMultiplicationAllFields.json` is derived from upstream's
+    `ComparatorChallenges/MatrixMultiplication.json`. The module names and theorem names
+    were
+    changed, and an informational `_modification_notice` property carrying the change
+    notice was
+    added (JSON has no comments); the checking fields are otherwise as upstream.
+  - `lakefile.lean` is reduced from upstream's lakefile to the two dependencies used
+  here and the one
+    compatibility patch they need.
+  - `.gitignore` is upstream's `.gitignore` verbatim, followed by one marked added rule
+  (`/.lake`,
+    so that a `.lake` symlink is also ignored).
+  - `lake-manifest.json` is not a copy of upstream's manifest: it was generated by `lake
+  update` for
+    this project and lists only the packages this project uses. Each of its package
+    entries (pins
+    included) is identical to the corresponding entry of upstream's manifest. Being
+    generated, it
+    carries no notice; `lake update` would not preserve one.
+  - `lean-toolchain` and `LICENSE` are copied unchanged.
+* Not included: everything else in openai/math, including upstream's other results and its
+  remaining comparator challenges.
+
+Lean Pool port: module paths and namespaces changed; the external Brouwer dependency
+is replaced by the pooled simplex theorem. Entropy proofs use the public Mathlib API.
+-/
+
+@[expose] public section
+
+namespace MatrixMultiplicationAllFields
+
+/-- The matrix multiplication exponent is at most 9/4 over every field. -/
+theorem omega_le_nine_quarters_all_fields (F : Type*) [Field F] :
+    MatrixMultiplication.Arithmetic.omega F ≤ (9 : ℝ) / 4 :=
+  MatrixMultiplication.omega_le_nine_quarters_all_fields F
+
+end MatrixMultiplicationAllFields