diff --git a/research/plane-port-global-rank-dual/CERTIFICATE.json b/research/plane-port-global-rank-dual/CERTIFICATE.json new file mode 100644 index 0000000000..5122975358 --- /dev/null +++ b/research/plane-port-global-rank-dual/CERTIFICATE.json @@ -0,0 +1,443 @@ +{"schema":"plane-port-global-rank-dual/certificate/1","scale":1048576,"lower_bound_num":18233853,"lower_bound_den":131072,"columns":[{"clique":[10],"w":3174}, +{"clique":[20],"w":44682}, +{"clique":[0,12],"w":154428}, +{"clique":[2,7],"w":22963}, +{"clique":[2,10],"w":2627}, +{"clique":[2,47],"w":18686}, +{"clique":[3,8],"w":69072}, +{"clique":[3,26],"w":9635}, +{"clique":[3,39],"w":41498}, +{"clique":[4,20],"w":17812}, +{"clique":[4,21],"w":69939}, +{"clique":[4,22],"w":231}, +{"clique":[4,36],"w":41815}, +{"clique":[6,24],"w":14059}, +{"clique":[6,28],"w":5388}, +{"clique":[7,46],"w":47339}, +{"clique":[8,28],"w":47091}, +{"clique":[8,34],"w":2309}, +{"clique":[9,40],"w":88462}, +{"clique":[10,27],"w":152867}, +{"clique":[13,14],"w":35607}, +{"clique":[16,18],"w":1476}, +{"clique":[16,45],"w":23103}, +{"clique":[18,21],"w":134}, +{"clique":[20,38],"w":4101}, +{"clique":[21,45],"w":75460}, +{"clique":[23,45],"w":48858}, +{"clique":[26,31],"w":143289}, +{"clique":[27,40],"w":18454}, +{"clique":[28,29],"w":32077}, +{"clique":[34,39],"w":5497}, +{"clique":[2,6,21],"w":5561}, +{"clique":[4,11,43],"w":122501}, +{"clique":[4,36,47],"w":21472}, +{"clique":[5,30,49],"w":59933}, +{"clique":[7,20,46],"w":28642}, +{"clique":[0,6,24,46],"w":27186}, +{"clique":[0,10,19,46],"w":6614}, +{"clique":[1,10,17,42],"w":8298}, +{"clique":[1,16,29,42],"w":107643}, +{"clique":[2,10,17,27],"w":3794}, +{"clique":[3,21,26,39],"w":29197}, +{"clique":[4,5,24,38],"w":23430}, +{"clique":[4,14,22,25],"w":10434}, +{"clique":[6,18,20,31],"w":109603}, +{"clique":[7,12,29,52],"w":52974}, +{"clique":[9,12,29,49],"w":19539}, +{"clique":[22,25,26,46],"w":7607}, +{"clique":[0,4,13,14,38],"w":20285}, +{"clique":[0,6,8,19,28],"w":4528}, +{"clique":[0,7,12,22,25],"w":31229}, +{"clique":[1,9,10,38,53],"w":3839}, +{"clique":[1,9,40,42,48],"w":44666}, +{"clique":[1,10,23,42,45],"w":58843}, +{"clique":[2,5,12,29,49],"w":267}, +{"clique":[2,7,21,46,52],"w":10609}, +{"clique":[2,10,11,19,47],"w":18942}, +{"clique":[2,10,19,25,43],"w":8640}, +{"clique":[2,25,35,40,47],"w":721}, +{"clique":[3,11,37,39,43],"w":7071}, +{"clique":[4,5,30,36,47],"w":10896}, +{"clique":[4,11,14,22,25],"w":13756}, +{"clique":[4,23,25,26,31],"w":4149}, +{"clique":[5,30,38,48,50],"w":7800}, +{"clique":[6,8,18,21,28],"w":43100}, +{"clique":[9,23,27,40,47],"w":15122}, +{"clique":[10,11,19,23,47],"w":1312}, +{"clique":[10,11,19,35,47],"w":37821}, +{"clique":[10,17,29,32,49],"w":42291}, +{"clique":[12,28,29,35,49],"w":1913}, +{"clique":[0,6,20,24,38,46],"w":23162}, +{"clique":[0,8,12,29,49,52],"w":11676}, +{"clique":[0,12,17,22,29,42],"w":5723}, +{"clique":[1,3,6,14,31,53],"w":49012}, +{"clique":[1,3,16,20,29,42],"w":7168}, +{"clique":[1,10,17,23,42,45],"w":32900}, +{"clique":[1,10,18,45,51,53],"w":21430}, +{"clique":[1,10,42,46,51,53],"w":3752}, +{"clique":[2,3,7,26,39,46],"w":19418}, +{"clique":[2,5,7,12,15,47],"w":42720}, +{"clique":[2,10,19,25,35,47],"w":24801}, +{"clique":[2,16,42,47,48,50],"w":18085}, +{"clique":[3,8,22,26,34,39],"w":25360}, +{"clique":[4,5,15,22,24,25],"w":49553}, +{"clique":[4,13,14,20,32,38],"w":16481}, +{"clique":[4,20,24,35,36,38],"w":2657}, +{"clique":[4,22,24,34,38,39],"w":8438}, +{"clique":[6,15,20,30,31,50],"w":3372}, +{"clique":[6,20,28,35,38,50],"w":76007}, +{"clique":[6,24,33,34,44,55],"w":24473}, +{"clique":[7,12,20,29,38,52],"w":5378}, +{"clique":[7,13,14,18,45,53],"w":276}, +{"clique":[7,16,26,40,41,46],"w":21226}, +{"clique":[7,20,28,29,35,52],"w":24879}, +{"clique":[8,10,17,27,34,39],"w":29111}, +{"clique":[8,28,40,47,48,54],"w":14069}, +{"clique":[9,10,15,18,21,32],"w":15324}, +{"clique":[10,17,18,27,38,53],"w":7802}, +{"clique":[13,14,32,40,45,47],"w":18503}, +{"clique":[0,6,20,28,48,50,54],"w":42876}, +{"clique":[0,7,13,14,26,27,46],"w":12830}, +{"clique":[0,8,28,42,48,50,54],"w":30144}, +{"clique":[2,3,16,33,44,47,55],"w":1449}, +{"clique":[2,4,21,35,36,39,45],"w":6181}, +{"clique":[2,7,9,12,15,22,24],"w":41655}, +{"clique":[2,7,12,22,34,39,52],"w":31049}, +{"clique":[2,8,12,15,30,49,50],"w":219}, +{"clique":[2,18,21,35,36,39,45],"w":1084}, +{"clique":[3,4,11,14,20,32,43],"w":23246}, +{"clique":[3,4,14,29,49,53,54],"w":34533}, +{"clique":[3,14,17,29,32,42,49],"w":11}, +{"clique":[3,22,26,34,37,39,44],"w":20077}, +{"clique":[4,5,14,18,30,36,53],"w":20195}, +{"clique":[4,11,15,21,22,24,25],"w":2103}, +{"clique":[4,13,14,36,40,41,45],"w":13145}, +{"clique":[4,17,24,29,38,49,54],"w":29682}, +{"clique":[4,24,25,29,40,49,54],"w":471}, +{"clique":[5,24,40,41,48,49,54],"w":7441}, +{"clique":[5,27,30,40,47,50,54],"w":83249}, +{"clique":[6,14,18,27,31,36,53],"w":3159}, +{"clique":[6,19,31,35,36,40,47],"w":9885}, +{"clique":[6,20,24,31,38,50,54],"w":30599}, +{"clique":[7,9,22,34,37,39,52],"w":24751}, +{"clique":[7,15,16,18,20,21,32],"w":12128}, +{"clique":[7,16,20,31,42,48,50],"w":3265}, +{"clique":[7,18,21,34,36,37,39],"w":32012}, +{"clique":[11,13,14,15,19,20,32],"w":11352}, +{"clique":[0,6,10,23,27,33,38,46],"w":7268}, +{"clique":[0,7,9,12,15,19,22,30],"w":1617}, +{"clique":[0,7,16,19,40,45,46,47],"w":17310}, +{"clique":[0,10,25,32,33,35,45,49],"w":44034}, +{"clique":[0,12,17,29,33,49,54,55],"w":6273}, +{"clique":[0,13,16,19,40,45,46,47],"w":13531}, +{"clique":[0,14,18,22,26,41,46,53],"w":16824}, +{"clique":[1,3,9,16,26,28,42,50],"w":27583}, +{"clique":[1,3,9,16,26,31,40,42],"w":381}, +{"clique":[1,5,7,14,15,30,46,53],"w":2154}, +{"clique":[1,5,10,11,15,19,43,46],"w":7651}, +{"clique":[1,9,10,22,38,42,46,51],"w":10613}, +{"clique":[1,9,12,29,33,34,44,55],"w":772}, +{"clique":[1,9,19,23,40,42,45,47],"w":9352}, +{"clique":[2,3,7,16,26,39,46,52],"w":7511}, +{"clique":[2,4,11,14,18,43,53,54],"w":10775}, +{"clique":[2,5,12,30,33,35,47,55],"w":19289}, +{"clique":[2,7,21,26,34,39,46,52],"w":19293}, +{"clique":[2,10,11,19,25,26,31,43],"w":6411}, +{"clique":[2,10,33,35,40,41,45,47],"w":12343}, +{"clique":[2,11,24,25,43,48,49,54],"w":3590}, +{"clique":[3,4,8,11,16,36,37,39],"w":3830}, +{"clique":[3,4,24,29,39,49,53,54],"w":11744}, +{"clique":[3,8,16,24,26,39,48,50],"w":2924}, +{"clique":[3,8,21,30,36,39,45,53],"w":5151}, +{"clique":[3,26,31,33,35,40,41,47],"w":7842}, +{"clique":[5,12,14,17,29,30,49,53],"w":8198}, +{"clique":[5,14,28,32,38,49,50,54],"w":22083}, +{"clique":[5,21,30,35,36,39,48,50],"w":10860}, +{"clique":[7,13,14,21,26,31,32,45],"w":7208}, +{"clique":[9,13,16,33,40,44,45,55],"w":11034}, +{"clique":[11,16,18,19,21,24,32,49],"w":18217}, +{"clique":[0,3,12,29,33,35,41,51,55],"w":14966}, +{"clique":[0,5,7,12,22,29,34,37,52],"w":20905}, +{"clique":[0,6,10,19,23,27,40,46,47],"w":1561}, +{"clique":[0,6,18,19,20,21,31,32,46],"w":4855}, +{"clique":[0,7,19,22,25,28,46,47,51],"w":9096}, +{"clique":[0,12,13,14,16,17,32,42,45],"w":21332}, +{"clique":[0,12,22,33,34,35,40,41,47],"w":89}, +{"clique":[1,3,22,24,26,39,40,41,46],"w":16929}, +{"clique":[1,4,5,14,18,35,36,49,53],"w":2293}, +{"clique":[1,5,7,15,16,20,25,48,50],"w":972}, +{"clique":[1,8,20,23,33,34,44,45,55],"w":1081}, +{"clique":[1,9,10,17,23,29,33,51,55],"w":37329}, +{"clique":[1,9,12,15,17,30,42,49,50],"w":214}, +{"clique":[1,10,17,20,38,41,46,51,55],"w":3236}, +{"clique":[2,3,6,11,15,19,30,31,43],"w":226}, +{"clique":[2,3,9,12,16,26,29,43,52],"w":19661}, +{"clique":[2,3,12,29,39,43,49,52,54],"w":1880}, +{"clique":[2,4,11,13,14,16,25,37,43],"w":32050}, +{"clique":[2,6,12,31,33,34,44,47,55],"w":25134}, +{"clique":[2,8,28,29,35,37,43,45,52],"w":15313}, +{"clique":[2,9,12,28,40,45,47,50,54],"w":10804}, +{"clique":[2,9,12,29,33,43,52,54,55],"w":8025}, +{"clique":[3,4,11,22,34,37,39,41,43],"w":39641}, +{"clique":[3,5,11,22,24,34,37,39,48],"w":3172}, +{"clique":[3,7,16,24,26,32,40,41,46],"w":1147}, +{"clique":[3,8,22,24,26,34,37,39,44],"w":7668}, +{"clique":[4,11,13,14,16,18,32,43,52],"w":15772}, +{"clique":[4,11,22,24,25,34,37,44,51],"w":266}, +{"clique":[4,16,18,22,23,33,40,41,45],"w":15070}, +{"clique":[5,7,15,18,21,24,34,37,48],"w":21169}, +{"clique":[5,10,11,15,22,34,37,41,48],"w":13131}, +{"clique":[5,12,15,29,34,37,44,51,55],"w":1918}, +{"clique":[5,12,24,28,38,41,49,50,54],"w":7844}, +{"clique":[5,14,17,27,29,30,46,49,53],"w":830}, +{"clique":[7,18,21,28,35,36,39,51,52],"w":1548}, +{"clique":[8,10,22,25,26,34,37,39,48],"w":27975}, +{"clique":[9,10,19,27,32,40,47,49,54],"w":4448}, +{"clique":[10,17,22,25,26,27,34,37,39],"w":5195}, +{"clique":[11,13,14,18,19,30,43,51,53],"w":21036}, +{"clique":[0,6,8,10,22,34,37,39,44,51],"w":21715}, +{"clique":[0,8,12,15,22,28,29,34,37,41],"w":1009}, +{"clique":[0,9,10,19,32,35,40,45,46,47],"w":1383}, +{"clique":[0,10,25,32,33,35,44,46,51,55],"w":5790}, +{"clique":[1,3,7,16,22,26,29,39,46,52],"w":1539}, +{"clique":[1,3,7,16,26,33,40,41,42,46],"w":27314}, +{"clique":[1,3,8,11,14,19,26,31,43,53],"w":11753}, +{"clique":[1,4,5,11,15,16,18,21,43,53],"w":2894}, +{"clique":[1,5,7,13,14,30,38,46,51,53],"w":12302}, +{"clique":[1,5,10,13,17,18,38,45,49,53],"w":9023}, +{"clique":[1,6,8,16,23,31,33,44,52,55],"w":32940}, +{"clique":[1,6,9,12,24,31,38,49,53,54],"w":10443}, +{"clique":[1,7,9,12,13,15,17,30,42,50],"w":9624}, +{"clique":[1,9,10,11,13,17,38,42,50,53],"w":4846}, +{"clique":[1,9,12,29,33,40,44,49,54,55],"w":11951}, +{"clique":[1,9,16,18,26,31,40,42,48,50],"w":689}, +{"clique":[2,3,6,9,11,12,19,24,28,43],"w":2212}, +{"clique":[2,3,9,12,24,29,39,49,53,54],"w":9243}, +{"clique":[2,3,12,16,29,33,41,44,51,55],"w":4307}, +{"clique":[2,4,8,11,16,22,25,37,43,52],"w":4484}, +{"clique":[2,5,12,14,15,16,18,29,49,53],"w":23447}, +{"clique":[2,6,10,17,23,27,29,33,51,55],"w":21414}, +{"clique":[2,6,11,14,18,28,43,50,53,54],"w":1669}, +{"clique":[2,6,20,25,31,33,35,36,47,55],"w":17713}, +{"clique":[2,7,16,18,21,28,42,46,51,52],"w":40539}, +{"clique":[2,9,12,15,29,30,35,40,45,47],"w":5313}, +{"clique":[4,5,11,15,18,21,22,34,37,43],"w":12395}, +{"clique":[4,19,21,28,32,36,40,47,49,54],"w":6644}, +{"clique":[5,7,11,14,15,18,30,46,51,53],"w":16801}, +{"clique":[5,7,15,18,20,23,27,30,46,51],"w":10768}, +{"clique":[5,10,11,15,19,21,23,25,32,49],"w":8287}, +{"clique":[5,10,27,32,38,40,47,48,49,54],"w":13695}, +{"clique":[5,14,18,27,30,38,46,49,53,54],"w":6094}, +{"clique":[5,17,21,24,28,38,48,49,50,54],"w":20844}, +{"clique":[6,9,22,24,25,27,34,37,38,40],"w":5569}, +{"clique":[6,10,11,19,20,23,27,31,43,52],"w":1193}, +{"clique":[7,9,13,14,15,21,26,31,32,46],"w":9127}, +{"clique":[7,9,13,14,15,21,26,32,40,45],"w":643}, +{"clique":[8,12,22,24,26,34,37,38,39,41],"w":3460}, +{"clique":[9,10,27,33,40,44,48,49,54,55],"w":10408}, +{"clique":[9,12,27,29,33,37,40,44,54,55],"w":38720}, +{"clique":[10,17,18,20,21,27,32,35,38,49],"w":37171}, +{"clique":[10,21,23,29,32,33,41,45,49,55],"w":11749}, +{"clique":[10,25,27,32,33,40,44,49,54,55],"w":49460}, +{"clique":[0,3,7,22,23,26,34,39,41,46,52],"w":23829}, +{"clique":[0,4,22,24,28,34,38,39,41,46,51],"w":7838}, +{"clique":[0,6,9,10,21,32,33,35,38,46,55],"w":7835}, +{"clique":[0,6,16,23,27,31,33,44,46,51,55],"w":5811}, +{"clique":[0,8,12,13,14,15,28,32,35,45,49],"w":4671}, +{"clique":[0,9,10,19,22,23,32,40,45,46,47],"w":24304}, +{"clique":[0,12,13,14,17,28,32,36,38,45,49],"w":102}, +{"clique":[1,3,5,7,20,26,30,39,46,52,53],"w":5445}, +{"clique":[1,3,7,9,16,26,31,40,42,46,52],"w":6810}, +{"clique":[1,3,9,26,31,33,34,44,46,53,55],"w":17320}, +{"clique":[1,5,7,15,21,22,24,25,34,48,53],"w":2444}, +{"clique":[1,5,13,14,17,29,30,38,46,49,53],"w":5246}, +{"clique":[1,5,14,29,30,38,47,48,49,53,54],"w":2887}, +{"clique":[1,6,10,17,22,29,39,42,46,51,53],"w":1367}, +{"clique":[1,6,10,20,31,33,34,41,44,48,55],"w":11566}, +{"clique":[1,6,10,31,33,34,41,44,49,53,55],"w":22289}, +{"clique":[1,6,16,18,20,21,24,31,42,48,50],"w":1097}, +{"clique":[1,7,9,12,13,15,17,30,45,50,53],"w":3621}, +{"clique":[1,7,9,13,14,17,29,38,42,52,53],"w":6050}, +{"clique":[1,7,9,14,16,29,38,46,51,52,53],"w":22502}, +{"clique":[1,7,16,23,25,26,31,42,45,48,50],"w":18434}, +{"clique":[1,9,10,13,17,38,42,47,50,53,54],"w":23185}, +{"clique":[1,9,16,23,25,40,42,45,47,48,50],"w":30334}, +{"clique":[1,10,11,17,19,23,25,46,51,53,55],"w":1991}, +{"clique":[1,10,13,17,29,33,41,44,51,53,55],"w":8983}, +{"clique":[2,3,12,19,22,24,26,34,39,41,43],"w":2360}, +{"clique":[2,3,26,31,33,35,40,41,44,47,55],"w":16755}, +{"clique":[2,4,11,16,22,23,25,33,37,43,52],"w":20986}, +{"clique":[3,4,11,19,22,34,35,36,37,39,43],"w":21502}, +{"clique":[3,7,9,12,15,22,26,30,37,39,40],"w":37634}, +{"clique":[3,9,15,19,23,26,27,30,31,32,40],"w":7098}, +{"clique":[4,5,13,14,15,17,27,29,30,32,49],"w":7184}, +{"clique":[4,5,14,15,22,25,29,30,46,51,53],"w":9192}, +{"clique":[4,11,14,18,28,36,43,49,50,53,54],"w":268}, +{"clique":[4,11,19,20,24,25,31,38,43,49,54],"w":721}, +{"clique":[6,8,10,11,17,22,23,27,34,37,39],"w":1481}, +{"clique":[6,8,10,11,22,34,35,37,39,43,52],"w":9585}, +{"clique":[6,8,15,20,23,33,34,37,44,45,55],"w":33152}, +{"clique":[6,9,12,27,29,33,40,47,52,54,55],"w":21325}, +{"clique":[6,20,23,24,31,33,34,44,45,51,55],"w":5809}, +{"clique":[6,20,30,31,33,35,44,47,48,50,55],"w":24667}, +{"clique":[7,9,11,15,21,22,24,25,34,37,39],"w":28305}, +{"clique":[7,9,16,18,21,23,27,28,40,46,51],"w":18194}, +{"clique":[7,9,25,26,27,28,35,40,46,47,52],"w":18}, +{"clique":[7,13,14,16,17,18,21,26,32,42,45],"w":28724}, +{"clique":[7,18,21,22,24,26,34,37,38,39,41],"w":3052}, +{"clique":[8,10,17,22,27,29,34,37,39,51,52],"w":4332}, +{"clique":[9,12,13,14,15,17,27,30,31,49,53],"w":5272}, +{"clique":[0,6,8,10,19,22,29,34,37,39,44,51],"w":8112}, +{"clique":[0,6,10,17,23,25,27,29,33,46,51,55],"w":10994}, +{"clique":[0,7,9,13,14,16,19,40,42,45,46,47],"w":3606}, +{"clique":[0,7,9,19,25,26,27,31,35,40,46,47],"w":2490}, +{"clique":[0,7,12,13,14,16,18,19,29,51,52,53],"w":3093}, +{"clique":[0,7,19,21,24,28,32,40,41,46,51,55],"w":10450}, +{"clique":[0,9,10,32,33,34,35,44,46,47,51,55],"w":4544}, +{"clique":[0,10,17,18,21,32,33,35,41,45,46,49],"w":16029}, +{"clique":[0,13,14,17,19,25,28,29,32,42,46,49],"w":2742}, +{"clique":[1,5,12,13,29,30,33,44,49,53,54,55],"w":323}, +{"clique":[1,5,12,14,15,18,28,29,34,41,49,53],"w":900}, +{"clique":[1,6,8,15,20,23,30,31,33,42,48,50],"w":7645}, +{"clique":[1,6,10,18,20,31,34,42,44,50,51,53],"w":6048}, +{"clique":[1,6,14,18,20,30,31,42,48,50,53,54],"w":5861}, +{"clique":[1,8,10,18,22,34,38,39,41,46,51,53],"w":3517}, +{"clique":[1,9,10,13,17,44,45,48,50,51,53,55],"w":3045}, +{"clique":[2,3,5,12,30,36,37,39,43,45,50,54],"w":4728}, +{"clique":[2,3,6,9,12,16,24,33,44,50,51,55],"w":2741}, +{"clique":[2,3,7,9,16,21,26,28,39,42,48,50],"w":9882}, +{"clique":[2,3,7,26,31,33,35,41,46,47,52,55],"w":3116}, +{"clique":[2,6,8,11,19,28,34,37,44,47,51,55],"w":1747}, +{"clique":[2,7,9,15,21,25,26,30,31,45,48,50],"w":14674}, +{"clique":[2,7,9,16,23,33,38,45,48,51,52,55],"w":2147}, +{"clique":[2,9,12,25,30,33,40,45,47,50,54,55],"w":2682}, +{"clique":[2,10,13,17,33,35,44,45,47,51,53,55],"w":552}, +{"clique":[2,10,17,23,25,27,29,33,37,44,51,55],"w":20343}, +{"clique":[2,11,14,18,19,23,26,27,31,43,46,53],"w":1956}, +{"clique":[3,5,7,15,21,22,26,32,34,39,41,48],"w":23500}, +{"clique":[3,6,9,11,12,15,30,31,33,43,51,55],"w":17683}, +{"clique":[3,6,9,21,24,28,29,32,39,40,49,54],"w":10516}, +{"clique":[3,7,9,21,26,29,30,32,39,40,46,52],"w":7453}, +{"clique":[4,5,11,16,18,24,33,37,38,41,43,49],"w":22610}, +{"clique":[4,11,19,20,24,25,28,37,38,43,49,54],"w":41527}, +{"clique":[6,8,10,17,22,23,27,34,37,38,39,42],"w":7977}, +{"clique":[6,10,20,31,32,33,35,40,41,44,47,55],"w":225}, +{"clique":[6,11,16,18,20,21,23,24,32,33,43,45],"w":7194}, +{"clique":[6,16,18,20,21,23,24,31,32,38,45,49],"w":2668}, +{"clique":[7,13,14,16,26,32,40,41,42,45,46,47],"w":13683}, +{"clique":[8,10,11,19,22,25,34,36,37,39,44,51],"w":16336}, +{"clique":[9,10,17,22,23,25,27,34,36,37,38,39],"w":30282}, +{"clique":[10,13,17,25,33,35,44,45,46,49,53,55],"w":12394}, +{"clique":[0,3,5,12,15,24,29,34,37,41,44,49,55],"w":13848}, +{"clique":[0,3,7,9,12,15,22,26,27,29,30,37,40],"w":14975}, +{"clique":[0,3,8,12,17,22,26,27,29,34,37,39,42],"w":4678}, +{"clique":[0,5,7,13,14,29,38,45,47,48,52,53,54],"w":10108}, +{"clique":[0,7,12,22,24,26,29,34,37,38,39,41,52],"w":36840}, +{"clique":[0,9,12,13,14,19,30,32,40,44,45,47,54],"w":4544}, +{"clique":[1,3,6,9,16,17,24,33,44,48,50,53,55],"w":4557}, +{"clique":[1,4,5,11,14,18,28,35,36,38,43,51,53],"w":1170}, +{"clique":[1,4,8,11,14,22,25,28,38,43,50,53,54],"w":10271}, +{"clique":[1,5,7,13,17,19,30,38,41,46,51,53,55],"w":20150}, +{"clique":[1,5,7,14,18,22,30,36,38,48,50,53,54],"w":938}, +{"clique":[1,7,9,15,16,23,28,40,42,45,47,48,50],"w":9562}, +{"clique":[1,7,9,16,18,21,26,28,29,40,42,46,52],"w":8438}, +{"clique":[1,9,10,13,17,38,39,42,45,48,50,51,53],"w":1320}, +{"clique":[1,9,13,16,17,29,33,44,45,49,52,53,55],"w":35008}, +{"clique":[1,10,13,17,29,33,41,44,48,49,53,54,55],"w":26676}, +{"clique":[2,3,6,8,12,24,29,39,43,49,52,53,54],"w":68353}, +{"clique":[2,3,6,9,12,24,31,33,44,49,50,54,55],"w":48763}, +{"clique":[2,6,12,15,20,25,30,31,33,35,44,47,55],"w":14723}, +{"clique":[2,8,16,17,23,25,29,33,44,45,49,52,55],"w":5075}, +{"clique":[2,9,12,13,14,15,19,25,29,30,37,43,51],"w":759}, +{"clique":[3,6,9,15,23,27,30,31,33,40,44,51,55],"w":9384}, +{"clique":[3,7,9,16,26,27,28,37,39,40,42,48,50],"w":16666}, +{"clique":[4,5,11,15,16,21,23,24,25,33,37,43,55],"w":1763}, +{"clique":[4,8,11,19,28,34,35,36,37,41,44,47,55],"w":3202}, +{"clique":[5,10,11,15,18,21,22,34,36,37,39,41,48],"w":9505}, +{"clique":[5,10,15,17,18,20,21,26,27,31,32,34,48],"w":30492}, +{"clique":[5,13,14,25,27,30,32,38,40,47,48,49,54],"w":46574}, +{"clique":[6,8,20,25,31,32,33,34,35,44,47,48,55],"w":5504}, +{"clique":[6,9,27,30,31,33,36,40,47,48,50,54,55],"w":2654}, +{"clique":[7,11,13,14,16,18,19,21,42,45,46,51,53],"w":4753}, +{"clique":[9,18,21,24,27,28,37,38,40,42,48,49,54],"w":14794}, +{"clique":[0,4,13,14,18,19,20,28,32,35,36,43,46,51],"w":92}, +{"clique":[0,5,15,16,20,23,33,37,40,44,45,47,48,55],"w":12469}, +{"clique":[0,6,8,10,19,20,25,31,32,34,44,46,51,55],"w":11448}, +{"clique":[0,6,8,12,22,24,28,29,37,38,39,41,52,54],"w":4209}, +{"clique":[0,6,9,12,17,24,27,29,33,38,49,53,54,55],"w":14874}, +{"clique":[0,7,9,18,21,23,26,27,30,31,32,40,46,52],"w":13968}, +{"clique":[0,8,10,22,23,25,29,34,37,39,44,48,51,52],"w":4856}, +{"clique":[0,8,12,30,33,37,40,41,44,45,47,50,54,55],"w":3723}, +{"clique":[1,3,7,9,11,14,15,19,21,23,26,30,31,53],"w":32655}, +{"clique":[1,3,7,9,12,14,17,22,26,29,30,42,52,53],"w":11108}, +{"clique":[1,5,7,13,18,30,36,38,39,45,48,50,53,54],"w":22565}, +{"clique":[1,5,11,13,14,18,30,38,41,48,49,50,53,54],"w":61657}, +{"clique":[1,6,9,24,25,31,33,44,48,49,50,53,54,55],"w":1941}, +{"clique":[1,6,10,17,18,20,31,38,42,48,49,50,53,54],"w":1452}, +{"clique":[1,7,9,16,17,21,23,28,29,38,42,46,51,52],"w":7017}, +{"clique":[1,8,10,17,22,29,34,39,42,44,46,51,52,53],"w":3605}, +{"clique":[1,13,14,16,18,28,36,42,44,45,48,50,51,53],"w":93094}, +{"clique":[2,3,4,16,23,26,33,40,41,44,45,47,50,55],"w":25171}, +{"clique":[2,3,7,16,23,26,33,40,41,45,46,47,52,55],"w":7057}, +{"clique":[2,6,9,11,21,24,25,33,35,37,43,51,52,55],"w":1514}, +{"clique":[4,8,13,30,33,36,40,41,44,45,47,50,54,55],"w":12493}, +{"clique":[6,8,11,22,24,25,34,37,39,42,44,48,50,51],"w":7297}, +{"clique":[6,8,21,24,28,32,38,40,41,48,49,50,54,55],"w":11270}, +{"clique":[7,9,13,14,18,26,28,29,35,38,45,46,52,53],"w":1839}, +{"clique":[9,10,22,23,25,26,27,34,37,38,40,42,48,50],"w":8828}, +{"clique":[0,5,7,14,17,18,19,23,26,27,30,31,38,46,53],"w":13939}, +{"clique":[0,6,10,17,20,27,31,32,33,38,48,49,50,54,55],"w":20504}, +{"clique":[1,3,4,5,11,14,20,26,28,35,36,43,46,52,53],"w":4078}, +{"clique":[1,3,6,9,11,14,19,30,31,42,44,46,47,51,53],"w":490}, +{"clique":[1,3,6,9,16,23,24,31,33,44,45,49,52,53,55],"w":9349}, +{"clique":[1,4,5,11,16,20,23,24,25,33,38,43,46,51,55],"w":5549}, +{"clique":[1,5,13,17,29,30,41,44,45,47,48,49,53,54,55],"w":49946}, +{"clique":[1,7,9,12,13,17,29,30,33,35,45,47,52,53,55],"w":16201}, +{"clique":[1,9,10,15,17,18,22,34,39,42,44,48,50,51,53],"w":19853}, +{"clique":[2,3,5,12,17,29,30,33,35,41,44,47,49,53,55],"w":1323}, +{"clique":[2,4,5,11,14,18,20,21,28,38,43,46,49,53,54],"w":3385}, +{"clique":[2,4,5,11,19,20,23,24,25,28,37,38,43,51,55],"w":58531}, +{"clique":[2,4,8,11,15,16,18,20,21,23,36,37,39,43,45],"w":5940}, +{"clique":[2,5,7,13,14,19,25,26,30,31,38,45,46,47,53],"w":25159}, +{"clique":[2,6,8,16,20,23,27,31,33,40,44,47,48,50,55],"w":14923}, +{"clique":[2,8,10,17,20,23,29,33,34,37,44,45,51,52,55],"w":2039}, +{"clique":[4,5,13,14,20,30,32,38,40,41,46,47,49,50,54],"w":12974}, +{"clique":[0,3,4,5,14,19,21,30,32,36,40,41,46,47,49,54],"w":1162}, +{"clique":[0,5,7,13,14,18,20,30,31,35,36,38,46,51,52,53],"w":687}, +{"clique":[0,7,13,14,19,20,21,25,28,29,32,35,45,46,47,52],"w":21808}, +{"clique":[0,9,10,19,21,22,25,26,27,32,34,35,38,40,46,47],"w":33372}, +{"clique":[1,7,9,15,16,17,21,22,23,25,28,36,42,45,48,50],"w":2475}, +{"clique":[2,3,5,12,29,30,33,35,37,40,41,44,45,47,51,55],"w":14149}, +{"clique":[2,8,12,13,20,30,33,37,40,41,44,45,47,50,54,55],"w":33926}, +{"clique":[0,3,6,8,20,21,24,28,32,36,39,40,41,48,49,50,54],"w":10679}, +{"clique":[0,3,8,12,17,22,28,29,34,35,37,39,41,42,44,51,52],"w":103971}, +{"clique":[1,3,6,8,14,17,30,31,36,41,42,47,48,49,50,53,54],"w":22402}, +{"clique":[2,8,10,11,22,23,25,26,27,34,37,38,39,42,43,48,50],"w":5365}, +{"clique":[4,5,11,13,14,15,18,19,20,21,30,31,32,35,36,43,51],"w":70312}, +{"clique":[6,9,10,21,25,27,31,32,36,38,40,42,47,48,49,50,54],"w":20043}, +{"clique":[6,9,11,22,24,25,28,34,35,36,37,39,42,44,48,50,51],"w":32732}, +{"clique":[0,4,8,13,14,15,18,19,20,21,26,30,31,32,35,36,43,46],"w":72895}, +{"clique":[1,4,5,11,13,14,18,19,20,26,30,31,35,38,41,43,46,53],"w":23220}, +{"clique":[1,4,8,11,14,16,18,21,23,28,36,42,43,45,46,51,52,53],"w":58344}, +{"clique":[2,3,4,8,11,15,19,21,22,26,28,34,35,36,37,39,41,43],"w":50751}, +{"clique":[2,5,10,13,15,17,20,25,26,27,31,33,35,44,47,48,53,55],"w":34690}, +{"clique":[6,9,10,11,17,18,22,23,27,34,36,37,39,42,44,48,50,51],"w":118}, +{"clique":[6,11,16,20,21,23,24,25,27,31,32,33,38,43,48,51,52,55],"w":28838}, +{"clique":[0,3,4,8,14,15,19,20,23,26,30,31,32,36,40,41,45,46,47],"w":55509}, +{"clique":[0,3,8,12,15,19,22,24,26,28,29,34,35,36,37,39,40,41,44],"w":702}, +{"clique":[0,5,7,12,13,14,19,20,25,27,29,30,32,35,36,38,40,47,52],"w":59550}, +{"clique":[0,5,12,13,15,17,20,26,29,30,33,35,36,41,44,45,47,53,55],"w":8036}, +{"clique":[2,6,8,10,11,17,22,23,25,27,34,36,37,38,39,42,43,48,50],"w":39507}, +{"clique":[2,6,8,11,12,19,22,24,25,28,34,35,36,37,38,39,43,51,52],"w":33457}, +{"clique":[4,11,16,17,18,19,20,21,23,24,26,27,31,32,38,42,43,46,52],"w":51503}, +{"clique":[4,8,11,19,21,22,23,24,25,27,28,34,36,37,38,39,42,43,51,52],"w":73878}, +{"clique":[0,3,6,8,12,15,17,19,20,24,27,28,29,32,34,35,36,39,42,43,49],"w":18950}, +{"clique":[1,7,9,17,18,21,22,23,24,28,29,34,36,38,39,42,45,46,51,52,53],"w":34379}, +{"clique":[2,6,9,11,17,21,23,24,25,27,28,34,36,37,38,39,42,43,48,49,50],"w":23071}, +{"clique":[0,3,6,8,12,15,19,20,24,28,29,32,34,35,36,39,40,41,42,44,45,49],"w":7847}, +{"clique":[1,4,5,11,13,14,17,18,20,21,30,31,36,38,41,43,45,46,49,50,53,54],"w":19648}, +{"clique":[1,8,10,17,18,19,21,22,23,26,29,34,36,38,39,41,42,43,45,46,52,53],"w":5704}, +{"clique":[0,4,8,17,18,19,21,22,23,24,28,29,32,34,38,39,41,42,43,45,46,51,52],"w":688}, +{"clique":[0,4,8,13,17,18,19,20,21,24,28,29,32,35,36,38,39,41,42,43,45,46,49,52],"w":27736}, +{"clique":[2,4,8,11,17,18,19,21,22,24,28,34,35,36,38,39,41,42,43,45,46,51,52,53],"w":264}]} diff --git a/research/plane-port-global-rank-dual/EVIDENCE.md b/research/plane-port-global-rank-dual/EVIDENCE.md new file mode 100644 index 0000000000..b02256f52d --- /dev/null +++ b/research/plane-port-global-rank-dual/EVIDENCE.md @@ -0,0 +1,50 @@ +# Search evidence for the 224 conjecture + +**Heuristic numerical search, not a proof.** Script: [search/real_escape.py](search/real_escape.py). +Raw result lines: [search/results/](search/results/). + +## Method + +For a group `D` of planes, every term slot has fixed plane supports `(A, R)` with `A, R` subsets of +`D` (for 5-7 planes only sides of 1-2 planes, the whole group and all-but-one). The objective is +the mask residual on fixed cells plus `lam * sum_k t(A_k, R_k) |u_k| |v_k|`, minimised by L-BFGS +with `lam` raised in steps. Survivors are pruned by weight and refitted exactly by least squares. +Whenever the refit is exact (max residual below `1e-9`), the run records the **true** cost: the +sum of tariffs of the actual nonzero supports. The mask is the strict one: free entries between +orthogonal planes. A decomposition of the identity endpoint is also a strict-mask decoder, so +"no escape" here also covers the identity endpoint used by the three- and four-plane rank duals. + +Real solutions include every rational one, so a real minimum of `4|D|` excludes all denominators on +that group. The search is local optimisation from random starts and can miss a cheaper decoder. +Where it stops above the baseline, it did not even reach the known decoder, so that line is +weak evidence. + +## Results + +No run found an exact decoder below `4|D|`. + +| Groups | Starts | Reached baseline | Above baseline | Below baseline | +|---|---:|---:|---:|---:| +| 6 open triple classes of `three-plane-rank-dual` | 40 | 6 | 0 | 0 | +| 40 random open quadruples of `four-plane-rank-dual` | 30 | 30 | 10 | 0 | +| 60 most degenerate quadruples (3 of them open) | 30 | 44 | 16 | 0 | +| 23 induced C5s | 15 | 6 | 17 | 0 | +| C5 + 1 most degenerate plane (23) | 15 | 5 | 18 | 0 | +| C5 + 2 most degenerate planes (23) | 15 | 3 | 20 | 0 | + +The baselines are 12, 16, 20, 24 and 28. On quadruples the solver usually reaches 16. On 5-7 plane +groups it often stops 2-10 above, so those rows say little beyond "nothing cheap was found". + +The open quadruples were sampled with `random.Random(2026).sample` from the 5,584 index-zero +quadruples of `four-plane-rank-dual/CERT-INDEX.bin.gz`. The open triple classes are the six classes +of `three-plane-rank-dual/CERTIFICATES.json` that carry an `f2_minimum_mass` field; one example +triple per class is searched. + +## Provenance + +The 60 degenerate quadruples and the C5 groups ran on Kaggle with the same search core from the +fork branch `Matarener/integer-mult-bounds:v4-plane-lb`. The C5 run stopped after 49 of 69 +groups on an `SVD did not converge` error inside a refit; the refit now skips such a prefix, and the +remaining 20 groups ran separately. The `quads-degenerate` and `c5` modes of `real_escape.py` +reproduce the same group lists. The open-quadruple run used `real_escape.py` from this package on +Kaggle; the open-triple run used it locally. diff --git a/research/plane-port-global-rank-dual/FULL-CHECK.json b/research/plane-port-global-rank-dual/FULL-CHECK.json new file mode 100644 index 0000000000..513a60c373 --- /dev/null +++ b/research/plane-port-global-rank-dual/FULL-CHECK.json @@ -0,0 +1,14 @@ +{ + "schema": "plane-port-global-rank-dual/verify/1", + "planes": 56, + "generated_subspaces": 39087, + "ordered_pairs_checked": 1527793569, + "complete": true, + "columns": 443, + "scale": 1048576, + "min_slack": 0, + "tight_pairs": 1732, + "lower_bound": "18233853/131072", + "lower_bound_float": 139.1132583618164, + "new_kappa_claimed": false +} diff --git a/research/plane-port-global-rank-dual/PROOF.md b/research/plane-port-global-rank-dual/PROOF.md new file mode 100644 index 0000000000..1dba9e1f33 --- /dev/null +++ b/research/plane-port-global-rank-dual/PROOF.md @@ -0,0 +1,94 @@ +# Proof of the global bound + +## Object + +The 112 selected ports carry binary labels `q_p` in `F_2^9`. The retained PR1825 matching +(`research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json`) pairs them into 56 planes +`E_i = span(q_a, q_b)`. Every plane is nondegenerate: its 2 x 2 Gram matrix over `F_2` has rank 2. +Two planes are *orthogonal* when every vector of one is orthogonal to every vector of the other; +109 of the 1,540 plane pairs are orthogonal. + +A **decoder** over a field `F` is a finite family of rank-one terms `u_k v_k^T` with +`u_k, v_k in F^112` and `M = sum_k u_k v_k^T`, satisfying the strict scalar mask of PR1889: + +- `M_pp = 1` for every port; +- `M_pq = 0` when `p != q` and the planes of `p` and `q` are equal or non-orthogonal; +- `M_pq` is free when the planes of `p` and `q` are orthogonal. + +`F` is arbitrary: `Q` with any denominators (in particular even ones), `R`, `C`, or a finite field. + +**Tariff** (the contract of #4365, unchanged). Let `A_k` and `R_k` be the sets of planes that contain a +port where `u_k`, respectively `v_k`, is nonzero, and `W(X) = span(E_i : i in X)`. The term costs + + t_k = rank over F_2 of the dot-product pairing between W(A_k) and W(R_k) + = dim W(A_k) - dim(W(A_k) meet W(R_k)^perp). + +It depends only on the plane supports. Charges add: the decoder costs `sum_k t_k`. + +## Theorem + +For every field `F` and every decoder, + + sum_k t_k >= 18233853 / 131072 = 139.1132..., + +hence `sum_k t_k >= 140`, because the cost is an integer. + +## Proof + +A **clique** is a set `Q` of pairwise non-orthogonal planes. Write `P(Q)` for its `2|Q|` ports. + +**Lemma 1 (identity block).** For every clique `Q`, at least `2|Q|` terms touch `Q` on both sides, +that is, have `A_k` meeting `Q` and `R_k` meeting `Q`. + +*Proof.* Every pair of distinct ports in `P(Q)` lies in one plane or in two non-orthogonal planes, so +the mask fixes `M` restricted to `P(Q)` to the identity `I_{2|Q|}`. A term that misses `P(Q)` on +one side restricts to zero there. Hence `I_{2|Q|}` is a sum of the restrictions of the touching +terms, each of rank at most one, and their number is at least `2|Q|`. This holds over every field. +Lean: `V4.identity_block_needs_terms` in [lean/V4Duality.lean](lean/V4Duality.lean). Its hypothesis +is the identity block on a port set `S`; its conclusion counts the terms nonzero on `S` on both +sides. + +**Lemma 2 (weak duality).** Let `w_Q >= 0` be weights on cliques such that every term satisfies + + sum over cliques Q touched by term k on both sides of w_Q <= t_k. (F) + +Then `sum_Q w_Q * 2|Q| <= sum_k t_k`. + +*Proof.* Swap the order of summation and use Lemma 1. Lean: `V4.weak_duality`. + +**Lemma 3 (finite check).** Condition (F) holds for every possible term if, for every ordered pair +`(A, R)` of subspaces generated by nonempty plane sets, + + sum over cliques Q with in(A) meets Q and in(R) meets Q of w_Q <= t(A, R), (F') + +where `in(A)` is the set of planes contained in `A`. + +*Proof.* For a term with nonempty supports put `A = W(A_k)`, `R = W(R_k)`. Then `A_k` is contained in +`in(A)`, so every clique touched by the term is counted in (F'), and `t_k = t(A, R)`. A term with an +empty side costs 0 and touches no clique. + +**The certificate.** [CERTIFICATE.json](CERTIFICATE.json) lists 443 cliques, of sizes up to 24, +with integer weights `w_Q / 2^20`. [verify.py](verify.py) recomputes the planes from the pinned +archive and matching, enumerates all 39,087 subspaces generated by plane sets, computes their +tariffs, checks that every column is a clique and checks (F') on all `39,087^2 = 1,527,793,569` +ordered pairs in exact integer arithmetic. The minimum slack is 0, attained on 1,732 pairs. The +bound is `sum_Q w_Q 2|Q| / 2^20 = 18233853/131072`. + +Lemmas 1-3 and the certificate give the theorem. + +## Where the certificate came from + +The weights are a rounded-down optimal dual of a clique linear programme solved by column +generation (separation over all ordered span pairs, on Kaggle). Only the rounded certificate +matters for the proof. We do not know the optimum of the full clique programme. A floating-point +pricing estimate from the same run suggests it is at most about 167; that estimate is not +certified here. + +## What the proof does not use + +- No coefficient restriction: no integrality, no parity, no bound on denominators or term counts. +- No symmetry `u_k = v_k` and no positivity. +- Free mask entries are never used; only identity blocks on cliques. + +It also leaves out everything outside the #4365 contract: native realization, hosting, routing and +any non-additive or concave pricing. diff --git a/research/plane-port-global-rank-dual/README.md b/research/plane-port-global-rank-dual/README.md new file mode 100644 index 0000000000..ee074b60df --- /dev/null +++ b/research/plane-port-global-rank-dual/README.md @@ -0,0 +1,120 @@ +# Every plane-port decoder costs at least 140, over every field + +**Scoped proof with an exact finite certificate and two Lean-checked lemmas. No new κ.** +For the selected 112 ports matched into 56 planes (PR1825) and the strict scalar mask (PR1889), +every finite rank-one decoder, over **any** coefficient field, has additive full-plane COPY mass + + sum of tariffs >= 18233853/131072 = 139.113..., hence >= 140. + +This is the first global bound for the whole 56-plane decoder that holds for arbitrary rational +coefficients, in particular with even denominators. Before it, the only all-field global bound was +the fitting rank 49. The value 224 is proved only for 2-integral coefficients and characteristic 2 +(Philippe Van Velzen), and for decoders split into disjoint plane pairs (#4365). + +The package also states the **conjecture that 224 holds over every field**, gives the structural +conditions an escape below 224 would have to meet, and reports a numerical search over real +coefficients on the open local cases left by the three- and four-plane rank duals. That search +found no escape. It is evidence, not proof. + +## Contract + +Unchanged from CubeJerry's #4365, as used by `three-plane-rank-dual` and `four-plane-rank-dual`: +a term `u vᵀ` costs the binary pairing rank between the spans of the complete planes touched by +`u` and by `v`; charges add; coefficients lie in any field. The endpoint here is the full strict +112-port mask: unit diagonal, zeros inside planes and between non-orthogonal planes, free entries +between orthogonal planes. [PROOF.md](PROOF.md) states it precisely. + +## Why it matters + +`plane-port-copy-budgets` (josie) prices the plane-port lever: a decoder must cost at most about +160-164 per call just to match the incumbent word, and the lever map in Discussion 2278 needs about +128 for doubling κ. The bound 140 excludes the doubling target for every coefficient field inside +this contract. The break-even window `[140, 164]` stays open, and only for characteristic-0 +coefficients with essential even denominators ([THEORY.md](THEORY.md), E1). + +## Proof in one paragraph + +On a clique `Q` of pairwise non-orthogonal planes the mask is the identity on `2|Q|` ports, so at +least `2|Q|` terms touch `Q` on both sides, over every field. Weights `w_Q >= 0` with +`sum_{Q touched by a term} w_Q <= tariff` for every possible term then give +`total tariff >= sum_Q 2|Q| w_Q` by weak duality. Tariffs depend only on the generated spans, so +the feasibility condition is a finite check over all 39,087² ordered pairs of plane-generated +subspaces. [CERTIFICATE.json](CERTIFICATE.json) gives 443 cliques with integer weights `/2^20`. +The two abstract lemmas are kernel-checked in Lean ([lean/](lean/)); the finite check is +[verify.py](verify.py). + +## Evidence for the conjecture + +[EVIDENCE.md](EVIDENCE.md) has the tables. In short, a sparse real-coefficient search with exact +refits found no local decoder below 4 per plane on: + +- all 6 open triple classes of `three-plane-rank-dual` (the classes with no all-field certificate); +- 40 random open quadruples of `four-plane-rank-dual`, plus 3 more open ones met by chance; +- the 60 most degenerate quadruples; +- 69 groups built from the 23 induced 5-cycles and their 6- and 7-plane extensions. + +A real solution space contains every rational one, so a real minimum of `4|S|` excludes every +denominator. The search is local optimization from random starts, and on 5-7 plane groups it often +stops above the baseline, so these runs are weak evidence there. + +## Reproduce + +From the repository root, with Python 3.12 and numpy 2: + +```sh +python3 -B research/plane-port-global-rank-dual/verify.py # bounded: every 97th row, ~1 min +python3 -B research/plane-port-global-rank-dual/verify.py --full # all 1.53e9 pairs, ~7 min +bash research/plane-port-global-rank-dual/lean/check.sh # Lean v4.21.0 + Mathlib cache +``` + +The bounded run checks the census, 20,000 tariffs against Gaussian elimination, every clique and +weight, the bound, three rejecting controls, and feasibility on 403 of 39,087 rows. The full run +writes [FULL-CHECK.json](FULL-CHECK.json): all 1,527,793,569 ordered pairs, minimum slack 0 on +1,732 tight pairs. The searches need scipy: + +```sh +python3 research/plane-port-global-rank-dual/search/real_escape.py triples-open 40 +python3 research/plane-port-global-rank-dual/search/real_escape.py quads-open 40 30 2026 +python3 research/plane-port-global-rank-dual/search/real_escape.py quads-degenerate 60 30 +python3 research/plane-port-global-rank-dual/search/real_escape.py c5 15 +``` + +## Not covered + +- The conjecture itself: no bound between 140 and 224 is proved for characteristic 0. +- The optimum of the full clique programme. A floating-point column-generation estimate suggests it + is at most about 167, so this method alone may not reach 164; that estimate is not certified. +- Native realization, hosting, routing and the coverage law, which are #4365's caveats. +- Non-additive or concave pricing. + +## Open next questions + +1. **Does every decoder cost at least 224 over Q?** + - *Why it matters:* it would close the plane-port lever for every coefficient field. + - *First step:* turn the 2-adic layering of THEORY.md E2 into an induction on the top valuation, + bounding what a zero-mask binary layer can save on the integral layer. + - *Blocked by:* no known lower bound for zero-mask layers. +2. **Can a stronger functional beat the clique programme?** + - *Why it matters:* `[140, 164]` is the break-even window; a certified value above 164 would close + the lever in this contract without settling the conjecture. + - *First step:* add the sharp C5 covers of `c5-residual-weighted-cover` and the four-plane + certificates as columns, with the same exhaustive span-pair separation. + - *Blocked by:* nothing; the column-generation code is in the fork branch named in TASK.json. +3. **Is there an exact rational escape on an open four-plane class?** + - *Why it matters:* a cost-15 decoder would be the first mixing gain under #4365's contract. + - *First step:* exact search with forced half coefficients (THEORY.md E1) on the lowest LP class + of `four-plane-rank-dual`. + - *Blocked by:* nothing. + +## Credit + +The contract and the two-plane theorem are CubeJerry's (#4365). The rank-dual functional +`sum_X w_X rank(M_XX)` is pinterbanget's (Ryanson Jonathan: #4421 and the four-plane extension); +this package applies it to cliques of the whole 112-port mask. The 224 bound for 2-integral decoders is +Philippe Van Velzen's (Discussion 1587, #2532). The fitting rank 49 is from PR2471 (ywz65) and +PR2484 (Sagar Thakrar). The C5 results are Tekalign's, Sagar Thakrar's and Nick Petalas's. +The plane-port budgets are josie's. Labels and matching come from PR1825/2126 (Cinna Davis). + +Prepared by Mark (Matarener) with substantial Claude Code assistance in derivation, code, Lean and +writing. The verifier was written separately from the code that generated the certificate, in the +same AI-assisted project. No independent human review is claimed. Apache-2.0. diff --git a/research/plane-port-global-rank-dual/SOURCES.json b/research/plane-port-global-rank-dual/SOURCES.json new file mode 100644 index 0000000000..f238d4ef5f --- /dev/null +++ b/research/plane-port-global-rank-dual/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/four-plane-rank-dual/CERT-INDEX.bin.gz", + "usage": "input", + "git_blob": "7c525e1ed8af5069c8bb28cac9fefe40406a9261", + "sha256": "b66ba05b1b37a1be42c85ce855eca387a822df9d0b5d93a2d46d8c46d84ad7b1" + }, + { + "path": "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json", + "usage": "input", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + }, + { + "path": "research/three-plane-rank-dual/CERTIFICATES.json", + "usage": "input", + "git_blob": "43087b96986d9e770807d090f2286a6e2135df4a", + "sha256": "f343036b3788969a690c87e6cdded90b2351d90caa5340c8b813e2240ffb0438" + } + ] +} diff --git a/research/plane-port-global-rank-dual/TASK.json b/research/plane-port-global-rank-dual/TASK.json new file mode 100644 index 0000000000..c5a2e96fa8 --- /dev/null +++ b/research/plane-port-global-rank-dual/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Global all-field lower bound 18233853/131072 (hence 140) on the additive full-plane COPY mass of every finite scalar decoder of the strict 112-port PR1825/PR1889 mask, via a rank-dual certificate on 443 cliques; Lean for the two abstract lemmas; conjecture 224 with escape-structure notes and a real-coefficient search on open local cases.", + "scope_change_reason": "The card asks about block decoders and larger-rank children; this package answers the coefficient question for the plane-port decoder instead: can even denominators lower its COPY mass below the 2-integral floor 224? It proves a global all-field floor and leaves the dyadic gap [140, 224] open.", + "bottleneck_link": "Side result for the plane-port coverage lever (plane-port-copy-budgets): a per-call charge of at most about 160-164 is needed to break even and about 128 to double kappa; 140 excludes the doubling target for every coefficient field in #4365's contract.", + "budget_minutes": 600, + "stop_rule": "Stop at the exact certified clique bound plus local search evidence; do not attempt a native construction.", + "outcome": "completed", + "evidence": "verify.py: closure census of 39,087 generated subspaces, tariffs cross-checked by Gaussian elimination, 443 clique columns, exhaustive feasibility on all 39,087^2 ordered pairs (FULL-CHECK.json), three rejecting controls. Lean v4.21.0/Mathlib: V4.identity_block_needs_terms, V4.weak_duality, V4.decoder_cost_ge, axioms propext/Classical.choice/Quot.sound only. Search: search/results.", + "author": "Mark (Matarener)", + "ai_assistance": "Claude Code (Anthropic) for derivation, certificate generation, verifier, Lean proofs, searches and writing; computations on Kaggle. No independent human review claimed.", + "open_questions": [ + { + "question": "Does every decoder of the strict mask cost at least 224 over Q?", + "why_it_matters": "It would close the plane-port lever for every coefficient field.", + "first_step": "Induct on the top 2-adic valuation (THEORY.md E2), bounding what a zero-mask binary layer can save.", + "blocked_by": "No known lower bound for zero-mask layers." + }, + { + "question": "Can a functional stronger than the clique programme certify more than 164?", + "why_it_matters": "It would close the break-even window in this contract without settling the conjecture.", + "first_step": "Add sharp C5 covers and four-plane certificates as columns with the same exhaustive span-pair separation.", + "blocked_by": "Nothing." + }, + { + "question": "Is there an exact rational cost-15 decoder on an open four-plane class?", + "why_it_matters": "It would be the first mixing gain under #4365's contract.", + "first_step": "Exact search with forced half coefficients on the lowest LP class of four-plane-rank-dual.", + "blocked_by": "Nothing." + } + ], + "fork_branch": "https://github.com/Matarener/integer-mult-bounds/tree/v4-plane-lb (certificate generation and column-generation code)" +} diff --git a/research/plane-port-global-rank-dual/THEORY.md b/research/plane-port-global-rank-dual/THEORY.md new file mode 100644 index 0000000000..bfa8755cae --- /dev/null +++ b/research/plane-port-global-rank-dual/THEORY.md @@ -0,0 +1,84 @@ +# The 224 conjecture and the structure of a possible escape + +Notation as in [PROOF.md](PROOF.md). "Escape" means a decoder, or a decoder restricted to a group +of planes, that costs less than 2 per port. + +## Conjecture + +**Every decoder of the strict 112-port mask costs at least 224, over every field.** + +Equivalently, under #4365's contract, plane ports cannot lower the additive COPY mass below +separate coordinate messages, whatever the coefficients. What is proved: + +| Class | Bound | Source | +|---|---:|---| +| 2-integral coefficients (odd denominators) | 224, sharp | Philippe Van Velzen, Discussion 1587; #2532 | +| fields of characteristic 2 | 224, sharp | same rank argument; Lean `V4.decoder_cost_ge` | +| decoders split into disjoint plane pairs, any field | 224 | CubeJerry, `two-plane-copy-floor` (#4365) | +| any decoder, any field | 49 | fitting rank, `paired-plane-minrank-bracket-audit` | +| **any decoder, any field** | **140** | **this package** | + +The gap is therefore `[140, 224]`, and it concerns only fields of characteristic 0, so in +particular rational decoders with even denominators. + +## E1. Why an escape must use essential halves + +The tariff depends only on the plane supports `(A_k, R_k)`. If the same support pattern, or a +pattern with smaller supports, is realized by some decoder over `F_2`, then its cost is at least 224 +by the characteristic-2 theorem, because tariffs are monotone under shrinking supports. So an +escape needs a support pattern whose mask equations are solvable over `Q` but have no solution +over `F_2` with those supports. By the 2-integral theorem, no rescaling `u_k -> 2^a u_k`, +`v_k -> 2^-a v_k` of the terms may make all coefficients 2-integral. + +## E2. 2-adic layering + +Rescale every term of a rational decoder so that `u_k` is primitive (minimum 2-adic valuation 0). +Let `-e < 0` be the smallest valuation among the `v_k`, and `L` the set of terms that reach it. On +every fixed mask entry `M_pq` is an integer, so the leading parts cancel: + + sum over k in L of (u_k mod 2)(2^e v_k mod 2)^T = 0 on all fixed entries, over F_2. + +The most fractional layer is a binary decomposition of the zero mask, free entries arbitrary. Such +layers are not free: each term still pays its full tariff. An escape must buy, with zero-mask +layers, a saving on the integral layer that the binary argument does not see. This is the same +mechanism as the known escape in `research/bit-full-borel-2adic-floor`, and the positive +half-integral barrier of `c5-dyadic-decoder-gate` (Tekalign) shows that the first layer alone does +not suffice in that model. Bounding what zero-mask layers can buy would settle the conjecture. + +## E3. A necessary spectral condition on cliques + +Let `S` be a clique, so the mask on its `2|S|` ports is the identity. Split the terms that touch +`S` on both sides into *diagonal* terms, where some plane of `S` lies in both `A_k` and `R_k` +(tariff at least 2, since the pairing already has rank 2 on that plane), and *cross* terms, where +`A_k` and `R_k` meet `S` in disjoint plane sets (tariff `t_j >= 1`, since the planes are +non-orthogonal). Let `N` be the sum of the cross terms restricted to `S` and `m = dim ker(I - N)`. +The diagonal terms sum to `I - N`, so there are at least `2|S| - m` of them, and + + cost on S >= 4|S| - 2m + sum_j t_j. + +A saving on `S` needs `2m > sum_j t_j`: the cross part must have eigenvalue 1 with multiplicity above +half its tariff. + +- If the cross terms are bipartite (the planes of `S` split into two sides and every cross term goes + between them), then `N` is similar to `-N`, so in characteristic not 2 the eigenspaces for 1 and + -1 have the same dimension `m` and both lie in the range of `N`. Hence `2m <= rank N <= sum_j t_j` + and there is no saving. For two planes this reproves the 8 of `two-plane-copy-floor`. +- So a saving needs odd cycles among the cross terms. These are not rare: 879 plane pairs have a + single-plane cross term of tariff 1, these pairs touch all 56 planes, they form 5,136 triangles, + and the graph is not bipartite. The combinatorial condition alone excludes nothing. +- The extreme case `m = 2|S| - 2` forces `I - N` to have rank 2, which is realizable over `F_2` and + therefore excluded by E1. + +## E4. Where an escape is most plausible + +On groups that contain orthogonal plane pairs, the mask has free entries and its rank drops below +`2|S|` over every field: 5 instead of 4 per induced 5-cycle, 49 instead of 48 globally. Over `F_2` +the binary Gram lift removes the free entries, which is why the 224 bound survives those rank +savings in characteristic 2. Over `Q` there is no such lift. Odd holes of the non-orthogonality +graph together with dyadic coefficients are therefore the main suspects. The proven local +results there are sharp at 20 on the C5s (`c5-gram-rank-cover`, `c5-asymmetric-cost-floor`, +`c5-residual-weighted-cover`), and our numerical search found nothing cheaper on C5s extended by +one or two planes ([EVIDENCE.md](EVIDENCE.md)). + +E1-E4 are structural observations, written proofs only; they are not formalized and they do not +prove the conjecture. diff --git a/research/plane-port-global-rank-dual/VERIFY.json b/research/plane-port-global-rank-dual/VERIFY.json new file mode 100644 index 0000000000..c7329da08f --- /dev/null +++ b/research/plane-port-global-rank-dual/VERIFY.json @@ -0,0 +1,25 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.2.6" + ], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/four-plane-rank-dual/CERT-INDEX.bin.gz", + "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json", + "research/three-plane-rank-dual/CERTIFICATES.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "closure census, tariff formula vs Gaussian elimination, clique columns, bound, three rejecting controls, feasibility on every 97th row; --full checks all rows (FULL-CHECK.json)" + } + ] +} diff --git a/research/plane-port-global-rank-dual/lean/V4Duality.lean b/research/plane-port-global-rank-dual/lean/V4Duality.lean new file mode 100644 index 0000000000..5da80935f1 --- /dev/null +++ b/research/plane-port-global-rank-dual/lean/V4Duality.lean @@ -0,0 +1,100 @@ +import Mathlib + +/-! +# V4: the abstract half of the clique-dual lower bound on plane-port decoders + +A plane-port decoder is a matrix `M = ∑ₖ uₖ vₖᵀ` over any field `F` (e.g. ℚ with arbitrary, also even, denominators) on a finite port set `ι`. + +* `identity_block_needs_terms`: if `M` restricted to a port set `S` is the identity, then at least `|S|` + terms `k` touch `S` on both sides (`uₖ` nonzero somewhere on `S` and `vₖ` nonzero somewhere on `S`). + For a clique of pairwise non-orthogonal planes the mask forces exactly this identity block. +* `weak_duality`: if every column `x` (a clique) is touched by at least `r x` terms and the weights `lam ≥ 0` + satisfy `∑_{x touched by k} lam x ≤ cost k` for every term `k`, then `∑ₓ lam x * r x ≤ ∑ₖ cost k`. + +Together: any feasible weight vector `lam` on cliques gives `total tariff ≥ ∑_Q lam_Q · 2|Q|`. +The finite feasibility check of a concrete `lam` is a separate, data-dependent step. +-/ + +open Finset + +namespace V4 + +/-- Weak duality for covering bounds. -/ +theorem weak_duality {K X : Type*} [Fintype K] [Fintype X] + (touch : K → X → Prop) [∀ k x, Decidable (touch k x)] + (cost : K → ℝ) (lam r : X → ℝ) (hlam : ∀ x, 0 ≤ lam x) + (hcover : ∀ x, r x ≤ ((univ.filter fun k => touch k x).card : ℝ)) + (hfeas : ∀ k, ∑ x ∈ univ.filter (fun x => touch k x), lam x ≤ cost k) : + ∑ x, lam x * r x ≤ ∑ k, cost k := by + have h1 : ∀ x, lam x * ((univ.filter fun k => touch k x).card : ℝ) + = ∑ k, if touch k x then lam x else 0 := by + intro x + rw [Finset.card_filter] + push_cast + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro k _ + split_ifs <;> simp + calc ∑ x, lam x * r x + ≤ ∑ x, lam x * ((univ.filter fun k => touch k x).card : ℝ) := + Finset.sum_le_sum fun x _ => mul_le_mul_of_nonneg_left (hcover x) (hlam x) + _ = ∑ x, ∑ k, if touch k x then lam x else 0 := Finset.sum_congr rfl fun x _ => h1 x + _ = ∑ k, ∑ x, if touch k x then lam x else 0 := Finset.sum_comm + _ = ∑ k, ∑ x ∈ univ.filter (fun x => touch k x), lam x := by + apply Finset.sum_congr rfl + intro k _ + rw [Finset.sum_filter] + _ ≤ ∑ k, cost k := Finset.sum_le_sum fun k _ => hfeas k + +/-- An identity block on a port set `S` needs at least `|S|` rank-one terms touching `S` on both sides. -/ +theorem identity_block_needs_terms {F ι K : Type*} [Field F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype K] [DecidableEq K] + (u v : K → ι → F) (S : Finset ι) + (hM : ∀ p ∈ S, ∀ q ∈ S, ∑ k, u k p * v k q = if p = q then 1 else 0) : + S.card ≤ (univ.filter fun k => (∃ p ∈ S, u k p ≠ 0) ∧ (∃ q ∈ S, v k q ≠ 0)).card := by + classical + set T := univ.filter fun k => (∃ p ∈ S, u k p ≠ 0) ∧ (∃ q ∈ S, v k q ≠ 0) with hT + let w : K → (S → F) := fun k p => u k p + let W : Submodule (F) (S → F) := + Submodule.span (F) ((T.image w : Finset (S → F)) : Set (S → F)) + have key : ∀ q : S, (Pi.single q 1 : S → F) ∈ W := by + intro q + have hsum : (Pi.single q 1 : S → F) = ∑ k ∈ T, v k q • w k := by + funext p + simp only [Finset.sum_apply, Pi.smul_apply, smul_eq_mul, w] + have hz : ∀ k ∈ (univ : Finset K), k ∉ T → v k q * u k p = 0 := by + intro k _ hk + rw [hT, Finset.mem_filter] at hk + simp only [Finset.mem_univ, true_and] at hk + by_cases h : ∃ p ∈ S, u k p ≠ 0 + · have hv : ∀ q ∈ S, v k q = 0 := by + intro q' hq' + by_contra hne + exact hk ⟨h, q', hq', hne⟩ + rw [hv q q.2, zero_mul] + · push_neg at h + rw [h p p.2, mul_zero] + rw [Finset.sum_subset (Finset.subset_univ T) hz] + have h := hM p p.2 q q.2 + simp_rw [mul_comm (v _ (q : ι))] + rw [h, Pi.single_apply] + by_cases hpq : p = q + · simp [hpq] + · have : (p : ι) ≠ q := fun e => hpq (Subtype.ext e) + simp [hpq, this] + rw [hsum] + refine Submodule.sum_mem _ fun k hk => Submodule.smul_mem _ _ ?_ + exact Submodule.subset_span (Finset.mem_coe.mpr (Finset.mem_image_of_mem w hk)) + have htop : W = ⊤ := by + rw [eq_top_iff, ← (Pi.basisFun (F) S).span_eq, Submodule.span_le] + rintro _ ⟨q, rfl⟩ + simpa [Pi.basisFun_apply] using key q + calc S.card = Fintype.card S := (Fintype.card_coe S).symm + _ = Module.finrank (F) (S → F) := (Module.finrank_fintype_fun_eq_card (F)).symm + _ = Module.finrank (F) W := by rw [htop, finrank_top] + _ ≤ (T.image w).card := finrank_span_finset_le_card _ + _ ≤ T.card := Finset.card_image_le + +end V4 + +#print axioms V4.weak_duality +#print axioms V4.identity_block_needs_terms diff --git a/research/plane-port-global-rank-dual/lean/V4Rank.lean b/research/plane-port-global-rank-dual/lean/V4Rank.lean new file mode 100644 index 0000000000..f9d5b933c3 --- /dev/null +++ b/research/plane-port-global-rank-dual/lean/V4Rank.lean @@ -0,0 +1,113 @@ +import Mathlib + +/-! +# V4: every plane-port decoder costs at least 2 × (number of ports) + +Setting (over any field `F`). Each port `p : ι` carries the two label vectors `L p 0, L p 1 : d → F` of its plane. +A decoder is `M = ∑ₖ uₖ vₖᵀ` (`u v : K → ι → F`). The term `k` is priced by `rank ((A k)ᵀ * B k)`, where the columns of +`A k` (resp. `B k`) span a subspace containing the labels of every port in the support of `uₖ` (resp. `vₖ`); with bases +this is exactly the rank of the dot-product pairing between the source-plane span and the reader-plane span (the tariff). + +`lift L u` is the `d × (2 × ι)` matrix whose column `(a, p)` is `u p • L p a`. Hypotheses `hA`, `hB` say these columns lie +in the spans of `A k`, `B k`. The mask is used only through `hdiag` (`M p p = 1`) and `hoff` (for `p ≠ q`, `M p q` vanishes +or the two planes are orthogonal), and every plane has an invertible 2 × 2 Gram matrix (`hgram`). + +Conclusion: `2 * |ι| ≤ ∑ₖ tariffₖ`. Proof: `∑ₖ (lift uₖ)ᵀ (lift vₖ)` is block diagonal with the invertible plane Grams, +so it has rank `2|ι|`; rank is subadditive; and each summand has rank at most its tariff. +-/ + +open Matrix Finset + +set_option linter.unusedSectionVars false + +namespace V4 + +variable {F : Type*} [Field F] {ι d K : Type*} [Fintype ι] [DecidableEq ι] [Fintype d] [DecidableEq d] [Fintype K] + +/-- column `(a, p)` is `u p • L p a` -/ +def lift (L : ι → Fin 2 → d → F) (u : ι → F) : Matrix d (Fin 2 × ι) F := fun i ab => u ab.2 * L ab.2 ab.1 i + +/-- the rank of one term is at most its tariff -/ +theorem rank_term_le {m : Type*} [Fintype m] (X Y : Matrix d (Fin 2 × ι) F) (A B : Matrix d m F) + (hX : ∃ C : Matrix m (Fin 2 × ι) F, X = A * C) (hY : ∃ C : Matrix m (Fin 2 × ι) F, Y = B * C) : + (Xᵀ * Y).rank ≤ (Aᵀ * B).rank := by + obtain ⟨C, rfl⟩ := hX + obtain ⟨C', rfl⟩ := hY + have h : (A * C)ᵀ * (B * C') = Cᵀ * ((Aᵀ * B) * C') := by + simp only [transpose_mul, Matrix.mul_assoc] + rw [h] + exact (rank_mul_le_right _ _).trans (rank_mul_le_left _ _) + +/-- rank of a sum of two matrices -/ +theorem rank_add_le' {m n : Type*} [Fintype m] [Fintype n] (A B : Matrix m n F) : + (A + B).rank ≤ A.rank + B.rank := by + unfold Matrix.rank + rw [Matrix.mulVecLin_add] + have h : LinearMap.range (A.mulVecLin + B.mulVecLin) + ≤ LinearMap.range A.mulVecLin ⊔ LinearMap.range B.mulVecLin := by + intro y hy + obtain ⟨x, rfl⟩ := LinearMap.mem_range.mp hy + rw [LinearMap.add_apply] + exact Submodule.add_mem_sup (LinearMap.mem_range_self _ x) (LinearMap.mem_range_self _ x) + exact (Submodule.finrank_mono h).trans (Submodule.finrank_add_le_finrank_add_finrank _ _) + +/-- rank is subadditive over finite sums -/ +theorem rank_sum_le {m n : Type*} [Fintype m] [Fintype n] (s : Finset K) (f : K → Matrix m n F) : + (∑ k ∈ s, f k).rank ≤ ∑ k ∈ s, (f k).rank := by + classical + refine Finset.induction_on s ?_ ?_ + · simp + · intro a s ha ih + rw [Finset.sum_insert ha, Finset.sum_insert ha] + exact (rank_add_le' _ _).trans (Nat.add_le_add_left ih _) + +/-- the sum of the lifted terms, entrywise -/ +theorem sum_lift (L : ι → Fin 2 → d → F) (u v : K → ι → F) (a b : Fin 2) (p q : ι) : + (∑ k, (lift L (u k))ᵀ * lift L (v k)) (a, p) (b, q) + = (∑ k, u k p * v k q) * (∑ i, L p a i * L q b i) := by + rw [Matrix.sum_apply, Finset.sum_mul] + apply Finset.sum_congr rfl + intro k _ + simp only [mul_apply, transpose_apply, lift, Finset.mul_sum] + apply Finset.sum_congr rfl + intro i _ + ring + +/-- **Main theorem.** Every decoder whose mask kills all non-orthogonal off-diagonal pairs and keeps the diagonal costs +at least `2 * |ι|`. -/ +theorem decoder_cost_ge (L : ι → Fin 2 → d → F) (u v : K → ι → F) {m : Type*} [Fintype m] + (A B : K → Matrix d m F) + (hA : ∀ k, ∃ C : Matrix m (Fin 2 × ι) F, lift L (u k) = A k * C) + (hB : ∀ k, ∃ C : Matrix m (Fin 2 × ι) F, lift L (v k) = B k * C) + (hdiag : ∀ p, ∑ k, u k p * v k p = 1) + (hoff : ∀ p q, p ≠ q → ∀ a b, (∑ k, u k p * v k q) * (∑ i, L p a i * L q b i) = 0) + (hgram : ∀ p, IsUnit (Matrix.of fun a b : Fin 2 => ∑ i, L p a i * L p b i)) : + 2 * Fintype.card ι ≤ ∑ k, ((A k)ᵀ * B k).rank := by + classical + set G : ι → Matrix (Fin 2) (Fin 2) F := fun p => Matrix.of fun a b => ∑ i, L p a i * L p b i with hG + have hD : (∑ k, (lift L (u k))ᵀ * lift L (v k)) = blockDiagonal G := by + ext ⟨a, p⟩ ⟨b, q⟩ + rw [sum_lift] + by_cases hpq : p = q + · subst hpq + rw [blockDiagonal_apply_eq, hdiag, one_mul] + simp [hG] + · rw [blockDiagonal_apply_ne G a b hpq] + exact hoff p q hpq a b + have hunit : IsUnit (blockDiagonal G) := by + rw [Matrix.isUnit_iff_isUnit_det, det_blockDiagonal] + exact IsUnit.prod_univ_iff.mpr fun p => (Matrix.isUnit_iff_isUnit_det _).mp (hgram p) + have hrank : (blockDiagonal G).rank = 2 * Fintype.card ι := by + rw [rank_of_isUnit _ hunit, Fintype.card_prod, Fintype.card_fin] + calc 2 * Fintype.card ι = (∑ k, (lift L (u k))ᵀ * lift L (v k)).rank := by rw [hD, hrank] + _ ≤ ∑ k, ((lift L (u k))ᵀ * lift L (v k)).rank := rank_sum_le _ _ + _ ≤ ∑ k, ((A k)ᵀ * B k).rank := + Finset.sum_le_sum fun k _ => rank_term_le _ _ _ _ (hA k) (hB k) + +end V4 + +#print axioms V4.rank_add_le' +#print axioms V4.rank_term_le +#print axioms V4.rank_sum_le +#print axioms V4.sum_lift +#print axioms V4.decoder_cost_ge diff --git a/research/plane-port-global-rank-dual/lean/check.sh b/research/plane-port-global-rank-dual/lean/check.sh new file mode 100644 index 0000000000..ede6f4a48f --- /dev/null +++ b/research/plane-port-global-rank-dual/lean/check.sh @@ -0,0 +1,15 @@ +#!/usr/bin/env bash +# Kernel-check both files: Lean v4.21.0 (elan) + the pinned Mathlib cache; reject sorry, errors and non-standard axioms. +set -euo pipefail +cd "$(dirname "$0")" +command -v lake >/dev/null || { curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y --default-toolchain none >/dev/null; export PATH="$HOME/.elan/bin:$PATH"; } +lake exe cache get > cache.log 2>&1 || { tail -20 cache.log; exit 1; } +for f in V4Duality.lean V4Rank.lean; do + echo "=== $f" + lake env lean -DwarningAsError=true "$f" 2>&1 | tee "$f.out" + if grep -q "sorry" "$f.out"; then echo "SORRY in $f"; exit 1; fi + if grep -q "error" "$f.out"; then echo "ERROR in $f"; exit 1; fi + if grep "depends on axioms" "$f.out" | grep -v -E "\[(propext|Classical.choice|Quot.sound)(, (propext|Classical.choice|Quot.sound))*\]$"; then echo "BAD AXIOMS"; exit 1; fi +done +rm -f cache.log ./*.out +echo "ALL LEAN CHECKS PASSED" diff --git a/research/plane-port-global-rank-dual/lean/lake-manifest.json b/research/plane-port-global-rank-dual/lean/lake-manifest.json new file mode 100644 index 0000000000..7fea5106df --- /dev/null +++ b/research/plane-port-global-rank-dual/lean/lake-manifest.json @@ -0,0 +1,116 @@ +{ + "version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "308445d7985027f538e281e18df29ca16ede2ba3", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "308445d7985027f538e281e18df29ca16ede2ba3", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c4aa78186d388e50a436e8362b947bae125a2933", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6980f6ca164de593cb77cd03d8eac549cc444156", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.62", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8ff27701d003456fd59f13a9212431239d902aef", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "e9c65db4823976353cd0bb03199a172719efbeb7", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8d2067bf518731a70a255d4a61b5c103922c772e", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "V4Duality", + "lakeDir": ".lake" +} diff --git a/research/plane-port-global-rank-dual/lean/lakefile.toml b/research/plane-port-global-rank-dual/lean/lakefile.toml new file mode 100644 index 0000000000..32822d1fc0 --- /dev/null +++ b/research/plane-port-global-rank-dual/lean/lakefile.toml @@ -0,0 +1,9 @@ +name = "V4Duality" + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4" +rev = "308445d7985027f538e281e18df29ca16ede2ba3" + +[[lean_lib]] +name = "V4Duality" diff --git a/research/plane-port-global-rank-dual/lean/lean-toolchain b/research/plane-port-global-rank-dual/lean/lean-toolchain new file mode 100644 index 0000000000..980709bbba --- /dev/null +++ b/research/plane-port-global-rank-dual/lean/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.21.0 diff --git a/research/plane-port-global-rank-dual/search/real_escape.py b/research/plane-port-global-rank-dual/search/real_escape.py new file mode 100644 index 0000000000..6e3adfde57 --- /dev/null +++ b/research/plane-port-global-rank-dual/search/real_escape.py @@ -0,0 +1,178 @@ +#!/usr/bin/env python3 +"""Heuristic real-coefficient escape search for local plane-port decoders (evidence, not proof). + +For a group D of matched planes, minimise ||mask residual||^2 + lam * sum_k t_k * |u_k||v_k| over real rank-one +terms u_k v_k^T whose plane supports are fixed per slot (L-BFGS, lam raised in steps), then prune by weight, refit +the survivors exactly by least squares and record the TRUE cost (sum of binary pairing tariffs of the actual +supports) whenever the refit is exact (max residual < 1e-9). Fixed mask cells: diagonal 1; 0 inside a plane and +between non-orthogonal planes; entries between orthogonal planes are free. A real solution space contains every +rational one, so a cost below 4|D| would be an escape for every denominator. "No escape" is local-search evidence. + +usage: real_escape.py triples-open STARTS | quads-open N STARTS SEED | quads-degenerate N STARTS + | c5 STARTS | groups "a,b,c;d,e,f,g" STARTS +""" +import gzip, io, itertools, json, random, sys, tarfile, time, multiprocessing as mp +from pathlib import Path +import numpy as np, scipy.optimize as so +ROOT = Path(__file__).resolve().parents[3] +ARCHIVE = ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +MATCHING = ROOT / 'research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json' +TRI = ROOT / 'research/three-plane-rank-dual/CERTIFICATES.json' +QUAD = ROOT / 'research/four-plane-rank-dual/CERT-INDEX.bin.gz' +dot = lambda x, y: (x & y).bit_count() & 1 +def lead(b): return 1 << (b.bit_length() - 1) +def reduce(basis, v): + for b in basis: + if v & lead(b): v ^= b + return v +def add(basis, v): + basis = list(basis); v = reduce(basis, v) + if not v: return tuple(basis) + L = lead(v); basis = [b ^ v if b & L else b for b in basis] + [v] + return tuple(sorted(basis, reverse=True)) +def span(vs): + s = () + for v in vs: s = add(s, v) + return s +def contains(s, v): return reduce(s, v) == 0 +def pair_rank(A, B): + """rank over F2 of the pairing matrix between bases A and B""" + rows = [sum(dot(x, y) << k for k, y in enumerate(B)) for x in A] + r = 0 + for bit in range(len(B)): + piv = next((i for i in range(r, len(rows)) if rows[i] >> bit & 1), None) + if piv is None: continue + rows[r], rows[piv] = rows[piv], rows[r] + for i in range(len(rows)): + if i != r and rows[i] >> bit & 1: rows[i] ^= rows[r] + r += 1 + return r + +with tarfile.open(ARCHIVE) as _a: + labels = [r['q'] for r in json.loads(_a.extractfile(_a.getmember(MEMBER)).read())['recipes']] +pairs = json.loads(MATCHING.read_text())['matching'] +planes = [(labels[a], labels[b]) for a, b in pairs]; NP = len(planes) +ORTH = [[i != j and all(dot(x, y) == 0 for x in planes[i] for y in planes[j]) for j in range(NP)] for i in range(NP)] +def sp(D): return span([v for i in D for v in planes[i]]) +def tar(A, R): return pair_rank(sp(A), sp(R)) if A and R else 0 +COPIES = 2 +def search(D, starts, seed): + global COPIES + COPIES = 2 if len(D) <= 5 else 1 + t0 = time.time() + def L(*a): print('[%s %5.0fs]' % (','.join(map(str, D)), time.time() - t0), *a, flush=True) + rng = np.random.default_rng(seed); g = len(D); m = 2 * g + fixed = [(p, q, float(p == q)) for p in range(m) for q in range(m) if p == q or p // 2 == q // 2 or not ORTH[D[p // 2]][D[q // 2]]] + P = np.array([f[0] for f in fixed]); Q = np.array([f[1] for f in fixed]); T = np.array([f[2] for f in fixed]) + subsets = [tuple(i for i in range(g) if x >> i & 1) for x in range(1, 1 << g)] + if g >= 5: # keep the type list tractable: small sides, the whole group, and complements of single planes + full = tuple(range(g)); co = [tuple(j for j in range(g) if j != i) for i in range(g)] + subsets = [S for S in subsets if len(S) <= 2] + [full] + co + types = [(A, R, tar([D[i] for i in A], [D[i] for i in R])) for A in subsets for R in subsets] + types = [t for t in types if t[2] > 0] * COPIES + K = len(types) + L('start: %d term slots (%d types x %d copies), %d fixed mask cells, %d starts' % (K, K // COPIES, COPIES, len(fixed), starts)) + MU = np.array([[1.0 if p // 2 in A else 0.0 for p in range(m)] for A, R, c in types]) + MV = np.array([[1.0 if p // 2 in R else 0.0 for p in range(m)] for A, R, c in types]) + cost = np.array([c for A, R, c in types], dtype=float) + def unpack(x): return x[:K*m].reshape(K, m) * MU, x[K*m:].reshape(K, m) * MV + def f(x, lam): + U, V = unpack(x); M = U.T @ V; r = M[P, Q] - T + nu = (U * U).sum(1); nv = (V * V).sum(1); w = np.sqrt(nu * nv + 1e-8) + val = (r * r).sum() + lam * (cost * w).sum() + GM = np.zeros((m, m)); np.add.at(GM, (P, Q), 2 * r) + gU = (V @ GM.T) + lam * (cost * nv / w)[:, None] * U + gV = (U @ GM) + lam * (cost * nu / w)[:, None] * V + return val, np.concatenate([(gU * MU).ravel(), (gV * MV).ravel()]) + def refit(active): + idx = np.array(active); Ka = len(idx) + def res(y): + U = y[:Ka*m].reshape(Ka, m) * MU[idx]; V = y[Ka*m:].reshape(Ka, m) * MV[idx] + return (U.T @ V)[P, Q] - T + return res, Ka + best = None + for s in range(starts): + x = rng.normal(scale=0.7, size=2 * K * m) + for lam in (0.0, 0.001, 0.003, 0.01, 0.02, 0.05): + x = so.minimize(f, x, args=(lam,), jac=True, method='L-BFGS-B', options={'maxiter': 3000}).x + U, V = unpack(x); wts = np.sqrt((U * U).sum(1) * (V * V).sum(1)) + resid = float(np.abs((U.T @ V)[P, Q] - T).max()) + order = [k for k in np.argsort(-wts) if wts[k] > 1e-6] + # smallest prefix (by weight) whose exact refit works; try a few prefix sizes + for n_keep in range(4, len(order) + 1): + active = order[:n_keep] + if sum(cost[k] for k in active) >= (best[0] if best else 1e9): break + res, Ka = refit(active) + y0 = np.concatenate([U[active].ravel(), V[active].ravel()]) + try: + r = so.least_squares(res, y0, method='trf', max_nfev=1500) + except (np.linalg.LinAlgError, ValueError) as e: # e.g. "SVD did not converge" on a degenerate refit + L('start %d: refit of %d terms failed (%s), skipping prefix' % (s + 1, Ka, e)); continue + if np.abs(r.fun).max() < 1e-9: + Ua = r.x[:Ka*m].reshape(Ka, m) * MU[active]; Va = r.x[Ka*m:].reshape(Ka, m) * MV[active] + true = 0 + for k in range(Ka): + A = tuple(sorted({p // 2 for p in range(m) if abs(Ua[k, p]) > 1e-9})); R = tuple(sorted({p // 2 for p in range(m) if abs(Va[k, p]) > 1e-9})) + true += tar([D[i] for i in A], [D[i] for i in R]) + improved = best is None or true < best[0] + if improved: + best = (true, [(types[k][0], types[k][1]) for k in active]) + L('start %d: exact decoder with %d terms, nominal %d, true cost %d%s' % (s + 1, Ka, int(sum(cost[k] for k in active)), true, ' NEW BEST' if improved else '')) + break + else: + L('start %d: no exact refit (max residual after relaxation %.2e, nonzero terms %d)' % (s + 1, resid, len(order))) + L('done: best exact real decoder cost', best[0] if best else None) + return best + +def _run(a): + D, st, sd = a + return D, search(D, st, sd) + +def open_triples(): + """one example per open class of research/three-plane-rank-dual (classes without an all-field certificate)""" + return [tuple(c['example']) for c in json.loads(TRI.read_text())['classes'] if 'f2_minimum_mass' in c] + +def open_quads(): + idx = gzip.decompress(QUAD.read_bytes()) + return [q for n, q in enumerate(itertools.combinations(range(NP), 4)) if (idx[2 * n] | idx[2 * n + 1] << 8) == 0] + +def degenerate_quads(n): + """the n quadruples with the smallest whole-group tariff t(D, D), ties broken by more non-orthogonal pairs""" + cand = [(tar(D, D), -sum(not ORTH[a][b] for a, b in itertools.combinations(D, 2)), D) + for D in itertools.combinations(range(NP), 4)] + return [D for _, _, D in sorted(cand)[:n]] + +def c5_groups(): + """the induced 5-cycles of the non-orthogonality graph, each also extended by its 1 and 2 most degenerate planes""" + non = [[i != j and not ORTH[i][j] for j in range(NP)] for i in range(NP)] + holes = sorted(S for S in itertools.combinations(range(NP), 5) if all(sum(non[a][b] for b in S) == 2 for a in S)) + out = [] + for H in holes: + out.append(H); cur = list(H) + for _ in range(2): + best = min((x for x in range(NP) if x not in cur), key=lambda x: (tar(cur + [x], cur + [x]), x)) + cur = cur + [best]; out.append(tuple(cur)) + return holes, out + +if __name__ == '__main__': + mode = sys.argv[1] + if mode == 'triples-open': + groups, starts = open_triples(), int(sys.argv[2]) + elif mode == 'quads-open': + n, starts, seed = int(sys.argv[2]), int(sys.argv[3]), int(sys.argv[4]) + oq = open_quads(); print('open quadruples', len(oq), flush=True) + groups = random.Random(seed).sample(oq, n) + elif mode == 'quads-degenerate': + groups, starts = degenerate_quads(int(sys.argv[2])), int(sys.argv[3]) + elif mode == 'c5': + holes, groups = c5_groups(); starts = int(sys.argv[2]); print('induced C5s', len(holes), 'groups', len(groups), flush=True) + else: + groups = [tuple(int(x) for x in g.split(',')) for g in sys.argv[2].split(';')]; starts = int(sys.argv[3]) + t0 = time.time() + with mp.get_context('spawn').Pool(4) as pool: + for D, best in pool.imap_unordered(_run, [(D, starts, i) for i, D in enumerate(groups)]): + base = 4 * len(D); tag = 'ESCAPE' if best and best[0] < base else 'no escape' + print('RESULT group', D, 'baseline', base, 'best exact real decoder cost', best[0] if best else None, '->', tag, + '%.0fs' % (time.time() - t0), flush=True) + if best and best[0] < base: print(' terms:', best[1], flush=True) diff --git a/research/plane-port-global-rank-dual/search/results/c5-run1.txt b/research/plane-port-global-rank-dual/search/results/c5-run1.txt new file mode 100644 index 0000000000..918434b995 --- /dev/null +++ b/research/plane-port-global-rank-dual/search/results/c5-run1.txt @@ -0,0 +1,50 @@ +# Kaggle v4-real-c5 run 1 (69 groups, 15 starts, 2026-10-25): 49 of 69 finished, no escape; stopped on an SVD error in a refit; the other 20 are in c5-run2.txt +group (3, 6, 7, 10, 13) size 5 baseline 20 best exact real decoder cost 24 -> no escape 236s +group (3, 4, 6, 10, 13) size 5 baseline 20 best exact real decoder cost 22 -> no escape 245s +group (3, 4, 6, 10, 13, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 262s +group (3, 6, 7, 10, 13, 1) size 6 baseline 24 best exact real decoder cost 26 -> no escape 483s +group (3, 7, 10, 38, 44) size 5 baseline 20 best exact real decoder cost 24 -> no escape 485s +group (3, 4, 6, 10, 13, 0, 1) size 7 baseline 28 best exact real decoder cost 32 -> no escape 592s +group (3, 7, 10, 38, 44, 1) size 6 baseline 24 best exact real decoder cost 26 -> no escape 749s +group (3, 10, 12, 13, 23) size 5 baseline 20 best exact real decoder cost 24 -> no escape 829s +group (3, 6, 7, 10, 13, 1, 14) size 7 baseline 28 best exact real decoder cost 28 -> no escape 843s +group (3, 10, 12, 13, 23, 0) size 6 baseline 24 best exact real decoder cost 24 -> no escape 1007s +group (3, 7, 10, 38, 44, 1, 8) size 7 baseline 28 best exact real decoder cost 32 -> no escape 1048s +group (3, 10, 13, 16, 34) size 5 baseline 20 best exact real decoder cost 26 -> no escape 1095s +group (3, 10, 13, 16, 34, 0) size 6 baseline 24 best exact real decoder cost 28 -> no escape 1289s +group (3, 10, 13, 30, 34) size 5 baseline 20 best exact real decoder cost 20 -> no escape 1348s +group (3, 10, 12, 13, 23, 0, 1) size 7 baseline 28 best exact real decoder cost 34 -> no escape 1400s +group (3, 10, 13, 30, 34, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 1574s +group (3, 10, 14, 18, 55) size 5 baseline 20 best exact real decoder cost 24 -> no escape 1614s +group (3, 10, 13, 16, 34, 0, 1) size 7 baseline 28 best exact real decoder cost 30 -> no escape 1623s +group (3, 10, 14, 18, 55, 11) size 6 baseline 24 best exact real decoder cost 32 -> no escape 1844s +group (3, 10, 18, 24, 47) size 5 baseline 20 best exact real decoder cost 20 -> no escape 1867s +group (3, 10, 13, 30, 34, 0, 1) size 7 baseline 28 best exact real decoder cost 34 -> no escape 1963s +group (3, 10, 18, 24, 47, 0) size 6 baseline 24 best exact real decoder cost 28 -> no escape 2121s +group (3, 10, 14, 18, 55, 11, 12) size 7 baseline 28 best exact real decoder cost 34 -> no escape 2157s +group (3, 13, 18, 22, 55) size 5 baseline 20 best exact real decoder cost 22 -> no escape 2183s +group (3, 13, 18, 22, 55, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 2364s +group (4, 6, 12, 13, 23) size 5 baseline 20 best exact real decoder cost 24 -> no escape 2395s +group (3, 10, 18, 24, 47, 0, 1) size 7 baseline 28 best exact real decoder cost 38 -> no escape 2445s +group (4, 6, 12, 13, 23, 2) size 6 baseline 24 best exact real decoder cost 26 -> no escape 2616s +group (4, 7, 12, 21, 44) size 5 baseline 20 best exact real decoder cost 20 -> no escape 2692s +group (3, 13, 18, 22, 55, 0, 2) size 7 baseline 28 best exact real decoder cost 32 -> no escape 2750s +group (4, 7, 12, 21, 44, 0) size 6 baseline 24 best exact real decoder cost 24 -> no escape 2904s +group (4, 6, 12, 13, 23, 2, 26) size 7 baseline 28 best exact real decoder cost 32 -> no escape 2940s +group (6, 7, 13, 22, 49) size 5 baseline 20 best exact real decoder cost 22 -> no escape 2991s +group (6, 7, 13, 22, 49, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 3181s +group (6, 13, 22, 26, 49) size 5 baseline 20 best exact real decoder cost 24 -> no escape 3222s +group (4, 7, 12, 21, 44, 0, 1) size 7 baseline 28 best exact real decoder cost 30 -> no escape 3309s +group (6, 13, 22, 26, 49, 0) size 6 baseline 24 best exact real decoder cost 28 -> no escape 3463s +group (6, 7, 13, 22, 49, 0, 1) size 7 baseline 28 best exact real decoder cost 30 -> no escape 3551s +group (6, 13, 23, 26, 54) size 5 baseline 20 best exact real decoder cost 24 -> no escape 3552s +group (6, 13, 23, 26, 54, 11) size 6 baseline 24 best exact real decoder cost 24 -> no escape 3707s +group (6, 13, 26, 34, 54) size 5 baseline 20 best exact real decoder cost 20 -> no escape 3777s +group (6, 13, 22, 26, 49, 0, 1) size 7 baseline 28 best exact real decoder cost 28 -> no escape 3821s +group (6, 13, 26, 34, 54, 5) size 6 baseline 24 best exact real decoder cost 24 -> no escape 3970s +group (7, 10, 12, 21, 44) size 5 baseline 20 best exact real decoder cost 22 -> no escape 4062s +group (6, 13, 23, 26, 54, 11, 14) size 7 baseline 28 best exact real decoder cost 32 -> no escape 4119s +group (7, 10, 12, 21, 44, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 4245s +group (6, 13, 26, 34, 54, 5, 12) size 7 baseline 28 best exact real decoder cost 30 -> no escape 4344s +group (7, 10, 24, 43, 47) size 5 baseline 20 best exact real decoder cost 20 -> no escape 4362s +group (7, 10, 24, 43, 47, 0) size 6 baseline 24 best exact real decoder cost 28 -> no escape 4530s diff --git a/research/plane-port-global-rank-dual/search/results/c5-run2.txt b/research/plane-port-global-rank-dual/search/results/c5-run2.txt new file mode 100644 index 0000000000..840662c687 --- /dev/null +++ b/research/plane-port-global-rank-dual/search/results/c5-run2.txt @@ -0,0 +1,21 @@ +# Kaggle v4-real-c5-2 (remaining 20 of 69 groups, 15 starts, SVD-safe refit, 2026-10-25): no escape +group (10, 12, 16, 23, 35) size 5 baseline 20 best exact real decoder cost 24 -> no escape 299s +group (10, 12, 16, 23, 35, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 330s +group (10, 12, 16, 23, 54) size 5 baseline 20 best exact real decoder cost 20 -> no escape 643s +group (7, 10, 12, 21, 44, 0, 1) size 7 baseline 28 best exact real decoder cost 28 -> no escape 734s +group (7, 10, 24, 43, 47, 0, 1) size 7 baseline 28 best exact real decoder cost 32 -> no escape 775s +group (10, 12, 16, 23, 54, 0) size 6 baseline 24 best exact real decoder cost 26 -> no escape 965s +group (10, 12, 16, 23, 35, 0, 1) size 7 baseline 28 best exact real decoder cost 34 -> no escape 1024s +group (10, 14, 28, 31, 39) size 5 baseline 20 best exact real decoder cost 24 -> no escape 1069s +group (10, 14, 28, 31, 39, 0) size 6 baseline 24 best exact real decoder cost 24 -> no escape 1301s +group (13, 16, 23, 34, 35) size 5 baseline 20 best exact real decoder cost 22 -> no escape 1348s +group (10, 12, 16, 23, 54, 0, 1) size 7 baseline 28 best exact real decoder cost 34 -> no escape 1446s +group (13, 16, 23, 34, 35, 6) size 6 baseline 24 best exact real decoder cost 26 -> no escape 1618s +group (10, 14, 28, 31, 39, 0, 1) size 7 baseline 28 best exact real decoder cost 32 -> no escape 1751s +group (14, 18, 24, 47, 55) size 5 baseline 20 best exact real decoder cost 28 -> no escape 1769s +group (14, 18, 24, 47, 55, 0) size 6 baseline 24 best exact real decoder cost 28 -> no escape 1985s +group (13, 16, 23, 34, 35, 6, 15) size 7 baseline 28 best exact real decoder cost 34 -> no escape 2051s +group (14, 24, 28, 30, 33) size 5 baseline 20 best exact real decoder cost 26 -> no escape 2067s +group (14, 24, 28, 30, 33, 2) size 6 baseline 24 best exact real decoder cost 26 -> no escape 2273s +group (14, 18, 24, 47, 55, 0, 1) size 7 baseline 28 best exact real decoder cost 30 -> no escape 2426s +group (14, 24, 28, 30, 33, 2, 3) size 7 baseline 28 best exact real decoder cost 32 -> no escape 2548s diff --git a/research/plane-port-global-rank-dual/search/results/quads-degenerate-60.txt b/research/plane-port-global-rank-dual/search/results/quads-degenerate-60.txt new file mode 100644 index 0000000000..992bf3d1ce --- /dev/null +++ b/research/plane-port-global-rank-dual/search/results/quads-degenerate-60.txt @@ -0,0 +1,61 @@ +# Kaggle v4-real-quads (60 most degenerate quadruples, 30 starts, 2026-10-25): no escape below 16 +quad (14, 19, 32, 46) best exact real decoder cost 16 -> no escape 199s +quad (19, 21, 25, 32) best exact real decoder cost 16 -> no escape 199s +quad (11, 19, 32, 43) best exact real decoder cost 16 -> no escape 239s +quad (11, 21, 28, 43) best exact real decoder cost 16 -> no escape 314s +quad (35, 36, 45, 47) best exact real decoder cost 16 -> no escape 376s +quad (19, 23, 42, 51) best exact real decoder cost 18 -> no escape 377s +quad (44, 51, 52, 55) best exact real decoder cost 18 -> no escape 445s +quad (49, 53, 54, 55) best exact real decoder cost 18 -> no escape 499s +quad (0, 3, 24, 32) best exact real decoder cost 16 -> no escape 533s +quad (0, 3, 27, 32) best exact real decoder cost 20 -> no escape 550s +quad (0, 6, 42, 47) best exact real decoder cost 16 -> no escape 605s +quad (0, 8, 16, 50) best exact real decoder cost 16 -> no escape 662s +quad (0, 8, 18, 52) best exact real decoder cost 18 -> no escape 702s +quad (0, 12, 19, 44) best exact real decoder cost 16 -> no escape 714s +quad (0, 12, 20, 43) best exact real decoder cost 18 -> no escape 774s +quad (0, 17, 23, 32) best exact real decoder cost 18 -> no escape 848s +quad (0, 27, 32, 40) best exact real decoder cost 16 -> no escape 872s +quad (0, 31, 42, 47) best exact real decoder cost 16 -> no escape 873s +quad (0, 36, 39, 46) best exact real decoder cost 16 -> no escape 950s +quad (0, 40, 47, 55) best exact real decoder cost 16 -> no escape 1014s +quad (1, 3, 29, 52) best exact real decoder cost 16 -> no escape 1054s +quad (0, 41, 45, 51) best exact real decoder cost 16 -> no escape 1054s +quad (1, 4, 11, 50) best exact real decoder cost 18 -> no escape 1134s +quad (1, 4, 11, 51) best exact real decoder cost 16 -> no escape 1206s +quad (1, 4, 11, 52) best exact real decoder cost 16 -> no escape 1232s +quad (1, 4, 43, 51) best exact real decoder cost 16 -> no escape 1233s +quad (1, 4, 43, 53) best exact real decoder cost 16 -> no escape 1328s +quad (1, 4, 51, 52) best exact real decoder cost 18 -> no escape 1383s +quad (1, 4, 51, 53) best exact real decoder cost 16 -> no escape 1408s +quad (1, 11, 19, 43) best exact real decoder cost 16 -> no escape 1435s +quad (1, 11, 33, 53) best exact real decoder cost 16 -> no escape 1500s +quad (1, 11, 51, 52) best exact real decoder cost 18 -> no escape 1550s +quad (1, 13, 14, 18) best exact real decoder cost 18 -> no escape 1578s +quad (1, 13, 14, 53) best exact real decoder cost 16 -> no escape 1647s +quad (1, 15, 20, 42) best exact real decoder cost 16 -> no escape 1696s +quad (1, 16, 18, 42) best exact real decoder cost 16 -> no escape 1731s +quad (1, 16, 22, 39) best exact real decoder cost 16 -> no escape 1765s +quad (1, 20, 31, 45) best exact real decoder cost 16 -> no escape 1801s +quad (1, 22, 34, 39) best exact real decoder cost 18 -> no escape 1915s +quad (1, 25, 29, 53) best exact real decoder cost 18 -> no escape 1920s +quad (1, 28, 44, 53) best exact real decoder cost 16 -> no escape 1940s +quad (1, 30, 35, 53) best exact real decoder cost 16 -> no escape 1974s +quad (1, 33, 45, 46) best exact real decoder cost 16 -> no escape 2073s +quad (1, 34, 39, 53) best exact real decoder cost 16 -> no escape 2112s +quad (1, 35, 47, 53) best exact real decoder cost 18 -> no escape 2119s +quad (1, 43, 51, 53) best exact real decoder cost 18 -> no escape 2162s +quad (2, 3, 26, 48) best exact real decoder cost 16 -> no escape 2235s +quad (2, 3, 48, 51) best exact real decoder cost 16 -> no escape 2274s +quad (2, 4, 11, 50) best exact real decoder cost 16 -> no escape 2297s +quad (2, 4, 11, 51) best exact real decoder cost 16 -> no escape 2341s +quad (2, 4, 11, 52) best exact real decoder cost 16 -> no escape 2419s +quad (2, 4, 50, 51) best exact real decoder cost 16 -> no escape 2437s +quad (2, 9, 21, 49) best exact real decoder cost 16 -> no escape 2454s +quad (2, 11, 26, 43) best exact real decoder cost 16 -> no escape 2516s +quad (2, 11, 43, 50) best exact real decoder cost 16 -> no escape 2596s +quad (2, 11, 50, 51) best exact real decoder cost 16 -> no escape 2613s +quad (2, 11, 43, 52) best exact real decoder cost 16 -> no escape 2617s +quad (2, 12, 15, 17) best exact real decoder cost 16 -> no escape 2681s +quad (2, 16, 21, 45) best exact real decoder cost 16 -> no escape 2737s +quad (2, 12, 15, 43) best exact real decoder cost 18 -> no escape 2737s diff --git a/research/plane-port-global-rank-dual/search/results/quads-open-40.txt b/research/plane-port-global-rank-dual/search/results/quads-open-40.txt new file mode 100644 index 0000000000..6a7362e8b6 --- /dev/null +++ b/research/plane-port-global-rank-dual/search/results/quads-open-40.txt @@ -0,0 +1,41 @@ +# Kaggle v4-pr-verify (2026-10-25): 40 random open quadruples of four-plane-rank-dual (seed 2026), 30 starts, strict mask: no escape +group (18, 21, 29, 31) baseline 16 best exact real decoder cost 16 -> no escape +group (10, 16, 18, 42) baseline 16 best exact real decoder cost 16 -> no escape +group (18, 35, 47, 54) baseline 16 best exact real decoder cost 20 -> no escape +group (3, 13, 30, 41) baseline 16 best exact real decoder cost 18 -> no escape +group (6, 28, 33, 36) baseline 16 best exact real decoder cost 16 -> no escape +group (2, 29, 39, 47) baseline 16 best exact real decoder cost 16 -> no escape +group (24, 33, 35, 47) baseline 16 best exact real decoder cost 18 -> no escape +group (30, 34, 44, 45) baseline 16 best exact real decoder cost 16 -> no escape +group (21, 25, 38, 41) baseline 16 best exact real decoder cost 16 -> no escape +group (26, 32, 37, 49) baseline 16 best exact real decoder cost 18 -> no escape +group (22, 37, 44, 53) baseline 16 best exact real decoder cost 16 -> no escape +group (14, 26, 32, 51) baseline 16 best exact real decoder cost 18 -> no escape +group (20, 25, 27, 45) baseline 16 best exact real decoder cost 16 -> no escape +group (23, 34, 35, 37) baseline 16 best exact real decoder cost 16 -> no escape +group (17, 27, 40, 42) baseline 16 best exact real decoder cost 16 -> no escape +group (15, 22, 31, 34) baseline 16 best exact real decoder cost 16 -> no escape +group (7, 13, 44, 55) baseline 16 best exact real decoder cost 16 -> no escape +group (0, 1, 16, 19) baseline 16 best exact real decoder cost 18 -> no escape +group (2, 6, 28, 31) baseline 16 best exact real decoder cost 16 -> no escape +group (25, 35, 50, 54) baseline 16 best exact real decoder cost 16 -> no escape +group (3, 6, 14, 26) baseline 16 best exact real decoder cost 16 -> no escape +group (9, 10, 21, 24) baseline 16 best exact real decoder cost 18 -> no escape +group (15, 30, 31, 37) baseline 16 best exact real decoder cost 16 -> no escape +group (2, 25, 37, 41) baseline 16 best exact real decoder cost 16 -> no escape +group (0, 2, 39, 43) baseline 16 best exact real decoder cost 18 -> no escape +group (10, 13, 23, 48) baseline 16 best exact real decoder cost 16 -> no escape +group (43, 44, 49, 51) baseline 16 best exact real decoder cost 16 -> no escape +group (17, 27, 29, 40) baseline 16 best exact real decoder cost 18 -> no escape +group (6, 14, 54, 55) baseline 16 best exact real decoder cost 16 -> no escape +group (12, 13, 21, 53) baseline 16 best exact real decoder cost 16 -> no escape +group (7, 21, 32, 49) baseline 16 best exact real decoder cost 16 -> no escape +group (12, 16, 23, 44) baseline 16 best exact real decoder cost 18 -> no escape +group (13, 14, 34, 35) baseline 16 best exact real decoder cost 16 -> no escape +group (18, 42, 47, 50) baseline 16 best exact real decoder cost 16 -> no escape +group (28, 35, 40, 43) baseline 16 best exact real decoder cost 16 -> no escape +group (1, 42, 43, 44) baseline 16 best exact real decoder cost 16 -> no escape +group (11, 23, 37, 53) baseline 16 best exact real decoder cost 16 -> no escape +group (21, 27, 32, 37) baseline 16 best exact real decoder cost 16 -> no escape +group (2, 12, 48, 54) baseline 16 best exact real decoder cost 16 -> no escape +group (13, 23, 43, 53) baseline 16 best exact real decoder cost 16 -> no escape diff --git a/research/plane-port-global-rank-dual/search/results/triples-open.txt b/research/plane-port-global-rank-dual/search/results/triples-open.txt new file mode 100644 index 0000000000..ea362c2ba8 --- /dev/null +++ b/research/plane-port-global-rank-dual/search/results/triples-open.txt @@ -0,0 +1,7 @@ +# local run 2026-10-25 (Windows, 4 processes): one example per open class of three-plane-rank-dual, 40 starts: no escape +group (0, 12, 29) baseline 12 best exact real decoder cost 12 -> no escape +group (0, 7, 46) baseline 12 best exact real decoder cost 12 -> no escape +group (0, 12, 19) baseline 12 best exact real decoder cost 12 -> no escape +group (2, 35, 47) baseline 12 best exact real decoder cost 12 -> no escape +group (0, 19, 46) baseline 12 best exact real decoder cost 12 -> no escape +group (0, 12, 15) baseline 12 best exact real decoder cost 12 -> no escape diff --git a/research/plane-port-global-rank-dual/verify.py b/research/plane-port-global-rank-dual/verify.py new file mode 100644 index 0000000000..19cdcb405c --- /dev/null +++ b/research/plane-port-global-rank-dual/verify.py @@ -0,0 +1,229 @@ +#!/usr/bin/env python3 +"""Exact replay of the global rank-dual certificate for the 56-plane port decoder. + +Checks, from the pinned selected archive and the retained PR1825 matching: + +1. the 56 matched planes and their pairwise orthogonality; +2. every subspace of F2^9 generated by a nonempty set of planes (closure census); +3. the binary pairing tariff t(A, R) = dim A - dim(A meet R^perp) for ordered pairs of such + subspaces, cross-checked against direct Gaussian elimination on 20,000 random pairs; +4. that every certificate column is a clique of pairwise non-orthogonal planes with a positive + integer weight; +5. feasibility: for every ordered pair (A, R) of generated subspaces, + sum_{Q : A meets Q and R meets Q} w_Q <= SCALE * t(A, R), + where "A meets Q" means some plane of Q lies inside A; +6. the bound sum_Q w_Q * 2|Q| / SCALE = 18233853/131072; +7. rejecting controls: a perturbed certificate, a non-clique column and a wrong recorded bound + must each fail. + +Step 5 sums are integers below 2^30, so the float64 matrix product used for them is exact +(asserted). Needs numpy >= 2 (np.bitwise_count). + +Default (bounded, for CI): steps 1-4, 6, 7 in full and step 5 on every 97th row (403 rows x all +39,087 columns). `--full`: step 5 on all 39,087^2 ordered pairs (about 7 minutes on 4 cores); +the receipt is written to FULL-CHECK.json. `--rows a:b`: step 5 on rows a..b-1. +""" +import argparse, hashlib, json, random, tarfile, time +from fractions import Fraction +from pathlib import Path +import numpy as np + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +ARCHIVE = ROOT / 'research/community-frontier1094-audit/selected-replay.tar.gz' +ARCHIVE_SHA = 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6' +MEMBER = 'candidate/strict/global/base/work/complex-nine-native/DATA-PHASES.json' +MATCHING = ROOT / 'research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json' +MATCHING_SHA = '4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1' +T0 = time.time() + + +def log(*a): + print('%6.0fs' % (time.time() - T0), *a, flush=True) + + +class Fail(Exception): + pass + + +def need(c, msg): + if not c: + raise Fail(msg) + + +def sha(p): + return hashlib.sha256(p.read_bytes()).hexdigest() + + +def dot(x, y): + return bin(x & y).count('1') & 1 + + +def gauss_rank(rows): + """rank over F2 of a list of int bit-rows""" + rows = [r for r in rows if r]; rank = 0 + while rows: + piv = max(rows); top = piv.bit_length() - 1; rank += 1 + rows = [r ^ piv if r >> top & 1 else r for r in rows if r != piv] + rows = [r for r in rows if r] + return rank + + +def basis_of(elems): + b = [] + for x in elems: + for y in b: + x = min(x, x ^ y) + if x: + b.append(x) + return b + + +def geometry(): + need(sha(ARCHIVE) == ARCHIVE_SHA, 'archive hash') + need(sha(MATCHING) == MATCHING_SHA, 'matching hash') + with tarfile.open(ARCHIVE) as a: + labels = [r['q'] for r in json.loads(a.extractfile(a.getmember(MEMBER)).read())['recipes']] + matching = json.loads(MATCHING.read_text())['matching'] + need(len(labels) == 112 and len(matching) == 56, 'sizes') + need(sorted(p for e in matching for p in e) == list(range(112)), 'matching is perfect') + planes = [(labels[a], labels[b]) for a, b in matching] + pel = [{0, x, y, x ^ y} for x, y in planes] + need(all(len(e) == 4 for e in pel), 'planes are 2-dimensional') + need(all(gauss_rank([sum(dot(x, y) << k for k, y in enumerate(p)) for x in p]) == 2 for p in planes), + 'every plane is nondegenerate') + orth = [[i != j and all(dot(x, y) == 0 for x in pel[i] for y in pel[j]) for j in range(56)] for i in range(56)] + return planes, pel, orth + + +def census(planes): + """all subspaces generated by nonempty plane sets, as 512-entry element indicators""" + idx = np.arange(512) + frontier = {} + for x, y in planes: + m = np.zeros(512, bool); m[[0, x, y, x ^ y]] = True; frontier[m.tobytes()] = m + seen = dict(frontier) + while frontier: + F = np.array(list(frontier.values())); new = {} + for x, y in planes: + G = F | F[:, idx ^ x] | F[:, idx ^ y] | F[:, idx ^ x ^ y] + for g in G: + k = g.tobytes() + if k not in seen: + seen[k] = g; new[k] = g + frontier = new + return np.array(sorted(seen.values(), key=lambda m: (m.sum(), m.tobytes()))) + + +def check_certificate(cert, orth, inside, tariff_rows, n, rows, block): + SCALE = cert['scale']; cols = cert['columns'] + need(isinstance(SCALE, int) and SCALE > 0, 'scale') + for c in cols: + Q = c['clique'] + need(len(set(Q)) == len(Q) and all(0 <= i < 56 for i in Q), 'clique indices') + need(all(not orth[i][j] for i in Q for j in Q if i != j), 'column is a clique of non-orthogonal planes') + need(isinstance(c['w'], int) and c['w'] > 0, 'positive integer weight') + w = np.array([c['w'] for c in cols], dtype=np.int64) + need(int(w.sum()) < 2 ** 50, 'exact float64 range') + qm = np.zeros((len(cols), 56), bool) + for k, c in enumerate(cols): + qm[k, c['clique']] = True + touch = (inside.astype(np.int32) @ qm.T.astype(np.int32)) > 0 # span a meets clique k + Tf = touch.astype(np.float64); TW = (Tf * w.astype(np.float64)).T.copy() + worst = None; tight = 0 + for b0 in range(0, len(rows), block): + rs = np.array(rows[b0:b0 + block]) + slack = tariff_rows(rs) * SCALE - np.rint(Tf[rs] @ TW).astype(np.int64) + m = int(slack.min()); worst = m if worst is None else min(worst, m); tight += int((slack == 0).sum()) + need(m >= 0, 'feasibility violated near row %d' % int(rs[0])) + if b0 // block % 50 == 0 and len(rows) > 1000: + log('rows', b0 + len(rs), '/', len(rows), 'min slack', worst) + LB = Fraction(sum(c['w'] * 2 * len(c['clique']) for c in cols), SCALE) + need(LB == Fraction(cert['lower_bound_num'], cert['lower_bound_den']), 'recorded bound') + return LB, worst, tight, int(qm.sum(1).max()) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--rows', default=None) + ap.add_argument('--full', action='store_true') + ap.add_argument('--block', type=int, default=64) + args = ap.parse_args() + + planes, pel, orth = geometry() + log('56 nondegenerate planes; orthogonal plane pairs', sum(map(sum, orth)) // 2) + S = census(planes); n = len(S); size = S.sum(1) + need(all(int(s) & (int(s) - 1) == 0 for s in size), 'closures are subspaces') + dim = np.log2(size).round().astype(np.int64) + log('generated subspaces', n, 'by dimension', {int(k): int(v) for k, v in zip(*np.unique(dim, return_counts=True))}) + need(n == 39087, 'census size') + pmask = np.zeros((56, 512), bool) + for i, e in enumerate(pel): + pmask[i, list(e)] = True + inside = (S.astype(np.int32) @ pmask.T.astype(np.int32)) == 4 # plane i lies inside span a + + Dm = np.array([[dot(x, y) for y in range(512)] for x in range(512)], dtype=np.float32) + perp = (S.astype(np.float32) @ Dm) == 0 + Sp = np.packbits(S, axis=1, bitorder='little').view(np.uint64) + Pp = np.packbits(perp, axis=1, bitorder='little').view(np.uint64) + + def tariff_rows(rs): + cnt = np.bitwise_count(Sp[rs][:, None, :] & Pp[None, :, :]).sum(axis=2, dtype=np.int64) + return dim[rs, None] - np.log2(cnt).round().astype(np.int64) + + rng = random.Random(2026) + bases = [basis_of(np.flatnonzero(s).tolist()) for s in S] + need(all(len(b) == d for b, d in zip(bases, dim)), 'basis sizes') + checked = 0 + for a in rng.sample(range(n), 200): + row = tariff_rows(np.array([a]))[0] + for r in rng.sample(range(n), 100): + direct = gauss_rank([sum(dot(x, y) << k for k, y in enumerate(bases[r])) for x in bases[a]]) + need(int(row[r]) == direct, 'tariff formula vs Gaussian elimination') + checked += 1 + log('tariff formula matches Gaussian elimination on', checked, 'random pairs') + + if args.full: + rows = list(range(n)) + elif args.rows: + lo, hi = map(int, args.rows.split(':')); rows = list(range(lo, hi)) + else: + rows = list(range(0, n, 97)) + cert = json.loads((HERE / 'CERTIFICATE.json').read_text()) + LB, worst, tight, maxq = check_certificate(cert, orth, inside, tariff_rows, n, rows, args.block) + log('certificate PASSED on', len(rows), 'rows x', n, 'columns | min slack', worst, '| tight pairs', tight) + + # rejecting controls (on a small row set containing a tight pair) + ctrl_rows = rows[:64] + bad = json.loads(json.dumps(cert)) + bad['columns'][0]['w'] += cert['scale'] * 9 # cannot fit under any tariff <= 9 + bad['lower_bound_num'], bad['lower_bound_den'] = (Fraction(sum(c['w'] * 2 * len(c['clique']) for c in bad['columns']), + bad['scale'])).as_integer_ratio() + nonclique = json.loads(json.dumps(cert)) + i, j = next((i, j) for i in range(56) for j in range(56) if orth[i][j]) + nonclique['columns'][0]['clique'] = [i, j] + wrong = json.loads(json.dumps(cert)); wrong['lower_bound_num'] += 1 + for name, c in [('overweight column', bad), ('orthogonal pair as clique', nonclique), ('wrong recorded bound', wrong)]: + try: + check_certificate(c, orth, inside, tariff_rows, n, ctrl_rows, args.block) + except Fail: + log('control rejected:', name) + else: + raise SystemExit('FAILED: control accepted: ' + name) + + full = len(rows) == n + res = {'schema': 'plane-port-global-rank-dual/verify/1', 'planes': 56, 'generated_subspaces': n, + 'ordered_pairs_checked': len(rows) * n, 'complete': full, 'columns': len(cert['columns']), + 'max_clique': maxq, 'scale': cert['scale'], 'min_slack': worst, 'tight_pairs': tight, + 'lower_bound': str(LB), 'lower_bound_float': float(LB), 'new_kappa_claimed': False} + print(json.dumps(res, indent=1)) + if full: + (HERE / 'FULL-CHECK.json').write_text(json.dumps(res, indent=1) + '\n') + print('PASS_PLANE_PORT_GLOBAL_RANK_DUAL' + ('_FULL' if full else '_SAMPLED')) + + +if __name__ == '__main__': + try: + main() + except Fail as e: + raise SystemExit('FAILED: %s' % e)