diff --git a/research/bit-two-relation-any-registers/CERTIFICATE.json b/research/bit-two-relation-any-registers/CERTIFICATE.json new file mode 100644 index 0000000000..50527cb795 --- /dev/null +++ b/research/bit-two-relation-any-registers/CERTIFICATE.json @@ -0,0 +1 @@ +{"schema_version":1,"encoding":"matrix bit 4*i+j is entry (i,j); subspace bit v marks binary vector v","records":[[2,4,6,3],[2,8,10,3],[2,12,14,3],[2,16,18,9],[2,64,66,3],[2,68,70,3],[2,80,82,9],[2,84,86,9],[2,128,130,3],[2,136,138,3],[2,144,146,9],[2,152,154,9],[2,192,194,3],[2,204,206,3],[2,208,210,9],[2,220,222,9],[2,256,258,17],[2,272,274,17],[2,336,338,255],[2,512,514,3],[2,516,518,3],[2,768,770,9],[2,784,786,9],[2,852,854,9],[2,2048,2050,3],[2,2056,2058,3],[2,2060,2062,3],[2,2176,2178,3],[2,2184,2186,3],[2,2240,2242,3],[2,2252,2254,3],[2,2304,2306,17],[2,2312,2314,17],[2,2456,2458,17],[2,2512,2514,255],[2,2560,2562,3],[2,2572,2574,3],[2,2688,2690,3],[2,2696,2698,3],[2,2816,2818,9],[2,2824,2826,9],[2,2960,2962,9],[2,3036,3038,9],[2,4096,4098,17],[2,4112,4114,17],[2,4240,4242,17],[2,4352,4354,17],[2,4368,4370,17],[2,6400,6402,17],[2,6544,6546,17],[2,8192,8194,3],[2,8200,8202,3],[2,8704,8706,3],[2,10752,10754,3],[2,10760,10762,3],[2,12288,12290,9],[2,12304,12306,9],[2,12440,12442,9],[2,13056,13058,9],[2,13072,13074,9],[2,15104,15106,9],[2,15256,15258,9],[2,16384,16386,3],[2,16388,16390,3],[2,16396,16398,3],[2,16448,16450,3],[2,16452,16454,3],[2,16576,16578,3],[2,16588,16590,3],[2,20480,20482,257],[2,20484,20486,257],[2,20564,20566,257],[2,20688,20690,3855],[2,20736,20738,257],[2,20816,20818,257],[2,22796,22798,4097],[2,23004,23006,4097],[2,24576,24578,3],[2,24588,24590,3],[2,24640,24642,3],[2,24644,24646,3],[2,25088,25090,3],[2,25092,25094,3],[2,27328,27330,3],[2,27340,27342,3],[2,28672,28674,9],[2,28676,28678,9],[2,28752,28754,9],[2,28892,28894,9],[2,29440,29442,9],[2,29524,29526,9],[2,31500,31502,9],[2,31696,31698,9],[4,8,12,3],[4,10,14,3],[4,16,20,5],[4,64,68,3],[4,66,70,3],[4,80,84,5],[4,128,132,3],[4,136,140,3],[4,138,142,3],[4,144,148,5],[4,152,156,5],[4,192,196,3],[4,202,206,3],[4,208,212,5],[4,216,220,5],[4,256,260,5],[4,272,276,5],[4,336,340,5],[4,512,516,3],[4,514,518,3],[4,768,772,33],[4,770,774,33],[4,784,788,255],[4,850,854,33],[4,2048,2052,3],[4,2056,2060,3],[4,2176,2180,3],[4,2184,2188,3],[4,2240,2244,3],[4,2248,2252,3],[4,2304,2308,5],[4,2312,2316,5],[4,2456,2460,5],[4,2512,2516,5],[4,2560,2564,3],[4,2570,2574,3],[4,2688,2692,3],[4,2698,2702,3],[4,2816,2820,33],[4,2826,2830,33],[4,2960,2964,255],[4,3034,3038,33],[4,4096,4100,5],[4,4112,4116,5],[4,4240,4244,5],[4,4352,4356,5],[4,4368,4372,5],[4,6400,6404,5],[4,6544,6548,5],[4,8192,8196,3],[4,8194,8198,3],[4,8202,8206,3],[4,8704,8708,3],[4,8706,8710,3],[4,10752,10756,3],[4,10762,10766,3],[4,12288,12292,257],[4,12290,12294,257],[4,12304,12308,257],[4,12442,12446,1025],[4,13058,13062,257],[4,13072,13076,257],[4,15104,15108,1025],[4,15258,15262,1025],[4,16384,16388,3],[4,16392,16396,3],[4,16448,16452,3],[4,16576,16580,3],[4,16584,16588,3],[4,20480,20484,5],[4,20560,20564,5],[4,20688,20692,5],[4,20736,20740,5],[4,20816,20820,5],[4,22792,22796,5],[4,23000,23004,5],[4,24576,24580,3],[4,24586,24590,3],[4,24640,24644,3],[4,24642,24646,3],[4,25088,25092,3],[4,25090,25094,3],[4,27328,27332,3],[4,27338,27342,3],[4,28672,28676,33],[4,28674,28678,33],[4,28752,28756,33],[4,28890,28894,33],[4,29440,29444,33],[4,29522,29526,33],[4,31498,31502,33],[4,31696,31700,33],[6,8,14,3],[6,10,12,3],[6,16,22,9],[6,64,70,3],[6,66,68,3],[6,80,86,9],[6,82,84,9],[6,128,134,3],[6,136,142,3],[6,138,140,3],[6,144,150,9],[6,152,158,9],[6,192,198,3],[6,200,206,3],[6,208,214,9],[6,218,220,9],[6,256,262,33],[6,272,278,65],[6,336,342,33],[6,512,518,3],[6,514,516,3],[6,768,774,9],[6,770,772,9],[6,784,790,9],[6,848,854,9],[6,2048,2054,3],[6,2056,2062,3],[6,2058,2060,3],[6,2176,2182,3],[6,2184,2190,3],[6,2240,2246,3],[6,2250,2252,3],[6,2304,2310,33],[6,2312,2318,33],[6,2456,2462,65],[6,2512,2518,33],[6,2560,2566,3],[6,2568,2574,3],[6,2688,2694,3],[6,2698,2700,3],[6,2816,2822,9],[6,2826,2828,9],[6,2960,2966,9],[6,3032,3038,9],[6,4096,4102,65],[6,4112,4118,65],[6,4240,4246,65],[6,4352,4358,65],[6,4368,4374,65],[6,6400,6406,65],[6,6544,6550,65],[6,8192,8198,3],[6,8194,8196,3],[6,8202,8204,3],[6,8704,8710,3],[6,8706,8708,3],[6,10752,10758,3],[6,10762,10764,3],[6,12288,12294,9],[6,12290,12292,9],[6,12304,12310,9],[6,12442,12444,9],[6,13058,13060,9],[6,13072,13078,9],[6,15104,15110,9],[6,15258,15260,9],[6,16384,16390,3],[6,16386,16388,3],[6,16394,16396,3],[6,16448,16454,3],[6,16450,16452,3],[6,16576,16582,3],[6,16586,16588,3],[6,20480,20486,33],[6,20482,20484,33],[6,20562,20564,33],[6,20688,20694,33],[6,20736,20742,33],[6,20816,20822,33],[6,22794,22796,33],[6,23002,23004,33],[6,24576,24582,3],[6,24584,24590,3],[6,24640,24646,3],[6,25088,25094,3],[6,27328,27334,3],[6,27336,27342,3],[6,28672,28678,9],[6,28752,28758,9],[6,28888,28894,9],[6,29440,29446,9],[6,29520,29526,9],[6,31496,31502,9],[6,31696,31702,9],[8,16,24,5],[8,64,72,3],[8,68,76,3],[8,70,78,3],[8,80,88,5],[8,84,92,5],[8,128,136,3],[8,130,138,3],[8,144,152,5],[8,192,200,3],[8,198,206,3],[8,208,216,5],[8,212,220,5],[8,256,264,5],[8,272,280,5],[8,336,344,5],[8,512,520,3],[8,514,522,3],[8,518,526,3],[8,768,776,17],[8,770,778,17],[8,784,792,17],[8,854,862,65],[8,2048,2056,3],[8,2052,2060,3],[8,2176,2184,3],[8,2240,2248,3],[8,2244,2252,3],[8,2304,2312,5],[8,2448,2456,5],[8,2512,2520,5],[8,2560,2568,3],[8,2566,2574,3],[8,2688,2696,3],[8,2690,2698,3],[8,2816,2824,17],[8,2818,2826,17],[8,2960,2968,17],[8,3030,3038,65],[8,4096,4104,5],[8,4112,4120,5],[8,4240,4248,5],[8,4352,4360,5],[8,4368,4376,5],[8,6400,6408,5],[8,6544,6552,5],[8,8192,8200,3],[8,8194,8202,3],[8,8704,8712,3],[8,8706,8714,3],[8,10752,10760,3],[8,10754,10762,3],[8,12288,12296,17],[8,12290,12298,17],[8,12304,12312,17],[8,12434,12442,17],[8,13058,13066,17],[8,13072,13080,17],[8,15104,15112,17],[8,15250,15258,17],[8,16384,16392,3],[8,16388,16396,3],[8,16448,16456,3],[8,16452,16460,3],[8,16576,16584,3],[8,16580,16588,3],[8,20480,20488,5],[8,20484,20492,5],[8,20564,20572,5],[8,20688,20696,5],[8,20736,20744,5],[8,20816,20824,5],[8,22788,22796,5],[8,22996,23004,5],[8,24576,24584,3],[8,24582,24590,3],[8,24640,24648,3],[8,24646,24654,3],[8,25088,25096,3],[8,25094,25102,3],[8,27328,27336,3],[8,27334,27342,3],[8,28672,28680,65],[8,28678,28686,65],[8,28752,28760,65],[8,28886,28894,65],[8,29440,29448,65],[8,29526,29534,65],[8,31494,31502,65],[8,31696,31704,65],[10,16,26,9],[10,64,74,3],[10,68,78,3],[10,70,76,3],[10,80,90,9],[10,84,94,9],[10,128,138,3],[10,130,136,3],[10,144,154,9],[10,146,152,9],[10,192,202,3],[10,196,206,3],[10,208,218,9],[10,214,220,9],[10,256,266,17],[10,272,282,17],[10,336,346,129],[10,512,522,3],[10,514,520,3],[10,518,524,3],[10,768,778,9],[10,770,776,9],[10,784,794,9],[10,854,860,9],[10,2048,2058,3],[10,2050,2056,3],[10,2054,2060,3],[10,2176,2186,3],[10,2178,2184,3],[10,2240,2250,3],[10,2246,2252,3],[10,2304,2314,17],[10,2306,2312,17],[10,2450,2456,17],[10,2512,2522,129],[10,2560,2570,3],[10,2564,2574,3],[10,2688,2698,3],[10,2816,2826,9],[10,2960,2970,9],[10,3028,3038,9],[10,4096,4106,17],[10,4112,4122,17],[10,4240,4250,17],[10,4352,4362,17],[10,4368,4378,17],[10,6400,6410,17],[10,6544,6554,17],[10,8192,8202,3],[10,8194,8200,3],[10,8704,8714,3],[10,8706,8712,3],[10,10752,10762,3],[10,12288,12298,9],[10,12290,12296,9],[10,12304,12314,9],[10,12432,12442,9],[10,13058,13064,9],[10,13072,13082,9],[10,15104,15114,9],[10,15248,15258,9],[10,16384,16394,3],[10,16388,16398,3],[10,16390,16396,3],[10,16448,16458,3],[10,16452,16462,3],[10,16576,16586,3],[10,16582,16588,3],[10,20480,20490,129],[10,20484,20494,129],[10,20564,20574,129],[10,20688,20698,129],[10,20736,20746,129],[10,20816,20826,129],[10,22790,22796,129],[10,22998,23004,129],[10,24576,24586,3],[10,24580,24590,3],[10,24640,24650,3],[10,24646,24652,3],[10,25088,25098,3],[10,25094,25100,3],[10,27328,27338,3],[10,27332,27342,3],[10,28672,28682,9],[10,28678,28684,9],[10,28752,28762,9],[10,28884,28894,9],[10,29440,29450,9],[10,29526,29532,9],[10,31492,31502,9],[10,31696,31706,9],[12,16,28,5],[12,64,76,3],[12,68,72,3],[12,70,74,3],[12,80,92,5],[12,84,88,5],[12,128,140,3],[12,132,136,3],[12,134,138,3],[12,144,156,5],[12,148,152,5],[12,192,204,3],[12,194,206,3],[12,208,220,5],[12,256,268,5],[12,272,284,5],[12,336,348,5],[12,512,524,3],[12,514,526,3],[12,518,522,3],[12,768,780,33],[12,770,782,33],[12,784,796,129],[12,854,858,33],[12,2048,2060,3],[12,2052,2056,3],[12,2176,2188,3],[12,2180,2184,3],[12,2240,2252,3],[12,2304,2316,5],[12,2308,2312,5],[12,2452,2456,5],[12,2512,2524,5],[12,2560,2572,3],[12,2562,2574,3],[12,2688,2700,3],[12,2694,2698,3],[12,2816,2828,33],[12,2822,2826,33],[12,2960,2972,129],[12,3026,3038,33],[12,4096,4108,5],[12,4112,4124,5],[12,4240,4252,5],[12,4352,4364,5],[12,4368,4380,5],[12,6400,6412,5],[12,6544,6556,5],[12,8192,8204,3],[12,8194,8206,3],[12,8198,8202,3],[12,8704,8716,3],[12,8706,8718,3],[12,10752,10764,3],[12,10758,10762,3],[12,12288,12300,129],[12,12290,12302,129],[12,12304,12316,129],[12,12438,12442,129],[12,13058,13070,129],[12,13072,13084,129],[12,15104,15116,129],[12,15254,15258,129],[12,16384,16396,3],[12,16388,16392,3],[12,16448,16460,3],[12,16452,16456,3],[12,16576,16588,3],[12,20480,20492,5],[12,20484,20488,5],[12,20564,20568,5],[12,20688,20700,5],[12,20736,20748,5],[12,20816,20828,5],[12,22784,22796,5],[12,22992,23004,5],[12,24576,24588,3],[12,24578,24590,3],[12,24640,24652,3],[12,24646,24650,3],[12,25088,25100,3],[12,25094,25098,3],[12,27328,27340,3],[12,27330,27342,3],[12,28672,28684,33],[12,28678,28682,33],[12,28752,28764,33],[12,28882,28894,33],[12,29440,29452,33],[12,29526,29530,33],[12,31490,31502,33],[12,31696,31708,33],[14,16,30,9],[14,64,78,3],[14,68,74,3],[14,70,72,3],[14,80,94,9],[14,84,90,9],[14,128,142,3],[14,132,138,3],[14,134,136,3],[14,144,158,9],[14,150,152,9],[14,192,206,3],[14,208,222,9],[14,210,220,9],[14,256,270,33],[14,272,286,65],[14,336,350,33],[14,512,526,3],[14,514,524,3],[14,518,520,3],[14,768,782,9],[14,770,780,9],[14,784,798,9],[14,854,856,9],[14,2048,2062,3],[14,2050,2060,3],[14,2054,2056,3],[14,2176,2190,3],[14,2182,2184,3],[14,2240,2254,3],[14,2242,2252,3],[14,2304,2318,33],[14,2310,2312,33],[14,2454,2456,65],[14,2512,2526,33],[14,2560,2574,3],[14,2688,2702,3],[14,2692,2698,3],[14,2816,2830,9],[14,2820,2826,9],[14,2960,2974,9],[14,3024,3038,9],[14,4096,4110,65],[14,4112,4126,65],[14,4240,4254,65],[14,4352,4366,65],[14,4368,4382,65],[14,6400,6414,65],[14,6544,6558,65],[14,8192,8206,3],[14,8194,8204,3],[14,8196,8202,3],[14,8704,8718,3],[14,8706,8716,3],[14,10752,10766,3],[14,10756,10762,3],[14,12288,12302,9],[14,12290,12300,9],[14,12304,12318,9],[14,12436,12442,9],[14,13058,13068,9],[14,13072,13086,9],[14,15104,15118,9],[14,15252,15258,9],[14,16384,16398,3],[14,16386,16396,3],[14,16388,16394,3],[14,16448,16462,3],[14,16452,16458,3],[14,16576,16590,3],[14,16578,16588,3],[14,20480,20494,33],[14,20484,20490,33],[14,20564,20570,33],[14,20688,20702,33],[14,20736,20750,33],[14,20816,20830,33],[14,22786,22796,33],[14,22994,23004,33],[14,24576,24590,3],[14,24640,24654,3],[14,24646,24648,3],[14,25088,25102,3],[14,25094,25096,3],[14,27328,27342,3],[14,28672,28686,9],[14,28678,28680,9],[14,28752,28766,9],[14,28880,28894,9],[14,29440,29454,9],[14,29526,29528,9],[14,31488,31502,9],[14,31696,31710,9],[16,64,80,5],[16,68,84,5],[16,70,86,9],[16,128,144,5],[16,136,152,5],[16,138,154,9],[16,192,208,5],[16,204,220,5],[16,206,222,9],[16,256,272,5],[16,320,336,5],[16,512,528,17],[16,514,530,17],[16,518,534,255],[16,768,784,9],[16,770,786,9],[16,838,854,9],[16,2048,2064,5],[16,2056,2072,5],[16,2060,2076,5],[16,2176,2192,5],[16,2184,2200,5],[16,2240,2256,5],[16,2252,2268,5],[16,2304,2320,5],[16,2312,2328,5],[16,2440,2456,5],[16,2496,2512,5],[16,2560,2576,17],[16,2574,2590,255],[16,2688,2704,17],[16,2698,2714,17],[16,2816,2832,9],[16,2826,2842,9],[16,2944,2960,9],[16,3022,3038,9],[16,4096,4112,5],[16,4224,4240,5],[16,4352,4368,5],[16,6400,6416,5],[16,6528,6544,5],[16,8192,8208,17],[16,8194,8210,17],[16,8202,8218,17],[16,8704,8720,17],[16,8706,8722,17],[16,10752,10768,17],[16,10762,10778,17],[16,12288,12304,9],[16,12290,12306,9],[16,12426,12442,9],[16,13056,13072,9],[16,13058,13074,9],[16,15104,15120,9],[16,15242,15258,9],[16,16384,16400,5],[16,16388,16404,5],[16,16396,16412,5],[16,16448,16464,5],[16,16452,16468,5],[16,16576,16592,5],[16,16588,16604,5],[16,20480,20496,5],[16,20484,20500,5],[16,20548,20564,5],[16,20672,20688,5],[16,20736,20752,5],[16,20800,20816,5],[16,22796,22812,5],[16,22988,23004,5],[16,24576,24592,257],[16,24590,24606,3855],[16,24640,24656,257],[16,24646,24662,257],[16,25088,25104,257],[16,25094,25110,257],[16,27328,27344,4097],[16,27342,27358,4097],[16,28672,28688,9],[16,28678,28694,9],[16,28736,28752,9],[16,28878,28894,9],[16,29440,29456,9],[16,29510,29526,9],[16,31502,31518,9],[16,31680,31696,9],[18,70,84,9],[18,138,152,9],[18,206,220,9],[18,770,784,9],[18,12290,12304,9],[18,13058,13072,9],[20,64,84,5],[20,68,80,5],[22,70,80,9],[24,128,152,5],[24,136,144,5],[26,138,144,9],[28,192,220,5],[30,206,208,9],[64,128,192,3],[64,136,200,3],[64,138,202,3],[64,142,206,3],[64,144,208,5],[64,152,216,5],[64,156,220,5],[64,256,320,5],[64,272,336,5],[64,512,576,3],[64,514,578,3],[64,518,582,3],[64,768,832,65],[64,770,834,255],[64,784,848,65],[64,790,854,65],[64,2048,2112,3],[64,2056,2120,3],[64,2060,2124,3],[64,2176,2240,3],[64,2184,2248,3],[64,2188,2252,3],[64,2304,2368,5],[64,2312,2376,5],[64,2448,2512,5],[64,2456,2520,5],[64,2560,2624,3],[64,2574,2638,3],[64,2688,2752,3],[64,2698,2762,3],[64,2816,2880,65],[64,2826,2890,255],[64,2960,3024,65],[64,2974,3038,65],[64,4096,4160,5],[64,4112,4176,5],[64,4240,4304,5],[64,4352,4416,5],[64,4368,4432,5],[64,6400,6464,5],[64,6544,6608,5],[64,8192,8256,3],[64,8194,8258,3],[64,8202,8266,3],[64,8704,8768,3],[64,8706,8770,3],[64,10752,10816,3],[64,10762,10826,3],[64,12288,12352,257],[64,12290,12354,257],[64,12304,12368,257],[64,12442,12506,513],[64,13058,13122,257],[64,13072,13136,257],[64,15104,15168,513],[64,15258,15322,513],[64,16384,16448,3],[64,16388,16452,3],[64,16396,16460,3],[64,16512,16576,3],[64,16524,16588,3],[64,20480,20544,5],[64,20484,20548,5],[64,20500,20564,5],[64,20624,20688,5],[64,20736,20800,5],[64,20752,20816,5],[64,22796,22860,5],[64,22940,23004,5],[64,24576,24640,3],[64,24582,24646,3],[64,24590,24654,3],[64,25088,25152,3],[64,25094,25158,3],[64,27264,27328,3],[64,27278,27342,3],[64,28672,28736,65],[64,28678,28742,65],[64,28688,28752,65],[64,28830,28894,65],[64,29440,29504,65],[64,29462,29526,65],[64,31502,31566,65],[64,31632,31696,65],[68,128,196,3],[68,132,192,3],[68,136,204,3],[68,138,206,3],[68,144,212,5],[68,148,208,5],[68,152,220,5],[68,256,324,5],[68,272,340,5],[68,276,336,5],[68,512,580,3],[68,514,582,3],[68,518,578,3],[68,768,836,9],[68,770,838,9],[68,784,852,9],[68,786,854,9],[68,2048,2116,3],[68,2056,2124,3],[68,2060,2120,3],[68,2176,2244,3],[68,2180,2240,3],[68,2184,2252,3],[68,2304,2372,5],[68,2312,2380,5],[68,2452,2512,5],[68,2456,2524,5],[68,2560,2628,3],[68,2574,2634,3],[68,2688,2756,3],[68,2698,2766,3],[68,2816,2884,9],[68,2826,2894,9],[68,2960,3028,9],[68,2970,3038,9],[68,4096,4164,5],[68,4112,4180,5],[68,4240,4308,5],[68,4352,4420,5],[68,4368,4436,5],[68,6400,6468,5],[68,6544,6612,5],[68,8192,8260,3],[68,8194,8262,3],[68,8202,8270,3],[68,8704,8772,3],[68,8706,8774,3],[68,10752,10820,3],[68,10762,10830,3],[68,12288,12356,9],[68,12290,12358,9],[68,12304,12372,9],[68,12442,12510,9],[68,13058,13126,9],[68,13072,13140,9],[68,15104,15172,9],[68,15258,15326,9],[68,16384,16452,3],[68,16388,16448,3],[68,16396,16456,3],[68,16516,16576,3],[68,16520,16588,3],[68,20480,20548,5],[68,20484,20544,5],[68,20496,20564,5],[68,20628,20688,5],[68,20736,20804,5],[68,20756,20816,5],[68,22796,22856,5],[68,22936,23004,5],[68,24576,24644,3],[68,24578,24646,3],[68,24580,24640,3],[68,24590,24650,3],[68,25088,25156,3],[68,25094,25154,3],[68,27268,27328,3],[68,27274,27342,3],[68,28672,28740,9],[68,28678,28738,9],[68,28692,28752,9],[68,28826,28894,9],[68,29440,29508,9],[68,29458,29526,9],[68,31502,31562,9],[68,31636,31696,9],[70,128,198,3],[70,134,192,3],[70,136,206,3],[70,138,204,3],[70,144,214,9],[70,150,208,9],[70,152,222,9],[70,154,220,9],[70,256,326,255],[70,272,342,65],[70,278,336,65],[70,512,582,3],[70,514,580,3],[70,518,576,3],[70,768,838,9],[70,770,836,9],[70,784,854,9],[70,2048,2118,3],[70,2056,2126,3],[70,2060,2122,3],[70,2176,2246,3],[70,2182,2240,3],[70,2184,2254,3],[70,2186,2252,3],[70,2304,2374,129],[70,2312,2382,65],[70,2454,2512,65],[70,2456,2526,65],[70,2560,2630,3],[70,2574,2632,3],[70,2688,2758,3],[70,2698,2764,3],[70,2816,2886,9],[70,2826,2892,9],[70,2960,3030,9],[70,2968,3038,9],[70,4096,4166,65],[70,4112,4182,65],[70,4240,4310,65],[70,4352,4422,65],[70,4368,4438,65],[70,6400,6470,65],[70,6544,6614,65],[70,8192,8262,3],[70,8194,8260,3],[70,8202,8268,3],[70,8704,8774,3],[70,8706,8772,3],[70,10752,10822,3],[70,10762,10828,3],[70,12288,12358,9],[70,12290,12356,9],[70,12304,12374,9],[70,12442,12508,9],[70,13058,13124,9],[70,13072,13142,9],[70,15104,15174,9],[70,15258,15324,9],[70,16384,16454,3],[70,16386,16452,3],[70,16388,16450,3],[70,16390,16448,3],[70,16396,16458,3],[70,16518,16576,3],[70,16522,16588,3],[70,20480,20550,129],[70,20484,20546,129],[70,20498,20564,129],[70,20630,20688,129],[70,20736,20806,129],[70,20758,20816,129],[70,22796,22858,129],[70,22938,23004,129],[70,24576,24646,3],[70,24582,24640,3],[70,24590,24648,3],[70,25088,25158,3],[70,25094,25152,3],[70,27270,27328,3],[70,27272,27342,3],[70,28672,28742,9],[70,28678,28736,9],[70,28694,28752,9],[70,28824,28894,9],[70,29440,29510,9],[70,29456,29526,9],[70,31502,31560,9],[70,31638,31696,9],[72,136,192,3],[72,152,208,5],[72,2184,2240,3],[72,2456,2512,5],[72,16396,16452,3],[72,24590,24646,3],[74,138,192,3],[76,144,220,5],[76,2176,2252,3],[76,16396,16448,3],[78,128,206,3],[78,2960,3038,9],[78,24590,24640,3],[80,128,208,5],[80,136,216,5],[80,138,218,9],[80,140,220,5],[80,144,192,5],[80,152,200,5],[80,158,206,9],[80,256,336,5],[80,272,320,5],[80,512,592,65],[80,514,594,33],[80,518,598,33],[80,768,848,9],[80,770,850,9],[80,774,854,9],[80,784,832,9],[80,2048,2128,5],[80,2056,2136,5],[80,2060,2140,5],[80,2176,2256,5],[80,2184,2264,5],[80,2192,2240,5],[80,2204,2252,5],[80,2304,2384,5],[80,2312,2392,5],[80,2432,2512,5],[80,2456,2504,5],[80,2560,2640,65],[80,2574,2654,33],[80,2688,2768,33],[80,2698,2778,33],[80,2816,2896,9],[80,2826,2906,9],[80,2958,3038,9],[80,2960,3008,9],[80,4096,4176,5],[80,4112,4160,5],[80,4240,4288,5],[80,4352,4432,5],[80,4368,4416,5],[80,6400,6480,5],[80,6544,6592,5],[80,8192,8272,33],[80,8194,8274,33],[80,8202,8282,33],[80,8704,8784,33],[80,8706,8786,33],[80,10752,10832,33],[80,10762,10842,33],[80,12288,12368,9],[80,12290,12370,9],[80,12304,12352,9],[80,12442,12490,9],[80,13058,13138,9],[80,13072,13120,9],[80,15104,15184,9],[80,15258,15306,9],[80,16384,16464,5],[80,16388,16468,5],[80,16396,16476,5],[80,16400,16448,5],[80,16404,16452,5],[80,16528,16576,5],[80,16540,16588,5],[80,20480,20560,5],[80,20484,20564,5],[80,20608,20688,5],[80,20736,20816,5],[80,22796,22876,5],[80,22924,23004,5],[80,24576,24656,65],[80,24590,24670,65],[80,24592,24640,65],[80,24598,24646,65],[80,25088,25168,65],[80,25094,25174,65],[80,27280,27328,65],[80,27294,27342,65],[80,28672,28752,9],[80,28678,28758,9],[80,28814,28894,9],[80,29440,29520,9],[80,29446,29526,9],[80,31502,31582,9],[80,31616,31696,9],[84,128,212,5],[84,132,208,5],[84,136,220,5],[84,138,222,9],[84,144,196,5],[84,148,192,5],[84,152,204,5],[84,154,206,9],[84,256,340,5],[84,260,336,5],[84,272,324,5],[84,512,596,255],[84,514,598,33],[84,518,594,33],[84,768,852,9],[84,770,854,9],[84,784,836,9],[84,2048,2132,5],[84,2056,2140,5],[84,2060,2136,5],[84,2176,2260,5],[84,2184,2268,5],[84,2196,2240,5],[84,2200,2252,5],[84,2304,2388,5],[84,2312,2396,5],[84,2436,2512,5],[84,2456,2508,5],[84,2560,2644,129],[84,2574,2650,33],[84,2688,2772,33],[84,2698,2782,33],[84,2816,2900,9],[84,2826,2910,9],[84,2954,3038,9],[84,2960,3012,9],[84,4096,4180,5],[84,4112,4164,5],[84,4240,4292,5],[84,4352,4436,5],[84,4368,4420,5],[84,6400,6484,5],[84,6544,6596,5],[84,8192,8276,33],[84,8194,8278,33],[84,8202,8286,33],[84,8704,8788,33],[84,8706,8790,33],[84,10752,10836,33],[84,10762,10846,33],[84,12288,12372,9],[84,12290,12374,9],[84,12304,12356,9],[84,12442,12494,9],[84,13058,13142,9],[84,13072,13124,9],[84,15104,15188,9],[84,15258,15310,9],[84,16384,16468,5],[84,16388,16464,5],[84,16396,16472,5],[84,16400,16452,5],[84,16404,16448,5],[84,16532,16576,5],[84,16536,16588,5],[84,20480,20564,5],[84,20484,20560,5],[84,20612,20688,5],[84,20736,20820,5],[84,20740,20816,5],[84,22796,22872,5],[84,22920,23004,5],[84,24576,24660,129],[84,24590,24666,129],[84,24594,24646,129],[84,24596,24640,129],[84,25088,25172,129],[84,25094,25170,129],[84,27284,27328,129],[84,27290,27342,129],[84,28672,28756,9],[84,28676,28752,9],[84,28678,28754,9],[84,28810,28894,9],[84,29440,29524,9],[84,29442,29526,9],[84,31502,31578,9],[84,31620,31696,9],[86,138,220,9],[86,152,206,9],[86,768,854,9],[86,28678,28752,9],[86,29440,29526,9],[88,136,208,5],[88,152,192,5],[90,138,208,9],[92,128,220,5],[94,144,206,9],[128,256,384,5],[128,272,400,5],[128,336,464,5],[128,512,640,3],[128,514,642,3],[128,518,646,3],[128,768,896,17],[128,770,898,17],[128,784,912,17],[128,854,982,33],[128,2048,2176,3],[128,2056,2184,3],[128,2060,2188,3],[128,2112,2240,3],[128,2124,2252,3],[128,2304,2432,5],[128,2312,2440,5],[128,2328,2456,5],[128,2384,2512,5],[128,2560,2688,3],[128,2570,2698,3],[128,2574,2702,3],[128,2816,2944,17],[128,2826,2954,17],[128,2832,2960,17],[128,2910,3038,33],[128,4096,4224,5],[128,4112,4240,5],[128,4352,4480,5],[128,4368,4496,5],[128,6400,6528,5],[128,6416,6544,5],[128,8192,8320,3],[128,8194,8322,3],[128,8202,8330,3],[128,8704,8832,3],[128,8706,8834,3],[128,10752,10880,3],[128,10762,10890,3],[128,12288,12416,17],[128,12290,12418,17],[128,12304,12432,17],[128,12314,12442,17],[128,13058,13186,17],[128,13072,13200,17],[128,15104,15232,17],[128,15130,15258,17],[128,16384,16512,3],[128,16388,16516,3],[128,16396,16524,3],[128,16448,16576,3],[128,16452,16580,3],[128,16460,16588,3],[128,20480,20608,5],[128,20484,20612,5],[128,20560,20688,5],[128,20564,20692,5],[128,20736,20864,5],[128,20816,20944,5],[128,22796,22924,5],[128,22876,23004,5],[128,24576,24704,3],[128,24590,24718,3],[128,24640,24768,3],[128,24646,24774,3],[128,25088,25216,3],[128,25094,25222,3],[128,27200,27328,3],[128,27214,27342,3],[128,28672,28800,33],[128,28678,28806,33],[128,28752,28880,33],[128,28766,28894,33],[128,29440,29568,33],[128,29526,29654,33],[128,31502,31630,33],[128,31568,31696,33],[132,2060,2184,3],[132,2574,2698,3],[132,16452,16576,3],[132,20564,20688,5],[136,256,392,5],[136,272,408,5],[136,336,472,5],[136,512,648,3],[136,514,650,3],[136,518,654,3],[136,768,904,9],[136,770,906,9],[136,784,920,9],[136,854,990,9],[136,2048,2184,3],[136,2056,2176,3],[136,2060,2180,3],[136,2116,2252,3],[136,2120,2240,3],[136,2304,2440,5],[136,2312,2432,5],[136,2320,2456,5],[136,2392,2512,5],[136,2560,2696,3],[136,2562,2698,3],[136,2568,2688,3],[136,2574,2694,3],[136,2816,2952,9],[136,2826,2946,9],[136,2840,2960,9],[136,2902,3038,9],[136,4096,4232,5],[136,4112,4248,5],[136,4120,4240,5],[136,4352,4488,5],[136,4368,4504,5],[136,6400,6536,5],[136,6424,6544,5],[136,8192,8328,3],[136,8194,8330,3],[136,8202,8322,3],[136,8704,8840,3],[136,8706,8842,3],[136,10752,10888,3],[136,10762,10882,3],[136,12288,12424,9],[136,12290,12426,9],[136,12304,12440,9],[136,12306,12442,9],[136,13058,13194,9],[136,13072,13208,9],[136,15104,15240,9],[136,15122,15258,9],[136,16384,16520,3],[136,16388,16524,3],[136,16396,16516,3],[136,16448,16584,3],[136,16452,16588,3],[136,16456,16576,3],[136,20480,20616,5],[136,20484,20620,5],[136,20564,20700,5],[136,20568,20688,5],[136,20736,20872,5],[136,20816,20952,5],[136,22796,22916,5],[136,22868,23004,5],[136,24576,24712,3],[136,24590,24710,3],[136,24640,24776,3],[136,24646,24782,3],[136,25088,25224,3],[136,25094,25230,3],[136,27206,27342,3],[136,27208,27328,3],[136,28672,28808,9],[136,28678,28814,9],[136,28752,28888,9],[136,28758,28894,9],[136,29440,29576,9],[136,29526,29662,9],[136,31502,31622,9],[136,31576,31696,9],[138,256,394,17],[138,272,410,17],[138,336,474,33],[138,512,650,3],[138,514,648,3],[138,518,652,3],[138,768,906,9],[138,770,904,9],[138,784,922,9],[138,854,988,9],[138,2048,2186,3],[138,2050,2184,3],[138,2056,2178,3],[138,2058,2176,3],[138,2060,2182,3],[138,2118,2252,3],[138,2122,2240,3],[138,2304,2442,17],[138,2312,2434,17],[138,2322,2456,17],[138,2394,2512,33],[138,2560,2698,3],[138,2570,2688,3],[138,2574,2692,3],[138,2816,2954,9],[138,2826,2944,9],[138,2842,2960,9],[138,2900,3038,9],[138,4096,4234,17],[138,4112,4250,17],[138,4122,4240,17],[138,4352,4490,17],[138,4368,4506,17],[138,6400,6538,17],[138,6426,6544,17],[138,8192,8330,3],[138,8194,8328,3],[138,8202,8320,3],[138,8704,8842,3],[138,8706,8840,3],[138,10752,10890,3],[138,10762,10880,3],[138,12288,12426,9],[138,12290,12424,9],[138,12304,12442,9],[138,13058,13192,9],[138,13072,13210,9],[138,15104,15242,9],[138,15120,15258,9],[138,16384,16522,3],[138,16388,16526,3],[138,16396,16518,3],[138,16448,16586,3],[138,16452,16590,3],[138,16454,16588,3],[138,16458,16576,3],[138,20480,20618,33],[138,20484,20622,33],[138,20564,20702,33],[138,20570,20688,33],[138,20736,20874,33],[138,20816,20954,33],[138,22796,22918,33],[138,22870,23004,33],[138,24576,24714,3],[138,24590,24708,3],[138,24640,24778,3],[138,24646,24780,3],[138,25088,25226,3],[138,25094,25228,3],[138,27204,27342,3],[138,27210,27328,3],[138,28672,28810,9],[138,28678,28812,9],[138,28752,28890,9],[138,28756,28894,9],[138,29440,29578,9],[138,29526,29660,9],[138,31502,31620,9],[138,31578,31696,9],[140,2060,2176,3],[140,16448,16588,3],[142,2574,2688,3],[142,28752,28894,9],[144,256,400,5],[144,272,384,5],[144,336,448,5],[144,512,656,17],[144,514,658,17],[144,518,662,129],[144,768,912,9],[144,770,914,9],[144,784,896,9],[144,854,966,9],[144,2048,2192,5],[144,2056,2200,5],[144,2060,2204,5],[144,2064,2176,5],[144,2072,2184,5],[144,2128,2240,5],[144,2140,2252,5],[144,2304,2448,5],[144,2312,2456,5],[144,2368,2512,5],[144,2560,2704,17],[144,2574,2718,129],[144,2576,2688,17],[144,2586,2698,17],[144,2816,2960,9],[144,2826,2970,9],[144,2894,3038,9],[144,4096,4240,5],[144,4112,4224,5],[144,4352,4496,5],[144,4368,4480,5],[144,6400,6544,5],[144,8192,8336,17],[144,8194,8338,17],[144,8202,8346,17],[144,8704,8848,17],[144,8706,8850,17],[144,10752,10896,17],[144,10762,10906,17],[144,12288,12432,9],[144,12290,12434,9],[144,12298,12442,9],[144,12304,12416,9],[144,13058,13202,9],[144,13072,13184,9],[144,15104,15248,9],[144,15114,15258,9],[144,16384,16528,5],[144,16388,16532,5],[144,16396,16540,5],[144,16448,16592,5],[144,16452,16596,5],[144,16464,16576,5],[144,16476,16588,5],[144,20480,20624,5],[144,20484,20628,5],[144,20544,20688,5],[144,20564,20676,5],[144,20736,20880,5],[144,20816,20928,5],[144,22796,22940,5],[144,22860,23004,5],[144,24576,24720,129],[144,24590,24734,129],[144,24640,24784,129],[144,24646,24790,129],[144,25088,25232,129],[144,25094,25238,129],[144,27216,27328,129],[144,27230,27342,129],[144,28672,28816,9],[144,28678,28822,9],[144,28750,28894,9],[144,28752,28864,9],[144,29440,29584,9],[144,29526,29638,9],[144,31502,31646,9],[144,31552,31696,9],[152,256,408,5],[152,272,392,5],[152,336,456,5],[152,512,664,17],[152,514,666,17],[152,518,670,65],[152,768,920,9],[152,770,922,9],[152,784,904,9],[152,854,974,9],[152,2048,2200,5],[152,2056,2192,5],[152,2060,2196,5],[152,2064,2184,5],[152,2072,2176,5],[152,2132,2252,5],[152,2136,2240,5],[152,2304,2456,5],[152,2312,2448,5],[152,2376,2512,5],[152,2560,2712,17],[152,2574,2710,65],[152,2578,2698,17],[152,2584,2688,17],[152,2816,2968,9],[152,2824,2960,9],[152,2826,2962,9],[152,2886,3038,9],[152,4096,4248,5],[152,4104,4240,5],[152,4112,4232,5],[152,4352,4504,5],[152,4368,4488,5],[152,6400,6552,5],[152,6408,6544,5],[152,8192,8344,17],[152,8194,8346,17],[152,8202,8338,17],[152,8704,8856,17],[152,8706,8858,17],[152,10752,10904,17],[152,10762,10898,17],[152,12288,12440,9],[152,12290,12442,9],[152,12304,12424,9],[152,13058,13210,9],[152,13072,13192,9],[152,15104,15256,9],[152,15106,15258,9],[152,16384,16536,5],[152,16388,16540,5],[152,16396,16532,5],[152,16448,16600,5],[152,16452,16604,5],[152,16468,16588,5],[152,16472,16576,5],[152,20480,20632,5],[152,20484,20636,5],[152,20552,20688,5],[152,20564,20684,5],[152,20736,20888,5],[152,20816,20936,5],[152,22796,22932,5],[152,22852,23004,5],[152,24576,24728,65],[152,24590,24726,65],[152,24640,24792,65],[152,24646,24798,65],[152,25088,25240,65],[152,25094,25246,65],[152,27222,27342,65],[152,27224,27328,65],[152,28672,28824,9],[152,28678,28830,9],[152,28742,28894,9],[152,28752,28872,9],[152,29440,29592,9],[152,29526,29646,9],[152,31502,31638,9],[152,31560,31696,9],[154,2826,2960,9],[154,12288,12442,9],[154,15104,15258,9],[192,256,448,5],[192,272,464,5],[192,336,400,5],[192,512,704,3],[192,514,706,3],[192,518,710,3],[192,768,960,65],[192,770,962,129],[192,784,976,65],[192,854,918,65],[192,2048,2240,3],[192,2056,2248,3],[192,2060,2252,3],[192,2112,2176,3],[192,2120,2184,3],[192,2304,2496,5],[192,2312,2504,5],[192,2320,2512,5],[192,2392,2456,5],[192,2560,2752,3],[192,2574,2766,3],[192,2624,2688,3],[192,2634,2698,3],[192,2816,3008,65],[192,2826,3018,129],[192,2846,3038,65],[192,2896,2960,65],[192,4096,4288,5],[192,4112,4304,5],[192,4176,4240,5],[192,4352,4544,5],[192,4368,4560,5],[192,6400,6592,5],[192,6480,6544,5],[192,8192,8384,3],[192,8194,8386,3],[192,8202,8394,3],[192,8704,8896,3],[192,8706,8898,3],[192,10752,10944,3],[192,10762,10954,3],[192,12288,12480,129],[192,12290,12482,129],[192,12304,12496,129],[192,12378,12442,129],[192,13058,13250,129],[192,13072,13264,129],[192,15104,15296,129],[192,15194,15258,129],[192,16384,16576,3],[192,16388,16580,3],[192,16396,16588,3],[192,16448,16512,3],[192,16452,16516,3],[192,20480,20672,5],[192,20484,20676,5],[192,20496,20688,5],[192,20564,20628,5],[192,20736,20928,5],[192,20816,20880,5],[192,22796,22988,5],[192,22812,23004,5],[192,24576,24768,3],[192,24590,24782,3],[192,24640,24704,3],[192,24646,24710,3],[192,25088,25280,3],[192,25094,25286,3],[192,27136,27328,3],[192,27150,27342,3],[192,28672,28864,65],[192,28678,28870,65],[192,28702,28894,65],[192,28752,28816,65],[192,29440,29632,65],[192,29526,29590,65],[192,31502,31694,65],[192,31504,31696,65],[196,2056,2252,3],[196,16388,16576,3],[200,2056,2240,3],[200,16388,16588,3],[204,2048,2252,3],[204,2060,2240,3],[204,16384,16588,3],[204,16396,16576,3],[206,256,462,255],[206,272,478,65],[206,336,414,65],[206,512,718,3],[206,514,716,3],[206,518,712,3],[206,768,974,9],[206,770,972,9],[206,784,990,9],[206,854,920,9],[206,2048,2254,3],[206,2050,2252,3],[206,2056,2246,3],[206,2060,2242,3],[206,2062,2240,3],[206,2118,2184,3],[206,2126,2176,3],[206,2304,2510,129],[206,2312,2502,65],[206,2334,2512,65],[206,2390,2456,65],[206,2560,2766,3],[206,2574,2752,3],[206,2628,2698,3],[206,2638,2688,3],[206,2816,3022,9],[206,2826,3012,9],[206,2832,3038,9],[206,2910,2960,9],[206,4096,4302,65],[206,4112,4318,65],[206,4190,4240,65],[206,4352,4558,65],[206,4368,4574,65],[206,6400,6606,65],[206,6494,6544,65],[206,8192,8398,3],[206,8194,8396,3],[206,8202,8388,3],[206,8704,8910,3],[206,8706,8908,3],[206,10752,10958,3],[206,10762,10948,3],[206,12288,12494,9],[206,12290,12492,9],[206,12304,12510,9],[206,12372,12442,9],[206,13058,13260,9],[206,13072,13278,9],[206,15104,15310,9],[206,15188,15258,9],[206,16384,16590,3],[206,16386,16588,3],[206,16388,16586,3],[206,16396,16578,3],[206,16398,16576,3],[206,16448,16526,3],[206,16452,16522,3],[206,20480,20686,129],[206,20484,20682,129],[206,20510,20688,129],[206,20564,20634,129],[206,20736,20942,129],[206,20816,20894,129],[206,22796,22978,129],[206,22802,23004,129],[206,24576,24782,3],[206,24590,24768,3],[206,24640,24718,3],[206,24646,24712,3],[206,25088,25294,3],[206,25094,25288,3],[206,27136,27342,3],[206,27150,27328,3],[206,28672,28878,9],[206,28678,28872,9],[206,28688,28894,9],[206,28752,28830,9],[206,29440,29646,9],[206,29526,29592,9],[206,31502,31680,9],[206,31518,31696,9],[208,256,464,5],[208,272,448,5],[208,336,384,5],[208,512,720,65],[208,514,722,33],[208,518,726,33],[208,768,976,9],[208,770,978,9],[208,784,960,9],[208,854,902,9],[208,2048,2256,5],[208,2056,2264,5],[208,2060,2268,5],[208,2064,2240,5],[208,2076,2252,5],[208,2128,2176,5],[208,2136,2184,5],[208,2304,2512,5],[208,2312,2520,5],[208,2376,2456,5],[208,2560,2768,65],[208,2574,2782,33],[208,2640,2688,33],[208,2650,2698,33],[208,2816,3024,9],[208,2826,3034,9],[208,2830,3038,9],[208,2880,2960,9],[208,4096,4304,5],[208,4112,4288,5],[208,4160,4240,5],[208,4352,4560,5],[208,4368,4544,5],[208,6400,6608,5],[208,6464,6544,5],[208,8192,8400,33],[208,8194,8402,33],[208,8202,8410,33],[208,8704,8912,33],[208,8706,8914,33],[208,10752,10960,33],[208,10762,10970,33],[208,12288,12496,9],[208,12290,12498,9],[208,12304,12480,9],[208,12362,12442,9],[208,13058,13266,9],[208,13072,13248,9],[208,15104,15312,9],[208,15178,15258,9],[208,16384,16592,5],[208,16388,16596,5],[208,16396,16604,5],[208,16400,16576,5],[208,16412,16588,5],[208,16448,16528,5],[208,16452,16532,5],[208,20480,20688,5],[208,20484,20692,5],[208,20564,20612,5],[208,20736,20944,5],[208,20816,20864,5],[208,22796,23004,5],[208,24576,24784,65],[208,24590,24798,65],[208,24640,24720,65],[208,24646,24726,65],[208,25088,25296,65],[208,25094,25302,65],[208,27152,27328,65],[208,27166,27342,65],[208,28672,28880,9],[208,28678,28886,9],[208,28686,28894,9],[208,28752,28800,9],[208,29440,29648,9],[208,29526,29574,9],[208,31488,31696,9],[208,31502,31710,9],[212,2826,3038,9],[212,20484,20688,5],[216,2312,2512,5],[216,28678,28894,9],[220,256,476,5],[220,272,460,5],[220,336,396,5],[220,512,732,255],[220,514,734,33],[220,518,730,33],[220,768,988,9],[220,770,990,9],[220,784,972,9],[220,854,906,9],[220,2048,2268,5],[220,2056,2260,5],[220,2060,2256,5],[220,2064,2252,5],[220,2076,2240,5],[220,2132,2184,5],[220,2140,2176,5],[220,2304,2524,5],[220,2312,2516,5],[220,2316,2512,5],[220,2372,2456,5],[220,2560,2780,129],[220,2574,2770,33],[220,2646,2698,33],[220,2652,2688,33],[220,2816,3036,9],[220,2818,3038,9],[220,2826,3030,9],[220,2892,2960,9],[220,4096,4316,5],[220,4112,4300,5],[220,4172,4240,5],[220,4352,4572,5],[220,4368,4556,5],[220,6400,6620,5],[220,6476,6544,5],[220,8192,8412,33],[220,8194,8414,33],[220,8202,8406,33],[220,8704,8924,33],[220,8706,8926,33],[220,10752,10972,33],[220,10762,10966,33],[220,12288,12508,9],[220,12290,12510,9],[220,12304,12492,9],[220,12358,12442,9],[220,13058,13278,9],[220,13072,13260,9],[220,15104,15324,9],[220,15174,15258,9],[220,16384,16604,5],[220,16388,16600,5],[220,16396,16592,5],[220,16400,16588,5],[220,16412,16576,5],[220,16448,16540,5],[220,16452,16536,5],[220,20480,20700,5],[220,20484,20696,5],[220,20492,20688,5],[220,20564,20616,5],[220,20736,20956,5],[220,20816,20876,5],[220,22784,23004,5],[220,22796,22992,5],[220,24576,24796,129],[220,24590,24786,129],[220,24640,24732,129],[220,24646,24730,129],[220,25088,25308,129],[220,25094,25306,129],[220,27154,27342,129],[220,27164,27328,129],[220,28672,28892,9],[220,28674,28894,9],[220,28678,28890,9],[220,28752,28812,9],[220,29440,29660,9],[220,29526,29578,9],[220,31500,31696,9],[220,31502,31698,9],[222,2816,3038,9],[222,28672,28894,9],[222,31502,31696,9],[256,512,768,17],[256,514,770,17],[256,518,774,33],[256,528,784,17],[256,598,854,33],[256,2048,2304,5],[256,2056,2312,5],[256,2060,2316,5],[256,2176,2432,5],[256,2184,2440,5],[256,2200,2456,5],[256,2240,2496,5],[256,2252,2508,5],[256,2256,2512,5],[256,2560,2816,17],[256,2570,2826,17],[256,2574,2830,33],[256,2688,2944,17],[256,2698,2954,17],[256,2704,2960,17],[256,2782,3038,33],[256,4096,4352,5],[256,4112,4368,5],[256,4240,4496,5],[256,6144,6400,5],[256,6288,6544,5],[256,8192,8448,17],[256,8194,8450,17],[256,8202,8458,17],[256,8704,8960,17],[256,8706,8962,17],[256,10752,11008,17],[256,10762,11018,17],[256,12288,12544,17],[256,12290,12546,17],[256,12304,12560,17],[256,12442,12698,17],[256,12802,13058,17],[256,12816,13072,17],[256,14848,15104,17],[256,15002,15258,17],[256,16384,16640,5],[256,16388,16644,5],[256,16396,16652,5],[256,16448,16704,5],[256,16452,16708,5],[256,16576,16832,5],[256,16588,16844,5],[256,20480,20736,5],[256,20484,20740,5],[256,20560,20816,5],[256,20564,20820,5],[256,20688,20944,5],[256,22540,22796,5],[256,22748,23004,5],[256,24576,24832,257],[256,24590,24846,1025],[256,24640,24896,257],[256,24646,24902,257],[256,25088,25344,257],[256,25094,25350,257],[256,27328,27584,1025],[256,27342,27598,1025],[256,28672,28928,33],[256,28678,28934,33],[256,28752,29008,33],[256,28894,29150,33],[256,29184,29440,33],[256,29270,29526,33],[256,31246,31502,33],[256,31440,31696,33],[258,512,770,17],[258,514,768,17],[260,518,770,33],[260,2060,2312,5],[260,2574,2826,33],[260,20484,20736,5],[260,20564,20816,5],[262,518,768,33],[264,2048,2312,5],[264,2056,2304,5],[266,2560,2826,17],[268,2060,2304,5],[270,2574,2816,33],[272,512,784,17],[272,514,786,17],[272,518,790,65],[272,528,768,17],[272,530,770,17],[272,582,854,65],[272,2048,2320,5],[272,2056,2328,5],[272,2060,2332,5],[272,2064,2304,5],[272,2072,2312,5],[272,2176,2448,5],[272,2184,2456,5],[272,2240,2512,5],[272,2252,2524,5],[272,2560,2832,17],[272,2574,2846,65],[272,2576,2816,17],[272,2586,2826,17],[272,2688,2960,17],[272,2698,2970,17],[272,2766,3038,65],[272,4096,4368,5],[272,4112,4352,5],[272,4240,4480,5],[272,6160,6400,5],[272,6272,6544,5],[272,8192,8464,17],[272,8194,8466,17],[272,8202,8474,17],[272,8704,8976,17],[272,8706,8978,17],[272,10752,11024,17],[272,10762,11034,17],[272,12288,12560,17],[272,12290,12562,17],[272,12304,12544,17],[272,12442,12682,17],[272,12800,13072,17],[272,12818,13058,17],[272,14864,15104,17],[272,14986,15258,17],[272,16384,16656,5],[272,16388,16660,5],[272,16396,16668,5],[272,16448,16720,5],[272,16452,16724,5],[272,16576,16848,5],[272,16588,16860,5],[272,20480,20752,5],[272,20484,20756,5],[272,20496,20736,5],[272,20544,20816,5],[272,20564,20804,5],[272,20688,20928,5],[272,22556,22796,5],[272,22732,23004,5],[272,24576,24848,65],[272,24590,24862,65],[272,24640,24912,65],[272,24646,24918,65],[272,25088,25360,65],[272,25094,25366,65],[272,27328,27600,65],[272,27342,27614,65],[272,28672,28944,65],[272,28678,28950,65],[272,28752,28992,65],[272,28894,29134,65],[272,29200,29440,65],[272,29254,29526,65],[272,31262,31502,65],[272,31424,31696,65],[274,514,784,17],[278,518,784,65],[280,2176,2456,5],[282,2698,2960,17],[284,2252,2512,5],[336,512,848,65],[336,514,850,33],[336,518,854,33],[336,576,784,65],[336,592,768,33],[336,594,770,33],[336,2048,2384,5],[336,2056,2392,5],[336,2060,2396,5],[336,2128,2304,5],[336,2136,2312,5],[336,2176,2512,5],[336,2184,2520,5],[336,2240,2448,5],[336,2248,2456,5],[336,2252,2460,5],[336,2560,2896,65],[336,2574,2910,33],[336,2640,2816,33],[336,2650,2826,33],[336,2688,3024,33],[336,2698,3034,33],[336,2702,3038,33],[336,2752,2960,65],[336,4096,4432,5],[336,4112,4416,5],[336,4160,4368,5],[336,4176,4352,5],[336,4240,4544,5],[336,6224,6400,5],[336,6336,6544,5],[336,8192,8528,33],[336,8194,8530,33],[336,8202,8538,33],[336,8704,9040,33],[336,8706,9042,33],[336,10752,11088,33],[336,10762,11098,33],[336,12288,12624,129],[336,12290,12626,129],[336,12304,12608,129],[336,12442,12746,129],[336,12864,13072,129],[336,12882,13058,129],[336,14928,15104,129],[336,15050,15258,129],[336,16384,16720,5],[336,16388,16724,5],[336,16396,16732,5],[336,16448,16656,5],[336,16452,16660,5],[336,16576,16784,5],[336,16588,16796,5],[336,20480,20816,5],[336,20484,20820,5],[336,20560,20736,5],[336,20564,20740,5],[336,20688,20864,5],[336,22620,22796,5],[336,22668,23004,5],[336,24576,24912,65],[336,24590,24926,65],[336,24640,24848,65],[336,24646,24854,65],[336,25088,25424,65],[336,25094,25430,65],[336,27328,27536,65],[336,27342,27550,65],[336,28672,29008,33],[336,28678,29014,33],[336,28752,28928,33],[336,28894,29070,33],[336,29190,29526,33],[336,29264,29440,33],[336,31326,31502,33],[336,31360,31696,33],[340,514,854,33],[340,2252,2456,5],[340,2698,3038,33],[340,20484,20816,5],[340,20564,20736,5],[342,512,854,65],[344,2184,2512,5],[344,2240,2456,5],[350,2688,3038,33],[384,2176,2304,5],[384,2184,2312,5],[384,2688,2816,17],[384,2698,2826,17],[384,4240,4368,5],[384,20688,20816,5],[392,2176,2312,5],[392,2184,2304,5],[394,2688,2826,17],[394,2698,2816,17],[400,2056,2456,5],[400,2560,2960,17],[400,4240,4352,5],[404,2060,2456,5],[408,2048,2456,5],[414,2574,2960,65],[448,2240,2304,5],[452,2252,2312,5],[456,2240,2312,5],[460,2252,2304,5],[464,2048,2512,5],[464,2574,3038,33],[464,20688,20736,5],[472,2056,2512,5],[476,2060,2512,5],[478,2560,3038,65],[512,2048,2560,3],[512,2056,2568,3],[512,2060,2572,3],[512,2062,2574,3],[512,2176,2688,3],[512,2184,2696,3],[512,2186,2698,3],[512,2240,2752,3],[512,2252,2764,3],[512,2304,2816,17],[512,2312,2824,17],[512,2314,2826,17],[512,2448,2960,17],[512,2456,2968,17],[512,2512,3024,65],[512,2526,3038,65],[512,4096,4608,17],[512,4112,4624,17],[512,4240,4752,17],[512,4352,4864,17],[512,4368,4880,17],[512,6400,6912,17],[512,6544,7056,17],[512,8192,8704,3],[512,8194,8706,3],[512,8202,8714,3],[512,10240,10752,3],[512,10250,10762,3],[512,12288,12800,17],[512,12290,12802,17],[512,12304,12816,17],[512,12442,12954,17],[512,12546,13058,17],[512,12560,13072,17],[512,14592,15104,17],[512,14746,15258,17],[512,16384,16896,3],[512,16388,16900,3],[512,16396,16908,3],[512,16448,16960,3],[512,16452,16964,3],[512,16576,17088,3],[512,16588,17100,3],[512,20480,20992,257],[512,20484,20996,257],[512,20564,21076,257],[512,20688,21200,513],[512,20736,21248,257],[512,20816,21328,257],[512,22796,23308,513],[512,23004,23516,513],[512,24576,25088,3],[512,24582,25094,3],[512,24590,25102,3],[512,24640,25152,3],[512,24646,25158,3],[512,26816,27328,3],[512,26830,27342,3],[512,28672,29184,65],[512,28678,29190,65],[512,28752,29264,65],[512,28894,29406,65],[512,28928,29440,65],[512,29014,29526,65],[512,30990,31502,65],[512,31184,31696,65],[514,2048,2562,3],[514,2050,2560,3],[514,2056,2570,3],[514,2060,2574,3],[514,2176,2690,3],[514,2178,2688,3],[514,2184,2698,3],[514,2240,2754,3],[514,2252,2766,3],[514,2304,2818,17],[514,2306,2816,17],[514,2312,2826,17],[514,2450,2960,17],[514,2456,2970,17],[514,2512,3026,33],[514,2524,3038,33],[514,4096,4610,17],[514,4112,4626,17],[514,4240,4754,17],[514,4352,4866,17],[514,4368,4882,17],[514,6400,6914,17],[514,6544,7058,17],[514,8192,8706,3],[514,8194,8704,3],[514,8202,8712,3],[514,10242,10752,3],[514,10248,10762,3],[514,12288,12802,17],[514,12290,12800,17],[514,12304,12818,17],[514,12442,12952,17],[514,12544,13058,17],[514,12562,13072,17],[514,14594,15104,17],[514,14744,15258,17],[514,16384,16898,3],[514,16388,16902,3],[514,16396,16910,3],[514,16448,16962,3],[514,16452,16966,3],[514,16576,17090,3],[514,16588,17102,3],[514,20480,20994,33],[514,20484,20998,33],[514,20564,21078,33],[514,20688,21202,33],[514,20736,21250,33],[514,20816,21330,33],[514,22796,23310,33],[514,23004,23518,33],[514,24576,25090,3],[514,24578,25088,3],[514,24580,25094,3],[514,24590,25100,3],[514,24640,25154,3],[514,24646,25156,3],[514,26818,27328,3],[514,26828,27342,3],[514,28672,29186,33],[514,28678,29188,33],[514,28752,29266,33],[514,28894,29404,33],[514,28930,29440,33],[514,29012,29526,33],[514,30988,31502,33],[514,31186,31696,33],[518,2048,2566,3],[518,2054,2560,3],[518,2056,2574,3],[518,2060,2570,3],[518,2176,2694,3],[518,2182,2688,3],[518,2184,2702,3],[518,2188,2698,3],[518,2240,2758,3],[518,2252,2762,3],[518,2304,2822,33],[518,2310,2816,33],[518,2312,2830,33],[518,2316,2826,33],[518,2454,2960,65],[518,2456,2974,65],[518,2512,3030,33],[518,2520,3038,33],[518,4096,4614,65],[518,4112,4630,65],[518,4240,4758,65],[518,4352,4870,65],[518,4368,4886,65],[518,6400,6918,65],[518,6544,7062,65],[518,8192,8710,3],[518,8194,8708,3],[518,8196,8706,3],[518,8198,8704,3],[518,8202,8716,3],[518,10246,10752,3],[518,10252,10762,3],[518,12288,12806,129],[518,12290,12804,129],[518,12304,12822,129],[518,12442,12956,129],[518,12548,13058,129],[518,12566,13072,129],[518,14598,15104,129],[518,14748,15258,129],[518,16384,16902,3],[518,16388,16898,3],[518,16396,16906,3],[518,16448,16966,3],[518,16452,16962,3],[518,16576,17094,3],[518,16588,17098,3],[518,20480,20998,33],[518,20484,20994,33],[518,20564,21074,33],[518,20688,21206,33],[518,20736,21254,33],[518,20816,21334,33],[518,22796,23306,33],[518,23004,23514,33],[518,24576,25094,3],[518,24582,25088,3],[518,24590,25096,3],[518,24640,25158,3],[518,24646,25152,3],[518,26822,27328,3],[518,26824,27342,3],[518,28672,29190,33],[518,28678,29184,33],[518,28752,29270,33],[518,28894,29400,33],[518,28934,29440,33],[518,29008,29526,33],[518,30984,31502,33],[518,31190,31696,33],[520,2056,2560,3],[520,2184,2688,3],[520,2312,2816,17],[520,2456,2960,17],[520,8202,8706,3],[520,24590,25094,3],[522,2176,2698,3],[522,2304,2826,17],[522,8202,8704,3],[524,2060,2560,3],[526,2048,2574,3],[526,2512,3038,33],[526,24590,25088,3],[576,2240,2688,3],[576,2512,2960,65],[576,24640,25088,3],[576,24646,25094,3],[582,2252,2698,3],[582,2456,3038,65],[582,24640,25094,3],[582,24646,25088,3],[586,2240,2698,3],[588,2252,2688,3],[640,2048,2688,3],[640,2176,2560,3],[642,2056,2698,3],[646,2060,2698,3],[646,2184,2574,3],[648,2056,2688,3],[648,2184,2560,3],[650,2048,2698,3],[652,2060,2688,3],[654,2176,2574,3],[656,2304,2960,17],[658,2456,2826,17],[664,2312,2960,17],[664,2456,2816,17],[704,2240,2560,3],[706,2252,2574,3],[716,2252,2560,3],[718,2240,2574,3],[720,2512,2816,33],[726,2312,3038,33],[730,2512,2826,33],[734,2304,3038,33],[768,2048,2816,9],[768,2056,2824,9],[768,2058,2826,9],[768,2060,2828,9],[768,2176,2944,9],[768,2184,2952,9],[768,2192,2960,9],[768,2240,3008,9],[768,2252,3020,9],[768,2270,3038,9],[768,2304,2560,17],[768,2312,2568,17],[768,2318,2574,33],[768,2432,2688,17],[768,2442,2698,17],[768,2456,2712,17],[768,2512,2768,33],[768,4096,4864,17],[768,4112,4880,17],[768,4240,5008,17],[768,4352,4608,17],[768,4368,4624,17],[768,6400,6656,17],[768,6544,6800,17],[768,8192,8960,17],[768,8194,8962,17],[768,8202,8970,17],[768,8448,8704,17],[768,8450,8706,17],[768,10496,10752,17],[768,10506,10762,17],[768,12288,13056,9],[768,12290,13058,9],[768,12304,13072,9],[768,12442,13210,9],[768,14336,15104,9],[768,14490,15258,9],[768,16384,17152,9],[768,16388,17156,9],[768,16396,17164,9],[768,16448,17216,9],[768,16452,17220,9],[768,16576,17344,9],[768,16588,17356,9],[768,20480,21248,33],[768,20484,21252,33],[768,20564,21332,33],[768,20688,21456,33],[768,20736,20992,33],[768,20816,21072,33],[768,22796,23052,33],[768,23004,23260,33],[768,24576,25344,65],[768,24590,25358,65],[768,24640,25408,65],[768,24646,25414,65],[768,24832,25088,65],[768,24838,25094,65],[768,27072,27328,65],[768,27086,27342,65],[768,28672,29440,9],[768,28678,29446,9],[768,28752,29520,9],[768,28758,29526,9],[768,28894,29662,9],[768,30734,31502,9],[768,30928,31696,9],[770,2048,2818,9],[770,2050,2816,9],[770,2056,2826,9],[770,2060,2830,9],[770,2176,2946,9],[770,2184,2954,9],[770,2194,2960,9],[770,2240,3010,9],[770,2252,3022,9],[770,2268,3038,9],[770,2304,2562,17],[770,2306,2560,17],[770,2312,2570,17],[770,2316,2574,33],[770,2434,2688,17],[770,2440,2698,17],[770,2456,2714,17],[770,2512,2770,33],[770,4096,4866,17],[770,4112,4882,17],[770,4240,5010,17],[770,4352,4610,17],[770,4368,4626,17],[770,6400,6658,17],[770,6544,6802,17],[770,8192,8962,17],[770,8194,8960,17],[770,8202,8968,17],[770,8448,8706,17],[770,8450,8704,17],[770,10498,10752,17],[770,10504,10762,17],[770,12288,13058,9],[770,12290,13056,9],[770,12304,13074,9],[770,12306,13072,9],[770,12442,13208,9],[770,14338,15104,9],[770,14488,15258,9],[770,16384,17154,9],[770,16388,17158,9],[770,16396,17166,9],[770,16448,17218,9],[770,16452,17222,9],[770,16576,17346,9],[770,16588,17358,9],[770,20480,21250,33],[770,20484,21254,33],[770,20564,21334,33],[770,20688,21458,33],[770,20736,20994,33],[770,20816,21074,33],[770,22796,23054,33],[770,23004,23262,33],[770,24576,25346,129],[770,24590,25356,129],[770,24640,25410,129],[770,24646,25412,129],[770,24834,25088,129],[770,24836,25094,129],[770,27074,27328,129],[770,27084,27342,129],[770,28672,29442,9],[770,28674,29440,9],[770,28678,29444,9],[770,28752,29522,9],[770,28756,29526,9],[770,28894,29660,9],[770,30732,31502,9],[770,30930,31696,9],[774,2060,2826,9],[774,2312,2574,33],[774,28678,29440,9],[774,28752,29526,9],[776,2056,2816,9],[776,2312,2560,17],[778,2048,2826,9],[780,2060,2816,9],[782,2304,2574,33],[784,2048,2832,9],[784,2056,2840,9],[784,2060,2844,9],[784,2064,2816,9],[784,2074,2826,9],[784,2176,2960,9],[784,2184,2968,9],[784,2240,3024,9],[784,2252,3036,9],[784,2254,3038,9],[784,2304,2576,17],[784,2312,2584,17],[784,2320,2560,17],[784,2334,2574,65],[784,2448,2688,17],[784,2456,2696,17],[784,2458,2698,17],[784,2512,2752,65],[784,4096,4880,17],[784,4112,4864,17],[784,4240,4992,17],[784,4352,4624,17],[784,4368,4608,17],[784,6400,6672,17],[784,6544,6784,17],[784,8192,8976,17],[784,8194,8978,17],[784,8202,8986,17],[784,8464,8704,17],[784,8466,8706,17],[784,10512,10752,17],[784,10522,10762,17],[784,12288,13072,9],[784,12290,13074,9],[784,12304,13056,9],[784,12306,13058,9],[784,12442,13194,9],[784,14352,15104,9],[784,14474,15258,9],[784,16384,17168,9],[784,16388,17172,9],[784,16396,17180,9],[784,16448,17232,9],[784,16452,17236,9],[784,16576,17360,9],[784,16588,17372,9],[784,20480,21264,129],[784,20484,21268,129],[784,20564,21316,129],[784,20688,21440,129],[784,20736,21008,129],[784,20816,21056,129],[784,22796,23068,129],[784,23004,23244,129],[784,24576,25360,65],[784,24590,25374,65],[784,24640,25424,65],[784,24646,25430,65],[784,24848,25088,65],[784,24854,25094,65],[784,27088,27328,65],[784,27102,27342,65],[784,28672,29456,9],[784,28678,29462,9],[784,28688,29440,9],[784,28742,29526,9],[784,28752,29504,9],[784,28894,29646,9],[784,30750,31502,9],[784,30912,31696,9],[786,2252,3038,9],[786,2456,2698,17],[786,12290,13072,9],[786,12304,13058,9],[792,2184,2960,9],[792,2456,2688,17],[798,2240,3038,9],[848,2240,2960,9],[848,2512,2688,33],[848,28678,29526,9],[848,28752,29440,9],[854,2048,2902,9],[854,2056,2910,9],[854,2060,2906,9],[854,2134,2816,9],[854,2140,2826,9],[854,2176,3030,9],[854,2184,3038,9],[854,2240,2966,9],[854,2246,2960,9],[854,2252,2970,9],[854,2304,2646,33],[854,2312,2654,33],[854,2390,2560,65],[854,2392,2574,33],[854,2456,2766,65],[854,2512,2694,33],[854,2518,2688,33],[854,2524,2698,33],[854,4096,4950,65],[854,4112,4934,65],[854,4240,5062,65],[854,4352,4694,65],[854,4368,4678,65],[854,6400,6742,65],[854,6544,6854,65],[854,8192,9046,33],[854,8194,9044,33],[854,8202,9052,33],[854,8532,8706,33],[854,8534,8704,33],[854,10582,10752,33],[854,10588,10762,33],[854,12288,13142,9],[854,12290,13140,9],[854,12304,13126,9],[854,12358,13072,9],[854,12372,13058,9],[854,12442,13260,9],[854,14422,15104,9],[854,14540,15258,9],[854,16384,17238,9],[854,16388,17234,9],[854,16396,17242,9],[854,16448,17174,9],[854,16452,17170,9],[854,16576,17302,9],[854,16588,17306,9],[854,20480,21334,33],[854,20484,21330,33],[854,20564,21250,33],[854,20688,21382,33],[854,20736,21078,33],[854,20816,20998,33],[854,22796,23130,33],[854,23004,23178,33],[854,24576,25430,65],[854,24590,25432,65],[854,24640,25366,65],[854,24646,25360,65],[854,24912,25094,65],[854,24918,25088,65],[854,27030,27328,65],[854,27032,27342,65],[854,28672,29526,9],[854,28678,29520,9],[854,28752,29446,9],[854,28758,29440,9],[854,28894,29576,9],[854,30808,31502,9],[854,30854,31696,9],[858,2512,2698,33],[860,2252,2960,9],[862,2176,3038,9],[896,2176,2816,9],[896,2304,2688,17],[898,2184,2826,9],[898,2312,2698,17],[904,2184,2816,9],[904,2312,2688,17],[904,28894,29526,9],[906,2176,2826,9],[906,2304,2698,17],[906,12442,13072,9],[912,2048,2960,9],[918,2456,2574,65],[920,2056,2960,9],[920,2456,2560,17],[920,12442,13058,9],[924,2060,2960,9],[960,2240,2816,9],[966,2252,2826,9],[970,2240,2826,9],[972,2252,2816,9],[976,2512,2560,65],[978,2060,3038,9],[982,2056,3038,9],[990,2048,3038,9],[990,2512,2574,33],[990,28894,29440,9],[2048,4096,6144,5],[2048,4112,6160,5],[2048,4240,6288,5],[2048,4352,6400,5],[2048,4368,6416,5],[2048,4496,6544,5],[2048,8192,10240,3],[2048,8194,10242,3],[2048,8202,10250,3],[2048,8704,10752,3],[2048,8706,10754,3],[2048,8714,10762,3],[2048,12288,14336,9],[2048,12290,14338,9],[2048,12304,14352,9],[2048,12442,14490,9],[2048,13056,15104,9],[2048,13058,15106,9],[2048,13072,15120,9],[2048,13210,15258,9],[2048,16384,18432,3],[2048,16388,18436,3],[2048,16396,18444,3],[2048,16448,18496,3],[2048,16452,18500,3],[2048,16576,18624,3],[2048,16588,18636,3],[2048,20480,22528,5],[2048,20484,22532,5],[2048,20564,22612,5],[2048,20688,22736,5],[2048,20736,22784,5],[2048,20748,22796,5],[2048,20816,22864,5],[2048,20956,23004,5],[2048,24576,26624,3],[2048,24590,26638,3],[2048,24640,26688,3],[2048,24646,26694,3],[2048,25088,27136,3],[2048,25094,27142,3],[2048,25280,27328,3],[2048,25294,27342,3],[2048,28672,30720,9],[2048,28678,30726,9],[2048,28752,30800,9],[2048,28894,30942,9],[2048,29440,31488,9],[2048,29454,31502,9],[2048,29526,31574,9],[2048,29648,31696,9],[2050,8706,10752,3],[2050,13058,15104,9],[2056,4096,6152,5],[2056,4112,6168,5],[2056,4240,6296,5],[2056,4352,6408,5],[2056,4360,6400,5],[2056,4368,6424,5],[2056,4504,6544,5],[2056,8192,10248,3],[2056,8194,10250,3],[2056,8202,10242,3],[2056,8704,10760,3],[2056,8706,10762,3],[2056,8712,10752,3],[2056,12288,14344,9],[2056,12290,14346,9],[2056,12304,14360,9],[2056,12442,14482,9],[2056,13058,15114,9],[2056,13064,15104,9],[2056,13072,15128,9],[2056,13202,15258,9],[2056,16384,18440,3],[2056,16388,18444,3],[2056,16396,18436,3],[2056,16448,18504,3],[2056,16452,18508,3],[2056,16576,18632,3],[2056,16588,18628,3],[2056,20480,22536,5],[2056,20484,22540,5],[2056,20564,22620,5],[2056,20688,22744,5],[2056,20736,22792,5],[2056,20740,22796,5],[2056,20816,22872,5],[2056,20948,23004,5],[2056,24576,26632,3],[2056,24590,26630,3],[2056,24640,26696,3],[2056,24646,26702,3],[2056,25088,27144,3],[2056,25094,27150,3],[2056,25286,27342,3],[2056,25288,27328,3],[2056,28672,30728,9],[2056,28678,30734,9],[2056,28752,30808,9],[2056,28894,30934,9],[2056,29440,31496,9],[2056,29446,31502,9],[2056,29526,31582,9],[2056,29656,31696,9],[2058,8704,10762,3],[2060,4096,6156,5],[2060,4112,6172,5],[2060,4240,6300,5],[2060,4352,6412,5],[2060,4364,6400,5],[2060,4368,6428,5],[2060,4508,6544,5],[2060,8192,10252,3],[2060,8194,10254,3],[2060,8202,10246,3],[2060,8704,10764,3],[2060,8706,10766,3],[2060,8710,10762,3],[2060,8716,10752,3],[2060,12288,14348,9],[2060,12290,14350,9],[2060,12304,14364,9],[2060,12442,14486,9],[2060,13058,15118,9],[2060,13068,15104,9],[2060,13072,15132,9],[2060,13206,15258,9],[2060,16384,18444,3],[2060,16388,18440,3],[2060,16396,18432,3],[2060,16448,18508,3],[2060,16452,18504,3],[2060,16576,18636,3],[2060,16588,18624,3],[2060,20480,22540,5],[2060,20484,22536,5],[2060,20564,22616,5],[2060,20688,22748,5],[2060,20736,22796,5],[2060,20816,22876,5],[2060,20944,23004,5],[2060,24576,26636,3],[2060,24590,26626,3],[2060,24640,26700,3],[2060,24646,26698,3],[2060,25088,27148,3],[2060,25094,27146,3],[2060,25282,27342,3],[2060,25292,27328,3],[2060,28672,30732,9],[2060,28678,30730,9],[2060,28752,30812,9],[2060,28894,30930,9],[2060,29440,31500,9],[2060,29442,31502,9],[2060,29526,31578,9],[2060,29660,31696,9],[2062,29440,31502,9],[2064,4368,6400,5],[2064,13072,15104,9],[2136,29526,31502,9],[2140,20816,22796,5],[2176,4096,6272,5],[2176,4112,6288,5],[2176,4240,6160,5],[2176,4352,6528,5],[2176,4368,6544,5],[2176,4480,6400,5],[2176,8192,10368,3],[2176,8194,10370,3],[2176,8202,10378,3],[2176,8704,10880,3],[2176,8706,10882,3],[2176,8832,10752,3],[2176,8842,10762,3],[2176,12288,14464,9],[2176,12290,14466,9],[2176,12304,14480,9],[2176,12442,14362,9],[2176,13058,15234,9],[2176,13072,15248,9],[2176,13082,15258,9],[2176,13184,15104,9],[2176,16384,18560,3],[2176,16388,18564,3],[2176,16396,18572,3],[2176,16448,18624,3],[2176,16452,18628,3],[2176,16576,18496,3],[2176,16588,18508,3],[2176,20480,22656,5],[2176,20484,22660,5],[2176,20564,22740,5],[2176,20688,22608,5],[2176,20736,22912,5],[2176,20816,22992,5],[2176,20828,23004,5],[2176,20876,22796,5],[2176,24576,26752,3],[2176,24590,26766,3],[2176,24640,26816,3],[2176,24646,26822,3],[2176,25088,27264,3],[2176,25094,27270,3],[2176,25152,27328,3],[2176,25166,27342,3],[2176,28672,30848,9],[2176,28678,30854,9],[2176,28752,30928,9],[2176,28894,30814,9],[2176,29440,31616,9],[2176,29520,31696,9],[2176,29526,31702,9],[2176,29582,31502,9],[2182,29526,31696,9],[2184,4096,6280,5],[2184,4112,6296,5],[2184,4240,6168,5],[2184,4352,6536,5],[2184,4368,6552,5],[2184,4376,6544,5],[2184,4488,6400,5],[2184,8192,10376,3],[2184,8194,10378,3],[2184,8202,10370,3],[2184,8704,10888,3],[2184,8706,10890,3],[2184,8834,10762,3],[2184,8840,10752,3],[2184,12288,14472,9],[2184,12290,14474,9],[2184,12304,14488,9],[2184,12442,14354,9],[2184,13058,15242,9],[2184,13072,15256,9],[2184,13074,15258,9],[2184,13192,15104,9],[2184,16384,18568,3],[2184,16388,18572,3],[2184,16396,18564,3],[2184,16448,18632,3],[2184,16452,18636,3],[2184,16576,18504,3],[2184,16588,18500,3],[2184,20480,22664,5],[2184,20484,22668,5],[2184,20564,22748,5],[2184,20688,22616,5],[2184,20736,22920,5],[2184,20816,23000,5],[2184,20820,23004,5],[2184,20868,22796,5],[2184,24576,26760,3],[2184,24590,26758,3],[2184,24640,26824,3],[2184,24646,26830,3],[2184,25088,27272,3],[2184,25094,27278,3],[2184,25158,27342,3],[2184,25160,27328,3],[2184,28672,30856,9],[2184,28678,30862,9],[2184,28752,30936,9],[2184,28894,30806,9],[2184,29440,31624,9],[2184,29526,31710,9],[2184,29528,31696,9],[2184,29574,31502,9],[2186,13072,15258,9],[2188,20816,23004,5],[2192,4352,6544,5],[2200,13058,15258,9],[2240,4096,6336,5],[2240,4112,6352,5],[2240,4240,6224,5],[2240,4352,6592,5],[2240,4368,6608,5],[2240,4432,6544,5],[2240,4544,6400,5],[2240,8192,10432,3],[2240,8194,10434,3],[2240,8202,10442,3],[2240,8704,10944,3],[2240,8706,10946,3],[2240,8896,10752,3],[2240,8906,10762,3],[2240,12288,14528,9],[2240,12290,14530,9],[2240,12304,14544,9],[2240,12442,14426,9],[2240,13058,15298,9],[2240,13072,15312,9],[2240,13146,15258,9],[2240,13248,15104,9],[2240,16384,18624,3],[2240,16388,18628,3],[2240,16396,18636,3],[2240,16448,18560,3],[2240,16452,18564,3],[2240,16576,18432,3],[2240,16588,18444,3],[2240,20480,22720,5],[2240,20484,22724,5],[2240,20564,22676,5],[2240,20688,22544,5],[2240,20736,22976,5],[2240,20764,23004,5],[2240,20816,22928,5],[2240,20940,22796,5],[2240,24576,26816,3],[2240,24590,26830,3],[2240,24640,26752,3],[2240,24646,26758,3],[2240,25088,27328,3],[2240,25094,27334,3],[2240,25102,27342,3],[2240,28672,30912,9],[2240,28678,30918,9],[2240,28752,30864,9],[2240,28894,30750,9],[2240,29440,31680,9],[2240,29456,31696,9],[2240,29526,31638,9],[2240,29646,31502,9],[2246,25094,27328,3],[2248,25094,27342,3],[2252,4096,6348,5],[2252,4112,6364,5],[2252,4240,6236,5],[2252,4352,6604,5],[2252,4368,6620,5],[2252,4444,6544,5],[2252,4556,6400,5],[2252,8192,10444,3],[2252,8194,10446,3],[2252,8202,10438,3],[2252,8704,10956,3],[2252,8706,10958,3],[2252,8902,10762,3],[2252,8908,10752,3],[2252,12288,14540,9],[2252,12290,14542,9],[2252,12304,14556,9],[2252,12442,14422,9],[2252,13058,15310,9],[2252,13072,15324,9],[2252,13142,15258,9],[2252,13260,15104,9],[2252,16384,18636,3],[2252,16388,18632,3],[2252,16396,18624,3],[2252,16448,18572,3],[2252,16452,18568,3],[2252,16576,18444,3],[2252,16588,18432,3],[2252,20480,22732,5],[2252,20484,22728,5],[2252,20564,22680,5],[2252,20688,22556,5],[2252,20736,22988,5],[2252,20752,23004,5],[2252,20816,22940,5],[2252,20928,22796,5],[2252,24576,26828,3],[2252,24590,26818,3],[2252,24640,26764,3],[2252,24646,26762,3],[2252,25088,27340,3],[2252,25090,27342,3],[2252,25094,27338,3],[2252,25100,27328,3],[2252,28672,30924,9],[2252,28678,30922,9],[2252,28752,30876,9],[2252,28894,30738,9],[2252,29440,31692,9],[2252,29468,31696,9],[2252,29526,31642,9],[2252,29634,31502,9],[2254,25088,27342,3],[2256,29440,31696,9],[2268,20736,23004,5],[2304,4096,6400,5],[2304,4112,6416,5],[2304,4240,6544,5],[2304,4352,6144,5],[2304,4368,6160,5],[2304,8192,10496,17],[2304,8194,10498,17],[2304,8202,10506,17],[2304,8704,11008,17],[2304,8706,11010,17],[2304,8960,10752,17],[2304,8970,10762,17],[2304,12288,14592,17],[2304,12290,14594,17],[2304,12304,14608,17],[2304,12442,14746,17],[2304,12800,15104,17],[2304,12954,15258,17],[2304,13058,14850,17],[2304,13072,14864,17],[2304,16384,18688,5],[2304,16388,18692,5],[2304,16396,18700,5],[2304,16448,18752,5],[2304,16452,18756,5],[2304,16576,18880,5],[2304,16588,18892,5],[2304,20480,22784,5],[2304,20484,22788,5],[2304,20492,22796,5],[2304,20564,22868,5],[2304,20688,22992,5],[2304,20700,23004,5],[2304,20736,22528,5],[2304,20816,22608,5],[2304,24576,26880,129],[2304,24590,26894,129],[2304,24640,26944,129],[2304,24646,26950,129],[2304,25088,27392,129],[2304,25094,27398,129],[2304,25536,27328,129],[2304,25550,27342,129],[2304,28672,30976,33],[2304,28678,30982,33],[2304,28752,31056,33],[2304,28894,31198,33],[2304,29198,31502,33],[2304,29392,31696,33],[2304,29440,31232,33],[2304,29526,31318,33],[2312,4096,6408,5],[2312,4104,6400,5],[2312,4112,6424,5],[2312,4240,6552,5],[2312,4248,6544,5],[2312,4352,6152,5],[2312,4368,6168,5],[2312,8192,10504,17],[2312,8194,10506,17],[2312,8202,10498,17],[2312,8704,11016,17],[2312,8706,11018,17],[2312,8962,10762,17],[2312,8968,10752,17],[2312,12288,14600,17],[2312,12290,14602,17],[2312,12304,14616,17],[2312,12442,14738,17],[2312,12808,15104,17],[2312,12946,15258,17],[2312,13058,14858,17],[2312,13072,14872,17],[2312,16384,18696,5],[2312,16388,18700,5],[2312,16396,18692,5],[2312,16448,18760,5],[2312,16452,18764,5],[2312,16576,18888,5],[2312,16588,18884,5],[2312,20480,22792,5],[2312,20484,22796,5],[2312,20564,22876,5],[2312,20688,23000,5],[2312,20692,23004,5],[2312,20736,22536,5],[2312,20816,22616,5],[2312,24576,26888,65],[2312,24590,26886,65],[2312,24640,26952,65],[2312,24646,26958,65],[2312,25088,27400,65],[2312,25094,27406,65],[2312,25542,27342,65],[2312,25544,27328,65],[2312,28672,30984,33],[2312,28678,30990,33],[2312,28752,31064,33],[2312,28894,31190,33],[2312,29190,31502,33],[2312,29400,31696,33],[2312,29440,31240,33],[2312,29526,31326,33],[2316,20480,22796,5],[2316,20688,23004,5],[2320,4112,6400,5],[2392,20564,22796,5],[2432,4112,6544,5],[2440,20564,23004,5],[2448,4096,6544,5],[2448,4240,6400,5],[2456,4096,6552,5],[2456,4104,6544,5],[2456,4112,6536,5],[2456,4240,6408,5],[2456,4248,6400,5],[2456,4352,6296,5],[2456,4368,6280,5],[2456,8192,10648,17],[2456,8194,10650,17],[2456,8202,10642,17],[2456,8704,11160,17],[2456,8706,11162,17],[2456,9106,10762,17],[2456,9112,10752,17],[2456,12288,14744,17],[2456,12290,14746,17],[2456,12304,14728,17],[2456,12442,14594,17],[2456,12802,15258,17],[2456,12952,15104,17],[2456,13058,15002,17],[2456,13072,14984,17],[2456,16384,18840,5],[2456,16388,18844,5],[2456,16396,18836,5],[2456,16448,18904,5],[2456,16452,18908,5],[2456,16576,18776,5],[2456,16588,18772,5],[2456,20480,22936,5],[2456,20484,22940,5],[2456,20548,23004,5],[2456,20564,22988,5],[2456,20628,22796,5],[2456,20688,22856,5],[2456,20736,22680,5],[2456,20816,22728,5],[2456,24576,27032,65],[2456,24590,27030,65],[2456,24640,27096,65],[2456,24646,27102,65],[2456,25088,27544,65],[2456,25094,27550,65],[2456,25430,27342,65],[2456,25432,27328,65],[2456,28672,31128,65],[2456,28678,31134,65],[2456,28752,31176,65],[2456,28894,31046,65],[2456,29256,31696,65],[2456,29334,31502,65],[2456,29440,31384,65],[2456,29526,31438,65],[2512,4096,6608,5],[2512,4112,6592,5],[2512,4160,6544,5],[2512,4240,6464,5],[2512,4304,6400,5],[2512,4352,6352,5],[2512,4368,6336,5],[2512,8192,10704,33],[2512,8194,10706,33],[2512,8202,10714,33],[2512,8704,11216,33],[2512,8706,11218,33],[2512,9168,10752,33],[2512,9178,10762,33],[2512,12288,14800,129],[2512,12290,14802,129],[2512,12304,14784,129],[2512,12442,14666,129],[2512,12874,15258,129],[2512,13008,15104,129],[2512,13058,15058,129],[2512,13072,15040,129],[2512,16384,18896,5],[2512,16388,18900,5],[2512,16396,18908,5],[2512,16448,18832,5],[2512,16452,18836,5],[2512,16576,18704,5],[2512,16588,18716,5],[2512,20480,22992,5],[2512,20484,22996,5],[2512,20492,23004,5],[2512,20564,22916,5],[2512,20688,22784,5],[2512,20700,22796,5],[2512,20736,22736,5],[2512,20816,22656,5],[2512,24576,27088,65],[2512,24590,27102,65],[2512,24640,27024,65],[2512,24646,27030,65],[2512,25088,27600,65],[2512,25094,27606,65],[2512,25360,27328,65],[2512,25374,27342,65],[2512,28672,31184,33],[2512,28678,31190,33],[2512,28752,31104,33],[2512,28894,30990,33],[2512,29184,31696,33],[2512,29406,31502,33],[2512,29440,31440,33],[2512,29526,31366,33],[2520,20484,23004,5],[2524,20480,23004,5],[2524,20688,22796,5],[2560,4096,6656,17],[2560,4112,6672,17],[2560,4240,6800,17],[2560,4352,6912,17],[2560,4368,6928,17],[2560,4864,6400,17],[2560,5008,6544,17],[2560,8192,10752,3],[2560,8194,10754,3],[2560,8202,10762,3],[2560,8704,10240,3],[2560,8706,10242,3],[2560,12288,14848,17],[2560,12290,14850,17],[2560,12304,14864,17],[2560,12442,15002,17],[2560,12544,15104,17],[2560,12698,15258,17],[2560,13058,14594,17],[2560,13072,14608,17],[2560,16384,18944,3],[2560,16388,18948,3],[2560,16396,18956,3],[2560,16448,19008,3],[2560,16452,19012,3],[2560,16576,19136,3],[2560,16588,19148,3],[2560,20480,23040,129],[2560,20484,23044,129],[2560,20564,23124,129],[2560,20688,23248,129],[2560,20736,23296,129],[2560,20816,23376,129],[2560,21260,22796,129],[2560,21468,23004,129],[2560,24576,27136,3],[2560,24590,27150,3],[2560,24640,27200,3],[2560,24646,27206,3],[2560,24768,27328,3],[2560,24782,27342,3],[2560,25088,26624,3],[2560,25094,26630,3],[2560,28672,31232,65],[2560,28678,31238,65],[2560,28752,31312,65],[2560,28894,31454,65],[2560,28942,31502,65],[2560,29136,31696,65],[2560,29440,30976,65],[2560,29526,31062,65],[2562,8194,10752,3],[2568,8194,10762,3],[2570,8192,10762,3],[2570,8202,10752,3],[2574,4096,6670,65],[2574,4112,6686,65],[2574,4240,6814,65],[2574,4352,6926,65],[2574,4368,6942,65],[2574,4878,6400,65],[2574,5022,6544,65],[2574,8192,10766,3],[2574,8194,10764,3],[2574,8196,10762,3],[2574,8202,10756,3],[2574,8206,10752,3],[2574,8704,10254,3],[2574,8706,10252,3],[2574,12288,14862,129],[2574,12290,14860,129],[2574,12304,14878,129],[2574,12442,14996,129],[2574,12558,15104,129],[2574,12692,15258,129],[2574,13058,14604,129],[2574,13072,14622,129],[2574,16384,18958,3],[2574,16388,18954,3],[2574,16396,18946,3],[2574,16448,19022,3],[2574,16452,19018,3],[2574,16576,19150,3],[2574,16588,19138,3],[2574,20480,23054,33],[2574,20484,23050,33],[2574,20564,23130,33],[2574,20688,23262,33],[2574,20736,23310,33],[2574,20816,23390,33],[2574,21250,22796,33],[2574,21458,23004,33],[2574,24576,27150,3],[2574,24590,27136,3],[2574,24640,27214,3],[2574,24646,27208,3],[2574,24768,27342,3],[2574,24782,27328,3],[2574,25088,26638,3],[2574,25094,26632,3],[2574,28672,31246,33],[2574,28678,31240,33],[2574,28752,31326,33],[2574,28894,31440,33],[2574,28928,31502,33],[2574,29150,31696,33],[2574,29440,30990,33],[2574,29526,31064,33],[2688,4096,6784,17],[2688,4112,6800,17],[2688,4240,6672,17],[2688,4352,7040,17],[2688,4368,7056,17],[2688,4880,6544,17],[2688,4992,6400,17],[2688,8192,10880,3],[2688,8194,10882,3],[2688,8202,10890,3],[2688,8320,10752,3],[2688,8330,10762,3],[2688,8704,10368,3],[2688,8706,10370,3],[2688,12288,14976,17],[2688,12290,14978,17],[2688,12304,14992,17],[2688,12442,14874,17],[2688,12570,15258,17],[2688,12672,15104,17],[2688,13058,14722,17],[2688,13072,14736,17],[2688,16384,19072,3],[2688,16388,19076,3],[2688,16396,19084,3],[2688,16448,19136,3],[2688,16452,19140,3],[2688,16576,19008,3],[2688,16588,19020,3],[2688,20480,23168,33],[2688,20484,23172,33],[2688,20564,23252,33],[2688,20688,23120,33],[2688,20736,23424,33],[2688,20816,23504,33],[2688,21340,23004,33],[2688,21388,22796,33],[2688,24576,27264,3],[2688,24590,27278,3],[2688,24640,27328,3],[2688,24646,27334,3],[2688,24654,27342,3],[2688,25088,26752,3],[2688,25094,26758,3],[2688,28672,31360,33],[2688,28678,31366,33],[2688,28752,31440,33],[2688,28894,31326,33],[2688,29008,31696,33],[2688,29070,31502,33],[2688,29440,31104,33],[2688,29526,31190,33],[2694,24646,27328,3],[2696,24646,27342,3],[2698,4096,6794,17],[2698,4112,6810,17],[2698,4240,6682,17],[2698,4352,7050,17],[2698,4368,7066,17],[2698,4890,6544,17],[2698,5002,6400,17],[2698,8192,10890,3],[2698,8194,10888,3],[2698,8202,10880,3],[2698,8320,10762,3],[2698,8330,10752,3],[2698,8704,10378,3],[2698,8706,10376,3],[2698,12288,14986,17],[2698,12290,14984,17],[2698,12304,15002,17],[2698,12442,14864,17],[2698,12560,15258,17],[2698,12682,15104,17],[2698,13058,14728,17],[2698,13072,14746,17],[2698,16384,19082,3],[2698,16388,19086,3],[2698,16396,19078,3],[2698,16448,19146,3],[2698,16452,19150,3],[2698,16576,19018,3],[2698,16588,19014,3],[2698,20480,23178,33],[2698,20484,23182,33],[2698,20564,23262,33],[2698,20688,23130,33],[2698,20736,23434,33],[2698,20816,23514,33],[2698,21334,23004,33],[2698,21382,22796,33],[2698,24576,27274,3],[2698,24590,27268,3],[2698,24640,27338,3],[2698,24644,27342,3],[2698,24646,27340,3],[2698,24650,27328,3],[2698,25088,26762,3],[2698,25094,26764,3],[2698,28672,31370,33],[2698,28678,31372,33],[2698,28752,31450,33],[2698,28894,31316,33],[2698,29018,31696,33],[2698,29060,31502,33],[2698,29440,31114,33],[2698,29526,31196,33],[2702,24640,27342,3],[2752,24576,27328,3],[2752,24590,27342,3],[2766,24576,27342,3],[2766,24590,27328,3],[2816,4096,6912,17],[2816,4112,6928,17],[2816,4240,7056,17],[2816,4352,6656,17],[2816,4368,6672,17],[2816,4608,6400,17],[2816,4752,6544,17],[2816,8192,11008,17],[2816,8194,11010,17],[2816,8202,11018,17],[2816,8448,10752,17],[2816,8458,10762,17],[2816,8704,10496,17],[2816,8706,10498,17],[2816,12288,15104,9],[2816,12290,15106,9],[2816,12304,15120,9],[2816,12442,15258,9],[2816,13058,14338,9],[2816,13072,14352,9],[2816,16384,19200,9],[2816,16388,19204,9],[2816,16396,19212,9],[2816,16448,19264,9],[2816,16452,19268,9],[2816,16576,19392,9],[2816,16588,19404,9],[2816,20480,23296,33],[2816,20484,23300,33],[2816,20564,23380,33],[2816,20688,23504,33],[2816,20736,23040,33],[2816,20816,23120,33],[2816,21004,22796,33],[2816,21212,23004,33],[2816,24576,27392,65],[2816,24590,27406,65],[2816,24640,27456,65],[2816,24646,27462,65],[2816,25024,27328,65],[2816,25038,27342,65],[2816,25088,26880,65],[2816,25094,26886,65],[2816,28672,31488,9],[2816,28678,31494,9],[2816,28686,31502,9],[2816,28752,31568,9],[2816,28880,31696,9],[2816,28894,31710,9],[2816,29440,30720,9],[2816,29526,30806,9],[2818,12290,15104,9],[2824,28678,31502,9],[2826,4096,6922,17],[2826,4112,6938,17],[2826,4240,7066,17],[2826,4352,6666,17],[2826,4368,6682,17],[2826,4618,6400,17],[2826,4762,6544,17],[2826,8192,11018,17],[2826,8194,11016,17],[2826,8202,11008,17],[2826,8448,10762,17],[2826,8458,10752,17],[2826,8704,10506,17],[2826,8706,10504,17],[2826,12288,15114,9],[2826,12290,15112,9],[2826,12298,15104,9],[2826,12304,15130,9],[2826,12432,15258,9],[2826,12442,15248,9],[2826,13058,14344,9],[2826,13072,14362,9],[2826,16384,19210,9],[2826,16388,19214,9],[2826,16396,19206,9],[2826,16448,19274,9],[2826,16452,19278,9],[2826,16576,19402,9],[2826,16588,19398,9],[2826,20480,23306,33],[2826,20484,23310,33],[2826,20564,23390,33],[2826,20688,23514,33],[2826,20736,23050,33],[2826,20816,23130,33],[2826,20998,22796,33],[2826,21206,23004,33],[2826,24576,27402,129],[2826,24590,27396,129],[2826,24640,27466,129],[2826,24646,27468,129],[2826,25028,27342,129],[2826,25034,27328,129],[2826,25088,26890,129],[2826,25094,26892,129],[2826,28672,31498,9],[2826,28676,31502,9],[2826,28678,31500,9],[2826,28752,31578,9],[2826,28890,31696,9],[2826,28894,31700,9],[2826,29440,30730,9],[2826,29526,30812,9],[2830,28672,31502,9],[2830,28894,31696,9],[2832,12304,15104,9],[2910,28752,31502,9],[2944,28752,31696,9],[2954,12304,15258,9],[2960,4096,7056,17],[2960,4112,7040,17],[2960,4240,6912,17],[2960,4352,6800,17],[2960,4368,6784,17],[2960,4608,6544,17],[2960,4752,6400,17],[2960,8192,11152,17],[2960,8194,11154,17],[2960,8202,11162,17],[2960,8592,10752,17],[2960,8602,10762,17],[2960,8704,10640,17],[2960,8706,10642,17],[2960,12288,15248,9],[2960,12290,15250,9],[2960,12298,15258,9],[2960,12304,15232,9],[2960,12432,15104,9],[2960,12442,15114,9],[2960,13058,14482,9],[2960,13072,14464,9],[2960,16384,19344,9],[2960,16388,19348,9],[2960,16396,19356,9],[2960,16448,19408,9],[2960,16452,19412,9],[2960,16576,19280,9],[2960,16588,19292,9],[2960,20480,23440,129],[2960,20484,23444,129],[2960,20564,23492,129],[2960,20688,23360,129],[2960,20736,23184,129],[2960,20816,23232,129],[2960,21068,23004,129],[2960,21148,22796,129],[2960,24576,27536,65],[2960,24590,27550,65],[2960,24640,27600,65],[2960,24646,27606,65],[2960,24912,27328,65],[2960,24926,27342,65],[2960,25088,27024,65],[2960,25094,27030,65],[2960,28672,31632,9],[2960,28678,31638,9],[2960,28736,31696,9],[2960,28752,31680,9],[2960,28830,31502,9],[2960,28894,31566,9],[2960,29440,30864,9],[2960,29526,30918,9],[2968,12290,15258,9],[2970,12288,15258,9],[2970,12442,15104,9],[3024,28672,31696,9],[3024,28894,31502,9],[3030,28678,31696,9],[3038,4096,7134,65],[3038,4112,7118,65],[3038,4240,6990,65],[3038,4352,6878,65],[3038,4368,6862,65],[3038,4686,6544,65],[3038,4830,6400,65],[3038,8192,11230,33],[3038,8194,11228,33],[3038,8202,11220,33],[3038,8660,10762,33],[3038,8670,10752,33],[3038,8704,10718,33],[3038,8706,10716,33],[3038,12288,15326,9],[3038,12290,15324,9],[3038,12304,15310,9],[3038,12356,15258,9],[3038,12442,15172,9],[3038,12510,15104,9],[3038,13058,14556,9],[3038,13072,14542,9],[3038,16384,19422,9],[3038,16388,19418,9],[3038,16396,19410,9],[3038,16448,19358,9],[3038,16452,19354,9],[3038,16576,19230,9],[3038,16588,19218,9],[3038,20480,23518,33],[3038,20484,23514,33],[3038,20564,23434,33],[3038,20688,23310,33],[3038,20736,23262,33],[3038,20816,23182,33],[3038,20994,23004,33],[3038,21202,22796,33],[3038,24576,27614,65],[3038,24590,27600,65],[3038,24640,27550,65],[3038,24646,27544,65],[3038,24848,27342,65],[3038,24862,27328,65],[3038,25088,27102,65],[3038,25094,27096,65],[3038,28672,31710,9],[3038,28678,31704,9],[3038,28686,31696,9],[3038,28752,31630,9],[3038,28880,31502,9],[3038,28894,31488,9],[3038,29440,30942,9],[3038,29526,30856,9],[4096,8192,12288,17],[4096,8194,12290,17],[4096,8202,12298,17],[4096,8208,12304,17],[4096,8346,12442,17],[4096,8704,12800,17],[4096,8706,12802,17],[4096,8962,13058,17],[4096,8976,13072,17],[4096,10752,14848,17],[4096,10762,14858,17],[4096,11008,15104,17],[4096,11162,15258,17],[4096,16384,20480,5],[4096,16388,20484,5],[4096,16396,20492,5],[4096,16448,20544,5],[4096,16452,20548,5],[4096,16468,20564,5],[4096,16576,20672,5],[4096,16588,20684,5],[4096,16592,20688,5],[4096,16640,20736,5],[4096,16720,20816,5],[4096,18700,22796,5],[4096,18908,23004,5],[4096,24576,28672,65],[4096,24582,28678,65],[4096,24590,28686,65],[4096,24640,28736,65],[4096,24646,28742,65],[4096,24656,28752,65],[4096,24798,28894,65],[4096,25088,29184,65],[4096,25094,29190,65],[4096,25344,29440,65],[4096,25430,29526,65],[4096,27328,31424,65],[4096,27342,31438,65],[4096,27406,31502,65],[4096,27600,31696,65],[4098,8192,12290,17],[4098,8194,12288,17],[4100,16384,20484,5],[4100,16388,20480,5],[4102,24576,28678,65],[4104,8202,12290,17],[4104,16396,20484,5],[4104,24590,28678,65],[4106,8202,12288,17],[4108,16396,20480,5],[4110,24590,28672,65],[4112,8192,12304,17],[4112,8194,12306,17],[4112,8202,12314,17],[4112,8208,12288,17],[4112,8210,12290,17],[4112,8330,12442,17],[4112,8704,12816,17],[4112,8706,12818,17],[4112,8960,13072,17],[4112,8978,13058,17],[4112,10752,14864,17],[4112,10762,14874,17],[4112,11024,15104,17],[4112,11146,15258,17],[4112,16384,20496,5],[4112,16388,20500,5],[4112,16396,20508,5],[4112,16400,20480,5],[4112,16404,20484,5],[4112,16448,20560,5],[4112,16452,20564,5],[4112,16576,20688,5],[4112,16588,20700,5],[4112,16656,20736,5],[4112,16704,20816,5],[4112,18716,22796,5],[4112,18892,23004,5],[4112,24576,28688,65],[4112,24590,28702,65],[4112,24592,28672,65],[4112,24598,28678,65],[4112,24640,28752,65],[4112,24646,28758,65],[4112,24782,28894,65],[4112,25088,29200,65],[4112,25094,29206,65],[4112,25360,29440,65],[4112,25414,29526,65],[4112,27328,31440,65],[4112,27342,31454,65],[4112,27422,31502,65],[4112,27584,31696,65],[4114,8194,12304,17],[4116,16448,20564,5],[4118,24646,28752,65],[4122,8202,12304,17],[4124,16588,20688,5],[4160,16448,20480,5],[4160,16452,20484,5],[4160,24640,28672,65],[4160,24646,28678,65],[4164,16448,20484,5],[4164,16452,20480,5],[4166,24640,28678,65],[4166,24646,28672,65],[4176,16388,20564,5],[4176,24576,28752,65],[4180,16384,20564,5],[4184,16396,20564,5],[4190,24590,28752,65],[4240,8192,12432,17],[4240,8194,12434,17],[4240,8202,12442,17],[4240,8320,12304,17],[4240,8336,12288,17],[4240,8338,12290,17],[4240,8704,12944,17],[4240,8706,12946,17],[4240,9088,13072,17],[4240,9106,13058,17],[4240,10752,14992,17],[4240,10762,15002,17],[4240,11018,15258,17],[4240,11152,15104,17],[4240,16384,20624,5],[4240,16388,20628,5],[4240,16396,20636,5],[4240,16448,20688,5],[4240,16452,20692,5],[4240,16528,20480,5],[4240,16532,20484,5],[4240,16576,20560,5],[4240,16580,20564,5],[4240,16588,20572,5],[4240,16784,20736,5],[4240,16832,20816,5],[4240,18764,23004,5],[4240,18844,22796,5],[4240,24576,28816,65],[4240,24590,28830,65],[4240,24640,28880,65],[4240,24646,28886,65],[4240,24654,28894,65],[4240,24720,28672,65],[4240,24726,28678,65],[4240,24768,28752,65],[4240,25088,29328,65],[4240,25094,29334,65],[4240,25488,29440,65],[4240,25542,29526,65],[4240,27328,31312,65],[4240,27342,31326,65],[4240,27456,31696,65],[4240,27550,31502,65],[4244,16452,20688,5],[4244,16576,20564,5],[4248,8194,12442,17],[4248,16588,20564,5],[4248,24646,28894,65],[4250,8192,12442,17],[4254,24640,28894,65],[4288,16576,20480,5],[4292,16576,20484,5],[4296,16588,20484,5],[4300,16588,20480,5],[4304,16384,20688,5],[4304,24590,28894,65],[4308,16388,20688,5],[4316,16396,20688,5],[4318,24576,28894,65],[4352,8192,12544,17],[4352,8194,12546,17],[4352,8202,12554,17],[4352,8448,12288,17],[4352,8450,12290,17],[4352,8464,12304,17],[4352,8602,12442,17],[4352,8704,13056,17],[4352,8706,13058,17],[4352,8720,13072,17],[4352,10752,15104,17],[4352,10762,15114,17],[4352,10906,15258,17],[4352,16384,20736,5],[4352,16388,20740,5],[4352,16396,20748,5],[4352,16448,20800,5],[4352,16452,20804,5],[4352,16464,20816,5],[4352,16576,20928,5],[4352,16588,20940,5],[4352,16640,20480,5],[4352,16644,20484,5],[4352,16724,20564,5],[4352,16848,20688,5],[4352,18444,22796,5],[4352,18652,23004,5],[4352,24576,28928,65],[4352,24590,28942,65],[4352,24640,28992,65],[4352,24646,28998,65],[4352,24832,28672,65],[4352,24838,28678,65],[4352,24912,28752,65],[4352,25054,28894,65],[4352,25088,29440,65],[4352,25094,29446,65],[4352,25174,29526,65],[4352,27150,31502,65],[4352,27328,31680,65],[4352,27342,31694,65],[4352,27344,31696,65],[4354,8704,13058,17],[4356,16388,20736,5],[4358,25094,29440,65],[4362,10762,15104,17],[4364,16396,20736,5],[4368,8192,12560,17],[4368,8194,12562,17],[4368,8202,12570,17],[4368,8448,12304,17],[4368,8464,12288,17],[4368,8466,12290,17],[4368,8586,12442,17],[4368,8704,13072,17],[4368,8706,13074,17],[4368,8722,13058,17],[4368,10752,15120,17],[4368,10762,15130,17],[4368,10768,15104,17],[4368,10890,15258,17],[4368,16384,20752,5],[4368,16388,20756,5],[4368,16396,20764,5],[4368,16400,20736,5],[4368,16448,20816,5],[4368,16452,20820,5],[4368,16576,20944,5],[4368,16588,20956,5],[4368,16656,20480,5],[4368,16660,20484,5],[4368,16708,20564,5],[4368,16832,20688,5],[4368,18460,22796,5],[4368,18636,23004,5],[4368,24576,28944,65],[4368,24590,28958,65],[4368,24640,29008,65],[4368,24646,29014,65],[4368,24848,28672,65],[4368,24854,28678,65],[4368,24896,28752,65],[4368,25038,28894,65],[4368,25088,29456,65],[4368,25094,29462,65],[4368,25104,29440,65],[4368,25158,29526,65],[4368,27166,31502,65],[4368,27328,31696,65],[4368,27342,31710,65],[4370,8706,13072,17],[4372,16452,20816,5],[4382,27342,31696,65],[4416,16448,20736,5],[4420,16452,20736,5],[4432,16384,20816,5],[4432,25094,29526,65],[4436,16388,20816,5],[4438,25088,29526,65],[4444,16396,20816,5],[4496,10762,15258,17],[4496,16576,20816,5],[4506,10752,15258,17],[4508,16588,20816,5],[4544,16576,20736,5],[4544,27342,31502,65],[4556,16588,20736,5],[4558,27328,31502,65],[4608,8704,12288,17],[4608,8706,12290,17],[4608,25088,28672,65],[4608,25094,28678,65],[4610,8704,12290,17],[4610,8706,12288,17],[4614,25088,28678,65],[4614,25094,28672,65],[4624,8704,12304,17],[4626,8706,12304,17],[4688,25088,28752,65],[4694,25094,28752,65],[4760,8706,12442,17],[4762,8704,12442,17],[4824,25094,28894,65],[4830,25088,28894,65],[4864,8194,13058,17],[4864,24576,29440,65],[4866,8192,13058,17],[4872,8202,13058,17],[4878,24590,29440,65],[4880,8192,13072,17],[4880,24646,29526,65],[4882,8194,13072,17],[4886,24640,29526,65],[4890,8202,13072,17],[4928,24640,29440,65],[4934,24646,29440,65],[4950,24576,29526,65],[4952,24590,29526,65],[6400,8192,14592,17],[6400,8194,14594,17],[6400,8202,14602,17],[6400,8704,15104,17],[6400,8706,15106,17],[6400,8858,15258,17],[6400,10496,12288,17],[6400,10498,12290,17],[6400,10512,12304,17],[6400,10650,12442,17],[6400,10752,13056,17],[6400,10754,13058,17],[6400,10762,13066,17],[6400,10768,13072,17],[6400,16384,22784,5],[6400,16388,22788,5],[6400,16396,22796,5],[6400,16448,22848,5],[6400,16452,22852,5],[6400,16576,22976,5],[6400,16588,22988,5],[6400,16604,23004,5],[6400,18432,20736,5],[6400,18512,20816,5],[6400,18688,20480,5],[6400,18692,20484,5],[6400,18772,20564,5],[6400,18896,20688,5],[6400,24576,30976,65],[6400,24590,30990,65],[6400,24640,31040,65],[6400,24646,31046,65],[6400,25088,31488,65],[6400,25094,31494,65],[6400,25102,31502,65],[6400,25296,31696,65],[6400,26880,28672,65],[6400,26886,28678,65],[6400,26960,28752,65],[6400,27102,28894,65],[6400,27136,29440,65],[6400,27222,29526,65],[6400,27328,29632,65],[6400,27342,29646,65],[6402,8706,15104,17],[6402,10752,13058,17],[6408,10762,13058,17],[6408,16388,22796,5],[6408,25094,31502,65],[6412,16384,22796,5],[6414,25088,31502,65],[6416,10752,13072,17],[6416,16588,23004,5],[6426,10762,13072,17],[6428,16576,23004,5],[6472,16452,22796,5],[6476,16448,22796,5],[6544,8192,14736,17],[6544,8194,14738,17],[6544,8202,14746,17],[6544,8704,15248,17],[6544,8706,15250,17],[6544,8714,15258,17],[6544,8848,15104,17],[6544,10506,12442,17],[6544,10624,12304,17],[6544,10640,12288,17],[6544,10642,12290,17],[6544,10752,13200,17],[6544,10762,13210,17],[6544,10880,13072,17],[6544,10898,13058,17],[6544,16384,22928,5],[6544,16388,22932,5],[6544,16396,22940,5],[6544,16448,22992,5],[6544,16452,22996,5],[6544,16460,23004,5],[6544,16540,22796,5],[6544,16576,22864,5],[6544,16588,22876,5],[6544,18576,20736,5],[6544,18624,20816,5],[6544,18752,20688,5],[6544,18832,20480,5],[6544,18836,20484,5],[6544,18884,20564,5],[6544,24576,31120,65],[6544,24590,31134,65],[6544,24640,31184,65],[6544,24646,31190,65],[6544,25088,31632,65],[6544,25094,31638,65],[6544,25152,31696,65],[6544,25246,31502,65],[6544,26958,28894,65],[6544,27024,28672,65],[6544,27030,28678,65],[6544,27072,28752,65],[6544,27280,29440,65],[6544,27328,29520,65],[6544,27334,29526,65],[6544,27342,29534,65],[6550,27328,29526,65],[6552,8706,15258,17],[6552,16452,23004,5],[6552,27342,29526,65],[6554,8704,15258,17],[6556,16448,23004,5],[6592,16588,22796,5],[6592,27328,29440,65],[6604,16576,22796,5],[6606,27342,29440,65],[6608,16396,23004,5],[6608,25088,31696,65],[6614,25094,31696,65],[6616,16388,23004,5],[6620,16384,23004,5],[6656,10752,12288,17],[6658,10752,12290,17],[6664,10762,12290,17],[6666,10762,12288,17],[6672,10752,12304,17],[6672,27342,28894,65],[6682,10762,12304,17],[6686,27328,28894,65],[6800,10762,12442,17],[6800,27328,28752,65],[6810,10752,12442,17],[6814,27342,28752,65],[6848,27328,28672,65],[6854,27328,28678,65],[6856,27342,28678,65],[6862,27342,28672,65],[6912,8192,15104,17],[6912,24590,31502,65],[6914,8194,15104,17],[6922,8202,15104,17],[6926,24576,31502,65],[6984,24646,31502,65],[6990,24640,31502,65],[7056,8202,15258,17],[7056,24640,31696,65],[7062,24646,31696,65],[7064,8194,15258,17],[7066,8192,15258,17],[7120,24576,31696,65],[7134,24590,31696,65],[8192,16384,24576,3],[8192,16388,24580,3],[8192,16396,24588,3],[8192,16398,24590,3],[8192,16448,24640,3],[8192,16452,24644,3],[8192,16454,24646,3],[8192,16576,24768,3],[8192,16588,24780,3],[8192,16896,25088,3],[8192,16902,25094,3],[8192,19136,27328,3],[8192,19150,27342,3],[8192,20480,28672,33],[8192,20484,28676,33],[8192,20486,28678,33],[8192,20560,28752,33],[8192,20564,28756,33],[8192,20688,28880,33],[8192,20702,28894,33],[8192,20736,28928,33],[8192,20816,29008,33],[8192,21248,29440,33],[8192,21334,29526,33],[8192,22796,30988,33],[8192,23004,31196,33],[8192,23310,31502,33],[8192,23504,31696,33],[8194,16384,24578,3],[8194,16386,24576,3],[8194,16388,24582,3],[8194,16396,24590,3],[8194,16448,24642,3],[8194,16450,24640,3],[8194,16452,24646,3],[8194,16576,24770,3],[8194,16588,24782,3],[8194,16898,25088,3],[8194,16900,25094,3],[8194,19138,27328,3],[8194,19148,27342,3],[8194,20480,28674,33],[8194,20482,28672,33],[8194,20484,28678,33],[8194,20562,28752,33],[8194,20564,28758,33],[8194,20688,28882,33],[8194,20700,28894,33],[8194,20736,28930,33],[8194,20816,29010,33],[8194,21250,29440,33],[8194,21332,29526,33],[8194,22796,30990,33],[8194,23004,31198,33],[8194,23308,31502,33],[8194,23506,31696,33],[8196,16388,24576,3],[8196,16452,24640,3],[8196,20484,28672,33],[8196,20564,28752,33],[8198,16448,24646,3],[8198,20480,28678,33],[8202,16384,24586,3],[8202,16388,24590,3],[8202,16394,24576,3],[8202,16396,24582,3],[8202,16448,24650,3],[8202,16452,24654,3],[8202,16458,24640,3],[8202,16460,24646,3],[8202,16576,24778,3],[8202,16588,24774,3],[8202,16906,25088,3],[8202,16908,25094,3],[8202,19140,27342,3],[8202,19146,27328,3],[8202,20480,28682,33],[8202,20484,28686,33],[8202,20490,28672,33],[8202,20492,28678,33],[8202,20564,28766,33],[8202,20570,28752,33],[8202,20688,28890,33],[8202,20692,28894,33],[8202,20736,28938,33],[8202,20816,29018,33],[8202,21258,29440,33],[8202,21340,29526,33],[8202,22796,30982,33],[8202,23004,31190,33],[8202,23300,31502,33],[8202,23514,31696,33],[8204,16396,24576,3],[8206,16384,24590,3],[8206,20688,28894,33],[8256,16384,24640,3],[8256,16448,24576,3],[8258,16388,24646,3],[8260,16388,24640,3],[8260,16452,24576,3],[8262,16384,24646,3],[8266,16396,24646,3],[8266,16452,24590,3],[8268,16396,24640,3],[8270,16448,24590,3],[8272,20480,28752,33],[8274,20564,28678,33],[8276,20484,28752,33],[8276,20564,28672,33],[8320,16576,24640,3],[8320,20688,28752,33],[8326,16576,24646,3],[8330,16588,24646,3],[8330,20564,28894,33],[8332,16588,24640,3],[8384,16576,24576,3],[8386,16588,24590,3],[8396,16588,24576,3],[8398,16576,24590,3],[8400,20688,28672,33],[8406,20688,28678,33],[8410,20484,28894,33],[8414,20480,28894,33],[8448,20736,28672,33],[8448,20816,28752,33],[8454,20736,28678,33],[8528,20736,28752,33],[8528,20816,28672,33],[8534,20816,28678,33],[8590,20816,28894,33],[8670,20736,28894,33],[8704,16384,25088,3],[8704,16388,25092,3],[8704,16390,25094,3],[8704,16396,25100,3],[8704,16448,25152,3],[8704,16452,25156,3],[8704,16576,25280,3],[8704,16588,25292,3],[8704,16896,24576,3],[8704,16910,24590,3],[8704,16960,24640,3],[8704,16966,24646,3],[8704,18624,27328,3],[8704,18638,27342,3],[8704,20480,29184,33],[8704,20484,29188,33],[8704,20564,29268,33],[8704,20688,29392,33],[8704,20736,29440,33],[8704,20816,29520,33],[8704,20822,29526,33],[8704,20992,28672,33],[8704,20998,28678,33],[8704,21072,28752,33],[8704,21214,28894,33],[8704,22796,31500,33],[8704,22798,31502,33],[8704,22992,31696,33],[8704,23004,31708,33],[8706,16384,25090,3],[8706,16386,25088,3],[8706,16388,25094,3],[8706,16396,25102,3],[8706,16448,25154,3],[8706,16452,25158,3],[8706,16576,25282,3],[8706,16588,25294,3],[8706,16898,24576,3],[8706,16908,24590,3],[8706,16962,24640,3],[8706,16964,24646,3],[8706,18626,27328,3],[8706,18636,27342,3],[8706,20480,29186,33],[8706,20484,29190,33],[8706,20564,29270,33],[8706,20688,29394,33],[8706,20736,29442,33],[8706,20738,29440,33],[8706,20816,29522,33],[8706,20820,29526,33],[8706,20994,28672,33],[8706,20996,28678,33],[8706,21074,28752,33],[8706,21212,28894,33],[8706,22796,31502,33],[8706,22994,31696,33],[8706,23004,31710,33],[8708,16388,25088,3],[8710,16384,25094,3],[8710,20816,29526,33],[8714,16396,25094,3],[8716,16396,25088,3],[8716,23004,31696,33],[8768,16448,25088,3],[8770,16452,25094,3],[8772,16452,25088,3],[8774,16448,25094,3],[8784,20816,29440,33],[8790,20736,29526,33],[8896,16576,25088,3],[8902,16576,25094,3],[8906,16588,25094,3],[8908,16588,25088,3],[8914,23004,31502,33],[8924,22796,31696,33],[8960,20480,29440,33],[8962,20564,29526,33],[8964,20484,29440,33],[9042,20484,29526,33],[9044,20564,29440,33],[9046,20480,29526,33],[9094,20688,29526,33],[9168,20688,29440,33],[10498,23004,28894,33],[10506,22796,28678,33],[10508,22796,28672,33],[10588,22796,28752,33],[10636,23004,28752,33],[10706,22796,28894,33],[10714,23004,28678,33],[10716,23004,28672,33],[10752,16384,27136,3],[10752,16388,27140,3],[10752,16396,27148,3],[10752,16448,27200,3],[10752,16452,27204,3],[10752,16576,27328,3],[10752,16588,27340,3],[10752,16590,27342,3],[10752,18432,25088,3],[10752,18438,25094,3],[10752,18944,24576,3],[10752,18958,24590,3],[10752,19008,24640,3],[10752,19014,24646,3],[10752,20480,31232,33],[10752,20484,31236,33],[10752,20564,31316,33],[10752,20688,31440,33],[10752,20736,31488,33],[10752,20750,31502,33],[10752,20816,31568,33],[10752,20944,31696,33],[10752,22784,29440,33],[10752,22796,29452,33],[10752,22870,29526,33],[10752,23004,29660,33],[10752,23040,28672,33],[10752,23046,28678,33],[10752,23120,28752,33],[10752,23262,28894,33],[10754,16588,27342,3],[10762,16384,27146,3],[10762,16388,27150,3],[10762,16396,27142,3],[10762,16448,27210,3],[10762,16452,27214,3],[10762,16576,27338,3],[10762,16580,27342,3],[10762,16586,27328,3],[10762,16588,27334,3],[10762,18442,25088,3],[10762,18444,25094,3],[10762,18948,24590,3],[10762,18954,24576,3],[10762,19018,24640,3],[10762,19020,24646,3],[10762,20480,31242,33],[10762,20484,31246,33],[10762,20564,31326,33],[10762,20688,31450,33],[10762,20736,31498,33],[10762,20740,31502,33],[10762,20816,31578,33],[10762,20954,31696,33],[10762,22794,29440,33],[10762,22796,29446,33],[10762,22876,29526,33],[10762,23004,29654,33],[10762,23050,28672,33],[10762,23052,28678,33],[10762,23130,28752,33],[10762,23252,28894,33],[10764,16588,27328,3],[10764,22796,29440,33],[10766,16576,27342,3],[10766,20736,31502,33],[10842,22796,29526,33],[10846,20816,31502,33],[10880,16448,27328,3],[10880,20816,31696,33],[10884,16452,27328,3],[10890,16452,27342,3],[10890,23004,29526,33],[10894,16448,27342,3],[10944,16384,27328,3],[10946,16396,27342,3],[10948,16388,27328,3],[10954,16388,27342,3],[10956,16396,27328,3],[10958,16384,27342,3],[10960,20736,31696,33],[10972,23004,29440,33],[11008,20688,31696,33],[11018,20484,31502,33],[11022,20480,31502,33],[11098,20564,31502,33],[11140,20564,31696,33],[11216,20480,31696,33],[11220,20484,31696,33],[11230,20688,31502,33],[12288,16384,28672,9],[12288,16388,28676,9],[12288,16390,28678,9],[12288,16396,28684,9],[12288,16448,28736,9],[12288,16452,28740,9],[12288,16464,28752,9],[12288,16576,28864,9],[12288,16588,28876,9],[12288,16606,28894,9],[12288,17152,29440,9],[12288,17238,29526,9],[12288,19214,31502,9],[12288,19408,31696,9],[12288,20480,24576,129],[12288,20484,24580,129],[12288,20494,24590,129],[12288,20544,24640,129],[12288,20550,24646,129],[12288,20564,24660,129],[12288,20688,24784,129],[12288,20736,24832,129],[12288,20816,24912,129],[12288,20992,25088,129],[12288,20998,25094,129],[12288,22796,26892,129],[12288,23004,27100,129],[12288,23232,27328,129],[12288,23246,27342,129],[12290,16384,28674,9],[12290,16386,28672,9],[12290,16388,28678,9],[12290,16396,28686,9],[12290,16448,28738,9],[12290,16452,28742,9],[12290,16466,28752,9],[12290,16576,28866,9],[12290,16588,28878,9],[12290,16604,28894,9],[12290,17154,29440,9],[12290,17236,29526,9],[12290,19212,31502,9],[12290,19410,31696,9],[12290,20480,24578,129],[12290,20482,24576,129],[12290,20484,24582,129],[12290,20492,24590,129],[12290,20546,24640,129],[12290,20548,24646,129],[12290,20564,24662,129],[12290,20688,24786,129],[12290,20736,24834,129],[12290,20816,24914,129],[12290,20994,25088,129],[12290,20996,25094,129],[12290,22796,26894,129],[12290,23004,27102,129],[12290,23234,27328,129],[12290,23244,27342,129],[12292,16388,28672,9],[12292,20484,24576,129],[12294,16384,28678,9],[12298,16396,28678,9],[12298,20484,24590,129],[12300,16396,28672,9],[12302,20480,24590,129],[12304,16384,28688,9],[12304,16388,28692,9],[12304,16396,28700,9],[12304,16400,28672,9],[12304,16406,28678,9],[12304,16448,28752,9],[12304,16452,28756,9],[12304,16576,28880,9],[12304,16588,28892,9],[12304,16590,28894,9],[12304,17168,29440,9],[12304,17222,29526,9],[12304,19230,31502,9],[12304,19392,31696,9],[12304,20480,24592,129],[12304,20484,24596,129],[12304,20496,24576,129],[12304,20510,24590,129],[12304,20560,24640,129],[12304,20564,24644,129],[12304,20566,24646,129],[12304,20688,24768,129],[12304,20736,24848,129],[12304,20816,24896,129],[12304,21008,25088,129],[12304,21014,25094,129],[12304,22796,26908,129],[12304,23004,27084,129],[12304,23248,27328,129],[12304,23262,27342,129],[12306,16588,28894,9],[12306,20564,24646,129],[12308,16452,28752,9],[12308,20564,24640,129],[12318,16576,28894,9],[12352,16448,28672,9],[12352,20480,24640,129],[12354,16452,28678,9],[12354,20484,24646,129],[12356,16452,28672,9],[12356,20484,24640,129],[12358,16448,28678,9],[12358,20480,24646,129],[12368,16384,28752,9],[12372,16388,28752,9],[12372,20564,24576,129],[12378,20564,24590,129],[12380,16396,28752,9],[12432,16576,28752,9],[12432,20688,24640,129],[12438,20688,24646,129],[12442,16384,28826,9],[12442,16388,28830,9],[12442,16396,28822,9],[12442,16448,28890,9],[12442,16452,28894,9],[12442,16538,28672,9],[12442,16540,28678,9],[12442,16576,28762,9],[12442,16586,28752,9],[12442,16588,28758,9],[12442,17306,29440,9],[12442,17356,29526,9],[12442,19274,31696,9],[12442,19348,31502,9],[12442,20480,24730,129],[12442,20484,24734,129],[12442,20564,24782,129],[12442,20628,24590,129],[12442,20634,24576,129],[12442,20688,24650,129],[12442,20698,24640,129],[12442,20700,24646,129],[12442,20736,24986,129],[12442,20816,25034,129],[12442,21146,25088,129],[12442,21148,25094,129],[12442,22796,27030,129],[12442,23004,26950,129],[12442,23124,27342,129],[12442,23130,27328,129],[12444,16588,28752,9],[12446,16448,28894,9],[12480,16576,28672,9],[12486,16576,28678,9],[12490,16588,28678,9],[12492,16588,28672,9],[12496,20688,24576,129],[12498,16396,28894,9],[12506,16388,28894,9],[12510,16384,28894,9],[12510,20688,24590,129],[12544,20736,24576,129],[12558,20736,24590,129],[12560,20816,24640,129],[12566,20816,24646,129],[12608,20736,24640,129],[12614,20736,24646,129],[12624,20816,24576,129],[12638,20816,24590,129],[12800,20480,25088,129],[12802,20484,25094,129],[12804,20484,25088,129],[12806,20480,25094,129],[12882,20564,25094,129],[12884,20564,25088,129],[13008,20688,25088,129],[13014,20688,25094,129],[13056,16384,29440,9],[13056,20736,25088,129],[13058,16384,29442,9],[13058,16386,29440,9],[13058,16388,29446,9],[13058,16396,29454,9],[13058,16448,29506,9],[13058,16452,29510,9],[13058,16468,29526,9],[13058,16576,29634,9],[13058,16588,29646,9],[13058,17154,28672,9],[13058,17156,28678,9],[13058,17234,28752,9],[13058,17372,28894,9],[13058,18444,31502,9],[13058,18642,31696,9],[13058,20480,25346,129],[13058,20484,25350,129],[13058,20564,25430,129],[13058,20688,25554,129],[13058,20736,25090,129],[13058,20738,25088,129],[13058,20740,25094,129],[13058,20816,25170,129],[13058,21250,24576,129],[13058,21260,24590,129],[13058,21314,24640,129],[13058,21316,24646,129],[13058,22796,27150,129],[13058,22978,27328,129],[13058,22988,27342,129],[13058,23004,27358,129],[13060,16388,29440,9],[13062,20736,25094,129],[13068,16396,29440,9],[13072,16384,29456,9],[13072,16388,29460,9],[13072,16396,29468,9],[13072,16400,29440,9],[13072,16448,29520,9],[13072,16452,29524,9],[13072,16454,29526,9],[13072,16576,29648,9],[13072,16588,29660,9],[13072,17168,28672,9],[13072,17174,28678,9],[13072,17216,28752,9],[13072,17358,28894,9],[13072,18462,31502,9],[13072,18624,31696,9],[13072,20480,25360,129],[13072,20484,25364,129],[13072,20564,25412,129],[13072,20688,25536,129],[13072,20736,25104,129],[13072,20752,25088,129],[13072,20758,25094,129],[13072,20816,25152,129],[13072,21264,24576,129],[13072,21278,24590,129],[13072,21328,24640,129],[13072,21334,24646,129],[13072,22796,27164,129],[13072,22992,27328,129],[13072,23004,27340,129],[13072,23006,27342,129],[13074,16452,29526,9],[13074,23004,27342,129],[13078,16448,29526,9],[13084,23004,27328,129],[13120,16448,29440,9],[13124,16452,29440,9],[13136,20816,25088,129],[13138,16388,29526,9],[13142,16384,29526,9],[13142,20816,25094,129],[13146,16396,29526,9],[13206,16576,29526,9],[13210,16588,29526,9],[13248,16576,29440,9],[13250,22796,27342,129],[13260,16588,29440,9],[13260,22796,27328,129],[14594,22796,24590,129],[14604,22796,24576,129],[14666,22796,24646,129],[14668,22796,24640,129],[14746,23004,24646,129],[14748,23004,24640,129],[14802,23004,24590,129],[14812,23004,24576,129],[14864,20688,27328,129],[14878,20688,27342,129],[14996,20564,27328,129],[15002,20564,27342,129],[15040,20480,27328,129],[15044,20484,27328,129],[15050,20484,27342,129],[15054,20480,27342,129],[15104,16384,31488,9],[15104,16388,31492,9],[15104,16396,31500,9],[15104,16398,31502,9],[15104,16448,31552,9],[15104,16452,31556,9],[15104,16576,31680,9],[15104,16588,31692,9],[15104,16592,31696,9],[15104,18432,29440,9],[15104,18518,29526,9],[15104,19200,28672,9],[15104,19206,28678,9],[15104,19280,28752,9],[15104,19422,28894,9],[15104,20480,27392,129],[15104,20484,27396,129],[15104,20564,27476,129],[15104,20688,27600,129],[15104,20736,27136,129],[15104,20816,27216,129],[15104,20928,27328,129],[15104,20942,27342,129],[15104,22784,25088,129],[15104,22790,25094,129],[15104,22796,25100,129],[15104,23004,25308,129],[15104,23296,24576,129],[15104,23310,24590,129],[15104,23360,24640,129],[15104,23366,24646,129],[15106,16396,31502,9],[15114,16388,31502,9],[15114,22796,25094,129],[15116,22796,25088,129],[15118,16384,31502,9],[15120,16576,31696,9],[15132,16588,31696,9],[15178,16452,31502,9],[15182,16448,31502,9],[15248,16448,31696,9],[15248,20816,27328,129],[15252,16452,31696,9],[15258,16384,31642,9],[15258,16388,31646,9],[15258,16396,31638,9],[15258,16448,31706,9],[15258,16452,31710,9],[15258,16458,31696,9],[15258,16532,31502,9],[15258,16576,31578,9],[15258,16588,31574,9],[15258,18586,29440,9],[15258,18636,29526,9],[15258,19268,28894,9],[15258,19354,28672,9],[15258,19356,28678,9],[15258,19402,28752,9],[15258,20480,27546,129],[15258,20484,27550,129],[15258,20564,27598,129],[15258,20688,27466,129],[15258,20736,27290,129],[15258,20816,27338,129],[15258,20820,27342,129],[15258,20826,27328,129],[15258,22796,25238,129],[15258,22938,25088,129],[15258,22940,25094,129],[15258,23004,25158,129],[15258,23444,24590,129],[15258,23450,24576,129],[15258,23514,24640,129],[15258,23516,24646,129],[15262,20816,27342,129],[15296,20736,27328,129],[15298,16588,31502,9],[15310,16576,31502,9],[15310,20736,27342,129],[15312,16384,31696,9],[15316,16388,31696,9],[15322,23004,25094,129],[15324,16396,31696,9],[15324,23004,25088,129]]} diff --git a/research/bit-two-relation-any-registers/PROOF.md b/research/bit-two-relation-any-registers/PROOF.md new file mode 100644 index 0000000000..8dca10ed1d --- /dev/null +++ b/research/bit-two-relation-any-registers/PROOF.md @@ -0,0 +1,418 @@ +# Two exponent relations cannot amortize rank at any scalar width + +Prepared for **@CubeJerry** with substantial OpenAI Codex assistance. +New work is Apache-2.0. This is a written reduction to a named inherited +three-register theorem, not a proof-assistant formalization. The finite +controls corroborate the new lemmas; they do not establish unbounded +quantifiers by enumeration. + +## 1. Main theorem and exact inherited ingredients + +Let `H` be a torsion-free abelian group generated by finitely many +exponents `A_1,...,A_k`. Let `L` be the kernel of `Z^k -> H` sending +basis vector `j` to `A_j`. Write `[A][B]=[A+B]` in `R=F_2[H]`. +A scalar call on any finite number `W` of registers is + +\[ +D_j=I+([A_j]-1)N_j,\qquad N_j=x_jy_j^T,\quad +x_j,y_j\in\mathbb F_2^W,\quad y_j^Tx_j=1. +\] + +**Theorem.** If `rank L <= 2` and the exact whole-matrix endpoint is + +\[ +\prod_{j=1}^kD_j=\operatorname{diag}([C_1],\ldots,[C_W]), \tag{1} +\] + +then there are pairwise disjoint subsets `S_1,...,S_W` of the call +indices such that + +\[ +C_i=\sum_{j\in S_i}A_j. \tag{2} +\] + +The theorem allows arbitrary width and word length, repeated targets, +identity targets, and arbitrary diagonal monomial helper outputs. +Neither a frame-rank hypothesis, target invertibility, nor a fixed +address dimension is needed. For rational matrix exponents it implies + +\[ +\sum_i\operatorname{rank}_{\mathbb Q}C_i +\le\sum_j\operatorname{rank}_{\mathbb Q}A_j. \tag{3} +\] + +The scalar field is binary; rational address entries are never reduced +modulo two. Constant binary basis changes below are proof changes of +coordinates, not interposed free address transformations or a physical +implementation invoice. + +We use these precisely scoped inherited ingredients: + +* **Three-register disjoint subsets:** David Govea's CrocSwap/integer-mult-bounds#720, README + Sections 1--4, proves (2) at `W<=3`, for any torsion-free exponent + group and relation rank at most two. It permits identity and repeated + targets and arbitrary address ranks. Pad with identity coordinates + when `W<3`. We use this universal lemma, not CrocSwap/integer-mult-bounds#720's later finite + address-dimension-three word search. +* **Off-diagonal fibers:** Nick Petalas's CrocSwap/integer-mult-bounds#5921 proves that a realized + nonzero off-diagonal pattern has exactly one binary rank-one + idempotent lift, except a single edge `E_ab`, whose two lifts are + `E_aa+E_ab` and `E_bb+E_ab`. +* The cube-relation reduction below follows CrocSwap/integer-mult-bounds#720. The common-pattern + cyclic/acyclic organization follows woklerx's CrocSwap/integer-mult-bounds#1456. Their arguments + are recalled to make the new composition checkable. + +woklerx's CrocSwap/integer-mult-bounds#1846 already classifies all 4,964 four-register pattern +planes as reducible. We independently replay that finite result, but +the analytic scalar classification in Section 4 makes it unnecessary +as a proof dependency of this theorem. + +## 2. Saturation, augmentation and the free-coordinate split + +The generated group `H` is finitely generated and torsion-free, hence +free abelian. The sequence `0 -> L -> Z^k -> H -> 0` splits, so reduction +modulo two identifies the kernel of `F_2^k -> H/2H` with `L/2L`. +Expand the universal product `prod_j(I+(t_j-1)N_j)` at `t=1`. +Its first-order off-diagonal coefficient vectors belong to `L/2L` +by (1). Consequently the span of the occurring off-diagonal patterns +has dimension at most two. + +Only subset sums of frames occur in the universal product. A difference +of subset indicators is a *cube relation*, whose entries belong to +`{-1,0,1}`. If these relations span at most one rational dimension, let +`L_0` be their saturated span in `Z^k`. Then `L_0` is contained in `L` +and has rank at most one. Two subset sums coincide modulo `L` exactly +when they coincide modulo `L_0`, because their difference is itself a +cube relation. Replacing `H` by the torsion-free lift `Z^k/L_0` preserves +every coefficient fiber of the product and its diagonal monomial +endpoint. It suffices to prove (2) in the lift and map back. Its +first-order pattern span is at most one, handled in Section 3. + +Otherwise choose independent cube relations `r,s`. If their reductions +modulo two are independent, an odd `2 x 2` minor is `+1` or `-1`: cube +entries bound its absolute value by two. Thus they generate a saturated +rank-two lattice and form a basis of `L`. If their reductions coincide, +replace them by `(r+s)/2,(r-s)/2`. These are integral cube vectors +with disjoint nonempty supports and a unit minor, again a basis of `L`. +For this cube-valued basis there are binary off-diagonal matrices `B,C` +with + +\[ +\operatorname{offdiag}(N_j) +=(r_j\bmod2)B+(s_j\bmod2)C. \tag{4} +\] + +Pattern span at most one is covered by Section 3. If its dimension is +two, `B,C` are independent. Let `S` index noncoordinate projectors and +`T` coordinate projectors. For `j in T`, (4) forces `r_j=s_j=0` +modulo two, hence integrally because they are cube-valued. Every +relation is supported on `S`, and + +\[ +H\simeq (\mathbb Z^S/L)\oplus\mathbb Z^T=H_S\oplus\mathbb Z^T. \tag{5} +\] + +Thus the coordinate calls have independent free exponent coordinates. +Projecting onto `H_S` removes all of them and preserves a diagonal +endpoint. Section 5 will return them to their original target labels. +This exact lattice split is essential; arbitrary coordinate gates +cannot be added to a noncoordinate pool's invariant-subspace claim. + +## 3. A common pattern at arbitrary width and at most two relations + +If all patterns vanish, every projector is a coordinate projector and +(2) is immediate. If the common nonzero pattern is acyclic, a common +coordinate order makes every projector, including coordinate gates, +triangular. A rank-one idempotent then has exactly one nonzero diagonal +entry. Product diagonals give disjoint subsets. + +In the cyclic case the pattern uniquely determines a projector `N=xy^T`, +as in CrocSwap/integer-mult-bounds#1456 or the fiber lemma. Let `I=supp(x) intersect supp(y)`. +All directed cycles are in `I`, where the graph is complete off the +diagonal. Its size `s` is odd by idempotence, and cyclicity forces +`s>=3`. Order coordinates in `supp(x)\supp(y)`, then `I`, then +`supp(y)\supp(x)`; all other coordinates are isolated. The common +projector and every coordinate projector become block upper triangular. +The only nonzero diagonal block of `N` is the all-ones idempotent `J_s`. +Outside it, singleton targets are sums of their own coordinate-call +frames. The core subword still has relation rank at most two: its +relations embed into the original lattice by zero extension. + +It remains to generalize the common-J argument of CrocSwap/integer-mult-bounds#720 Section 3. + +**Common-J lemma.** For every odd `s>=3`, a word with projectors in +`{J_s,E_11,...,E_ss}`, relation rank at most two and diagonal monomial +endpoint has the same endpoint after deleting all J factors. + +Write augmentation variables `u_j=t_j-1`, and let `L_J` be their sum +over J calls. If none occurs there is nothing to prove. Otherwise +`L_J` is a nonzero universal linear form and first-order off-diagonal +vanishing puts it in the at-most-two-dimensional linear relation space. +For coordinate `i` set + +\[ +K_i=\operatorname{offdiag}(J_sE_{ii}+E_{ii}J_s),\qquad +q_i=\sum_{j:N_j=E_{ii}}u_j\sum_{a=3`. The Laurent domain gives `d_j=d_k`, so `D=dI`. Oddness of `s` +makes `J_s` idempotent, and the word is `d U(bc)`. Diagonality forces +`bc=1`, leaving exactly `D`. Restoring exterior factors proves the +common-J lemma. Together with the triangular tails this establishes +(2) whenever the pattern span has dimension at most one, at any width. + +## 4. Joint-image classification for every two-pattern pool + +Let `P` be a two-dimensional space of off-diagonal binary matrices in +`M_W(F_2)`. Its *noncoordinate pool* contains every rank-one idempotent +whose nonzero pattern lies in `P`. + +**Joint-image lemma.** Either the pool's joint image has dimension at +most **three**, or the pool consists of exactly the four lifts of two +single edges on four distinct coordinates. That exceptional pool is +coordinate triangular and has joint-image dimension four. + +We use the fiber lemma of CrocSwap/integer-mult-bounds#5921. A single edge `E_ab` has exactly the +lifts + +\[ +E_{aa}+E_{ab}=e_a(e_a+e_b)^T,\qquad +E_{bb}+E_{ab}=(e_a+e_b)e_b^T, \tag{8} +\] + +whose images span `e_a,e_b`. Every other realized nonzero pattern has +one lift. For completeness, two distinct lifts differ by a nonzero +diagonal matrix of rank at most two and trace zero, hence supported +on exactly two diagonal positions. Both their image and covector +spaces lie in those positions; the six binary `2 x 2` rank-one +idempotents give exactly (8). This fiber theorem is inherited, not +claimed as new. + +There are at most three realized nonzero patterns. If all three are +realized and none is a single edge, only three projectors occur, so +the image bound follows. Suppose exactly one is a single edge +`p=E_ab`, with the other two patterns `q,r=q+p` represented uniquely +by `M=xy^T`, `N=uv^T`. Then + +\[ +K=M+N=E_{ab}+D,\quad D\text{ diagonal},\quad +\operatorname{rank}K\le2,\quad\operatorname{tr}D=0. \tag{9} +\] + +The diagonal support of `D` has size at most three since +`rank D <= rank K+1`. It has even size by trace zero. Therefore +`D=0` or `D=E_cc+E_dd` for distinct `c,d`. + +If `D=0`, either `x,u` agree or they are independent. In the latter +case the rank-one sum `K` forces `y=v`; then `(x+u)y^T=E_ab` gives +`x+u=e_a`. In either case adding the edge-lift image span +`span(e_a,e_b)` to `im M+im N` gives dimension at most three. + +If `D=E_cc+E_dd`, the sets `{c,d}` and `{a,b}` must intersect. +Otherwise columns `b,c,d` of `K` are the three independent vectors +`e_a,e_c,e_d`. In every allowed case `rank K=2`: the principal minor +on `c,d` is an identity matrix possibly with one off-diagonal entry, +so has determinant one. Thus `im M+im N=im K`. Adding `e_a,e_b` +is contained in the coordinate union `{a,b,c,d}`, now of size at +most three. + +If all three patterns are realized and two are single edges, their +sum has exactly two off-diagonal entries. A rank-one idempotent +realizing that sum has support intersection of size one: a cyclic +intersection has odd size at least three and at least six edges. +For the two disjoint tails' sizes `a_0,b_0`, the edge count is +`a_0+b_0+a_0 b_0=2`, forcing `(a_0,b_0)=(2,0)` or `(0,2)`. +The two edges share a row or a column and use three coordinates. +All five possible lifts are supported there, so again the joint +image has dimension at most three. A two-dimensional space cannot +contain three distinct matrix units, since they are linearly +independent. + +If fewer than three patterns are realized, there are at most three +projectors unless both realized patterns are single edges. Their four +lifts have joint image equal to the coordinate span of their endpoints. +This is at most three-dimensional unless all four endpoints differ. +In that exceptional case the edges are disjoint, and a coordinate +order making both edges upper triangular triangularizes the entire +pool. This proves the lemma in every ambient dimension. + +The sharp example is `P=span(E_01,E_23)`. Its four lifts have independent +joint image; the third pattern is unrealized. The joint-image maximum +is therefore four, improving the cardinality-derived image bound five +in CrocSwap/integer-mult-bounds#5921. That predecessor's sharp pool-cardinality maximum five is +unchanged. The new statement identifies precisely every image-dimension- +four case, rather than merely checking fixed small register counts. + +## 5. Restrict the image and reconstruct every original target + +In the remaining pattern-span-two case use the split (5), and project +away all coordinate calls `T`. The remaining endpoint is diagonal, +possibly with additional equal or zero target exponents. Apply the +joint-image lemma to its complete pattern pool. + +For the exceptional disjoint-edge pool, coordinate triangularity +assigns disjoint frame subsets directly. Otherwise let `V` be its +joint image, of dimension at most three. Every projector preserves +`V` and induces zero on the quotient. The endpoint also preserves +`V tensor R`. + +The invariant subspace need not be spanned by original coordinate +vectors. For each distinct projected target exponent `h`, let `E_h` +be the span of original coordinate vectors with that value, and +`pi_h` the coordinate projection. For `v in V`, + +\[ +Dv=\sum_h[h]\pi_hv\in V\otimes R. +\] + +Mapping to `(F_2^W/V) tensor R` and using linear independence of +monomials gives `pi_h v in V` for every `h`. Consequently + +\[ +V=\bigoplus_h(V\cap E_h). \tag{10} +\] + +Choose a binary basis within each `E_h` adapted to this intersection, +and put the basis vectors of `V` first. The endpoint stays diagonal +with its original monomial multiset, while all projectors are block +upper triangular. Each restricted projector on `V` is rank one and +idempotent: its nonzero image vector lies in `V` and is fixed by it. +All quotient projectors vanish, so the quotient endpoint is identity. +On each complementary equal-value block that endpoint is multiplication +by `[h]`; hence every quotient label has `h=0`, since distinct group +elements are distinct basis monomials. + +The relation lattice of the restricted word is unchanged; more generally, +removing identity factors embeds its relation lattice by zero extension +and cannot increase its rank above two. Apply the inherited +three-register disjoint-subset lemma to `V`, padding with identity +coordinates if needed. Match its target monomials, with multiplicity, +to original projected target labels. The quotient labels all have +zero exponent and receive empty subsets. Repeated target values pose +no problem: choose any matching inside each equal-value class. + +Finally project (1) onto a free generator `t in T`. Its only surviving +call is its original coordinate projector `E_ii`; thus its exponent +belongs to exactly original target `i`. Append that index to target +`i`'s assigned subset. The direct sum (5) makes the reconstructed +exponent equal to the full original target. The assignments remain +pairwise disjoint. This completes the theorem for every `W`. + +## 6. Rank consequence and historical boundary + +Apply rank subadditivity to (2) to obtain (3). With rational rank-one +paid frames, any saving below total target rank therefore requires +**at least three independent rational frame relations**, regardless +of register count, address dimension or diagonal helper outputs. + +For eight calls and three invertible rational `3 x 3` data targets, +frame span at least six gives relation rank at most two but total +target rank at least nine. Such a word is impossible even with +arbitrarily many dirty auxiliary inputs and arbitrary diagonal +monomial auxiliary outputs. + +The four-register span-six case was already covered by CrocSwap/integer-mult-bounds#4119, CrocSwap/integer-mult-bounds#5075, +CrocSwap/integer-mult-bounds#5231 and CrocSwap/integer-mult-bounds#5552. Spans at least seven were already excluded at arbitrary +width by the one-relation work. The new span-six consequence extends +the helper width, and follows from a theorem at every word length. +JoyboyBrian's CrocSwap/integer-mult-bounds#5481 already excludes the five-call `2 x 2` block with +arbitrary diagonal auxiliaries and closes eight-call frame spans at +most four. Combining those earlier results with the present theorem +leaves frame span five as the remaining eight-call case in this formal +alphabet. This is not a claim that a span-five construction exists. + +The six-call span-three fixture in the verifier is a known sharpness +and scope control, not a new construction or closure of CrocSwap/integer-mult-bounds#5481. This +package supplies no new supplier, physical implementation, recursive +invoice or multiplication exponent. **No new κ.** + +## 7. Verification and provenance + +The proof depends on CrocSwap/integer-mult-bounds#720's precise universal three-register lemma. +That lemma is inherited, not newly proof-kernel verified here. The +CrocSwap/integer-mult-bounds#5921 fiber lemma is credited and recalled; CrocSwap/integer-mult-bounds#1456 and CrocSwap/integer-mult-bounds#720 supply the +common-pattern and augmentation framework. The final analytic proof +does not depend on the finite 4,964-plane census, though our certificate +independently replays CrocSwap/integer-mult-bounds#1846 and checks that the new structural statement +agrees with every pool there. + +Further finite controls check all 108,165 generated pattern planes +on five registers, 20,097 bounded common-J prefix placements, whole +formal endpoints and meaningful rejected mutations. They corroborate +specific lemmas; they do not prove arbitrary width, word length or +rational-lattice statements by sampling. No unrelated full CrocSwap/integer-mult-bounds#468/#720 +address-dimension-three search is rerun. + +Base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. Exact source pins are in +SOURCES.json. The initially assigned five-call restored-helper question +was found already solved by CrocSwap/integer-mult-bounds#5481; the lead explicitly reassigned the +scope to the arbitrary-width two-relation question left in CrocSwap/integer-mult-bounds#1456, +CrocSwap/integer-mult-bounds#1846 and CrocSwap/integer-mult-bounds#5921. The selected conditional bound and all five inherited +assumptions remain unchanged. + +Credit eumemic's CrocSwap/integer-mult-bounds#288 formal model; Ali Romman's CrocSwap/integer-mult-bounds#468 relation and rank +methods; David Govea's CrocSwap/integer-mult-bounds#720 theorem/common-J proof; woklerx's CrocSwap/integer-mult-bounds#1456 +one-relation result and CrocSwap/integer-mult-bounds#1846 classification; Nick Petalas's CrocSwap/integer-mult-bounds#5921 fiber +and cardinality theorem; JoyboyBrian's CrocSwap/integer-mult-bounds#5481 five-call obstruction; +Josie Elliston's CrocSwap/integer-mult-bounds#6055 independent short-word census; and the cited +four-register span-six contributors. @CubeJerry's CrocSwap/integer-mult-bounds#6760 compression +motivated the original assignment but is not a proof dependency of the +final result. Substantial OpenAI Codex assistance includes separately +assigned mathematical review. No human or proof-kernel acceptance is +asserted. diff --git a/research/bit-two-relation-any-registers/README.md b/research/bit-two-relation-any-registers/README.md new file mode 100644 index 0000000000..f888fe1683 --- /dev/null +++ b/research/bit-two-relation-any-registers/README.md @@ -0,0 +1,196 @@ +# Two frame relations cannot share rank, at any register count + +**Scoped universal lower bound. No new κ.** In the formal binary +scalar-idempotent model, a word with at most two independent integral +relations among its address frames cannot save paid rank, regardless +of its number of scalar registers or diagonal auxiliary outputs. + +More precisely, every target address in a diagonal monomial endpoint +is a sum of a disjoint subset of the paid addresses. For rational +matrix frames this gives + +\[ +\sum_i \operatorname{rank}_{\mathbb Q} C_i +\le \sum_j \operatorname{rank}_{\mathbb Q} A_j. +\] + +Thus rank-one calls need **at least three independent frame relations** +to beat total target rank. In particular, eight calls for three +invertible `3 x 3` targets cannot have frame span six, even with +arbitrarily many dirty auxiliaries and arbitrary diagonal monomial +auxiliary outputs. Combined with earlier results, frame span five is +the remaining eight-call case in this formal alphabet. + +## What is new relative to the archive + +The result extends David Govea's three-register disjoint-subset theorem +in CrocSwap/integer-mult-bounds#720 and woklerx's arbitrary-register +one-relation bound in CrocSwap/integer-mult-bounds#1456. It resolves +their missing width/two-relation combination by three compatible steps: + +1. A common cyclic pattern reduces to an odd all-ones core. The + quadratic prefix argument is extended to **every odd core size**, + proving that its noncoordinate calls cancel at a diagonal endpoint. +2. A two-pattern noncoordinate pool has joint image dimension at most + **three**, except the four lifts of two disjoint single edges, + which are coordinate triangular. This is a written classification + for every width. Its sharp maximum image dimension four improves + the bound five obtained from the pool-cardinality theorem in + CrocSwap/integer-mult-bounds#5921; that predecessor's sharp + cardinality theorem remains unchanged. +3. A saturated cube-valued relation basis separates intervening + coordinate calls as free exponent generators. Restrict the remaining + word to its small image, apply the inherited three-register theorem, + then reconstruct every original target, including repeated values. + +[PROOF.md](PROOF.md) supplies each step and its exact inherited hypotheses. +The final analytic proof does not depend on a new finite scalar census. +[REVIEW.md](REVIEW.md) records a separate written mathematical review and +an alternate target-label argument. It checks the precise inherited +CrocSwap/integer-mult-bounds#720 scope without claiming a new proof of that +three-register theorem or a replay of its unrelated address search. +We credit and independently replay woklerx's **existing** 4,964-plane +classification in CrocSwap/integer-mult-bounds#1846 as corroboration. + +Several narrower results were already established and are not claimed +as new here. JoyboyBrian's CrocSwap/integer-mult-bounds#5481 excluded +five calls for three invertible `2 x 2` targets with arbitrary diagonal +auxiliaries, closing the span-four handoff in +CrocSwap/integer-mult-bounds#4118. Josie Elliston's +CrocSwap/integer-mult-bounds#6055 independently enumerated the five-call +case through five registers. The **four-register** span-six case was +closed by CrocSwap/integer-mult-bounds#4119, +CrocSwap/integer-mult-bounds#5075, CrocSwap/integer-mult-bounds#5231 and +CrocSwap/integer-mult-bounds#5552. The new theorem is at arbitrary +width, arbitrary word length, and arbitrary address dimension. + +## Exact evidence and verification boundary + +The universal proof is written. Its central inherited dependency is +CrocSwap/integer-mult-bounds#720's three-register relation theorem, not +that package's later address-dimension-three search. That theorem is +**inherited, not newly formally verified here**. Nick Petalas's +CrocSwap/integer-mult-bounds#5921 off-diagonal fiber lemma is credited +and recalled in the proof. No unmerged source or network fetch is +needed to run the standalone checker. + +The finite tests corroborate precise parts of the argument: + +| Check | Executed domain | +| --- | --- | +| Historical four-register alphabet | All 65,536 binary matrices; exactly 120 rank-one idempotents | +| Historical pattern-plane replay | All 104 nonzero patterns and 4,964 generated planes | +| Certificate coverage | Every plane once; every projector preserves its explicit proper-subspace witness | +| Invariant block reduction | All 3,600 invariant projector/subspace pairs on four registers | +| Sharp joint-image classification | Every generated pattern plane at widths 2, 3, 4, 5: 1, 129, 4,964, 108,165 planes | +| Equality cases | Exactly 12 image-dimension-four pools at width four and 60 at width five; all are disjoint-edge pools | +| Odd-core quadratic mechanism | 20,097 prefix-placement cases at core sizes 3, 5, 7 and J-call counts 2, 3, 4, one coordinate occurrence per role | +| Whole formal endpoints | Odd-core cancellation and noncancellation words; a six-call rational span-three fixture | +| Failure controls | Omitted plane, proper but noninvariant witness, deleted paid calls, missing helper cleanup, separated internal gaps | +| Scope controls | Irreducible odd-width common-J alphabet, nontriangular three-coordinate subblock, intervening coordinate gates, and repeated-target eigenspaces | + +[CERTIFICATE.json](CERTIFICATE.json) records all 4,964 invariant-space +witnesses. [verify.py](verify.py) regenerates the complete domain and +checks each witness directly. Its structural census uses a separate +outer-product enumeration at widths through five. The universal proof +does not extrapolate those finite counts. + +The six-call fixture has integer frames `2 E11, 2 E22`, then +`2 E11, 4 E22`, then `3 [[1,1],[1,1]], [[1,-1],[-1,1]]` on the three +data coordinates. These span the symmetric `2 x 2` space and produce +`2 I`, `diag(2,4)`, `[[4,2],[2,4]]`, while helpers remain identity. +Their target relatives have commutator determinant one, so no common +algebraic flag is silently assumed. This is a sharpness control, +not a new construction. Even address entries remain nonzero; only +scalar coefficients use characteristic two. + +## Reproduce + +From the repository root, Python 3.12 and its standard library suffice: + +```sh +python3 -I -W error -B research/bit-two-relation-any-registers/verify.py +``` + +Expected first line: + +``` +PASS_TWO_RELATION_ANY_REGISTERS +``` + +The next JSON line gives every count above. The same complete check +is registered normally and with Python assertions disabled: + +```sh +python3 -I -O -W error -B research/bit-two-relation-any-registers/verify.py +python3 -B scripts/research_package.py --package research/bit-two-relation-any-registers --check-only +python3 -B scripts/research_package.py --package research/bit-two-relation-any-registers +``` + +Regenerate certificate bytes without changing the tracked file: + +```sh +python3 -I -B research/bit-two-relation-any-registers/verify.py --emit-certificate /tmp/two-relation-certificate.json +cmp research/bit-two-relation-any-registers/CERTIFICATE.json /tmp/two-relation-certificate.json +``` + +There is no random seed: domains are deterministic and fully exhausted +at the stated widths and prefix bounds. This is not a word search over +`120^5` cases. No native compiler, solver or third-party library is used. +Metadata validation authenticates the canonical provenance in +[SOURCES.json](SOURCES.json); the direct verifier is self-contained. +[VERIFY.json](VERIFY.json) declares no external live scientific inputs. + +## Scope, assumptions and provenance + +Base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`; catalogue revision 8; +seed 12, card `bit-new-register-model`. [TASK.json](TASK.json) retains +the full original card, the explicit scope change and stopping rule. +The original five-call question had already been solved; the contribution +addresses the remaining arbitrary-width two-relation question identified +across CrocSwap/integer-mult-bounds#1456, +CrocSwap/integer-mult-bounds#1846 and CrocSwap/integer-mult-bounds#5921. + +The theorem requires a torsion-free exponent group, binary rank-one +idempotent scalar calls, and exact whole-matrix diagonal monomial +endpoints. Helpers may be arbitrary inputs and may return arbitrary +diagonal monomials; exact identity restoration is a special case. +Finite-address coincidences, approximate endpoints, discarded or +zero-initialized-only inputs, nondiagonal outputs, nonabelian address +operations and other scalar fields are outside the theorem. + +The selected conditional κ remains `0.003125804` at the pinned base. +Native all-columns, owned erasure, compiler, precision/tape and analytic +recovery assumptions are unchanged. No complete supplier, physical +cost invoice or multiplication improvement follows from this obstruction. + +## Open next questions + +1. **Eight calls at frame span five.** This gives three independent + relations and is the remaining formal three-target case after the + older low-span results and this theorem. Begin with rank-three cube + relation lattices and the associated three-dimensional spaces of scalar + patterns. Unlike rank two, independent cube relations need not have a + unit minor; the free-coordinate split requires new saturation work. +2. **Sharp joint-image dimension for three-dimensional pattern spaces.** + Three disjoint edges give image dimension six, while + CrocSwap/integer-mult-bounds#5921 gives the upper bound ten from + cardinality. Extend the diagonal-difference argument before launching + a large pool search. A better width reduction would help the span-five + question, but does not itself prove a three-relation word theorem. + +## Credit and license + +Prepared for **@CubeJerry** with substantial OpenAI Codex assistance +for mathematical development, exact checking and separately assigned +adversarial review. No independent human acceptance or proof-assistant +certification is claimed. New files are **Apache-2.0**. + +Credit eumemic's CrocSwap/integer-mult-bounds#288 model; Ali Romman's +CrocSwap/integer-mult-bounds#468 scalar/relation framework; David Govea's +CrocSwap/integer-mult-bounds#720 theorem and common-J proof; woklerx's +CrocSwap/integer-mult-bounds#1456 and CrocSwap/integer-mult-bounds#1846; +Nick Petalas's CrocSwap/integer-mult-bounds#5921 fiber/cardinality theorem; +and the predecessors identified above. @CubeJerry's +CrocSwap/integer-mult-bounds#6760 compression motivated the original +assignment but is not a dependency of the final theorem. diff --git a/research/bit-two-relation-any-registers/REVIEW.md b/research/bit-two-relation-any-registers/REVIEW.md new file mode 100644 index 0000000000..35fc0a940b --- /dev/null +++ b/research/bit-two-relation-any-registers/REVIEW.md @@ -0,0 +1,232 @@ +# Independent review: two exponent relations at arbitrary scalar width + +Prepared for Jerry Chen / @CubeJerry with substantial OpenAI Codex assistance. +Apache-2.0. This is an independent written mathematical review, not external +human review or proof-kernel verification. No second copy of the author's +finite census was run for this review. + +Reviewed objects: + +- `research/bit-two-relation-any-registers/PROOF.md`, Sections 1–7. +- David Govea's CrocSwap/integer-mult-bounds#720, canonical base + `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, + `research/three-register-no-target-flag/README.md`, especially Sections 1–4. + +The new theorem is precisely about binary rank-one idempotent scalar calls +over the formal group algebra of a finitely generated torsion-free exponent +group, with at most two independent integer relations and an exact diagonal +monomial endpoint. It does not concern arbitrary scalar fields, torsion +relations, address changes between calls, or finite-address coincidence. + +## Review conclusion + +I find the new arbitrary-width reduction valid. The common-J argument extends +to every odd core size, the two-pattern image classification is exhaustive +without an ambient-width bound, and original repeated or identity target +labels can be recovered. The exact inherited #720 lemma has the needed +torsion-free, at-most-two-relation scope; it has no frame-rank, target-rank, +invertibility, flag or target-distinctness hypothesis. + +The conclusion remains a written theorem depending on that named inherited +three-register result. This review did not rerun #720's finite classification +or its unrelated address-dimension-three search. It also does not newly verify +every older low-span result cited for the historical eight-call summary. + +## 1. Saturation and the cube lift + +Because the finitely generated exponent group H is torsion-free, the exact +sequence from Z^k splits. Thus the mod-two linear relation space is exactly +L/2L, rather than a larger kernel created by torsion. First-order off-diagonal +coefficient vectors therefore span at most rank(L) directions. + +Every universal product entry is multilinear in the individual call variables: +each call contributes either its constant matrix part or one occurrence of its +own variable. Consequently a collision between two contributing exponent +monomials has a relation vector in {-1,0,1}^k. Saturating the rational span of +all such cube relations cannot introduce a new equality between subset sums, +and removes none. If that span has rank at most one, the resulting torsion-free +lift preserves all coefficient fibers. Each endpoint monomial has at least +one subset representative, so the lifted diagonal endpoint is well defined +as well; repeated or identity target values remain consistent. The returned +disjoint subsets map back to the original exponents. + +If two independent cube relations exist, the claimed saturated basis argument +is sound. Independent mod-two reductions give an odd 2-by-2 minor, necessarily +plus or minus one because its absolute value is at most two. Coincident +nonzero reductions give two integral half-sums with disjoint nonempty support +and a unit minor. Their membership in L uses saturation, equivalently +torsion-freeness of H. Since rank(L) is at most two, either basis spans all +of L integrally. + +In the pattern-span-two case, a coordinate projector has zero pattern, hence +both basis-relation coefficients there are zero modulo two. Cube-valued +coefficients make them zero as integers. This proves the direct sum +H=H_S plus Z^T and justifies removing coordinate calls before applying a +noncoordinate invariant-image argument. Without this step, the claimed +common image would not in general be invariant under arbitrary coordinate +projectors. + +## 2. Arbitrary odd common-J cores + +A cyclic rank-one binary idempotent has an odd support intersection of size +s at least three. Its off-diagonal graph gives upper-triangular tails around +an all-ones J_s core. Coordinate projectors preserve that block order. +The diagonal endpoint outside the core is already the disjoint product of +the corresponding coordinate calls, and the core relation lattice embeds +into the original lattice by zero extension. + +The following points make the degree-two argument valid rather than a +first-order heuristic: + +1. The universal first-order off-diagonal expression is a multiple of the + constant matrix `(J_s)_off`. Quotienting that matrix direction kills the + entire first-order expression before any Laurent substitution. Therefore + quadratic terms introduced by nonlinear substitutions into a surviving + universal linear term cannot interfere: no such term survives. +2. The associated graded augmentation ring of F2[H] is the polynomial ring + Sym(H/2H). After eliminating the nonzero J-sum relation L_J, at most one + further linear relation M remains. A nonzero homogeneous quadratic that + vanishes in the quotient is therefore divisible by M. +3. For the star matrices K_i, an equation sum(a_i K_i)=lambda J_off means + a_i+a_j=lambda for every distinct i,j. A triangle forces lambda=0; + then all a_i are equal. Thus the only star relation, even after this + matrix quotient, is their total sum. This works for every s at least + three, not just s=3. + +Eliminating the last J variable leaves independent proper J-prefix forms +P_1,...,P_(h-1). Every remaining quadratic q_i+q_s is bilinear between J +variables X and coordinate-call variables Y. If a nonzero bilinear +polynomial factors into two linear forms, its pure X and pure Y degree-two +parts must vanish. Since a polynomial ring over F2 is a domain, one factor +must be purely X and the other purely Y. Its coefficient matrix has rank one. +All its nonzero columns are therefore the same prefix P_j; distinct proper +prefixes are independent and cannot lie on one binary line. + +The common-divisor condition synchronizes the gap across all coordinates. +If q_s is nonzero, its own columns occur in every q_i+q_s, so their rank-one +prefix must agree. If q_s is zero, different nonzero q_i have disjoint +Y-variable supports; they cannot share a nonzero Y divisor. Their common +divisor is consequently the same X prefix. If just one quadratic is +nonzero, its own rank-one condition is enough. If all these quadratics are +identically zero before the final relation M, disjoint Y supports force all +q_i to vanish identically and there are no internal coordinate calls. + +This reduces the word to U(b) D U(c) after removing exterior invertible +diagonal factors. If either b or c equals one, an off-diagonal equation +forces the other to equal one. Otherwise subtracting two columns in a third +row gives `(b-1)(d_j-d_k)=0`. The Laurent domain and s at least three force +D=dI. Since J_s is idempotent for odd s, the remaining word is d U(bc), +whose off-diagonal equations force bc=1. Its endpoint is exactly the one +obtained by deleting all J calls. No word-length or core-size enumeration +is used in this conclusion. + +The phrase "all quadratics vanish" should consistently mean universal +vanishing after L_J has been eliminated and before imposing M; vanishing +modulo M alone would not imply the absence of internal coordinate calls. +The current argument uses the former meaning. + +## 3. The joint-image classification is exhaustive + +I checked all structural cases independently of the finite 4- and 5-register +data. + +Two distinct lifts of one nonzero off-diagonal pattern differ by a nonzero +diagonal matrix of rank at most two and trace zero. It therefore has exactly +two supported diagonal entries. Rank equality forces both images and both +covectors into those two coordinates. The binary 2-by-2 rank-one idempotents +give exactly the two stated lifts of a single edge; other realized nonzero +patterns have one lift. + +A two-dimensional pattern plane has only three nonzero elements. With no +edge ambiguity there are at most three projectors, giving image dimension +at most three. With exactly one edge and all three patterns realized, +write the other lifts as M,N and M+N=E_ab+D. Rank subadditivity bounds the +diagonal support of D by three, and trace parity makes it zero or two. + +- If D=0 and the two image vectors are independent, rank(M+N)=1 forces + their covectors equal and their image sum to e_a. Adding e_a,e_b thus + still spans at most three dimensions. Dependent images are easier. +- If D has support {c,d}, disjointness from {a,b} would produce three + independent columns, contrary to rank at most two. Its principal + {c,d} minor has determinant one, so rank(M+N)=2 and its image equals + the joint image of M,N. All image vectors then lie in the union of + at most three coordinate positions. + +With two edges and their sum realized, the latter has only two off-diagonal +entries. Its support intersection cannot have cyclic size at least three, +which would already create six edges. For intersection size one, the tail +sizes satisfy a+b+ab=2, forcing (2,0) or (0,2). Thus the two edges share a +row or a column and all lifts are supported on three coordinates. + +If only two edge patterns are realized, their four lifts span their +endpoints. The only image-dimension-four case has four distinct endpoints. +Those disjoint edges are simultaneously coordinate upper triangular, and +their sum is unrealizable by the preceding two-edge count. This proves the +claimed exception and rules out an unexamined high-width case. The sharp +pool span(E_01,E_23) also prevents incorrectly strengthening the bound to +three without the triangular exception. + +## 4. Independent target-label argument + +The author's invariant-eigenspace decomposition is valid: monomial +independence applied to a constant vector in V separates each distinct +target exponent's coordinate projection. Repeated target values require +grouping equal monomials, which the proof does. + +There is a stronger direct argument in this setting. Because every N_j has +image in V, a telescoping product identity gives + + (D-I)(F2^W tensor R) contained in V tensor R. + +For original target label i with projected exponent h_i not zero, +`(D-I)e_i=([h_i]-1)e_i`. Its image in the constant-vector quotient by V +can vanish only if e_i lies in V: apply a binary linear functional nonzero +on that quotient vector and use `[h_i]-1 != 0`. Consequently every original +nonzero-target coordinate axis lies in V, and + + V = span{e_i: h_i != 0} direct-sum (V intersect E_0). + +Choose those original nonzero target axes themselves in the restricted +basis, followed by a basis of the zero-target intersection. This retains +every nonzero target label directly, even when its exponent is repeated. +All quotient target labels have zero exponent. Each restricted projector +is still rank one and idempotent because its nonzero image vector lies in +V and is fixed. Applying the inherited three-register lemma is therefore +legitimate after padding if necessary. Any subsets assigned to artificial +zero-target basis vectors can simply be discarded; their sums are zero. + +Finally, projecting onto a free coordinate-call generator leaves only its +original coordinate projector. Formal monomial equality assigns that +generator to exactly its original target label with coefficient one, +and coefficient zero to all others. Reattaching these calls preserves +disjointness and reconstructs the full exponent by the exact direct sum. +No free scalar-basis transformation has been asserted as a physical gate. + +## 5. Quantifiers and consequences + +Every argument above is independent of W and k. The only finite width used +as an inherited mathematical theorem is at most three, reached by an +analytic image reduction. The disjoint-edge exception is solved directly +by triangular diagonals rather than by the 4,964-plane census. Thus the +finite 4- and 5-register checks corroborate the new structural lemma; they +do not carry the arbitrary-width quantifier. + +For rational matrix exponents the group map is additive over the rationals, +while scalar projectors remain binary. Rational address entries are not +reduced modulo two. Disjoint subset assignment and ordinary matrix-rank +subadditivity give total target rank no larger than total paid frame rank. +In particular, three invertible 3-by-3 targets require at least nine total +rank-one calls whenever the frame-relation rank is at most two, regardless +of additional diagonal monomial helper outputs. + +This proves no kappa improvement, physical supplier admission, recursive +cost model or unrestricted lower bound for three or more frame relations. +The historical remaining span-five case uses the separately cited earlier +low-span results as well as this theorem; it is not a new assertion that a +span-five construction exists. + +## Author response and final proof pin + +The requested distinction between universal quadratic vanishing and vanishing +modulo M is now explicit in PROOF.md. This clarifies the reviewed argument. +Final proof SHA256: `ad05bccffaf0fe11120312d8514146e5433d7032bbc65bd9d57974e06a6c3f82`. diff --git a/research/bit-two-relation-any-registers/SOURCES.json b/research/bit-two-relation-any-registers/SOURCES.json new file mode 100644 index 0000000000..5b0cf1290d --- /dev/null +++ b/research/bit-two-relation-any-registers/SOURCES.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "role": "Selected baseline at assignment" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81", + "role": "Original task and priority revision" + }, + { + "path": "research/bit-fivecall-dirty-block/PROOF.md", + "usage": "provenance", + "git_blob": "dc10506db48c67040c0743296cc0af13c85fc1c3", + "sha256": "9bae10083e68fb1bccf38827741100e394a5e66b19f7020d6c90fad8887dc50c", + "role": "Prior arbitrary-helper fivecall and span-four closures", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/5481" + }, + { + "path": "research/bit-four-role-two-patterns/README.md", + "usage": "provenance", + "git_blob": "e79087d9cd8f4473e6e48fa4e521902b7809f3a4", + "sha256": "e4ee830e783b20bfb0886ae8c91133a6138157ed5dcaac90ce16ddc616c8d49f", + "role": "Existing finite4964 census, independently replayed but not a final proof dependency", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1846" + }, + { + "path": "research/bit-one-relation-any-registers/PROOF.md", + "usage": "provenance", + "git_blob": "9b42c6cd2e93514bd8c5247e2ef2d516d6603ae6", + "sha256": "38805f881d0bd625418fd8bdc9410d06fe3873374db9678c722d13abd3bfe392", + "role": "Common-pattern framework and predecessor one-relation bound", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1456" + }, + { + "path": "research/bit-span4-five-call-two-relation/README.md", + "usage": "provenance", + "git_blob": "a8cf0a663e479b5570fc6e20a3eaff4db14e6ddf", + "sha256": "5af44cffa72cad900a0c367986cec6fd17448b7ceec2b8d145ee7554d62f465a", + "role": "Independent W<=5 fivecall corroboration, not a proof dependency", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/6055" + }, + { + "path": "research/coordinate-kernel-span-six-closure/PROOF.md", + "usage": "provenance", + "git_blob": "bf20f5d4f906dcb037503c027fe21b4e5e8deb11", + "sha256": "eb488595c5e931948ba737b9da2a7146ee7763af4ca163d826d7815610db5576", + "role": "Prior four-register span-six scope", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/5552" + }, + { + "path": "research/pattern-pool-cardinality/PROOF.md", + "usage": "provenance", + "git_blob": "4fce5d3b6a9c810cfd4d298b209dbd51cefa173c", + "sha256": "47ebe562180c7276bbf0636e9ba3aa1a84f8962ff8b60b3b2fb30cee4514e989", + "role": "Inherited all-width fiber lemma and previous image bound", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/5921" + }, + { + "path": "research/three-register-no-target-flag/README.md", + "usage": "provenance", + "git_blob": "290bfb79db5f4177b8b03bc2027c3848671fac9e", + "sha256": "95d4483da9b19df051c7d13fe290eefb82da019ab4be8e66ad9216199ddda4eb", + "role": "Inherited universal three-register disjoint-subset lemma and common-J method", + "originating_pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/720" + } + ], + "cited_pending_sources": [ + { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/6760", + "head": "3b3d6670d509fd74c1780cfacdf550badf8871db", + "path": "research/restored-helper-compression/PROOF.md", + "git_blob": "2f2a51dbcac84a0fe9a133514a8620ca0aa542ec", + "sha256": "4d9edf19ed4eec2708cbfcd186e9d6085af43cc0213e14fb2bd54efdeda2a20b", + "role": "Historical assignment motivation only; not a dependency of the final theorem.", + "runtime_input": false + } + ], + "pending_source_contract": "This exact-head historical citation is not an input or source_pin. The final proof uses canonical sources listed above; no pending Git object is needed for replay or the mathematical proof." +} diff --git a/research/bit-two-relation-any-registers/TASK.json b/research/bit-two-relation-any-registers/TASK.json new file mode 100644 index 0000000000..895671e2c0 --- /dev/null +++ b/research/bit-two-relation-any-registers/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a disjoint-subset and rank-budget theorem for any finite number of binary scalar registers and any word length with at most two independent exponent relations and exact diagonal monomial endpoints.", + "scope_change_reason": "The assigned fivecall restored-helper question was found already solved by merged CrocSwap/integer-mult-bounds#5481, and the finite4964 classification already existed in CrocSwap/integer-mult-bounds#1846. The lead explicitly reassigned the task to the unresolved arbitrary-width two-relation question, using the inherited three-register theorem, a new analytic joint-image classification and an odd-core common-J generalization.", + "bottleneck_link": "A rank-saving binary formal primitive now requires at least three independent rational frame relations. Eight-call 3x3 constructions at span six are excluded with any number of arbitrary diagonal auxiliaries; older results leave only span five. No new kappa or physical supplier follows.", + "budget_minutes": 90, + "stop_rule": "Complete the universal written reduction and independent adversarial check, or preserve a precisely scoped gap. Bound controls to scalar widths2..5 and odd cores3,5,7; do not launch a raw ordered-word search or claim the rank-three relation case.", + "outcome": "completed", + "evidence": "PROOF.md establishes the arbitrary-width theorem via the inherited #720 lemma. The analytic pool lemma gives image<=3 except disjoint-edge pools, and the common-J proof covers every odd core. verify.py independently replays4964 historical pools, checks108165 five-register planes,20097 prefix cases, exact endpoints and rejection controls.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance for mathematical development, exact Python verification, and separately assigned adversarial mathematical review. The reviewer supplied an alternate target-label argument. No human peer review or proof-kernel verification is claimed.", + "track_seed": 12, + "open_questions": [ + { + "question": "Can eight calls realize three invertible3x3 targets at frame span five with arbitrary diagonal auxiliaries?", + "why_it_matters": "This is the remaining eight-call case after the prior span<=4 theorem and the new arbitrary-width two-relation bound.", + "first_step": "Analyze rank-three saturated cube-relation lattices at eight calls and their three-dimensional scalar pattern spaces, retaining chronological gates and exact endpoints.", + "blocked_by": "The rank-two cube-basis unit-minor argument need not extend to rank three; the free-coordinate split and three-relation word theorem need new proofs." + }, + { + "question": "What is the sharp joint-image bound for a three-dimensional binary off-diagonal pattern space?", + "why_it_matters": "Three disjoint edges give dimension six, while the #5921 cardinality bound gives ten. Reducing this gap may bound the width in the remaining span-five case.", + "first_step": "Extend the diagonal-difference analysis to pattern sums and classify equality mechanisms before any large pool census.", + "blocked_by": "A scalar image bound alone does not establish endpoint compatibility or a three-relation disjoint-subset theorem." + } + ], + "coordination": "Lead rechecked archive provenance and formally expanded the original narrow assignment after identifying prior #5481/#1846 work. The lead reviewed the algebraic proof and a separate worker was assigned adversarial review; evidence and reviews are retained with the package." +} diff --git a/research/bit-two-relation-any-registers/VALIDATION.json b/research/bit-two-relation-any-registers/VALIDATION.json new file mode 100644 index 0000000000..f5122a1251 --- /dev/null +++ b/research/bit-two-relation-any-registers/VALIDATION.json @@ -0,0 +1,211 @@ +{ + "schema_version": 1, + "python": "3.12.14", + "platform": "Linux-6.18.57-x86_64-with-glibc2.39", + "status": "PASS_AUTHOR_LOCAL_VERIFICATION", + "normal_and_optimized_direct": "Both executed successfully after final verifier edit; identical full JSON counts.", + "registered_metadata": "PASS_PACKAGE_METADATA_AND_PINS", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE research/bit-two-relation-any-registers outcome=completed", + "certificate_regeneration": "Exact byte match against committed-intended CERTIFICATE.json", + "relocated_optimized_replay": "PASS_TWO_RELATION_ANY_REGISTERS with only verify.py and CERTIFICATE.json copied; no source repository or pending PR objects used.", + "relocated_report": { + "census": { + "full_rank_pools": 12, + "idempotents": 120, + "image_covector_ranks": [ + [ + 1, + 2, + 190 + ], + [ + 1, + 3, + 4 + ], + [ + 2, + 1, + 190 + ], + [ + 2, + 2, + 3520 + ], + [ + 2, + 3, + 108 + ], + [ + 3, + 1, + 4 + ], + [ + 3, + 2, + 108 + ], + [ + 3, + 3, + 828 + ], + [ + 4, + 4, + 12 + ] + ], + "irreducible_pools": 0, + "patterns": 104, + "planes": 4964, + "pool_sizes": [ + [ + 2, + 3814 + ], + [ + 3, + 1012 + ], + [ + 4, + 114 + ], + [ + 5, + 24 + ] + ] + }, + "certificate_rejections": [ + "omitted plane", + "proper but noninvariant witness" + ], + "common_j_controls": { + "odd_core_sizes": [ + 3, + 5, + 7 + ], + "one_gap_positive_words": 3, + "quadratic_prefix_cases": 20097, + "separated_gap_negative_words": 3, + "width_five_irreducible_control": true + }, + "exact_word_controls": { + "deleted_call_rejections": 6, + "helper_cleanup_rejection": 1, + "nonflag_commutator_determinant": 1, + "rational_frame_span": 3, + "sharp_six_call_words": 1 + }, + "joint_image_controls": [ + { + "idempotents": 6, + "image_dimensions": [ + [ + 2, + 1 + ] + ], + "patterns": 2, + "planes": 1, + "realized_two_edge_planes": 0, + "width": 2 + }, + { + "idempotents": 28, + "image_dimensions": [ + [ + 1, + 9 + ], + [ + 2, + 63 + ], + [ + 3, + 57 + ] + ], + "patterns": 19, + "planes": 129, + "realized_two_edge_planes": 6, + "width": 3 + }, + { + "idempotents": 120, + "image_dimensions": [ + [ + 1, + 194 + ], + [ + 2, + 3818 + ], + [ + 3, + 940 + ], + [ + 4, + 12 + ] + ], + "patterns": 104, + "planes": 4964, + "realized_two_edge_planes": 24, + "width": 4 + }, + { + "idempotents": 496, + "image_dimensions": [ + [ + 1, + 2515 + ], + [ + 2, + 97275 + ], + [ + 3, + 8315 + ], + [ + 4, + 60 + ] + ], + "patterns": 471, + "planes": 108165, + "realized_two_edge_planes": 60, + "width": 5 + } + ], + "structural_controls": { + "coordinate_split_control": true, + "invariant_block_cases": 3600, + "nontriangular_control": true, + "one_pattern_pools": 104, + "proper_subspaces": 65, + "repeated_target_control": true + } + }, + "verification_boundary": "Finite controls corroborate the written universal proof; #720 lemma inherited, no human/proof-kernel verification claimed.", + "source_sha256": { + "verify.py": "83b590379b6d0532b76ddd0979811a39ea13156e73ff622e587fdea47614818b", + "CERTIFICATE.json": "78ec903f3952f3eb3343a9122a7d482a5ed9bc7d8c098a3c70218bb5267b652b", + "PROOF.md": "ad05bccffaf0fe11120312d8514146e5433d7032bbc65bd9d57974e06a6c3f82", + "README.md": "238ae1a6b4f11b73e3e51a632701541a2d824e58293d8e01b3371adb53309208", + "REVIEW.md": "b5fa222353c446a6124b3c30bcd50c5a0eacc6f2aa25b58eda499565af744e47" + }, + "relocation_and_generation_seconds": 1.543514, + "review": "Separate worker reviewed the universal proof and exact #720 scope, supplied a distinct D-I target-label argument, found no defect, and requested one clarification now applied." +} diff --git a/research/bit-two-relation-any-registers/VERIFY.json b/research/bit-two-relation-any-registers/VERIFY.json new file mode 100644 index 0000000000..8f9176c0aa --- /dev/null +++ b/research/bit-two-relation-any-registers/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete historical4964-plane replay, new analytic joint-image classification at widths2..5 including108165 width-five planes,20097 odd-core prefix cases, exact formal endpoints, repeated-target and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete historical4964-plane replay, new analytic joint-image classification at widths2..5 including108165 width-five planes,20097 odd-core prefix cases, exact formal endpoints, repeated-target and rejection controls." + } + ] +} diff --git a/research/bit-two-relation-any-registers/verify.py b/research/bit-two-relation-any-registers/verify.py new file mode 100644 index 0000000000..723bc5d6b3 --- /dev/null +++ b/research/bit-two-relation-any-registers/verify.py @@ -0,0 +1,466 @@ +#!/usr/bin/env python3 +"""Exact finite lemma and controls for the four-register two-relation proof. + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +The universal group-lattice theorem is in PROOF.md; this is not formalization. +Only Python's standard library is used. Checks remain active under -O. +""" + +import argparse +from collections import Counter +from fractions import Fraction +from itertools import combinations, permutations, product +import json +from pathlib import Path + + +class VerificationError(Exception): + pass + + +def need(condition, message): + if not condition: + raise VerificationError(message) + + +def span(vectors): + result = {0} + for vector in vectors: + result |= {value ^ vector for value in tuple(result)} + return result + + +def brank(vectors): + return len(span(vectors)).bit_length() - 1 + + +def subspaces(n): + masks = set() + for dimension in range(1, n): + for basis in combinations(range(1, 1 << n), dimension): + values = span(basis) + if len(values) == 1 << dimension: + masks.add(sum(1 << value for value in values)) + return sorted(masks) + + +def rows(matrix, n=4): + return tuple((matrix >> (n * i)) & ((1 << n) - 1) for i in range(n)) + + +def packed(matrix): + n = len(matrix) + return sum(row << (n * i) for i, row in enumerate(matrix)) + + +def apply(matrix, vector): + return sum(((row & vector).bit_count() & 1) << i + for i, row in enumerate(matrix)) + + +def multiply(left, right): + return tuple(xor_rows(row, right) for row in left) + + +def xor_rows(mask, matrix): + result = 0 + for i, row in enumerate(matrix): + if mask >> i & 1: + result ^= row + return result + + +def invariant(matrix, space): + return all(space >> apply(matrix, v) & 1 + for v in range(1 << len(matrix)) if space >> v & 1) + + +def proper_space(space, n=4): + if type(space) is not int or not 0 < space < (1 << (1 << n)) - 1: + return False + values = [v for v in range(1 << n) if space >> v & 1] + return len(values) > 1 and 0 in values and all( + space >> (u ^ v) & 1 for u in values for v in values) + + +def catalogue(): + # Exhaust all 65,536 matrices, not merely a list of supplied outer products. + diagonal = sum(1 << (4 * i + i) for i in range(4)) + found = {} + for matrix in range(1 << 16): + rr = rows(matrix) + nonzero = set(rr) - {0} + if len(nonzero) != 1: + continue # A nonzero binary rank-one matrix has one nonzero row value. + if multiply(rr, rr) != rr: + continue + y = next(iter(nonzero)) + x = sum((row != 0) << i for i, row in enumerate(rr)) + need((x & y).bit_count() % 2 == 1, "idempotent self-pairing") + found[matrix] = (matrix & ~diagonal, x, y) + patterns = sorted({entry[0] for entry in found.values()} - {0}) + planes = sorted({tuple(sorted((p, q, p ^ q))) + for p, q in combinations(patterns, 2)}) + need(len(found) == 120, "120 rank-one idempotents") + need(len(patterns) == 104, "104 nonzero patterns") + need(len(planes) == 4964, "4964 pattern planes") + return found, patterns, planes + + +def pool(found, plane): + return sorted(m for m, (pattern, _, _) in found.items() if pattern in plane) + + +def canonical_full_rank_pools(): + result = set() + for p in permutations(range(4)): + result.add(tuple(sorted( + (1 << (4 * p[a] + p[a])) | (1 << (4 * p[b] + p[c])) + for a, b, c in ((0, 0, 1), (1, 0, 1), (2, 2, 3), (3, 2, 3))))) + need(len(result) == 12, "twelve disjoint-edge pools") + return result + + +def make_certificate(found, planes, spaces): + records = [] + for plane in planes: + matrices = [rows(m) for m in pool(found, plane)] + witness = next((s for s in spaces if all(invariant(m, s) for m in matrices)), None) + need(witness is not None, "an irreducible pool was found") + records.append([*plane, witness]) + return {"schema_version": 1, + "encoding": "matrix bit 4*i+j is entry (i,j); subspace bit v marks binary vector v", + "records": records} + + +def check_certificate(document, found, planes): + need(document.get("schema_version") == 1, "certificate schema") + records = document.get("records") + need(type(records) is list and len(records) == len(planes), "plane coverage count") + seen = set() + sizes, ranks = Counter(), Counter() + full_rank = set() + for record in records: + need(type(record) is list and len(record) == 4, "record shape") + p, q, r, space = record + plane = (p, q, r) + need(plane not in seen, "duplicate plane") + seen.add(plane) + need(proper_space(space), "witness is not a proper binary subspace") + matrices = pool(found, plane) + need(matrices, "empty pool") + for matrix in matrices: + need(invariant(rows(matrix), space), "noninvariant witness") + rx = brank(found[m][1] for m in matrices) + ry = brank(found[m][2] for m in matrices) + sizes[len(matrices)] += 1 + ranks[rx, ry] += 1 + if rx == ry == 4: + full_rank.add(tuple(matrices)) + need(seen == set(planes), "complete plane domain differs") + need(dict(sizes) == {2: 3814, 3: 1012, 4: 114, 5: 24}, "pool-size census") + need(full_rank == canonical_full_rank_pools(), "full-rank pool characterization") + return {"idempotents": 120, "patterns": 104, "planes": len(seen), + "pool_sizes": sorted(sizes.items()), + "image_covector_ranks": [list(key) + [value] for key, value in sorted(ranks.items())], + "full_rank_pools": len(full_rank), "irreducible_pools": 0} + + +def reject(function, description): + try: + function() + except VerificationError: + return description + raise VerificationError("negative control accepted: " + description) + + +def inverse(matrix): + n = len(matrix) + work = [row | (1 << (n + i)) for i, row in enumerate(matrix)] + for j in range(n): + pivot = next((i for i in range(j, n) if work[i] >> j & 1), None) + need(pivot is not None, "basis is singular") + work[j], work[pivot] = work[pivot], work[j] + for i in range(n): + if i != j and work[i] >> j & 1: + work[i] ^= work[j] + return tuple(row >> n for row in work) + + +def adapted_basis(space): + basis = [] + for value in range(1, 16): + if space >> value & 1 and value not in span(basis): + basis.append(value) + dimension = len(basis) + for value in range(1, 16): + if value not in span(basis): + basis.append(value) + return tuple(sum(((basis[j] >> i) & 1) << j for j in range(4)) + for i in range(4)), dimension + + +def structural_controls(found, patterns, spaces): + count = 0 + for space in spaces: + basis, d = adapted_basis(space) + inv = inverse(basis) + for matrix in found: + rr = rows(matrix) + if not invariant(rr, space): + continue + block = multiply(multiply(inv, rr), basis) + need(all(not (block[i] & ((1 << d) - 1)) for i in range(d, 4)), "lower block") + left = tuple(block[i] & ((1 << d) - 1) for i in range(d)) + right = tuple(block[i] >> d for i in range(d, 4)) + need(bool(any(left)) != bool(any(right)), "exactly one active block") + active = left if any(left) else right + need(multiply(active, active) == active and brank(active) == 1, "active block projector") + count += 1 + coordinates = [1 << (4 * i + i) for i in range(4)] + for pattern in patterns: + matrices = [rows(m) for m, entry in found.items() if entry[0] == pattern] + matrices += [rows(m) for m in coordinates] + need(any(all(invariant(m, s) for m in matrices) for s in spaces), "one-pattern reduction") + + # P,Q,R from #720: irreducible on three active coordinates, reducible on four. + exceptional = ((3, 0, 0), (2, 2, 0), (0, 5, 5)) + need(not any(all(invariant(m, s) for m in exceptional) for s in subspaces(3)), + "three-register exception must not be labelled triangular") + embedded = tuple(tuple(m) + (0,) for m in exceptional) + need(all(invariant(m, (1 << 0) | (1 << 8)) for m in embedded), "embedded invariant line") + + overlapping = [(7, 7, 7, 0), (0, 14, 14, 14)] + with_coordinates = overlapping + [rows(m) for m in coordinates] + need(any(all(invariant(m, s) for m in overlapping) for s in spaces), "noncoordinate reduction") + need(not any(all(invariant(m, s) for m in with_coordinates) for s in spaces), + "coordinate calls cannot be retained in general pool lemma") + + # Repeated target values can preserve a non-coordinate line; separating them cannot. + line = {0, 3} + def diagonal_preserves(groups): + return all((v & group) in line for v in line for group in groups) + need(diagonal_preserves((3, 4, 8)), "equal-target invariant decomposition") + need(not diagonal_preserves((1, 6, 8)), "separated-target rejection") + return {"proper_subspaces": len(spaces), "invariant_block_cases": count, + "one_pattern_pools": len(patterns), "nontriangular_control": True, + "coordinate_split_control": True, "repeated_target_control": True} + + +def qrank(matrix): + matrix = [[Fraction(x) for x in row] for row in matrix] + if not matrix: + return 0 + rank = 0 + for j in range(len(matrix[0])): + pivot = next((i for i in range(rank, len(matrix)) if matrix[i][j]), None) + if pivot is None: + continue + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + scalar = matrix[rank][j] + matrix[rank] = [value / scalar for value in matrix[rank]] + for i in range(len(matrix)): + if i != rank: + scalar = matrix[i][j] + matrix[i] = [a - scalar * b for a, b in zip(matrix[i], matrix[rank])] + rank += 1 + if rank == len(matrix): + break + return rank + + +ZERO = (0, 0, 0, 0) + + +def polynomial_product(left, right): + result = set() + for a in left: + for b in right: + exponent = tuple(x + y for x, y in zip(a, b)) + result.symmetric_difference_update((exponent,)) + return result + + +def formal_word(calls, n): + result = [[{ZERO} if i == j else set() for j in range(n)] for i in range(n)] + for frame, x, y in calls: + need(len(frame) == 4 and frame != ZERO and (x & y).bit_count() % 2, "legal formal call") + factor = [[{ZERO} if i == j else set() for j in range(n)] for i in range(n)] + for i in range(n): + for j in range(n): + if x >> i & 1 and y >> j & 1: + factor[i][j].symmetric_difference_update((ZERO, frame)) + new = [[set() for _ in range(n)] for _ in range(n)] + for i in range(n): + for j in range(n): + for k in range(n): + new[i][j].symmetric_difference_update(polynomial_product(result[i][k], factor[k][j])) + result = new + return result + + +def endpoint(targets): + return [[{target} if i == j else set() for j in range(len(targets))] + for i, target in enumerate(targets)] + + +def exact_word_controls(): + # Six rank-one integer frames in Sym_2, span three; all address arithmetic stays over Z. + frames = [(2, 0, 0, 0), (0, 0, 0, 2), (2, 0, 0, 0), + (0, 0, 0, 4), (3, 3, 3, 3), (1, -1, -1, 1)] + calls = [(frame, 1 << (j // 2), 1 << (j // 2)) for j, frame in enumerate(frames)] + targets = [(2, 0, 0, 2), (2, 0, 0, 4), (4, 2, 2, 4), ZERO] + need(qrank(frames) == 3, "six-call frame span three") + need(all(qrank((f[:2], f[2:])) == 1 for f in frames), "rank-one rational frames") + need(all(qrank((c[:2], c[2:])) == 2 for c in targets[:3]), "invertible targets") + need(formal_word(calls, 4) == endpoint(targets), "six-call exact endpoint") + for j in range(6): + need(formal_word(calls[:j] + calls[j + 1:], 4) != endpoint(targets), "deleted-call rejection") + # C1^-1 C2=diag(1,2), C1^-1 C3=[[2,1],[1,2]]: commutator determinant one. + u = tuple(Fraction(v, 2) for v in targets[1]) + v = tuple(Fraction(value, 2) for value in targets[2]) + def product2(a, b): + return tuple(sum(a[2 * i + k] * b[2 * k + j] for k in range(2)) + for i in range(2) for j in range(2)) + commutator = tuple(a - b for a, b in zip(product2(u, v), product2(v, u))) + need(commutator[0] * commutator[3] - commutator[1] * commutator[2] == 1, + "no-common-algebraic-flag witness") + helper = (1, 0, 0, 0) + restored = calls + [(helper, 8, 8), (tuple(-x for x in helper), 8, 8)] + need(formal_word(restored, 4) == endpoint(targets), "arbitrary helper restoration") + need(formal_word(restored[:-1], 4) != endpoint(targets), "missing helper cleanup") + return {"sharp_six_call_words": 1, "rational_frame_span": 3, + "deleted_call_rejections": 6, "helper_cleanup_rejection": 1, + "nonflag_commutator_determinant": 1} + + +def joint_image_controls(): + """Bounded corroboration of the written all-width lemma; not extrapolation.""" + report = [] + for n in range(2, 6): + diagonal = sum(1 << (n * i + i) for i in range(n)) + by_pattern = {} + total = 0 + for x in range(1, 1 << n): + for y in range(1, 1 << n): + if not (x & y).bit_count() % 2: + continue + total += 1 + matrix = sum((y if x >> i & 1 else 0) << (n * i) for i in range(n)) + pattern = matrix & ~diagonal + if pattern: + by_pattern.setdefault(pattern, []).append(x) + for pattern, images in by_pattern.items(): + need(len(images) == (2 if pattern.bit_count() == 1 else 1), "inherited fiber control") + planes = {tuple(sorted((p, q, p ^ q))) for p, q in combinations(by_pattern, 2)} + histogram = Counter() + two_edges_realized = 0 + for plane in planes: + images = [x for pattern in plane for x in by_pattern.get(pattern, [])] + dimension = brank(images) + need(dimension <= 4, "joint image exceeds four") + histogram[dimension] += 1 + edges = [p for p in plane if p.bit_count() == 1] + if dimension == 4: + need(len(edges) == 2 and edges[0] ^ edges[1] not in by_pattern, + "dimension four must have exactly two realized edge patterns") + endpoints = [coordinate for edge in edges + for coordinate in divmod(edge.bit_length() - 1, n)] + need(len(set(endpoints)) == 4, "dimension-four edges must have disjoint endpoints") + if len(edges) == 2 and edges[0] ^ edges[1] in by_pattern: + a, b = divmod(edges[0].bit_length() - 1, n) + c, d = divmod(edges[1].bit_length() - 1, n) + need(a == c or b == d, "realized two-edge pattern must share row or column") + need(dimension <= 3, "two-edge realized pool dimension") + two_edges_realized += 1 + if n >= 4: + need(max(histogram) == 4, "sharp image dimension four") + report.append({"width": n, "idempotents": total, "patterns": len(by_pattern), + "planes": len(planes), "image_dimensions": sorted(histogram.items()), + "realized_two_edge_planes": two_edges_realized}) + return report + + +def common_j_controls(): + """Exact bounded checks for the new odd-core quadratic and endpoint steps.""" + prefix_cases = 0 + for s in (3, 5, 7): + # Stars have the one all-sum relation, independent of the J pattern. + stars = [tuple(((1 << s) - 1) ^ (1 << i) if row == i else (1 << i) + for row in range(s)) for i in range(s)] + packed_stars = [packed(m) for m in stars] + j_off = packed(tuple(((1 << s) - 1) ^ (1 << i) for i in range(s))) + need(brank(packed_stars) == s - 1, "star relation rank") + need(j_off not in span(packed_stars), "J pattern independent of stars") + # One coordinate occurrence per role. Universal proof covers all multiplicities. + for h in (2, 3, 4): + prefixes = [0] + [(1 << gap) - 1 for gap in range(1, h)] + for placements in product(prefixes, repeat=s): + common = None + for i in range(s - 1): + columns = [0] * s + columns[i], columns[-1] = placements[i], placements[-1] + nonzero = set(columns) - {0} + if len(nonzero) > 1: + common = set() + break + if nonzero: + j_factor = next(iter(nonzero)) + c_factor = sum((bool(value)) << j for j, value in enumerate(columns)) + factors = {("J", j_factor), ("coordinate", c_factor)} + common = factors if common is None else common & factors + divisible = common is None or bool(common) + single_gap = len(set(placements) - {0}) <= 1 + need(divisible == single_gap, "shared linear divisor versus single gap") + prefix_cases += 1 + j = (1 << s) - 1 + b, a = (1, 0, 0, 0), (0, 0, 0, 1) + minus_b, minus_a = tuple(-v for v in b), tuple(-v for v in a) + positive = [(b, j, j), (a, 1, 1), (minus_a, 1, 1), (minus_b, j, j)] + negative = [(b, j, j), (a, 1, 1), (minus_b, j, j), (minus_a, 1, 1)] + need(formal_word(positive, s) == endpoint([ZERO] * s), "odd-core one-gap cancellation") + bad = formal_word(negative, s) + need(any(bad[i][k] for i in range(s) for k in range(s) if i != k), + "separated internal gaps rejected by exact endpoint") + # A five-coordinate common-J pool plus coordinates is irreducible. The + # arbitrary-width case needs the quadratic proof, not a four-dimensional image shortcut. + spaces5 = subspaces(5) + need(len(spaces5) == 372, "five-coordinate proper subspace count") + matrices = [(31,) * 5] + [tuple(1 << i if row == i else 0 for row in range(5)) for i in range(5)] + need(not any(all(invariant(m, space) for m in matrices) for space in spaces5), + "odd-width full common-pattern alphabet must remain irreducible") + return {"odd_core_sizes": [3, 5, 7], "quadratic_prefix_cases": prefix_cases, + "one_gap_positive_words": 3, "separated_gap_negative_words": 3, + "width_five_irreducible_control": True} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-certificate", type=Path) + args = parser.parse_args() + found, patterns, planes = catalogue() + spaces = subspaces(4) + need(len(spaces) == 65, "65 proper nonzero binary subspaces") + if args.emit_certificate: + document = make_certificate(found, planes, spaces) + args.emit_certificate.write_text(json.dumps(document, separators=(",", ":")) + "\n") + else: + document = json.loads(Path(__file__).with_name("CERTIFICATE.json").read_text()) + census = check_certificate(document, found, planes) + controls = [] + bad = dict(document, records=document["records"][:-1]) + controls.append(reject(lambda: check_certificate(bad, found, planes), "omitted plane")) + bad_records = [list(row) for row in document["records"]] + first_pool = pool(found, tuple(bad_records[0][:3])) + bad_records[0][3] = next(s for s in spaces if not all(invariant(rows(m), s) for m in first_pool)) + controls.append(reject(lambda: check_certificate(dict(document, records=bad_records), found, planes), + "proper but noninvariant witness")) + report = {"census": census, "structural_controls": structural_controls(found, patterns, spaces), + "exact_word_controls": exact_word_controls(), "certificate_rejections": controls, + "joint_image_controls": joint_image_controls(), "common_j_controls": common_j_controls()} + print("PASS_TWO_RELATION_ANY_REGISTERS") + print(json.dumps(report, sort_keys=True)) + + +if __name__ == "__main__": + main()