[jacobalansussman]

Change and mathematical scope

Adds one package, research/complex-small-m-lower-bounds. It collects lower bounds on the number of calls s that a
unit for W complex arrays needs at small block size m, each in a stated game, and the smallest shapes they leave
open. It is a bounded index of one obstruction family plus the bounds behind it. No construction, no new κ, no
claim about integer multiplication.

Result	Game	Status
The kept-subspace bound (a general form of #288's FO lemma)	engine game	proved in Lean
m = 2: s ≥ 2W	engine game; every game with bounded free steps	proved in Lean; argued by hand in the bounded games (one AI reviewer)
m = 3: s ≥ 14W/5 (saving at most 6.28e-2; every unit with 4 or fewer arrays excluded)	engine game; widened game	proved in Lean; argued by hand in the widened game (three AI reviewers)
m = 4: s ≥ 41W/13 (saving at most 1.71e-1)	engine and widened games	checked by computer; in the widened game it also rests on the keptness argument, argued by hand
m ≥ 4: at least 2.9447 calls per array (2.99172 at m = 5, 2.97290 at m = 6)	engine game	argued by hand (two AI reviewers reproduced the numbers)
m = 3 without phase letters: s ≥ 3W for every group of address maps	no-phase game	argued by hand (one AI reviewer); certificate checked by computer here
One array needs m calls; W ≥ 2 arrays need max(W + m, 2W)	every game with bounded free steps	argued by hand (AI reviewers)

The engine game is the game of the Lean engine in my repository: OpenAI's letters (calls C_v, shifts, rational
mixing with scratch) plus invertible XOR-linear address maps and phases i^(z·x + c). Every bound is for units right
at every number of digit columns. The Lean statements are for rational mixing; complex mixing is argued from the
same proof. Statuses use my public repository's words; no person has read any of the proofs.

Smallest open shapes (engine game): 5 in 14 at m = 3 (6.28e-2, exactly on the bound), 2 in 7 at m = 4 (9.63e-2),
3 in 10 and 4 in 13 at m = 4; 2 in 7 and 3 in 9 at m = 5; 2 in 8 and 3 in 9 at m = 6 (3 in 9 is not excluded by any
bound I know). In games that make neighbouring-column maps free, 2 in 5 and 3 in 6 at m = 3.

README section 7 answers the two small-gadget questions in David Harvey's note "On the recently proposed
o(n log n) integer multiplication algorithm" (20 October 2026): why one array cannot save (his §6; argued by hand, for programs right at every digit width), and his
suggested search for "a non-trivial gadget for I ⊗ B^(⊗3) acting on C^4 ⊗ (C^2)^(⊗3)" (his §8), which needs at
least 12 calls by the m = 3 bound (14 × 4 = 56 > 55 = 5 × 11): proved in Lean for C-calls with rational mixing,
argued by hand for complex mixing and B-calls, for programs right at every digit width. At width 1 the question
degenerates (one zero scratch array makes C^(⊗3) free; checked by verify.py). In his §7.4 model as written,
m = 3 and m = 4 never save for programs right at every digit width (argued by hand at m = 3, checked by computer
at m = 4), so a search there that tests each candidate at width 2 or more is a good calibration run.

Remaining obligations: the Lean files are not run by the hub's intake (built on an 8-core Linux machine, 11
minutes, 10.06 GB peak); the m = 4 demand determinant is author evidence (C, about an hour); the hand arguments have
AI reviewers only; whether #288's full register model lies inside the engine game is not checked, so #288's open
m = 3 cases are claimed excluded only in the engine game.

Task and overlap

• Base f626db5c3a3d781d8f7695038776c621651f75e1. Card scope-navigation (method "Index one tightly related family
  of obstructions with explicit excluded and open hypotheses"), scope_status: changed, reason in TASK.json: the
  package also adds bounds that are not on main.
• No live inputs from this repository. Provenance rows: the task catalogue, Negative results from a search for a new coding mechanism: m = 2 closed on both sides, flag theorems, closed routes (no new κ) #288's retained README and Prove a two-register cost bound for three scalar mixing blocks #2108's
  README. The data files are copied unchanged from my public repository
  (jacobalansussman/wht-power-saving-lean at 86e575e28ed94890872dcff1bb2621d7ff559cbd); verify.py checks each
  file's sha256 and SOURCES.json lists the source paths and Git blobs.
• Nearest work and what this adds: Negative results from a search for a new coding mechanism: m = 2 closed on both sides, flag theorems, closed routes (no new κ) #288 (eumemic: FO lemma, m = 2, 50W/21 at m = 3 with W = 2, s = 5 and W = 3,
  s = 8 open) → a Lean proof on an engine's definitions with scratch and singular mixing, 14W/5 at m = 3, and
  bounds at m ≥ 4; Prove a two-register cost bound for three scalar mixing blocks #2108 (jmbarrancoml: a five-call solution needs at least four nonmonomial mixing blocks; "We do not
  settle the five-call problem") → excluded in the engine game; Negative results from a search for a new coding mechanism: m = 2 closed on both sides, flag theorems, closed routes (no new κ) #288's doubled-import bound E + σ ≥ 2W and P1's
  "at least 2W children" row → 2W at every block in every game with bounded free steps (argued by hand); Swapnil
  Jain's P1/P2, cited through Negative results from a search for a new coding mechanism: m = 2 closed on both sides, flag theorems, closed routes (no new κ) #288; bit-side
  parallels Prove nine calls are necessary for three abelian bit registers #468, Research theorem: nine-call bound for arbitrary invertible three-register targets #720, Research: dirty auxiliary registers do not save in the two-register m=3 bit model (no new kappa) #1882, Research: clean ancillas do not save in the two-register m=3 bit model (no new kappa) #2167, Research theorem: common-flag rational-frame obstruction (no new kappa) #825, Research: structural barriers for kappa = 0.01 (no new exponent) #203, Scoped corollary (no κ): PR288 open item 3 (full-Borel bit register model) on unit targets is closed for 2-integral data — mW floor via PR288's FO-on-Λ/2Λ with P1's ν; free maps singular mod 2 allowed #2613 (other models; not inputs). README section 2 has one
  "closest prior work; this adds" sentence per item and a short factual paragraph on Negative results from a search for a new coding mechanism: m = 2 closed on both sides, flag theorems, closed routes (no new κ) #288's Fano obstruction. I found no hub
  package with bounds at m ≥ 4 or the no-phase m = 3 bound; that is a search result, not a proof of novelty.

Validation

python3 scripts/research_package.py --package research/complex-small-m-lower-bounds --check-only
python3.12 -B scripts/research_package.py --package research/complex-small-m-lower-bounds
# = python3 -B research/complex-small-m-lower-bounds/verify.py --part main       (PASS_COMPLEX_SMALL_M_LOWER_BOUNDS_MAIN)
#   python3 -B research/complex-small-m-lower-bounds/verify.py --part controls   (PASS_COMPLEX_SMALL_M_LOWER_BOUNDS_CONTROLS)
python3 -B scripts/check_research_commit.py --package research/complex-small-m-lower-bounds

Standard library only. On a shallow clone at the base with Python 3.12.13 on an Apple M4 (macOS): --check-only
passes; the registered replay passes in about 2.4 seconds of wall time (verify.py peaks at about 33 MB, the
runner's whole process tree at about 103 MB) and leaves no files behind;
the commit byte check passes on a local commit; the planner selects only this package; the onboarding tests pass
(26). Not run: --check-source-history (it needs full Git history), and Linux x86 (no native code is used).

Evidence inside the check: block-2 and block-3 caps by exact vectors over the Gaussian integers, and attained; the
block-3 demand 224 by a certified 224 × 224 minor and by the rank of the whole 280 × 280 block; two calls in a row at
most 144; the character block of rank at least 28 in two formats by two routines; the eight 28 × 28 blocks of the Lean data
file times the formula matrix equal to the identity mod 65537 (the check Lean's kernel ran); the face certificate of
the no-phase bound, exact over Q(i); the m = 4 arithmetic and the format of its certificate; the width-1 program;
every figure and exclusion in the README tables.

Failure controls (each must be rejected, and is): demand certificate with a repeated row, a composite modulus, a row
inside the hook, a 225 × 225 minor; two-call certificate with a changed and a repeated vector; a cap of 79; the three
corrupted certificates of my repository; one Lean inverse entry plus 1; a face cap of 7; a CNOT claimed to keep the
face span; the width-1 program at width 2; 4 in 11 claimed allowed, 5 in 14 and 2 in 7 claimed excluded.

Not run by this package: the Lean build (statements quoted verbatim in README section 5; axioms propext,
Classical.choice, Quot.sound; a negative control rejected; two AI reviewers rebuilt or restated it), and the
m = 4 determinant (author-evidence/check_m0.c, determinant 1797789153 modulo 2,147,483,629). No independent human
review.

Credit

eumemic (#288) for the certificate method and the m = 2 and m = 3 results this builds on; Swapnil Jain (P1, P2);
jmbarrancoml (#2108); aliromman (#468), davidgovea (#720), waynenilsen (#1882, #2167), navinor (#825), huxint (#203)
and thakrarsagar (#2613) for the bit-side parallels; OpenAI for the Lean engine and cost model; Ryan Shea for the Lean
tree the files were built in; David Harvey for the questions of README section 7.

Substantial AI assistance: the programs, checks, proofs, Lean files and texts were written by AI agents (Anthropic
Claude) under my direction. The Lean proofs are checked by Lean's kernel; no independent human review is claimed.
Apache-2.0.

Open next questions

In README (## Open next questions) and TASK.json. The smallest useful follow-ups: 5 in 14 at m = 3 (decide one
sector of its symmetric sub-game exactly, judged at width 6); 2 in 7 at m = 4 (an exact search with address maps
in the middle and phase letters between calls, or a certificate above 3.5 calls per array); whether #288's full
register model keeps the m = 3 hook (list its free elements and test each); 2 in 5 and 3 in 6 at m = 3 with
neighbouring-column maps free; Lean for complex mixing and for 41W/13; 2 in 7, 2 in 8 and 3 in 9 at m = 5 and 6.

Workflow feedback (optional)

None.

🤖 Generated with Claude Code