diff --git a/research/k8-pair-dyadic-seed25/CERTIFICATE.json b/research/k8-pair-dyadic-seed25/CERTIFICATE.json new file mode 100644 index 0000000000..d44d7d0a25 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/CERTIFICATE.json @@ -0,0 +1 @@ +{"base":"1b59b624d21924f8e3537cdc1ac52d3be6eda2fe","orientations":{"backward":{"baseline_endpoint":{"all_restored":true,"centre_columns":8,"data_helper_columns":704,"dirty_helper_columns":480,"formal_input_columns":712},"bounded_pilot":{"assignments":38624,"delta_histogram":[[-256,1],[-240,1],[-235,1],[-218,1],[-216,2],[-204,1],[-202,1],[-200,1],[-199,1],[-197,2],[-196,3],[-195,3],[-194,3],[-193,1],[-192,1],[-191,2],[-190,1],[-189,1],[-188,1],[-186,1],[-182,3],[-180,3],[-178,5],[-176,4],[-175,2],[-173,1],[-172,2],[-171,3],[-170,1],[-169,2],[-166,3],[-165,2],[-164,1],[-163,1],[-162,1],[-161,1],[-160,1],[-159,1],[-158,9],[-157,3],[-156,2],[-155,3],[-154,5],[-153,1],[-152,2],[-151,1],[-150,2],[-149,3],[-147,2],[-146,1],[-145,2],[-144,3],[-143,2],[-142,6],[-141,5],[-140,2],[-139,5],[-138,3],[-137,5],[-136,1],[-135,4],[-134,1],[-133,1],[-132,2],[-131,4],[-130,4],[-129,2],[-128,1],[-127,5],[-126,4],[-125,3],[-124,1],[-123,1],[-122,3],[-121,4],[-120,5],[-119,4],[-118,1],[-117,5],[-116,7],[-115,7],[-114,6],[-113,9],[-112,3],[-111,5],[-110,4],[-109,3],[-108,4],[-107,3],[-106,3],[-105,7],[-104,4],[-103,9],[-102,11],[-101,6],[-100,6],[-99,10],[-98,7],[-97,5],[-96,6],[-95,3],[-94,11],[-93,4],[-92,3],[-91,5],[-90,11],[-89,8],[-88,6],[-87,3],[-86,7],[-85,8],[-84,4],[-83,12],[-82,13],[-81,15],[-80,7],[-79,11],[-78,15],[-77,9],[-76,11],[-75,5],[-74,10],[-73,12],[-72,12],[-71,11],[-70,9],[-69,9],[-68,10],[-67,12],[-66,17],[-65,20],[-64,11],[-63,22],[-62,17],[-61,13],[-60,17],[-59,14],[-58,23],[-57,10],[-56,19],[-55,16],[-54,13],[-53,17],[-52,24],[-51,17],[-50,17],[-49,12],[-48,23],[-47,23],[-46,22],[-45,37],[-44,27],[-43,27],[-42,30],[-41,25],[-40,35],[-39,33],[-38,36],[-37,36],[-36,31],[-35,36],[-34,28],[-33,36],[-32,32],[-31,27],[-30,32],[-29,30],[-28,41],[-27,42],[-26,38],[-25,38],[-24,42],[-23,32],[-22,40],[-21,48],[-20,51],[-19,40],[-18,46],[-17,55],[-16,56],[-15,30],[-14,41],[-13,50],[-12,47],[-11,44],[-10,51],[-9,37],[-8,61],[-7,49],[-6,56],[-5,43],[-4,90],[-3,57],[-2,70],[-1,68],[0,67],[1,69],[2,57],[3,53],[4,76],[5,70],[6,83],[7,60],[8,58],[9,63],[10,78],[11,83],[12,71],[13,80],[14,80],[15,73],[16,75],[17,66],[18,75],[19,88],[20,92],[21,91],[22,84],[23,70],[24,104],[25,80],[26,86],[27,97],[28,97],[29,76],[30,103],[31,105],[32,110],[33,97],[34,96],[35,81],[36,91],[37,88],[38,77],[39,87],[40,96],[41,117],[42,99],[43,113],[44,100],[45,95],[46,100],[47,97],[48,91],[49,107],[50,91],[51,117],[52,115],[53,94],[54,116],[55,100],[56,122],[57,103],[58,122],[59,110],[60,113],[61,116],[62,122],[63,100],[64,117],[65,106],[66,125],[67,110],[68,121],[69,118],[70,113],[71,108],[72,127],[73,114],[74,114],[75,110],[76,125],[77,115],[78,123],[79,129],[80,106],[81,113],[82,117],[83,110],[84,117],[85,127],[86,103],[87,111],[88,128],[89,99],[90,122],[91,114],[92,113],[93,129],[94,124],[95,104],[96,119],[97,119],[98,139],[99,128],[100,101],[101,136],[102,147],[103,130],[104,107],[105,129],[106,117],[107,124],[108,109],[109,118],[110,128],[111,107],[112,107],[113,134],[114,130],[115,105],[116,117],[117,128],[118,130],[119,145],[120,139],[121,145],[122,159],[123,140],[124,134],[125,145],[126,143],[127,143],[128,112],[129,122],[130,125],[131,131],[132,127],[133,110],[134,123],[135,123],[136,130],[137,132],[138,139],[139,141],[140,134],[141,128],[142,120],[143,131],[144,121],[145,132],[146,109],[147,129],[148,130],[149,127],[150,122],[151,124],[152,121],[153,127],[154,123],[155,120],[156,124],[157,129],[158,132],[159,119],[160,134],[161,131],[162,145],[163,118],[164,118],[165,127],[166,124],[167,133],[168,142],[169,115],[170,101],[171,118],[172,113],[173,110],[174,105],[175,132],[176,130],[177,113],[178,106],[179,111],[180,119],[181,122],[182,112],[183,126],[184,118],[185,145],[186,113],[187,109],[188,123],[189,115],[190,107],[191,133],[192,117],[193,105],[194,95],[195,111],[196,104],[197,106],[198,98],[199,119],[200,127],[201,84],[202,127],[203,106],[204,120],[205,103],[206,110],[207,103],[208,109],[209,103],[210,87],[211,97],[212,108],[213,95],[214,81],[215,110],[216,98],[217,95],[218,93],[219,88],[220,80],[221,89],[222,95],[223,77],[224,94],[225,84],[226,78],[227,103],[228,84],[229,100],[230,92],[231,110],[232,95],[233,100],[234,106],[235,87],[236,86],[237,75],[238,109],[239,74],[240,96],[241,92],[242,94],[243,88],[244,86],[245,76],[246,89],[247,102],[248,84],[249,79],[250,81],[251,95],[252,94],[253,86],[254,86],[255,80],[256,94],[257,78],[258,73],[259,66],[260,68],[261,73],[262,78],[263,68],[264,65],[265,71],[266,86],[267,85],[268,87],[269,72],[270,78],[271,77],[272,66],[273,73],[274,75],[275,73],[276,71],[277,75],[278,65],[279,83],[280,67],[281,78],[282,60],[283,78],[284,92],[285,58],[286,77],[287,61],[288,60],[289,61],[290,66],[291,55],[292,81],[293,68],[294,67],[295,68],[296,79],[297,44],[298,64],[299,58],[300,64],[301,73],[302,65],[303,62],[304,60],[305,52],[306,46],[307,52],[308,53],[309,69],[310,59],[311,61],[312,49],[313,58],[314,57],[315,52],[316,43],[317,44],[318,53],[319,53],[320,64],[321,56],[322,48],[323,53],[324,45],[325,59],[326,52],[327,52],[328,39],[329,38],[330,29],[331,39],[332,51],[333,49],[334,38],[335,38],[336,53],[337,38],[338,50],[339,43],[340,46],[341,42],[342,43],[343,48],[344,32],[345,36],[346,37],[347,34],[348,39],[349,30],[350,32],[351,39],[352,36],[353,35],[354,38],[355,49],[356,34],[357,37],[358,24],[359,28],[360,23],[361,32],[362,24],[363,39],[364,34],[365,32],[366,33],[367,19],[368,30],[369,39],[370,34],[371,26],[372,22],[373,26],[374,24],[375,25],[376,22],[377,32],[378,31],[379,12],[380,20],[381,24],[382,25],[383,29],[384,25],[385,32],[386,25],[387,22],[388,29],[389,16],[390,21],[391,19],[392,23],[393,19],[394,20],[395,22],[396,18],[397,22],[398,17],[399,23],[400,22],[401,12],[402,16],[403,26],[404,18],[405,13],[406,24],[407,17],[408,22],[409,15],[410,21],[411,13],[412,16],[413,15],[414,17],[415,16],[416,23],[417,22],[418,19],[419,13],[420,22],[421,21],[422,17],[423,12],[424,16],[425,15],[426,12],[427,11],[428,12],[429,17],[430,13],[431,14],[432,14],[433,8],[434,12],[435,16],[436,10],[437,23],[438,12],[439,11],[440,13],[441,14],[442,9],[443,16],[444,11],[445,10],[446,16],[447,14],[448,6],[449,3],[450,8],[451,6],[452,8],[453,6],[454,8],[455,7],[456,11],[457,12],[458,11],[459,8],[460,11],[461,12],[462,9],[463,13],[464,10],[465,10],[466,7],[467,5],[468,5],[469,6],[470,10],[471,8],[472,10],[473,8],[474,8],[475,11],[476,10],[477,3],[478,7],[479,7],[480,7],[481,3],[482,9],[483,4],[484,5],[485,4],[486,2],[487,8],[488,2],[489,5],[490,5],[491,1],[492,3],[493,2],[494,8],[495,3],[496,5],[497,1],[498,3],[499,3],[500,3],[501,4],[502,1],[503,4],[504,3],[505,1],[506,3],[507,3],[508,4],[510,1],[511,2],[512,2],[513,2],[514,1],[515,4],[516,6],[517,5],[518,1],[519,1],[520,2],[521,1],[522,2],[523,1],[524,4],[525,4],[526,2],[527,1],[529,4],[530,1],[532,3],[533,1],[534,3],[535,3],[536,1],[538,1],[539,2],[541,1],[542,1],[544,3],[548,3],[549,1],[550,1],[551,1],[552,2],[553,3],[554,1],[556,2],[557,4],[558,1],[559,2],[564,1],[566,1],[568,1],[570,2],[575,1],[576,1],[577,1]],"exponents":[-2,-1,1,2],"helpers":[225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,274,276,278,279,280,281,283,284,285,286,287,288,290,292,294,295,296,297,299,300,301,302,303,304,306,308,310,312,313,315,316,317,318,319,320,322,324,326,328,329,331,332,333,334,335,336,338,340,342,343,344,345,347,348,349,350,351,352,354,356,358,359,360,361,363,364,365,366,367,368,370,372,374,375,376,377,379,380,381,382,383,384,386,388,390,391,392,393,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,478,479,480,481,482,483,490,491,492,493,494,495,499,502,503,504,505,507,511,514,515,516,517,519,530,542,546,547,548,549,558,560,568,570],"pairs":2414,"winner":{"delta_real":-256,"exponents":[2,1],"helpers":[427,430],"interaction_delta_real":0,"separate_single_delta_real":-256}},"candidate_endpoint":{"all_restored":true,"centre_columns":8,"data_helper_columns":704,"dirty_helper_columns":480,"formal_input_columns":712},"candidate_sha256":"d8bac18a43eb36e708d904675776f2f488b8894de3830425e9a5bd14e06dee3b","domain":"all integer exponent pairs, including zero","helpers":[225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,274,276,278,279,280,281,283,284,285,286,287,288,290,292,294,295,296,297,299,300,301,302,303,304,306,308,310,312,313,315,316,317,318,319,320,322,324,326,328,329,331,332,333,334,335,336,338,340,342,343,344,345,347,348,349,350,351,352,354,356,358,359,360,361,363,364,365,366,367,368,370,372,374,375,376,377,379,380,381,382,383,384,386,388,390,391,392,393,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,478,479,480,481,482,483,490,491,492,493,494,495,499,502,503,504,505,507,511,514,515,516,517,519,530,542,546,547,548,549,558,560,568,570],"interacting_pairs":2414,"pair_rows_sha256":"417edb391940dc21e50cb80a8059b4d4ab458b520a61661e78ea98f33d1f4f08","pairs":27966,"prices":{"copy-init":{"after":{"charged_payload_bits":192,"complex_primitives":148442,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":68,"prefix_l1":"14824960514781440791821/64","real_primitives":74221},"before":{"charged_payload_bits":192,"complex_primitives":149018,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":68,"prefix_l1":"14824960514781440791821/64","real_primitives":74509},"saving_complex":576},"horner":{"after":{"charged_payload_bits":192,"complex_primitives":198398,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":68,"prefix_l1":"14824960514781440791821/64","real_primitives":99199},"before":{"charged_payload_bits":192,"complex_primitives":198814,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":68,"prefix_l1":"14824960514781440791821/64","real_primitives":99407},"saving_complex":416}},"separable_pairs":25552,"vertices":735975,"winner":{"delta_real":-288,"exponents":[2,2],"helpers":[251,427],"interaction_delta_real":0,"separate_single_delta_real":-288}},"forward":{"baseline_endpoint":{"all_restored":true,"centre_columns":8,"data_helper_columns":704,"dirty_helper_columns":480,"formal_input_columns":712},"bounded_pilot":{"assignments":38624,"delta_histogram":[[-256,1],[-240,1],[-235,1],[-218,1],[-216,2],[-204,1],[-202,1],[-200,1],[-199,1],[-197,2],[-196,3],[-195,3],[-194,3],[-193,1],[-192,1],[-191,2],[-190,1],[-189,1],[-188,1],[-186,1],[-182,3],[-180,3],[-178,5],[-176,4],[-175,2],[-173,1],[-172,2],[-171,3],[-170,1],[-169,2],[-166,3],[-165,2],[-164,1],[-163,1],[-162,1],[-161,1],[-160,1],[-159,1],[-158,9],[-157,3],[-156,2],[-155,3],[-154,5],[-153,1],[-152,2],[-151,1],[-150,2],[-149,3],[-147,2],[-146,1],[-145,2],[-144,3],[-143,2],[-142,6],[-141,5],[-140,2],[-139,5],[-138,3],[-137,5],[-136,1],[-135,4],[-134,1],[-133,1],[-132,2],[-131,4],[-130,4],[-129,2],[-128,1],[-127,5],[-126,4],[-125,3],[-124,1],[-123,1],[-122,3],[-121,4],[-120,5],[-119,4],[-118,1],[-117,5],[-116,7],[-115,7],[-114,6],[-113,9],[-112,3],[-111,5],[-110,4],[-109,3],[-108,4],[-107,3],[-106,3],[-105,7],[-104,4],[-103,9],[-102,11],[-101,6],[-100,6],[-99,10],[-98,7],[-97,5],[-96,6],[-95,3],[-94,11],[-93,4],[-92,3],[-91,5],[-90,11],[-89,8],[-88,6],[-87,3],[-86,7],[-85,8],[-84,4],[-83,12],[-82,13],[-81,15],[-80,7],[-79,11],[-78,15],[-77,9],[-76,11],[-75,5],[-74,10],[-73,12],[-72,12],[-71,11],[-70,9],[-69,9],[-68,10],[-67,12],[-66,17],[-65,20],[-64,11],[-63,22],[-62,17],[-61,13],[-60,17],[-59,14],[-58,23],[-57,10],[-56,19],[-55,16],[-54,13],[-53,17],[-52,24],[-51,17],[-50,17],[-49,12],[-48,23],[-47,23],[-46,22],[-45,37],[-44,27],[-43,27],[-42,30],[-41,25],[-40,35],[-39,33],[-38,36],[-37,36],[-36,31],[-35,36],[-34,28],[-33,36],[-32,32],[-31,27],[-30,32],[-29,30],[-28,41],[-27,42],[-26,38],[-25,38],[-24,42],[-23,32],[-22,40],[-21,48],[-20,51],[-19,40],[-18,46],[-17,55],[-16,56],[-15,30],[-14,41],[-13,50],[-12,47],[-11,44],[-10,51],[-9,37],[-8,61],[-7,49],[-6,56],[-5,43],[-4,90],[-3,57],[-2,70],[-1,68],[0,67],[1,69],[2,57],[3,53],[4,76],[5,70],[6,83],[7,60],[8,58],[9,63],[10,78],[11,83],[12,71],[13,80],[14,80],[15,73],[16,75],[17,66],[18,75],[19,88],[20,92],[21,91],[22,84],[23,70],[24,104],[25,80],[26,86],[27,97],[28,97],[29,76],[30,103],[31,105],[32,110],[33,97],[34,96],[35,81],[36,91],[37,88],[38,77],[39,87],[40,96],[41,117],[42,99],[43,113],[44,100],[45,95],[46,100],[47,97],[48,91],[49,107],[50,91],[51,117],[52,115],[53,94],[54,116],[55,100],[56,122],[57,103],[58,122],[59,110],[60,113],[61,116],[62,122],[63,100],[64,117],[65,106],[66,125],[67,110],[68,121],[69,118],[70,113],[71,108],[72,127],[73,114],[74,114],[75,110],[76,125],[77,115],[78,123],[79,129],[80,106],[81,113],[82,117],[83,110],[84,117],[85,127],[86,103],[87,111],[88,128],[89,99],[90,122],[91,114],[92,113],[93,129],[94,124],[95,104],[96,119],[97,119],[98,139],[99,128],[100,101],[101,136],[102,147],[103,130],[104,107],[105,129],[106,117],[107,124],[108,109],[109,118],[110,128],[111,107],[112,107],[113,134],[114,130],[115,105],[116,117],[117,128],[118,130],[119,145],[120,139],[121,145],[122,159],[123,140],[124,134],[125,145],[126,143],[127,143],[128,112],[129,122],[130,125],[131,131],[132,127],[133,110],[134,123],[135,123],[136,130],[137,132],[138,139],[139,141],[140,134],[141,128],[142,120],[143,131],[144,121],[145,132],[146,109],[147,129],[148,130],[149,127],[150,122],[151,124],[152,121],[153,127],[154,123],[155,120],[156,124],[157,129],[158,132],[159,119],[160,134],[161,131],[162,145],[163,118],[164,118],[165,127],[166,124],[167,133],[168,142],[169,115],[170,101],[171,118],[172,113],[173,110],[174,105],[175,132],[176,130],[177,113],[178,106],[179,111],[180,119],[181,122],[182,112],[183,126],[184,118],[185,145],[186,113],[187,109],[188,123],[189,115],[190,107],[191,133],[192,117],[193,105],[194,95],[195,111],[196,104],[197,106],[198,98],[199,119],[200,127],[201,84],[202,127],[203,106],[204,120],[205,103],[206,110],[207,103],[208,109],[209,103],[210,87],[211,97],[212,108],[213,95],[214,81],[215,110],[216,98],[217,95],[218,93],[219,88],[220,80],[221,89],[222,95],[223,77],[224,94],[225,84],[226,78],[227,103],[228,84],[229,100],[230,92],[231,110],[232,95],[233,100],[234,106],[235,87],[236,86],[237,75],[238,109],[239,74],[240,96],[241,92],[242,94],[243,88],[244,86],[245,76],[246,89],[247,102],[248,84],[249,79],[250,81],[251,95],[252,94],[253,86],[254,86],[255,80],[256,94],[257,78],[258,73],[259,66],[260,68],[261,73],[262,78],[263,68],[264,65],[265,71],[266,86],[267,85],[268,87],[269,72],[270,78],[271,77],[272,66],[273,73],[274,75],[275,73],[276,71],[277,75],[278,65],[279,83],[280,67],[281,78],[282,60],[283,78],[284,92],[285,58],[286,77],[287,61],[288,60],[289,61],[290,66],[291,55],[292,81],[293,68],[294,67],[295,68],[296,79],[297,44],[298,64],[299,58],[300,64],[301,73],[302,65],[303,62],[304,60],[305,52],[306,46],[307,52],[308,53],[309,69],[310,59],[311,61],[312,49],[313,58],[314,57],[315,52],[316,43],[317,44],[318,53],[319,53],[320,64],[321,56],[322,48],[323,53],[324,45],[325,59],[326,52],[327,52],[328,39],[329,38],[330,29],[331,39],[332,51],[333,49],[334,38],[335,38],[336,53],[337,38],[338,50],[339,43],[340,46],[341,42],[342,43],[343,48],[344,32],[345,36],[346,37],[347,34],[348,39],[349,30],[350,32],[351,39],[352,36],[353,35],[354,38],[355,49],[356,34],[357,37],[358,24],[359,28],[360,23],[361,32],[362,24],[363,39],[364,34],[365,32],[366,33],[367,19],[368,30],[369,39],[370,34],[371,26],[372,22],[373,26],[374,24],[375,25],[376,22],[377,32],[378,31],[379,12],[380,20],[381,24],[382,25],[383,29],[384,25],[385,32],[386,25],[387,22],[388,29],[389,16],[390,21],[391,19],[392,23],[393,19],[394,20],[395,22],[396,18],[397,22],[398,17],[399,23],[400,22],[401,12],[402,16],[403,26],[404,18],[405,13],[406,24],[407,17],[408,22],[409,15],[410,21],[411,13],[412,16],[413,15],[414,17],[415,16],[416,23],[417,22],[418,19],[419,13],[420,22],[421,21],[422,17],[423,12],[424,16],[425,15],[426,12],[427,11],[428,12],[429,17],[430,13],[431,14],[432,14],[433,8],[434,12],[435,16],[436,10],[437,23],[438,12],[439,11],[440,13],[441,14],[442,9],[443,16],[444,11],[445,10],[446,16],[447,14],[448,6],[449,3],[450,8],[451,6],[452,8],[453,6],[454,8],[455,7],[456,11],[457,12],[458,11],[459,8],[460,11],[461,12],[462,9],[463,13],[464,10],[465,10],[466,7],[467,5],[468,5],[469,6],[470,10],[471,8],[472,10],[473,8],[474,8],[475,11],[476,10],[477,3],[478,7],[479,7],[480,7],[481,3],[482,9],[483,4],[484,5],[485,4],[486,2],[487,8],[488,2],[489,5],[490,5],[491,1],[492,3],[493,2],[494,8],[495,3],[496,5],[497,1],[498,3],[499,3],[500,3],[501,4],[502,1],[503,4],[504,3],[505,1],[506,3],[507,3],[508,4],[510,1],[511,2],[512,2],[513,2],[514,1],[515,4],[516,6],[517,5],[518,1],[519,1],[520,2],[521,1],[522,2],[523,1],[524,4],[525,4],[526,2],[527,1],[529,4],[530,1],[532,3],[533,1],[534,3],[535,3],[536,1],[538,1],[539,2],[541,1],[542,1],[544,3],[548,3],[549,1],[550,1],[551,1],[552,2],[553,3],[554,1],[556,2],[557,4],[558,1],[559,2],[564,1],[566,1],[568,1],[570,2],[575,1],[576,1],[577,1]],"exponents":[-2,-1,1,2],"helpers":[225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,274,276,278,279,280,281,283,284,285,286,287,288,290,292,294,295,296,297,299,300,301,302,303,304,306,308,310,312,313,315,316,317,318,319,320,322,324,326,328,329,331,332,333,334,335,336,338,340,342,343,344,345,347,348,349,350,351,352,354,356,358,359,360,361,363,364,365,366,367,368,370,372,374,375,376,377,379,380,381,382,383,384,386,388,390,391,392,393,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,478,479,480,481,482,483,490,491,492,493,494,495,499,502,503,504,505,507,511,514,515,516,517,519,530,542,546,547,548,549,558,560,568,570],"pairs":2414,"winner":{"delta_real":-256,"exponents":[-2,-1],"helpers":[427,430],"interaction_delta_real":0,"separate_single_delta_real":-256}},"candidate_endpoint":{"all_restored":true,"centre_columns":8,"data_helper_columns":704,"dirty_helper_columns":480,"formal_input_columns":712},"candidate_sha256":"1d756480ebe954f304b717104954eee78d26d81f2b96de35e10da76e7bb511c2","domain":"all integer exponent pairs, including zero","helpers":[225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,241,242,243,244,245,246,247,248,249,250,251,252,253,254,255,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,274,276,278,279,280,281,283,284,285,286,287,288,290,292,294,295,296,297,299,300,301,302,303,304,306,308,310,312,313,315,316,317,318,319,320,322,324,326,328,329,331,332,333,334,335,336,338,340,342,343,344,345,347,348,349,350,351,352,354,356,358,359,360,361,363,364,365,366,367,368,370,372,374,375,376,377,379,380,381,382,383,384,386,388,390,391,392,393,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,478,479,480,481,482,483,490,491,492,493,494,495,499,502,503,504,505,507,511,514,515,516,517,519,530,542,546,547,548,549,558,560,568,570],"interacting_pairs":2414,"pair_rows_sha256":"2cb96e4cc5ce176816dab09312e080c2c3445088de06ce45baec922c56556454","pairs":27966,"prices":{"copy-init":{"after":{"charged_payload_bits":192,"complex_primitives":148426,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":52,"prefix_l1":"2765345294379392599/1024","real_primitives":74213},"before":{"charged_payload_bits":192,"complex_primitives":149002,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":52,"prefix_l1":"2765345294379392599/1024","real_primitives":74501},"saving_complex":576},"horner":{"after":{"charged_payload_bits":192,"complex_primitives":198350,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":52,"prefix_l1":"2765345294379392599/1024","real_primitives":99175},"before":{"charged_payload_bits":192,"complex_primitives":198766,"paid_profile":{"1":2412,"2":418,"3":432,"4":142,"5":82,"8":8},"prefix_bits":52,"prefix_l1":"2765345294379392599/1024","real_primitives":99383},"saving_complex":416}},"separable_pairs":25552,"vertices":735975,"winner":{"delta_real":-288,"exponents":[-2,-2],"helpers":[251,427],"interaction_delta_real":0,"separate_single_delta_real":-288}}},"scope":"all integer gauges on at most two cold/FULL unwrapped helpers","seed":25,"status":"PASS_K8_PAIR_DYADIC_CENSUS"} diff --git a/research/k8-pair-dyadic-seed25/CLAIM.json b/research/k8-pair-dyadic-seed25/CLAIM.json new file mode 100644 index 0000000000..ab6a1d8dd4 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/CLAIM.json @@ -0,0 +1,59 @@ +{ + "track": "complex supplier", + "seed": 25, + "seed_source": "secrets.randbelow(100), OS randomness", + "started_utc": "2026-10-13T19:56:01Z", + "expected_finish_utc": "2026-10-13T20:36:01Z", + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "candidates": [ + { + "object": "P112 masked decoder with rank-one odd-support correction", + "decision": "deferred; requires a new realization contract and broader synthesis" + }, + { + "object": "P104 term delivery with paid downward frame moves", + "decision": "not selected; PR1125 already covers this mechanism" + }, + { + "object": "PR1094 k8 two interacting helper diagonal scaling", + "decision": "selected; PR1161 covers single helpers; PR1170 consolidates existing stage scales" + } + ], + "scope": "Every unordered pair of non-center helpers joined by an ADD, each exponent in {-2,-1,1,2}; exact primitive costs and full maps for the best witness. Seed selects radius 1+seed%3=2. Existing SCALE and non-scalar events retained; entry/exit scales paid.", + "predecessor": { + "pr": 1161, + "head": "d210969d3158a1e6c505e41f67dd84e555c88564" + }, + "changed_hypothesis": "Two helper coordinates may change simultaneously, including their connecting ADD coefficients.", + "optimistic_budget": "Recursive profile stays fixed; only a strictly reduced fully paid scalar primitive count is an acceptable local construction result. No kappa claim.", + "stopping_rule": "Complete finite adjacent-pair census; one winning exact scalar replay; stop new experiments by 20:26:01 UTC.", + "coordination": "No pinned issue returned by GraphQL; local claim, discussion board and 808 open PRs inspected.", + "deliverable": "One research package: exact finite search receipt, reproducible checker, witness, controls, pins and attribution.", + "attribution": "Hanson Sun with substantial OpenAI Codex assistance; credit PR1161 and its predecessor lineage; Apache-2.0.", + "pivot": { + "reason": "The bounded connected winner has zero interaction gain; the two best separate helpers nominate a stronger witness. Affine-cell geometry permits finite certification over all integer exponents.", + "domain": "All unordered pairs among the 237 cold-to-FULL, unwrapped, non-center helpers with no COPY/clear incidence; integer exponents including zero; same original ADD topology and all existing SCALEs fixed.", + "method": "Exact line-arrangement vertices; independent rectangular integer enumeration on interacting pairs and separable single-coordinate enumeration elsewhere.", + "coverage_goal": "27966 unordered helper pairs per orientation; no arbitrary exponent cutoff." + }, + "result": { + "status": "verified finite scalar contribution", + "helpers": [ + 251, + 427 + ], + "forward_exponents": [ + -2, + -2 + ], + "backward_exponents": [ + 2, + 2 + ], + "saving_complex_primitives_per_orientation": 576, + "pairs_per_orientation": 27966, + "exponents": "all integers", + "new_kappa": false, + "artifact_url": "https://github.com/bbMisk/integer-mult-bounds/tree/hanson/complex-pair-scaling-seed25/research/k8-pair-dyadic-seed25" + } +} diff --git a/research/k8-pair-dyadic-seed25/CONTEXT.json b/research/k8-pair-dyadic-seed25/CONTEXT.json new file mode 100644 index 0000000000..f0176f3257 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/CONTEXT.json @@ -0,0 +1,48 @@ +{ + "selected_at_base": { + "kappa": "836330098538459/500000000000000000", + "binding_supplier": "complex", + "reference": "research/community-frontier1094-audit/ASSEMBLY.json" + }, + "source_authors": [ + "woklerx / PR1161", + "Sagar Thakrar / PR696", + "Rohan Arun / PR1094", + "Jeremy Kothe / PR1042 and k8/T16 lineage", + "icekylinx / PR425, PR433, PR531, gauge44", + "Douglas Colkitt / retained source-bound review" + ], + "new_contributor": "Hanson Sun / bbMisk", + "assistance": "Substantial OpenAI Codex assistance: research, implementation, verification, documentation", + "license": "Apache-2.0", + "overlap": [ + { + "pr": 1161, + "head": "d210969d3158a1e6c505e41f67dd84e555c88564", + "scope": "one non-center helper, all integer exponents", + "delta": "two helper coordinates, shared-edge interaction, exact pair census; byte-for-byte retained engine functions credited" + }, + { + "pr": 1170, + "head": "df273e3cb1e62c1bfdf6599160b538e7a4b879d7", + "scope": "existing A/B SCALE consolidation", + "delta": "existing SCALE operations fixed; no composition claim" + }, + { + "pr": 1064, + "head": "b0181971c2364744d1dd9b0c2d4ee1ea532b8bb6", + "scope": "local eight-register factory source scaling", + "delta": "whole selected finite scalar provider; all pairs within restricted boundary interface" + } + ], + "new_kappa": false, + "native_admission": false, + "global_hosted_invoice": false, + "formal_Lean_multiplication_theorem": false, + "final_overlap": { + "open_prs": 820, + "highest_observed_pr": 1211, + "specific_predecessor_head_unchanged": true, + "duplicates_found": false + } +} diff --git a/research/k8-pair-dyadic-seed25/PAIR-CENSUS.json.gz b/research/k8-pair-dyadic-seed25/PAIR-CENSUS.json.gz new file mode 100644 index 0000000000..92e371de65 Binary files /dev/null and b/research/k8-pair-dyadic-seed25/PAIR-CENSUS.json.gz differ diff --git a/research/k8-pair-dyadic-seed25/PROGRAMS.json.gz b/research/k8-pair-dyadic-seed25/PROGRAMS.json.gz new file mode 100644 index 0000000000..9455614a79 Binary files /dev/null and b/research/k8-pair-dyadic-seed25/PROGRAMS.json.gz differ diff --git a/research/k8-pair-dyadic-seed25/README.md b/research/k8-pair-dyadic-seed25/README.md new file mode 100644 index 0000000000..ec4303d21a --- /dev/null +++ b/research/k8-pair-dyadic-seed25/README.md @@ -0,0 +1,85 @@ +# Exact two-helper dyadic scaling of the k8 scalar provider + +Scaling L251 and L427 saves 576 scalar primitives per complex invocation in each orientation. This is optimal among dyadic gauges on at most two of the 237 eligible helpers, with ADD topology and existing SCALEs fixed. Each pair's cost is affine between vertical, horizontal and diagonal break lines. Boundary charges make it coercive; unit discounts lower boundary values. A minimum therefore occurs at an integral intersection. Independent integer-grid enumeration confirms every pair minimum. Exact replay checks all 712 input columns. Native hosting remains unchecked; no new kappa is claimed. Hanson Sun, with substantial OpenAI Codex assistance, credits @woklerx's PR1161, Sagar Thakrar's lowerer and the retained supplier lineage. + +| Orientation | Gauges on L251, L427 | Baseline | Candidate | Scalar saving | +|---|---|---:|---:|---:| +| Forward | 1/4, 1/4 | 149002 | 148426 | 576 | +| Backward | 4, 4 | 149018 | 148442 | 576 | + +| Scope / evidence | Value | +|---|---| +| Status | Finite scalar construction; scoped optimization proof | +| Base | `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` | +| Predecessor | [PR1161](https://github.com/CrocSwap/integer-mult-bounds/pull/1161), `d210969d3158a1e6c505e41f67dd84e555c88564` | +| Scalar compiler | Sagar Thakrar, [PR696 lowering](../complex-dyadic-lowering/lower.py) | +| Pair domain | 237 non-center, no-COPY/clear, unwrapped helpers; entry frame 0, exit FULL | +| Exponents | All of `Z²`, including zero | +| Topology | Original ADD operands/order; original SCALE/COPY/clear operations fixed | +| Pair count / orientation | 27966 = 2414 interacting + 25552 separable | +| Vertex evaluations / orientation | 735975 | +| Independent integer-grid evaluations | 19162332, plus separable single-coordinate enumeration | +| Original Horner saving | 416 scalar primitives / complex invocation / orientation | +| Added boundary charges | 8 real shifts = 16 scalar primitives / complex invocation | +| New helpers / frame moves / recursive children | 0 / 0 / 0 | +| Paid profile | Exact equality in both orientations | +| Positive prefix bounds | 52 / 68 bits; retained local charge 192 bits | +| Independent literal inputs | 6 exact dirty-state cases, including coefficient workspace | +| Rejection controls | 16 | +| Excluded | Other helper interfaces; 3+ simultaneous gauges; negative signs; changing existing SCALEs; coefficient-work persistence; native/global invoice admission | +| Inherited | All-size compiler, common-label/mutable-source realization, whole-call hosting, precision/tape, analytic transfer, bit H1–H5 | +| Concurrent comparator | [PR1170](https://github.com/CrocSwap/integer-mult-bounds/pull/1170): stage SCALE consolidation; composition untested | +| License | Apache-2.0 | + +```sh +python3 -I -B research/k8-pair-dyadic-seed25/verify.py +python3 -I -B research/k8-pair-dyadic-seed25/independent.py +python3 -I -O -B research/k8-pair-dyadic-seed25/test_package.py +``` + +```text +PASS_K8_PAIR_DYADIC_CENSUS +PASS_INDEPENDENT_PAIR_GRID_AND_PRIMITIVES +PASS_PAIR_REJECTION_CONTROLS +``` + +## Exact algebra and finite reduction + +```text +h,j in eligible_helpers; (k,l) in Z² +k_h = k, k_j = l, all other k_r = 0 +D = diag(2^k_r) +ADD(t,s,q) -> ADD(t,s,q * 2^(k_t-k_s)) +D^-1 (D A_m D^-1) ... (D A_1 D^-1) D = A_m ... A_1 + +|q_g| = p_g * 2^e_g, p_g positive odd +c(p,e) = 2 + floor(log2(p)) + popcount(p) + |e| - [p=1 and e=0] +f_g(x) = |x| - [p_g=1 and x=0] +Delta(k,l) = 2|k| + 2|l| + + sum_g (f_g(e_g + sigma_g*k + tau_g*l) - f_g(e_g)) +(sigma_g,tau_g) in {(0,0),(1,0),(-1,0),(0,1),(0,-1),(1,-1),(-1,1)} +Delta(k,l) >= 2|k| + 2|l| - sum_g f_g(e_g) - number_of_ADDs + +V = {0} union {-sigma_g*e_g : tau_g=0, sigma_g!=0} +H = {0} union {-tau_g*e_g : sigma_g=0, tau_g!=0} +D_break = {-sigma_g*e_g : sigma_g=-tau_g!=0} +Vertices = {(v,h): v in V, h in H} + union {(v,v-d): v in V, d in D_break} + union {(h+d,h): h in H, d in D_break} + +Delta: lower semicontinuous, coercive, affine on each relative face interior +face boundary discounts <= adjacent affine limits +all nonparallel line-pair determinants = +/-1 +min_(Z²) Delta = min_(R²) Delta = min_Vertices Delta + +M = max_g |e_g| = 15 +Vertices subset [-2M,2M]² +Independent interacting-pair grid = {-31,...,31}² +Separable pairs: min Delta = min Delta_h + min Delta_j +``` + +[Certificate](CERTIFICATE.json) · [Full pair census](PAIR-CENSUS.json.gz) · +[Candidate programs](PROGRAMS.json.gz) · [Task card](CLAIM.json) · +[Sources](SOURCES.json) · [Validation](VALIDATION.json) · +[Retained predecessor proof](vendor/pr1161/PROOF.md) · +[Retained attribution](vendor/pr1161/PROVENANCE.md) diff --git a/research/k8-pair-dyadic-seed25/SOURCES.json b/research/k8-pair-dyadic-seed25/SOURCES.json new file mode 100644 index 0000000000..99db189c2d --- /dev/null +++ b/research/k8-pair-dyadic-seed25/SOURCES.json @@ -0,0 +1,11 @@ +{ + "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "pr1161_head": "d210969d3158a1e6c505e41f67dd84e555c88564", + "vendor": { + "engine.py": "997b34533aea200c339263a96dd6f76facf21bf54b1627ab244e2ae72d348400", + "SOURCES.json": "45f24dbd27239e499600e497e3d86cf812f3b45122088ad083a836e8d646b320", + "BASE-SELECTED.json": "c49e308d209dfbaba184a0d41dbc03cb424663f7ad8136d56aba088bba7f5723", + "PROVENANCE.md": "76dca2049e8c008da0398fd722745e421be92c66dac876cf8463295f6cb18518", + "PROOF.md": "89cbba31b4d95b9c7c69e3bbccd9858e45cd43e1968c39472af7e03fea0e3e54" + } +} diff --git a/research/k8-pair-dyadic-seed25/VALIDATION.json b/research/k8-pair-dyadic-seed25/VALIDATION.json new file mode 100644 index 0000000000..726172ab98 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/VALIDATION.json @@ -0,0 +1,132 @@ +{ + "status": "PASS_SCOPED_FINITE_SCALAR_PACKAGE", + "verified_utc": "2026-10-13T20:14:26.147547+00:00", + "python": "3.14.6 (main, Jun 10 2026, 10:03:53) [Clang 21.0.0 (clang-2100.0.123.102)]", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "base": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "checks": [ + { + "command": "python3 -I -B research/k8-pair-dyadic-seed25/verify.py --write", + "exit_code": 0 + }, + { + "command": "python3 -I -O -B research/k8-pair-dyadic-seed25/verify.py", + "exit_code": 0, + "output": "PASS_K8_PAIR_DYADIC_CENSUS\nbackward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [2, 2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576\nforward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [-2, -2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576" + }, + { + "command": "python3 -I -O -B research/k8-pair-dyadic-seed25/independent.py", + "exit_code": 0, + "result": { + "orientations": { + "backward": { + "baseline_real_primitives": 74509, + "candidate_real_primitives": 74221, + "exact_dirty_cases": 3, + "grid_evaluations": 9581166, + "grid_radius": 31, + "interacting_pairs": 2414, + "pairs": 27966, + "valuation_bound": 15 + }, + "forward": { + "baseline_real_primitives": 74501, + "candidate_real_primitives": 74213, + "exact_dirty_cases": 3, + "grid_evaluations": 9581166, + "grid_radius": 31, + "interacting_pairs": 2414, + "pairs": 27966, + "valuation_bound": 15 + } + }, + "status": "PASS_INDEPENDENT_PAIR_GRID_AND_PRIMITIVES" + } + }, + { + "command": "python3 -I -O -B research/k8-pair-dyadic-seed25/test_package.py", + "exit_code": 0, + "result": { + "positive_fixtures": [ + "shared_unit_edge", + "unit_discount_off_zero" + ], + "rejected": [ + "first_entry_omitted", + "second_entry_omitted", + "first_exit_omitted", + "second_exit_omitted", + "backward_boundary_sign_reversed", + "incident_coefficient_not_conjugated", + "candidate_digest_changed", + "data_register_scaled", + "center_carrier_scaled", + "unit_discount_omitted", + "boundary_scales_unpaid", + "missing_vendor_pin", + "changed_vendor_pin", + "missing_original_source_pin", + "shared_edge_treated_as_two_independent_edges", + "paid_rank_changed" + ], + "status": "PASS_PAIR_REJECTION_CONTROLS" + } + }, + { + "command": "python3 -B scripts/verify_selected_result.py", + "exit_code": 0, + "scope": "selected record/source integrity only" + }, + { + "command": "ruff check research/k8-pair-dyadic-seed25/verify.py research/k8-pair-dyadic-seed25/independent.py research/k8-pair-dyadic-seed25/test_package.py", + "exit_code": 0 + } + ], + "package_mutations": [ + { + "label": "optimized_offline_relocation", + "exit_code": 0, + "wall_seconds": 4.384, + "output": "PASS_K8_PAIR_DYADIC_CENSUS\nbackward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [2, 2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576\nforward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [-2, -2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576" + }, + { + "label": "gzip_header_variation_preserves_payload", + "exit_code": 0, + "wall_seconds": 4.329, + "output": "PASS_K8_PAIR_DYADIC_CENSUS\nbackward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [2, 2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576\nforward pairs 27966 vertices 735975 winner {'helpers': [251, 427], 'exponents': [-2, -2], 'delta_real': -288, 'separate_single_delta_real': -288, 'interaction_delta_real': 0} saving_complex 576" + }, + { + "label": "actual_candidate_coefficient_corruption", + "exit_code": 1, + "wall_seconds": 4.338, + "output": "Traceback (most recent call last):\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 255, in \n main()\n ~~~~^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 244, in main\n need(canonical(programs) == canonical(json.loads(gzip.decompress((HERE / 'PROGRAMS.json.gz').read_bytes()))),\n ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n 'complete candidate program mismatch')\n ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 24, in need\n raise ValueError(message)\nValueError: complete candidate program mismatch" + }, + { + "label": "actual_pinned_source_corruption", + "exit_code": 1, + "wall_seconds": 0.203, + "output": "Traceback (most recent call last):\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 255, in \n main()\n ~~~~^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 233, in main\n result, programs = compute()\n ~~~~~~~^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 198, in compute\n lib = predecessor()\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 42, in predecessor\n need(sha((folder / name).read_bytes()) == digest, 'vendor hash: ' + name)\n ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 24, in need\n raise ValueError(message)\nValueError: vendor hash: engine.py" + }, + { + "label": "actual_certificate_corruption", + "exit_code": 1, + "wall_seconds": 4.121, + "output": "Traceback (most recent call last):\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 255, in \n main()\n ~~~~^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 242, in main\n need(canonical(result) == canonical(json.loads((HERE / 'CERTIFICATE.json').read_bytes())),\n ~~~~^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n 'complete certificate mismatch')\n ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^\n File \"/research/k8-pair-dyadic-seed25/verify.py\", line 24, in need\n raise ValueError(message)\nValueError: complete certificate mismatch" + } + ], + "not_run": [ + "full native admission", + "global hosted invoice", + "full selected cold replay", + "repository-wide historical suites", + "hosted CI", + "Lean theorem" + ], + "compressed_output_equality": "canonical JSON payload; gzip header variation tested", + "upstream_changes": false, + "selected_frontier_changes": false, + "prose_style_pass": { + "status": "skipped_by_explicit_user_authorization", + "authorization": "Skip Emulate and submit PR" + } +} diff --git a/research/k8-pair-dyadic-seed25/independent.py b/research/k8-pair-dyadic-seed25/independent.py new file mode 100644 index 0000000000..a35aa11f12 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/independent.py @@ -0,0 +1,197 @@ +"""Independent integer-grid and literal-primitive check; Hanson Sun, OpenAI Codex. + +Apache-2.0. Imports Sagar Thakrar's pinned lowerer. Does not import verify.py +or PR1161's engine, search, transform, price, invoice, or replay implementation. +""" +from collections import Counter, defaultdict +from fractions import Fraction as F +from functools import lru_cache +import gzip +import hashlib +import importlib.util +from itertools import combinations +import json +from pathlib import Path +import random +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(value, message): + if not value: + raise ValueError(message) + + +def digest(raw): + return hashlib.sha256(raw).hexdigest() + + +def run(): + pins = json.loads((HERE / 'vendor/pr1161/SOURCES.json').read_bytes()) + for name, expected in pins['files'].items(): + data = (ROOT / name).read_bytes() + need(digest(data if name.endswith('.gz') else data.replace(b'\r\n', b'\n')) == expected, + 'source hash: ' + name) + with tarfile.open(ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz') as archive: + def read(name): + data = archive.extractfile('candidate/strict/global8/base/providers/gauge44/' + name).read() + need(digest(data) == pins['archive_members']['slots/local/' + name], 'archive member') + return json.loads(gzip.decompress(data)) + word = read('CANONICAL-WORD.json.gz') + programs = read('LOCAL-PROGRAMS.json.gz') + candidate = json.loads(gzip.decompress((HERE / 'PROGRAMS.json.gz').read_bytes())) + certificate = json.loads((HERE / 'CERTIFICATE.json').read_bytes()) + pair_rows = json.loads(gzip.decompress((HERE / 'PAIR-CENSUS.json.gz').read_bytes())) + for orientation, rows in pair_rows.items(): + raw = json.dumps(rows, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + need(digest(raw) == certificate['orientations'][orientation]['pair_rows_sha256'], 'census binding') + spec = importlib.util.spec_from_file_location('sagar_thakrar_lower', ROOT / 'research/complex-dyadic-lowering/lower.py') + lower = importlib.util.module_from_spec(spec) + spec.loader.exec_module(lower) + helpers = set(range(224, 704)) - set(word['centers']) + for events in programs.values(): + for event in events: + if event[0] == 'residual_adapter': + helpers.discard(event[2]) + if event[0] == 'scalar' and event[1][0] in ('copy', 'clear'): + for register in event[1][1:]: + if isinstance(register, list) and register[0] == 'L': + helpers.discard(register[1]) + helpers = sorted(h for h in helpers if word['start'][h] == 0 and word['final'][h] == 1) + need(len(helpers) == 237, 'exact physical helper domain') + helper_set = set(helpers) + results = {} + + @lru_cache(None) + def literal_cost(numerator, denominator, shift): + q = F(numerator, denominator) * F(2) ** shift + return len(lower.lower(['add', ['L', 0], ['L', 1], q.numerator, q.denominator])) + + def valuation(q): + exponent = 0 + q = abs(q) + while q.denominator > 1: + q *= 2 + exponent -= 1 + while q.numerator % 2 == 0: + q /= 2 + exponent += 1 + return exponent + + for orientation, events in programs.items(): + by_helper = {h: Counter() for h in helpers} + by_pair = defaultdict(Counter) + max_valuation = 0 + for event in events: + if event[0] != 'scalar' or event[1][0] != 'add': + continue + gate = event[1] + t, s = gate[1:3] + n, d = gate[3:5] + q = F(n, d) + max_valuation = max(max_valuation, abs(valuation(q))) + for register, sign in ((t, 1), (s, -1)): + if register[0] == 'L' and register[1] in helper_set: + by_helper[register[1]][n, d, sign] += 1 + if t[0] == s[0] == 'L' and t[1] in helper_set and s[1] in helper_set: + a, b = sorted((t[1], s[1])) + by_pair[a, b][n, d, t[1] == a] += 1 + + # Every vertex of k=c, ell=c, k-ell=c lies inside [-2M,2M]^2 + # when all nonzero intercepts have magnitude at most M. Search the + # ENTIRE integer square, plus its outer ring; no vertex routine is used. + radius = 2 * max_valuation + 1 + grid = range(-radius, radius + 1) + singles = {} + for h, terms in by_helper.items(): + singles[h] = {k: 2 * abs(k) + sum(count * (literal_cost(n, d, sign * k) - literal_cost(n, d, 0)) + for (n, d, sign), count in terms.items()) for k in grid} + rows = {(row[0], row[1]): row for row in pair_rows[orientation]} + need(set(rows) == set(combinations(helpers, 2)), 'complete pair inventory') + need(certificate['orientations'][orientation]['helpers'] == helpers, 'helper domain equality') + grid_evaluations = 0 + minima = [] + for a, b in combinations(helpers, 2): + edges = by_pair.get((a, b), {}) + if not edges: + # Independent separable enumeration, not Cartesian vertex enumeration. + ka = min(grid, key=lambda k: (singles[a][k], abs(k), k)) + kb = min(grid, key=lambda k: (singles[b][k], abs(k), k)) + best = (singles[a][ka] + singles[b][kb], abs(ka) + abs(kb), ka, kb) + else: + # Tabulate the shared ADD price directly from primitive lengths. + coupled = {difference: sum(count * literal_cost(n, d, difference if target_a else -difference) + for (n, d, target_a), count in edges.items()) + for difference in range(-2 * radius, 2 * radius + 1)} + baseline_shared = coupled[0] + solo_a = {k: sum(count * literal_cost(n, d, k if target_a else -k) + for (n, d, target_a), count in edges.items()) for k in grid} + solo_b = {k: sum(count * literal_cost(n, d, -k if target_a else k) + for (n, d, target_a), count in edges.items()) for k in grid} + best = min((singles[a][ka] + singles[b][kb] + coupled[ka - kb] + - solo_a[ka] - solo_b[kb] + baseline_shared, + abs(ka) + abs(kb), ka, kb) for ka in grid for kb in grid) + grid_evaluations += len(grid) ** 2 + need(best[0] == rows[a, b][3], 'pair optimum: ' + str((a, b))) + # Primary tie choice is among vertices; an interior grid point may tie. + minima.append((best[0], a, b)) + selected = certificate['orientations'][orientation]['winner'] + need(min(minima) == (selected['delta_real'], *selected['helpers']), 'global minimum') + new_events = candidate[orientation] + need([e for e in events if e[0] != 'scalar'] == [e for e in new_events if e[0] != 'scalar'], + 'non-scalar event identity') + old_ops = [op for e in events if e[0] == 'scalar' for op in lower.lower(e[1])] + new_ops = [op for e in new_events if e[0] == 'scalar' for op in lower.lower(e[1])] + price = certificate['orientations'][orientation]['prices']['copy-init'] + need(len(old_ops) == price['before']['real_primitives'], 'baseline literal count') + need(len(new_ops) == price['after']['real_primitives'], 'candidate literal count') + need(len(new_ops) - len(old_ops) == selected['delta_real'], 'literal saving') + rng = random.Random(25 + (orientation == 'backward')) + all_registers = [('L', i) for i in range(704)] + [('C', i) for i in range(8)] + [('W', 0)] + for case in range(3): + original = {r: F(rng.randrange(-10000, 10000), 2 ** rng.randrange(4)) for r in all_registers} + if case == 1: + original.update({('L', i): F((-1) ** i * (i + 1) ** 3, 8) for i in range(224, 704)}) + if case == 2: + original.update({('L', i): F(0) for i in range(224)}) + expected = original.copy() + for i in range(112): + if orientation == 'forward': + expected['L', 112 + i] += original['L', i] + else: + expected['L', i] -= original['L', 112 + i] + for i in range(8): + expected['C', i] = F(0) + expected['W', 0] = F(0) + for operations in (old_ops, new_ops): + state = original.copy() + for op in operations: + tag, target = op[:2] + if tag == 'clear': + state[target] = F(0) + elif tag == 'copy': + state[target] = state[op[2]] + elif tag == 'double': + state[target] *= 2 + elif tag == 'halve': + state[target] /= 2 + elif tag == 'negate': + state[target] = -state[target] + elif tag == 'add': + state[target] += state[op[2]] + elif tag == 'subtract': + state[target] -= state[op[2]] + else: + raise ValueError('unknown primitive') + need(state == expected, 'literal dirty-state endpoint') + results[orientation] = {'pairs': len(rows), 'interacting_pairs': len(by_pair), + 'valuation_bound': max_valuation, 'grid_radius': radius, + 'grid_evaluations': grid_evaluations, 'exact_dirty_cases': 3, + 'baseline_real_primitives': len(old_ops), 'candidate_real_primitives': len(new_ops)} + return {'status': 'PASS_INDEPENDENT_PAIR_GRID_AND_PRIMITIVES', 'orientations': results} + + +if __name__ == '__main__': + print(json.dumps(run(), sort_keys=True)) diff --git a/research/k8-pair-dyadic-seed25/test_package.py b/research/k8-pair-dyadic-seed25/test_package.py new file mode 100644 index 0000000000..4724bfb29e --- /dev/null +++ b/research/k8-pair-dyadic-seed25/test_package.py @@ -0,0 +1,94 @@ +"""Semantic rejection controls. Hanson Sun / OpenAI Codex, Apache-2.0.""" +import copy +import gzip +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location('pair_verifier', HERE / 'verify.py') +v = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(v) + + +def main(): + lib = v.predecessor() + word, original, _, _ = lib.load() + programs = json.loads(gzip.decompress((HERE / 'PROGRAMS.json.gz').read_bytes())) + cert = json.loads((HERE / 'CERTIFICATE.json').read_bytes()) + rejected = [] + + def reject(name, operation): + try: + operation() + except (ValueError, KeyError): + rejected.append(name) + else: + raise ValueError('incorrectly accepted control: ' + name) + + forward = programs['forward'] + for index, name in ((1, 'first_entry_omitted'), (2, 'second_entry_omitted'), + (-2, 'first_exit_omitted'), (-3, 'second_exit_omitted')): + bad = copy.deepcopy(forward) + bad.pop(index) + reject(name, lambda bad=bad: lib.replay(bad, 'forward')) + + bad = copy.deepcopy(programs['backward']) + bad[1][1][2:4] = [1, 4] + reject('backward_boundary_sign_reversed', lambda: lib.replay(bad, 'backward')) + + bad = copy.deepcopy(forward) + for event in bad: + if event[0] == 'scalar' and event[1][0] == 'add' and ['L', 251] in event[1][1:3]: + event[1][3] *= 2 + break + reject('incident_coefficient_not_conjugated', lambda: lib.replay(bad, 'forward')) + reject('candidate_digest_changed', lambda: v.need(v.sha(v.canonical(bad)) == cert['orientations']['forward']['candidate_sha256'], 'hash mismatch')) + + reject('data_register_scaled', lambda: lib.transform(original['forward'], word, 12, -2)) + reject('center_carrier_scaled', lambda: lib.transform(original['forward'], word, 224, -2)) + reject('unit_discount_omitted', lambda: v.need(lib.price(lib.Q(1)) == 3, 'unit costs two')) + price = cert['orientations']['forward']['prices']['copy-init'] + reject('boundary_scales_unpaid', lambda: v.need(price['saving_complex'] == 592, 'eight real boundary shifts paid')) + + pins = json.loads((HERE / 'SOURCES.json').read_bytes()) + badpins = copy.deepcopy(pins) + del badpins['vendor']['engine.py'] + reject('missing_vendor_pin', lambda: v.predecessor(badpins)) + badpins2 = copy.deepcopy(pins) + badpins2['vendor']['engine.py'] = '0' * 64 + reject('changed_vendor_pin', lambda: v.predecessor(badpins2)) + baseline_pins = json.loads((HERE / 'vendor/pr1161/SOURCES.json').read_bytes()) + del baseline_pins['files'][next(iter(baseline_pins['files']))] + reject('missing_original_source_pin', lambda: lib.check_sources(baseline_pins)) + + # A shared unit ADD does not equal the sum of two isolated gauge prices. + # Both registers doubled leaves its coefficient 1. Boundary shifts cost 4. + shared = [['scalar', ['add', ['L', 251], ['L', 427], 1, 1], 0]] + small = v.census(lib, shared, [251, 427]) + both_plus_one = small['rows'][0][2][10] + v.need(both_plus_one == 4, 'shared-edge interaction fixture') + reject('shared_edge_treated_as_two_independent_edges', lambda: v.need(both_plus_one == 8, 'interaction correction required')) + + # A unit shortcut can beat the lower weighted median: preserve its point dip. + discount = [['scalar', ['add', ['L', 251], ['L', x], 1, 2], 0] for x in (0, 1)] + exact = v.exact_census(lib, discount, [251, 427]) + v.need(exact['winner']['exponents'] == [1, 0] and exact['winner']['delta_real'] == -2, + 'nonconvex unit-discount optimum') + + # Changed physical events may leave scalar endpoints untouched, so compare + # the complete event stream separately instead of accepting map equality. + bad = copy.deepcopy(forward) + for event in bad: + if event[0] == 'climb': + event[5] += 1 + break + reject('paid_rank_changed', lambda: v.need( + [e for e in bad if e[0] != 'scalar'] == [e for e in forward if e[0] != 'scalar'], + 'physical stream mismatch')) + print(json.dumps({'status': 'PASS_PAIR_REJECTION_CONTROLS', 'rejected': rejected, + 'positive_fixtures': ['shared_unit_edge', 'unit_discount_off_zero']}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/k8-pair-dyadic-seed25/vendor/pr1161/BASE-SELECTED.json b/research/k8-pair-dyadic-seed25/vendor/pr1161/BASE-SELECTED.json new file mode 100644 index 0000000000..74e4acfe73 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/vendor/pr1161/BASE-SELECTED.json @@ -0,0 +1 @@ +{"audited_source_head":"0fc329d0bec93ca7cd288eaea1295172e8789810","certificate":"research/community-frontier1094-audit/ASSEMBLY.json","certificate_sha256":"1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045","decimal":"0.001672660197076918","kappa":"836330098538459/500000000000000000","previous_kappa":"1672188119205421/1000000000000000000","previous_record":"certificates/checkpoints/frontier1042.json","proof":"docs/research/community-batch1099-review.md","proof_supplements":{".github/workflows/t37-owners.yml":"c13acc2902c007237103072b7ec10caf5ca21c1b319d27934f194af2f7d87026","certificates/replay-coverage/pr741-sw4-v1.json":"7acd5033bc78e3f473718269edaa267c2785d84fbe95ccf6815a33dcf58c2756","docs/research/community-batch1047-review.md":"a6271faf5db0afe3ff7d24a34a3be7a959cdc33ee37784572fba014ee5358787","docs/research/community-batch1099-review.md":"7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb","docs/research/community-batch952-review.md":"04db59dfc2c31453229b6061bbf59547e71ce3abdc0ce0f6779144bb0dde127b","docs/research/community-cold617-review.md":"b3f2bcbae1249f1f651032022ce1e6e2bfb3f563ce580bf53671f50a074d7046","docs/research/community-frontier741-review.md":"4634694fa75ea9e749ecf19d3db3e4d82effe3b61a2efdf08ac5a97275fb676a","docs/research/community-frontier799-review.md":"bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052","docs/research/community-frontier890-review.md":"cd03b7c2c6c09db2cfa89ae40133ae44e1deb6e32ec5ddd23aacecc9c50f2fea","docs/research/community-hyperplane599-review.md":"3298cd0d451541508af232cac72efbd7c10580e6c6ad493a855ab0faa01ade8c","docs/research/community-k492-review.md":"3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47","research/community-batch1099-audit/check_frontier1094.py":"2608ef213260a43d09a40b3429742f7a5f280861b54acae66400a7c29a123f51","research/complex-571-cold14-b3/PROOF-NOTE.md":"1cf592cbc8ab8e21d2dd8c1e945a5c64c6d5cde1216fb06e05a36c1c6ec6613d","research/complex-571-cold14-b3/README.md":"1945785785c153c7d0e8d4c071adabe626c1091b71721ff85d2d67191b376b96","research/complex-571-free4fc8/NOTICE.md":"a4c084abdc1c7a9ac683eeb11124335d51cff8a6deba6ee92ba5a12bceaa2c97","research/complex-571-hpeq5/README.md":"4000b37f6c07c09d971dc4010ceb137c13340f3a8809d3272046ccaf746c3e2b","research/complex-double-replica-owners/PROOF.md":"db99599e3966bec253c577c23915e2a2899c4c4e8568044efc11c7918b137bbc","research/complex-joint-prefix/proof/CONSTRUCTION.md":"a92e610e7a598d99c612d1b63d1a03a49c0cd1e15ddd29fa55c465ddd8c18105","research/complex-k492-owner-repair/PROOF-NOTE-R.md":"22312bb347bdf159e6a01a45c47675e6170d33b258e2fd9ed52aee88fb92c0ed","research/complex-k492-owner-repair/PROOF-NOTE.md":"337d70fe7abd9afca1d90954c23bde87f4dc27888cc1a6b4bb80506fd6fbf8c5","research/complex-k492-owner-repair/README.md":"ee5a1ace4828f7a073be97e95c2d931988774dd3a29a877e65abdf429aeec902","research/complex-multicold/proof/CONSTRUCTION.md":"27ece5e1c11b90d97a808b56eff897b998c10e61016db95867f84e6e6aef132f","research/complex-multicold/vendor/pr559/PROOF.md":"d5d498edc56fdef8c5798af7f5ec66948bd2f66c553b9efe366cdaab01bd3453","research/complex-sw4-frame8/PROVENANCE.md":"c7648719b01dd93af2c3a2c6e951a54711d13892dc4bd4339d16edb4c37c9bf0","research/complex-t21-owner-bound/PROOF.md":"2aa0aa6ec1d87402138564c38749b5ca0f058c16817efdf58a2685d2d90cb417","research/complex-t21-owners/PROOF.md":"78721b32fceb34b21b8e77c95381c38c60276e72e6d9c2e9c6262cb347457def","research/complex-t37-owners/ALL-T-PROOF.md":"4c0c71ccd0afb850538af1b467e5208b7eb3edd0260fded84e02a8c01dfc868b","research/complex-t37-owners/PROOF.md":"09b39ad0d5f1f59f54dcff15c16640f7a7acf27e6597660acaf957b95c7e8510","research/e8-bit-p111-tuned/tune/README.md":"46c7917fb252949f38b7bcd88cf568efc282e3ea065b61d11e457e41673d0b2d","research/e8-bit-r420/README.md":"9807be57c6adf26b30e4f54e2f8160075bbc05091f1a6d157e43d2a4620c1c9f","research/gauge44-barch/PROOF-NOTE-BARCH.md":"c24f211b09358b25d6cf47dd18e4bbd8bcf4ecf279e6f1c6c90613cfa230818d","research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md":"39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036","research/hyperplane-end-lean/HyperplaneEnd/Exact.lean":"eebf3a3982af7ab9be45777b272a6aaa523206fa7667ceb6df63ad6589fd8183","research/hyperplane-end-lean/PROOF.md":"1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9","research/kernel-frame-coalescing/PROOF.md":"fa8b2f36b9590ee80ff45d3f7724f8c7de8ad29a29f366d5133010c77e41fe1b","research/structural-gain/frontier-composition/README.md":"70f0f791cbe3b2603f85d85bb9055aa0ee1df6dc06ba82fc1921356948312887","scripts/verify_cold617_interface.py":"95d7a9094c05ad975fb72f5ab7605593003245a503c8456764987e512028fa6a","scripts/verify_frontier1042.py":"700fdcaeb6e8f57f6e63c71c2dd1652fc5b183e8d706cd092779bdc0d271e854","scripts/verify_frontier1094.py":"c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949","scripts/verify_frontier588_bindings.py":"6d1932eea7b1936598118ea8e607b09c29b6e31b749ec41bbe0744ea4f0b606d","scripts/verify_frontier626.py":"2207bd0ef04a19ef276869085afdedad80a0938fa75db5e1aa7ab73fd3429444","scripts/verify_frontier626_bindings.py":"cda63ff41c6d6e2e352c7bf75b84e690c0ce57e4ec6c0355573bb5d9b1f98280","scripts/verify_frontier741.py":"215ee6a12de8dc2392e6811a1b8f2140035f6b2d2a0d2100ff4bd2fdcb8bb39b","scripts/verify_frontier741_bindings.py":"eff455167e2fd0bc9a67d35241d0e69d8edc58f3a23e776dcfe8f500ca8e8d67","scripts/verify_frontier741_bridge_coverage.py":"9a14f26762b6126eb54ed43db90371773374fe98733ada80ee871a74afa3b836","scripts/verify_frontier799.py":"19fe1b32079095160dc00fe2f7df75e0fcbc82cff37f7159b755c8a63bd5ce99","scripts/verify_frontier799_bindings.py":"43897b3c99212d6134870898a1840f32898aa1b3679b299e654901568ad7e19b","scripts/verify_frontier890.py":"88ea38dbef62dd7c0dd46e212618520cc89213edddb2032800e5509993958175","scripts/verify_frontier942.py":"27c6713532d9f53f55dfff4884d55a2d9ae74b68156e37a44596c0418fbed5b7","scripts/verify_hpe_lean_binding.py":"52aa1d23641e4c716b43c98f6b883ad042087dd03a9d01369e8e6a735b07aa03","scripts/verify_replay_coverage.py":"babe5941d7e6dac4248613ef01f950ee7bb6199e7355021aea4cf854fd1b91c5"},"reproduce":"make frontier1094-verify","review":"docs/research/community-batch1099-review.md","reviewed_dependency_heads":{"1004":"1974578f82a30158dd5fcdcdf226b83df8e7196f","1005":"779e80aef469bc3a28b19f1adde199871a9a22e3","1018":"eac7547cb191f875d5f5ea5f9bbb1d2b8c51c4ef","1022":"58618bcbfe88a252467755fc283c04c3db5ca4fd","1028":"be4bd89cb4483dcee43257200cd27601f938f13d","1031":"e900534f0beda892c726723524203b97471fb9a3","1042":"7e8ef087c02a77038a28a337a7ee3a77039cac0d","1050":"c87242f846cfab8c0b97fd889b5fecb0eacef939","1053":"6f92ce8884929c9fd4730c86a28e2e3735de02af","1055":"a8ea308976f1709eef0a328463f010cf51469277","1056":"d0201efbd68c4acc9832b84bcc986c8781b83c4f","1061":"223f581afb1d63d5f8476a69040617e11bcd50e4","1063":"d9377d32e0c97e41338e704c3960fd6f2fa73806","1065":"387d935e354a931d636e2c5e6ee63a6910f78a1b","1068":"cc71375eae4e8754da0f5d940cb519d66625fb2e","1074":"052afc128954f7b6a2b3c409eb4d72248e4020f2","1082":"0c2e294ec204e83846d27344f829d15ed9ee7cc6","1087":"589d1cedf5ef5f231182f4ec86408616311a8af0","1094":"0fc329d0bec93ca7cd288eaea1295172e8789810","543":"2065fe4f72a914d907f1046603f5a36f17018535","568":"71c99ac935a33bb7b59a1b4a7af8725a939b0b90","569":"1424da81263a5305b35e4cf74ef686c275f03f3f","571":"b7bdc5a8de18fcf418cfb9c7d83a2b1097a5e4a3","575":"eac6f7e378ab622dac50a2fd4b7ef6eab014de44","583":"89be768f0157f5a3d8e4db69cf1748768605eac9","586":"4846fee5b06af770e9b3a10c36200f673d656725","588":"6d0e53b66c29abd17981881a09eaff41ac862d85","589":"a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46","591":"f622547244bf6d895a571a7b035142ba66279806","592":"1f471c445c06a45a32e2c47e8d74c8264b68356b","593":"fdb6dcc6d7bc29764c5b6b4d32b7fa050acf74a4","596":"7732dd5e46863ff294b5e443661cb9d99abf4e01","599":"bc13c8a3e000442606bd2dbe8583a17649ba6c32","601":"529ab7dcb59d5ea7a5798e9e06cf5b3aee8a1550","604":"1b795c5d7dea746ba310572585c0ef067574b4a6","615":"bf8a49a34350599763cced8592db81dc62c2c1c0","617":"904d62855723c00f8acef9a287a10768598fdeb2","622":"f69477f4f6d3c7eb1f740b166881bffed4ffa9f6","623":"e39a615ca601ce5d62abeb24f3fcdb8644ca1005","626":"660de893d27bb7abd1d5b01b1640207528a5c851","741":"e516b1463606840a15f80aac1995d64ce0092e89","799":"80e6463157cfc80b85af09e7e2f14748fe2dac60","858":"ae2e25fee91540c83ceee5a60e3b07422ce21c7d","869":"73e86f69bf9a391e3c334999f7bbe3825dc42759","870":"b734850dc348800942f0ffd1f0723fdec7539b2b","890":"4b3bd8cbe8e3e81c44161017c9b72c905a8040a8","942":"1960cfa919a0945d0ca4cb14ea96237000037903","987":"5142511af0437572aca71b35d1987cd2b47bb5e3"},"scope":"Finite composition under inherited all-size/compiler, common-label/mutable-source, whole-call hosting, precision/tape, analytic and bit H1-H5 assumptions. Not a full Lean multiplication theorem.","source_manifest":"research/community-frontier1094-audit/SELECTED-SOURCE.json","source_prs":[1094,1087,1082,1074,1068,1065,1063,1061,1056,1055,1053,1050,1042,1031,1028,1022,1018,1005,1004,987,942,890,870,869,858,799,741,699,685,676,664,660,659,656,655,653,658,649,645,635,589,555,545,626,623,622,620,617,615,604,601,596,592,591,593,599,588,543,584,586,583,582,579,576,575,574,571,569,568,567,564,562,561,559,558,552,550,548,541,535,510,503,531,523,493,514,507,484,496,505,522,520,472,458,445,442,425,433,370,361,315],"status":"Maintainer-reviewed conditional finite construction; see the integration receipt for publication and PR resolution status","validation":"docs/research/community-batch1099-integration.json"} diff --git a/research/k8-pair-dyadic-seed25/vendor/pr1161/PROOF.md b/research/k8-pair-dyadic-seed25/vendor/pr1161/PROOF.md new file mode 100644 index 0000000000..d2925051c5 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/vendor/pr1161/PROOF.md @@ -0,0 +1,106 @@ +# Scope and exact algebra + +Fix one non-center helper h and k in Z. Let D multiply its entire scalar register +by2^k and leave every other data, helper and center coordinate fixed. An ADD +`t += q*s` becomes `t += (q*2^(k_t-k_s))*s`, where k_h=k and all other k_i=0. +Each existing SCALE commutes with D and is left literally unchanged. Clear/COPY +events have no incidence with h by the definition of the477-helper domain. + +For chronological original operations A1,...,Am, the new chronological word is +D, DA1D^-1,...,DAmD^-1,D^-1. Its matrix is + +```text +D^-1 (DAmD^-1) ... (DA1D^-1) D = Am ... A1. +``` + +This equality holds on all input vectors, including arbitrary helper dirt. It +does not assume a helper is initially zero. The stored backward program is +checked independently; the inverse-transpose coefficient rule changes the +chosen basis to D^-1 (k=+2), in the same chronological direction, rather than +naively reusing k=-2. Both candidate and original forward transfer are +`Y += X`, and both backward transfers are `X -= Y`, preserving480 helpers and +clearing8 centers. The sparse rational replay includes each center's initial +dirty column, not merely zero center initialization. + +All unchanged non-scalar operations act linearly on an individual register; +uniform scalar multiplication commutes with them. Center operations act on the +separate C registers. Excluding helper COPY sources ensures they commute too. +The selected candidate h427 starts in frame0 and ends in FULL frame1, and has +no residual wrapper. Its entry scale is after the zero-precondition phase +marker; the exit is after full-frame cleanup, before the done marker. This is +why the concrete stream requires no new frame climb or wrapper. Coefficient +changes use the original operands and frame labels. Native type/admission +replay and the complete hosted/compiler invoice remain separate obligations. + +# Actual retained cost, including the unit discontinuity + +For reduced q with |q|=p*2^e and positive odd p, Sagar Thakrar's retained +copy-init lowerer emits + +```text +c(p,e) = 2 + floor(log2(p)) + popcount(p) + |e| - 1[p=1 and e=0]. +``` + +The shortcut at q=+1 or-1 costs2: signed direct ADD followed by work clear. +Otherwise COPY initializes work from the source; numerator Horner steps, any +denominator halvings, signed accumulation and final clear are all charged. +The old Horner formula is `3+floor(log2(p))+popcount(p)+|e|`. +SCALE by a signed power of two costs `|e|+1[q<0]`. New boundary scales are +positive and cost2|k| in total, per real component. Real and imaginary words +each incur this complete cost. + +For each ADD incident with h, set s=+1 when h is its target and s=-1 when h is +its source. The exact change is + +```text +Delta_h(k) = 2|k| + sum_g ( c(p_g,e_g+s_g*k) - c(p_g,e_g) ). +``` + +No unchanged SCALE or disjoint ADD contributes a delta. Complete invoices +nevertheless recount them, and also count all clears/COPYs. The coefficient +work is arbitrary on entry: non-unit COPY overwrites it; unit direct ADD does +not read it; every macro clears it on exit. The independent checker executes +the predecessor's literal primitive words, including that work register. + +# Why finitely many exponents certify an unbounded optimum + +Let B={0} union {-s_g*e_g}. All absolute-value slope changes and all negative +unit discounts occur at integer points of B. Between consecutive points the +undiscounted objective is affine and there are no discounts. An affine function +attains its minimum at an endpoint (or is constant); the possible negative +discounts at endpoints only strengthen this conclusion. Outside the extreme +points every absolute-value term has the same outward slope, so the objective +increases with slope `2 + number_of_incident_ADDs`. Therefore at least one global +integer minimizer is in B. The method does not assume convexity of the discounted +function and is not simply a weighted-median argument. + +The certificate prices every B point for all477 helpers, including k=0, in both +orientations. It uses (cost,|k|,k) to resolve per-helper ties and then helper index +for global ties. The independent method enumerates *every* integer from two +below to two above the extreme valuations and derives the outward slope using +the actual lowerer's lengths. It agrees with every per-helper certificate row. +The unique global winner in each orientation is h427, with123 incident ADDs; +forward costs at k=-4,-3,-2,-1,0,1 are75,-46,-166,-128,0,132 relative to baseline. +The backward list is reflected. No exponent cutoff assumption is used. + +The pure unit-discount control has two incident coefficients1/2: the continuous +absolute-value objective is constant between k=0 and1, so the lower weighted +median is0; the correct discounted price strictly prefers1 by2 primitives. + +# Prefix and admission boundary + +For the source-bound positive scalar envelope, each original L/C register starts +with majorant1, clears set it to0, COPY copies it, SCALE multiplies by|q|, and +ADD replaces the target majorant by target+|q|*source. During non-unit numerator +Horner construction, the work majorant is at most |numerator(q)|*source before +denominator halvings. Unit direct ADD does not touch work until it clears. +Starting coefficient work at arbitrary unit majorant1 covers its dirty entry. +This exact rational recurrence accounts for every emitted primitive's absolute +coefficient majorant. Its complete maximum is unchanged at52/68bits, below192. + +These are scalar-majorant and exact map certificates for one finite provider +word, with actual retained lowering. They are not a rerun of the native checker, +global512-bit accounting, row inventory/packing admission, or the outer root. +The477-helper cost optimum fixes all other coordinate scales; joint scaling, +center normalization, phase-varying diagonals, stage retiming and coefficient +work persistence lie outside the class. The current selected result is retained. diff --git a/research/k8-pair-dyadic-seed25/vendor/pr1161/PROVENANCE.md b/research/k8-pair-dyadic-seed25/vendor/pr1161/PROVENANCE.md new file mode 100644 index 0000000000..6ee8cde472 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/vendor/pr1161/PROVENANCE.md @@ -0,0 +1,46 @@ +# Attribution and scope selection + +Prepared by @woklerx with substantial OpenAI Codex assistance, Apache-2.0. +No independent human review is claimed. Original source notices are retained. + +The current frozen construction is Rohan Arun's PR1094 rare-pattern exchange +placement on Jeremy Kothe's checked k8/T16 supplier, following PR1042. Its actual +archived gauge44 provider is byte-identical to the pinned slots/local provider +in the PR1042 archive. Douglas Colkitt's review, selected-source and complete +assembly receipts establish the inherited lineage; this package does not claim +to authenticate or repeat those native/global executions. The scalar program +and exact local invoice are from the credited icekylinx/PR425/433/531, +Jeremy Kothe/PR622 and gauge44-slots construction lineage. The stronger lowering +is Sagar Thakrar's `research/complex-dyadic-lowering/lower.py`, whose retained +source is imported by the independent checker. The optimum accounts for its +unit shortcut and does not claim an old-Horner gain that disappears there. + +Seed32 is the assigned complex-supplier track at fixed base +`ce7ad1b6ab09452c3478723a2e96ed5ff212dc08`. Three candidates considered: + +1. Uniform dyadic basis change on one complete-program helper (chosen). +2. Further coefficient-work sharing/rescaling (rejected as close to PR739/811, + PR984 and previous sprint round7/PR1032). +3. Frame-transition retiming (rejected as close to rounds26/29). + +Targeted live Curiosity Bot GitHub provider queries covered dyadic conjugation, +diagonal gauge, rescaling, scalar and helper work. PR739 was inspected directly: +it keeps private coefficient work across successive magnitude blocks, not a +uniform helper coordinate change through the full scalar word. PR836 concerns +unitary register mixing; PR426/401 concern other chronological/response gauges. +PR947 prices constant-row center shears; PR1081 fixes CK helper matching. +None supplies this one-helper unbounded valuation/discount certificate. + +Concurrent round31 was coordinated explicitly: it carries *existing* SCALEs +through stage A/B with a time-varying diagonal and consolidates them at stage +boundaries. This package fixes every existing SCALE and inserts two new inverse +boundary scales for one helper across all phases. Neither result asserts that +the two savings compose. Earlier rounds22 butterflies,23 cell minimum,25 dirt +span coverage,26 commuting frame barrier and29 Clifford transition rank have +different mechanisms and obligations. + +The exact mandatory source inventory uses LF-normalized text hashes and exact +binary/archive bytes. Archive member hashes bind original gzip containers, not +recompressed equivalents. Candidate hashes use sorted-key canonical JSON with +integer/list schema. Frozen selection and exact base are context; verification +does not require the mutable selected-result pointer still to select PR1094. diff --git a/research/k8-pair-dyadic-seed25/vendor/pr1161/SOURCES.json b/research/k8-pair-dyadic-seed25/vendor/pr1161/SOURCES.json new file mode 100644 index 0000000000..841bf21533 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/vendor/pr1161/SOURCES.json @@ -0,0 +1 @@ +{"archive_members":{"slots/local/CANONICAL-WORD.json.gz":"16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219","slots/local/INDEPENDENT-LOCAL-REPLAY.json":"13dd18297162569532983db1a2ab67926b064330cd7edd3587e7b546b2dedf17","slots/local/LOCAL-CHECKS.json":"2b8b1891a736598010232bfb26abc31973b265a53a2009a3fcfd9138b5ecadb4","slots/local/LOCAL-PROGRAMS.json.gz":"241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a"},"base":"ce7ad1b6ab09452c3478723a2e96ed5ff212dc08","files":{"docs/research/community-batch1099-review.md":"7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb","research/community-frontier1042-audit/RESULT.json":"bf12c6ed3b412539638b76addb40591a631609b2ab9e5ee0db1f6bbe067d0ec0","research/community-frontier1042-audit/selected-replay.tar.gz":"22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754","research/community-frontier1094-audit/ASSEMBLY.json":"1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045","research/community-frontier1094-audit/RESULT.json":"1e3e47e9ec24bcb6fb5f703b7fce0aab658d84ff72bfae5da3ae429d17b6e752","research/community-frontier1094-audit/selected-replay.tar.gz":"f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6","research/complex-dyadic-lowering/README.md":"798209e9869d1612a2c34412ef2eb87c0eb0dcebcbed9963a45e0fe248326c2f","research/complex-dyadic-lowering/lower.py":"eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753","research/gauge44-slots/code/invoice_allcold.py":"141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec","research/gauge44-slots/independent/audit_local.py":"03afcfc9da428b3f6edac81c1fee7f277ab81b64998efae78380b63498dec6cd","scripts/verify_frontier1094.py":"c7e20f59968ed5736fb859735de4de207de3418083e37012310ebcded946b949"},"format":"exact-inventory-text-lf-binary-exact-sha256-v1","selected_snapshot_sha256":"cba7a81945a737a475251e77c6a1da21ffbc22d56ea835f4ee7dfbb813ae796e"} diff --git a/research/k8-pair-dyadic-seed25/vendor/pr1161/engine.py b/research/k8-pair-dyadic-seed25/vendor/pr1161/engine.py new file mode 100644 index 0000000000..33c0db7fe7 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/vendor/pr1161/engine.py @@ -0,0 +1,209 @@ +"""One-helper dyadic basis search. @woklerx with OpenAI Codex, Apache-2.0. + +Retained copy-init lowering: Sagar Thakrar's complex-dyadic-lowering/lower.py; +original Horner vocabulary: icekylinx PR425/433/531, Jeremy Kothe PR622. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +import copy, gzip, hashlib, json, tarfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = 'ce7ad1b6ab09452c3478723a2e96ed5ff212dc08' +ARCHIVE = 'research/community-frontier1042-audit/selected-replay.tar.gz' +REQUIRED = frozenset([ + ARCHIVE, 'research/community-frontier1042-audit/RESULT.json', + 'research/community-frontier1094-audit/selected-replay.tar.gz', + 'research/community-frontier1094-audit/RESULT.json', + 'research/community-frontier1094-audit/ASSEMBLY.json', + 'docs/research/community-batch1099-review.md', + 'scripts/verify_frontier1094.py', + 'research/complex-dyadic-lowering/lower.py', + 'research/complex-dyadic-lowering/README.md', + 'research/gauge44-slots/code/invoice_allcold.py', + 'research/gauge44-slots/independent/audit_local.py']) +MEMBERS = ('CANONICAL-WORD.json.gz','LOCAL-PROGRAMS.json.gz', + 'INDEPENDENT-LOCAL-REPLAY.json','LOCAL-CHECKS.json') + +def require(value, message): + if not value: raise ValueError(message) + +def canonical(value): + return json.dumps(json.loads(json.dumps(value)), sort_keys=True, + separators=(',', ':'), allow_nan=False).encode() + +def digest(data): return hashlib.sha256(data).hexdigest() +def pin(path): + b = path.read_bytes() + return digest(b if path.name.endswith('.gz') else b.replace(b'\r\n',b'\n')) + +def check_sources(manifest=None): + m = manifest if manifest is not None else json.loads((HERE/'SOURCES.json').read_bytes()) + require(m['base'] == BASE and set(m['files']) == REQUIRED, 'source inventory') + require(set(m['archive_members'])=={'slots/local/'+n for n in MEMBERS},'archive member inventory') + for p,d in m['files'].items(): require(pin(ROOT/p)==d, 'source pin '+p) + selected=json.loads((HERE/'BASE-SELECTED.json').read_bytes()) + require(digest(canonical(selected))==m['selected_snapshot_sha256'],'selected snapshot') + require(selected['kappa']=='836330098538459/500000000000000000','selected kappa') + old=json.loads((ROOT/'research/community-frontier1042-audit/RESULT.json').read_bytes()) + current=json.loads((ROOT/'research/community-frontier1094-audit/RESULT.json').read_bytes()) + require(current['baseline_receipt_sha256']==digest((ROOT/'research/community-frontier1042-audit/RESULT.json').read_bytes()),'selected baseline receipt') + require(old['status']=='PASS_COMPLETE_PR1042_COMPOSITION' and current['status']=='PASS_COMPLETE_PR1094_COMPOSITION','selected receipt statuses') + return m + +def load(): + m=check_sources(); objs={} + with tarfile.open(ROOT/ARCHIVE) as t: + for n in MEMBERS: + name='slots/local/'+n; raw=t.extractfile(name).read() + require(digest(raw)==m['archive_members'][name], 'archive member '+name) + objs[n]=json.loads(gzip.decompress(raw) if n.endswith('.gz') else raw) + w=objs[MEMBERS[0]]; programs=objs[MEMBERS[1]]; receipt=objs[MEMBERS[2]] + require(set(m['archive_members'])=={'slots/local/'+n for n in MEMBERS},'archive member inventory') + with tarfile.open(ROOT/'research/community-frontier1094-audit/selected-replay.tar.gz') as t: + for n in MEMBERS: + raw=t.extractfile('candidate/strict/global8/base/providers/gauge44/'+n).read() + require(digest(raw)==m['archive_members']['slots/local/'+n],'selected1094 provider alias '+n) + require((w['v'],w['h'],w['R'])==(112,9,480),'source dimensions') + require(receipt['canonical_word_sha256']==m['archive_members']['slots/local/'+MEMBERS[0]] and receipt['local_programs_sha256']==m['archive_members']['slots/local/'+MEMBERS[1]],'native receipt artifact binding') + require(set(programs)=={'forward','backward'},'orientations') + return w,programs,receipt,objs[MEMBERS[3]] + +def power(k): return Q(2**k) if k>=0 else Q(1,2**-k) + +def parts(q): + a=abs(q.numerator);d=q.denominator + require(a and d&(d-1)==0,'nonzero dyadic') + v=(a&-a).bit_length()-1 + return a>>v, v-(d.bit_length()-1) + +def price(q, mode='copy-init'): + p,e=parts(q) + return 3+(p.bit_length()-1)+p.bit_count()+abs(e) if mode=='horner' else 2+(p.bit_length()-1)+p.bit_count()+abs(e)-int(p==1 and e==0) + +def cost(g,mode='copy-init'): + if g[0]=='add':return price(Q(g[3],g[4]),mode) + if g[0] in ('copy','clear'):return 1 + require(g[0]=='scale','scalar opcode') + q=Q(g[2],g[3]);p,e=parts(q);require(p==1,'power of two scale') + return abs(e)+int(q<0) + +def domain(w,programs): + excluded=set(w['centers']) & set(range(224,704)) + for events in programs.values(): + for ev in events: + if ev[0]=='scalar' and ev[1][0] in ('copy','clear'): + for r in ev[1][1:]: + if isinstance(r,list) and r[0]=='L' and 224<=r[1]<704:excluded.add(r[1]) + return sorted(set(range(224,704))-excluded),sorted(excluded) + +def search(events,helpers,mode='copy-init'): + terms=defaultdict(list) + for ev in events: + if ev[0]=='scalar' and ev[1][0]=='add': + g=ev[1];p,e=parts(Q(g[3],g[4])) + for r,s in ((g[1],1),(g[2],-1)): + if r[0]=='L':terms[r[1]].append((p,e,s)) + rows=[] + for h in helpers: + ts=terms[h]; points=sorted({0}|{-s*e for p,e,s in ts}) + def delta(k): + return 2*abs(k)+sum(abs(e+s*k)-abs(e) - (int(p==1 and e+s*k==0)-int(p==1 and e==0) if mode=='copy-init' else 0) for p,e,s in ts) + values=[[k,delta(k)] for k in points] + best=min(values,key=lambda kv:(kv[1],abs(kv[0]),kv[0])) + rows.append(dict(helper=h,incident_adds=len(ts),candidates=values,best_k=best[0],delta=best[1],tail_slope=2+len(ts))) + return rows + +def transform(events,w,h,k): + require(224<=h<704 and h not in w['centers'],'non-center helper only') + result=copy.deepcopy(events) + for ev in result: + if ev[0]!='scalar':continue + g=ev[1] + if g[0]=='add': + shift=k*(int(g[1]==['L',h])-int(g[2]==['L',h])) + q=Q(g[3],g[4])*power(shift);g[3:5]=[q.numerator,q.denominator] + elif g[0] in ('copy','clear'): + require(['L',h] not in g[1:],'copy/clear carrier excluded') + q=power(k); entry=['scalar',['scale',['L',h],q.numerator,q.denominator],w['start'][h]] + q=1/q; leave=['scalar',['scale',['L',h],q.numerator,q.denominator],w['final'][h]] + # The materialized winner is cold/FULL and has no residual wrapper. The + # exit scale follows full-frame cleanup, in the retained FULL coordinate. + require(w['start'][h]==0 and w['final'][h]==1,'materialized cold/FULL helper') + require(not any(e[0]=='residual_adapter' and e[2]==h for e in result),'unwrapped helper') + require(result[0]==['phase','zero_frame_precondition'] and result[-1]==['phase','done'],'boundary phases') + result.insert(len(result)-1,leave);result.insert(1,entry) + require([e for e in result if e[0]!='scalar']==[e for e in events if e[0]!='scalar'],'nonscalar stream preserved') + return result + +def replay(events,orientation): + # Independent formal variables for all 704 data/helper and 8 centre registers. + rows={('L',i):{i:Q(1)} for i in range(704)} + rows.update({('C',i):{704+i:Q(1)} for i in range(8)}) + for ev in events: + if ev[0]!='scalar':continue + g=ev[1];t=tuple(g[1]);tag=g[0] + if tag=='clear':rows[t]={} + elif tag=='copy':rows[t]=dict(rows[tuple(g[2])]) + elif tag=='scale':rows[t]={i:a*Q(g[2],g[3]) for i,a in rows[t].items()} + elif tag=='add': + s=tuple(g[2]);q=Q(g[3],g[4]);require(t!=s,'distinct add operands') + for i,a in rows[s].items(): + v=rows[t].get(i,Q(0))+q*a + if v:rows[t][i]=v + else:rows[t].pop(i,None) + else:raise ValueError('scalar opcode') + for i in range(704): + expected={i:Q(1)} + if orientation=='forward' and 112<=i<224:expected[i-112]=Q(1) + if orientation=='backward' and i<112:expected[i+112]=Q(-1) + require(rows['L',i]==expected,'all-column endpoint '+str((orientation,i))) + require(all(not rows['C',i] for i in range(8)),'private centre erased') + return dict(formal_input_columns=712,data_helper_columns=704,dirty_helper_columns=480,centre_columns=8,all_restored=True) + +def invoice(events,mode): + env={('L',i):Q(1) for i in range(704)} + env.update({('C',i):Q(1) for i in range(8)}) + peak=Q(1);count=0;paid=Counter() + for ev in events: + if ev[0]=='climb':paid[ev[5]]+=1 + elif ev[0]=='center':paid[ev[4]]+=1 + if ev[0]!='scalar':continue + g=ev[1];tag=g[0];t=tuple(g[1]);count+=cost(g,mode) + if tag=='clear':env[t]=Q(0) + elif tag=='copy':env[t]=env[tuple(g[2])] + elif tag=='scale': + q=Q(g[2],g[3]);env[t]*=abs(q) + else: + s=tuple(g[2]);q=Q(g[3],g[4]);a=abs(q.numerator) + # Integer Horner work grows to |numerator| times source before halving. + # Copy-init has the same bound; unit direct-add does not touch W until clear. + if mode=='horner' or abs(q)!=1:peak=max(peak,a*env[s]) + env[t]+=abs(q)*env[s] + peak=max(peak,env[t]) + bits=peak.numerator.bit_length()-peak.denominator.bit_length()+1 + require(peak<2**192,'local 192-bit payload cap') + return dict(real_primitives=count,complex_primitives=2*count,prefix_l1=str(peak),prefix_bits=bits,charged_payload_bits=192,paid_profile=dict(sorted(paid.items()))) + +def compute(): + w,programs,receipt,checks=load();helpers,excluded=domain(w,programs) + result=dict(base=BASE,geometry=dict(v=112,h=9,R=480),helpers=helpers,excluded_center_or_copy_helpers=excluded,orientations={}) + candidates={} + for orientation in ('forward','backward'): + events=programs[orientation];rows=search(events,helpers) + winner=min(rows,key=lambda row:(row['delta'],row['helper'],abs(row['best_k']),row['best_k'])) + h,k=winner['helper'],winner['best_k'];candidate=transform(events,w,h,k);candidates[orientation]=candidate + entry={ 'optima':rows,'winner':winner,'candidate_sha256':digest(canonical(candidate)), + 'boundary_frames':[w['start'][h],w['final'][h]],'baseline_endpoint':replay(events,orientation),'candidate_endpoint':replay(candidate,orientation),'prices':{}} + for mode in ('horner','copy-init'): + before=invoice(events,mode);after=invoice(candidate,mode) + require(before['paid_profile']==after['paid_profile'],'paid children unchanged') + if mode=='horner': + require(before['prefix_l1']==receipt['local'][orientation]['prefix_l1_upper'],'source prefix invoice') + require(before['complex_primitives']==checks[orientation]['real_component_primitive_bound'],'source primitive invoice') + else:require(after['real_primitives']-before['real_primitives']==winner['delta'],'search vs whole stream cost') + entry['prices'][mode]=dict(before=before,after=after,saving_real=before['real_primitives']-after['real_primitives'],saving_complex=before['complex_primitives']-after['complex_primitives']) + result['orientations'][orientation]=entry + result['status']='PASS_EXACT_UNBOUNDED_SINGLE_NONCENTER_HELPER_DYADIC_GAUGE' + return result,candidates diff --git a/research/k8-pair-dyadic-seed25/verify.py b/research/k8-pair-dyadic-seed25/verify.py new file mode 100644 index 0000000000..fccfbf7217 --- /dev/null +++ b/research/k8-pair-dyadic-seed25/verify.py @@ -0,0 +1,255 @@ +"""Exact two-helper dyadic gauges. Hanson Sun / OpenAI Codex, Apache-2.0. + +PR1161's source loader, exact scalar replay, lowering price and single-coordinate +transform are retained byte-for-byte. The new search includes the pair interaction. +""" +import argparse +from collections import Counter, defaultdict +import gzip +import hashlib +import importlib.util +import json +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +EXPONENTS = (-2, -1, 1, 2) # Radius 1 + assignment seed 25 % 3. +VENDOR_FILES = frozenset(('engine.py', 'SOURCES.json', 'BASE-SELECTED.json', + 'PROVENANCE.md', 'PROOF.md')) + + +def need(value, message): + if not value: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':'), allow_nan=False).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def predecessor(manifest=None): + pins = manifest or json.loads((HERE / 'SOURCES.json').read_bytes()) + need(pins['base'] == '1b59b624d21924f8e3537cdc1ac52d3be6eda2fe', 'base pin') + need(pins['pr1161_head'] == 'd210969d3158a1e6c505e41f67dd84e555c88564', 'PR1161 pin') + need(set(pins['vendor']) == VENDOR_FILES, 'vendor inventory') + folder = HERE / 'vendor/pr1161' + for name, digest in pins['vendor'].items(): + need(sha((folder / name).read_bytes()) == digest, 'vendor hash: ' + name) + spec = importlib.util.spec_from_file_location('credited_pr1161', folder / 'engine.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + module.ROOT = ROOT # Relocation only; the original module bytes are unchanged. + return module + + +def eligible(lib, word, programs): + helpers, _ = lib.domain(word, programs) + wrapped = {e[2] for stream in programs.values() for e in stream + if e[0] == 'residual_adapter'} + return [h for h in helpers if word['start'][h] == 0 and word['final'][h] == 1 + and h not in wrapped] + + +def census(lib, events, helpers): + allowed = set(helpers) + single = {h: {k: 2 * abs(k) for k in EXPONENTS} for h in helpers} + shared = defaultdict(Counter) + + def variable_price(unit, exponent): + return abs(exponent) - int(unit and exponent == 0) + + for event in events: + if event[0] != 'scalar' or event[1][0] != 'add': + continue + gate = event[1] + p, e = lib.parts(lib.Q(gate[3], gate[4])) + unit = p == 1 + target = gate[1][1] if gate[1][0] == 'L' else None + source = gate[2][1] if gate[2][0] == 'L' else None + need(target is None or source is None or target != source, 'distinct ADD operands') + for helper, sign in ((target, 1), (source, -1)): + if helper in allowed: + for k in EXPONENTS: + single[helper][k] += variable_price(unit, e + sign * k) - variable_price(unit, e) + if target in allowed and source in allowed: + pair = tuple(sorted((target, source))) + shared[pair][(unit, e, target == pair[0])] += 1 + + rows = [] + histogram = Counter() + winner = None + for (a, b), edges in sorted(shared.items()): + values = [] + for ka in EXPONENTS: + for kb in EXPONENTS: + correction = 0 + for (unit, e, target_first), count in edges.items(): + kt, ks = (ka, kb) if target_first else (kb, ka) + correction += count * (variable_price(unit, e + kt - ks) + - variable_price(unit, e + kt) + - variable_price(unit, e - ks) + + variable_price(unit, e)) + delta = single[a][ka] + single[b][kb] + correction + values.append(delta) + histogram[delta] += 1 + key = (delta, a, b, abs(ka) + abs(kb), ka, kb) + if winner is None or key < winner: + winner = key + rows.append([a, b, values]) + need(winner is not None, 'nonempty interacting-pair domain') + d, a, b, _, ka, kb = winner + return {'helpers': helpers, 'exponents': list(EXPONENTS), 'pairs': len(rows), + 'assignments': 16 * len(rows), 'rows': rows, + 'delta_histogram': [[d, n] for d, n in sorted(histogram.items())], + 'winner': {'helpers': [a, b], 'exponents': [ka, kb], 'delta_real': d, + 'separate_single_delta_real': single[a][ka] + single[b][kb], + 'interaction_delta_real': d - single[a][ka] - single[b][kb]}} + + +def exact_census(lib, events, helpers): + """Affine-cell vertices certify all integer exponents; axes allow one helper.""" + allowed = set(helpers) + incident = {h: Counter() for h in helpers} + shared = defaultdict(Counter) + for event in events: + if event[0] != 'scalar' or event[1][0] != 'add': + continue + g = event[1] + p, e = lib.parts(lib.Q(g[3], g[4])) + t = g[1][1] if g[1][0] == 'L' else None + s = g[2][1] if g[2][0] == 'L' else None + for h, sign in ((t, 1), (s, -1)): + if h in allowed: + incident[h][p == 1, e, sign] += 1 + if t in allowed and s in allowed: + a, b = sorted((t, s)) + shared[a, b][p == 1, e, t == a] += 1 + + def f(unit, exponent): + return abs(exponent) - int(unit and exponent == 0) + + cache = {} + + def single(h, k): + if (h, k) not in cache: + cache[h, k] = 2 * abs(k) + sum(n * (f(u, e + sign * k) - f(u, e)) + for (u, e, sign), n in incident[h].items()) + return cache[h, k] + + rows = [] + counts = Counter() + best = None + for a, b in combinations(helpers, 2): + edges = shared.get((a, b), {}) + # Removing shared edges leaves vertical/horizontal slope-change lines. + ta, tb = incident[a].copy(), incident[b].copy() + diagonals = set() + for (u, e, target_first), n in edges.items(): + sa = 1 if target_first else -1 + ta[u, e, sa] -= n + tb[u, e, -sa] -= n + diagonals.add(-sa * e) + vertical = {0} | {-s * e for (u, e, s), n in ta.items() if n} + horizontal = {0} | {-s * e for (u, e, s), n in tb.items() if n} + vertices = {(k, ell) for k in vertical for ell in horizontal} + vertices.update((k, k - d) for k in vertical for d in diagonals) + vertices.update((ell + d, ell) for ell in horizontal for d in diagonals) + pair_best = None + evaluated = [] + for ka, kb in sorted(vertices): + correction = 0 + for (u, e, target_first), n in edges.items(): + kt, ks = (ka, kb) if target_first else (kb, ka) + correction += n * (f(u, e + kt - ks) - f(u, e + kt) - f(u, e - ks) + f(u, e)) + delta = single(a, ka) + single(b, kb) + correction + key = (delta, abs(ka) + abs(kb), ka, kb) + evaluated.append([ka, kb, delta]) + if pair_best is None or key < pair_best: + pair_best = key + delta, _, ka, kb = pair_best + rows.append([a, b, len(vertices), delta, ka, kb, sha(canonical(evaluated))]) + counts['pairs'] += 1 + counts['interacting_pairs' if edges else 'separable_pairs'] += 1 + counts['vertices'] += len(vertices) + key = (delta, a, b, abs(ka) + abs(kb), ka, kb) + if best is None or key < best: + best = key + d, a, b, _, ka, kb = best + return {'helpers': helpers, 'domain': 'all integer exponent pairs, including zero', + **counts, 'rows': rows, + 'winner': {'helpers': [a, b], 'exponents': [ka, kb], 'delta_real': d, + 'separate_single_delta_real': single(a, ka) + single(b, kb), + 'interaction_delta_real': d - single(a, ka) - single(b, kb)}} + + +def construct(lib, word, events, winner): + result = events + for helper, exponent in zip(winner['helpers'], winner['exponents']): + result = lib.transform(result, word, helper, exponent) + return result + + +def compute(): + lib = predecessor() + word, programs, _, _ = lib.load() + helpers = eligible(lib, word, programs) + certificate = {'base': '1b59b624d21924f8e3537cdc1ac52d3be6eda2fe', + 'seed': 25, 'scope': 'all integer gauges on at most two cold/FULL unwrapped helpers', + 'orientations': {}} + witnesses = {} + for orientation, events in programs.items(): + pilot = census(lib, events, helpers) + result = exact_census(lib, events, helpers) + result['bounded_pilot'] = {k: v for k, v in pilot.items() if k != 'rows'} + candidate = construct(lib, word, events, result['winner']) + result['candidate_sha256'] = sha(canonical(candidate)) + result['baseline_endpoint'] = lib.replay(events, orientation) + result['candidate_endpoint'] = lib.replay(candidate, orientation) + result['prices'] = {} + for mode in ('copy-init', 'horner'): + before = lib.invoice(events, mode) + after = lib.invoice(candidate, mode) + need(before['paid_profile'] == after['paid_profile'], 'unchanged recursive profile') + if mode == 'copy-init': + need(after['real_primitives'] - before['real_primitives'] == result['winner']['delta_real'], + 'search versus complete invoice') + result['prices'][mode] = {'before': before, 'after': after, + 'saving_complex': before['complex_primitives'] - after['complex_primitives']} + certificate['orientations'][orientation] = result + witnesses[orientation] = candidate + certificate['status'] = 'PASS_K8_PAIR_DYADIC_CENSUS' + return certificate, witnesses + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result, programs = compute() + pair_rows = {o: row.pop('rows') for o, row in result['orientations'].items()} + for orientation, rows in pair_rows.items(): + result['orientations'][orientation]['pair_rows_sha256'] = sha(canonical(rows)) + if args.write: + (HERE / 'CERTIFICATE.json').write_bytes(canonical(result) + b'\n') + (HERE / 'PAIR-CENSUS.json.gz').write_bytes(gzip.compress(canonical(pair_rows), mtime=0)) + (HERE / 'PROGRAMS.json.gz').write_bytes(gzip.compress(canonical(programs), mtime=0)) + else: + need(canonical(result) == canonical(json.loads((HERE / 'CERTIFICATE.json').read_bytes())), + 'complete certificate mismatch') + need(canonical(programs) == canonical(json.loads(gzip.decompress((HERE / 'PROGRAMS.json.gz').read_bytes()))), + 'complete candidate program mismatch') + need(canonical(pair_rows) == canonical(json.loads(gzip.decompress((HERE / 'PAIR-CENSUS.json.gz').read_bytes()))), + 'complete pair census mismatch') + print(result['status']) + for orientation, row in result['orientations'].items(): + print(orientation, 'pairs', row['pairs'], 'vertices', row['vertices'], + 'winner', row['winner'], 'saving_complex', row['prices']['copy-init']['saving_complex']) + + +if __name__ == '__main__': + main()