Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Round-eight complex network in the item-language gate class

Open
IntMul.Kappa.R8.cxNetR8G

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationround-eightturing-machines

Round-eight complex network in the item-language gate class.

There exist a time bound TTT, a complex-network interface

J:Prop8IfaceH 12 869 228 T 576 hcxJ:\mathrm{Prop8IfaceH}\,12\,869\,228\,T\,576\,h^{\mathrm{cx}}J:Prop8IfaceH12869228T576hcx

and a gate budget AAA such that JJJ lies in the item-language gate class GClassH J A\mathrm{GClassH}\,J\,AGClassHJA, where hcx=Jain.cxR8h^{\mathrm{cx}}=\mathrm{Jain.cxR8}hcx=Jain.cxR8 is Jain's round-eight complex histogram (signed reclaim and completed-core sharing; width mc=576m_c=576mc​=576, role count Wc=12 869 228W_c=12\,869\,228Wc​=12869228, rank sum sc=7 410 813 248s_c=7\,410\,813\,248sc​=7410813248).

This is the round-eight counterpart of the proved round-six node

IntMul.Kappa.R6.Cx.cxNetR6G:∃T,  ∃J:Prop8IfaceH 207387136 T 576 Jain.cxR6,  ∃A,  GClassH J A.\mathrm{IntMul.Kappa.R6.Cx.cxNetR6G}: \exists T,\;\exists J:\mathrm{Prop8IfaceH}\,207387136\,T\,576\,\mathrm{Jain.cxR6},\;\exists A,\;\mathrm{GClassH}\,J\,A.IntMul.Kappa.R6.Cx.cxNetR6G:∃T,∃J:Prop8IfaceH207387136T576Jain.cxR6,∃A,GClassHJA.

Together with BitNetMomStmtG for Jain.bitR8 and the parametric Proposition 14 (P14NeedG / p14NeedG_all), it is the complex-network hypothesis of kappa_finalG_at at the round-eight constants, and therefore a leaf of jain_round8_framework.

Jain lists as proof interfaces (assumed, not machine-checked in the certificate repo): the alternating normal form for residuals, binary address adapters for exterior children of the sharing, and stage two as the complement time-reversal of stage one.

Preamble
import Definitions.Def_IntMul_Kappa_RG_Defs
import Definitions.Def_IntMul_KappaJainData

set_option autoImplicit false
set_option relaxedAutoImplicit false
Formal statement
namespace IntMul.Kappa.R8

open IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx IntMul.Kappa.R6.IL3H

/-- Round-eight complex interchange (signed reclaim, completed-core sharing) in the gate class. -/
theorem cxNetR8G :
    ∃ T, ∃ J : Prop8IfaceH 12869228 T 576 Jain.cxR8, ∃ A, GClassH J A := by
  sorry

end IntMul.Kappa.R8
Source
S. Jain, integer-mult-kappa, https://github.com/Swapnil-jain/integer-mult-kappa/tree/5868dc701a9bec375c9dc5391d992ab3b8c35f3f — README 'Round eight' (complex side: signed reclaim, completed-core sharing; W=12869228, m=576), lean/Round8.lean (cxHist), independent/round8-coreshare/, independent/round8-complex-gate/; interface shape from Prove2me IntMul.Kappa.R6.Cx.cxNetR6G and Def_IntMul_Kappa_RG_Defs (Prop8IfaceH, GClassH); conditional on OpenAI manuscript and Colkitt framework, plus icekylinx normal-form interfaces (PRs #24, #104)

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me