From 2e29f0628e7dd3b99a4577f3f46880858d5dd096 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 19:11:53 +0000 Subject: [PATCH] feat(research): raise the all-field plane-port decoder floor to 141 A new 425-clique point of PR5560's clique programme certifies 36732955/262144 > 140. It is checked exactly on all 39,087^2 ordered span pairs. --- .../CERTIFICATE.json | 427 ++++++++++++++++++ .../plane-port-clique-floor-141/README.md | 110 +++++ .../plane-port-clique-floor-141/SOURCES.json | 36 ++ .../plane-port-clique-floor-141/TASK.json | 87 ++++ .../plane-port-clique-floor-141/VERIFY.json | 24 + .../generate/colgen.py | 143 ++++++ .../generate/geom.py | 65 +++ .../generate/roundcert.py | 37 ++ .../plane-port-clique-floor-141/verify.py | 245 ++++++++++ 9 files changed, 1174 insertions(+) create mode 100644 research/plane-port-clique-floor-141/CERTIFICATE.json create mode 100644 research/plane-port-clique-floor-141/README.md create mode 100644 research/plane-port-clique-floor-141/SOURCES.json create mode 100644 research/plane-port-clique-floor-141/TASK.json create mode 100644 research/plane-port-clique-floor-141/VERIFY.json create mode 100644 research/plane-port-clique-floor-141/generate/colgen.py create mode 100644 research/plane-port-clique-floor-141/generate/geom.py create mode 100644 research/plane-port-clique-floor-141/generate/roundcert.py create mode 100644 research/plane-port-clique-floor-141/verify.py diff --git a/research/plane-port-clique-floor-141/CERTIFICATE.json b/research/plane-port-clique-floor-141/CERTIFICATE.json new file mode 100644 index 0000000000..359e938f31 --- /dev/null +++ b/research/plane-port-clique-floor-141/CERTIFICATE.json @@ -0,0 +1,427 @@ +{"schema": "plane-port-clique-floor-141/certificate/1", "scale": 1048576, "lower_bound_num": 36732955, "lower_bound_den": 262144, "columns": [ +{"clique":[7],"w":61705}, +{"clique":[20],"w":38122}, +{"clique":[0,12],"w":160251}, +{"clique":[2,21],"w":16632}, +{"clique":[2,47],"w":21869}, +{"clique":[3,8],"w":37642}, +{"clique":[4,20],"w":9699}, +{"clique":[4,21],"w":30419}, +{"clique":[5,30],"w":4447}, +{"clique":[6,24],"w":3660}, +{"clique":[7,46],"w":30903}, +{"clique":[8,28],"w":10724}, +{"clique":[9,40],"w":58350}, +{"clique":[10,27],"w":115456}, +{"clique":[16,18],"w":4158}, +{"clique":[21,45],"w":50719}, +{"clique":[23,45],"w":11755}, +{"clique":[26,31],"w":105991}, +{"clique":[0,7,46],"w":8206}, +{"clique":[0,12,29],"w":10074}, +{"clique":[0,12,45],"w":17930}, +{"clique":[1,10,45],"w":40239}, +{"clique":[2,7,52],"w":27901}, +{"clique":[2,12,47],"w":5500}, +{"clique":[2,22,25],"w":14307}, +{"clique":[3,8,39],"w":10416}, +{"clique":[3,14,32],"w":9882}, +{"clique":[3,26,39],"w":55543}, +{"clique":[4,11,43],"w":90519}, +{"clique":[5,30,46],"w":1645}, +{"clique":[6,8,28],"w":32970}, +{"clique":[6,20,31],"w":25723}, +{"clique":[6,28,50],"w":2125}, +{"clique":[7,16,18],"w":10161}, +{"clique":[7,20,46],"w":28015}, +{"clique":[7,26,46],"w":21546}, +{"clique":[8,28,29],"w":3050}, +{"clique":[9,21,40],"w":18075}, +{"clique":[9,27,40],"w":26244}, +{"clique":[10,17,27],"w":45317}, +{"clique":[10,20,32],"w":3860}, +{"clique":[10,27,40],"w":9780}, +{"clique":[13,14,32],"w":9284}, +{"clique":[20,34,39],"w":4160}, +{"clique":[25,26,31],"w":13375}, +{"clique":[26,30,31],"w":2331}, +{"clique":[30,50,51],"w":11145}, +{"clique":[0,6,24,46],"w":50092}, +{"clique":[0,10,19,46],"w":4115}, +{"clique":[0,10,27,46],"w":667}, +{"clique":[0,12,16,45],"w":4791}, +{"clique":[0,12,28,29],"w":5331}, +{"clique":[1,5,30,46],"w":1686}, +{"clique":[1,16,29,42],"w":90451}, +{"clique":[2,10,19,47],"w":4482}, +{"clique":[2,25,35,47],"w":13934}, +{"clique":[3,8,34,39],"w":27720}, +{"clique":[3,20,32,39],"w":105}, +{"clique":[3,35,36,39],"w":6323}, +{"clique":[4,5,24,38],"w":12260}, +{"clique":[4,11,18,21],"w":1289}, +{"clique":[4,18,21,36],"w":39131}, +{"clique":[4,20,24,38],"w":17525}, +{"clique":[4,21,36,39],"w":23945}, +{"clique":[4,22,24,25],"w":17519}, +{"clique":[5,26,30,46],"w":1575}, +{"clique":[6,18,20,31],"w":69431}, +{"clique":[6,18,21,28],"w":34656}, +{"clique":[6,18,21,31],"w":15666}, +{"clique":[6,24,38,46],"w":3239}, +{"clique":[7,9,15,30],"w":2659}, +{"clique":[7,12,29,52],"w":18523}, +{"clique":[8,28,35,45],"w":35354}, +{"clique":[9,23,27,40],"w":24756}, +{"clique":[10,21,32,45],"w":18975}, +{"clique":[10,32,45,49],"w":5714}, +{"clique":[13,14,20,32],"w":22618}, +{"clique":[22,25,26,46],"w":2052}, +{"clique":[0,10,19,35,47],"w":9654}, +{"clique":[0,12,24,29,49],"w":6127}, +{"clique":[1,9,40,42,48],"w":20017}, +{"clique":[1,10,23,42,45],"w":28535}, +{"clique":[2,3,11,19,43],"w":22478}, +{"clique":[2,10,11,19,47],"w":9}, +{"clique":[2,12,29,49,52],"w":27166}, +{"clique":[4,11,13,14,43],"w":27409}, +{"clique":[4,13,14,27,38],"w":18467}, +{"clique":[4,23,27,30,51],"w":2732}, +{"clique":[4,36,40,47,54],"w":10822}, +{"clique":[5,7,15,21,46],"w":26218}, +{"clique":[5,12,29,30,49],"w":20390}, +{"clique":[5,25,30,48,50],"w":7888}, +{"clique":[5,30,38,48,50],"w":9519}, +{"clique":[6,14,18,28,53],"w":7972}, +{"clique":[6,14,18,36,53],"w":9223}, +{"clique":[7,13,14,32,45],"w":6337}, +{"clique":[7,15,18,20,30],"w":9661}, +{"clique":[7,16,20,25,48],"w":1909}, +{"clique":[8,22,34,37,39],"w":30627}, +{"clique":[8,28,35,45,49],"w":2278}, +{"clique":[9,12,15,22,30],"w":21661}, +{"clique":[10,11,19,35,47],"w":35690}, +{"clique":[10,17,29,32,49],"w":58681}, +{"clique":[16,18,21,28,50],"w":10344}, +{"clique":[16,18,26,40,41],"w":24411}, +{"clique":[16,20,25,48,50],"w":737}, +{"clique":[0,8,12,29,49,52],"w":1730}, +{"clique":[0,9,12,15,30,49],"w":5102}, +{"clique":[0,28,42,48,50,51],"w":37443}, +{"clique":[1,3,4,16,29,42],"w":10829}, +{"clique":[1,3,6,14,31,53],"w":65616}, +{"clique":[1,8,33,34,44,55],"w":6230}, +{"clique":[1,10,17,23,42,45],"w":14951}, +{"clique":[1,10,18,45,51,53],"w":12256}, +{"clique":[1,16,20,42,48,50],"w":37561}, +{"clique":[2,3,22,26,39,46],"w":10677}, +{"clique":[2,5,7,12,15,47],"w":45951}, +{"clique":[2,5,12,16,40,47],"w":2402}, +{"clique":[2,7,23,31,45,52],"w":3088}, +{"clique":[2,10,19,25,35,47],"w":18500}, +{"clique":[2,12,26,31,35,47],"w":463}, +{"clique":[3,8,22,26,34,39],"w":14111}, +{"clique":[3,22,26,30,39,46],"w":8921}, +{"clique":[4,5,15,22,24,25],"w":42018}, +{"clique":[4,5,30,36,40,47],"w":32469}, +{"clique":[4,11,19,23,43,52],"w":2489}, +{"clique":[4,13,14,25,26,31],"w":5944}, +{"clique":[4,13,14,27,36,38],"w":7383}, +{"clique":[4,22,26,34,39,41],"w":15}, +{"clique":[5,12,15,24,29,49],"w":12669}, +{"clique":[6,15,20,30,31,50],"w":6274}, +{"clique":[6,20,28,35,38,50],"w":71092}, +{"clique":[6,24,33,34,44,55],"w":26977}, +{"clique":[7,16,26,40,41,46],"w":2950}, +{"clique":[7,20,28,29,35,52],"w":26380}, +{"clique":[7,22,34,37,39,52],"w":34751}, +{"clique":[8,10,17,27,34,39],"w":7276}, +{"clique":[8,28,40,47,48,54],"w":2878}, +{"clique":[16,23,33,44,45,55],"w":33215}, +{"clique":[21,28,32,49,50,54],"w":21968}, +{"clique":[0,6,20,28,48,50,54],"w":39478}, +{"clique":[0,7,13,14,26,27,46],"w":9588}, +{"clique":[0,8,28,42,48,50,54],"w":21203}, +{"clique":[1,5,10,11,15,19,43],"w":3264}, +{"clique":[1,9,10,11,19,23,42],"w":17961}, +{"clique":[1,9,10,17,26,29,42],"w":9682}, +{"clique":[1,9,23,28,29,42,52],"w":9390}, +{"clique":[1,10,34,38,42,46,51],"w":5008}, +{"clique":[2,4,21,35,36,39,45],"w":5941}, +{"clique":[2,7,9,12,15,22,24],"w":44794}, +{"clique":[2,8,12,28,29,43,52],"w":36876}, +{"clique":[2,9,16,23,40,45,47],"w":47141}, +{"clique":[2,10,33,35,41,45,49],"w":10928}, +{"clique":[2,18,21,35,36,39,45],"w":354}, +{"clique":[3,4,11,14,20,32,43],"w":11101}, +{"clique":[3,4,14,29,49,53,54],"w":37869}, +{"clique":[3,22,26,34,37,39,44],"w":35540}, +{"clique":[4,5,13,14,36,40,47],"w":5804}, +{"clique":[4,5,14,18,30,36,53],"w":15053}, +{"clique":[4,11,15,21,22,24,25],"w":25994}, +{"clique":[4,17,24,29,38,49,54],"w":24038}, +{"clique":[5,14,29,30,38,49,53],"w":11877}, +{"clique":[5,24,29,38,46,49,54],"w":4899}, +{"clique":[5,24,40,41,48,49,54],"w":15841}, +{"clique":[5,27,30,40,47,50,54],"w":90756}, +{"clique":[6,19,31,35,36,40,47],"w":3129}, +{"clique":[6,20,24,31,33,35,38],"w":19997}, +{"clique":[6,20,24,31,38,50,54],"w":15606}, +{"clique":[6,20,31,33,35,47,55],"w":18994}, +{"clique":[7,9,22,34,37,39,52],"w":5155}, +{"clique":[7,12,20,29,34,39,52],"w":837}, +{"clique":[7,18,21,34,36,37,39],"w":26635}, +{"clique":[10,11,15,19,20,21,32],"w":15073}, +{"clique":[0,4,13,14,20,25,32,46],"w":11347}, +{"clique":[0,6,10,23,27,33,38,46],"w":4214}, +{"clique":[0,9,12,24,29,38,49,54],"w":13637}, +{"clique":[0,10,25,32,33,35,45,49],"w":13146}, +{"clique":[0,12,17,29,33,49,54,55],"w":2237}, +{"clique":[0,13,16,19,40,45,46,47],"w":18780}, +{"clique":[0,14,18,22,26,41,46,53],"w":783}, +{"clique":[1,3,9,16,26,28,42,50],"w":1661}, +{"clique":[1,3,9,16,26,31,40,42],"w":14254}, +{"clique":[1,5,7,14,15,30,46,53],"w":1153}, +{"clique":[1,5,10,18,23,38,45,53],"w":32015}, +{"clique":[1,9,10,22,38,42,46,51],"w":3371}, +{"clique":[1,9,12,29,33,34,44,55],"w":4488}, +{"clique":[1,9,19,23,40,42,45,47],"w":3384}, +{"clique":[2,3,7,16,26,39,46,52],"w":904}, +{"clique":[2,4,11,14,18,43,53,54],"w":27153}, +{"clique":[2,5,12,30,33,35,47,55],"w":6595}, +{"clique":[2,7,21,26,34,39,46,52],"w":14116}, +{"clique":[2,10,11,19,25,26,31,43],"w":13586}, +{"clique":[2,10,33,35,40,41,45,47],"w":1441}, +{"clique":[3,4,8,11,22,34,37,39],"w":8963}, +{"clique":[3,4,8,16,23,27,39,40],"w":12669}, +{"clique":[3,4,24,29,39,49,53,54],"w":13911}, +{"clique":[3,8,16,24,26,39,48,50],"w":1687}, +{"clique":[3,8,21,30,36,39,45,53],"w":3539}, +{"clique":[3,26,31,33,35,40,41,47],"w":11339}, +{"clique":[5,12,14,17,29,30,49,53],"w":8877}, +{"clique":[5,14,28,32,38,49,50,54],"w":20276}, +{"clique":[7,13,14,21,26,31,32,45],"w":3682}, +{"clique":[7,16,18,22,26,40,41,46],"w":14284}, +{"clique":[11,16,18,19,21,24,32,49],"w":23277}, +{"clique":[0,3,12,29,33,35,41,51,55],"w":10988}, +{"clique":[0,5,7,12,22,29,34,37,52],"w":22839}, +{"clique":[0,6,10,19,23,27,40,46,47],"w":4869}, +{"clique":[0,7,19,22,25,28,46,47,51],"w":13264}, +{"clique":[0,12,13,14,16,17,32,42,45],"w":20849}, +{"clique":[1,3,22,24,26,39,40,41,46],"w":8070}, +{"clique":[1,5,7,15,16,20,25,48,50],"w":3971}, +{"clique":[1,9,10,13,17,38,42,49,53],"w":46500}, +{"clique":[1,9,10,17,23,29,33,51,55],"w":45844}, +{"clique":[1,10,17,20,38,41,46,51,55],"w":3934}, +{"clique":[2,3,9,12,16,26,29,43,52],"w":3920}, +{"clique":[2,4,11,13,14,16,25,37,43],"w":39890}, +{"clique":[2,6,12,31,33,34,44,47,55],"w":31148}, +{"clique":[2,9,12,29,33,43,52,54,55],"w":12476}, +{"clique":[3,4,11,22,34,37,39,41,43],"w":63902}, +{"clique":[4,5,11,15,19,23,30,31,43],"w":15724}, +{"clique":[4,11,13,14,16,18,32,43,52],"w":7504}, +{"clique":[4,11,22,24,25,34,37,44,51],"w":461}, +{"clique":[4,16,18,22,23,33,40,41,45],"w":9031}, +{"clique":[5,7,15,18,21,24,34,37,48],"w":12210}, +{"clique":[5,10,11,15,22,34,37,41,48],"w":19721}, +{"clique":[5,12,15,29,34,37,44,51,55],"w":3377}, +{"clique":[5,12,24,28,38,41,49,50,54],"w":2234}, +{"clique":[5,14,17,27,29,30,46,49,53],"w":6740}, +{"clique":[7,18,21,28,35,36,39,51,52],"w":6232}, +{"clique":[8,10,22,25,26,34,37,39,48],"w":34691}, +{"clique":[9,10,19,27,32,40,47,49,54],"w":2314}, +{"clique":[10,17,22,25,26,27,34,37,39],"w":886}, +{"clique":[10,17,22,26,32,34,39,41,46],"w":1621}, +{"clique":[10,17,23,25,27,29,32,42,49],"w":14145}, +{"clique":[11,13,14,18,19,30,43,51,53],"w":11196}, +{"clique":[0,6,8,10,22,34,37,39,44,51],"w":20059}, +{"clique":[0,9,10,19,32,35,40,45,46,47],"w":9325}, +{"clique":[0,10,25,32,33,35,44,46,51,55],"w":21776}, +{"clique":[1,3,7,16,22,26,29,39,46,52],"w":725}, +{"clique":[1,3,7,16,26,33,40,41,42,46],"w":48073}, +{"clique":[1,3,8,11,14,19,26,31,43,53],"w":10499}, +{"clique":[1,5,7,13,14,30,38,46,51,53],"w":1049}, +{"clique":[1,5,10,13,17,18,38,45,49,53],"w":120}, +{"clique":[1,6,8,16,23,31,33,44,52,55],"w":11912}, +{"clique":[1,6,9,12,24,31,38,49,53,54],"w":1066}, +{"clique":[1,7,9,12,13,15,17,30,42,50],"w":8527}, +{"clique":[1,9,12,29,33,40,44,49,54,55],"w":9031}, +{"clique":[1,9,16,18,26,31,40,42,48,50],"w":12097}, +{"clique":[2,3,9,12,24,29,39,49,53,54],"w":7928}, +{"clique":[2,3,12,16,29,33,41,44,51,55],"w":7335}, +{"clique":[2,4,8,11,16,22,25,37,43,52],"w":3948}, +{"clique":[2,5,12,14,15,16,18,29,49,53],"w":1950}, +{"clique":[2,6,11,14,18,28,43,50,53,54],"w":339}, +{"clique":[2,6,20,25,31,33,35,36,47,55],"w":5151}, +{"clique":[2,7,16,18,21,28,42,46,51,52],"w":36185}, +{"clique":[4,5,11,15,18,21,22,34,37,43],"w":18851}, +{"clique":[5,7,11,14,15,18,30,46,51,53],"w":25578}, +{"clique":[5,10,11,15,19,21,23,25,32,49],"w":2864}, +{"clique":[5,10,27,32,38,40,47,48,49,54],"w":5570}, +{"clique":[5,14,18,27,30,38,46,49,53,54],"w":4026}, +{"clique":[5,17,21,24,28,38,48,49,50,54],"w":12134}, +{"clique":[6,9,22,24,25,27,34,37,38,40],"w":4771}, +{"clique":[6,10,11,19,20,23,27,31,43,52],"w":6048}, +{"clique":[7,9,13,14,15,21,26,31,32,46],"w":13370}, +{"clique":[9,10,27,33,40,44,48,49,54,55],"w":18771}, +{"clique":[9,12,27,29,33,37,40,44,54,55],"w":43250}, +{"clique":[10,17,18,20,21,27,32,35,38,49],"w":33943}, +{"clique":[10,17,22,23,25,26,27,29,32,42],"w":7526}, +{"clique":[10,25,27,32,33,40,44,49,54,55],"w":44728}, +{"clique":[0,3,7,22,23,26,34,39,41,46,52],"w":28364}, +{"clique":[0,4,22,24,28,34,38,39,41,46,51],"w":5642}, +{"clique":[0,6,9,10,21,32,33,35,38,46,55],"w":11446}, +{"clique":[0,6,16,23,27,31,33,44,46,51,55],"w":6474}, +{"clique":[0,8,12,13,14,15,28,32,35,45,49],"w":20022}, +{"clique":[0,9,10,19,22,23,32,40,45,46,47],"w":4087}, +{"clique":[1,3,5,7,20,26,30,39,46,52,53],"w":23349}, +{"clique":[1,3,7,9,16,26,31,40,42,46,52],"w":6819}, +{"clique":[1,3,9,26,31,33,34,44,46,53,55],"w":1301}, +{"clique":[1,5,13,14,17,29,30,38,46,49,53],"w":2937}, +{"clique":[1,6,10,20,31,33,34,41,44,48,55],"w":12214}, +{"clique":[1,6,10,31,33,34,41,44,49,53,55],"w":28301}, +{"clique":[1,7,9,12,13,15,17,30,45,50,53],"w":612}, +{"clique":[1,7,9,14,16,29,38,46,51,52,53],"w":26809}, +{"clique":[1,7,16,23,25,26,31,42,45,48,50],"w":1868}, +{"clique":[1,9,10,13,17,38,42,47,50,53,54],"w":8685}, +{"clique":[1,9,16,23,25,40,42,45,47,48,50],"w":27223}, +{"clique":[2,3,12,19,22,24,26,34,39,41,43],"w":12983}, +{"clique":[2,4,11,16,22,23,25,33,37,43,52],"w":16378}, +{"clique":[3,4,11,19,22,34,35,36,37,39,43],"w":8870}, +{"clique":[3,7,9,12,15,22,26,30,37,39,40],"w":21197}, +{"clique":[3,9,15,19,23,26,27,30,31,32,40],"w":827}, +{"clique":[4,5,14,15,22,25,29,30,46,51,53],"w":2573}, +{"clique":[6,8,10,11,22,34,35,37,39,43,52],"w":2138}, +{"clique":[6,8,15,20,23,33,34,37,44,45,55],"w":28043}, +{"clique":[6,9,12,27,29,33,40,47,52,54,55],"w":16660}, +{"clique":[6,20,23,24,31,33,34,44,45,51,55],"w":11542}, +{"clique":[6,20,30,31,33,35,44,47,48,50,55],"w":11566}, +{"clique":[7,9,11,15,21,22,24,25,34,37,39],"w":20976}, +{"clique":[7,13,14,16,17,18,21,26,32,42,45],"w":41590}, +{"clique":[8,10,17,22,27,29,34,37,39,51,52],"w":519}, +{"clique":[0,6,8,10,19,22,29,34,37,39,44,51],"w":1959}, +{"clique":[0,6,10,17,23,25,27,29,33,46,51,55],"w":21990}, +{"clique":[0,7,9,13,14,16,19,40,42,45,46,47],"w":13386}, +{"clique":[0,7,12,13,14,16,18,19,29,51,52,53],"w":11173}, +{"clique":[0,7,19,21,24,28,32,40,41,46,51,55],"w":3839}, +{"clique":[0,10,17,18,21,32,33,35,41,45,46,49],"w":8147}, +{"clique":[1,6,8,15,20,23,30,31,33,42,48,50],"w":2837}, +{"clique":[1,6,10,18,20,31,34,42,44,50,51,53],"w":1068}, +{"clique":[1,6,14,18,20,30,31,42,48,50,53,54],"w":5971}, +{"clique":[2,3,5,12,30,36,37,39,43,45,50,54],"w":4309}, +{"clique":[2,3,7,9,16,21,26,28,39,42,48,50],"w":11819}, +{"clique":[2,3,7,26,31,33,35,41,46,47,52,55],"w":26281}, +{"clique":[2,6,8,11,19,28,34,37,44,47,51,55],"w":2855}, +{"clique":[2,7,9,15,21,25,26,30,31,45,48,50],"w":10873}, +{"clique":[2,7,9,16,23,33,38,45,48,51,52,55],"w":2763}, +{"clique":[2,9,12,25,30,33,40,45,47,50,54,55],"w":10673}, +{"clique":[2,10,13,17,33,35,44,45,47,51,53,55],"w":15884}, +{"clique":[2,10,17,23,25,27,29,33,37,44,51,55],"w":22791}, +{"clique":[3,5,7,15,21,22,26,32,34,39,41,48],"w":12534}, +{"clique":[3,6,9,11,12,15,30,31,33,43,51,55],"w":15769}, +{"clique":[3,6,9,21,24,28,29,32,39,40,49,54],"w":19680}, +{"clique":[4,5,11,16,18,24,33,37,38,41,43,49],"w":24720}, +{"clique":[4,11,19,20,24,25,28,37,38,43,49,54],"w":48745}, +{"clique":[6,8,10,17,22,23,27,34,37,38,39,42],"w":3819}, +{"clique":[6,10,20,31,32,33,35,40,41,44,47,55],"w":2167}, +{"clique":[6,11,16,18,20,21,23,24,32,33,43,45],"w":4389}, +{"clique":[6,16,18,20,21,23,24,31,32,38,45,49],"w":5294}, +{"clique":[7,13,14,16,26,32,40,41,42,45,46,47],"w":3948}, +{"clique":[8,10,11,19,22,25,34,36,37,39,44,51],"w":11347}, +{"clique":[9,10,17,22,23,25,27,34,36,37,38,39],"w":26461}, +{"clique":[10,13,17,25,33,35,44,45,46,49,53,55],"w":5965}, +{"clique":[0,3,7,9,12,15,22,26,27,29,30,37,40],"w":23928}, +{"clique":[0,3,8,12,17,22,26,27,29,34,37,39,42],"w":9285}, +{"clique":[0,5,7,13,14,29,38,45,47,48,52,53,54],"w":18491}, +{"clique":[0,7,12,22,24,26,29,34,37,38,39,41,52],"w":40068}, +{"clique":[1,4,5,11,14,18,28,35,36,38,43,51,53],"w":2123}, +{"clique":[1,4,8,11,14,22,25,28,38,43,50,53,54],"w":2175}, +{"clique":[1,5,7,13,17,19,30,38,41,46,51,53,55],"w":21275}, +{"clique":[1,7,9,15,16,23,28,40,42,45,47,48,50],"w":13693}, +{"clique":[1,7,9,16,18,21,26,28,29,40,42,46,52],"w":3482}, +{"clique":[1,9,13,16,17,29,33,44,45,49,52,53,55],"w":45672}, +{"clique":[1,10,13,17,29,33,41,44,48,49,53,54,55],"w":20678}, +{"clique":[2,3,6,8,12,24,29,39,43,49,52,53,54],"w":57567}, +{"clique":[2,3,6,9,12,24,31,33,44,49,50,54,55],"w":60672}, +{"clique":[2,6,12,15,20,25,30,31,33,35,44,47,55],"w":17430}, +{"clique":[2,8,16,17,23,25,29,33,44,45,49,52,55],"w":11460}, +{"clique":[3,6,9,15,23,27,30,31,33,40,44,51,55],"w":8627}, +{"clique":[3,7,9,16,26,27,28,37,39,40,42,48,50],"w":29395}, +{"clique":[4,5,11,15,16,21,23,24,25,33,37,43,55],"w":1608}, +{"clique":[4,8,11,19,28,34,35,36,37,41,44,47,55],"w":2759}, +{"clique":[5,10,11,15,18,21,22,34,36,37,39,41,48],"w":19928}, +{"clique":[5,10,15,17,18,20,21,26,27,31,32,34,48],"w":41439}, +{"clique":[5,13,14,25,27,30,32,38,40,47,48,49,54],"w":48665}, +{"clique":[6,8,20,25,31,32,33,34,35,44,47,48,55],"w":7947}, +{"clique":[6,9,27,30,31,33,36,40,47,48,50,54,55],"w":895}, +{"clique":[7,11,13,14,16,18,19,21,42,45,46,51,53],"w":7452}, +{"clique":[9,18,21,24,27,28,37,38,40,42,48,49,54],"w":6943}, +{"clique":[0,5,15,16,20,23,33,37,40,44,45,47,48,55],"w":12631}, +{"clique":[0,6,8,10,19,20,25,31,32,34,44,46,51,55],"w":12840}, +{"clique":[0,6,8,12,22,24,28,29,37,38,39,41,52,54],"w":13313}, +{"clique":[0,6,9,12,17,24,27,29,33,38,49,53,54,55],"w":18353}, +{"clique":[0,7,9,18,21,23,26,27,30,31,32,40,46,52],"w":1058}, +{"clique":[0,8,10,22,23,25,29,34,37,39,44,48,51,52],"w":4638}, +{"clique":[1,3,7,9,11,14,15,19,21,23,26,30,31,53],"w":34189}, +{"clique":[1,3,7,9,12,14,17,22,26,29,30,42,52,53],"w":12418}, +{"clique":[1,5,7,13,18,30,36,38,39,45,48,50,53,54],"w":32096}, +{"clique":[1,5,11,13,14,18,30,38,41,48,49,50,53,54],"w":47308}, +{"clique":[1,8,10,17,22,29,34,39,42,44,46,51,52,53],"w":6096}, +{"clique":[1,13,14,16,18,28,36,42,44,45,48,50,51,53],"w":83094}, +{"clique":[2,3,4,16,23,26,33,40,41,44,45,47,50,55],"w":25165}, +{"clique":[4,8,13,30,33,36,40,41,44,45,47,50,54,55],"w":7428}, +{"clique":[6,8,11,22,24,25,34,37,39,42,44,48,50,51],"w":4108}, +{"clique":[6,8,21,24,28,32,38,40,41,48,49,50,54,55],"w":25260}, +{"clique":[7,9,13,14,18,26,28,29,35,38,45,46,52,53],"w":2885}, +{"clique":[0,5,7,14,17,18,19,23,26,27,30,31,38,46,53],"w":23181}, +{"clique":[0,6,10,17,20,27,31,32,33,38,48,49,50,54,55],"w":18980}, +{"clique":[1,3,4,5,11,14,20,26,28,35,36,43,46,52,53],"w":1271}, +{"clique":[1,3,6,9,11,14,19,30,31,42,44,46,47,51,53],"w":380}, +{"clique":[1,3,6,9,16,23,24,31,33,44,45,49,52,53,55],"w":3432}, +{"clique":[1,4,5,11,16,20,23,24,25,33,38,43,46,51,55],"w":2394}, +{"clique":[1,5,13,17,29,30,41,44,45,47,48,49,53,54,55],"w":61651}, +{"clique":[1,7,9,12,13,17,29,30,33,35,45,47,52,53,55],"w":18013}, +{"clique":[1,9,10,15,17,18,22,34,39,42,44,48,50,51,53],"w":17643}, +{"clique":[2,4,5,11,19,20,23,24,25,28,37,38,43,51,55],"w":46369}, +{"clique":[2,4,8,11,15,16,18,20,21,23,36,37,39,43,45],"w":2795}, +{"clique":[2,5,7,13,14,19,25,26,30,31,38,45,46,47,53],"w":28378}, +{"clique":[2,6,8,16,20,23,27,31,33,40,44,47,48,50,55],"w":22038}, +{"clique":[2,7,9,13,14,16,17,18,21,28,38,42,46,50,51],"w":2583}, +{"clique":[2,8,10,17,20,23,29,33,34,37,44,45,51,52,55],"w":4675}, +{"clique":[4,5,13,14,20,30,32,38,40,41,46,47,49,50,54],"w":16602}, +{"clique":[0,3,4,5,14,19,21,30,32,36,40,41,46,47,49,54],"w":13048}, +{"clique":[0,7,13,14,19,20,21,25,28,29,32,35,45,46,47,52],"w":28449}, +{"clique":[0,9,10,19,21,22,25,26,27,32,34,35,38,40,46,47],"w":45713}, +{"clique":[1,7,9,15,16,17,21,22,23,25,28,36,42,45,48,50],"w":5744}, +{"clique":[2,3,5,12,29,30,33,35,37,40,41,44,45,47,51,55],"w":16553}, +{"clique":[2,8,12,13,20,30,33,37,40,41,44,45,47,50,54,55],"w":38921}, +{"clique":[0,3,6,8,20,21,24,28,32,36,39,40,41,48,49,50,54],"w":13263}, +{"clique":[0,3,8,12,17,22,28,29,34,35,37,39,41,42,44,51,52],"w":92959}, +{"clique":[1,3,6,8,14,17,30,31,36,41,42,47,48,49,50,53,54],"w":23018}, +{"clique":[2,8,10,11,22,23,25,26,27,34,37,38,39,42,43,48,50],"w":8623}, +{"clique":[4,5,11,13,14,15,18,19,20,21,30,31,32,35,36,43,51],"w":70787}, +{"clique":[6,9,10,21,25,27,31,32,36,38,40,42,47,48,49,50,54],"w":22411}, +{"clique":[6,9,11,22,24,25,28,34,35,36,37,39,42,44,48,50,51],"w":33694}, +{"clique":[0,4,8,13,14,15,18,19,20,21,26,30,31,32,35,36,43,46],"w":72604}, +{"clique":[1,4,5,11,13,14,18,19,20,26,30,31,35,38,41,43,46,53],"w":25439}, +{"clique":[1,4,8,11,14,16,18,21,23,28,36,42,43,45,46,51,52,53],"w":75007}, +{"clique":[2,3,4,8,11,15,19,21,22,26,28,34,35,36,37,39,41,43],"w":42010}, +{"clique":[2,5,10,13,15,17,20,25,26,27,31,33,35,44,47,48,53,55],"w":34077}, +{"clique":[6,9,10,11,17,18,22,23,27,34,36,37,39,42,44,48,50,51],"w":1743}, +{"clique":[6,11,16,20,21,23,24,25,27,31,32,33,38,43,48,51,52,55],"w":26885}, +{"clique":[0,3,4,8,14,15,19,20,23,26,30,31,32,36,40,41,45,46,47],"w":67456}, +{"clique":[0,3,8,12,15,19,22,24,26,28,29,34,35,36,37,39,40,41,44],"w":1246}, +{"clique":[0,5,7,12,13,14,19,20,25,27,29,30,32,35,36,38,40,47,52],"w":51419}, +{"clique":[2,6,8,10,11,17,22,23,25,27,34,36,37,38,39,42,43,48,50],"w":53539}, +{"clique":[2,6,8,11,12,19,22,24,25,28,34,35,36,37,38,39,43,51,52],"w":47560}, +{"clique":[4,11,16,17,18,19,20,21,23,24,26,27,31,32,38,42,43,46,52],"w":45367}, +{"clique":[4,8,11,19,21,22,23,24,25,27,28,34,36,37,38,39,42,43,51,52],"w":70579}, +{"clique":[0,3,6,8,12,15,17,19,20,24,27,28,29,32,34,35,36,39,42,43,49],"w":7203}, +{"clique":[1,7,9,17,18,21,22,23,24,28,29,34,36,38,39,42,45,46,51,52,53],"w":51588}, +{"clique":[2,6,9,11,17,21,23,24,25,27,28,34,36,37,38,39,42,43,48,49,50],"w":16183}, +{"clique":[0,3,6,8,12,15,19,20,24,28,29,32,34,35,36,39,40,41,42,44,45,49],"w":16974}, +{"clique":[1,4,5,11,13,14,17,18,20,21,30,31,36,38,41,43,45,46,49,50,53,54],"w":17416}, +{"clique":[1,8,10,17,18,19,21,22,23,26,29,34,36,38,39,41,42,43,45,46,52,53],"w":636}, +{"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":2568}, +{"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":30233} +]} diff --git a/research/plane-port-clique-floor-141/README.md b/research/plane-port-clique-floor-141/README.md new file mode 100644 index 0000000000..a32c3f34a6 --- /dev/null +++ b/research/plane-port-clique-floor-141/README.md @@ -0,0 +1,110 @@ +# Every plane-port decoder costs at least 141, over every field + +**Exact finite certificate for a scoped lower bound. No new κ.** +Take the strict 112-port mask with its 56 matched planes (PR1825, PR1889) and CubeJerry's +additive full-plane COPY tariff (#4365). Every finite rank-one decoder of this mask, over any +coefficient field, costs at least + + 36732955/262144 = 140.1251..., hence >= 141. + +This raises the all-field floor of Mark (Matarener)'s +[PR #5560](https://github.com/CrocSwap/integer-mult-bounds/pull/5560) +(`research/plane-port-global-rank-dual`) from 140 to 141. It answers that package's Open next +question 2 ("Can a stronger functional beat the clique programme?") with a better point of the +same programme. It does not reach the break-even value 164 or the 224 conjecture. + +## What is new + +The proof is #5560's, unchanged. Lemma 1 says a clique `Q` of pairwise non-orthogonal planes +carries an identity block, so at least `2|Q|` terms touch it on both sides. Lemma 2 is weak +duality, and Lemma 3 reduces condition (F) to ordered pairs of plane-generated subspaces. Any +nonnegative clique weights that satisfy + + sum over cliques Q with a plane inside A and a plane inside R of w_Q <= t(A, R) + +for every ordered pair `(A, R)` of the 39,087 generated subspaces therefore bound every decoder +by `sum_Q 2|Q| w_Q`. See #5560's [PROOF.md](../plane-port-global-rank-dual/PROOF.md). + +The new part is the weight vector. #5560's 443 columns give 139.11. This +[CERTIFICATE.json](CERTIFICATE.json) has 425 clique columns, of sizes 1 to 24, with integer +weights over `2^20`. Their value is 140.1251. The columns came from fresh row-and-column +generation. The pricing step is a local search over cliques, against duals of +the active span-pair rows. Every round separated exhaustively over all 1,527,793,569 ordered pairs. + +## Evidence + +[verify.py](verify.py) was written separately from the generator. It checks, in exact arithmetic: + +- the 56 planes from the pinned archive and matching, each nondegenerate, with 109 orthogonal pairs; +- an independent closure census by reduced echelon bases: 39,087 subspaces; +- the tariff `dim A - dim(A meet R^perp)`, compared with Gaussian elimination of the pairing + matrix on 4,000 random pairs; +- every column is a clique with a positive integer weight; +- feasibility on **all** 39,087² ordered pairs. The minimum slack is 0. It is attained exactly + on the 1,732 pairs with tariff 0, which no clique can touch, and every positive-tariff pair + has positive slack; +- the recorded bound 36732955/262144 > 140; +- four rejecting controls: an overweight column, an orthogonal pair as a clique, a wrong + recorded bound, and #5560's own certificate, which passes feasibility but stays at 139.11 < 140. + +Load sums stay below 2^40 and census counts are at most 512, so the floating-point matrix +products are exact. The full run takes about 30 seconds on a 2026 Apple laptop. + +## Reproduce + +From the repository root, with CPython 3.12 and numpy 2: + +```sh +python3.12 -B research/plane-port-clique-floor-141/verify.py # full check, prints PASS_PLANE_PORT_CLIQUE_FLOOR_141 +python3.12 -B research/plane-port-clique-floor-141/verify.py --sampled # every 97th row only +python3.12 -B scripts/research_package.py --package research/plane-port-clique-floor-141 +``` + +Optional regeneration, which needs scipy and is not part of the proof: + +```sh +PLANE_PORT_CACHE=/tmp/ppcf python3.12 -B research/plane-port-clique-floor-141/generate/colgen.py 1 40 +PLANE_PORT_CACHE=/tmp/ppcf python3.12 -B research/plane-port-clique-floor-141/generate/roundcert.py +``` + +`colgen.py` starts from #5560's columns and all singletons. It stops at the first point +certified above 140. `roundcert.py` floors the weights onto the `2^20` grid and checks them +exactly. It writes the certificate into the cache directory. The cache holds a 1.5 GB tariff +matrix. On macOS with CPython 3.12.15, numpy 2.5.4 (Accelerate) and scipy 1.18.1, the generator +stopped after 14 rounds, in about 6 minutes. It reproduced this CERTIFICATE.json byte for byte. +Other BLAS or HiGHS builds may produce a different valid certificate, and verify.py checks +whichever certificate is present. + +## Not covered + +- The optimum of the clique programme. #5560 reports a floating-point pricing estimate of + about 167. This run did not price exactly, so no upper bound is certified here. +- The conjecture that 224 holds over every field. The interval [141, 224] stays open for + characteristic-0 coefficients with even denominators. +- Native realization, hosting, routing, the coverage law and concave pricing. These are + #4365's and #5560's caveats. No supplier, κ or selected-frontier change follows. + +## Open next questions + +1. **What is the optimum of the clique programme, and is it above 164?** A certified value + above 164 would close the plane-port lever in #4365's contract for every field. *First step:* + raise `STOP` in `generate/colgen.py` and add an exact MILP pricer, which also certifies an + upper bound. *Blocked by:* local-search pricing found fewer than ten new columns per round + near 140. +2. **Can non-clique columns do better?** #5560's estimate of about 167 leaves little room above + 164. *First step:* add the sharp C5 covers of `c5-residual-weighted-cover` and the three- and + four-plane rank duals as columns, with the same exhaustive separation. *Blocked by:* nothing. + One separation pass takes about 15 seconds. +3. **Does every decoder cost at least 224 over Q?** This is #5560's conjecture. *First step:* + #5560 THEORY.md E2, induction on the top 2-adic valuation. *Blocked by:* there is no known + bound for zero-mask binary layers. + +## Credit + +The clique programme, Lemmas 1-3 and the 140 certificate are Mark (Matarener)'s +([#5560](https://github.com/CrocSwap/integer-mult-bounds/pull/5560)). That package's own credits +also apply. The contract and two-plane theorem are CubeJerry's (#4365). The rank-dual +functional is pinterbanget's (#4421). The 224 bound for 2-integral decoders is Philippe Van +Velzen's (Discussion 1587, #2532). The plane-port budgets are josie's (#1808). The labels and +matching come from PR1825/2126 (Cinna Davis). The new certificate, generator and verifier were +produced by Nick Petalas. Apache-2.0. diff --git a/research/plane-port-clique-floor-141/SOURCES.json b/research/plane-port-clique-floor-141/SOURCES.json new file mode 100644 index 0000000000..dbe0eb78d7 --- /dev/null +++ b/research/plane-port-clique-floor-141/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json", + "usage": "input", + "git_blob": "7ca668d7d50c7276e89b0f6f9575e1b9f1ad9ef6", + "sha256": "4fd648f7b5178bff5441bf364d58234b7bc1a43b924bc6da03013c948f1473b1" + }, + { + "path": "research/plane-port-global-rank-dual/CERTIFICATE.json", + "usage": "input", + "git_blob": "512297535886e717087af5cb0ade0a747a2bb400", + "sha256": "20ccaf90c909c602bacc101f3dc540848c844903506e8bce70eb06f28c1ec342" + } + ] +} diff --git a/research/plane-port-clique-floor-141/TASK.json b/research/plane-port-clique-floor-141/TASK.json new file mode 100644 index 0000000000..ac96e4f479 --- /dev/null +++ b/research/plane-port-clique-floor-141/TASK.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "coframe", + "signed moment", + "5693", + "5698" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Global all-field lower bound 36732955/262144 = 140.1251 (hence 141) on the additive full-plane COPY mass of every finite scalar decoder of the strict 112-port PR1825/PR1889 mask, under CubeJerry's #4365 tariff. It is a new 425-clique feasible point of PR5560's clique programme, checked exactly on all 39,087^2 ordered span pairs. PR5560's Lemmas 1-3 are reused unchanged.", + "scope_change_reason": "The card asks for a legal decoder or coframe change that improves the full signed moment. This package instead raises a lower bound on one decoder family's COPY mass: it answers Open next question 2 of PR5560 (research/plane-port-global-rank-dual), the stronger clique-programme certificate. It narrows the plane-port break-even window from [140, 164] to [141, 164].", + "bottleneck_link": "Side result for the plane-port coverage lever (plane-port-copy-budgets). A decoder must cost at most about 160-164 per call to break even with the incumbent word. The all-field floor rises from 140 to 141, which shrinks that window by one unit. No kappa change.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact certificate above 140 (floor 141); further column generation is left as an open question.", + "outcome": "completed", + "evidence": "verify.py: independent closure census of 39,087 generated subspaces, tariffs cross-checked by Gaussian elimination on 4,000 random pairs, 425 clique columns, exact feasibility on all 1,527,793,569 ordered pairs (minimum slack 0, attained exactly on the 1,732 zero-tariff pairs), bound 36732955/262144, and four rejecting controls including PR5560's own certificate (139.11 < 140). generate/ holds the row-and-column generation and rounding code (scipy HiGHS); it is not needed for the proof.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the optimum of the full clique programme, and does it exceed 164?", + "why_it_matters": "A certified value above 164 would close the plane-port lever for every coefficient field in #4365's contract without settling the 224 conjecture.", + "first_step": "Continue generate/colgen.py past the 140 stop (raise STOP), and replace the local-search pricing with an exact MILP pricer to obtain a certified upper bound on the programme.", + "blocked_by": "Local-search pricing slowed to fewer than ten new columns per round near 140; no exact pricing bound is available yet." + }, + { + "question": "Can columns other than cliques (C5 covers, three- and four-plane rank duals) beat the clique programme's optimum?", + "why_it_matters": "PR5560 estimates the clique programme at about 167, which leaves little headroom above 164.", + "first_step": "Add the sharp C5 covers of c5-residual-weighted-cover as columns, with the same exhaustive span-pair separation used by verify.py.", + "blocked_by": "Nothing; the separation step takes about 15 seconds on one machine." + }, + { + "question": "Does every decoder cost at least 224 over Q?", + "why_it_matters": "This is PR5560's conjecture, and it would close the lever for every field.", + "first_step": "PR5560 THEORY.md E2: induct on the top 2-adic valuation.", + "blocked_by": "No known lower bound for zero-mask binary layers." + } + ] +} diff --git a/research/plane-port-clique-floor-141/VERIFY.json b/research/plane-port-clique-floor-141/VERIFY.json new file mode 100644 index 0000000000..a0596e7274 --- /dev/null +++ b/research/plane-port-clique-floor-141/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.2.6" + ], + "inputs": [ + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/paired-plane-port-matching-seed6c563a/CERTIFICATE.json", + "research/plane-port-global-rank-dual/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 400, + "checks": "independent closure census (39,087 spans), tariff vs Gaussian elimination on 4,000 pairs, clique columns, exact feasibility on all 39,087^2 ordered pairs, bound 36732955/262144 > 140, four rejecting controls" + } + ] +} diff --git a/research/plane-port-clique-floor-141/generate/colgen.py b/research/plane-port-clique-floor-141/generate/colgen.py new file mode 100644 index 0000000000..5d782175ef --- /dev/null +++ b/research/plane-port-clique-floor-141/generate/colgen.py @@ -0,0 +1,143 @@ +"""Row-and-column generation for the clique programme of PR5560 (certificate generator; needs scipy for HiGHS). + +max sum_c 2|Q_c| w_c s.t. sum_{c touched by (a,r)} w_c <= T[a,r] for all ordered span pairs. +""" +import json, sys, time +from pathlib import Path +import numpy as np +import scipy.sparse as sp +from scipy.optimize import linprog +from geom import load, ROOT, CACHE + +T0 = time.time() +rng = np.random.default_rng(int(sys.argv[1]) if len(sys.argv) > 1 else 1) +ITERS = int(sys.argv[2]) if len(sys.argv) > 2 else 40 +STOP = 140.0 # stop at the first point certified above this value + + +def log(*a): + print('%6.0fs' % (time.time() - T0), *a, flush=True) + + +inside, T, orth = load() +n = len(T) +Tf = T.astype(np.float32) +INS = inside.astype(np.float32) +log('spans', n) + +cert = json.loads((ROOT / 'research/plane-port-global-rank-dual/CERTIFICATE.json').read_text()) +cols = {tuple(sorted(c['clique'])) for c in cert['columns']} +cols |= {(i,) for i in range(56)} +cols = sorted(cols) + + +def qmat(cs): + q = np.zeros((len(cs), 56), np.float32) + for k, c in enumerate(cs): + q[k, list(c)] = 1 + return q + + +def separate(cs, w, top=4000): + """max ratio load/T over all rows, and the most violated pairs""" + keep = w > 1e-12 + q = qmat([c for c, k in zip(cs, keep) if k]); wk = w[keep].astype(np.float32) + touch = ((INS @ q.T) > 0).astype(np.float32) + TW = (touch * wk).T.copy() + worst = 0.0; cand = [] + B = 4096 + for b0 in range(0, n, B): + L = touch[b0:b0 + B] @ TW + t = Tf[b0:b0 + B] + ratio = np.where(t > 0, L / np.maximum(t, 1), np.where(L > 1e-6, np.inf, 0)) + worst = max(worst, float(ratio.max())) + viol = L - t + idx = np.argpartition(viol.ravel(), -top)[-top:] + v = viol.ravel()[idx] + sel = idx[v > 1e-7] + for f, vv in zip(sel, viol.ravel()[sel]): + cand.append((float(vv), b0 + f // n, f % n)) + cand.sort(reverse=True) + return worst, [(a, r) for _, a, r in cand[:top]] + + +def price(rows, y, ntry=400, keepn=200): + """local search for cliques with positive reduced profit 2|Q| - sum y [touch]""" + act = y > 1e-9 + if not act.any(): + return [] + ra = np.array([a for (a, r), k in zip(rows, act) if k]); rr = np.array([r for (a, r), k in zip(rows, act) if k]) + yy = y[act] + A = inside[ra]; R = inside[rr] # K x 56 bool + compat = ~orth + found = {} + for _ in range(ntry): + q = np.zeros(56, bool) + order = rng.permutation(56) + q[order[0]] = True + while True: + ta = (A & q).any(1); tr = (R & q).any(1) + base = 2 * q.sum() - yy @ (ta & tr) + # add moves + ok = compat[q].all(0) & ~q + nta = ta[:, None] | A; ntr = tr[:, None] | R + gain_add = 2 * q.sum() + 2 - yy @ (nta & ntr) + gain_add = np.where(ok, gain_add, -np.inf) + # remove moves (recompute) + best_rm = -np.inf; brm = -1 + for i in np.flatnonzero(q): + q2 = q.copy(); q2[i] = False + if not q2.any(): + continue + g = 2 * q2.sum() - yy @ ((A & q2).any(1) & (R & q2).any(1)) + if g > best_rm: + best_rm, brm = g, i + i = int(np.argmax(gain_add + rng.random(56) * 1e-9)) + if gain_add[i] > base + 1e-9 and gain_add[i] >= best_rm: + q[i] = True + elif best_rm > base + 1e-9: + q[brm] = False + else: + break + if base > 1e-7: + found[tuple(np.flatnonzero(q))] = base + return sorted(found, key=found.get, reverse=True)[:keepn] + + +def master(cs, rows): + q = qmat(cs).astype(bool) + ra = np.array([a for a, r in rows]); rr = np.array([r for a, r in rows]) + M = ((inside[ra].astype(np.int32) @ q.T.astype(np.int32)) > 0) & ((inside[rr].astype(np.int32) @ q.T.astype(np.int32)) > 0) + c = -2 * q.sum(1).astype(float) + res = linprog(c, A_ub=sp.csr_matrix(M.astype(float)), b_ub=T[ra, rr].astype(float), bounds=(0, None), method='highs') + assert res.status == 0, res.message + return res.x, -res.ineqlin.marginals, -res.fun + + +# initial rows: separation of the certificate weights scaled to be loose +w0 = np.zeros(len(cols)) +cmap = {c: k for k, c in enumerate(cols)} +for c in cert['columns']: + w0[cmap[tuple(sorted(c['clique']))]] = c['w'] / cert['scale'] +rows = set() +_, rws = separate(cols, w0 * 1.3, top=20000) +rows |= set(rws) +rows = sorted(rows) +best = 0 +for it in range(ITERS): + w, y, val = master(cols, rows) + worst, rws = separate(cols, w) + cert_val = val / max(worst, 1.0) + if cert_val > best: + best = cert_val + np.save(CACHE / 'best_w.npy', w); (CACHE / 'best_cols.json').write_text(json.dumps([list(map(int, c)) for c in cols])) + newrows = [r for r in rws if r not in set(rows)] + newcols = [c for c in price(rows, y) if c not in cmap] + log('it', it, 'rows', len(rows), 'cols', len(cols), 'LP', round(val, 4), 'maxratio', round(worst, 5), + 'certified~', round(cert_val, 4), 'best', round(best, 4), '+rows', len(newrows), '+cols', len(newcols)) + if best > STOP or (not newrows and not newcols): + break + rows = sorted(set(rows) | set(newrows)) + for c in newcols: + cmap[c] = len(cols); cols.append(c) +log('done best', best) diff --git a/research/plane-port-clique-floor-141/generate/geom.py b/research/plane-port-clique-floor-141/generate/geom.py new file mode 100644 index 0000000000..31257b8b0f --- /dev/null +++ b/research/plane-port-clique-floor-141/generate/geom.py @@ -0,0 +1,65 @@ +"""Geometry for the 56-plane decoder clique programme (certificate generation only; not the verifier).""" +import json, os, tarfile +from pathlib import Path +import numpy as np + +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' +CACHE = Path(os.environ.get('PLANE_PORT_CACHE', '/tmp/plane-port-clique-floor-141')) + + +def dot(x, y): + return bin(x & y).count('1') & 1 + + +def planes(): + 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'] + pl = [(labels[a], labels[b]) for a, b in matching] + pel = [{0, x, y, x ^ y} for x, y in pl] + orth = np.array([[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 pl, pel, orth + + +def census(pl): + idx = np.arange(512) + frontier = {} + for x, y in pl: + 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 pl: + 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 load(): + """inside (n x 56 bool), tariff (n x n int8), orth (56 x 56 bool)""" + CACHE.mkdir(parents=True, exist_ok=True) + pl, pel, orth = planes() + f = CACHE / 'geom.npz' + if f.exists(): + z = np.load(f) + return z['inside'], z['T'], orth + S = census(pl) + dim = np.log2(S.sum(1)).round().astype(np.int64) + 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 + 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 + cnt = S.astype(np.float32) @ perp.T.astype(np.float32) # |A meet R^perp|, exact (<= 512) + T = (dim[:, None] - np.log2(cnt).round().astype(np.int64)).astype(np.int8) + np.savez(f, inside=inside, T=T) + return inside, T, orth diff --git a/research/plane-port-clique-floor-141/generate/roundcert.py b/research/plane-port-clique-floor-141/generate/roundcert.py new file mode 100644 index 0000000000..983ed14257 --- /dev/null +++ b/research/plane-port-clique-floor-141/generate/roundcert.py @@ -0,0 +1,37 @@ +"""Round the best LP solution to an exact integer certificate (certificate generator).""" +import json, sys +from fractions import Fraction +import numpy as np +from geom import load, CACHE + +SCALE = 2 ** 20 +inside, T, orth = load() +n = len(T) +w = np.load(CACHE / 'best_w.npy'); cols = json.loads((CACHE / 'best_cols.json').read_text()) +shrink = Fraction(1) - Fraction(1, 10 ** 6) +while True: + W = [int(Fraction(float(x)) * SCALE * shrink) for x in w] # floor + keep = [(c, k) for c, k in zip(cols, W) if k > 0] + q = np.zeros((len(keep), 56), np.int32) + for i, (c, k) in enumerate(keep): + q[i, c] = 1 + wk = np.array([k for _, k in keep], dtype=np.float64) + touch = ((inside.astype(np.int32) @ q.T) > 0).astype(np.float64) + TW = (touch * wk).T.copy() + worst = None + for b0 in range(0, n, 2048): + L = np.rint(touch[b0:b0 + 2048] @ TW).astype(np.int64) + m = int((T[b0:b0 + 2048].astype(np.int64) * SCALE - L).min()) + worst = m if worst is None else min(worst, m) + LB = Fraction(sum(k * 2 * len(c) for c, k in keep), SCALE) + print('shrink', float(shrink), 'columns', len(keep), 'min slack', worst, 'bound', float(LB), flush=True) + if worst >= 0: + break + shrink *= Fraction(999, 1000) +out = {'schema': 'plane-port-clique-floor-141/certificate/1', 'scale': SCALE, + 'lower_bound_num': LB.numerator, 'lower_bound_den': LB.denominator, + 'columns': [{'clique': sorted(int(i) for i in c), 'w': k} for c, k in sorted(keep, key=lambda t: (len(t[0]), sorted(t[0])))]} +s = '{' + ', '.join('"%s": %s' % (k, json.dumps(v)) for k, v in out.items() if k != 'columns') +s += ', "columns": [\n' + ',\n'.join(json.dumps(c, separators=(',', ':')) for c in out['columns']) + '\n]}\n' +(CACHE / 'CERTIFICATE.json').write_text(s) +print('bound', LB, float(LB)) diff --git a/research/plane-port-clique-floor-141/verify.py b/research/plane-port-clique-floor-141/verify.py new file mode 100644 index 0000000000..23156c1f0b --- /dev/null +++ b/research/plane-port-clique-floor-141/verify.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Exact check of the 141 clique certificate for the strict 56-plane port decoder. + +The certificate is a feasible point of PR5560's clique programme. This script checks, from the +pinned selected archive and the PR1825 matching: + +1. the 56 matched planes, each nondegenerate, and their 109 orthogonal pairs; +2. the closure census: 39,087 subspaces of F2^9 generated by nonempty plane sets; +3. the tariff t(A, R) = dim A - dim(A meet R^perp) for every ordered pair, cross-checked + against Gaussian elimination of the pairing matrix on 4,000 random pairs; +4. every certificate column is a clique of pairwise non-orthogonal planes with a positive + integer weight; +5. feasibility on ALL 39,087^2 ordered pairs (A, R): + sum_{Q : some plane of Q lies in A and some plane of Q lies in R} w_Q <= SCALE * t(A, R); + slack 0 occurs exactly on the tariff-0 pairs; +6. the bound sum_Q 2|Q| w_Q / SCALE = 36732955/262144 > 140, hence every decoder costs >= 141; +7. rejecting controls: an overweight column, a non-clique column, a wrong recorded bound and + PR5560's own certificate (which is feasible but does not reach 140) must each fail. + +All load sums are integers below 2^40 and all census counts are at most 512, so the float64 +and float32 matrix products used here are exact; both facts are asserted. Needs numpy >= 2. +""" +import hashlib, json, random, sys, 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' +PRED = ROOT / 'research/plane-port-global-rank-dual/CERTIFICATE.json' +PRED_SHA = '20ccaf90c909c602bacc101f3dc540848c844903506e8bce70eb06f28c1ec342' +N_SPANS = 39087 +BLOCK = 2048 +T0 = time.time() + + +class Fail(Exception): + pass + + +def need(cond, msg): + if not cond: + raise Fail(msg) + + +def log(*a): + print('%6.1fs' % (time.time() - T0), *a, flush=True) + + +def sha(p): + return hashlib.sha256(p.read_bytes()).hexdigest() + + +def parity(x): + return bin(x).count('1') & 1 + + +def f2_rank(rows): + rank = 0 + rows = [r for r in rows if r] + while rows: + p = rows.pop() + low = p & -p + rows = [r ^ p if r & low else r for r in rows] + rows = [r for r in rows if r] + rank += 1 + return rank + + +def planes(): + 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']] + match = json.loads(MATCHING.read_text())['matching'] + need(len(labels) == 112 and len(match) == 56, 'port and plane counts') + need(sorted(p for e in match for p in e) == list(range(112)), 'perfect matching') + pl = [(labels[a], labels[b]) for a, b in match] + for x, y in pl: + need(f2_rank([x, y]) == 2, 'plane is two-dimensional') + need(parity(x & x) * parity(y & y) ^ parity(x & y) == 1, 'plane Gram is nonsingular over F2') + orth = np.array([[i != j and all(parity(u & v) == 0 for u in pl[i] for v in pl[j]) for j in range(56)] + for i in range(56)]) + need(int(orth.sum()) == 2 * 109, '109 orthogonal plane pairs') + return pl, orth + + +def census(pl): + """subspaces generated by nonempty plane sets, as sorted tuples of basis-reduced generators""" + def reduce(basis, v): + for b in basis: + v = min(v, v ^ b) + return v + + def canon(vectors): + basis = [] + for v in vectors: + v = reduce(basis, v) + if v: + basis = [min(b, b ^ v) for b in basis] + [v] + # fully reduced echelon form is unique for a subspace + basis.sort(reverse=True) + out = [] + for v in basis: + v = reduce(out, v) + out = [min(b, b ^ v) for b in out] + [v] + return tuple(sorted(out)) + + seen = set(); frontier = set() + for x, y in pl: + frontier.add(canon([x, y])) + seen |= frontier + while frontier: + new = set() + for s in frontier: + for x, y in pl: + t = canon(list(s) + [x, y]) + if t not in seen: + seen.add(t); new.add(t) + frontier = new + return sorted(seen, key=lambda b: (len(b), b)) + + +def elements(basis): + els = [0] + for b in basis: + els += [e ^ b for e in els] + return els + + +def main(): + full = '--sampled' not in sys.argv + pl, orth = planes() + log('56 nondegenerate planes, 109 orthogonal pairs') + bases = census(pl) + n = len(bases) + need(n == N_SPANS, 'census size %d' % n) + dim = np.array([len(b) for b in bases], dtype=np.int64) + log('generated subspaces', n, 'by dimension', dict(zip(*map(lambda a: a.tolist(), np.unique(dim, return_counts=True))))) + + S = np.zeros((n, 512), np.float32) + for k, b in enumerate(bases): + S[k, elements(b)] = 1 + pmask = np.zeros((56, 512), np.float32) + for i, (x, y) in enumerate(pl): + pmask[i, [0, x, y, x ^ y]] = 1 + inside = (S @ pmask.T) == 4 # plane i lies in span k + need(all(inside[k].any() for k in range(n)), 'every span contains a plane') + D = np.array([[parity(u & v) for v in range(512)] for u in range(512)], dtype=np.float32) + perpT = ((S @ D) == 0).astype(np.float32).T.copy() # 512 x n: element in R^perp + + def tariffs(r0, r1): + cnt = S[r0:r1] @ perpT # |A meet R^perp| <= 512, exact + c = cnt.astype(np.int64) + need(bool(((c & (c - 1)) == 0).all()) and int(c.min()) >= 1, 'intersections are subspaces') + return dim[r0:r1, None] - np.log2(c).round().astype(np.int64) + + rng = random.Random(141) + for _ in range(40): + a = rng.randrange(n); row = tariffs(a, a + 1)[0] + for _ in range(100): + r = rng.randrange(n) + gram = [sum(parity(u & v) << j for j, v in enumerate(bases[r])) for u in bases[a]] + need(int(row[r]) == f2_rank(gram), 'tariff vs Gaussian elimination') + log('tariff formula matches Gaussian elimination on 4000 random pairs') + + def check(cert, rows): + scale = cert['scale']; cols = cert['columns'] + need(isinstance(scale, int) and scale > 0, 'scale') + q = np.zeros((len(cols), 56), np.float64) + for k, c in enumerate(cols): + Q = c['clique'] + need(len(set(Q)) == len(Q) > 0 and all(isinstance(i, int) and 0 <= i < 56 for i in Q), 'clique indices') + need(not any(orth[i][j] for i in Q for j in Q), 'column is a clique of non-orthogonal planes') + need(isinstance(c['w'], int) and c['w'] > 0, 'positive integer weight') + q[k, Q] = 1 + w = np.array([c['w'] for c in cols], dtype=np.float64) + need(float(w.sum()) < 2 ** 40, 'exact float64 range') + touch = ((inside.astype(np.float64) @ q.T) > 0).astype(np.float64) + TW = (touch * w).T.copy() + worst = None; tight = 0; zero = 0 + for r0 in range(0, len(rows), BLOCK): + rs = rows[r0:r0 + BLOCK] + lo, hi = rs[0], rs[-1] + 1 + if hi - lo == len(rs): + t = tariffs(lo, hi) + else: + t = np.concatenate([tariffs(a, a + 1) for a in rs]) + load = np.rint(touch[rs] @ TW).astype(np.int64) + slack = t * scale - load + m = int(slack.min()); worst = m if worst is None else min(worst, m) + tight += int((slack == 0).sum()); zero += int((t == 0).sum()) + need(m >= 0, 'feasibility violated in rows %d..%d' % (lo, hi)) + LB = Fraction(sum(2 * len(c['clique']) * c['w'] for c in cols), scale) + need(LB == Fraction(cert['lower_bound_num'], cert['lower_bound_den']), 'recorded bound') + return LB, worst, tight, zero + + rows = list(range(n)) if full else list(range(0, n, 97)) + cert = json.loads((HERE / 'CERTIFICATE.json').read_text()) + LB, worst, tight, zero = check(cert, rows) + need(LB > 140, 'bound exceeds 140') + need(tight == zero, 'slack 0 occurs only on tariff-0 pairs') + log('certificate PASSED on', len(rows), 'x', n, 'ordered pairs; min slack', worst, 'tight pairs', tight, '= tariff-0 pairs') + + ctrl = list(range(0, n, 977)) + bad = json.loads(json.dumps(cert)); bad['columns'][-1]['w'] += 10 * cert['scale'] + bad['lower_bound_num'], bad['lower_bound_den'] = Fraction( + sum(2 * len(c['clique']) * c['w'] for c in bad['columns']), bad['scale']).as_integer_ratio() + nonclique = json.loads(json.dumps(cert)) + i, j = map(int, np.argwhere(orth)[0]); 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(c, ctrl) + except Fail: + log('control rejected:', name) + else: + raise SystemExit('FAILED: control accepted: ' + name) + need(sha(PRED) == PRED_SHA, 'PR5560 certificate hash') + pred = json.loads(PRED.read_text()) + pLB = check(pred, ctrl)[0] + need(pLB < 140 < LB, 'PR5560 certificate stays below 140; this one exceeds it') + log('control: PR5560 certificate is feasible on the control rows with bound', float(pLB), '< 140') + + res = {'schema': 'plane-port-clique-floor-141/verify/1', 'planes': 56, 'orthogonal_pairs': 109, + 'generated_subspaces': n, 'ordered_pairs_checked': len(rows) * n, 'complete': full, + 'columns': len(cert['columns']), 'max_clique': max(len(c['clique']) for c in cert['columns']), + 'scale': cert['scale'], 'min_slack': worst, 'tight_pairs': tight, 'tariff_zero_pairs': zero, + 'lower_bound': str(LB), 'lower_bound_float': float(LB), 'integer_floor': 141, + 'new_kappa_claimed': False} + print(json.dumps(res, indent=1)) + print('PASS_PLANE_PORT_CLIQUE_FLOOR_141' + ('' if full else '_SAMPLED')) + + +if __name__ == '__main__': + try: + main() + except Fail as e: + raise SystemExit('FAILED: %s' % e)