From a692ebd1aa88be3dee73d42688fadf407f3a7d42 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Tue, 13 Oct 2026 20:21:49 +0000 Subject: [PATCH 1/2] Research: extend CK target forest floor to all dyadic weights --- .../ck-all-dyadic-forest-seed23/CLAIM.json | 21 + .../ck-all-dyadic-forest-seed23/EXPECTED.json | 2329 +++++++++++++++++ .../ck-all-dyadic-forest-seed23/README.md | 209 ++ .../ck-all-dyadic-forest-seed23/SOURCES.json | 20 + .../ck-all-dyadic-forest-seed23/VALIDATION.md | 88 + .../independent.py | 111 + .../test_package.py | 60 + .../ck-all-dyadic-forest-seed23/verify.py | 326 +++ 8 files changed, 3164 insertions(+) create mode 100644 research/ck-all-dyadic-forest-seed23/CLAIM.json create mode 100644 research/ck-all-dyadic-forest-seed23/EXPECTED.json create mode 100644 research/ck-all-dyadic-forest-seed23/README.md create mode 100644 research/ck-all-dyadic-forest-seed23/SOURCES.json create mode 100644 research/ck-all-dyadic-forest-seed23/VALIDATION.md create mode 100755 research/ck-all-dyadic-forest-seed23/independent.py create mode 100755 research/ck-all-dyadic-forest-seed23/test_package.py create mode 100755 research/ck-all-dyadic-forest-seed23/verify.py diff --git a/research/ck-all-dyadic-forest-seed23/CLAIM.json b/research/ck-all-dyadic-forest-seed23/CLAIM.json new file mode 100644 index 0000000000..9ec168fe70 --- /dev/null +++ b/research/ck-all-dyadic-forest-seed23/CLAIM.json @@ -0,0 +1,21 @@ +{ + "track": "complex supplier", + "assignment_seed": 23, + "seed_source": "secrets.randbelow(100), operating-system randomness", + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "scope": "Historical PR626 CK compensation, arbitrary nonzero dyadic single-parent target forest weights, independent binary-Horner coefficient lowering", + "candidates": [ + {"task": "Selected k8 rank-seven ends / owner packing", "decision": "Rejected: crowded by PR1090 and PR1117 through PR1169"}, + {"task": "Contracted factory fixed-order diagonal scales", "decision": "Rejected: complex-factory-scale-frontier27 closes this class; PR1064/1106 also overlap"}, + {"task": "CK nonunit target-parent coefficients", "decision": "Chosen after coefficient-domain refinement below"} + ], + "pivot": "Initial fixed-topology signed-power-of-two hypothesis had no gains, but deeper all-state PR-body search identified PR964 already closing all power-of-two CK forests. That duplicate was abandoned. Exactly one pivot changes the coefficient class to arbitrary dyadic numerators, explicitly left open by PR964. PR961 supplies credited universal tails for the different X4 matrix, not CK census results.", + "domain": "All 12432 ordered distinct CK target pairs and 1086 signed coefficients n/8, 1<=abs(n)<=543; written universal tails for reduced denominator exponent >=4 or magnitude >=68", + "stopping_rule": "Complete deterministic finite core and tail proof, no optimizer restarts or time-limited search", + "method": "Exact integer coefficient-pair histograms, fully paid root/unit dominance, inherited forest exchange lemma, independent Prim/cycle check, all-column rational endpoint controls", + "optimistic_budget": "E(i,j,lambda)=R(C_i-lambda*C_j)+2H(lambda). Both target-boundary shears, residual coefficient work and clears charged. Other local stages and all recursive children fixed; any exclusion cannot change kappa.", + "expected_deliverable": "Exact scoped exclusion or concrete nonunit improving edge with complete cost; no hosted supplier or kappa claim", + "coordination": "No pinned sprint coordination issue existed; open issues913 and650 were unrelated. Discussions1163,1166,1167 had no comments/claims on entry. Local claim and parent reservation; parent approved the overlap-driven pivot.", + "expected_finish": "2026-10-13T22:30:00Z", + "status": "research in progress" +} diff --git a/research/ck-all-dyadic-forest-seed23/EXPECTED.json b/research/ck-all-dyadic-forest-seed23/EXPECTED.json new file mode 100644 index 0000000000..2342f5f2c4 --- /dev/null +++ b/research/ck-all-dyadic-forest-seed23/EXPECTED.json @@ -0,0 +1,2329 @@ +{ + "controls": { + "columns": 716, + "mixed_nonunit_edges": 106, + "orientations": 2, + "rejected": [ + "omitted_preparation", + "omitted_restoration", + "sign_error", + "nonunit_stale_residual", + "reversed_preparation", + "reversed_restoration", + "root_only_domination", + "alphabet_only_domination", + "non_dyadic_coefficient", + "denominator_tail_started_too_early" + ], + "witness_additions": 3342 + }, + "cycle_inequalities": 12544, + "finite": { + "coefficient_count": 1086, + "finite_cases": 13501152, + "group_costs_sha256": "b52788e8fc41293379c05dc693baf494426302e8733d98bc2930435685f0f571", + "histogram_groups": 8275, + "margin_histogram": { + "100": 11, + "1000": 11564, + "1001": 10807, + "1002": 11177, + "1003": 10602, + "1004": 11387, + "1005": 10537, + "1006": 11738, + "1007": 10462, + "1008": 11460, + "1009": 10992, + "101": 4, + "1010": 11704, + "1011": 10285, + "1012": 11200, + "1013": 10881, + "1014": 10978, + "1015": 11283, + "1016": 11984, + "1017": 10754, + "1018": 11292, + "1019": 11261, + "102": 13, + "1020": 11590, + "1021": 11170, + "1022": 11672, + "1023": 10941, + "1024": 11603, + "1025": 11617, + "1026": 12011, + "1027": 10969, + "1028": 11625, + "1029": 10895, + "103": 3, + "1030": 11916, + "1031": 11459, + "1032": 12372, + "1033": 11680, + "1034": 11412, + "1035": 11424, + "1036": 12236, + "1037": 11979, + "1038": 11980, + "1039": 11169, + "104": 3, + "1040": 11980, + "1041": 11774, + "1042": 12054, + "1043": 11280, + "1044": 12390, + "1045": 11632, + "1046": 12703, + "1047": 11640, + "1048": 12855, + "1049": 11632, + "105": 12, + "1050": 12608, + "1051": 12078, + "1052": 12227, + "1053": 12121, + "1054": 12664, + "1055": 12275, + "1056": 13007, + "1057": 11884, + "1058": 12940, + "1059": 12697, + "106": 8, + "1060": 12790, + "1061": 12343, + "1062": 13372, + "1063": 12256, + "1064": 13087, + "1065": 12226, + "1066": 13779, + "1067": 12576, + "1068": 12549, + "1069": 13316, + "107": 8, + "1070": 13248, + "1071": 12603, + "1072": 13494, + "1073": 12527, + "1074": 14416, + "1075": 13025, + "1076": 13345, + "1077": 12949, + "1078": 12705, + "1079": 13789, + "1080": 13928, + "1081": 12993, + "1082": 13583, + "1083": 13039, + "1084": 13826, + "1085": 13371, + "1086": 13683, + "1087": 12500, + "1088": 13434, + "1089": 13337, + "1090": 13933, + "1091": 13136, + "1092": 14193, + "1093": 13401, + "1094": 13224, + "1095": 13084, + "1096": 14123, + "1097": 13357, + "1098": 14954, + "1099": 13634, + "110": 2, + "1100": 14476, + "1101": 13438, + "1102": 13840, + "1103": 12854, + "1104": 13899, + "1105": 14000, + "1106": 15492, + "1107": 13097, + "1108": 14147, + "1109": 13415, + "111": 6, + "1110": 13878, + "1111": 12962, + "1112": 14616, + "1113": 14638, + "1114": 14415, + "1115": 14619, + "1116": 14935, + "1117": 14470, + "1118": 14743, + "1119": 14791, + "112": 17, + "1120": 15482, + "1121": 14672, + "1122": 14587, + "1123": 14217, + "1124": 14911, + "1125": 14629, + "1126": 15039, + "1127": 14903, + "1128": 14742, + "1129": 14547, + "113": 10, + "1130": 16132, + "1131": 15122, + "1132": 15903, + "1133": 15044, + "1134": 16160, + "1135": 15017, + "1136": 15834, + "1137": 15459, + "1138": 16371, + "1139": 15473, + "114": 5, + "1140": 15386, + "1141": 14990, + "1142": 15951, + "1143": 14908, + "1144": 16157, + "1145": 15126, + "1146": 15550, + "1147": 15409, + "1148": 16093, + "1149": 15687, + "115": 3, + "1150": 16282, + "1151": 14497, + "1152": 16676, + "1153": 14942, + "1154": 16220, + "1155": 15386, + "1156": 16004, + "1157": 15363, + "1158": 16247, + "1159": 15680, + "1160": 15527, + "1161": 14624, + "1162": 16614, + "1163": 15261, + "1164": 16662, + "1165": 16047, + "1166": 16471, + "1167": 15080, + "1168": 16547, + "1169": 15694, + "117": 2, + "1170": 16880, + "1171": 15531, + "1172": 17298, + "1173": 15661, + "1174": 15631, + "1175": 15217, + "1176": 15907, + "1177": 15445, + "1178": 16703, + "1179": 15480, + "1180": 16598, + "1181": 16741, + "1182": 17343, + "1183": 16004, + "1184": 16424, + "1185": 16350, + "1186": 17135, + "1187": 16655, + "1188": 16787, + "1189": 16811, + "1190": 17386, + "1191": 16756, + "1192": 17247, + "1193": 16630, + "1194": 17617, + "1195": 16930, + "1196": 18270, + "1197": 16995, + "1198": 18068, + "1199": 17023, + "1200": 18823, + "1201": 17322, + "1202": 17636, + "1203": 17413, + "1204": 17549, + "1205": 17092, + "1206": 18305, + "1207": 17043, + "1208": 18669, + "1209": 17193, + "121": 8, + "1210": 19047, + "1211": 16804, + "1212": 18274, + "1213": 18077, + "1214": 17993, + "1215": 17651, + "1216": 18222, + "1217": 17175, + "1218": 18197, + "1219": 17072, + "122": 4, + "1220": 18376, + "1221": 16988, + "1222": 18413, + "1223": 17309, + "1224": 18044, + "1225": 17535, + "1226": 18250, + "1227": 17123, + "1228": 17961, + "1229": 18023, + "123": 6, + "1230": 18563, + "1231": 16864, + "1232": 18146, + "1233": 16593, + "1234": 18371, + "1235": 18100, + "1236": 18201, + "1237": 17313, + "1238": 18342, + "1239": 17556, + "124": 32, + "1240": 18255, + "1241": 17453, + "1242": 18567, + "1243": 17511, + "1244": 18544, + "1245": 17251, + "1246": 17454, + "1247": 17524, + "1248": 18138, + "1249": 17074, + "125": 8, + "1250": 18651, + "1251": 17391, + "1252": 18041, + "1253": 16943, + "1254": 18478, + "1255": 18185, + "1256": 19448, + "1257": 17378, + "1258": 18900, + "1259": 17740, + "126": 2, + "1260": 19346, + "1261": 18448, + "1262": 19591, + "1263": 18408, + "1264": 19788, + "1265": 18740, + "1266": 19176, + "1267": 18040, + "1268": 19351, + "1269": 19319, + "127": 27, + "1270": 19958, + "1271": 18108, + "1272": 18866, + "1273": 18829, + "1274": 19745, + "1275": 19199, + "1276": 20309, + "1277": 18629, + "1278": 20200, + "1279": 20088, + "128": 2, + "1280": 20358, + "1281": 20015, + "1282": 19274, + "1283": 19096, + "1284": 20017, + "1285": 19512, + "1286": 20500, + "1287": 18515, + "1288": 19407, + "1289": 18482, + "129": 8, + "1290": 19108, + "1291": 18508, + "1292": 18917, + "1293": 18989, + "1294": 19257, + "1295": 18718, + "1296": 19265, + "1297": 17826, + "1298": 19675, + "1299": 18967, + "130": 7, + "1300": 19990, + "1301": 17821, + "1302": 20417, + "1303": 18003, + "1304": 18846, + "1305": 18336, + "1306": 17572, + "1307": 18272, + "1308": 19205, + "1309": 18110, + "131": 18, + "1310": 19281, + "1311": 18030, + "1312": 19066, + "1313": 17378, + "1314": 19428, + "1315": 18151, + "1316": 19065, + "1317": 18376, + "1318": 18711, + "1319": 17826, + "132": 12, + "1320": 18876, + "1321": 18389, + "1322": 18033, + "1323": 17896, + "1324": 18953, + "1325": 17872, + "1326": 18431, + "1327": 17220, + "1328": 19241, + "1329": 18549, + "133": 12, + "1330": 19443, + "1331": 19637, + "1332": 18797, + "1333": 18000, + "1334": 19862, + "1335": 17600, + "1336": 19026, + "1337": 18949, + "1338": 19597, + "1339": 18475, + "134": 17, + "1340": 19401, + "1341": 19193, + "1342": 19454, + "1343": 18064, + "1344": 18670, + "1345": 18217, + "1346": 18433, + "1347": 18624, + "1348": 20454, + "1349": 18884, + "135": 20, + "1350": 19383, + "1351": 18331, + "1352": 20145, + "1353": 18875, + "1354": 19266, + "1355": 17800, + "1356": 18946, + "1357": 17405, + "1358": 20285, + "1359": 18153, + "136": 10, + "1360": 18212, + "1361": 17786, + "1362": 18304, + "1363": 17335, + "1364": 18460, + "1365": 17030, + "1366": 19344, + "1367": 16622, + "1368": 18372, + "1369": 17257, + "137": 23, + "1370": 17992, + "1371": 16871, + "1372": 17235, + "1373": 16945, + "1374": 18325, + "1375": 17554, + "1376": 17971, + "1377": 15921, + "1378": 17270, + "1379": 16687, + "138": 13, + "1380": 17787, + "1381": 16408, + "1382": 16512, + "1383": 16101, + "1384": 17099, + "1385": 15774, + "1386": 16737, + "1387": 15663, + "1388": 16859, + "1389": 16241, + "139": 19, + "1390": 16927, + "1391": 16280, + "1392": 16477, + "1393": 16585, + "1394": 16532, + "1395": 15973, + "1396": 17012, + "1397": 16153, + "1398": 17061, + "1399": 15680, + "140": 26, + "1400": 17289, + "1401": 15698, + "1402": 16831, + "1403": 15649, + "1404": 16419, + "1405": 16206, + "1406": 17426, + "1407": 15261, + "1408": 16315, + "1409": 15389, + "141": 34, + "1410": 16555, + "1411": 15841, + "1412": 16368, + "1413": 16530, + "1414": 16689, + "1415": 15813, + "1416": 16705, + "1417": 16265, + "1418": 15887, + "1419": 14280, + "142": 54, + "1420": 16545, + "1421": 15572, + "1422": 15717, + "1423": 14974, + "1424": 16422, + "1425": 14784, + "1426": 15630, + "1427": 15032, + "1428": 15624, + "1429": 14329, + "143": 32, + "1430": 15711, + "1431": 15202, + "1432": 15600, + "1433": 13659, + "1434": 14516, + "1435": 14590, + "1436": 14953, + "1437": 14563, + "1438": 14837, + "1439": 13686, + "144": 69, + "1440": 13764, + "1441": 13842, + "1442": 14316, + "1443": 12991, + "1444": 13758, + "1445": 13798, + "1446": 14310, + "1447": 13433, + "1448": 14265, + "1449": 13212, + "145": 36, + "1450": 13138, + "1451": 12810, + "1452": 13958, + "1453": 12475, + "1454": 13596, + "1455": 12428, + "1456": 12818, + "1457": 12419, + "1458": 13221, + "1459": 12773, + "146": 71, + "1460": 13326, + "1461": 12007, + "1462": 12891, + "1463": 12246, + "1464": 13095, + "1465": 12191, + "1466": 12813, + "1467": 11786, + "1468": 12724, + "1469": 12405, + "147": 36, + "1470": 12787, + "1471": 12019, + "1472": 12565, + "1473": 11120, + "1474": 12639, + "1475": 12523, + "1476": 13117, + "1477": 11445, + "1478": 12221, + "1479": 11958, + "148": 56, + "1480": 12496, + "1481": 11977, + "1482": 12201, + "1483": 10920, + "1484": 12493, + "1485": 11530, + "1486": 12438, + "1487": 11553, + "1488": 12037, + "1489": 11534, + "149": 56, + "1490": 11857, + "1491": 11146, + "1492": 11614, + "1493": 11258, + "1494": 11473, + "1495": 10960, + "1496": 12330, + "1497": 11264, + "1498": 11156, + "1499": 11237, + "150": 74, + "1500": 11947, + "1501": 10711, + "1502": 10387, + "1503": 10260, + "1504": 10922, + "1505": 10509, + "1506": 10524, + "1507": 10195, + "1508": 10279, + "1509": 9884, + "151": 45, + "1510": 10221, + "1511": 9922, + "1512": 10277, + "1513": 10156, + "1514": 10666, + "1515": 9605, + "1516": 10747, + "1517": 9726, + "1518": 9954, + "1519": 9207, + "152": 78, + "1520": 9811, + "1521": 9348, + "1522": 9774, + "1523": 8846, + "1524": 9629, + "1525": 9083, + "1526": 9367, + "1527": 8722, + "1528": 9854, + "1529": 8838, + "153": 106, + "1530": 9481, + "1531": 8609, + "1532": 9474, + "1533": 8796, + "1534": 8942, + "1535": 9234, + "1536": 8845, + "1537": 8818, + "1538": 9257, + "1539": 8702, + "154": 84, + "1540": 9142, + "1541": 8604, + "1542": 9262, + "1543": 7897, + "1544": 9321, + "1545": 8454, + "1546": 8960, + "1547": 8340, + "1548": 8899, + "1549": 8120, + "155": 73, + "1550": 8238, + "1551": 8305, + "1552": 8407, + "1553": 7857, + "1554": 8351, + "1555": 7509, + "1556": 8100, + "1557": 7596, + "1558": 8606, + "1559": 7360, + "156": 57, + "1560": 8076, + "1561": 7385, + "1562": 7944, + "1563": 7416, + "1564": 8052, + "1565": 7531, + "1566": 8271, + "1567": 7287, + "1568": 8141, + "1569": 7251, + "157": 86, + "1570": 7828, + "1571": 7321, + "1572": 8129, + "1573": 6962, + "1574": 7990, + "1575": 6853, + "1576": 7356, + "1577": 6706, + "1578": 7706, + "1579": 6863, + "158": 104, + "1580": 7097, + "1581": 6529, + "1582": 6885, + "1583": 6652, + "1584": 6946, + "1585": 6167, + "1586": 6973, + "1587": 6171, + "1588": 6652, + "1589": 6132, + "159": 82, + "1590": 6871, + "1591": 6341, + "1592": 6507, + "1593": 6159, + "1594": 6550, + "1595": 6518, + "1596": 6806, + "1597": 6528, + "1598": 6752, + "1599": 5804, + "160": 106, + "1600": 6386, + "1601": 6085, + "1602": 6661, + "1603": 6063, + "1604": 6526, + "1605": 5901, + "1606": 6083, + "1607": 5666, + "1608": 6532, + "1609": 5850, + "161": 94, + "1610": 6292, + "1611": 5782, + "1612": 6708, + "1613": 5671, + "1614": 6177, + "1615": 5455, + "1616": 5903, + "1617": 5895, + "1618": 5936, + "1619": 5588, + "162": 70, + "1620": 5782, + "1621": 5563, + "1622": 6068, + "1623": 5553, + "1624": 5685, + "1625": 5580, + "1626": 5476, + "1627": 4981, + "1628": 5370, + "1629": 5181, + "163": 91, + "1630": 5900, + "1631": 5107, + "1632": 5595, + "1633": 5301, + "1634": 5557, + "1635": 5216, + "1636": 5402, + "1637": 5056, + "1638": 5291, + "1639": 4860, + "164": 110, + "1640": 5250, + "1641": 4999, + "1642": 5783, + "1643": 4773, + "1644": 5091, + "1645": 4752, + "1646": 5321, + "1647": 4680, + "1648": 4616, + "1649": 4386, + "165": 82, + "1650": 5375, + "1651": 4531, + "1652": 5148, + "1653": 4250, + "1654": 4703, + "1655": 4506, + "1656": 4634, + "1657": 4317, + "1658": 4435, + "1659": 3956, + "166": 112, + "1660": 4913, + "1661": 4392, + "1662": 4529, + "1663": 4174, + "1664": 4317, + "1665": 4181, + "1666": 4661, + "1667": 4115, + "1668": 4148, + "1669": 3841, + "167": 83, + "1670": 4418, + "1671": 3695, + "1672": 4717, + "1673": 3959, + "1674": 4017, + "1675": 3753, + "1676": 4415, + "1677": 3860, + "1678": 4438, + "1679": 4114, + "168": 132, + "1680": 4309, + "1681": 4012, + "1682": 4093, + "1683": 3722, + "1684": 4346, + "1685": 4092, + "1686": 4090, + "1687": 3468, + "1688": 4018, + "1689": 3661, + "169": 101, + "1690": 4083, + "1691": 3733, + "1692": 4098, + "1693": 3958, + "1694": 4462, + "1695": 3865, + "1696": 4081, + "1697": 3734, + "1698": 4104, + "1699": 3662, + "170": 145, + "1700": 4012, + "1701": 3689, + "1702": 4184, + "1703": 3570, + "1704": 3988, + "1705": 3639, + "1706": 3995, + "1707": 3737, + "1708": 4109, + "1709": 3607, + "171": 108, + "1710": 3702, + "1711": 3148, + "1712": 3985, + "1713": 3073, + "1714": 4010, + "1715": 3233, + "1716": 3869, + "1717": 3377, + "1718": 3824, + "1719": 3368, + "172": 150, + "1720": 3427, + "1721": 3302, + "1722": 3282, + "1723": 3341, + "1724": 3675, + "1725": 3253, + "1726": 3521, + "1727": 3153, + "1728": 3625, + "1729": 3415, + "173": 111, + "1730": 3434, + "1731": 3078, + "1732": 3348, + "1733": 3301, + "1734": 3469, + "1735": 2957, + "1736": 3476, + "1737": 3243, + "1738": 3191, + "1739": 3000, + "174": 145, + "1740": 3496, + "1741": 2883, + "1742": 3404, + "1743": 2959, + "1744": 3304, + "1745": 2600, + "1746": 3576, + "1747": 2735, + "1748": 3342, + "1749": 2975, + "175": 83, + "1750": 3019, + "1751": 2795, + "1752": 2969, + "1753": 2571, + "1754": 2739, + "1755": 2680, + "1756": 2892, + "1757": 2600, + "1758": 3368, + "1759": 2751, + "176": 132, + "1760": 3234, + "1761": 2731, + "1762": 3064, + "1763": 2626, + "1764": 3134, + "1765": 2635, + "1766": 2751, + "1767": 2381, + "1768": 3220, + "1769": 2764, + "177": 103, + "1770": 3013, + "1771": 2543, + "1772": 2803, + "1773": 2802, + "1774": 3185, + "1775": 2620, + "1776": 3080, + "1777": 2569, + "1778": 2834, + "1779": 2341, + "178": 124, + "1780": 2874, + "1781": 2480, + "1782": 3136, + "1783": 2652, + "1784": 2843, + "1785": 2432, + "1786": 2614, + "1787": 3018, + "1788": 2781, + "1789": 2443, + "179": 121, + "1790": 2829, + "1791": 2445, + "1792": 2697, + "1793": 2743, + "1794": 2818, + "1795": 2611, + "1796": 2767, + "1797": 2608, + "1798": 2651, + "1799": 2625, + "180": 161, + "1800": 2931, + "1801": 2653, + "1802": 2697, + "1803": 2299, + "1804": 3138, + "1805": 2751, + "1806": 2577, + "1807": 2349, + "1808": 2750, + "1809": 2263, + "181": 97, + "1810": 2625, + "1811": 2536, + "1812": 2611, + "1813": 2427, + "1814": 2765, + "1815": 2562, + "1816": 2724, + "1817": 2479, + "1818": 2736, + "1819": 2291, + "182": 147, + "1820": 2576, + "1821": 2529, + "1822": 2459, + "1823": 2313, + "1824": 2393, + "1825": 2367, + "1826": 2313, + "1827": 2523, + "1828": 2527, + "1829": 2643, + "183": 108, + "1830": 2320, + "1831": 2245, + "1832": 2341, + "1833": 2197, + "1834": 2392, + "1835": 2261, + "1836": 2508, + "1837": 2154, + "1838": 2689, + "1839": 2171, + "184": 187, + "1840": 2289, + "1841": 2177, + "1842": 2424, + "1843": 2076, + "1844": 2548, + "1845": 2036, + "1846": 2233, + "1847": 2128, + "1848": 2380, + "1849": 1887, + "185": 91, + "1850": 2112, + "1851": 2182, + "1852": 2479, + "1853": 2119, + "1854": 2185, + "1855": 1890, + "1856": 2129, + "1857": 1900, + "1858": 2290, + "1859": 1991, + "186": 157, + "1860": 2168, + "1861": 2018, + "1862": 2224, + "1863": 1857, + "1864": 2114, + "1865": 1965, + "1866": 2012, + "1867": 1782, + "1868": 2302, + "1869": 1855, + "187": 104, + "1870": 2160, + "1871": 1815, + "1872": 2170, + "1873": 1736, + "1874": 1826, + "1875": 1875, + "1876": 1937, + "1877": 1907, + "1878": 2261, + "1879": 1779, + "188": 154, + "1880": 2223, + "1881": 1817, + "1882": 1868, + "1883": 1991, + "1884": 1848, + "1885": 1946, + "1886": 1747, + "1887": 1824, + "1888": 1941, + "1889": 1835, + "189": 119, + "1890": 2000, + "1891": 1909, + "1892": 2017, + "1893": 1679, + "1894": 1937, + "1895": 1700, + "1896": 1975, + "1897": 2050, + "1898": 2025, + "1899": 1850, + "190": 171, + "1900": 1982, + "1901": 1857, + "1902": 2059, + "1903": 1765, + "1904": 1904, + "1905": 1677, + "1906": 1918, + "1907": 1577, + "1908": 1990, + "1909": 1897, + "191": 120, + "1910": 1984, + "1911": 1562, + "1912": 1713, + "1913": 1693, + "1914": 1934, + "1915": 1625, + "1916": 1792, + "1917": 1865, + "1918": 1659, + "1919": 1694, + "192": 188, + "1920": 1650, + "1921": 1569, + "1922": 1673, + "1923": 1591, + "1924": 1624, + "1925": 1738, + "1926": 1486, + "1927": 1718, + "1928": 1573, + "1929": 1519, + "193": 126, + "1930": 1532, + "1931": 1603, + "1932": 1599, + "1933": 1449, + "1934": 1631, + "1935": 1520, + "1936": 1624, + "1937": 1474, + "1938": 1701, + "1939": 1425, + "194": 169, + "1940": 1774, + "1941": 1525, + "1942": 1402, + "1943": 1363, + "1944": 1462, + "1945": 1325, + "1946": 1360, + "1947": 1356, + "1948": 1488, + "1949": 1397, + "195": 176, + "1950": 1530, + "1951": 1263, + "1952": 1419, + "1953": 1191, + "1954": 1360, + "1955": 1202, + "1956": 1323, + "1957": 1227, + "1958": 1196, + "1959": 1144, + "196": 209, + "1960": 1314, + "1961": 1423, + "1962": 1111, + "1963": 1003, + "1964": 1231, + "1965": 1101, + "1966": 1335, + "1967": 1076, + "1968": 1235, + "1969": 1135, + "197": 186, + "1970": 1251, + "1971": 994, + "1972": 1184, + "1973": 1117, + "1974": 1063, + "1975": 1050, + "1976": 1175, + "1977": 1172, + "1978": 1285, + "1979": 1011, + "198": 181, + "1980": 962, + "1981": 1165, + "1982": 1121, + "1983": 1093, + "1984": 1174, + "1985": 1061, + "1986": 1201, + "1987": 994, + "1988": 1081, + "1989": 1028, + "199": 155, + "1990": 1157, + "1991": 1009, + "1992": 1063, + "1993": 1044, + "1994": 1079, + "1995": 877, + "1996": 1064, + "1997": 1061, + "1998": 988, + "1999": 1003, + "200": 209, + "2000": 1148, + "2001": 1046, + "2002": 935, + "2003": 1013, + "2004": 1128, + "2005": 989, + "2006": 913, + "2007": 910, + "2008": 981, + "2009": 856, + "201": 180, + "2010": 823, + "2011": 904, + "2012": 1007, + "2013": 785, + "2014": 918, + "2015": 732, + "2016": 901, + "2017": 829, + "2018": 807, + "2019": 919, + "202": 225, + "2020": 829, + "2021": 878, + "2022": 769, + "2023": 855, + "2024": 882, + "2025": 774, + "2026": 937, + "2027": 808, + "2028": 895, + "2029": 749, + "203": 154, + "2030": 796, + "2031": 773, + "2032": 793, + "2033": 722, + "2034": 732, + "2035": 725, + "2036": 802, + "2037": 754, + "2038": 729, + "2039": 630, + "204": 233, + "2040": 723, + "2041": 688, + "2042": 596, + "2043": 607, + "2044": 696, + "2045": 615, + "2046": 727, + "2047": 621, + "2048": 656, + "2049": 574, + "205": 197, + "2050": 574, + "2051": 516, + "2052": 587, + "2053": 514, + "2054": 567, + "2055": 522, + "2056": 553, + "2057": 447, + "2058": 562, + "2059": 462, + "206": 242, + "2060": 548, + "2061": 572, + "2062": 565, + "2063": 456, + "2064": 524, + "2065": 510, + "2066": 461, + "2067": 420, + "2068": 638, + "2069": 424, + "207": 248, + "2070": 528, + "2071": 384, + "2072": 477, + "2073": 407, + "2074": 456, + "2075": 339, + "2076": 449, + "2077": 482, + "2078": 461, + "2079": 444, + "208": 250, + "2080": 463, + "2081": 418, + "2082": 401, + "2083": 451, + "2084": 428, + "2085": 386, + "2086": 390, + "2087": 399, + "2088": 463, + "2089": 375, + "209": 210, + "2090": 447, + "2091": 361, + "2092": 440, + "2093": 397, + "2094": 376, + "2095": 384, + "2096": 366, + "2097": 332, + "2098": 426, + "2099": 380, + "210": 271, + "2100": 317, + "2101": 338, + "2102": 443, + "2103": 350, + "2104": 331, + "2105": 377, + "2106": 428, + "2107": 327, + "2108": 337, + "2109": 297, + "211": 293, + "2110": 308, + "2111": 335, + "2112": 375, + "2113": 272, + "2114": 352, + "2115": 235, + "2116": 306, + "2117": 300, + "2118": 299, + "2119": 216, + "212": 288, + "2120": 295, + "2121": 244, + "2122": 273, + "2123": 311, + "2124": 301, + "2125": 256, + "2126": 233, + "2127": 241, + "2128": 268, + "2129": 245, + "213": 323, + "2130": 252, + "2131": 277, + "2132": 280, + "2133": 206, + "2134": 241, + "2135": 210, + "2136": 214, + "2137": 216, + "2138": 228, + "2139": 194, + "214": 310, + "2140": 251, + "2141": 182, + "2142": 174, + "2143": 197, + "2144": 196, + "2145": 205, + "2146": 151, + "2147": 161, + "2148": 235, + "2149": 188, + "215": 298, + "2150": 198, + "2151": 115, + "2152": 170, + "2153": 143, + "2154": 119, + "2155": 129, + "2156": 192, + "2157": 155, + "2158": 161, + "2159": 111, + "216": 314, + "2160": 143, + "2161": 100, + "2162": 121, + "2163": 96, + "2164": 148, + "2165": 95, + "2166": 110, + "2167": 101, + "2168": 151, + "2169": 113, + "217": 208, + "2170": 106, + "2171": 98, + "2172": 116, + "2173": 83, + "2174": 137, + "2175": 96, + "2176": 79, + "2177": 88, + "2178": 154, + "2179": 78, + "218": 346, + "2180": 135, + "2181": 108, + "2182": 119, + "2183": 87, + "2184": 113, + "2185": 111, + "2186": 116, + "2187": 96, + "2188": 97, + "2189": 79, + "219": 318, + "2190": 133, + "2191": 85, + "2192": 108, + "2193": 70, + "2194": 135, + "2195": 77, + "2196": 150, + "2197": 62, + "2198": 74, + "2199": 92, + "220": 355, + "2200": 93, + "2201": 56, + "2202": 58, + "2203": 65, + "2204": 79, + "2205": 80, + "2206": 73, + "2207": 50, + "2208": 91, + "2209": 52, + "221": 322, + "2210": 59, + "2211": 36, + "2212": 86, + "2213": 59, + "2214": 36, + "2215": 49, + "2216": 74, + "2217": 64, + "2218": 59, + "2219": 40, + "222": 300, + "2220": 88, + "2221": 43, + "2222": 52, + "2223": 39, + "2224": 86, + "2225": 47, + "2226": 73, + "2227": 32, + "2228": 42, + "2229": 47, + "223": 355, + "2230": 46, + "2231": 37, + "2232": 39, + "2233": 35, + "2234": 54, + "2235": 39, + "2236": 35, + "2237": 31, + "2238": 23, + "2239": 29, + "224": 358, + "2240": 38, + "2241": 20, + "2242": 20, + "2243": 31, + "2244": 44, + "2245": 14, + "2246": 18, + "2247": 23, + "2248": 54, + "2249": 19, + "225": 333, + "2250": 36, + "2251": 15, + "2252": 23, + "2253": 19, + "2254": 31, + "2255": 13, + "2256": 24, + "2257": 16, + "2258": 16, + "2259": 15, + "226": 350, + "2260": 32, + "2261": 18, + "2262": 17, + "2263": 2, + "2264": 6, + "2265": 8, + "2266": 5, + "2267": 14, + "2268": 15, + "2269": 12, + "227": 373, + "2270": 32, + "2271": 1, + "2272": 21, + "2273": 7, + "2274": 15, + "2275": 12, + "2276": 7, + "2277": 1, + "2278": 5, + "2279": 8, + "228": 359, + "2280": 25, + "2281": 8, + "2282": 10, + "2283": 1, + "2284": 20, + "2285": 4, + "2286": 16, + "2287": 5, + "2288": 34, + "2289": 4, + "229": 305, + "2290": 16, + "2291": 3, + "2292": 28, + "2293": 3, + "2294": 29, + "2296": 10, + "2297": 6, + "2298": 7, + "2299": 2, + "230": 337, + "2300": 2, + "2301": 4, + "2302": 26, + "2303": 3, + "2304": 1, + "2306": 19, + "2307": 1, + "2308": 5, + "231": 345, + "2310": 11, + "2311": 2, + "2312": 7, + "2314": 2, + "2316": 8, + "2317": 3, + "232": 426, + "2320": 25, + "2323": 1, + "2324": 27, + "2327": 1, + "2328": 18, + "2329": 2, + "233": 339, + "2332": 9, + "2334": 3, + "2335": 3, + "2336": 1, + "234": 351, + "2340": 7, + "2342": 4, + "2344": 4, + "2346": 3, + "2348": 8, + "235": 383, + "2350": 4, + "2352": 1, + "2356": 2, + "236": 410, + "237": 337, + "2370": 2, + "2374": 3, + "2376": 2, + "2378": 3, + "238": 428, + "2380": 14, + "2382": 11, + "2384": 2, + "2386": 2, + "2388": 2, + "239": 387, + "2390": 2, + "2392": 5, + "2394": 7, + "2396": 2, + "2398": 4, + "240": 480, + "2402": 2, + "2404": 1, + "2406": 2, + "241": 416, + "2410": 2, + "2414": 12, + "2416": 2, + "2418": 4, + "242": 466, + "2420": 3, + "2422": 2, + "2424": 1, + "2428": 8, + "243": 399, + "2432": 4, + "2436": 1, + "244": 524, + "2440": 1, + "2442": 1, + "2448": 1, + "245": 374, + "246": 397, + "247": 455, + "2472": 1, + "248": 571, + "2484": 3, + "249": 476, + "2490": 3, + "2496": 1, + "250": 494, + "251": 541, + "2514": 2, + "252": 631, + "2520": 1, + "2526": 2, + "253": 521, + "2532": 1, + "254": 564, + "255": 466, + "256": 528, + "257": 524, + "258": 540, + "259": 577, + "260": 542, + "261": 537, + "262": 628, + "263": 596, + "264": 601, + "265": 568, + "266": 679, + "267": 545, + "268": 661, + "269": 623, + "270": 625, + "271": 655, + "272": 658, + "273": 549, + "274": 632, + "275": 552, + "276": 640, + "277": 512, + "278": 674, + "279": 585, + "280": 604, + "281": 585, + "282": 731, + "283": 613, + "284": 546, + "285": 564, + "286": 619, + "287": 514, + "288": 602, + "289": 616, + "290": 543, + "291": 607, + "292": 550, + "293": 557, + "294": 534, + "295": 629, + "296": 565, + "297": 548, + "298": 632, + "299": 528, + "300": 579, + "301": 585, + "302": 639, + "303": 549, + "304": 518, + "305": 590, + "306": 520, + "307": 536, + "308": 556, + "309": 575, + "310": 533, + "311": 459, + "312": 546, + "313": 483, + "314": 553, + "315": 521, + "316": 591, + "317": 490, + "318": 575, + "319": 549, + "320": 586, + "321": 529, + "322": 551, + "323": 521, + "324": 612, + "325": 520, + "326": 595, + "327": 549, + "328": 593, + "329": 521, + "330": 536, + "331": 546, + "332": 628, + "333": 634, + "334": 740, + "335": 672, + "336": 706, + "337": 632, + "338": 719, + "339": 738, + "340": 875, + "341": 748, + "342": 927, + "343": 776, + "344": 877, + "345": 794, + "346": 907, + "347": 819, + "348": 1037, + "349": 804, + "350": 884, + "351": 965, + "352": 960, + "353": 921, + "354": 998, + "355": 978, + "356": 1018, + "357": 923, + "358": 984, + "359": 1016, + "360": 1153, + "361": 1128, + "362": 1141, + "363": 1041, + "364": 1130, + "365": 996, + "366": 1209, + "367": 1141, + "368": 1157, + "369": 1100, + "370": 1173, + "371": 1081, + "372": 1142, + "373": 1154, + "374": 1181, + "375": 1074, + "376": 1159, + "377": 1085, + "378": 1271, + "379": 1085, + "380": 1110, + "381": 1172, + "382": 1210, + "383": 1207, + "384": 1164, + "385": 1114, + "386": 1201, + "387": 1164, + "388": 1148, + "389": 1188, + "390": 1158, + "391": 1059, + "392": 1302, + "393": 1074, + "394": 1076, + "395": 1125, + "396": 1233, + "397": 1130, + "398": 1145, + "399": 1125, + "400": 1208, + "401": 1217, + "402": 1109, + "403": 1128, + "404": 1178, + "405": 1118, + "406": 1207, + "407": 1164, + "408": 1331, + "409": 1305, + "410": 1487, + "411": 1222, + "412": 1319, + "413": 1343, + "414": 1333, + "415": 1351, + "416": 1440, + "417": 1432, + "418": 1548, + "419": 1458, + "420": 1444, + "421": 1474, + "422": 1415, + "423": 1466, + "424": 1624, + "425": 1539, + "426": 1552, + "427": 1529, + "428": 1691, + "429": 1493, + "430": 1629, + "431": 1636, + "432": 1625, + "433": 1691, + "434": 1600, + "435": 1690, + "436": 1770, + "437": 1804, + "438": 1816, + "439": 1786, + "440": 1826, + "441": 1626, + "442": 1790, + "443": 1793, + "444": 1840, + "445": 1639, + "446": 1805, + "447": 1810, + "448": 1778, + "449": 1851, + "450": 1943, + "451": 1843, + "452": 1854, + "453": 1927, + "454": 2033, + "455": 1843, + "456": 1836, + "457": 1980, + "458": 1896, + "459": 1830, + "460": 2011, + "461": 1806, + "462": 2021, + "463": 1859, + "464": 1861, + "465": 2033, + "466": 1978, + "467": 1912, + "468": 2165, + "469": 1817, + "470": 1987, + "471": 1909, + "472": 1872, + "473": 1950, + "474": 2051, + "475": 2016, + "476": 1933, + "477": 1938, + "478": 2156, + "479": 2029, + "480": 2092, + "481": 2031, + "482": 2041, + "483": 2028, + "484": 2148, + "485": 2168, + "486": 2149, + "487": 1994, + "488": 2298, + "489": 2253, + "490": 2234, + "491": 2157, + "492": 2428, + "493": 2334, + "494": 2484, + "495": 2225, + "496": 2444, + "497": 2254, + "498": 2312, + "499": 2312, + "500": 2564, + "501": 2451, + "502": 2561, + "503": 2506, + "504": 2654, + "505": 2368, + "506": 2693, + "507": 2509, + "508": 2589, + "509": 2549, + "510": 2868, + "511": 2756, + "512": 2864, + "513": 2602, + "514": 2792, + "515": 2707, + "516": 2709, + "517": 2506, + "518": 2912, + "519": 2669, + "520": 3007, + "521": 2735, + "522": 2919, + "523": 2929, + "524": 2977, + "525": 2958, + "526": 3066, + "527": 2819, + "528": 3070, + "529": 2761, + "530": 2885, + "531": 2753, + "532": 3041, + "533": 2976, + "534": 2773, + "535": 2838, + "536": 3150, + "537": 3113, + "538": 3088, + "539": 3112, + "540": 3219, + "541": 3078, + "542": 2920, + "543": 3003, + "544": 3129, + "545": 2932, + "546": 3307, + "547": 3293, + "548": 3329, + "549": 3192, + "550": 3489, + "551": 3253, + "552": 3417, + "553": 3148, + "554": 3601, + "555": 3250, + "556": 3636, + "557": 3312, + "558": 3739, + "559": 3535, + "560": 3631, + "561": 3618, + "562": 3642, + "563": 3288, + "564": 3780, + "565": 3566, + "566": 3563, + "567": 3696, + "568": 3961, + "569": 3570, + "570": 3743, + "571": 3939, + "572": 3828, + "573": 3784, + "574": 4122, + "575": 3850, + "576": 4229, + "577": 3757, + "578": 4115, + "579": 4220, + "580": 4290, + "581": 4007, + "582": 4119, + "583": 4082, + "584": 4498, + "585": 4153, + "586": 4369, + "587": 4266, + "588": 4471, + "589": 4203, + "590": 4639, + "591": 4446, + "592": 4469, + "593": 4024, + "594": 4547, + "595": 4132, + "596": 4544, + "597": 4346, + "598": 4640, + "599": 4300, + "600": 4639, + "601": 4308, + "602": 4578, + "603": 4358, + "604": 4400, + "605": 4325, + "606": 4747, + "607": 4319, + "608": 4565, + "609": 4264, + "610": 4782, + "611": 4731, + "612": 4831, + "613": 4404, + "614": 4678, + "615": 4668, + "616": 5024, + "617": 4618, + "618": 4820, + "619": 4441, + "620": 5078, + "621": 4622, + "622": 4982, + "623": 4609, + "624": 4709, + "625": 4576, + "626": 4732, + "627": 4787, + "628": 5103, + "629": 4912, + "63": 4, + "630": 5064, + "631": 5070, + "632": 4999, + "633": 5025, + "634": 5782, + "635": 5022, + "636": 5385, + "637": 4922, + "638": 5251, + "639": 4925, + "640": 5304, + "641": 4974, + "642": 5294, + "643": 5035, + "644": 5821, + "645": 4910, + "646": 5381, + "647": 5318, + "648": 5435, + "649": 5361, + "650": 5678, + "651": 5388, + "652": 5768, + "653": 5405, + "654": 5675, + "655": 5473, + "656": 5813, + "657": 5140, + "658": 5516, + "659": 5534, + "66": 2, + "660": 5874, + "661": 5489, + "662": 6005, + "663": 5539, + "664": 5897, + "665": 5533, + "666": 6116, + "667": 5668, + "668": 6088, + "669": 5852, + "670": 6055, + "671": 5598, + "672": 5977, + "673": 5663, + "674": 6007, + "675": 5804, + "676": 6102, + "677": 5499, + "678": 5928, + "679": 5932, + "680": 5818, + "681": 6023, + "682": 6178, + "683": 5754, + "684": 6260, + "685": 5804, + "686": 6342, + "687": 5937, + "688": 5715, + "689": 5724, + "690": 6187, + "691": 5614, + "692": 6156, + "693": 5972, + "694": 6016, + "695": 5859, + "696": 5950, + "697": 5833, + "698": 6215, + "699": 6137, + "70": 2, + "700": 6077, + "701": 5644, + "702": 6274, + "703": 5747, + "704": 6252, + "705": 6021, + "706": 6355, + "707": 5857, + "708": 6303, + "709": 5831, + "710": 6298, + "711": 5798, + "712": 6375, + "713": 5954, + "714": 6351, + "715": 5953, + "716": 6138, + "717": 6055, + "718": 6311, + "719": 5828, + "720": 6154, + "721": 5948, + "722": 6782, + "723": 5973, + "724": 6631, + "725": 6210, + "726": 6506, + "727": 5926, + "728": 6519, + "729": 6114, + "730": 6538, + "731": 6220, + "732": 6237, + "733": 6299, + "734": 6398, + "735": 6090, + "736": 6485, + "737": 6124, + "738": 6594, + "739": 6475, + "74": 4, + "740": 6691, + "741": 6336, + "742": 6893, + "743": 6188, + "744": 6717, + "745": 6377, + "746": 6716, + "747": 6529, + "748": 6456, + "749": 6701, + "750": 6484, + "751": 6566, + "752": 6833, + "753": 6432, + "754": 6777, + "755": 6194, + "756": 6693, + "757": 6562, + "758": 6972, + "759": 6659, + "760": 6915, + "761": 6303, + "762": 6970, + "763": 6513, + "764": 6657, + "765": 6583, + "766": 6827, + "767": 6846, + "768": 7038, + "769": 6633, + "770": 7029, + "771": 6324, + "772": 7197, + "773": 6578, + "774": 6939, + "775": 7080, + "776": 6460, + "777": 6741, + "778": 7087, + "779": 6390, + "780": 6852, + "781": 6720, + "782": 7116, + "783": 6541, + "784": 7000, + "785": 6456, + "786": 6987, + "787": 6803, + "788": 7188, + "789": 6700, + "790": 6937, + "791": 6615, + "792": 6867, + "793": 6615, + "794": 6903, + "795": 6416, + "796": 6935, + "797": 6543, + "798": 7190, + "799": 6734, + "800": 7164, + "801": 6725, + "802": 6686, + "803": 6735, + "804": 6858, + "805": 6671, + "806": 7378, + "807": 6656, + "808": 7107, + "809": 6797, + "810": 7208, + "811": 6951, + "812": 6931, + "813": 6626, + "814": 6987, + "815": 6521, + "816": 7097, + "817": 7270, + "818": 7482, + "819": 6882, + "820": 7390, + "821": 6868, + "822": 7464, + "823": 6744, + "824": 7034, + "825": 7651, + "826": 7172, + "827": 7281, + "828": 7401, + "829": 7192, + "830": 7451, + "831": 7252, + "832": 7612, + "833": 7152, + "834": 7572, + "835": 7231, + "836": 7533, + "837": 7259, + "838": 7648, + "839": 7514, + "840": 7927, + "841": 7307, + "842": 7486, + "843": 7623, + "844": 7843, + "845": 7330, + "846": 8087, + "847": 7341, + "848": 7990, + "849": 7168, + "850": 8262, + "851": 7437, + "852": 7821, + "853": 7511, + "854": 7880, + "855": 7588, + "856": 7635, + "857": 7368, + "858": 7721, + "859": 7607, + "860": 8000, + "861": 7571, + "862": 8026, + "863": 7599, + "864": 7598, + "865": 7577, + "866": 8208, + "867": 7775, + "868": 8147, + "869": 7483, + "870": 8050, + "871": 8056, + "872": 8092, + "873": 7691, + "874": 8248, + "875": 7805, + "876": 8269, + "877": 7811, + "878": 8174, + "879": 7776, + "88": 4, + "880": 8558, + "881": 8206, + "882": 8446, + "883": 7809, + "884": 8126, + "885": 7585, + "886": 8173, + "887": 8221, + "888": 8274, + "889": 7924, + "890": 8684, + "891": 7947, + "892": 8364, + "893": 8167, + "894": 8778, + "895": 8160, + "896": 8469, + "897": 8080, + "898": 8799, + "899": 8164, + "90": 1, + "900": 8996, + "901": 8210, + "902": 8643, + "903": 8222, + "904": 9033, + "905": 8612, + "906": 9091, + "907": 8607, + "908": 8963, + "909": 8715, + "910": 9224, + "911": 8764, + "912": 9437, + "913": 8663, + "914": 9365, + "915": 8941, + "916": 9271, + "917": 8339, + "918": 9236, + "919": 8821, + "92": 1, + "920": 9280, + "921": 8896, + "922": 9115, + "923": 9029, + "924": 9305, + "925": 9328, + "926": 9445, + "927": 9115, + "928": 9600, + "929": 9351, + "93": 2, + "930": 9382, + "931": 8796, + "932": 9514, + "933": 9509, + "934": 10183, + "935": 8741, + "936": 9815, + "937": 9134, + "938": 9271, + "939": 9206, + "94": 2, + "940": 9747, + "941": 9609, + "942": 10369, + "943": 9191, + "944": 9691, + "945": 9140, + "946": 10123, + "947": 9657, + "948": 9510, + "949": 10193, + "95": 1, + "950": 10132, + "951": 9515, + "952": 10157, + "953": 10011, + "954": 10287, + "955": 9473, + "956": 10595, + "957": 9466, + "958": 9783, + "959": 9782, + "960": 10106, + "961": 10355, + "962": 10218, + "963": 10227, + "964": 10225, + "965": 9547, + "966": 10352, + "967": 9706, + "968": 10004, + "969": 9983, + "970": 10172, + "971": 10219, + "972": 10322, + "973": 10064, + "974": 10699, + "975": 10186, + "976": 10134, + "977": 10207, + "978": 10723, + "979": 10288, + "98": 8, + "980": 10595, + "981": 10451, + "982": 10841, + "983": 10404, + "984": 11229, + "985": 10506, + "986": 11280, + "987": 10677, + "988": 10791, + "989": 10537, + "99": 6, + "990": 10592, + "991": 10994, + "992": 10570, + "993": 10761, + "994": 11433, + "995": 10575, + "996": 11474, + "997": 10409, + "998": 11569, + "999": 10678 + }, + "minimum_domination": [ + 63, + 123, + 125, + -24 + ], + "minimum_root_margin": [ + -116, + 114, + 184, + -24 + ], + "nonunit_cases": 13476288, + "nonunit_edges_beating_root": 941, + "ordered_pairs": 12432 + }, + "format": "ck-all-dyadic-forest-v1", + "literal_coefficient_cases": 4409, + "seed": 23, + "signed_floor": 16364, + "tail": { + "argument": "coordinatewise root domination plus two strictly positive boundary shears", + "denominator_exponent_from": 4, + "magnitude_from": 68, + "max_entry_price": 8 + } +} diff --git a/research/ck-all-dyadic-forest-seed23/README.md b/research/ck-all-dyadic-forest-seed23/README.md new file mode 100644 index 0000000000..2f1bae2702 --- /dev/null +++ b/research/ck-all-dyadic-forest-seed23/README.md @@ -0,0 +1,209 @@ +# CK target forests: arbitrary dyadic numerators do not lower the floor + +**Scoped negative complex-supplier result; no new κ.** The historical PR626 CK +single-parent target-forest floor remains **16,364 primitives per real component** +when each edge may use **any nonzero dyadic rational**, not just a signed power +of two. The existing PR816 witness attains this floor. No new circuit saving, +selected-supplier admission, runtime improvement or global circuit optimum is +claimed. + +This closes the explicitly unexamined non-power numerator class in +[Gareth Davidson's PR964](https://github.com/CrocSwap/integer-mult-bounds/pull/964). +It credits and adapts the universal tail reduction and forest-exchange argument +from [woklerx's PR961](https://github.com/CrocSwap/integer-mult-bounds/pull/961), +which checks the **different X4 matrix**, not this CK matrix. The new evidence +is the complete CK all-dyadic finite core, including a concrete reason the +stronger root-only domination argument from the power class cannot be reused. + +## Exact evidence and reproduction + +From the repository root, Python 3.10+ and the standard library suffice: + +```sh +python3 -I -O -B research/ck-all-dyadic-forest-seed23/verify.py && python3 -I -O -B research/ck-all-dyadic-forest-seed23/independent.py +``` + +Expected output: + +```text +PASS_CK_ALL_DYADIC_FOREST cases=13501152 floor=16364 margin=63 columns=716x2 controls=10 no_new_kappa +PASS_CK_PACKED_ORACLE cases=13501152 exact_lane_bits=20 full_receipt_match +``` + +The finite core covers all **12,432 ordered distinct target pairs** and **1,086 +coefficients** `n/8`, `1 <= abs(n) <= 543`: **13,501,152** cases, of which +**13,476,288** are nonunit. The core's minimum excess over the cheaper same-parent +signed-unit/root alternative is **63** component primitives; a witness is +child123, parent125, coefficient `-3`. This margin is a finite-core statement, +not a claimed uniform bound on the infinite tails. + +Root-only domination is false: child114, parent184, coefficient `-3` costs +**116 less than making child114 a root**, while still losing to a same-parent +signed-unit alternative. This is a concrete counterexample to extending PR964's +root-only comparison unchanged, not a counterexample to its correctly scoped +power-of-two theorem. There are **941** finite nonunit directed +edge/coefficient cases beating their root. `EXPECTED.json` records the exact +complete margin histogram, root-winning census, witness tie-breaking, and +per-histogram cost stream digest. + +The primary implementation uses gcd-reduced rational prices, sparse ordered +coefficient histograms and 16-bit packed cost vectors decoded by `struct`. The separate +oracle reads the dense CK matrix afresh, uses integer repeated division for +prices, and extracts 20-bit lanes by masking. Both check explicit no-carry +bounds; they share the histogram/packing idea, not implementation code. The +oracle reproduces every certificate field in the finite census, including +the full cost-stream digest. These are two AI-written implementations, not +independent human review. All 4,409 possible finite-core scalar coefficient +numerators receive a separate literal binary-Horner operation-count check. + +Dense Prim and all **12,544** signed-unit/root cycle inequalities recheck the +existing attaining witness. Exact sparse dyadic-integer replay checks **all 716 +arbitrary input columns in both orientations**, both for the original unit witness and +for a mixed nonunit forest with all106 parent edges changed, including overlapping +ancestor/descendant branches. Ten controls reject missing or misordered boundary +work, wrong signs, stale residuals, overstrong root/alphabet claims, non-dyadic +inputs and an invalid denominator-tail threshold. Private work is initially +cleared and finally cleared by the explicitly charged lowering; the panel +replay is on logical registers, not a fresh native primitive/frame emission. + +`--record` explicitly regenerates only this package's receipt. Default execution +compares every regenerated receipt field and never writes research artifacts. +This is complete deterministic coverage, not a timed optimizer or a failed search. + +## Cost class and proof + +Let `C` be the frozen CK quarter-grid matrix, with 112 target rows and492 helper +columns. Its 8,704 nonzeros are `a/4`, where `0 < abs(a) <= 4`. The compensated +map is `(y,h) -> (y+C h,h)` with arbitrary initial target and helper dirt. + +For reduced dyadic `q=n/2^d`, the retained independent binary-Horner lowering is + +``` +H(0)=0; H(q)=3+floor(log2(abs(n)))+popcount(abs(n))+d. +``` + +This includes initial coefficient-work CLEAR, numerator doublings and source +access additions, denominator halvings, signed target accumulation, and final +CLEAR. There is no cross-ADD work reuse. In particular `H(±1)=4`; this is the +historical tariff, **not** the stronger PR696 copy/unit tariff. Put +`R(v)=sum H(v_h)`. + +Choose any acyclic one-parent target forest and any nonzero dyadic `lambda_i` +on each child. Execute `y_i -= lambda_i*y_parent` in leaf-before-parent order, +then the residual update `(TC)h`, then the exact reverse inverse shears. Because +parents still hold their original inputs during preparation, row i of T is +`e_i-lambda_i e_parent`, without ancestor terms. Therefore + +``` +T^-1 (T y + T C h) = y + C h. +root price: R(C_i) +child price: E(i,j,lambda)=R(C_i-lambda*C_j)+2H(lambda). +``` + +The bill is the sum of these local prices. Both preparation and restoration +are charged; arbitrary target dirt cannot be discarded. Children refer to the +original parent compensation row even when the parent has its own parent. +Inverse-transposition swaps logical gate endpoints and negates coefficients, +retaining order, so the same sign-invariant bill applies. It does not transpose +private CLEAR instructions. + +### Universal tails (credited to PR961) + +The maximum original cell price is eight: +`H(1/4)=6, H(2/4)=5, H(3/4)=8, H(4/4)=4`. + +Write a reduced noninteger dyadic as `lambda=s*m/2^k`, m odd and positive. +If `k>=4`, a residual cell is `(a*2^k-s*m*b)/2^(k+2)`. +For `b!=0`, `v2(b)<=2=4`. Thus its price is at least `4+4=8`. For `b=0`, the original cell +is unchanged. Every cell therefore costs at least its original price. + +If `abs(lambda)>=68`, then for every `b!=0`, +`abs((a-lambda*b)/4)>=(abs(lambda)-4)/4>=16`. +For reduced `q=n/2^d` of magnitude at least16, `floor(log2(abs(n)))>=d+4`, +so `H(q)>=3+(d+4)+1+d>=8`. Again cells with `b=0` are unchanged. + +In both tails the residual is no cheaper than the original root row, and +`2H(lambda)>0` gives **strict** root domination. Any dyadic outside both tails +has denominator exponent at most3 and magnitude less than68, hence appears +uniquely as `n/8`, `1<=abs(n)<=543`. The tails are universal written valuation +and magnitude arguments, not claims that finite distant samples prove infinity. +Starting the denominator argument at3 would be unsound: original cell `3/4` +with parent cell1 and `lambda=5/8` becomes `1/8`, with price7 rather than8. + +### CK-specific finite inequality and forest exchange + +The complete census verifies for every nonunit coefficient in the core: + +``` +E(i,j,lambda) > min(R(C_i), E(i,j,-1), E(i,j,+1)). +``` + +This is **not implied by the quarter alphabet**. A synthetic pair with100 +copies of child entry `3/4` and parent entry `1/4` admits a cheaper coefficient3; +the checker retains this counter-control. Actual CK matrix information matters. + +For any nonunit edge in any admissible forest, choose its certified cheaper +alternative. A signed-unit alternative retains the same parent; a root +alternative deletes the edge. Neither creates a cycle. Descendants retain +their original parent rows and local costs. Repeating removes every nonunit +edge, strictly decreasing the total bill. The resulting signed-unit forest +has minimum16,364, checked by dense Prim and the pinned PR816 attaining tree's +cycle certificate. Because signed-unit forests are a subclass, the all-dyadic +minimum is the same. Every optimum in this precise class is signed-unit. + +Nonunit edge prices are directed: applying an undirected MST directly to all +dyadic edges would be invalid. The exchange step comes **before** using the +signed-unit undirected graph. The bound says nothing about arbitrary multi-parent +systems, arbitrary sequential shears, helper-basis changes, different lowering, +shared coefficient work, changed frames, or folded boundary work. + +## Provenance, selection and single pivot + +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`; OS assignment seed23, +complex-supplier track. `CLAIM.json` records three candidates and the single +pivot. The initial powers-of-two idea was abandoned on discovering PR964's +stronger existing exclusion; none of that duplicate is presented as new work. +The seed selected this track/object, not a different random replay. + +At the base, the selected reviewed conditional κ is +`836330098538459/500000000000000000 = 0.001672660197076918`, PR1094 with PR589/555. +We followed its selected record to `community-frontier1094-audit/ASSEMBLY.json`, +source manifest and `docs/research/community-batch1099-review.md`; the complex +side is binding. This historical CK result is **not** a new selected witness. +The ledger and live PR bodies were checked, including PR816/917/961/964/1080/1081. +PR1081 changes helper pairs under two tariffs; PR1080 changes the U8 two-sided +forest. Neither is composed with this fixed CK matrix result. There was no +pinned coordination issue; discussions1163/1166/1167 had no entry claims, and +a narrow local claim was reserved with the coordinating parent. + +`SOURCES.json` binds the two consumed runtime files by immutable bytes or +decompressed payload. The main checkout's source packages, selected frontier, +and `upstream/` are unchanged. Rooted-forest preparation, the existing circuit +and its66,520-real-primitive saving remain predecessor contributions. + +No full native re-emission, fresh whole-program prefix/precision check, global +owner/invoice/outer assembly, selected cold replay, full repository suite, +Lean theorem, hosted CI success or production integration is claimed. The +unchanged outside work and recursive children cancel in this local exclusion; +there is no improved fully paid recursive moment to feed into a new κ. +All-size/compiler, realization, hosting, precision/tape/exact recovery and +analytic assumptions remain inherited. This is not formal verification of +the full multiplication theorem. + +## Attribution and license + +Prepared by **Adam Gall (@adamgall)** with substantial **OpenAI Codex assistance** +in research, implementation, proof, controls and writing. Apache-2.0 under the +repository license. No independent human review is claimed. + +Credit **Gareth Davidson (@bitplane), PR964**, for the CK power-weight boundary; +**woklerx, PR961**, for the all-dyadic tails and forest-exchange method on X4; +**@dd-hemant, PR816**, for CK target forests and the attaining witness; +**ToikY, PR909**, for quarter-grid tail methods; **Oscar Fennell, PR759**, and +**Sricharan Vagvala, PR749**, for restored forest/pair predecessors; +**Ross Richardson, PR917/932**, and **David Awad, PR807**, for related compensation +work; and **Chafik Boukhalfa, Jeremy Kothe, icekylinx, DreamingOfClouds, eumemic** +and the retained source contributors for the CK supplier/compiler lineage. +All original notices and source licenses are preserved in place. diff --git a/research/ck-all-dyadic-forest-seed23/SOURCES.json b/research/ck-all-dyadic-forest-seed23/SOURCES.json new file mode 100644 index 0000000000..70ab38c627 --- /dev/null +++ b/research/ck-all-dyadic-forest-seed23/SOURCES.json @@ -0,0 +1,20 @@ +{ + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "files": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/ck/CANONICAL-WORD.json.gz": { + "encoding": "gzip-payload", + "sha256": "9bbc75dede090cfd7a0a0252424ea9d9f6211e2350d2a801d4e4f2f0784167c7" + }, + "research/complex-ck-target-forest/RECIPE.json": { + "encoding": "bytes", + "sha256": "a6f5ad8d774d9ec563b7bf6e68e481b4bee46253050eb2ef6ed6364c175ac809" + } + }, + "source_heads": { + "PR626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "PR816": "133735a2cc2319c12ba5d786214b2217e083e7da", + "PR964": "7a3bf8460cf6ca16a2bf008ff51fdb06df1af938", + "PR961": "4257ddf4b755cd0ac3bd3b0f6281cc5b2b1f72ad" + }, + "provenance": "PR961 head is the concurrent version pinned by PR964; proof consumed from the exact round base. Only the two files above are runtime inputs." +} diff --git a/research/ck-all-dyadic-forest-seed23/VALIDATION.md b/research/ck-all-dyadic-forest-seed23/VALIDATION.md new file mode 100644 index 0000000000..1773c7bb93 --- /dev/null +++ b/research/ck-all-dyadic-forest-seed23/VALIDATION.md @@ -0,0 +1,88 @@ +# Executed validation + +Environment: Linux x64, CPython 3.14.4, GCC15.2.0 build. Only Python's standard +library is required. Base and final refreshed upstream were both +`1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. + +## Complete checks + +Certificate generation: + +```sh +python3 -I -B research/ck-all-dyadic-forest-seed23/verify.py --record +``` + +Observed output (364.05 seconds in the shared research environment): + +```text +PASS_CK_ALL_DYADIC_FOREST cases=13501152 floor=16364 margin=63 columns=716x2 controls=10 no_new_kappa +``` + +Final isolated optimized replay, followed by the separately implemented full +integer oracle: + +```sh +python3 -I -O -B research/ck-all-dyadic-forest-seed23/verify.py && python3 -I -O -B research/ck-all-dyadic-forest-seed23/independent.py +``` + +Observed output (609.15 seconds combined): + +```text +PASS_CK_ALL_DYADIC_FOREST cases=13501152 floor=16364 margin=63 columns=716x2 controls=10 no_new_kappa +PASS_CK_PACKED_ORACLE cases=13501152 exact_lane_bits=20 full_receipt_match +``` + +Fast packaging controls on isolated temporary copies, including a path with +spaces, payload-preserving gzip corruption, recipe corruption and a missing +runtime input: + +```sh +python3 -I -O -B research/ck-all-dyadic-forest-seed23/test_package.py +``` + +Observed output (18.87 seconds): + +```text +PASS_CK_DYADIC_PACKAGE source_corruption=2 missing_source=1 optimized=1 outputs_preserved=1 +``` + +The primary and oracle agree on all13,501,152 finite cases, full margin histogram, +8,275 grouped cost streams and digest +`b52788e8fc41293379c05dc693baf494426302e8733d98bc2930435685f0f571`. +No nonunit tie or improvement survives the same-parent unit/root comparison; +941 cases beat their root, with minimum root margin−116. The finite minimum +against the valid alternative is63. The infinite tails are the separate written +proof in README, not an assertion of infinite execution. + +## Interrupted development invocations + +An initial uncompressed-list/Fraction-heavy certificate generation hit its +300-second invocation deadline; no failed mathematical predicate was reported. +A subsequent packed-vector but Fraction-heavy run was explicitly cancelled +before completing. A bounded traceback showed Fraction-heavy source processing; +row-wise dyadic-integer endpoint replay and integer-gcd tariff normalization +then replaced those avoidable operations without changing the census domain. + +The original packaging controls stalled awaiting child subprocess completion +and hit60 seconds; a30-second diagnostic showed the parent inside subprocess +communication. Final controls load the same isolated temporary verifier with +`runpy`, then exercise exactly the source-loading failure paths. The final +successful command above supersedes those interrupted invocation attempts. +These timings are execution records, **not** a controlled before/after performance +benchmark or a verifier-speedup claim. + +## Boundaries and overlap + +The final overlap refresh inspected new proposals through PR1205 and confirmed +PR961 (`4257ddf4b755cd0ac3bd3b0f6281cc5b2b1f72ad`) and PR964 +(`7a3bf8460cf6ca16a2bf008ff51fdb06df1af938`) are merged. Their ledger entries and +PR816 are incorporated. The new scope is CK non-power dyadic numerators; +PR964 closes CK powers of two and PR961 closes the different X4 matrix. +PR1080/1081 alter the helper side or source matrix/lowering, and are not composed. + +No full native/emitter/Clifford replay, global hosting/invoice/outer assembly, +selected cold replay, repository-wide suite, formal theorem prover or hosted CI +was executed for this unchanged-supplier research note. The original source, +selected result and upstream trees are not edited. The finite exact checks do +not discharge inherited all-size/compiler, realization, physical, precision/tape +or analytic obligations. No new κ is claimed. diff --git a/research/ck-all-dyadic-forest-seed23/independent.py b/research/ck-all-dyadic-forest-seed23/independent.py new file mode 100755 index 0000000000..0095414980 --- /dev/null +++ b/research/ck-all-dyadic-forest-seed23/independent.py @@ -0,0 +1,111 @@ +#!/usr/bin/env python3 +"""Integer-only packed-cost crosscheck; imports no primary checker. Apache-2.0.""" +from collections import Counter +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WIDTH = 20 +MASK = (1 << WIDTH)-1 +NS = tuple(range(-543,0)) + tuple(range(1,544)) + + +def demand(value, reason): + if not value: + raise ValueError(reason) + + +def digest(value): + return hashlib.sha256(json.dumps(value,sort_keys=True,separators=(',',':')).encode()).hexdigest() + + +def cost(n, denominator_power): + if not n: + return 0 + n = abs(n) + while denominator_power and n % 2 == 0: + n //= 2 + denominator_power -= 1 + count = 3 + denominator_power + while n: + count += n % 2 + n //= 2 + if n: + count += 1 + return count + + +def check(): + pins=json.loads((HERE/'SOURCES.json').read_text()) + path=next(p for p in pins['files'] if p.endswith('CANONICAL-WORD.json.gz')) + payload=gzip.decompress((ROOT/path).read_bytes()) + demand(hashlib.sha256(payload).hexdigest()==pins['files'][path]['sha256'],'word pin') + word=json.loads(payload) + rows=[[0]*492 for _ in range(112)] + for op,t,s,a,b,f in word['compensation']: + demand(op=='add' and f==0 and (4*a)%b==0,'panel') + rows[t-112][s-224]=(4*a)//b + grouped={} + for t,left in enumerate(rows): + for p,right in enumerate(rows): + if t==p: + continue + hist=tuple(sorted(Counter((a,b) for a,b in zip(left,right) if a or b).items())) + grouped.setdefault(hist,[]).append((t+112,p+112)) + # Each lane is a complete coefficient price; explicit bound prevents carries. + # At most 492 residual cells and two boundary shears; all terms <= 32. + demand((492+2)*32 < (1<>= WIDTH + demand(encoded==0,'packed overflow') + root=sum(count*cost(a,2) for (a,b),count in hist) + baseline=min(root,costs[535],costs[550]) # n=-8 and n=+8 + demand(NS[535]==-8 and NS[550]==8,'unit indices') + least=None + for n,value in zip(NS,costs): + if abs(n)==8: + continue + gap=value-baseline + demand(gap>0,'nonunit improvement') + margins[gap]+=len(pairs) + root_winners+=len(pairs)*(value 1: + require(b % 2 == 0, 'literal non-dyadic') + work_denominator *= 2 + b //= 2 + count += 1 + require(work*q.denominator == abs(q.numerator)*work_denominator, 'literal coefficient') + # Signed target accumulation and final private CLEAR. + return count + 2 + + +def load(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + objects = {} + for name, pin in pins['files'].items(): + data = (ROOT / name).read_bytes() + if pin['encoding'] == 'gzip-payload': + data = gzip.decompress(data) + require(hashlib.sha256(data).hexdigest() == pin['sha256'], 'source pin: ' + name) + objects[name] = json.loads(data) + word, recipe = objects[WORD], objects[RECIPE] + require((word['v'], word['R'], word['h']) == (112, 492, 9), 'geometry') + rows = {t: {} for t in TARGETS} + for op, t, h, a, b, frame in word['compensation']: + require(op == 'add' and t in rows and 224 <= h < 716 and frame == 0, 'panel interface') + require(word['start'][t] == word['start'][h] == 0, 'panel frame') + q, remainder = divmod(4*a, b) + require(remainder == 0 and 0 < abs(q) <= 4 and h not in rows[t], 'quarter alphabet') + rows[t][h] = q + require(sum(map(len, rows.values())) == 8704, 'panel cardinality') + return rows, recipe + + +def row_price(row): + return sum(price(a, 4) for a in row.values()) + + +def pair_histogram(left, right): + return Counter((left.get(h, 0), right.get(h, 0)) for h in left.keys() | right.keys()) + + +def edge_cost(histogram, n): + return 2 * price(n, 8) + sum(count * price(8*a - n*b, 32) for (a, b), count in histogram.items()) + + +def census(rows): + # Aggregation is exact: the histogram retains every ordered coefficient pair. + groups = {} + for t in TARGETS: + for p in TARGETS: + if t != p: + hist = tuple(sorted(pair_histogram(rows[t], rows[p]).items())) + groups.setdefault(hist, []).append((t, p)) + table = {(a, b): [price(8*a-n*b, 32) for n in NUMERATORS] + for a in range(-4, 5) for b in range(-4, 5) if a or b} + boundaries = [2*price(n, 8) for n in NUMERATORS] + # Exact 16-bit SIMD-in-an-integer: all residual prices are <=32 and + # there are <=492 cells plus two boundary operations, so no lane carries. + require(max(max(v) for v in table.values()) <= 32 and max(boundaries) <= 64, + 'packed scalar bound') + require((492+2)*32 < 65536, 'packed sum bound') + packed = {pair: int.from_bytes(struct.pack('<1086H', *values), 'little') + for pair, values in table.items()} + boundary = int.from_bytes(struct.pack('<1086H', *boundaries), 'little') + histogram = Counter() + root_winners = 0 + minimum = minimum_root = None + unit_indices = [NUMERATORS.index(-8), NUMERATORS.index(8)] + summaries = [] + for hist, pairs in sorted(groups.items()): + root = sum(count*price(a, 4) for (a, _), count in hist) + encoded = boundary + sum(count*packed[pair] for pair, count in hist) + costs = list(struct.unpack('<1086H', encoded.to_bytes(2172, 'little'))) + baseline = min(root, *(costs[i] for i in unit_indices)) + multiplicity = len(pairs) + first_pair = min(pairs) + local_min = None + for n, cost in zip(NUMERATORS, costs): + if abs(n) == 8: + continue + margin, root_margin = cost-baseline, cost-root + require(margin > 0, 'nonunit edge escapes domination') + histogram[margin] += multiplicity + root_winners += multiplicity * (root_margin < 0) + record = (margin, *first_pair, n) + root_record = (root_margin, *first_pair, n) + minimum = record if minimum is None else min(minimum, record) + minimum_root = root_record if minimum_root is None else min(minimum_root, root_record) + local_min = margin if local_min is None else min(local_min, margin) + summaries.append([list(map(list, hist)), len(pairs), digest(costs), local_min]) + return { + 'ordered_pairs': 12432, 'coefficient_count': len(NUMERATORS), + 'finite_cases': 12432*len(NUMERATORS), 'nonunit_cases': sum(histogram.values()), + 'histogram_groups': len(groups), 'minimum_domination': list(minimum), + 'minimum_root_margin': list(minimum_root), 'nonunit_edges_beating_root': root_winners, + 'margin_histogram': dict(sorted(histogram.items())), 'group_costs_sha256': digest(summaries), + } + + +def signed_floor(rows, recipe): + edges = [(row_price(rows[t]), -1, t, 0) for t in TARGETS] + for t in TARGETS: + for p in range(t+1, 224): + hist = pair_histogram(rows[t], rows[p]) + for sign in (-1, 1): + edges.append((edge_cost(hist, 8*sign), t, p, sign)) + # Independent dense Prim, not the predecessor's tie-broken Kruskal. + graph = {v: {} for v in [-1, *TARGETS]} + for w, a, b, _ in edges: + graph[a][b] = graph[b][a] = min(w, graph[a].get(b, w)) + seen, best, total = {-1}, dict(graph[-1]), 0 + while len(seen) != 113: + vertex = min((v for v in best if v not in seen), key=lambda v: (best[v], v)) + total += best[vertex] + seen.add(vertex) + for v, w in graph[vertex].items(): + if v not in seen: + best[v] = min(best.get(v, w), w) + selected = recipe['tree_edges'] + require(len(selected) == 112 and sum(e[0] for e in selected) == total, 'attaining floor') + available = set(edges) + adjacency = {v: [] for v in graph} + for w, a, b, s in selected: + require(tuple((w, a, b, s)) in available, 'unpriced selected edge') + adjacency[a].append((b, s, w)) + adjacency[b].append((a, s, w)) + queue, visited, order = [(-1, None)], {-1}, [] + for parent, predecessor in queue: + for child, sign, _ in sorted(adjacency[parent]): + if child == predecessor: + continue + require(child not in visited, 'forest cycle') + visited.add(child) + order.append((child, parent, sign)) + queue.append((child, parent)) + require(len(visited) == 113, 'disconnected witness') + maxima = {} + for start in adjacency: + walk = [(start, None, 0)] + for vertex, parent, maximum in walk: + maxima[start, vertex] = maximum + walk.extend((child, vertex, max(maximum, w)) for child, _, w in adjacency[vertex] if child != parent) + require(all(w >= maxima[a, b] for w, a, b, _ in edges), 'cycle inequality') + return total, order, len(edges) + + +def compile_panel(rows, order, coefficients=None): + coefficients = coefficients or {} + prep = [(t, p, -coefficients.get(t, Fraction(s))) for t, p, s in reversed(order) if p != -1] + residual = [] + for t, p, s in order: + c = coefficients.get(t, Fraction(s)) + support = rows[t].keys() | (rows[p].keys() if p != -1 else set()) + for h in sorted(support): + q = Fraction(rows[t].get(h, 0), 4) - (c*Fraction(rows[p].get(h, 0), 4) if p != -1 else 0) + if q: + residual.append((t, h, q)) + return prep + residual + [(t, p, -q) for t, p, q in reversed(prep)] + + +def replay(gates, backward=False): + # Exact row-wise dyadic integers; no floating point or modular recovery. + state = [{i: 1} for i in range(716)] + exponents = [0]*716 + for t, s, q in gates: + if backward: + t, s, q = s, t, -q + require(t != s, 'aliased panel gate') + a, b = q.numerator, q.denominator + require(b & (b-1) == 0, 'non-dyadic panel gate') + source_exponent = exponents[s] + b.bit_length()-1 + exponent = max(exponents[t], source_exponent) + if exponent != exponents[t]: + state[t] = {col: value << (exponent-exponents[t]) for col,value in state[t].items()} + multiplier = a << (exponent-source_exponent) + for col, value in state[s].items(): + result = state[t].get(col, 0) + multiplier*value + if result: + state[t][col] = result + else: + state[t].pop(col, None) + exponents[t] = exponent + normalized = [] + for row, exponent in zip(state, exponents): + shift = min([exponent, *((abs(v)&-abs(v)).bit_length()-1 for v in row.values())]) + normalized.append((exponent-shift, {col:value >> shift for col,value in row.items()})) + return normalized + + +def controls(rows, recipe, order, findings): + original = [(t, h, Fraction(a, 4)) for t, row in rows.items() for h, a in row.items()] + panel = compile_panel(rows, order) + require([['add',t,s,q.numerator,q.denominator,0] for t,s,q in panel] == recipe['compensation'], 'source witness reconstruction') + expected = [replay(original, b) for b in (False, True)] + require(all(replay(panel, b) == expected[b] for b in (False, True)), '716-column witness') + # Exercise nonunit coefficients on overlapping ancestor/descendant branches, + # not merely disjoint pairs. This is endpoint evidence, not an infinite replay. + mixed = {t: Fraction(((-1)**i)*(2*i+3), 8) for i,(t,p,_) in enumerate(order) if p != -1} + extended = compile_panel(rows, order, mixed) + require(all(replay(extended, b) == expected[b] for b in (False, True)), 'mixed dyadic forest identity') + reject = [] + mutations = { + 'omitted_preparation': panel[1:], + 'omitted_restoration': panel[:-1], + 'sign_error': [(panel[0][0],panel[0][1],-panel[0][2]), *panel[1:]], + 'nonunit_stale_residual': [(panel[0][0],panel[0][1],2*panel[0][2]), *panel[1:]], + 'reversed_preparation': list(reversed(panel[:106])) + panel[106:], + 'reversed_restoration': panel[:-106] + list(reversed(panel[-106:])), + } + for name, mutant in mutations.items(): + require(replay(mutant) != expected[0], 'missed mutation: '+name) + reject.append(name) + # A root-only domination theorem would be false on this actual CK input. + root_margin,t,p,n = findings['minimum_root_margin'] + require(edge_cost(pair_histogram(rows[t],rows[p]),n)-row_price(rows[t]) == root_margin < 0, 'root-only counterexample') + reject.append('root_only_domination') + # Quarter alphabet alone does not imply same-parent domination either. + synthetic = {(3,1): 100} + require(edge_cost(synthetic,24) < min(100*price(3,4),edge_cost(synthetic,-8),edge_cost(synthetic,8)), 'synthetic nonunit winner') + reject.append('alphabet_only_domination') + try: + price(1,3) + except ValueError: + reject.append('non_dyadic_coefficient') + else: + raise ValueError('non-dyadic accepted') + require(min(4+4, 8) >= max(price(a,4) for a in range(-4,5)), 'tail price threshold') + # Reducing the denominator cutoff to 3 is unsound: 3/4-(5/8)*1=1/8. + require(price(1,8) < price(3,4), 'tail arithmetic control') + reject.append('denominator_tail_started_too_early') + return {'columns':716, 'orientations':2, 'mixed_nonunit_edges':len(mixed), 'rejected':reject, + 'witness_additions':len(panel)} + + +def run(): + rows, recipe = load() + # Covers every coefficient appearing anywhere in the complete finite census. + for n in range(-2204,2205): + require(price(n,32) == literal_price(n,32), 'literal lowering count') + findings = census(rows) + floor, order, inequalities = signed_floor(rows,recipe) + require(floor == 16364, 'historical floor') + result = {'format':'ck-all-dyadic-forest-v1','seed':23,'finite':findings, + 'signed_floor':floor,'cycle_inequalities':inequalities, + 'tail':{'max_entry_price':8,'denominator_exponent_from':4,'magnitude_from':68, + 'argument':'coordinatewise root domination plus two strictly positive boundary shears'}, + 'literal_coefficient_cases':4409, + 'controls':controls(rows,recipe,order,findings)} + return json.loads(json.dumps(result)) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--record', action='store_true') + args = parser.parse_args() + result = run() + path = HERE/'EXPECTED.json' + if args.record: + path.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + require(json.loads(path.read_text()) == result, 'complete receipt mismatch') + print('PASS_CK_ALL_DYADIC_FOREST cases=13501152 floor=16364 margin=63 columns=716x2 controls=10 no_new_kappa') + + +if __name__ == '__main__': + main() From 9cd42fb94d2b74e7308ad783b20081aa85b868a1 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Tue, 13 Oct 2026 20:23:02 +0000 Subject: [PATCH 2/2] Record completed CK all-dyadic claim and PR1220 --- research/ck-all-dyadic-forest-seed23/CLAIM.json | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/research/ck-all-dyadic-forest-seed23/CLAIM.json b/research/ck-all-dyadic-forest-seed23/CLAIM.json index 9ec168fe70..fde242ec49 100644 --- a/research/ck-all-dyadic-forest-seed23/CLAIM.json +++ b/research/ck-all-dyadic-forest-seed23/CLAIM.json @@ -17,5 +17,9 @@ "expected_deliverable": "Exact scoped exclusion or concrete nonunit improving edge with complete cost; no hosted supplier or kappa claim", "coordination": "No pinned sprint coordination issue existed; open issues913 and650 were unrelated. Discussions1163,1166,1167 had no comments/claims on entry. Local claim and parent reservation; parent approved the overlap-driven pivot.", "expected_finish": "2026-10-13T22:30:00Z", - "status": "research in progress" + "status": "complete; focused research PR submitted", + "result": "All-dyadic CK target-forest floor remains16364. Complete13501152-case census has minimum valid domination margin63;941 nonunit cases beat their root (minimum−116), requiring the same-parent exchange. All716 columns in both orientations,10 mathematical controls, full independent census oracle and3 packaging rejection controls pass.", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1220", + "verification": "python3 -I -O -B research/ck-all-dyadic-forest-seed23/verify.py && python3 -I -O -B research/ck-all-dyadic-forest-seed23/independent.py; separate test_package.py", + "scope_limits": "Historical independent binary-Horner one-parent forest class only. No changed supplier, native/global admission, precision improvement or new kappa." }