From a7aeea067ec1e2b7e91b0ecec660512b7cafca26 Mon Sep 17 00:00:00 2001 From: Jacob Sussman <95983206+jacobalansussman@users.noreply.github.com> Date: Fri, 9 Oct 2026 12:56:10 -0400 Subject: [PATCH] Add a parallel-effort entry for a Fourier-side Lean development Add one bullet to CONTRIBUTORS.md under "Additional public parallel efforts". It links jacobalansussman/wht-power-saving-lean, pinned at commit fdfb781: a Lean 4 development in the RAM model of openai/math family 130. It proves the general frame lemma of pull request 130 for that model and checks the complex word of pull request 193, rebuilt from the published data, inside a five-stage layout. Documentation only. No bound, certificate, patch, note, script or test changes. The entry says that this is not the multiplication theorem of this project, that it makes no kappa claim, and that nothing in it has been replayed or reviewed here. Built by Jacob Sussman with a team of AI agents (Claude). Co-Authored-By: Claude Opus 5.5 --- CONTRIBUTORS.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CONTRIBUTORS.md b/CONTRIBUTORS.md index 049b44acfa..ee8e4b1399 100644 --- a/CONTRIBUTORS.md +++ b/CONTRIBUTORS.md @@ -211,3 +211,4 @@ verified posts, profile associations and unresolved account identities. - **Michiel Kosters** ([research repository](https://github.com/michielkosters/mathematics_ai/tree/2e0aa64ca09c87fc94f8575f59493f70cf929d71/problems/integer-multiplication-109); Douglas associates @one_line_proof) developed a parallel weighted-hypergraph/coordinate-frame candidate, compressed centers and aligned bit pairing. Our [review](research/parallel-announcements/README.md) reproduces the finite certificate with its transfer/precision limitations explicit. - **Abe / @abe_asfaw**, via a suggestion supplied by Douglas, identified the redundant complex center and its historical 26.5% numerical gain. We [checked the scalar identity, counts and assembly arithmetic](research/parallel-announcements/README.md), and credit this parallel observation alongside the already preserved rank-h center research. +- **Jacob Sussman** ([jacobalansussman](https://github.com/jacobalansussman/wht-power-saving-lean/tree/fdfb7815c15ec43af0fb54818a6a57ae4025126b)) published a separate Lean 4 development on the Fourier side (OpenAI's family 130, not this project's multiplication theorem): a proof of #130's general frame lemma for that RAM model, and a kernel check of #193's complex word, rebuilt from the published data, inside a five-stage layout. It was built with AI agents (Claude) and makes no κ claim. Nothing in it has been replayed or reviewed here.