Prove2Me

Round-six network data, CxNetDataS2_14

Definition
IntMul_Kappa_R6_Data_CxNetDataS2_14

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

complexity-theoryinteger-multiplicationkappa-improvement

Data bundle IntMul_Kappa_R6_Data_CxNetDataS2_14 of the round-six κ-improvement development: literal network data from the Lean module Solutions.R6CxNetDataS2_14 (S2_14), 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 14 of stage 2. -/
def S2_14 : 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 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 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/R6CxNetDataS2_14.lean (generated data).

View graph