Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Round-six network data, CxNetDataS1_0

Definition
IntMul_Kappa_R6_Data_CxNetDataS1_0

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Data bundle IntMul_Kappa_R6_Data_CxNetDataS1_0 of the round-six κ-improvement development: literal network data from the Lean module Solutions.R6CxNetDataS1_0 (S1_0), stored as Lean terms (large natural-number literals, BT trees and lists of numbers). These values are not proved correct by themselves; they are the certificates and snapshots that the kernel checks (decide +kernel nodes) evaluate. A value larger than one bundle is split into parts (X_p…) that are reassembled by an exact node/++ expression, so the reassembled term is definitionally the original one.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Definition code
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs24

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
set_option maxRecDepth 100000

namespace IntMul.Kappa.R6.Cx.NetData

open NetBT

/-- Code state snapshot 0 of stage 1. -/
def S1_0 : BT := (.node (.node (.node (.node (.node (.node (.node (.node (.leaf 0x20105000001010500000081050800000b010800000a810400000a810800000a010400000a010200000a010800000981040000098102000009810100000981080000090104000009010200000901010000090100800009010800000881040000088102000008810100000881008000088100400008810800000801040000080102000008010100000801008000080100400008010020000801080000078104000007810200000781010000078100800007810040000781002000078100100007810800000701040000070102000007010100000701008000070100400007010020000701001000070100080007010800000681040000068102000006810100000681008000068100400006810020000681001000068100080006810004000681080000060104000006010200000601010000060100800006010040000601002000060100100006010008000601000400060100020006010800000581040000058102000005810100000581008000058100400005810020000581001000058100080005810004000581000200058100010005810800000501040000050102000005010100000501008000050100400005010020000501001000050100080005010004000501000200050100010005010000800501080000048104000004810200000481010000048100800004810040000481002000048100100004810008000481000400048100020004810001000481000080048100004004810800000401040000040102000004010100000401008000040100400004010020000401001000040100080004010004000401000200040100010004010000800401000040040100002004010800000381040000038102000003810100000381008000038100400003810020000381001000038100080003810004000381000200038100010003810000800381000040038100002003810000100381080000030104000003010200000301010000030100800003010040000301002000030100100003010008000301000400030100020003010001000301000080030100004003010000200301000010030100000803010800000281040000028102000002810100000281008000028100400002810020000281001000028100080002810004000281000200028100010002810000800281000040028100002002810000100281000008028100000402810800000201040000020102000002010100000201008000020100400002010020000201001000020100080002010004000201000200020100010002010000800201000040020100002002010000100201000008020100000402010000020201080000018104000001810200000181010000018100800001810040000181002000018100100001810008000181000400018100020001810001000181000080018100004001810000200181000010018100000801810000040181000002018100000101810800000101040000010102000001010100000101008000010100400001010020000101001000010100080001010004000101000200010100010001010000800101000040010100002001010000100101000008010100000401010000020101000001010100000081010800000081040000008102000000810100000081008000008100400000810020000081001000008100080000810004000081000200008100010000810000800081000040008100002000810000100081000008008100000400810000020081000001008100000080810000004081) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x3fffffc0002fffffc00037ffffc0003bffffc0003dffffc0003effffc0003f7fffc0003fbfffc0003fdfffc0003fefffc0003ff7ffc0003ffbffc0003ffdffc0003ffeffc0003fff7fc0003fffbfc0003fffdfc0003fffefc0003ffff7c0003ffffbc0003ffffdc0003ffffec0003fffff40003fffff800000000000000000000000000000000000000000000000000000000000000000000000000000000))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))))) (.node (.node (.node (.node (.node (.leaf 0x4000619000200061908000005990400000599020000059901000005990080000599004000059900200005990010000599000800059900040005990002000599000100059908000005190400000519020000051901000005190080000519004000051900200005190010000519000800051900040005190002000519000100051900008005190800000499040000049902000004990100000499008000049900400004990020000499001000049900080004990004000499000200049900010004990000800499000040049908000004190400000419020000041901000004190080000419004000041900200004190010000419000800041900040004190002000419000100041900008004190000400419000020041908000003990400000399020000039901000003990080000399004000039900200003990010000399000800039900040003990002000399000100039900008003990000400399000020039900001003990800000b150800000a950400000a950800000a150400000a150200000a150800000995040000099502000009950100000995080000091504000009150200000915010000091500800009150800000895040000089502000008950100000895008000089500400008950800000815040000081502000008150100000815008000081500400008150020000815080000079504000007950200000795010000079500800007950040000795002000079500100007950800000715040000071502000007150100000715008000071500400007150020000715001000071500080007150800000695040000069502000006950100000695008000069500400006950020000695001000069500080006950004000695080000061504000006150200000615010000061500800006150040000615002000061500100006150008000615000400061500020006150800000595040000059502000005950100000595008000059500400005950020000595001000059500080005950004000595000200059500010005950800000515040000051502000005150100000515008000051500400005150020000515001000051500080005150004000515000200051500010005150000800515080000049504000004950200000495010000049500800004950040000495002000049500100004950008000495000400049500020004950001000495000080049500004004950800000415040000041502000004150100000415008000041500400004150020000415001000041500080004150004000415000200041500010004150000800415000040041500002004150800000395040000039502000003950100000395008000039500400003950020000395001000039500080003950004000395000200039500010003950000800395000040039500002003950000100395080000031504000003150200000315010000031500800003150040000315002000031500100003150008000315000400031500020003150001000315000080031500004003150000200315000010031500000803150800000b110800000a910400000a910800000a110400000a110200000a110800000991040000099102000009910100000991080000091104000009110200000911010000091100800009110800000891040000089102000008910100000891008000089100400008910800000811040000081102000008110100000811008000081100400008110020000811080000079104000007910200000791) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))))) (.node (.node (.node (.node (.node (.node (.leaf 0x100040d000080040d000040040d000020040d080000038d040000038d020000038d010000038d008000038d004000038d002000038d001000038d000800038d000400038d000200038d000100038d000080038d000040038d000020038d000010038d080000030d040000030d020000030d010000030d008000030d004000030d002000030d001000030d000800030d000400030d000200030d000100030d000080030d000040030d000020030d000010030d000008030d080000028d040000028d020000028d010000028d008000028d004000028d002000028d001000028d000800028d000400028d000200028d000100028d000080028d000040028d000020028d000010028d000008028d000004028d080000020d040000020d020000020d010000020d008000020d004000020d002000020d001000020d000800020d000400020d000200020d000100020d000080020d000040020d000020020d000010020d000008020d000004020d000002020d0800000b090800000a890400000a890800000a090400000a090200000a0908000009890400000989020000098901000009890800000909040000090902000009090100000909008000090908000008890400000889020000088901000008890080000889004000088908000008090400000809020000080901000008090080000809004000080900200008090800000789040000078902000007890100000789008000078900400007890020000789001000078908000007090400000709020000070901000007090080000709004000070900200007090010000709000800070908000006890400000689020000068901000006890080000689004000068900200006890010000689000800068900040006890800000609040000060902000006090100000609008000060900400006090020000609001000060900080006090004000609000200060908000005890400000589020000058901000005890080000589004000058900200005890010000589000800058900040005890002000589000100058908000005090400000509020000050901000005090080000509004000050900200005090010000509000800050900040005090002000509000100050900008005090800000489040000048902000004890100000489008000048900400004890020000489001000048900080004890004000489000200048900010004890000800489000040048908000004090400000409020000040901000004090080000409004000040900200004090010000409000800040900040004090002000409000100040900008004090000400409000020040908000003890400000389020000038901000003890080000389004000038900200003890010000389000800038900040003890002000389000100038900008003890000400389000020038900001003890800000309040000030902000003090100000309008000030900400003090020000309001000030900080003090004000309000200030900010003090000800309000040030900002003090000100309000008030908000002890400000289020000028901000002890080000289004000028900200002890010000289000800028900040002890002000289000100028900008002890000400289000020028900001002890000080289000004028908000002090400000209020000020901000002090080000209004000020900200002090010000209000800020900040002090002000209) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))))) (.node (.node (.node (.node (.node (.leaf 0x20000092d010000092d008000092d08000008ad04000008ad02000008ad01000008ad00800008ad00400008ad080000082d040000082d020000082d010000082d008000082d004000082d002000082d08000007ad04000007ad02000007ad01000007ad00800007ad00400007ad00200007ad00100007ad080000072d040000072d020000072d010000072d008000072d004000072d002000072d001000072d000800072d08000006ad04000006ad02000006ad01000006ad00800006ad00400006ad00200006ad00100006ad00080006ad00040006ad080000062d040000062d020000062d010000062d008000062d004000062d002000062d001000062d000800062d000400062d000200062d0800000b290800000aa90400000aa90800000a290400000a290200000a2908000009a904000009a902000009a901000009a90800000929040000092902000009290100000929008000092908000008a904000008a902000008a901000008a900800008a900400008a9080000082904000008290200000829010000082900800008290040000829002000082908000007a904000007a902000007a901000007a900800007a900400007a900200007a900100007a908000007290400000729020000072901000007290080000729004000072900200007290010000729000800072908000006a904000006a902000006a901000006a900800006a900400006a900200006a900100006a900080006a900040006a90800000629040000062902000006290100000629008000062900400006290020000629001000062900080006290004000629000200062908000005a904000005a902000005a901000005a900800005a900400005a900200005a900100005a900080005a900040005a900020005a900010005a90800000b250800000aa50400000aa50800000a250400000a250200000a2508000009a504000009a502000009a501000009a50800000925040000092502000009250100000925008000092508000008a504000008a502000008a501000008a500800008a500400008a5080000082504000008250200000825010000082500800008250040000825002000082508000007a504000007a502000007a501000007a500800007a500400007a500200007a500100007a508000007250400000725020000072501000007250080000725004000072500200007250010000725000800072508000006a504000006a502000006a501000006a500800006a500400006a500200006a500100006a500080006a500040006a50800000625040000062502000006250100000625008000062500400006250020000625001000062500080006250004000625000200062508000005a504000005a502000005a501000005a500800005a500400005a500200005a500100005a500080005a500040005a500020005a500010005a508000005250400000525020000052501000005250080000525004000052500200005250010000525000800052500040005250002000525000100052500008005250800000b210800000aa10400000aa10800000a210400000a210200000a2108000009a104000009a102000009a101000009a10800000921040000092102000009210100000921008000092108000008a104000008a102000008a101000008a100800008a100400008a1080000082104000008210200000821010000082100800008210040000821002000082108000007a104000007a102000007a101000007a100800007a1) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))))))) (.node (.node (.node (.node (.node (.node (.node (.leaf 0x10002090000800209000040020900002002090000100209000008020900000402090000020209080000018904000001890200000189010000018900800001890040000189002000018900100001890008000189000400018900020001890001000189000080018900004001890000200189000010018900000801890000040189000002018900000101890800000b050800000a850400000a850800000a050400000a050200000a05080000098504000009850200000985010000098508000009050400000905020000090501000009050080000905080000088504000008850200000885010000088500800008850040000885080000080504000008050200000805010000080500800008050040000805002000080508000007850400000785020000078501000007850080000785004000078500200007850010000785080000070504000007050200000705010000070500800007050040000705002000070500100007050008000705080000068504000006850200000685010000068500800006850040000685002000068500100006850008000685000400068508000006050400000605020000060501000006050080000605004000060500200006050010000605000800060500040006050002000605080000058504000005850200000585010000058500800005850040000585002000058500100005850008000585000400058500020005850001000585080000050504000005050200000505010000050500800005050040000505002000050500100005050008000505000400050500020005050001000505000080050508000004850400000485020000048501000004850080000485004000048500200004850010000485000800048500040004850002000485000100048500008004850000400485080000040504000004050200000405010000040500800004050040000405002000040500100004050008000405000400040500020004050001000405000080040500004004050000200405080000038504000003850200000385010000038500800003850040000385002000038500100003850008000385000400038500020003850001000385000080038500004003850000200385000010038508000003050400000305020000030501000003050080000305004000030500200003050010000305000800030500040003050002000305000100030500008003050000400305000020030500001003050000080305080000028504000002850200000285010000028500800002850040000285002000028500100002850008000285000400028500020002850001000285000080028500004002850000200285000010028500000802850000040285080000020504000002050200000205010000020500800002050040000205002000020500100002050008000205000400020500020002050001000205000080020500004002050000200205000010020500000802050000040205000002020508000001850400000185020000018501000001850080000185004000018500200001850010000185000800018500040001850002000185000100018500008001850000400185000020018500001001850000080185000004018500000201850000010185080000010504000001050200000105010000010500800001050040000105002000010500100001050008000105000400010500020001050001000105000080010500004001050000200105000010010500000801050000040105) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))))) (.node (.node (.node (.node (.node (.leaf 0x400007a100200007a100100007a108000007210400000721020000072101000007210080000721004000072100200007210010000721000800072108000006a104000006a102000006a101000006a100800006a100400006a100200006a100100006a100080006a100040006a10800000621040000062102000006210100000621008000062100400006210020000621001000062100080006210004000621000200062108000005a104000005a102000005a101000005a100800005a100400005a100200005a100100005a100080005a100040005a100020005a100010005a1080000052104000005210200000521010000052100800005210040000521002000052100100005210008000521000400052100020005210001000521000080052108000004a104000004a102000004a101000004a100800004a100400004a100200004a100100004a100080004a100040004a100020004a100010004a100008004a100004004a10800000b1d0800000a9d0400000a9d0800000a1d0400000a1d0200000a1d080000099d040000099d020000099d010000099d080000091d040000091d020000091d010000091d008000091d080000089d040000089d020000089d010000089d008000089d004000089d080000081d040000081d020000081d010000081d008000081d004000081d002000081d080000079d040000079d020000079d010000079d008000079d004000079d002000079d001000079d080000071d040000071d020000071d010000071d008000071d004000071d002000071d001000071d000800071d080000069d040000069d020000069d010000069d008000069d004000069d002000069d001000069d000800069d000400069d080000061d040000061d020000061d010000061d008000061d004000061d002000061d001000061d000800061d000400061d000200061d080000059d040000059d020000059d010000059d008000059d004000059d002000059d001000059d000800059d000400059d000200059d000100059d080000051d040000051d020000051d010000051d008000051d004000051d002000051d001000051d000800051d000400051d000200051d000100051d000080051d080000049d040000049d020000049d010000049d008000049d004000049d002000049d001000049d000800049d000400049d000200049d000100049d000080049d000040049d080000041d040000041d020000041d010000041d008000041d004000041d002000041d001000041d000800041d000400041d000200041d000100041d000080041d000040041d000020041d0800000b190800000a990400000a990800000a190400000a190200000a190800000999040000099902000009990100000999080000091904000009190200000919010000091900800009190800000899040000089902000008990100000899008000089900400008990800000819040000081902000008190100000819008000081900400008190020000819080000079904000007990200000799010000079900800007990040000799002000079900100007990800000719040000071902000007190100000719008000071900400007190020000719001000071900080007190800000699040000069902000006990100000699008000069900400006990020000699001000069900080006990004000699080000061904000006190200000619010000061900800006190040000619002000061900100006190008000619) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))))) (.node (.node (.node (.node (.node (.node (.leaf 0x10000079100800007910040000791002000079100100007910800000711040000071102000007110100000711008000071100400007110020000711001000071100080007110800000691040000069102000006910100000691008000069100400006910020000691001000069100080006910004000691080000061104000006110200000611010000061100800006110040000611002000061100100006110008000611000400061100020006110800000591040000059102000005910100000591008000059100400005910020000591001000059100080005910004000591000200059100010005910800000511040000051102000005110100000511008000051100400005110020000511001000051100080005110004000511000200051100010005110000800511080000049104000004910200000491010000049100800004910040000491002000049100100004910008000491000400049100020004910001000491000080049100004004910800000411040000041102000004110100000411008000041100400004110020000411001000041100080004110004000411000200041100010004110000800411000040041100002004110800000391040000039102000003910100000391008000039100400003910020000391001000039100080003910004000391000200039100010003910000800391000040039100002003910000100391080000031104000003110200000311010000031100800003110040000311002000031100100003110008000311000400031100020003110001000311000080031100004003110000200311000010031100000803110800000291040000029102000002910100000291008000029100400002910020000291001000029100080002910004000291000200029100010002910000800291000040029100002002910000100291000008029100000402910800000b0d0800000a8d0400000a8d0800000a0d0400000a0d0200000a0d080000098d040000098d020000098d010000098d080000090d040000090d020000090d010000090d008000090d080000088d040000088d020000088d010000088d008000088d004000088d080000080d040000080d020000080d010000080d008000080d004000080d002000080d080000078d040000078d020000078d010000078d008000078d004000078d002000078d001000078d080000070d040000070d020000070d010000070d008000070d004000070d002000070d001000070d000800070d080000068d040000068d020000068d010000068d008000068d004000068d002000068d001000068d000800068d000400068d080000060d040000060d020000060d010000060d008000060d004000060d002000060d001000060d000800060d000400060d000200060d080000058d040000058d020000058d010000058d008000058d004000058d002000058d001000058d000800058d000400058d000200058d000100058d080000050d040000050d020000050d010000050d008000050d004000050d002000050d001000050d000800050d000400050d000200050d000100050d000080050d080000048d040000048d020000048d010000048d008000048d004000048d002000048d001000048d000800048d000400048d000200048d000100048d000080048d000040048d080000040d040000040d020000040d010000040d008000040d004000040d002000040d001000040d000800040d000400040d000200040d) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))))) (.node (.node (.node (.node (.node (.leaf 0x800000b550800000b510800000ad10400000ad10800000b4d0800000acd0400000acd0800000a4d0400000a4d0200000a4d0800000b490800000ac90400000ac90800000a490400000a490200000a4908000009c904000009c902000009c901000009c90800000b450800000ac50400000ac50800000a450400000a450200000a4508000009c504000009c502000009c501000009c5080000094504000009450200000945010000094500800009450800000b410800000ac10400000ac10800000a410400000a410200000a4108000009c104000009c102000009c101000009c10800000941040000094102000009410100000941008000094108000008c104000008c102000008c101000008c100800008c100400008c10800000b3d0800000abd0400000abd0800000a3d0400000a3d0200000a3d08000009bd04000009bd02000009bd01000009bd080000093d040000093d020000093d010000093d008000093d08000008bd04000008bd02000008bd01000008bd00800008bd00400008bd080000083d040000083d020000083d010000083d008000083d004000083d002000083d0800000b390800000ab90400000ab90800000a390400000a390200000a3908000009b904000009b902000009b901000009b90800000939040000093902000009390100000939008000093908000008b904000008b902000008b901000008b900800008b900400008b9080000083904000008390200000839010000083900800008390040000839002000083908000007b904000007b902000007b901000007b900800007b900400007b900200007b900100007b90800000b350800000ab50400000ab50800000a350400000a350200000a3508000009b504000009b502000009b501000009b50800000935040000093502000009350100000935008000093508000008b504000008b502000008b501000008b500800008b500400008b5080000083504000008350200000835010000083500800008350040000835002000083508000007b504000007b502000007b501000007b500800007b500400007b500200007b500100007b50800000735040000073502000007350100000735008000073500400007350020000735001000073500080007350800000b310800000ab10400000ab10800000a310400000a310200000a3108000009b104000009b102000009b101000009b10800000931040000093102000009310100000931008000093108000008b104000008b102000008b101000008b100800008b100400008b1080000083104000008310200000831010000083100800008310040000831002000083108000007b104000007b102000007b101000007b100800007b100400007b100200007b100100007b108000007310400000731020000073101000007310080000731004000073100200007310010000731000800073108000006b104000006b102000006b101000006b100800006b100400006b100200006b100100006b100080006b100040006b10800000b2d0800000aad0400000aad0800000a2d0400000a2d0200000a2d08000009ad04000009ad02000009ad01000009ad080000092d040000092d) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))))) (.node (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))) (.node (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0))) (.node (.node (.leaf 0x0) (.leaf 0x0)) (.node (.leaf 0x0) (.leaf 0x0)))))))))

end IntMul.Kappa.R6.Cx.NetData
Source
S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean module Solutions/R6CxNetDataS1_0.lean (generated data).

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