files / problems / sidon-second-term / compute / refs / sidon_certificate_8kernel.py
"""Exact rational eight-kernel certificate proving C < 0.9435.
The outer parameters were obtained by numerical search. Every mathematical
check below uses fractions.Fraction; floating point arithmetic is used only
for decimal display.
"""
from fractions import Fraction as F
import hashlib
import math
from pathlib import Path
R = 8
m = 32
L = 4
n = m * L
DL = 100000000
DP = 1000000000000
DQ = 1000000000
ETA = F(17, 250000000000)
EXPECTED_A = F(497329054138522113993707809619, 390625000000000000000000000000)
EXPECTED_B = F(69918675237166718360455326217, 100000000000000000000000000000)
EXPECTED_LEAST_SLACK = F(4735171805469436153, 6250000000000000000000000000000)
EXPECTED_LEAST_SLACK_INDEX = 127
LAMBDA_INTS = [39490874, 8624912, 135342, 12911860, 20451562, 2832639, 9217142, 6335669]
P1_HALF_INTS = [10129562920, 12762809702, 8523333474, 14537214238, 13413387466, 18363618886, 17863905490,
23428409930, 23223647844, 30188836979, 30165622276, 39829682821, 39976283607, 56068050924,
56586355554, 104939277889]
P3_HALF_INTS = [11967783353, 18421100611, 16156102042, 32948516219, 30195555283, 35368894088, 28712630734,
34337026643, 34629857397, 47142409484, 45040510087, 48093467666, 33452257572, 30522523319,
21224235299, 31787130203]
P4_HALF_INTS = [989749957, 2699286232, 10823110362, 30629258034, 44646942089, 41341340451, 36239315220,
36823902420, 40214086819, 40646291716, 37180033707, 33970981059, 33576685061, 35289675485,
37074922956, 37854418432]
P5_HALF_INTS = [18996388126, 21678444172, 27164790473, 33945843122, 37406362358, 34592808215, 29578349046,
27961370310, 31992840518, 40021084581, 44592708954, 39843498311, 31479649882, 26630217365,
26294193576, 27821450991]
P6_HALF_INTS = [18040424358, 19475685735, 21837587060, 24559188198, 27651554398, 31485881495, 35599206229,
38164868020, 37879307570, 36097439406, 35318483998, 36381566702, 37611362690, 36491265383,
33108334899, 30297843859]
P7_HALF_INTS = [28481668153, 28198172999, 27981785340, 28322381466, 29512765605, 31318813715, 32909494070,
33431314629, 32937368727, 32429578006, 32804719353, 33896740055, 34437774991, 33286951203,
30936368937, 29114102751]
P8_HALF_INTS = [11399726890, 14408044846, 20624654356, 28429268964, 33425769790, 33434725937, 31876368574,
33072560906, 38542261053, 45575443730, 47488957142, 41663194985, 33778271463, 29107308579,
28209991261, 28963451524]
W1_INTS = [177948558, 224207461, 151086561, 264951210, 257921514, 345740370, 344377520, 453100201, 462200024,
600303571, 609215015, 799811930, 818528053, 1132131211, 1161069268, 2047825324, 2069605653,
1295278068, 1340667310, 1150926867, 1142917859, 1013777220, 1041588697, 979405871, 1005833816,
934216502, 962461487, 920142979, 974199711, 900962640, 986640033, 938333867, 861172294, 886550165,
853780461, 900783667, 922108552, 955337906, 958996360, 975547225, 996893710, 1025827408,
1031860260, 1050801279, 1065552035, 1073134394, 1043234125, 1111336291, 1089173218, 1018811114,
1018382059, 1001143919, 994776284, 985019093, 985357085, 982591803, 982541517, 980646070,
981469552, 980708341, 981991946, 988437739, 983508714, 980588123, 993162208, 991056105, 989793284,
996182832, 1001329623, 1005118766, 1005807311, 1006247549, 1009344942, 1011256838, 1010053921,
1010068864, 1010054254, 1008527418, 1004080111, 1006753394, 1003830023, 998308641, 997828399,
996055029, 995543508, 995324380, 996170223, 995896679, 995957065, 996868391, 997451965, 997327424,
997659673, 1000036352, 998534460, 998597820, 1001398051, 1000611533, 1000667144, 1001374938,
1001810027, 1001883149, 1001821488, 1001676946, 1001593129, 1001454164, 1001078984, 1001017744,
1000197296, 1000251095, 999802283, 999262350, 999261783, 999052003, 998950247, 998883208,
998962818, 999118069, 999373154, 999439782, 999507222, 999794323, 999844457, 999961816, 999971584,
1000314673, 1000201885, 1000074049]
W2_INTS = [548976542, 548976542, 553156871, 577420797, 612082315, 613388625, 636491923, 644945137, 683006011,
693611850, 720906054, 728188872, 765756925, 780770778, 820970224, 820970224, 846705735, 892251108,
919550464, 926141712, 968976371, 990585181, 1036264020, 1049762178, 1090235668, 1114704007,
1162600891, 1182847378, 1230979411, 1263774423, 1303010725, 1322679699, 854781928, 866295032,
902850081, 894557750, 900374171, 912696134, 931233442, 939259144, 942928531, 948082474, 963860446,
973672553, 976595847, 980699054, 989468985, 997042449, 1018257647, 995177247, 1010348721,
1020676453, 1023433042, 1020652268, 1020833096, 1024970225, 1029570333, 1024267160, 1021989163,
1020182649, 1017648335, 1002715135, 1009646249, 1006741056, 972053585, 977385300, 981181955,
982042141, 985753676, 988812548, 991955474, 992944698, 995573373, 997023402, 999054667, 999426033,
1003489769, 1001922011, 999014804, 1007495551, 1006195511, 1001796844, 1004185735, 1004787642,
1004510116, 1003278906, 1002584126, 1002524461, 1002610926, 1000967139, 1000433326, 999578891,
999140874, 998296114, 997681496, 997975998, 996662077, 997113576, 997575734, 998066426, 998850229,
999433815, 999741804, 999694356, 1000361279, 1000519294, 1000579702, 1000446717, 1001085368,
1000708754, 1000134097, 1000727921, 1000570612, 1000617857, 1000441588, 1000649039, 1000582199,
1000573939, 1000279535, 1000352347, 1000219519, 1000146620, 999932296, 999875425, 999841289,
999729062, 999816314, 999912481]
W3_INTS = [210241034, 323608068, 285419210, 590571334, 560191332, 659218439, 561561677, 685460588, 706026932,
950768782, 923475211, 1016157700, 781683583, 778254269, 626180859, 848478804, 840036946, 714451536,
877754208, 975919562, 1235712109, 1230888030, 1286287409, 1130682678, 1146300367, 1097649487,
1233522126, 1189077324, 1270158492, 1024057304, 1089797770, 1005233323, 850597379, 875317364,
879267989, 913818464, 918973168, 946350473, 944091651, 961632098, 961088940, 982045294, 980828527,
995054544, 982958594, 993185054, 972692202, 1012715550, 1017128031, 1008030392, 1018610101,
1028656493, 1039906077, 1037511865, 1033473061, 1023405563, 1017407423, 1011473285, 1008990450,
1007922498, 1006007107, 987161529, 990365531, 984190657, 978142283, 982394860, 984105770,
987515227, 990923309, 994603919, 996254469, 997815453, 998919070, 1001040883, 1001295554,
1000807371, 1004796667, 1003106534, 1000868018, 1006495253, 1005171375, 1003947373, 1004230705,
1004120704, 1003945049, 1002983079, 1001884660, 1000787017, 999770095, 998885273, 998705425,
997944851, 998081554, 997593124, 997163817, 997371342, 997794135, 998356695, 998694746, 999200479,
999699266, 1000204368, 1000379156, 1000481977, 1000627167, 1000797438, 1000761363, 1000532094,
1000978813, 1000688290, 1000294398, 1000619861, 1000196510, 1000404569, 999998462, 1000070209,
1000211137, 1000053748, 1000026183, 999854830, 999880513, 999778191, 1000200358, 999959427,
1000426845, 999988609, 1000170851, 999856249]
W4_INTS = [17387184, 47419034, 190264678, 539201386, 788965426, 741789822, 679228702, 723779616, 804136507,
824023757, 785301380, 762004139, 786546421, 835645782, 884685195, 925106856, 960392349, 978850571,
968365203, 960202715, 1010622992, 1106569991, 1187616423, 1205007315, 1188284325, 1225706780,
1352561166, 1437859448, 1229290543, 932653697, 840749865, 841876222, 839606132, 856258948,
887048756, 928605562, 950314166, 947001996, 951312094, 967536578, 978947184, 978428699, 976601551,
988353567, 1006796214, 1006338672, 1001258191, 1011607436, 1024124545, 1026651293, 1020145876,
1017874988, 1026743127, 1032872451, 1031846451, 1027959017, 1021626641, 1013244652, 1011861600,
1012774568, 995433618, 975606831, 972397310, 974686473, 977390395, 982940117, 988324646, 992078164,
994574170, 995954398, 997483886, 999566403, 1002084710, 1002337225, 1000238168, 1002864707,
1006907063, 1005234571, 1003375235, 1004480427, 1005257978, 1004784587, 1003325274, 1002434956,
1002890986, 1002593961, 1001428643, 1000352688, 999477841, 998757825, 998007728, 997570331,
997062350, 996524921, 996668457, 997182286, 997869195, 998921159, 999688320, 999869555, 1000153960,
1000515172, 1000669514, 1000728720, 1000937656, 1000989403, 1000618464, 1000765164, 1001113196,
1000748234, 1000414762, 1000390400, 1000229460, 999981046, 999622672, 999527633, 999948111,
1000053523, 999886147, 999895538, 999970241, 1000092623, 1000035947, 999970939, 1000012533,
1000001045, 1000054424, 1000153344]
W5_INTS = [333714287, 380830635, 479751805, 613984690, 698663073, 658172558, 596051871, 584828643, 684835089,
834994517, 937486421, 872003523, 766624526, 708168932, 735270283, 765822383, 787533922, 798108274,
830684124, 927179943, 1107286926, 1215271427, 1178004060, 1065585124, 1038996130, 1094692538,
1221523285, 1296646634, 1279887232, 1199525338, 1146968904, 1126818636, 850892714, 866191720,
897753251, 904079914, 915024680, 926677915, 940628285, 944578223, 948324532, 960478630, 977271712,
981280665, 977292912, 976298959, 984132249, 996029266, 1015082040, 1004454488, 1013669976,
1022524939, 1033078011, 1036985385, 1031368306, 1024872861, 1021621193, 1016782620, 1019169248,
1020467644, 1013823250, 997050391, 995921460, 992954543, 973870758, 979066396, 983370629,
984758963, 987308272, 990885789, 994289342, 995045409, 996846009, 998124731, 999660073, 1000497600,
1003260335, 1002272686, 1000708902, 1006195372, 1005947701, 1003433883, 1004495719, 1004642785,
1004576712, 1003744503, 1002688729, 1001862763, 1001239240, 999847952, 999582581, 999194765,
998642708, 997711933, 997163929, 997444934, 996958478, 997588655, 998197765, 998590950, 999095257,
999705180, 1000075674, 1000052303, 1000491337, 1000591561, 1000597669, 1000584028, 1001009991,
1000743905, 1000341278, 1000653086, 1000517498, 1000440547, 1000252446, 1000404568, 1000452362,
1000475651, 1000218177, 1000137614, 999971241, 999948855, 1000010575, 1000115759, 1000035780,
999884488, 999900808, 999946967]
W6_INTS = [316920633, 342134228, 386039614, 448050064, 523814659, 595717269, 686521042, 743565166, 769726473,
756864868, 772000269, 806478823, 859239165, 859160560, 836648329, 802676139, 829634096, 913392004,
997393107, 1033835103, 1052495370, 1062524412, 1117536128, 1171915730, 1216436983, 1203114974,
1176758169, 1139377714, 1129010174, 1114757938, 1108989088, 1107050508, 847118901, 864448867,
896575274, 903849957, 917149817, 931648019, 949070434, 959980041, 966020478, 969689648, 978139638,
985564195, 991396460, 996087303, 1000170270, 1003297019, 1016833889, 1008358574, 1021556587,
1028730272, 1028383826, 1024089915, 1022529205, 1024243552, 1024987970, 1017381008, 1010244269,
1004499934, 1000540577, 991115666, 994658004, 993670883, 975799255, 980699055, 984811926,
987317969, 990943441, 993596817, 995939609, 997052169, 999177411, 1000355238, 1001467640,
1001640194, 1004136585, 1003460845, 1001680448, 1006099679, 1005192717, 1002739449, 1004016065,
1004044014, 1003403578, 1002191445, 1001344561, 1000954479, 1000701701, 999455100, 998835185,
998144418, 997918621, 997663603, 997592608, 998039831, 997589519, 998117940, 998640299, 999143315,
999725793, 1000123456, 1000318231, 1000295354, 1000683235, 1000763363, 1000749778, 1000606210,
1000907763, 1000652288, 1000260440, 1000494673, 1000311318, 1000263049, 1000102845, 1000166536,
1000078865, 1000055654, 999927845, 1000050117, 1000050556, 1000048157, 999951426, 999961347,
1000020131, 1000041073, 1000116711, 1000141423]
W7_INTS = [500344567, 495364337, 495373008, 523432889, 575686570, 608167560, 657339926, 675536258, 704261173,
708212832, 742470682, 770236975, 816086246, 812732730, 812441943, 784384833, 810120319, 884217437,
950711541, 978686550, 1011996091, 1017256310, 1056916539, 1081718494, 1130335163, 1146848846,
1166904193, 1158232754, 1185217491, 1211751432, 1252782585, 1277050996, 852763717, 865406430,
901073991, 896139098, 904287394, 918210634, 937365516, 945972078, 949558698, 953990730, 968327253,
977888131, 981261970, 984617799, 991263662, 997236176, 1017111323, 998007940, 1014398006,
1024959076, 1026429773, 1021899825, 1020689578, 1024128392, 1028197681, 1022368377, 1018423770,
1015020087, 1011996867, 998747475, 1006034689, 1004272332, 973113925, 978318661, 982144951,
983403971, 987221823, 990261793, 993221731, 994133438, 996557307, 997917468, 999761587, 1000064691,
1003756282, 1002258873, 999496996, 1007179005, 1005969951, 1001978080, 1004207029, 1004717776,
1004295292, 1002947614, 1002143402, 1002008445, 1002056922, 1000516401, 999964137, 999137112,
998774944, 998118599, 997690565, 998073490, 996948086, 997401303, 997858853, 998352987, 999103830,
999645374, 999915635, 999853583, 1000449734, 1000585885, 1000627044, 1000483243, 1001045945,
1000683150, 1000139359, 1000667007, 1000511530, 1000539760, 1000355007, 1000516071, 1000429664,
1000414533, 1000164214, 1000262243, 1000163148, 1000107173, 999923290, 999899992, 999916975,
999855008, 999936778, 999992363]
W8_INTS = [200261845, 253109717, 363843393, 510202697, 613789086, 623630570, 618431663, 657550406, 778598700,
916305704, 974207516, 896572150, 797309256, 743517706, 756831041, 781957071, 805388376, 824903352,
866450543, 965810391, 1136022366, 1266204447, 1272236576, 1181998180, 1130430131, 1144973559,
1212198863, 1240989466, 1193138078, 1095076480, 1027346306, 1002680844, 845456356, 864169237,
894441603, 909792364, 924701701, 937864590, 952407726, 960110403, 966109249, 976196487, 986911618,
988633248, 985919982, 985524886, 991534184, 1001698673, 1016540873, 1013112157, 1020097837,
1026791152, 1035076989, 1039186327, 1034652908, 1025696696, 1017970093, 1011124775, 1009945055,
1008448253, 1001740801, 989047322, 986952113, 985714040, 976285186, 981362518, 985901145,
988392844, 990861780, 993765743, 996886946, 998129935, 999428432, 1000338040, 1001336927,
1001939978, 1003729252, 1003174065, 1002221822, 1005503132, 1005465758, 1003929313, 1004277450,
1004084632, 1003790574, 1002969136, 1001899136, 1000839426, 999914862, 998755459, 998441786,
998156773, 997844211, 997352283, 997167163, 997579104, 997609915, 998286443, 998900064, 999317456,
999709594, 1000133162, 1000448575, 1000486908, 1000717576, 1000745716, 1000716357, 1000673257,
1000896814, 1000691333, 1000385308, 1000502521, 1000355465, 1000223321, 1000027040, 1000083375,
1000113373, 1000108102, 999943152, 999901494, 999837933, 999922368, 1000064553, 1000174736,
1000154931, 1000081596, 1000087088, 1000105532]
def require(condition, message):
if not condition:
raise RuntimeError(message)
def symmetric_kernel(half):
values = [F(x, DP) for x in half]
return values + list(reversed(values))
lambdas = [F(x, DL) for x in LAMBDA_INTS]
kernels = [
symmetric_kernel(P1_HALF_INTS),
[F(1, m) for _ in range(m)],
symmetric_kernel(P3_HALF_INTS),
symmetric_kernel(P4_HALF_INTS),
symmetric_kernel(P5_HALF_INTS),
symmetric_kernel(P6_HALF_INTS),
symmetric_kernel(P7_HALF_INTS),
symmetric_kernel(P8_HALF_INTS),
]
weights = [
[F(x, DQ) + ETA for x in W1_INTS],
[F(x, DQ) + ETA for x in W2_INTS],
[F(x, DQ) + ETA for x in W3_INTS],
[F(x, DQ) + ETA for x in W4_INTS],
[F(x, DQ) + ETA for x in W5_INTS],
[F(x, DQ) + ETA for x in W6_INTS],
[F(x, DQ) + ETA for x in W7_INTS],
[F(x, DQ) + ETA for x in W8_INTS],
]
require(len(lambdas) == R, "wrong number of mixing weights")
require(len(kernels) == R, "wrong number of kernels")
require(len(weights) == R, "wrong number of boundary vectors")
require(all(x > 0 for x in lambdas), "a mixing weight is not positive")
require(sum(lambdas) == 1, "mixing weights do not sum to one")
for r, p in enumerate(kernels, start=1):
require(len(p) == m, f"kernel {r} has wrong length")
require(all(x >= 0 for x in p), f"kernel {r} has a negative entry")
require(sum(p) == 1, f"kernel {r} is not a probability vector")
require(p == list(reversed(p)), f"kernel {r} is not symmetric")
for r, w in enumerate(weights, start=1):
require(len(w) == n, f"boundary vector {r} has wrong length")
slacks = []
for q in range(n + 1):
total = F(0)
for lam, p, w in zip(lambdas, kernels, weights):
for i in range(m):
j = q + i
total += lam * p[i] * (w[j] if j < n else F(1))
slacks.append(total - 1)
require(all(s >= 0 for s in slacks), "a covering inequality failed")
require(slacks[n] == 0, "the final covering constraint is not equality")
positive = [(s, q) for q, s in enumerate(slacks) if s > 0]
least_positive, least_positive_index = min(positive)
require(
least_positive_index == EXPECTED_LEAST_SLACK_INDEX
and least_positive == EXPECTED_LEAST_SLACK,
("unexpected least positive slack", least_positive_index, least_positive),
)
a = F(m) * sum(
lam * sum(x * x for x in p)
for lam, p in zip(lambdas, kernels)
)
b = F(1) + F(2) * (
F(1, m) * sum(
lam * sum(x * x for x in w)
for lam, w in zip(lambdas, weights)
)
- L
)
require(a == EXPECTED_A, ("unexpected a", a))
require(b == EXPECTED_B, ("unexpected b", b))
require(b > 0, "b is not positive")
require(a * b < F(9435, 10000) ** 2, "C is not below 0.9435")
print("minimum constraint index =", min(range(n + 1), key=slacks.__getitem__))
print("minimum slack =", min(slacks))
print("least positive slack index =", least_positive_index)
print("least positive slack =", least_positive)
print("a =", a)
print("b =", b)
print("C^2 =", a * b)
print("C =", math.sqrt(float(a * b)))
print("Certified C < 0.9435")
path = Path(__file__)
digest = hashlib.sha256(path.read_bytes()).hexdigest()
print("SHA-256 =", digest)