Research: lower bounds for small complex units: m = 2 never saves, m = 3 needs 14W/5 calls (Lean, engine game), m = 4 needs 41W/13, and the smallest open cases (no new κ)

research/complex-small-m-lower-bounds/.gitattributes

@@ -0,0 +1,2 @@
+# Keep the package bytes exact: verify.py and SOURCES.json record the sha256 of the data files.
+* -text

research/complex-small-m-lower-bounds/SOURCES.json

@@ -0,0 +1,196 @@
+{
+ "schema_version": 1,
+ "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+ "upstream_repository": "https://github.com/CrocSwap/integer-mult-bounds",
+ "files": [
+  {
+   "path": "docs/research/agent-task-catalog.json",
+   "usage": "provenance",
+   "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+   "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+  },
+  {
+   "path": "research/abelian-cayley-metric-scope/sources/pr288-README.md",
+   "usage": "provenance",
+   "git_blob": "dc04f533bd0f3b185969bb259e876a73714f7285",
+   "sha256": "c091e98c415e2a80bb28402b789363eb97dd3492061ca8875e421ae437de7482"
+  },
+  {
+   "path": "research/two-register-three-mix/README.md",
+   "usage": "provenance",
+   "git_blob": "593549db00fac1a10734868380eab28bcb584cc2",
+   "sha256": "3353fe948c75fbfc56841260db02d5e14aba966d157d3390fe3d4785e397af60"
+  }
+ ],
+ "inputs_note": "No live inputs from this repository. The two research provenance rows are the predecessor texts quoted in README.md section 2 (#288 by eumemic, retained on main; #2108 by jmbarrancoml). verify.py reads only files inside this package.",
+ "external_sources": [
+  {
+   "what": "the files under data/ and author-evidence/ listed here: copied unchanged from my public repository (the files added on 23 October 2026 are listed in the next two entries); verify.py checks each file's sha256 (part pins). The commit is not a Git object of this repository, so it cannot be pinned with a source pin; the byte equality is recorded here.",
+   "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+   "commit": "86e575e28ed94890872dcff1bb2621d7ff559cbd",
+   "copies": [
+    {
+     "package_path": "data/cert_m3_dem.json",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m3_dem.json",
+     "source_git_blob": "76678077d87cd677caf91d56e306e2df3aab2b38",
+     "sha256": "99235c4fbfb37a2205a888b18292edbfa3be07970dd0550c47f79bbe66e802c3"
+    },
+    {
+     "package_path": "data/cert_m3_B2.json",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m3_B2.json",
+     "source_git_blob": "de6959c8ad45046f9a540c2c1c73051c75c8c9aa",
+     "sha256": "078eb2a6a481f5a176b2fce2331fb285dbe8e20b034c5bb4558abc2455a27cf6"
+    },
+    {
+     "package_path": "data/cert_m3_M0.json",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m3_M0.json",
+     "source_git_blob": "3be65e03f6b3b2069ccc597f7caa48b17bb57d48",
+     "sha256": "325f47b568ce2fee4d1b8848f19b0e27772340de5b4a04702d8799b3b1763748"
+    },
+    {
+     "package_path": "data/cert_m3_M0_c.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m3_M0_c.txt",
+     "source_git_blob": "2f5a07b14cf103e178d706f877d4196af3a486f1",
+     "sha256": "82169f3e70bc11ebdabc9b573f82f50f92e0a8073c5e747deb64714a84c0e6bc"
+    },
+    {
+     "package_path": "data/cert_m2_M0.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m2_M0.txt",
+     "source_git_blob": "40be8de96cbfe05b688e1b8f5fe2b5bcbe032359",
+     "sha256": "884bc29dbaf3714cb23426f56e28039e1dafb9b13f63a6b595b8dc15423f3cf0"
+    },
+    {
+     "package_path": "data/neg_m3_29.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/neg_m3_29.txt",
+     "source_git_blob": "fc5c183f52c9f224f909528fcd3ad7ff461507f3",
+     "sha256": "1d89519b59d32f23ca4dd5355b45ed03a226bec430bc90aeafaac0d001bbfa36"
+    },
+    {
+     "package_path": "data/neg_m3_comp.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/neg_m3_comp.txt",
+     "source_git_blob": "742b35a6db984ad1eae2b36e48d8cbdfef539b4f",
+     "sha256": "4ebc926017f670b43345af6d984039b4b93327ddb387e6d95d8f861133f65a8c"
+    },
+    {
+     "package_path": "data/neg_m3_dup.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/neg_m3_dup.txt",
+     "source_git_blob": "7bc7ff614a149449b0caf8f88a7b724ba65446cc",
+     "sha256": "f6fe0a5d3025396dcfe168214a33e4730e20c46187b5b68a5aeaf86cabbfa928"
+    },
+    {
+     "package_path": "data/cert_m4_M0.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m4_M0.txt",
+     "source_git_blob": "254beec5222daedda500ecdaac28ca712a3d6d7f",
+     "sha256": "72530af84ea9a702b9e48b1dd8d5e69e9b0552840096f38b5caac9667c4236e2"
+    },
+    {
+     "package_path": "data/Dem3Data.lean",
+     "source_path": "research/block-bounds-and-new-rules/programs/lean-block2-block3/PfLean/Dem3Data.lean",
+     "source_git_blob": "13b707be01006223776af137c661eaaf090446d1",
+     "sha256": "0982f9cf408a7d2f930b4e65d1e2b1bd6a22b3c0601c372886fa7d9bf4c0cc52"
+    },
+    {
+     "package_path": "author-evidence/check_m0.c",
+     "source_path": "research/block-bounds-and-new-rules/programs/hook-certificates-blocks-2-to-6/check_m0.c",
+     "source_git_blob": "5748359d049c7a4e10479b5f1487e118acc4db41",
+     "sha256": "8242342188fe73eb8ab0db9e48727d086ec78c38032bdfb76b38a3af40ceef6e"
+    }
+   ]
+  },
+  {
+   "what": "the Lean proofs quoted in README.md section 5 (not copied; the hub's intake does not run Lean)",
+   "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+   "commit": "86e575e28ed94890872dcff1bb2621d7ff559cbd",
+   "path": "research/block-bounds-and-new-rules/programs/lean-block2-block3",
+   "toolchain": "leanprover/lean4:v4.34.1; Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612",
+   "build_log": "research/block-bounds-and-new-rules/programs/lean-block2-block3/logs/rebuild_2026-10-19.txt",
+   "statements_log": "research/block-bounds-and-new-rules/programs/lean-block2-block3/logs/statements.txt"
+  },
+  {
+   "what": "the written arguments condensed in PROOF.md sections 4 to 7, and the programs behind the statuses",
+   "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+   "commit": "86e575e28ed94890872dcff1bb2621d7ff559cbd",
+   "paths": [
+    "research/block-bounds-and-new-rules/README.md",
+    "research/moonshot-small-blocks/README.md",
+    "research/theory-of-theories-and-logic/README.md",
+    "research/reed-muller-and-one-move/proofs/address-maps-per-array-targets-and-block3.md",
+    "research/existence-routes/proofs/families-commutative-slice.md",
+    "research/open-problems.md"
+   ]
+  },
+  {
+   "what": "the certificates for the block-4 inputs of section 7 (a_2 >= 48,576 and a_3 >= 68,320, one nonsingular minor per character, 16 characters each), their checker and its outputs, added on 23 October 2026 after #4643: copied unchanged; verify.py checks each file's sha256 (part pins) and their format (part depth)",
+   "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+   "commit": "ce3c2615cff7fc524c1fde3ddb99d151ba4ceee4",
+   "copies": [
+    {
+     "package_path": "data/cert_m4_g2_M0.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m4_g2_M0.txt",
+     "source_git_blob": "c205e36cd1112391cfe026c2c6d454bc8b02ad06",
+     "sha256": "1961d7482576245953e4b0368603ecf6295b02a8543334816e5c0139d64601c3"
+    },
+    {
+     "package_path": "data/cert_m4_g3_M0.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/cert_m4_g3_M0.txt",
+     "source_git_blob": "85151a1fb2fa087141b287296f32101090e7ce75",
+     "sha256": "b04afdc7cb060c96605aeff19ee8a1ceb0968785208f6e66a938ebec7c3125ca"
+    },
+    {
+     "package_path": "author-evidence/check_mj.c",
+     "source_path": "research/block-bounds-and-new-rules/programs/hook-certificates-blocks-2-to-6/check_mj.c",
+     "source_git_blob": "31f01fa28312aa2f0c1fa350c03f6c37b9b6fdf5",
+     "sha256": "ca59130c3153da31eac93282126c797afd555d9a0934f60ecb38e304f46e82e0"
+    },
+    {
+     "package_path": "author-evidence/out_check_m4_g2.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/outputs/out_check_m4_g2.txt",
+     "source_git_blob": "faecc5517d04475dcfe394e2b98b64289b6513c8",
+     "sha256": "7c4291efee95581d491be507e3f024d8ad36095d58440efd37c2ce9a1e5ea3c1"
+    },
+    {
+     "package_path": "author-evidence/out_check_m4_g3.txt",
+     "source_path": "research/block-bounds-and-new-rules/data/hook-certificates/outputs/out_check_m4_g3.txt",
+     "source_git_blob": "fa9efe468f0eb034cea724ff49306eda96aefa9b",
+     "sha256": "f82df0cd636ac90734699b2d4cf269354b59e4332687732a027f6bffe254f97a"
+    }
+   ]
+  },
+  {
+   "what": "the written proof of section 7 (my induction note, kept as written; its relative links refer to that repository), published on 23 October 2026: copied unchanged; verify.py checks its sha256",
+   "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+   "commit": "f08d308ff93f4867165a1e80765fe985c06b4edf",
+   "copies": [
+    {
+     "package_path": "author-evidence/induction-across-block-sizes.md",
+     "source_path": "research/block-bounds-and-new-rules/proofs/induction-across-block-sizes.md",
+     "source_git_blob": "9343bbd87a8e2d2b5b2b8fbca34da04033d95ce7",
+     "sha256": "0c2f6f5a07f1deccfa2b838c6d29bc6d86567069569890c37c820b03f7d888ef"
+    }
+   ]
+  },
+  {
+   "what": "the two AI reviewers' reports on that proof, their programs (fcheck.py is the split that part depth uses) and Fact A's matrices (not copied)",
+   "repository": "https://github.com/jacobalansussman/wht-power-saving-lean",
+   "commit": "f08d308ff93f4867165a1e80765fe985c06b4edf",
+   "paths": [
+    "research/block-bounds-and-new-rules/proofs/induction-across-block-sizes-skeptics.md",
+    "research/block-bounds-and-new-rules/programs/engine-bounds-blocks-5-and-6/skeptic-checks/",
+    "research/block-bounds-and-new-rules/programs/engine-bounds-blocks-5-and-6/fact-a/",
+    "research/block-bounds-and-new-rules/data/engine-bounds-blocks-5-and-6/"
+   ]
+  },
+  {
+   "what": "David Harvey, 'On the recently proposed o(n log n) integer multiplication algorithm', UNSW Sydney, 20 October 2026 (quoted in README.md section 7)",
+   "url": "https://web.maths.unsw.edu.au/~davidharvey/research/subnlogn.pdf"
+  },
+  {
+   "what": "Swapnil Jain's papers P1 and P2, cited through #288",
+   "doi": [
+    "10.5281/zenodo.23265442",
+    "10.5281/zenodo.23266393"
+   ]
+  }
+ ],
+ "source_boundary": "Only this new package is submitted. No file outside research/complex-small-m-lower-bounds changes."
+}