From 094204c9689a0185855b8c7ba35763d1a6598995 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 05:18:38 +0530 Subject: [PATCH 1/2] research: certify coupled temporal k8 gauge schedules --- .../CERTIFICATE.json | 3112 +++++++++++++++++ research/k8-paired-temporal-seed23/CLAIM.md | 63 + research/k8-paired-temporal-seed23/README.md | 226 ++ .../k8-paired-temporal-seed23/SOURCES.json | 34 + .../k8-paired-temporal-seed23/VALIDATION.json | 70 + research/k8-paired-temporal-seed23/replay.py | 174 + research/k8-paired-temporal-seed23/search.py | 185 + research/k8-paired-temporal-seed23/verify.py | 253 ++ 8 files changed, 4117 insertions(+) create mode 100644 research/k8-paired-temporal-seed23/CERTIFICATE.json create mode 100644 research/k8-paired-temporal-seed23/CLAIM.md create mode 100644 research/k8-paired-temporal-seed23/README.md create mode 100644 research/k8-paired-temporal-seed23/SOURCES.json create mode 100644 research/k8-paired-temporal-seed23/VALIDATION.json create mode 100644 research/k8-paired-temporal-seed23/replay.py create mode 100644 research/k8-paired-temporal-seed23/search.py create mode 100644 research/k8-paired-temporal-seed23/verify.py diff --git a/research/k8-paired-temporal-seed23/CERTIFICATE.json b/research/k8-paired-temporal-seed23/CERTIFICATE.json new file mode 100644 index 0000000000..3f388682c4 --- /dev/null +++ b/research/k8-paired-temporal-seed23/CERTIFICATE.json @@ -0,0 +1,3112 @@ +{ + "base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "seed": 23, + "domain": [ + -4, + 4 + ], + "pairs": [ + [ + 225, + 342 + ], + [ + 225, + 347 + ], + [ + 225, + 348 + ], + [ + 225, + 350 + ], + [ + 225, + 351 + ], + [ + 225, + 352 + ], + [ + 225, + 356 + ], + [ + 225, + 367 + ], + [ + 225, + 379 + ], + [ + 225, + 384 + ], + [ + 225, + 388 + ], + [ + 225, + 391 + ], + [ + 225, + 395 + ], + [ + 225, + 399 + ], + [ + 225, + 400 + ], + [ + 225, + 401 + ] + ], + "orientations": { + "forward": { + "census": [ + { + "pair": [ + 225, + 342 + ], + "delta_real": -204, + "best_tied_single_delta_real": -204, + "single_deltas_real": [ + -75, + -129 + ], + "strict_gap_real": 0, + "blocks": 16, + "incident_adds": 242, + "dense_edges": 1587762 + }, + { + "pair": [ + 225, + 347 + ], + "delta_real": -229, + "best_tied_single_delta_real": -229, + "single_deltas_real": [ + -75, + -154 + ], + "strict_gap_real": 0, + "blocks": 19, + "incident_adds": 252, + "dense_edges": 1653372 + }, + { + "pair": [ + 225, + 348 + ], + "delta_real": -260, + "best_tied_single_delta_real": -260, + "single_deltas_real": [ + -75, + -184 + ], + "strict_gap_real": 0, + "blocks": 16, + "incident_adds": 245, + "dense_edges": 1607445 + }, + { + "pair": [ + 225, + 350 + ], + "delta_real": -237, + "best_tied_single_delta_real": -234, + "single_deltas_real": [ + -75, + -163 + ], + "strict_gap_real": 3, + "blocks": 16, + "incident_adds": 226, + "dense_edges": 1482786 + }, + { + "pair": [ + 225, + 351 + ], + "delta_real": -220, + "best_tied_single_delta_real": -220, + "single_deltas_real": [ + -75, + -145 + ], + "strict_gap_real": 0, + "blocks": 17, + "incident_adds": 261, + "dense_edges": 1712421 + }, + { + "pair": [ + 225, + 352 + ], + "delta_real": -194, + "best_tied_single_delta_real": -194, + "single_deltas_real": [ + -75, + -119 + ], + "strict_gap_real": 0, + "blocks": 14, + "incident_adds": 215, + "dense_edges": 1410615 + }, + { + "pair": [ + 225, + 356 + ], + "delta_real": -238, + "best_tied_single_delta_real": -236, + "single_deltas_real": [ + -75, + -161 + ], + "strict_gap_real": 2, + "blocks": 16, + "incident_adds": 239, + "dense_edges": 1568079 + }, + { + "pair": [ + 225, + 367 + ], + "delta_real": -222, + "best_tied_single_delta_real": -222, + "single_deltas_real": [ + -75, + -147 + ], + "strict_gap_real": 0, + "blocks": 15, + "incident_adds": 242, + "dense_edges": 1587762 + }, + { + "pair": [ + 225, + 379 + ], + "delta_real": -246, + "best_tied_single_delta_real": -246, + "single_deltas_real": [ + -75, + -171 + ], + "strict_gap_real": 0, + "blocks": 19, + "incident_adds": 263, + "dense_edges": 1725543 + }, + { + "pair": [ + 225, + 384 + ], + "delta_real": -186, + "best_tied_single_delta_real": -184, + "single_deltas_real": [ + -75, + -112 + ], + "strict_gap_real": 2, + "blocks": 14, + "incident_adds": 214, + "dense_edges": 1404054 + }, + { + "pair": [ + 225, + 388 + ], + "delta_real": -231, + "best_tied_single_delta_real": -229, + "single_deltas_real": [ + -75, + -158 + ], + "strict_gap_real": 2, + "blocks": 13, + "incident_adds": 228, + "dense_edges": 1495908 + }, + { + "pair": [ + 225, + 391 + ], + "delta_real": -217, + "best_tied_single_delta_real": -217, + "single_deltas_real": [ + -75, + -142 + ], + "strict_gap_real": 0, + "blocks": 13, + "incident_adds": 228, + "dense_edges": 1495908 + }, + { + "pair": [ + 225, + 395 + ], + "delta_real": -225, + "best_tied_single_delta_real": -225, + "single_deltas_real": [ + -75, + -150 + ], + "strict_gap_real": 0, + "blocks": 17, + "incident_adds": 252, + "dense_edges": 1653372 + }, + { + "pair": [ + 225, + 399 + ], + "delta_real": -216, + "best_tied_single_delta_real": -216, + "single_deltas_real": [ + -75, + -141 + ], + "strict_gap_real": 0, + "blocks": 17, + "incident_adds": 242, + "dense_edges": 1587762 + }, + { + "pair": [ + 225, + 400 + ], + "delta_real": -113, + "best_tied_single_delta_real": -113, + "single_deltas_real": [ + -75, + -38 + ], + "strict_gap_real": 0, + "blocks": 14, + "incident_adds": 194, + "dense_edges": 1272834 + }, + { + "pair": [ + 225, + 401 + ], + "delta_real": -273, + "best_tied_single_delta_real": -271, + "single_deltas_real": [ + -75, + -199 + ], + "strict_gap_real": 2, + "blocks": 12, + "incident_adds": 244, + "dense_edges": 1600884 + } + ], + "winner": { + "pair": [ + 225, + 350 + ], + "delta_real": -237, + "best_tied_single_delta_real": -234, + "single_deltas_real": [ + -75, + -163 + ], + "strict_gap_real": 3, + "blocks": 16, + "incident_adds": 226, + "dense_edges": 1482786 + }, + "schedule": [ + [ + 194, + 0, + -1 + ], + [ + 225, + 0, + -1 + ], + [ + 267, + 0, + -1 + ], + [ + 298, + -1, + -1 + ], + [ + 373, + -1, + -1 + ], + [ + 666, + -1, + -1 + ], + [ + 822, + -1, + -2 + ], + [ + 891, + -1, + -2 + ], + [ + 952, + -1, + -2 + ], + [ + 1022, + -1, + -2 + ], + [ + 1051, + -1, + -2 + ], + [ + 1092, + -1, + -2 + ], + [ + 1118, + -1, + -2 + ], + [ + 1159, + -1, + -2 + ], + [ + 1220, + -1, + -2 + ], + [ + 1290, + -1, + -2 + ], + [ + 1375, + -1, + -2 + ], + [ + 1534, + -1, + -2 + ], + [ + 1616, + -1, + -2 + ], + [ + 1666, + -1, + -2 + ], + [ + 1730, + -1, + -2 + ], + [ + 1927, + -1, + -2 + ], + [ + 2025, + -1, + -2 + ], + [ + 2182, + -1, + -2 + ], + [ + 2260, + -1, + -1 + ], + [ + 2333, + -1, + -1 + ], + [ + 2398, + -1, + -1 + ], + [ + 2472, + -1, + -1 + ], + [ + 2505, + -1, + -1 + ], + [ + 2546, + -1, + -1 + ], + [ + 2576, + -1, + -1 + ], + [ + 2617, + -1, + -1 + ], + [ + 2682, + -1, + -1 + ], + [ + 2756, + -1, + -1 + ], + [ + 2789, + 0, + -1 + ], + [ + 2820, + 0, + -1 + ], + [ + 2862, + 0, + -1 + ], + [ + 2893, + -1, + -1 + ], + [ + 3401, + -1, + -2 + ], + [ + 3474, + -1, + -2 + ], + [ + 3592, + -1, + -2 + ], + [ + 3665, + -1, + -2 + ], + [ + 3728, + -1, + -2 + ], + [ + 3794, + -1, + -2 + ], + [ + 3939, + -1, + -2 + ], + [ + 4029, + -1, + -2 + ], + [ + 4094, + -1, + -2 + ], + [ + 4168, + -1, + -2 + ], + [ + 4213, + -1, + -2 + ], + [ + 4231, + -1, + -2 + ], + [ + 4264, + -1, + -2 + ], + [ + 4328, + -1, + -2 + ], + [ + 4552, + -1, + -1 + ], + [ + 4829, + -1, + -1 + ], + [ + 5225, + -1, + -1 + ], + [ + 5296, + -1, + -1 + ], + [ + 5539, + -1, + -1 + ], + [ + 5613, + -1, + -2 + ], + [ + 5674, + -1, + -2 + ], + [ + 5748, + -1, + -2 + ], + [ + 5780, + -1, + -2 + ], + [ + 5810, + -1, + -1 + ], + [ + 5880, + -1, + -1 + ], + [ + 5955, + -1, + -2 + ], + [ + 6034, + -1, + -2 + ], + [ + 6080, + -1, + -2 + ], + [ + 6114, + -1, + -2 + ], + [ + 6192, + -1, + -2 + ], + [ + 6271, + -1, + -2 + ], + [ + 6344, + -1, + -2 + ], + [ + 6419, + -1, + -2 + ], + [ + 6496, + -1, + -2 + ], + [ + 6531, + -1, + -2 + ], + [ + 6571, + -1, + -2 + ], + [ + 6604, + -1, + -2 + ], + [ + 6644, + -1, + -2 + ], + [ + 6713, + -1, + -2 + ], + [ + 6789, + -1, + -2 + ], + [ + 8729, + 0, + 0 + ], + [ + 8747, + 0, + 0 + ], + [ + 8760, + 0, + -1 + ], + [ + 8773, + 0, + 0 + ], + [ + 8790, + 0, + 0 + ], + [ + 8800, + 0, + 0 + ], + [ + 8816, + 0, + 0 + ], + [ + 8828, + 0, + 0 + ], + [ + 8842, + 0, + 0 + ], + [ + 9397, + 0, + 0 + ], + [ + 9452, + 0, + 0 + ], + [ + 9453, + -1, + 0 + ], + [ + 9501, + 0, + 0 + ], + [ + 9524, + 0, + 0 + ], + [ + 9541, + 0, + 0 + ], + [ + 9542, + 0, + 0 + ], + [ + 9543, + 0, + 0 + ], + [ + 9545, + 0, + 0 + ], + [ + 9546, + -1, + 0 + ], + [ + 9560, + 0, + 0 + ], + [ + 9563, + 0, + 0 + ], + [ + 9574, + 0, + 0 + ], + [ + 9580, + 0, + 0 + ], + [ + 9581, + -1, + 0 + ], + [ + 9582, + -1, + 0 + ], + [ + 9583, + -1, + 0 + ], + [ + 9584, + -1, + 0 + ], + [ + 9585, + -1, + 0 + ], + [ + 9591, + 0, + 0 + ], + [ + 9592, + 0, + 0 + ], + [ + 9593, + 0, + 0 + ], + [ + 9596, + 0, + 0 + ], + [ + 9600, + 0, + 0 + ], + [ + 9608, + 0, + 0 + ], + [ + 10949, + 0, + 0 + ], + [ + 10998, + 0, + 0 + ], + [ + 10999, + 0, + 0 + ], + [ + 11039, + 0, + 0 + ], + [ + 14211, + 0, + 0 + ], + [ + 14653, + 0, + 0 + ], + [ + 14949, + 0, + 0 + ], + [ + 15754, + 0, + 1 + ], + [ + 15755, + 0, + 1 + ], + [ + 15761, + 0, + 0 + ], + [ + 18338, + -1, + 0 + ], + [ + 18339, + -1, + 0 + ], + [ + 18340, + -1, + 0 + ], + [ + 18341, + -1, + 0 + ], + [ + 18342, + -1, + 0 + ], + [ + 18343, + -1, + 0 + ], + [ + 18344, + 1, + 0 + ], + [ + 18345, + 1, + 0 + ], + [ + 18379, + 0, + 0 + ], + [ + 18457, + 0, + 0 + ], + [ + 18469, + 0, + 1 + ], + [ + 18688, + 0, + 1 + ], + [ + 18699, + 0, + 1 + ], + [ + 18845, + 0, + 1 + ], + [ + 18875, + 0, + 1 + ], + [ + 18889, + 0, + 1 + ], + [ + 18903, + 0, + 1 + ], + [ + 18913, + 0, + 1 + ], + [ + 18976, + 1, + 1 + ], + [ + 18993, + 1, + 1 + ], + [ + 19124, + 1, + 1 + ], + [ + 19195, + 1, + 1 + ], + [ + 19361, + 1, + 1 + ], + [ + 19391, + 0, + 1 + ], + [ + 19501, + 0, + 1 + ], + [ + 19531, + -1, + 1 + ], + [ + 19555, + 0, + 1 + ], + [ + 19569, + 0, + 1 + ], + [ + 19589, + 0, + 1 + ], + [ + 19645, + 1, + 1 + ], + [ + 19869, + 1, + 1 + ], + [ + 19989, + 1, + 1 + ], + [ + 20011, + 1, + 1 + ], + [ + 20039, + 1, + 1 + ], + [ + 20060, + 1, + 1 + ], + [ + 20106, + 1, + 1 + ], + [ + 20131, + 0, + 1 + ], + [ + 20200, + 0, + 1 + ], + [ + 20225, + 0, + 1 + ], + [ + 20244, + 0, + 1 + ], + [ + 20283, + 0, + 1 + ], + [ + 20323, + -1, + 1 + ], + [ + 20698, + 1, + 1 + ], + [ + 20738, + 1, + 1 + ], + [ + 20771, + 1, + 1 + ], + [ + 20892, + 1, + 1 + ], + [ + 21081, + 1, + 1 + ], + [ + 21139, + 0, + 1 + ], + [ + 21190, + 0, + 1 + ], + [ + 21228, + 0, + 1 + ], + [ + 21418, + -1, + 1 + ], + [ + 21552, + 1, + 1 + ], + [ + 21613, + 1, + 1 + ], + [ + 21692, + 1, + 1 + ], + [ + 21758, + 0, + 1 + ], + [ + 21781, + -1, + 1 + ], + [ + 22035, + 1, + 1 + ], + [ + 22067, + 1, + 1 + ], + [ + 22124, + -1, + 1 + ], + [ + 22225, + 0, + 1 + ], + [ + 22259, + 0, + 1 + ], + [ + 22288, + 0, + 1 + ], + [ + 22428, + 0, + 1 + ], + [ + 22716, + -1, + 1 + ], + [ + 22756, + -1, + 1 + ], + [ + 22762, + 0, + 1 + ], + [ + 22782, + 0, + 1 + ], + [ + 22783, + 0, + 2 + ], + [ + 22784, + 0, + 2 + ], + [ + 22785, + 0, + 2 + ], + [ + 22786, + 0, + 1 + ], + [ + 22787, + 0, + 0 + ], + [ + 22788, + 0, + 0 + ], + [ + 22789, + 0, + 0 + ], + [ + 22790, + 0, + 0 + ], + [ + 22791, + 0, + 0 + ], + [ + 22792, + 0, + 0 + ], + [ + 22793, + 0, + 0 + ], + [ + 22794, + 0, + 0 + ], + [ + 22795, + 0, + 0 + ], + [ + 22796, + 0, + 0 + ], + [ + 22797, + 0, + 0 + ], + [ + 22798, + 0, + 0 + ], + [ + 22799, + 0, + 0 + ], + [ + 22800, + 0, + 0 + ], + [ + 22801, + 0, + 0 + ], + [ + 22812, + 0, + 0 + ], + [ + 22963, + 0, + 0 + ], + [ + 23146, + 0, + -1 + ], + [ + 23176, + 0, + -1 + ], + [ + 23187, + 0, + -1 + ], + [ + 23228, + -1, + -1 + ], + [ + 23267, + 0, + -1 + ], + [ + 23318, + 0, + -1 + ], + [ + 23346, + -1, + -1 + ], + [ + 23386, + -1, + -1 + ], + [ + 23439, + 1, + -1 + ], + [ + 23479, + 1, + -1 + ], + [ + 23608, + 1, + -1 + ], + [ + 24129, + 0, + -1 + ], + [ + 24256, + 0, + -1 + ], + [ + 24362, + 0, + -1 + ], + [ + 24424, + 0, + -1 + ], + [ + 24523, + 0, + -1 + ] + ], + "coupling_block": { + "first_incident_event": 18338, + "last_incident_event": 24523, + "incident_adds": 104, + "shared_event": 22786, + "shared_coefficient": "2", + "signs": [ + 1, + -1 + ], + "exponents": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "conditional_single_deltas_real": [ + [ + -35, + -38, + -41, + -43, + -42, + -39, + -36, + -33, + -30 + ], + [ + 0, + -3, + -6, + -9, + -12, + -14, + -12, + -9, + -6 + ] + ], + "single_optimal_exponents": [ + [ + -1 + ], + [ + 1 + ] + ], + "joint_minimizers": [ + [ + 0, + 1 + ] + ], + "joint_delta_real": -56, + "best_tied_single_delta_real": -53 + }, + "invariant": { + "inserted_scales": 55, + "scale_primitives_real": 62, + "changed_adds": 136, + "add_delta_real": -299, + "delta_real": -237 + }, + "before": { + "complex_primitives": 149002, + "prefix_l1": "2765345294379392599/1024", + "prefix_bits": 52, + "grid_depth_upper": 22, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "after": { + "complex_primitives": 148528, + "prefix_l1": "2765345294379392599/1024", + "prefix_bits": 52, + "grid_depth_upper": 22, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "candidate_sha256": "ab67877e2c13c1f589313c4835a25d25375129b323cdec22d4d6f2299c73b20c" + }, + "backward": { + "census": [ + { + "pair": [ + 225, + 342 + ], + "delta_real": -204, + "best_tied_single_delta_real": -204, + "single_deltas_real": [ + -75, + -129 + ], + "strict_gap_real": 0, + "blocks": 16, + "incident_adds": 242, + "dense_edges": 1587762 + }, + { + "pair": [ + 225, + 347 + ], + "delta_real": -229, + "best_tied_single_delta_real": -229, + "single_deltas_real": [ + -75, + -154 + ], + "strict_gap_real": 0, + "blocks": 19, + "incident_adds": 252, + "dense_edges": 1653372 + }, + { + "pair": [ + 225, + 348 + ], + "delta_real": -260, + "best_tied_single_delta_real": -260, + "single_deltas_real": [ + -75, + -184 + ], + "strict_gap_real": 0, + "blocks": 16, + "incident_adds": 245, + "dense_edges": 1607445 + }, + { + "pair": [ + 225, + 350 + ], + "delta_real": -237, + "best_tied_single_delta_real": -234, + "single_deltas_real": [ + -75, + -163 + ], + "strict_gap_real": 3, + "blocks": 16, + "incident_adds": 226, + "dense_edges": 1482786 + }, + { + "pair": [ + 225, + 351 + ], + "delta_real": -220, + "best_tied_single_delta_real": -220, + "single_deltas_real": [ + -75, + -145 + ], + "strict_gap_real": 0, + "blocks": 17, + "incident_adds": 261, + "dense_edges": 1712421 + }, + { + "pair": [ + 225, + 352 + ], + "delta_real": -194, + "best_tied_single_delta_real": -194, + "single_deltas_real": [ + -75, + -119 + ], + "strict_gap_real": 0, + "blocks": 14, + "incident_adds": 215, + "dense_edges": 1410615 + }, + { + "pair": [ + 225, + 356 + ], + "delta_real": -238, + "best_tied_single_delta_real": -236, + "single_deltas_real": [ + -75, + -161 + ], + "strict_gap_real": 2, + "blocks": 16, + "incident_adds": 239, + "dense_edges": 1568079 + }, + { + "pair": [ + 225, + 367 + ], + "delta_real": -222, + "best_tied_single_delta_real": -222, + "single_deltas_real": [ + -75, + -147 + ], + "strict_gap_real": 0, + "blocks": 15, + "incident_adds": 242, + "dense_edges": 1587762 + }, + { + "pair": [ + 225, + 379 + ], + "delta_real": -246, + "best_tied_single_delta_real": -246, + "single_deltas_real": [ + -75, + -171 + ], + "strict_gap_real": 0, + "blocks": 19, + "incident_adds": 263, + "dense_edges": 1725543 + }, + { + "pair": [ + 225, + 384 + ], + "delta_real": -186, + "best_tied_single_delta_real": -184, + "single_deltas_real": [ + -75, + -112 + ], + "strict_gap_real": 2, + "blocks": 14, + "incident_adds": 214, + "dense_edges": 1404054 + }, + { + "pair": [ + 225, + 388 + ], + "delta_real": -231, + "best_tied_single_delta_real": -229, + "single_deltas_real": [ + -75, + -158 + ], + "strict_gap_real": 2, + "blocks": 13, + "incident_adds": 228, + "dense_edges": 1495908 + }, + { + "pair": [ + 225, + 391 + ], + "delta_real": -217, + "best_tied_single_delta_real": -217, + "single_deltas_real": [ + -75, + -142 + ], + "strict_gap_real": 0, + "blocks": 13, + "incident_adds": 228, + "dense_edges": 1495908 + }, + { + "pair": [ + 225, + 395 + ], + "delta_real": -225, + "best_tied_single_delta_real": -225, + "single_deltas_real": [ + -75, + -150 + ], + "strict_gap_real": 0, + "blocks": 17, + "incident_adds": 252, + "dense_edges": 1653372 + }, + { + "pair": [ + 225, + 399 + ], + "delta_real": -216, + "best_tied_single_delta_real": -216, + "single_deltas_real": [ + -75, + -141 + ], + "strict_gap_real": 0, + "blocks": 17, + "incident_adds": 242, + "dense_edges": 1587762 + }, + { + "pair": [ + 225, + 400 + ], + "delta_real": -113, + "best_tied_single_delta_real": -113, + "single_deltas_real": [ + -75, + -38 + ], + "strict_gap_real": 0, + "blocks": 14, + "incident_adds": 194, + "dense_edges": 1272834 + }, + { + "pair": [ + 225, + 401 + ], + "delta_real": -273, + "best_tied_single_delta_real": -271, + "single_deltas_real": [ + -75, + -199 + ], + "strict_gap_real": 2, + "blocks": 12, + "incident_adds": 244, + "dense_edges": 1600884 + } + ], + "winner": { + "pair": [ + 225, + 350 + ], + "delta_real": -237, + "best_tied_single_delta_real": -234, + "single_deltas_real": [ + -75, + -163 + ], + "strict_gap_real": 3, + "blocks": 16, + "incident_adds": 226, + "dense_edges": 1482786 + }, + "schedule": [ + [ + 194, + 0, + 0 + ], + [ + 225, + 0, + 1 + ], + [ + 267, + 0, + 1 + ], + [ + 298, + 0, + 1 + ], + [ + 373, + 0, + 1 + ], + [ + 666, + 0, + 1 + ], + [ + 822, + 0, + 2 + ], + [ + 891, + 0, + 2 + ], + [ + 952, + 0, + 2 + ], + [ + 1022, + 0, + 2 + ], + [ + 1051, + 1, + 2 + ], + [ + 1092, + 1, + 2 + ], + [ + 1118, + 1, + 2 + ], + [ + 1159, + 1, + 2 + ], + [ + 1220, + 1, + 2 + ], + [ + 1290, + 1, + 2 + ], + [ + 1375, + 1, + 2 + ], + [ + 1534, + 1, + 2 + ], + [ + 1616, + 1, + 2 + ], + [ + 1666, + 1, + 2 + ], + [ + 1730, + 1, + 2 + ], + [ + 1927, + 1, + 2 + ], + [ + 2025, + 1, + 2 + ], + [ + 2182, + 1, + 2 + ], + [ + 2260, + 1, + 1 + ], + [ + 2333, + 1, + 1 + ], + [ + 2398, + 1, + 1 + ], + [ + 2472, + 1, + 1 + ], + [ + 2505, + 1, + 1 + ], + [ + 2546, + 1, + 1 + ], + [ + 2576, + 1, + 1 + ], + [ + 2617, + 0, + 1 + ], + [ + 2682, + 0, + 1 + ], + [ + 2756, + 0, + 1 + ], + [ + 2789, + 0, + 1 + ], + [ + 2820, + 0, + 1 + ], + [ + 2862, + 0, + 1 + ], + [ + 2893, + 0, + 1 + ], + [ + 3401, + 0, + 2 + ], + [ + 3474, + 0, + 2 + ], + [ + 3592, + 0, + 2 + ], + [ + 3665, + 0, + 2 + ], + [ + 3728, + 0, + 2 + ], + [ + 3794, + 0, + 2 + ], + [ + 3939, + 0, + 2 + ], + [ + 4029, + 0, + 2 + ], + [ + 4094, + 0, + 2 + ], + [ + 4168, + 1, + 2 + ], + [ + 4213, + 1, + 2 + ], + [ + 4231, + 1, + 2 + ], + [ + 4264, + 1, + 2 + ], + [ + 4328, + 1, + 2 + ], + [ + 4552, + 1, + 1 + ], + [ + 4829, + 1, + 1 + ], + [ + 5225, + 1, + 1 + ], + [ + 5296, + 1, + 1 + ], + [ + 5539, + 1, + 1 + ], + [ + 5613, + 1, + 1 + ], + [ + 5674, + 1, + 1 + ], + [ + 5748, + 1, + 1 + ], + [ + 5780, + 1, + 1 + ], + [ + 5810, + 1, + 1 + ], + [ + 5880, + 1, + 1 + ], + [ + 5955, + 1, + 2 + ], + [ + 6034, + 1, + 2 + ], + [ + 6080, + 1, + 2 + ], + [ + 6114, + 1, + 2 + ], + [ + 6192, + 1, + 2 + ], + [ + 6271, + 1, + 2 + ], + [ + 6344, + 1, + 2 + ], + [ + 6419, + 1, + 2 + ], + [ + 6496, + 1, + 2 + ], + [ + 6531, + 1, + 2 + ], + [ + 6571, + 1, + 2 + ], + [ + 6604, + 1, + 2 + ], + [ + 6644, + 0, + 2 + ], + [ + 6713, + 0, + 2 + ], + [ + 6789, + 0, + 2 + ], + [ + 8729, + 0, + 0 + ], + [ + 8747, + 0, + 0 + ], + [ + 8760, + 0, + 0 + ], + [ + 8773, + 0, + 0 + ], + [ + 8790, + 0, + 0 + ], + [ + 8800, + 0, + 0 + ], + [ + 8816, + 0, + -1 + ], + [ + 8828, + 0, + 0 + ], + [ + 8842, + 0, + 0 + ], + [ + 9397, + 0, + 0 + ], + [ + 9452, + 0, + 0 + ], + [ + 9453, + 0, + 0 + ], + [ + 9501, + 0, + 0 + ], + [ + 9524, + 0, + 0 + ], + [ + 9541, + 0, + 0 + ], + [ + 9542, + 0, + 0 + ], + [ + 9543, + 0, + 0 + ], + [ + 9545, + 0, + 0 + ], + [ + 9546, + 0, + 0 + ], + [ + 9560, + 0, + 0 + ], + [ + 9563, + 0, + 0 + ], + [ + 9574, + 0, + 0 + ], + [ + 9580, + 0, + 0 + ], + [ + 9581, + 1, + 0 + ], + [ + 9582, + 1, + 0 + ], + [ + 9583, + 1, + 0 + ], + [ + 9584, + 1, + 0 + ], + [ + 9585, + 1, + 0 + ], + [ + 9591, + 0, + 0 + ], + [ + 9592, + 0, + 0 + ], + [ + 9593, + 0, + 0 + ], + [ + 9596, + 0, + 0 + ], + [ + 9600, + 0, + 0 + ], + [ + 9608, + 0, + 0 + ], + [ + 10949, + 0, + 0 + ], + [ + 10998, + 0, + 0 + ], + [ + 10999, + 0, + -1 + ], + [ + 11039, + 0, + 0 + ], + [ + 14211, + 0, + 0 + ], + [ + 14653, + 0, + -1 + ], + [ + 14949, + 0, + 0 + ], + [ + 15754, + 0, + -1 + ], + [ + 15755, + 0, + -2 + ], + [ + 15761, + 0, + -1 + ], + [ + 18338, + 1, + -2 + ], + [ + 18339, + 1, + -2 + ], + [ + 18340, + 1, + -2 + ], + [ + 18341, + 1, + -2 + ], + [ + 18342, + 1, + -2 + ], + [ + 18343, + 1, + -2 + ], + [ + 18344, + -1, + -2 + ], + [ + 18345, + -1, + -2 + ], + [ + 18379, + 0, + -2 + ], + [ + 18457, + 0, + -2 + ], + [ + 18469, + -1, + -2 + ], + [ + 18688, + -1, + -2 + ], + [ + 18699, + 0, + -2 + ], + [ + 18845, + 0, + -2 + ], + [ + 18875, + 0, + -2 + ], + [ + 18889, + 0, + -2 + ], + [ + 18903, + 0, + -2 + ], + [ + 18913, + 0, + -2 + ], + [ + 18976, + -1, + -2 + ], + [ + 18993, + -1, + -2 + ], + [ + 19124, + -1, + -2 + ], + [ + 19195, + -1, + -2 + ], + [ + 19361, + -2, + -2 + ], + [ + 19391, + -1, + -2 + ], + [ + 19501, + -1, + -2 + ], + [ + 19531, + 0, + -2 + ], + [ + 19555, + 0, + -2 + ], + [ + 19569, + -1, + -2 + ], + [ + 19589, + -1, + -2 + ], + [ + 19645, + -1, + -2 + ], + [ + 19869, + -2, + -1 + ], + [ + 19989, + -2, + -1 + ], + [ + 20011, + -1, + -1 + ], + [ + 20039, + -1, + -1 + ], + [ + 20060, + -1, + -1 + ], + [ + 20106, + -1, + -1 + ], + [ + 20131, + -1, + -1 + ], + [ + 20200, + -1, + -1 + ], + [ + 20225, + -1, + -1 + ], + [ + 20244, + -1, + -1 + ], + [ + 20283, + 0, + -1 + ], + [ + 20323, + 0, + -1 + ], + [ + 20698, + -2, + -1 + ], + [ + 20738, + -1, + -1 + ], + [ + 20771, + -1, + -1 + ], + [ + 20892, + -1, + -1 + ], + [ + 21081, + -1, + -1 + ], + [ + 21139, + -1, + -1 + ], + [ + 21190, + -1, + -1 + ], + [ + 21228, + 0, + -1 + ], + [ + 21418, + 0, + -1 + ], + [ + 21552, + -2, + -1 + ], + [ + 21613, + -1, + -1 + ], + [ + 21692, + -1, + -1 + ], + [ + 21758, + 0, + -1 + ], + [ + 21781, + 0, + -1 + ], + [ + 22035, + -1, + -1 + ], + [ + 22067, + -1, + -1 + ], + [ + 22124, + 0, + -1 + ], + [ + 22225, + 0, + -1 + ], + [ + 22259, + -1, + -1 + ], + [ + 22288, + 0, + -1 + ], + [ + 22428, + 0, + -1 + ], + [ + 22716, + 0, + -1 + ], + [ + 22756, + 0, + -1 + ], + [ + 22762, + 0, + -1 + ], + [ + 22782, + 0, + -1 + ], + [ + 22783, + 0, + -2 + ], + [ + 22784, + 0, + -2 + ], + [ + 22785, + 0, + -2 + ], + [ + 22786, + 0, + -1 + ], + [ + 22787, + 0, + -1 + ], + [ + 22788, + 0, + -1 + ], + [ + 22789, + 0, + 0 + ], + [ + 22790, + 0, + 0 + ], + [ + 22791, + 0, + 0 + ], + [ + 22792, + 0, + 0 + ], + [ + 22793, + 0, + 0 + ], + [ + 22794, + 0, + 0 + ], + [ + 22795, + 0, + 0 + ], + [ + 22796, + 0, + -1 + ], + [ + 22797, + 0, + -1 + ], + [ + 22798, + 0, + -1 + ], + [ + 22799, + 0, + 0 + ], + [ + 22800, + 0, + 0 + ], + [ + 22801, + 0, + 0 + ], + [ + 22812, + 0, + 0 + ], + [ + 22963, + 0, + 0 + ], + [ + 23146, + 0, + 0 + ], + [ + 23176, + 0, + 0 + ], + [ + 23187, + 0, + 0 + ], + [ + 23228, + 0, + 0 + ], + [ + 23267, + -1, + 0 + ], + [ + 23318, + 0, + 0 + ], + [ + 23346, + 1, + 0 + ], + [ + 23386, + 1, + 0 + ], + [ + 23439, + -1, + 0 + ], + [ + 23479, + -1, + 0 + ], + [ + 23608, + -1, + 0 + ], + [ + 24129, + 0, + 0 + ], + [ + 24256, + 0, + 0 + ], + [ + 24362, + 0, + 0 + ], + [ + 24424, + 0, + 0 + ], + [ + 24523, + 0, + 0 + ] + ], + "coupling_block": { + "first_incident_event": 18338, + "last_incident_event": 24523, + "incident_adds": 104, + "shared_event": 22786, + "shared_coefficient": "-2", + "signs": [ + -1, + 1 + ], + "exponents": [ + -4, + -3, + -2, + -1, + 0, + 1, + 2, + 3, + 4 + ], + "conditional_single_deltas_real": [ + [ + -30, + -33, + -36, + -39, + -42, + -43, + -41, + -38, + -35 + ], + [ + -6, + -9, + -12, + -14, + -12, + -9, + -6, + -3, + 0 + ] + ], + "single_optimal_exponents": [ + [ + 1 + ], + [ + -1 + ] + ], + "joint_minimizers": [ + [ + 0, + -1 + ] + ], + "joint_delta_real": -56, + "best_tied_single_delta_real": -53 + }, + "invariant": { + "inserted_scales": 59, + "scale_primitives_real": 66, + "changed_adds": 145, + "add_delta_real": -303, + "delta_real": -237 + }, + "before": { + "complex_primitives": 149018, + "prefix_l1": "14824960514781440791821/64", + "prefix_bits": 68, + "grid_depth_upper": 26, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "after": { + "complex_primitives": 148544, + "prefix_l1": "14824960514781440791821/64", + "prefix_bits": 68, + "grid_depth_upper": 26, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "candidate_sha256": "c9623623ae55fbb9215eda20c40601054df2511cc77c75680dd1faf10dd45315" + } + }, + "formal_columns": 712, + "lowerer_checks": { + "adds": 327, + "scales": 23 + }, + "controls": { + "rejected": [ + "forward: omitted transition", + "forward: omitted transition changes map", + "forward: wrong scale frame", + "forward: exponent out of domain", + "forward: missing ADD schedule", + "backward: omitted transition", + "backward: omitted transition changes map", + "backward: wrong scale frame", + "backward: exponent out of domain", + "backward: missing ADD schedule", + "source corruption", + "source inventory omission" + ], + "tiny_paths": 729, + "zero_schedule_orientations": 2 + }, + "status": "PASS_K8_PAIRED_TEMPORAL_NO_NEW_KAPPA" +} diff --git a/research/k8-paired-temporal-seed23/CLAIM.md b/research/k8-paired-temporal-seed23/CLAIM.md new file mode 100644 index 0000000000..79b97ce68b --- /dev/null +++ b/research/k8-paired-temporal-seed23/CLAIM.md @@ -0,0 +1,63 @@ +# Paired temporal gauges with zero nonscalar boundaries + +Claimed 2026-10-13 23:32 UTC by Sagar Thakrar, with substantial OpenAI Codex +assistance. Apache-2.0. Track: complex supplier. OS-random assignment seed: 23. +Exact base: `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. +Branch: `research/cycle15-seed23-paired-temporal`. +Expected finish: 2026-10-14 00:07 UTC; verification/handoff starts by 23:57 UTC. + +## Candidate tasks and choice + +1. Another constant multihelper gauge. Declined: PR1263, PR1310 and PR1322 + already cover coordinate, pair and coherent-triple moves. +2. Another single-helper temporal gauge or independent composition. Declined: + PR1259, PR1270, PR1350 and PR1353 cover that mechanism; fresh Discussion1163 + claims cover zero-static helpers and L248/L253 composition. +3. Jointly optimize *interacting* temporal gauges with zero at every nonscalar + boundary. Selected. Shared ADDs depend on the difference of the two gauges, + so independent minima need not compose. This changes the optimization class. + +## Exact scope and method + +The selected PR1094 provider is the byte-identical seven-slot k8 provider in +the retained PR1042 archive. The eligible inventory has 237 cold/FULL, +unwrapped, non-center helpers without COPY/CLEAR. Its forward ADD interaction +graph has 2,414 unordered pairs. Seed23 selects sorted pairs [23:39]: +`(225,342), (225,347), (225,348), (225,350), (225,351), (225,352), (225,356), +(225,367), (225,379), (225,384), (225,388), (225,391), (225,395), (225,399), +(225,400), (225,401)`. + +For each pair and both orientations, optimize both exponents in [-4,4] before +every incident ADD. Both gauges must be zero at every nonscalar event and at +entry/exit. All other gauges are zero. Keep every original event, SCALE, +operand, frame, and recursive child. Charge changed ADD lowering, every +transition SCALE, and every reset. Use an exact two-dimensional shortest-path +recurrence and a separate dense transition oracle. Complete all 32 cases; +no enlarged box or further pair search is planned. This is a finite-domain +experiment, not an all-integer or global optimum claim. + +An optimistic complete scalar budget is the sum of all original macro prices, +changed ADD prices, and L1 variation of both exponent paths, including resets. +Only a negative complete delta is an improvement. A useful paired result must +also explain shared-ADD coupling relative to the independently optimized paths. +Paid recursive profiles stay fixed, so no new kappa follows from scalar savings. + +Expected artifact: one source-pinned finite construction or scoped negative +result, deterministic verifier/certificate, meaningful adverse controls, full +712-column scalar replay, and explicit local precision/frame limits. + +## Coordination and predecessors + +No pinned sprint issue exists, so this is the local claim requested by the +donor. At entry, 838 open PRs and all 38 discussion bodies were inspected; +Discussion1163's seven comments were read, including its two active temporal +claims. The overlap helper is refreshed before substantial work and submission. +Nearest sources: woklerx PR1161, Hanson Sun/bbMisk PR1214, Sagar Thakrar PR1259, +Philipp/mightyOil PR1263/1270/1310/1322 and Cinna Davis/1337isnot1337 +PR1350/1353. PR1350's L253/L254 follow-up is a different pair and background. +Existing k8 supplier and lowerer attribution is retained in the final note. + +The selected conditional kappa remains `836330098538459/500000000000000000`. +Inherited compiler, common-label/mutable-source, hosting, precision/tape, +analytic and bit H1-H5 obligations remain. No selected/frontier or upstream/ +files will change. diff --git a/research/k8-paired-temporal-seed23/README.md b/research/k8-paired-temporal-seed23/README.md new file mode 100644 index 0000000000..84025b1bb8 --- /dev/null +++ b/research/k8-paired-temporal-seed23/README.md @@ -0,0 +1,226 @@ +# A shared ADD defeats independent temporal gauge optimization + +On the frozen seven-slot k8 complex word, jointly scheduling L225 and L350 +saves **474 scalar primitives per complex invocation in each orientation**. +The joint optimum is **six primitives cheaper than every composition of +individually optimal schedules** in the declared domain, including all ties. +One shared ADD explains the entire difference. + +This is a finite scalar construction and a bounded optimization result. It +does not change the selected supplier, paid recursive profile, or kappa. The +larger constant-gauge construction in PR1263 and its successors already have +lower total scalar bills. This package establishes a coupling effect that +cannot be obtained by adding independently optimized temporal savings. + +| Complete local scalar word | Original | Joint L225/L350 | Saving | +|---|---:|---:|---:| +| Forward | 149,002 | 148,528 | 474 | +| Backward | 149,018 | 148,544 | 474 | + +The forward schedule inserts 55 SCALE macros costing 62 real-component +primitives and saves 299 in ADD lowering. The backward schedule inserts 59 +SCALE macros costing 66 and saves 303 in ADD lowering. Both net savings are +237 per real component. Real coefficients make the complex invoice twice that. + +## Reproduce + +With Python 3.10+ and the standard library, from the repository root: + +```sh +python3 -I -O -B research/k8-paired-temporal-seed23/verify.py +``` + +Expected output: + +```text +PASS_K8_PAIRED_TEMPORAL_NO_NEW_KAPPA pair=225,350 saved=474/474 strict_coupling_gain=6/6 pairs=16 orientations=2 columns=712 +``` + +The verifier writes no files, requires no network or Git history, and also +works when called by absolute path from another directory. `--emit` prints +the recomputed certificate instead of comparing it with [CERTIFICATE.json](CERTIFICATE.json). +Default verification always compares every deterministic certificate field. +Schedules contain the original zero-based event index and both exponents. +They determine the complete emitted word; its canonical JSON SHA256 is in the +certificate. [SOURCES.json](SOURCES.json) pins the immutable input archives, +receipt linkage, three consumed archive members and the literal lowerer. +Historical review/assembly hashes are provenance, not live replay dependencies. + +## Domain and completed coverage + +The investigation base is `bce54fb3f895cbe5cd4c0eb477c3afeed100190f`. +The OS assignment seed was 23, complex supplier. The [claim](CLAIM.md) records +three candidate tasks, overlap checks, the complete selected pair list and the +stopping rule. The source provider has 237 cold/FULL, unwrapped, non-center +helpers without COPY/CLEAR, and 2,414 unordered ADD-interacting pairs. +Seed23 selects sorted pairs [23:39]. All 16 pairs and both orientations are +complete; no pair or exponent-box expansion was performed. + +For each selected pair, both gauge exponents lie in the integers [-4,4]. They +may change before each ADD incident to either helper, and must equal zero +before **every nonscalar event**, including events on unrelated helpers. +Entry and exit exponents are zero. All other helpers have zero gauge. Every +original SCALE remains present and separately priced. No original operation, +operand, frame, source access, wrapper or recursive child is removed or +reordered. No new helper, COPY or CLEAR is introduced. Extra scales use the +helper's current frame, including scales that restore zero before a boundary. + +This domain covers arbitrary timing within each scalar block: between two +incident ADDs, original diagonal SCALEs commute with the gauge, other +operations do not use the selected helper, and the triangle inequality lets +multiple changes collapse into one at the next incident ADD without increasing +cost. There is no all-integer exponent claim and no global circuit optimum. + +Five pairs have a strict gap against **all** tied independent optima in both +orientations: L225 paired with L350, L356, L384, L388 and L401. Their real gaps +are 3, 2, 2, 2 and 2. L225/L350 is selected for the largest strict coupling gap, +with lexicographic pair order breaking ties. L225/L401 has the lowest complete +bill among these 16 pairs; no priority or best-known-circuit claim is made for +the chosen witness. The other eleven pairs show no strict advantage over the +best tied independent composition in this bounded domain. + +## Complete cost and exact recurrence + +Write a nonzero dyadic coefficient as `q = sign(q) p 2^e` with positive odd p. +The retained PR696 ADD lowerer has real-component price + +`C(q) = 1 + bit_length(p) + popcount(p) + |e| - [p=1 and e=0]`. + +This includes coefficient-work initialization and clearing. A SCALE by `2^d` +costs `|d|`. For a state `s=(a,b)`, an incident ADD's coefficient becomes +`q 2^(sigma_a a + sigma_b b)`, where each sigma is +1 for the destination, +-1 for the source and zero otherwise. A shared ADD uses their difference and +is charged once. + +Inside a scalar block, set `D_0(0,0)=0` and all other initial costs to infinity. +For each incident ADD i, the exact recurrence is + +`D_i(s) = C(q_i 2^(sigma_i dot s)) - C(q_i) + min_t(D_(i-1)(t) + ||s-t||_1)`. + +The block price is `min_s(D_last(s)+||s||_1)`, charging restoration. Sum block +prices and add the complete original word's invoice. All recursive work is +retained, so there is no discount to hide outside this scalar delta. + +[search.py](search.py) evaluates the transition minimum by two coordinate +distance transforms. [verify.py](verify.py) separately enumerates all 81 by 81 +state transitions with literal PR696 lowering lengths. It checks 49,693,014 +transition candidates across all 32 cases. These implementations share the +source-derived incident list and finite domain; they are independent transition +and price calculations, not independent extraction of the whole supplier. + +To handle ties correctly, the main checker finds each single-coordinate +shortest-path DAG using forward/backward costs, then minimizes joint cost over +the product of those DAGs. The dense oracle instead minimizes a lexicographic +pair: first the sum of the two independently charged path costs, then the +actual joint cost. The first objective attains the sum of the separate minima +because paths can be chosen independently; equality forces both paths to be +individually optimal. The second objective therefore checks every tied +composition without relying on the DAG implementation. Both methods agree. + +## The small coupling witness + +Only one block contributes the strict gap for L225/L350. Its incident events +run from 18,338 through 24,523, with 104 incident ADDs and just one shared ADD +at event 22,786. Forward, that shared ADD has coefficient 2 and exponent `a-b`. + +Let A(a) and B(b) be the independently optimized real-component block deltas, +conditioned on each helper's exponent at that shared ADD. Both include all +entry/transition/exit scales. The verifier reconstructs these profiles using +separate one-dimensional prefix and suffix minima and literal lowering: + +| Exponent | -4 | -3 | -2 | -1 | 0 | 1 | 2 | 3 | 4 | +|---|---:|---:|---:|---:|---:|---:|---:|---:|---:| +| A, L225 | -35 | -38 | -41 | -43 | -42 | -39 | -36 | -33 | -30 | +| B, L350 | 0 | -3 | -6 | -9 | -12 | -14 | -12 | -9 | -6 | + +Since there is exactly one shared ADD, the complete joint block delta is + +`A(a)+B(b)+C(2*2^(a-b))-C(2*2^a)-C(2*2^(-b))+C(2)`. + +The independent minimizers force `(a,b)=(-1,1)`. Their nominal sum is -57, +but the shared-operation correction is +4, giving -53. The unique best joint +state is `(0,1)`: A pays one more primitive while avoiding all four of that +correction, giving **-56**. All 81 state pairs are checked. Thus arbitrary +tie-breaking elsewhere cannot remove the three-primitive gap. The backward +profiles reverse the exponent order; its unique joint state is `(0,-1)` and +its separate minima force `(1,-1)`, with the same costs. + +Other blocks contribute the same -181 optimum with or without this coupling. +The full joint delta is -237, versus -234 for the best tied independent +composition. Twice their difference gives the six-primitive complex gain. + +## Identity, accounting and checks + +The actual candidate stream is parsed independently of its schedule. The +checker tracks the relative diagonal scale, verifies every conjugated ADD, +retains each original event, checks all inserted scale frames, and requires +both gauges to be zero at every nonscalar event. Thus the original nonscalar +interfaces receive exactly the same registers. This supplies an event-by-event +invariant, not an assumption that nonzero gauges commute through children. + +Both original and candidate scalar words replay on all 712 formal columns in +both directions, including arbitrary helper dirt and all private centers. +All 327 distinct ADD coefficients and 23 SCALE coefficients pass separate +literal primitive-map checks, including arbitrary coefficient-work input. +Complete literal invoices match the recurrence and the inherited paid profiles. +The local positive-prefix ceilings remain 52 bits forward and 68 backward; +the denominator-depth bounds remain 22 and 26. Their signed fixed-point +payload fits the retained 192-bit local allowance. + +The verifier includes 729 exhaustive tiny paths, two zero-schedule controls, +and twelve rejection checks for missing transition work, changed endpoints, +wrong frames, out-of-domain exponents, incomplete schedules, source corruption +and source-inventory omission. [VALIDATION.json](VALIDATION.json) records the +tested runtimes, source Git-blob checks, outside-checkout execution and repository +checks. + +The full selected cold replay and native/hosted admission were not run. The +added macro events can change adapter accounting in a future physical +composition. Local scalar savings alone do not establish a cheaper supplier +invoice or multiplication runtime. Inherited compiler, realization, +common-label/mutable-source, whole-call hosting, global precision/tape, +analytic-transfer and bit H1-H5 obligations remain. No finite replay here is +a formal proof of the full theorem. Selected kappa at the base remains +`836330098538459/500000000000000000`. + +## Predecessors and concurrent work + +- @woklerx PR1161 introduced the single-helper constant gauge. Hanson Sun / + @bbMisk PR1214 established the at-most-two constant-gauge optimum and priced + shared ADDs. Those constant families differ from this temporal family. +- Sagar Thakrar's PR1259 supplies the temporal recurrence, source loading, + sparse scalar replay and primitive invoice code adapted here. Philipp / + @mightyOil PR1270 supplies the zero-at-every-nonscalar-boundary contract and + single-helper census. These mechanisms are credited, not rediscovered claims. +- Philipp's PR1263/1310/1322 treat simultaneous constant gauges, pair moves and + coherent triples. Cinna Davis / @1337isnot1337 PR1350/1353 add L253/L248 + temporal gauges over a fixed many-helper background. Concurrent PR1369 now + covers the zero-static single helpers, and PR1376 proves that the disjoint + L248/L253 temporal objectives separate. This package starts at the original + zero-gauge word and proves a strict interaction gap for a different pair. + It does not claim superiority to their invoices. All these source heads are + recorded in SOURCES.json; PR1369/1376 are context, not runtime dependencies. +- The unchanged k8 provider follows Jeremy Kothe's construction/schedules, + Rohan Arun's selected PR1094 composition, the icekylinx scalar/frame lineage, + and the predecessors in the retained maintainer review. The literal PR696 + lowerer is Sagar Thakrar's contribution, building on that lineage. + +Contribution by Sagar Thakrar / `thakrarsagar`, with substantial OpenAI Codex +assistance in research, implementation, proof writing and review. New files +are under the repository's Apache-2.0 license. No independent human review is +claimed. Frozen packages, selected records and `upstream/` are unchanged. + +## Open next questions + +1. Can this pair's strict coupling advantage survive a fixed many-helper + background? First rederive the two conditional profiles on a pinned + PR1263/1310/1322 word. Their altered coefficients prevent adding these + savings numerically. Check active temporal claims before starting. +2. What physical invoice results after admitting the added SCALE events? + Begin with the unchanged native frame checker and count every added adapter. + Macro-event overhead may outweigh the local scalar saving; no favorable + supplier conclusion is assumed here. +3. Does an exact clipping argument close the unbounded two-coordinate domain? + Start from the single-shared-ADD conditional profiles. Independent clipping + need not preserve their difference, so the single-helper proof alone is + insufficient. The present [-4,4] census leaves that question open. diff --git a/research/k8-paired-temporal-seed23/SOURCES.json b/research/k8-paired-temporal-seed23/SOURCES.json new file mode 100644 index 0000000000..783c750aa5 --- /dev/null +++ b/research/k8-paired-temporal-seed23/SOURCES.json @@ -0,0 +1,34 @@ +{ + "base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "seed": 23, + "selected_kappa_at_base": "836330098538459/500000000000000000", + "files": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/community-frontier1042-audit/RESULT.json": "bf12c6ed3b412539638b76addb40591a631609b2ab9e5ee0db1f6bbe067d0ec0", + "research/community-frontier1094-audit/selected-replay.tar.gz": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "research/community-frontier1094-audit/RESULT.json": "1e3e47e9ec24bcb6fb5f703b7fce0aab658d84ff72bfae5da3ae429d17b6e752", + "research/complex-dyadic-lowering/lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + }, + "archive_members": { + "CANONICAL-WORD.json.gz": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "LOCAL-PROGRAMS.json.gz": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "INDEPENDENT-LOCAL-REPLAY.json": "13dd18297162569532983db1a2ab67926b064330cd7edd3587e7b546b2dedf17" + }, + "historical_context_files": { + "research/community-frontier1094-audit/ASSEMBLY.json": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "docs/research/community-batch1099-review.md": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + "predecessor_heads": { + "1161": "d210969d3158a1e6c505e41f67dd84e555c88564", + "1214": "26162c56ec9c50a80e49949f36d4dd9a137a76a6", + "1259": "61367611154266a982fe25e1a6243a8aad77227d", + "1263": "5fbaca13028846bddbb001e8e07addc2ab8e5816", + "1270": "69bc8d601d4738dc511fc76f869e1f3c3d4bc3d4", + "1310": "b9ca10f02fca37c8214d880c244ac14ead6bae7a", + "1322": "be26b6de169ff891ef8a5e5630af47557d4401b9", + "1350": "64b8a55c6933ffb6d9e30fa19f85d05b572d4aa5", + "1353": "efc6bfc3302a966ac0e1f5f4656e94b4cabeb9ca", + "1369": "f28e1c460cd910886f9b06835abd6b1c96d2992f", + "1376": "49f112ac76e95415fcea8969de28f74c8928b2b1" + } +} diff --git a/research/k8-paired-temporal-seed23/VALIDATION.json b/research/k8-paired-temporal-seed23/VALIDATION.json new file mode 100644 index 0000000000..ce05fc441b --- /dev/null +++ b/research/k8-paired-temporal-seed23/VALIDATION.json @@ -0,0 +1,70 @@ +{ + "status": "PASS_LOCAL_FINITE_VERIFICATION", + "verified_at_utc": "2026-10-13T23:46:00Z", + "base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", + "platform": "macOS-26.5.2-arm64-arm-64bit-Mach-O", + "certificate_sha256": "3c59f72bcd0768bf0740edebcb09427bcd48659b8bcbba762a0e30ca53aa2afc", + "replays": [ + { + "runtime": "CPython 3.14.8", + "command": "python3.14 -I -B research/k8-paired-temporal-seed23/verify.py", + "cwd": "repository root", + "exit": 0, + "seconds": 11.257 + }, + { + "runtime": "CPython 3.11.15", + "command": "python3.11 -I -O -B /research/k8-paired-temporal-seed23/verify.py", + "cwd": "/tmp", + "exit": 0, + "seconds": 15.874 + } + ], + "coverage": { + "selected_pairs": 16, + "orientations": 2, + "exponent_states_per_incident_add": 81, + "dense_transition_candidates": 49693014, + "formal_columns_per_word": 712, + "replayed_words": "original and selected candidate, both orientations", + "literal_add_coefficients": 327, + "literal_scale_coefficients": 23, + "tiny_exhaustive_paths": 729, + "embedded_rejection_controls": 12, + "zero_schedule_controls": 2, + "external_saved_certificate_corruption": "seed23 changed to24: optimized isolated default verification exits1 with saved certificate mismatch; original bytes restored" + }, + "other_checks": [ + "scripts/verify_selected_result.py: PASS selected record, exact kappa, original source inventory and proof supplement", + "git diff --check: PASS", + "all seven source/context SHA256 values agree with live bytes and git show at the exact base" + ], + "source_git_blobs": { + "research/community-frontier1042-audit/selected-replay.tar.gz": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "research/community-frontier1042-audit/RESULT.json": "8182d0818c0cbda7e52c10120f15b2c3a2c8f933", + "research/community-frontier1094-audit/selected-replay.tar.gz": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "research/community-frontier1094-audit/RESULT.json": "131d9c96a54632ae385ced4138fd7f30ad448a3e", + "research/complex-dyadic-lowering/lower.py": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8", + "research/community-frontier1094-audit/ASSEMBLY.json": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "docs/research/community-batch1099-review.md": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099" + }, + "overlap_refresh": { + "at_utc": "2026-10-13T23:44:20.652081Z", + "open_prs": 847, + "discussion_records": 94, + "local_records": 326, + "complete_remote_pagination": true, + "nearest_match": "PR1270 remains single-helper zero-boundary optimization and composition over a fixed two-helper word; no joint pair optimum", + "pinned_issue": false, + "final_pr_metadata_at_utc": "2026-10-13T23:47:42Z", + "final_open_prs": 850, + "new_relevant_results": "PR1369 zero-static one-coordinate census and PR1376 disjoint L248/L253 composition are distinct; exact heads and credit added to SOURCES.json and README.md" + }, + "not_checked": [ + "full selected cold replay", + "native or hosted admission and complete supplier adapter invoice", + "all-integer exponent schedules outside [-4,4] or other pairs", + "Linux, hosted CI success, Lean formalization, independent human review" + ], + "no_new_kappa": true +} diff --git a/research/k8-paired-temporal-seed23/replay.py b/research/k8-paired-temporal-seed23/replay.py new file mode 100644 index 0000000000..72a20a6e97 --- /dev/null +++ b/research/k8-paired-temporal-seed23/replay.py @@ -0,0 +1,174 @@ +"""Selected-provider scalar checks, adapted from Sagar Thakrar's PR1259. + +Sagar Thakrar with substantial OpenAI Codex assistance, Apache-2.0. +Retains the icekylinx/Jeremy Kothe supplier and PR696 lowerer semantics. +""" +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import json +from pathlib import Path +import runpy +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SEARCH = runpy.run_path(str(HERE / "search.py")) +require = SEARCH["require"] +OLD = "research/community-frontier1042-audit/" +NEW = "research/community-frontier1094-audit/" +LOWER = "research/complex-dyadic-lowering/lower.py" +FILES = {OLD + "selected-replay.tar.gz", NEW + "selected-replay.tar.gz", + OLD + "RESULT.json", NEW + "RESULT.json", LOWER} +MEMBERS = {"CANONICAL-WORD.json.gz", "LOCAL-PROGRAMS.json.gz", "INDEPENDENT-LOCAL-REPLAY.json"} + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False).encode() + + +def load(root=ROOT, manifest=None): + m = manifest if manifest is not None else json.loads((HERE / "SOURCES.json").read_bytes()) + require(m["base"] == "bce54fb3f895cbe5cd4c0eb477c3afeed100190f" and m["seed"] == 23, "assignment pin") + require(set(m["files"]) == FILES and set(m["archive_members"]) == MEMBERS, "complete source inventory") + for path, pin in m["files"].items(): + require(digest((root / path).read_bytes()) == pin, "source pin " + path) + result = {} + with tarfile.open(root / (OLD + "selected-replay.tar.gz")) as old, tarfile.open(root / (NEW + "selected-replay.tar.gz")) as new: + for name in sorted(MEMBERS): + raw = old.extractfile("slots/local/" + name).read() + require(digest(raw) == m["archive_members"][name], "archive member " + name) + actual = new.extractfile("candidate/strict/global8/base/providers/gauge44/" + name).read() + require(raw == actual, "selected provider alias " + name) + result[name] = json.loads(gzip.decompress(raw) if name.endswith(".gz") else raw) + old = json.loads((root / (OLD + "RESULT.json")).read_bytes()) + new = json.loads((root / (NEW + "RESULT.json")).read_bytes()) + require(old["status"] == "PASS_COMPLETE_PR1042_COMPOSITION" and new["status"] == "PASS_COMPLETE_PR1094_COMPOSITION", "receipt status") + require(new["baseline_receipt_sha256"] == m["files"][OLD + "RESULT.json"], "selected baseline binding") + word = result["CANONICAL-WORD.json.gz"] + require((word["v"], word["h"], word["R"]) == (112, 9, 480), "source geometry") + return word, result["LOCAL-PROGRAMS.json.gz"], result["INDEPENDENT-LOCAL-REPLAY.json"], runpy.run_path(str(root / LOWER))["lower"] + + +def apply(g, rows): + tag, t = g[0], tuple(g[1]) + if tag == "clear": + rows[t] = {} + elif tag == "copy": + rows[t] = dict(rows[tuple(g[2])]) + elif tag in ("scale", "double", "halve", "negate"): + q = Q(g[2], g[3]) if tag == "scale" else {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[t] = {i: q * a for i, a in rows[t].items()} + else: + require(tag in ("add", "subtract"), "scalar opcode") + s = tuple(g[2]) + require(s != t, "distinct ADD operands") + q = Q(g[3], g[4]) if len(g) == 5 else Q(1 if tag == "add" else -1) + for i, a in rows[s].items(): + v = rows[t].get(i, Q(0)) + q * a + if v: + rows[t][i] = v + else: + rows[t].pop(i, None) + + +def replay(events, orientation): + rows = {("L", i): {i: Q(1)} for i in range(704)} + rows.update({("C", i): {704 + i: Q(1)} for i in range(8)}) + for e in events: + if e[0] == "scalar": + apply(e[1], rows) + for i in range(704): + expected = {i: Q(1)} + if orientation == "forward" and 112 <= i < 224: + expected[i - 112] = Q(1) + if orientation == "backward" and i < 112: + expected[i + 112] = Q(-1) + require(rows["L", i] == expected, "all-column endpoint " + str((orientation, i))) + require(all(not rows["C", i] for i in range(8)), "private centers cleared") + + +def frame_check(events, word, pair): + frames = {h: word["start"][h] for h in pair} + for e in events: + if e[0] == "climb" and e[2] in pair: + require(frames[e[2]] == e[3], "helper climb incidence") + frames[e[2]] = e[4] + elif e[0] == "scalar": + for h in pair: + if ["L", h] in e[1]: + require(frames[h] == e[2], "helper scalar frame") + require(e[1][0] in ("add", "scale"), "helper COPY/CLEAR excluded") + elif e[0] == "residual_adapter": + require(e[2] not in pair, "helper wrapper excluded") + require(all(frames[h] == word["final"][h] for h in pair), "helper final frame") + + +def invoice(events, lower): + env = {("L", i): Q(1) for i in range(704)} + env.update({("C", i): Q(1) for i in range(8)}) + env["W", 0] = Q(1) + depths = {r: 0 for r in env} + peak, max_depth, count = Q(1), 0, 0 + paid = Counter() + for e in events: + if e[0] == "climb": + paid[e[5]] += 1 + if e[0] == "center": + paid[e[4]] += 1 + if e[0] != "scalar": + continue + for g in lower(e[1]): + count += 1 + tag, t = g[0], tuple(g[1]) + if tag == "clear": + env[t], depths[t] = Q(0), 0 + elif tag == "copy": + env[t], depths[t] = env[tuple(g[2])], depths[tuple(g[2])] + elif tag == "double": + env[t] *= 2 + depths[t] = max(0, depths[t] - 1) + elif tag == "halve": + env[t] /= 2 + depths[t] += 1 + elif tag in ("add", "subtract"): + env[t] += env[tuple(g[2])] + depths[t] = max(depths[t], depths[tuple(g[2])]) + else: + require(tag == "negate", "primitive opcode") + peak = max(peak, env[t]) + max_depth = max(max_depth, depths[t]) + if e[1][0] == "add": + require(env["W", 0] == 0, "coefficient work cleared") + bits = peak.numerator.bit_length() - peak.denominator.bit_length() + 1 + require(bits + max_depth < 192, "local signed fixed-point payload guard") + return {"complex_primitives": 2 * count, "prefix_l1": str(peak), "prefix_bits": bits, + "grid_depth_upper": max_depth, "paid_profile": {str(k): v for k, v in sorted(paid.items())}} + + +def lowerer_checks(programs, lower): + adds, scales = set(), set() + for events in programs: + for e in events: + if e[0] == "scalar" and e[1][0] == "add": + adds.add(Q(e[1][3], e[1][4])) + elif e[0] == "scalar" and e[1][0] == "scale": + scales.add(Q(e[1][2], e[1][3])) + for q in adds: + g = ["add", ["L", 0], ["L", 1], q.numerator, q.denominator] + rows = {("L", 0): {0: Q(1)}, ("L", 1): {1: Q(1)}, ("W", 0): {2: Q(1)}} + for op in lower(g): + apply(op, rows) + require(rows == {("L", 0): {0: Q(1), 1: q}, ("L", 1): {1: Q(1)}, ("W", 0): {}}, "arbitrary-work ADD map") + require(len(lower(g)) == SEARCH["price"](q), "literal/formula price") + for q in scales: + rows = {("L", 0): {0: Q(1)}} + for op in lower(["scale", ["L", 0], q.numerator, q.denominator]): + apply(op, rows) + require(rows == {("L", 0): {0: q}}, "lowered SCALE map") + return {"adds": len(adds), "scales": len(scales)} diff --git a/research/k8-paired-temporal-seed23/search.py b/research/k8-paired-temporal-seed23/search.py new file mode 100644 index 0000000000..f869aa6534 --- /dev/null +++ b/research/k8-paired-temporal-seed23/search.py @@ -0,0 +1,185 @@ +"""Joint bounded temporal gauges. Sagar Thakrar / OpenAI Codex, Apache-2.0. + +Extends the single-helper recurrence of Sagar Thakrar PR1259 and the zero-boundary +contract of Philipp/mightyOil PR1270. Coefficient price is the retained PR696 one. +""" +from copy import deepcopy +from fractions import Fraction as Q +from itertools import product + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def power(k): + return Q(2) ** k + + +def price(q): + a, d = abs(q.numerator), q.denominator + require(a > 0 and d & (d - 1) == 0, "nonzero dyadic coefficient") + v = (a & -a).bit_length() - 1 + odd, exponent = a >> v, v - (d.bit_length() - 1) + return 1 + odd.bit_length() + odd.bit_count() + abs(exponent) - int(odd == 1 and exponent == 0) + + +def eligible(word, programs): + excluded = set(word["centers"]) + for events in programs.values(): + for e in events: + if e[0] == "residual_adapter": + excluded.add(e[2]) + if e[0] == "scalar" and e[1][0] in ("copy", "clear"): + excluded.update(r[1] for r in e[1][1:] if isinstance(r, list) and r[0] == "L") + return [h for h in range(224, 704) if h not in excluded + and word["start"][h] == 0 and word["final"][h] == 1] + + +def pairs(programs, helpers): + result = set() + for e in programs["forward"]: + if e[0] == "scalar" and e[1][0] == "add": + a, b = e[1][1:3] + if a[0] == b[0] == "L" and a[1] in helpers and b[1] in helpers: + result.add(tuple(sorted((a[1], b[1])))) + return sorted(result) + + +def segments(events, pair): + result, current = [], [] + for i, e in enumerate(events): + if e[0] != "scalar": + if current: + result.append(current) + current = [] + elif e[1][0] == "add": + g = e[1] + signs = tuple(int(g[1] == ["L", h]) - int(g[2] == ["L", h]) for h in pair) + if any(signs): + current.append((i, Q(g[3], g[4]), signs)) + if current: + result.append(current) + return result + + +def distance(a, b): + return sum(abs(x - y) for x, y in zip(a, b)) + + +def optimize(blocks, domains=((-4, 4), (-4, 4))): + states = list(product(*(range(lo, hi + 1) for lo, hi in domains))) + require((0, 0) in states, "zero belongs to both gauge domains") + schedule, total = [], 0 + for block in blocks: + dp = {s: distance(s, (0, 0)) for s in states} + parents = [] + for _, q, signs in block: + # Separable exact L1 distance transform, retaining the predecessor. + best = {s: (v, s) for s, v in dp.items()} + for axis in range(2): + for order, step in ((states, 1), (list(reversed(states)), -1)): + for s in order: + t = list(s) + t[axis] -= step + t = tuple(t) + if t in best: + best[s] = min(best[s], (best[t][0] + 1, best[t][1])) + dp = {s: best[s][0] + price(q * power(sum(a * b for a, b in zip(s, signs)))) - price(q) + for s in states} + parents.append({s: best[s][1] for s in states}) + cost, state = min((v + distance(s, (0, 0)), s) for s, v in dp.items()) + total += cost + path = [] + for parent in reversed(parents): + path.append(state) + state = parent[state] + schedule.extend([[term[0], *s] for term, s in zip(block, reversed(path))]) + return {"delta_real": total, "schedule": schedule} + + +def schedule_cost(blocks, schedule): + require([r[0] for r in schedule] == [t[0] for b in blocks for t in b], "exact schedule coverage") + states = {i: (a, b) for i, a, b in schedule} + cost = 0 + for block in blocks: + old = (0, 0) + for i, q, signs in block: + new = states[i] + cost += distance(old, new) + price(q * power(sum(a * b for a, b in zip(new, signs)))) - price(q) + old = new + cost += distance(old, (0, 0)) + return cost + + +def tied_single_minimum(blocks, bound=4): + """Cheapest joint path among ALL separately optimal paths, including ties.""" + values = list(range(-bound, bound + 1)) + total = 0 + for block in blocks: + allowed = [] + for axis in range(2): + costs = [{k: price(q * power(signs[axis] * k)) - price(q) for k in values} + for _, q, signs in block] + forward = [{0: 0}] + for c in costs: + forward.append({k: min(v + abs(k - j) for j, v in forward[-1].items()) + c[k] + for k in values}) + optimum = min(v + abs(k) for k, v in forward[-1].items()) + backward = [None] * (len(block) + 1) + backward[-1] = {k: abs(k) for k in values} + for i in range(len(block) - 1, -1, -1): + backward[i] = {j: min(abs(k - j) + costs[i][k] + backward[i + 1][k] for k in values) + for j in values} + allowed.append([{k: [j for j, v in forward[i].items() + if v + abs(k - j) + costs[i][k] + backward[i + 1][k] == optimum] + for k in values} for i in range(len(block))]) + dp = {(0, 0): 0} + for i, (_, q, signs) in enumerate(block): + new = {} + for a, b in product(values, repeat=2): + predecessors = [(x, y) for x in allowed[0][i][a] for y in allowed[1][i][b] if (x, y) in dp] + if predecessors: + new[a, b] = min(dp[t] + distance((a, b), t) for t in predecessors) + new[a, b] += price(q * power(a * signs[0] + b * signs[1])) - price(q) + dp = new + require(bool(dp), "nonempty tied optimum paths") + total += min(v + distance(s, (0, 0)) for s, v in dp.items()) + return total + + +def transform(events, word, pair, schedule): + blocks = segments(events, pair) + schedule_cost(blocks, schedule) + require(all(type(k) is int and -4 <= k <= 4 for row in schedule for k in row[1:]), "bounded integer exponents") + by_index = {i: (a, b) for i, a, b in schedule} + current, frames, result = [0, 0], [word["start"][h] for h in pair], [] + inserted = 0 + + def move(new): + nonlocal inserted + for j, h in enumerate(pair): + if new[j] != current[j]: + q = power(new[j] - current[j]) + result.append(["scalar", ["scale", ["L", h], q.numerator, q.denominator], frames[j]]) + inserted += 1 + current[j] = new[j] + + for i, original in enumerate(events): + e = deepcopy(original) + if e[0] != "scalar": + move((0, 0)) + if i in by_index: + move(by_index[i]) + g = e[1] + k = sum(current[j] * (int(g[1] == ["L", h]) - int(g[2] == ["L", h])) for j, h in enumerate(pair)) + q = Q(g[3], g[4]) * power(k) + g[3:5] = [q.numerator, q.denominator] + result.append(e) + if e[0] == "climb" and e[2] in pair: + j = pair.index(e[2]) + require(frames[j] == e[3], "frame chronology") + frames[j] = e[4] + move((0, 0)) + return result, inserted diff --git a/research/k8-paired-temporal-seed23/verify.py b/research/k8-paired-temporal-seed23/verify.py new file mode 100644 index 0000000000..0d9ba0fc34 --- /dev/null +++ b/research/k8-paired-temporal-seed23/verify.py @@ -0,0 +1,253 @@ +"""Exact bounded paired-gauge census and complete finite scalar replay. + +Sagar Thakrar with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +from itertools import product +import json +from pathlib import Path +import runpy + +HERE = Path(__file__).resolve().parent +R = runpy.run_path(str(HERE / "replay.py")) +S = R["SEARCH"] +require = R["require"] + + +def dense_oracle(blocks, lower): + """Explicit 81-by-81 edges and literal macro prices; no L1 sweeps or tight-edge DAG.""" + states = list(product(range(-4, 5), repeat=2)) + lengths = [[abs(a - x) + abs(b - y) for x, y in states] for a, b in states] + boundary = [abs(a) + abs(b) for a, b in states] + cache = {} + + def price(q): + if q not in cache: + cache[q] = len(lower(["add", ["L", 0], ["L", 1], q.numerator, q.denominator])) + return cache[q] + + joint_total, tied_total, independent_total, edges = 0, 0, 0, 0 + for block in blocks: + joint = boundary[:] + lex = [(d, d) for d in boundary] + for _, q, (s, t) in block: + joint_new, lex_new = [], [] + base = price(q) + for n, (a, b) in enumerate(states): + distances = lengths[n] + c = price(q * Q(2) ** (a * s + b * t)) - base + separate = price(q * Q(2) ** (a * s)) + price(q * Q(2) ** (b * t)) - 2 * base + joint_new.append(min(v + d for v, d in zip(joint, distances)) + c) + v = min((x + d, y + d) for (x, y), d in zip(lex, distances)) + lex_new.append((v[0] + separate, v[1] + c)) + joint, lex = joint_new, lex_new + edges += len(states) ** 2 + joint_total += min(v + d for v, d in zip(joint, boundary)) + v = min((a + d, b + d) for (a, b), d in zip(lex, boundary)) + independent_total += v[0] + tied_total += v[1] + return joint_total, tied_total, independent_total, edges + + +def check_transform(original, candidate, word, pair): + """Read the actual candidate stream and verify the diagonal invariant at every event.""" + exponent = dict.fromkeys(pair, 0) + frames = {h: word["start"][h] for h in pair} + j, inserted, scale_cost, add_delta, changed = 0, 0, 0, 0, 0 + for e in original: + incident = e[0] == "scalar" and e[1][0] == "add" and any(["L", h] in e[1][1:3] for h in pair) + if incident or e[0] != "scalar": + while j < len(candidate) and candidate[j][0] == "scalar" and candidate[j][1][0] == "scale": + g = candidate[j][1] + require(g[1][0] == "L" and g[1][1] in pair, "inserted scale helper") + h, q = g[1][1], Q(g[2], g[3]) + require(q > 0 and q.numerator & (q.numerator - 1) == 0 and q.denominator & (q.denominator - 1) == 0, + "inserted positive power of two") + k = q.numerator.bit_length() - q.denominator.bit_length() + require(k != 0 and candidate[j][2] == frames[h], "inserted scale frame/nonidentity") + exponent[h] += k + require(-4 <= exponent[h] <= 4, "actual exponent domain") + scale_cost += abs(k) + inserted += 1 + j += 1 + require(j < len(candidate), "candidate contains original event") + actual = candidate[j] + if incident: + require(actual[:1] == e[:1] and actual[2:] == e[2:] and actual[1][:3] == e[1][:3], "ADD topology/frame") + target, source = e[1][1:3] + a = exponent.get(target[1], 0) if target[0] == "L" else 0 + b = exponent.get(source[1], 0) if source[0] == "L" else 0 + q, v = Q(e[1][3], e[1][4]), Q(actual[1][3], actual[1][4]) + require(v == q * Q(2) ** (a - b), "actual conjugated coefficient") + add_delta += S["price"](v) - S["price"](q) + changed += int(q != v) + else: + require(actual == e, "original event unchanged") + if e[0] != "scalar": + require(not any(exponent.values()), "zero at every nonscalar boundary") + if e[0] == "climb" and e[2] in pair: + require(frames[e[2]] == e[3], "original frame chain") + frames[e[2]] = e[4] + j += 1 + require(j == len(candidate) and not any(exponent.values()), "restored exit and no extra events") + return {"inserted_scales": inserted, "scale_primitives_real": scale_cost, + "changed_adds": changed, "add_delta_real": add_delta, "delta_real": scale_cost + add_delta} + + +def coupling_block(blocks, lower): + """Small 9-by-9 witness for the only block with a strict gap in pair225/350.""" + block = next(b for b in blocks if b[0][0] == 18338) + shared = [i for i, (_, _, signs) in enumerate(block) if all(signs)] + require(len(shared) == 1, "one shared ADD in coupling block") + at = shared[0] + values = range(-4, 5) + + def charge(q): + return len(lower(["add", ["L", 0], ["L", 1], q.numerator, q.denominator])) + + profiles = [] + for axis in range(2): + row = {0: 0} + for _, q, signs in block[:at + 1]: + row = {k: min(v + abs(k - j) for j, v in row.items()) + + charge(q * Q(2) ** (signs[axis] * k)) - charge(q) for k in values} + tail = {k: abs(k) for k in values} + for _, q, signs in reversed(block[at + 1:]): + tail = {j: min(abs(k - j) + charge(q * Q(2) ** (signs[axis] * k)) - charge(q) + tail[k] + for k in values) for j in values} + profiles.append([row[k] + tail[k] for k in values]) + event, q, signs = block[at] + table = [] + for a, b in product(values, repeat=2): + correction = charge(q * Q(2) ** (a * signs[0] + b * signs[1])) - charge(q * Q(2) ** (a * signs[0])) + correction += charge(q) - charge(q * Q(2) ** (b * signs[1])) + table.append([profiles[0][a + 4] + profiles[1][b + 4] + correction, a, b]) + joint = min(x[0] for x in table) + singles = [[k for k in values if profiles[axis][k + 4] == min(profiles[axis])] for axis in range(2)] + tied = min(c for c, a, b in table if a in singles[0] and b in singles[1]) + require(joint == -56 and tied == -53, "small coupling witness") + return {"first_incident_event": block[0][0], "last_incident_event": block[-1][0], "incident_adds": len(block), + "shared_event": event, "shared_coefficient": str(q), "signs": signs, "exponents": list(values), + "conditional_single_deltas_real": profiles, "single_optimal_exponents": singles, + "joint_minimizers": [x[1:] for x in table if x[0] == joint], + "joint_delta_real": joint, "best_tied_single_delta_real": tied} + + +def controls(word, programs, pair, schedules): + rejected = [] + + def reject(name, fn): + try: + fn() + except (ValueError, KeyError, IndexError): + rejected.append(name) + else: + raise ValueError("control accepted: " + name) + + for orientation in ("forward", "backward"): + original = programs[orientation] + candidate, _ = S["transform"](original, word, pair, schedules[orientation]) + inserted = next(i for i in range(len(candidate)) if candidate[i] != original[i]) + require(candidate[inserted][1][0] == "scale", "control insertion located") + bad = deepcopy(candidate) + del bad[inserted] + reject(orientation + ": omitted transition", lambda: check_transform(original, bad, word, pair)) + reject(orientation + ": omitted transition changes map", lambda: R["replay"](bad, orientation)) + bad = deepcopy(candidate) + bad[inserted][2] = -1 + reject(orientation + ": wrong scale frame", lambda: check_transform(original, bad, word, pair)) + bad_schedule = deepcopy(schedules[orientation]) + bad_schedule[0][1] = 5 + reject(orientation + ": exponent out of domain", lambda: S["transform"](original, word, pair, bad_schedule)) + reject(orientation + ": missing ADD schedule", lambda: S["transform"](original, word, pair, schedules[orientation][1:])) + blocks = S["segments"](original, pair) + zeros = [[i, 0, 0] for block in blocks for i, _, _ in block] + unchanged, count = S["transform"](original, word, pair, zeros) + require(unchanged == original and count == 0, "zero schedule positive control") + # Exhaust all 9^3 paths in a small interacting fixture, including tied single optima. + tiny = [[(0, Q(1, 2), (1, 0)), (1, Q(2), (-1, 1)), (2, Q(1), (0, -1))]] + states = list(product(range(-1, 2), repeat=2)) + records = [] + for path in product(states, repeat=3): + schedule = [[i, *k] for i, k in enumerate(path)] + joint = S["schedule_cost"](tiny, schedule) + separate = sum(S["schedule_cost"](tiny, [[i, k[0] if axis == 0 else 0, k[1] if axis == 1 else 0] + for i, k in enumerate(path)]) for axis in range(2)) + records.append((separate, joint)) + require(S["optimize"](tiny, ((-1, 1), (-1, 1)))["delta_real"] == min(x[1] for x in records), "exhaustive tiny joint optimum") + require(S["tied_single_minimum"](tiny, bound=1) == min(records)[1], "exhaustive tiny tied optimum") + manifest = json.loads((HERE / "SOURCES.json").read_bytes()) + bad = deepcopy(manifest) + bad["files"][R["LOWER"]] = "0" * 64 + reject("source corruption", lambda: R["load"](manifest=bad)) + bad = deepcopy(manifest) + del bad["archive_members"]["LOCAL-PROGRAMS.json.gz"] + reject("source inventory omission", lambda: R["load"](manifest=bad)) + return {"rejected": rejected, "tiny_paths": len(records), "zero_schedule_orientations": 2} + + +def compute(): + word, programs, source, lower = R["load"]() + helpers = S["eligible"](word, programs) + all_pairs = S["pairs"](programs, helpers) + require(len(helpers) == 237 and len(all_pairs) == 2414, "eligible interaction inventory") + pairs = all_pairs[23:39] + result = {"base": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f", "seed": 23, + "domain": [-4, 4], "pairs": pairs, "orientations": {}, "formal_columns": 712} + all_programs, schedules, witnesses = [], {}, [] + for orientation in ("forward", "backward"): + events = programs[orientation] + census = [] + for pair in pairs: + blocks = S["segments"](events, pair) + joint = S["optimize"](blocks) + tied = S["tied_single_minimum"](blocks) + a = S["optimize"](blocks, ((-4, 4), (0, 0))) + b = S["optimize"](blocks, ((0, 0), (-4, 4))) + oracle, oracle_tied, oracle_separate, edges = dense_oracle(blocks, lower) + require(joint["delta_real"] == oracle and tied == oracle_tied, "independent dense oracle") + require(a["delta_real"] + b["delta_real"] == oracle_separate, "independent separate optimum") + require(S["schedule_cost"](blocks, joint["schedule"]) == oracle, "attaining schedule") + census.append({"pair": pair, "delta_real": oracle, "best_tied_single_delta_real": tied, + "single_deltas_real": [a["delta_real"], b["delta_real"]], + "strict_gap_real": tied - oracle, "blocks": len(blocks), + "incident_adds": sum(map(len, blocks)), "dense_edges": edges}) + winner = min(census, key=lambda x: (-x["strict_gap_real"], x["pair"])) + pair = winner["pair"] + require(pair == (225, 350) and winner["strict_gap_real"] == 3, "largest strict coupling gap") + schedule = S["optimize"](S["segments"](events, pair))["schedule"] + candidate, inserted = S["transform"](events, word, pair, schedule) + invariant = check_transform(events, candidate, word, pair) + require(invariant["inserted_scales"] == inserted and invariant["delta_real"] == winner["delta_real"], "literal invariant invoice") + R["frame_check"](candidate, word, pair) + R["replay"](events, orientation) + R["replay"](candidate, orientation) + before, after = R["invoice"](events, lower), R["invoice"](candidate, lower) + require(after["complex_primitives"] - before["complex_primitives"] == 2 * winner["delta_real"], "full scalar invoice") + require(before["paid_profile"] == after["paid_profile"] == source["paid_profiles"][orientation], "paid profile unchanged") + require(before["prefix_l1"] == source["local"][orientation]["prefix_l1_upper"], "baseline prefix receipt") + result["orientations"][orientation] = {"census": census, "winner": winner, "schedule": schedule, + "coupling_block": coupling_block(S["segments"](events, pair), lower), + "invariant": invariant, "before": before, "after": after, "candidate_sha256": R["digest"](R["canonical"](candidate))} + schedules[orientation] = schedule + witnesses.append(pair) + all_programs.extend([events, candidate]) + require(witnesses[0] == witnesses[1], "one pair in both orientations") + result["lowerer_checks"] = R["lowerer_checks"](all_programs, lower) + result["controls"] = controls(word, programs, witnesses[0], schedules) + result["status"] = "PASS_K8_PAIRED_TEMPORAL_NO_NEW_KAPPA" + return result + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print the reproducible certificate without comparing a saved copy") + args = parser.parse_args() + result = compute() + if args.emit: + print(json.dumps(result, indent=2)) + else: + require(R["canonical"](result) == R["canonical"](json.loads((HERE / "CERTIFICATE.json").read_bytes())), "saved certificate mismatch") + print(result["status"] + " pair=225,350 saved=474/474 strict_coupling_gain=6/6 pairs=16 orientations=2 columns=712") From c2bc6848cffb2e2203095d4c4bbc45b0848c22e7 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar Date: Wed, 14 Oct 2026 05:19:48 +0530 Subject: [PATCH 2/2] docs: record paired temporal gauge handoff --- research/k8-paired-temporal-seed23/CLAIM.md | 33 +++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/research/k8-paired-temporal-seed23/CLAIM.md b/research/k8-paired-temporal-seed23/CLAIM.md index 79b97ce68b..529f71b90d 100644 --- a/research/k8-paired-temporal-seed23/CLAIM.md +++ b/research/k8-paired-temporal-seed23/CLAIM.md @@ -61,3 +61,36 @@ The selected conditional kappa remains `836330098538459/500000000000000000`. Inherited compiler, common-label/mutable-source, hosting, precision/tape, analytic and bit H1-H5 obligations remain. No selected/frontier or upstream/ files will change. + +## Completed result, 2026-10-13 23:49 UTC + +Submitted [PR1380](https://github.com/CrocSwap/integer-mult-bounds/pull/1380), +research commit `094204c9689a0185855b8c7ba35763d1a6598995`. +All 16 selected pairs and both orientations are complete, with no box expansion +or pivot. Five pairs have a strict coupling gap. L225/L350 has the largest: +-237 real primitives jointly versus -234 for the best composition of every +tied independent optimum. Complete scalar bills become 148,528/148,544, saving +474 per complex invocation in each orientation. The six-primitive coupling +advantage is isolated to one block and one shared ADD, with an exact 9-by-9 +conditional-cost witness. No new kappa or physical supplier invoice is claimed. + +Two optimization implementations agree on 49,693,014 transition candidates; +all 712 scalar columns, all changed frames and nonscalar boundaries, full +literal prices, unchanged paid profiles, local precision, 729 tiny paths and +twelve rejection controls pass. CPython3.14.8 and optimized3.11.15 pass, including +outside-checkout execution and an external saved-certificate corruption check. +Seven source/context Git blobs and selected-record integrity pass. The saved +certificate SHA256 is `3c59f72bcd0768bf0740edebcb09427bcd48659b8bcbba762a0e30ca53aa2afc`. + +The final overlap refresh covered 850 open PRs after the complete 94-record +discussion refresh at23:44. New PR1369 and PR1376 are credited with exact heads. +PR1376's disjoint objectives separate; this result proves a strict interaction +for a different pair and background. The source main remained at the same base +on the final fetch. No pinned issue existed, so this local claim receives its +single result update and is now released. Neither `codex` nor +`codex-automation` label exists in the target repository. + +Verification/handoff began before23:43, well before the23:57 cutoff. Native and +hosted admission, full cold replay, unbounded exponent optimization and formal +or human review remain unrun. Review the small coupling witness and the +scalar-cost versus complete-physical-cost boundary first.