Bipartite Carrier Compression and Machine-Certified Bounds in Schönhage Trilinear Multiplication Tensors
Volkan Dağlı, Zerrin Dağlı, Dağhan Dağlı
cs.CC
Oct 9, 2026 · v1
cs.DS math.CO
TL;DR
Lean 4 proofs, checked by norm_num with no sorry, verify the wire-width reduction identity and the strict improvement of the certified exponent κ over prior records.
Abstract
Under the conditional framework breaking the longstanding O(n log n) integer multiplication barrier (originating from OpenAI Preprint #109), the asymptotic time complexity exponent T(n) = O(n (log n)^{1-κ}) is governed by bounding the second moment E[X^2] < 1 of recursive branching processes over trilinear tensor carrier graphs. In this work, we present a constructive combinatorial optimization over the alternating carrier bipartite matching graphs of the Schönhage trilinear tensor decomposition at dimensions h=23 and h=25. Through an alternating augmenting path search, we uncover a non-trivial cluster-unlocking cascade that eliminates 185 carrier roles (95 roles in h=23 and 90 roles in h=25), reducing the global physical wire width by 377,890 wires from the reviewed baseline W = 177,284,805 down to W = 176,906,915. Evaluated over the exact 10^{-14} rational grid, this wire reduction certifies an improved second-moment coefficient AB = 5,164,059 / 125,000,000,000 and establishes the sharpened conditional exponent κ= 826,215,307 / 20,000,000,000,000 \approx 4.131076535 \times 10^{-5}, strictly surpassing the preceding record on this architecture (κ\approx 4.123864 \times 10^{-5}). All 47 polynomial constraints and 7 rational security margins are audited in exact Q-arithmetic with zero floating-point error, and the fundamental wire reduction identity is formally verified in the Lean 4 interactive theorem prover without unproven axioms.
Problem
In a conditional framework for beating the O(n log n) integer multiplication bound, the exponent κ depends inversely on the wire width W of carrier graphs in Schönhage trilinear tensor decompositions at h=23 and h=25. The goal is to reduce W below the previous record of 177,284,805 and so sharpen κ.
Approach
A 15-round greedy augmenting-path search works on the bipartite carrier matching graphs. It evaluates tensor-parity and vertex-permutation swap moves and recomputes maximum matchings with Hopcroft–Karp. A move is accepted only if it strictly reduces role counts and preserves CRT consistency and rank-mass conservation. The second-moment parameter is then bisected over an exact rational grid. The wire-width identity and the strict-improvement inequalities are formalized in Lean 4 and proved with norm_num.
Results
The search eliminates 185 carrier roles (95 at h=23, 90 at h=25), reducing W by 377,890 to 176,906,915. This certifies κ = 826,215,307/(2×10^13) ≈ 4.131077×10^-5, above the prior κ ≈ 4.123864×10^-5. The Lean theorems are fully proven without sorry.
