v1.0.0: Lean formalization over arbitrary fields

This release archives the Lean formalization of the matrix multiplication exponent bound at most 9/4 over every field, including finite fields and fields of positive characteristic.

OpenAI supplied the original 9/4 construction, complex-field proof, and arithmetic specification. This fork contributes the arbitrary-field extension, developed by GPT-6 Astra and GPT-6.1 Sol agents under Sela Navot's direction. Attribution, automation, and limitations are recorded in formalization.yaml and UPSTREAM.md.

Verification: Palomar's official mechanical verification passed for proof snapshot 8375e73 using Lean and the independent kernels recorded in the report:
https://github.com/PalomarRegistry/PalomarSubmission/actions/runs/37640339487

The release adds citation metadata, documentation, and the unmodified passing report to the identical merged proof tree. It changes no Lean source, dependency pin, Comparator configuration, or verification script. The report certifies its named snapshot; no new proof run for the metadata-only release commit is claimed.

The archive includes the official mechanical report, exact Lean/Mathlib dependency pins, and reproduction instructions. See docs/releases/v1.0.0.md for the evidence digest and source identity.

Palomar's automated review is pending as of 2026-10-07; no permanent Palomar registration or human peer review is claimed. This is an asymptotic arithmetic-operation bound, not a practical implementation or a bit-complexity result. No historical-priority claim is made.

License: Apache-2.0, with separate MIT notices for the vendored fixed-point modules.

Zenodo archive for this exact version: 10.5281/zenodo.23219128.
Concept DOI for all versions: 10.5281/zenodo.23219127.

The archived ZIP was verified byte-for-byte against all 171 tracked files at release commit c88bb830aeb6ebd83f1e48a7bdae566ff5e0924d. Archive SHA-256: d3bcd0c4036341ccf93c457e2de0958dd7dbf8cd5cb842a77b4051d1a2321f42.

Author ORCID: Sela Navot.