From 79cb4818d633ec0bef6e4c13106b7f29ed084ea5 Mon Sep 17 00:00:00 2001 From: themilkman216 Date: Wed, 14 Oct 2026 14:16:43 -0400 Subject: [PATCH] Research: multi-pair schedules cannot beat the nine-stage template (Theorem S, no new kappa) Proves N >= 2K + ceil(2K/(s-1)) local-word invocations for every s-stage schedule of shear-type local words (any pairs per stage, mixed orientation, arbitrary block-diagonal bridges, any pair-level signed rho), so every schedule is dominated port for port by the B-template at the same s. Parallel chains attain it at odd s (exact replay); exhaustive searches show it is not attained at (K=3, s=4). Priced on PR1800's T74 words, the best attained schedule reproduces b exactly; even s=8 is worth at most +0.70%. Co-Authored-By: Claude Opus 5.5 --- .../CHAINS-REPLAY.jsonl | 8 + .../multipair-schedule-bound/FAMILIES.json | 447 ++++++++++++++++++ research/multipair-schedule-bound/README.md | 198 ++++++++ .../multipair-schedule-bound/SOURCES.json | 30 ++ research/multipair-schedule-bound/TASK.json | 69 +++ research/multipair-schedule-bound/VERIFY.json | 21 + .../multipair-schedule-bound/chains_replay.py | 207 ++++++++ .../multipair-schedule-bound/diag_equality.py | 57 +++ .../multipair-schedule-bound/grader/F00.json | 3 + .../multipair-schedule-bound/grader/F01.json | 11 + .../multipair-schedule-bound/grader/F02.json | 11 + .../multipair-schedule-bound/grader/F03.json | 11 + .../multipair-schedule-bound/grader/F04.json | 11 + .../multipair-schedule-bound/grader/F05.json | 11 + .../multipair-schedule-bound/grader/F06.json | 11 + .../multipair-schedule-bound/grader/F07.json | 11 + .../multipair-schedule-bound/grader/F08.json | 11 + .../multipair-schedule-bound/grader/F09.json | 11 + .../multipair-schedule-bound/grader/F10.json | 11 + .../multipair-schedule-bound/grader/F11.json | 3 + .../multipair-schedule-bound/grader/F12.json | 11 + .../multipair-schedule-bound/grader/F13.json | 3 + .../inputs/T74-WORDS.json | 68 +++ .../multipair-schedule-bound/lemma_check.py | 124 +++++ .../price_families.py | 245 ++++++++++ .../profiles/F00.json | 13 + .../profiles/F01.json | 14 + .../profiles/F02.json | 15 + .../profiles/F03.json | 15 + .../profiles/F04.json | 15 + .../profiles/F05.json | 14 + .../profiles/F06.json | 15 + .../profiles/F07.json | 15 + .../profiles/F08.json | 15 + .../profiles/F09.json | 15 + .../profiles/F10.json | 15 + .../profiles/F11.json | 13 + .../profiles/F12.json | 15 + .../profiles/F13.json | 14 + .../multipair-schedule-bound/sched_search.py | 148 ++++++ .../search/K2_alternating.json | 7 + .../search/K2_mixed.json | 7 + .../search/K3_s4_N8_equality.json | 5 + .../search/K3_s4_N8_equality_full.json | 5 + .../search/K3_s4_equality_diagnostic.txt | 4 + .../search/K3_s5_N8_rank2_wastefree.json | 6 + research/multipair-schedule-bound/verify.py | 129 +++++ 47 files changed, 2118 insertions(+) create mode 100644 research/multipair-schedule-bound/CHAINS-REPLAY.jsonl create mode 100644 research/multipair-schedule-bound/FAMILIES.json create mode 100644 research/multipair-schedule-bound/README.md create mode 100644 research/multipair-schedule-bound/SOURCES.json create mode 100644 research/multipair-schedule-bound/TASK.json create mode 100644 research/multipair-schedule-bound/VERIFY.json create mode 100644 research/multipair-schedule-bound/chains_replay.py create mode 100644 research/multipair-schedule-bound/diag_equality.py create mode 100644 research/multipair-schedule-bound/grader/F00.json create mode 100644 research/multipair-schedule-bound/grader/F01.json create mode 100644 research/multipair-schedule-bound/grader/F02.json create mode 100644 research/multipair-schedule-bound/grader/F03.json create mode 100644 research/multipair-schedule-bound/grader/F04.json create mode 100644 research/multipair-schedule-bound/grader/F05.json create mode 100644 research/multipair-schedule-bound/grader/F06.json create mode 100644 research/multipair-schedule-bound/grader/F07.json create mode 100644 research/multipair-schedule-bound/grader/F08.json create mode 100644 research/multipair-schedule-bound/grader/F09.json create mode 100644 research/multipair-schedule-bound/grader/F10.json create mode 100644 research/multipair-schedule-bound/grader/F11.json create mode 100644 research/multipair-schedule-bound/grader/F12.json create mode 100644 research/multipair-schedule-bound/grader/F13.json create mode 100644 research/multipair-schedule-bound/inputs/T74-WORDS.json create mode 100644 research/multipair-schedule-bound/lemma_check.py create mode 100644 research/multipair-schedule-bound/price_families.py create mode 100644 research/multipair-schedule-bound/profiles/F00.json create mode 100644 research/multipair-schedule-bound/profiles/F01.json create mode 100644 research/multipair-schedule-bound/profiles/F02.json create mode 100644 research/multipair-schedule-bound/profiles/F03.json create mode 100644 research/multipair-schedule-bound/profiles/F04.json create mode 100644 research/multipair-schedule-bound/profiles/F05.json create mode 100644 research/multipair-schedule-bound/profiles/F06.json create mode 100644 research/multipair-schedule-bound/profiles/F07.json create mode 100644 research/multipair-schedule-bound/profiles/F08.json create mode 100644 research/multipair-schedule-bound/profiles/F09.json create mode 100644 research/multipair-schedule-bound/profiles/F10.json create mode 100644 research/multipair-schedule-bound/profiles/F11.json create mode 100644 research/multipair-schedule-bound/profiles/F12.json create mode 100644 research/multipair-schedule-bound/profiles/F13.json create mode 100644 research/multipair-schedule-bound/sched_search.py create mode 100644 research/multipair-schedule-bound/search/K2_alternating.json create mode 100644 research/multipair-schedule-bound/search/K2_mixed.json create mode 100644 research/multipair-schedule-bound/search/K3_s4_N8_equality.json create mode 100644 research/multipair-schedule-bound/search/K3_s4_N8_equality_full.json create mode 100644 research/multipair-schedule-bound/search/K3_s4_equality_diagnostic.txt create mode 100644 research/multipair-schedule-bound/search/K3_s5_N8_rank2_wastefree.json create mode 100644 research/multipair-schedule-bound/verify.py diff --git a/research/multipair-schedule-bound/CHAINS-REPLAY.jsonl b/research/multipair-schedule-bound/CHAINS-REPLAY.jsonl new file mode 100644 index 0000000000..20e11d53c6 --- /dev/null +++ b/research/multipair-schedule-bound/CHAINS-REPLAY.jsonl @@ -0,0 +1,8 @@ +{"chains": [[4, "forward"]], "K": 4, "s": 9, "N": 9, "m": 73, "W_per_replica_ports": 896, "D_per_replica": 320, "theorem_S_bound": 9, "attains_bound": true, "mixed_orientation_stages": 0, "pair_calls_per_stage": [1, 1, 1, 1, 1, 1, 1, 1, 1], "idle_windows_per_port": {"8": 6, "16": 4, "32": 4, "48": 4}, "largest_idle_child": 48, "R_max_halving_guard": 51, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +{"chains": [[2, "forward"], [2, "backward"]], "K": 4, "s": 5, "N": 10, "m": 41, "W_per_replica_ports": 896, "D_per_replica": 256, "theorem_S_bound": 10, "attains_bound": true, "mixed_orientation_stages": 5, "pair_calls_per_stage": [2, 2, 2, 2, 2], "idle_windows_per_port": {"8": 4, "16": 8}, "largest_idle_child": 16, "R_max_halving_guard": 28, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +{"chains": [[2, "forward"], [2, "forward"]], "K": 4, "s": 5, "N": 10, "m": 41, "W_per_replica_ports": 896, "D_per_replica": 256, "theorem_S_bound": 10, "attains_bound": true, "mixed_orientation_stages": 0, "pair_calls_per_stage": [2, 2, 2, 2, 2], "idle_windows_per_port": {"8": 4, "16": 8}, "largest_idle_child": 16, "R_max_halving_guard": 28, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +{"chains": [[4, "forward"], [4, "backward"]], "K": 8, "s": 9, "N": 18, "m": 73, "W_per_replica_ports": 1792, "D_per_replica": 640, "theorem_S_bound": 18, "attains_bound": true, "mixed_orientation_stages": 9, "pair_calls_per_stage": [2, 2, 2, 2, 2, 2, 2, 2, 2], "idle_windows_per_port": {"8": 12, "16": 8, "32": 8, "48": 8}, "largest_idle_child": 48, "R_max_halving_guard": 51, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +{"chains": [[4, "forward"], [3, "forward"]], "K": 7, "s": 9, "N": 16, "m": 73, "W_per_replica_ports": 1568, "D_per_replica": 544, "theorem_S_bound": 16, "attains_bound": true, "mixed_orientation_stages": 0, "pair_calls_per_stage": [2, 2, 2, 2, 2, 2, 2, 1, 1], "idle_windows_per_port": {"8": 10, "16": 8, "32": 8, "48": 6}, "largest_idle_child": 48, "R_max_halving_guard": 51, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +{"chains": [[3, "forward"], [3, "backward"], [1, "forward"]], "K": 7, "s": 7, "N": 17, "m": 57, "W_per_replica_ports": 1568, "D_per_replica": 480, "theorem_S_bound": 17, "attains_bound": true, "mixed_orientation_stages": 7, "pair_calls_per_stage": [3, 3, 3, 2, 2, 2, 2], "idle_windows_per_port": {"8": 8, "16": 8, "32": 10}, "largest_idle_child": 32, "R_max_halving_guard": 40, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +{"chains": [[1, "forward"], [1, "backward"], [1, "forward"]], "K": 3, "s": 3, "N": 9, "m": 25, "W_per_replica_ports": 672, "D_per_replica": 96, "theorem_S_bound": 9, "attains_bound": true, "mixed_orientation_stages": 3, "pair_calls_per_stage": [3, 3, 3], "idle_windows_per_port": {}, "largest_idle_child": 0, "R_max_halving_guard": 17, "largest_child_needs_split": false, "endpoint": "signed exchange, exact"} +PASS_F1_CHAINS_REPLAY cases=7 diff --git a/research/multipair-schedule-bound/FAMILIES.json b/research/multipair-schedule-bound/FAMILIES.json new file mode 100644 index 0000000000..839963fb7e --- /dev/null +++ b/research/multipair-schedule-bound/FAMILIES.json @@ -0,0 +1,447 @@ +{ + "T74_b_bracket": [ + "0.001679754956125544521335", + "0.001679754956125544521336" + ], + "helpers_per_call": { + "extra": 3738, + "gauge44": 3734 + }, + "call_split": { + "extra": 417, + "gauge44": 249 + }, + "families": [ + { + "id": "F00", + "label": "B_3 chain (s=7); t parallel B_3 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "K": 3, + "s": 7, + "N": 7, + "cst_inv": 64, + "largest_window": 32, + "status": "attained (chains_replay.py); Theorem S frontier at odd s", + "m": 57, + "W_rep": 672, + "R_cap": 32, + "R_max": 40, + "coverage_rep": "38080", + "local_rep": "1448458/37", + "idle_rep": "-39498/37", + "hosting_wall": true, + "D_rep": "-31210/37", + "b_lower": null, + "gain_percent": null, + "beats_T74": null, + "grader_error": "non-positive deficit (hosting wall) or rank outside (0, m)", + "ceiling": { + "error": "local word pays more mass than the coverage law allows" + }, + "idle_windows_per_port": { + "8": 4, + "16": 4, + "32": 4 + } + }, + { + "id": "F01", + "label": "B_4 chain (s=9); t parallel B_4 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "K": 4, + "s": 9, + "N": 9, + "cst_inv": 64, + "largest_window": 48, + "status": "attained (chains_replay.py); Theorem S frontier at odd s", + "m": 73, + "W_rep": 896, + "R_cap": 48, + "R_max": 51, + "coverage_rep": "65088", + "local_rep": "1862304/37", + "idle_rep": "545952/37", + "hosting_wall": false, + "D_rep": "320", + "b_lower": "0.001679754956125544521335", + "gain_percent": 0.0, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001687660538475, + "a_hi_exact": "67506421539/40000000000000" + }, + "idle_windows_per_port": { + "8": 6, + "16": 4, + "32": 4, + "48": 4 + } + }, + { + "id": "F02", + "label": "B_5 chain (s=11); t parallel B_5 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "K": 5, + "s": 11, + "N": 11, + "cst_inv": 64, + "largest_window": 64, + "status": "attained (chains_replay.py); Theorem S frontier at odd s", + "m": 89, + "W_rep": 1120, + "R_cap": 62, + "R_max": 62, + "coverage_rep": "99264", + "local_rep": "2276150/37", + "idle_rep": "1396618/37", + "hosting_wall": false, + "D_rep": "416", + "b_lower": "0.001656172228607112292838", + "gain_percent": -1.4039385585637565, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001656174410624, + "a_hi_exact": "12938862583/7812500000000" + }, + "idle_windows_per_port": { + "8": 8, + "16": 4, + "32": 4, + "48": 4, + "64": 4 + } + }, + { + "id": "F03", + "label": "B_6 chain (s=13); t parallel B_6 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "K": 6, + "s": 13, + "N": 13, + "cst_inv": 64, + "largest_window": 80, + "status": "attained (chains_replay.py); Theorem S frontier at odd s", + "m": 105, + "W_rep": 1344, + "R_cap": 74, + "R_max": 74, + "coverage_rep": "140608", + "local_rep": "2689994/37", + "idle_rep": "2512502/37", + "hosting_wall": false, + "D_rep": "512", + "b_lower": "0.001617382665125020322085", + "gain_percent": -3.7131779711720347, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001617384139259, + "a_hi_exact": "1617384139259/1000000000000000" + }, + "idle_windows_per_port": { + "8": 10, + "16": 4, + "32": 4, + "48": 4, + "64": 4, + "80": 4 + } + }, + { + "id": "F04", + "label": "B_7 chain (s=15); t parallel B_7 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "K": 7, + "s": 15, + "N": 15, + "cst_inv": 64, + "largest_window": 96, + "status": "attained (chains_replay.py); Theorem S frontier at odd s", + "m": 121, + "W_rep": 1568, + "R_cap": 85, + "R_max": 85, + "coverage_rep": "189120", + "local_rep": "3103840/37", + "idle_rep": "3893600/37", + "hosting_wall": false, + "D_rep": "608", + "b_lower": "0.001571246396968943417717", + "gain_percent": -6.459785027625851, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001571247570333, + "a_hi_exact": "1571247570333/1000000000000000" + }, + "idle_windows_per_port": { + "8": 12, + "16": 4, + "32": 4, + "48": 4, + "64": 4, + "80": 4, + "96": 4 + } + }, + { + "id": "F05", + "label": "B_4 || B_4 mixed orientation, s=9, K=8 (every stage = one forward + one backward local word, rank 2v)", + "K": 8, + "s": 9, + "N": 18, + "cst_inv": 64, + "largest_window": 48, + "status": "attained (chains_replay.py); equals two T74 replicas", + "m": 73, + "W_rep": 1792, + "R_cap": 48, + "R_max": 51, + "coverage_rep": "130176", + "local_rep": "3724608/37", + "idle_rep": "1091904/37", + "hosting_wall": false, + "D_rep": "640", + "b_lower": "0.001679754956125544521335", + "gain_percent": 0.0, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001687660538475, + "a_hi_exact": "67506421539/40000000000000" + }, + "idle_windows_per_port": { + "8": 14, + "16": 4, + "32": 4, + "48": 4, + "64": 4, + "80": 4, + "96": 4, + "112": 4 + } + }, + { + "id": "F06", + "label": "B_4 || B_3 unequal chains, s=9, K=7, N=16", + "K": 7, + "s": 9, + "N": 16, + "cst_inv": 64, + "largest_window": 48, + "status": "attained (chains_replay.py); Theorem S tight (ceil)", + "m": 73, + "W_rep": 1568, + "R_cap": 48, + "R_max": 51, + "coverage_rep": "113920", + "local_rep": "3310762/37", + "idle_rep": "904278/37", + "hosting_wall": false, + "D_rep": "544", + "b_lower": "0.001610042388228235763691", + "gain_percent": -4.150162953417025, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001617118093159, + "a_hi_exact": "1617118093159/1000000000000000" + }, + "idle_windows_per_port": { + "8": 12, + "16": 4, + "32": 4, + "48": 4, + "64": 4, + "80": 4, + "96": 4 + } + }, + { + "id": "F07", + "label": "s=8 by chains: B_3 plus one idle stage (best chain ratio N/K = 7/3), K=3, N=7", + "K": 3, + "s": 8, + "N": 7, + "cst_inv": 64, + "largest_window": 40, + "status": "attained (s=7 schedule padded by one stage)", + "m": 65, + "W_rep": 672, + "R_cap": 40, + "R_max": 45, + "coverage_rep": "43456", + "local_rep": "1448458/37", + "idle_rep": "159414/37", + "hosting_wall": false, + "D_rep": "224", + "b_lower": "0.00159028683109454299811", + "gain_percent": -5.326260518222558, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001596025238713, + "a_hi_exact": "1596025238713/1000000000000000" + } + }, + { + "id": "F08", + "label": "even s=8 at the Theorem S bound (K=7, N=16), idle children <= 40 (window multiple of a=8 under the guard); attainment open", + "K": 7, + "s": 8, + "N": 16, + "cst_inv": 64, + "largest_window": 40, + "status": "HYPOTHETICAL: only the lower bound is proved; chains need N=17; F2 search refutes the bound at (K=3, s=4)", + "m": 65, + "W_rep": 1568, + "R_cap": 40, + "R_max": 45, + "coverage_rep": "101376", + "local_rep": "3310762/37", + "idle_rep": "440150/37", + "hosting_wall": false, + "D_rep": "544", + "b_lower": "0.00168419220807572539741", + "gain_percent": 0.2641606702215461, + "beats_T74": true, + "grader_error": null, + "ceiling": { + "a_hi": 0.001691513511328, + "a_hi_exact": "52859797229/31250000000000" + } + }, + { + "id": "F09", + "label": "even s=8 at the Theorem S bound (K=7, N=16), idle children at R_max = 45 (ceiling-favorable); attainment open", + "K": 7, + "s": 8, + "N": 16, + "cst_inv": 64, + "largest_window": null, + "status": "HYPOTHETICAL: only the lower bound is proved; chains need N=17; F2 search refutes the bound at (K=3, s=4)", + "m": 65, + "W_rep": 1568, + "R_cap": 45, + "R_max": 45, + "coverage_rep": "101376", + "local_rep": "3310762/37", + "idle_rep": "440150/37", + "hosting_wall": false, + "D_rep": "544", + "b_lower": "0.001691512754596525670768", + "gain_percent": 0.6999710539983294, + "beats_T74": true, + "grader_error": null, + "ceiling": { + "a_hi": 0.001691513511328, + "a_hi_exact": "52859797229/31250000000000" + } + }, + { + "id": "F10", + "label": "even s=10 at the Theorem S bound (K=9, N=20), idle children at R_max = 57; attainment open", + "K": 9, + "s": 10, + "N": 20, + "cst_inv": 64, + "largest_window": null, + "status": "HYPOTHETICAL: only the lower bound is proved; chains need N=21; F2 search refutes the bound at (K=3, s=4)", + "m": 81, + "W_rep": 2016, + "R_cap": 57, + "R_max": 57, + "coverage_rep": "162560", + "local_rep": "4138454/37", + "idle_rep": "1876266/37", + "hosting_wall": false, + "D_rep": "736", + "b_lower": "0.001676096670260698677048", + "gain_percent": -0.2177868772766654, + "beats_T74": false, + "grader_error": null, + "ceiling": { + "a_hi": 0.001676097204183, + "a_hi_exact": "1676097204183/1000000000000000" + } + }, + { + "id": "F11", + "label": "even s=6 at the Theorem S bound (K=5, N=12), idle children at R_max = 34; attainment open", + "K": 5, + "s": 6, + "N": 12, + "cst_inv": 64, + "largest_window": null, + "status": "HYPOTHETICAL: only the lower bound is proved; chains need N=13; F2 search refutes the bound at (K=3, s=4)", + "m": 49, + "W_rep": 1120, + "R_cap": 34, + "R_max": 34, + "coverage_rep": "54528", + "local_rep": "2483072/37", + "idle_rep": "-465536/37", + "hosting_wall": true, + "D_rep": "-452512/37", + "b_lower": null, + "gain_percent": null, + "beats_T74": null, + "grader_error": "non-positive deficit (hosting wall) or rank outside (0, m)", + "ceiling": { + "error": "local word pays more mass than the coverage law allows" + } + }, + { + "id": "F12", + "label": "excluded: waste-free parallel s=9, K=8, N=17", + "K": 8, + "s": 9, + "N": 17, + "cst_inv": 64, + "largest_window": null, + "status": "EXCLUDED by Theorem S (N >= 18)", + "m": 73, + "W_rep": 1792, + "R_cap": 51, + "R_max": 51, + "coverage_rep": "130112", + "local_rep": "3517686/37", + "idle_rep": "1296458/37", + "hosting_wall": false, + "D_rep": "704", + "b_lower": "0.001950681375323732307036", + "gain_percent": 16.128925127454053, + "beats_T74": true, + "grader_error": null, + "ceiling": { + "a_hi": 0.001950683006291, + "a_hi_exact": "1950683006291/1000000000000000" + } + }, + { + "id": "F13", + "label": "excluded: s=9, K=8, two pairs per invocation, ONE centre path per invocation", + "K": 8, + "s": 9, + "N": 18, + "cst_inv": 64, + "pairs_per_inv": 2, + "largest_window": 48, + "status": "EXCLUDED: the two pairs carry independent totals (README Q1); the grader window stops at b = 0.003, so only the ceiling is reported", + "m": 73, + "W_rep": 1792, + "R_cap": 48, + "R_max": 51, + "coverage_rep": "129600", + "local_rep": "3703296/37", + "idle_rep": "1091904/37", + "hosting_wall": false, + "D_rep": "1216", + "b_lower": null, + "gain_percent": null, + "beats_T74": null, + "grader_error": "outside the engine search window [0, 0.003]", + "ceiling": { + "a_hi": 0.003208423385024, + "a_hi_exact": "50131615391/15625000000000" + } + } + ] +} diff --git a/research/multipair-schedule-bound/README.md b/research/multipair-schedule-bound/README.md new file mode 100644 index 0000000000..a01bb3bda9 --- /dev/null +++ b/research/multipair-schedule-bound/README.md @@ -0,0 +1,198 @@ +# Multi-pair schedules cannot beat the nine-stage template (Theorem S; no new κ) + +**Research note: a proved scheduling bound and a priced negative result. No κ claim; the selected record is unchanged.** + +The B_K schedule has two conventions that no PR has varied: + +- rule-table row 13 of [format-limits-corrected](../format-limits-corrected/README.md): one `(X, Y)` bank pair per local-word invocation; +- row 5: the pairwise signed exchange ρ. + +The format-limits ceiling theorem explicitly does not cover non-B_K schedules. This package closes that gap for the complex supplier's economics: + +- **Theorem S (proved).** Take any schedule of shear-type local words with `s` stages over `K` bank pairs. It needs at least `N ≥ 2K + ⌈2K/(s − 1)⌉` local-word invocations ("pair-calls"). + - Any number of pairs may run in a stage, with either orientation. + - Bridges may be arbitrary block-diagonal maps. + - ρ may be any pair-level signed exchange. + - Calls need not be pair-aligned. + - It generalises [cross-shear-stage-bound](../cross-shear-stage-bound/README.md), which is the case of one rank-`v` call per stage. +- **Consequence.** Per port, `D/W ≤ 1 − (cst/v)·s/(s − 1)`. Every schedule with `s` stages is dominated port for port by the B-template at the same `s`. +- **Attainment at odd `s`.** Parallel borrowing chains attain the bound, checked by exact replay. Their per-port profile is the B_K profile. +- **Priced on the T74 local words** of PR #1800, the current top open claim: + - the best attained schedule reproduces its complex exponent `b = 0.001679754956125544521335` exactly and does not beat it; + - `s = 7` hits the hosting wall; + - `s = 11`, `13` and `15` lose 1.40%, 3.71% and 6.46% of `b`. +- **The only unexplored room is even `s = 8`.** Even if Theorem S were attained there, it is worth at most +0.26% (window-aligned idle children) or +0.70% (packing-ceiling relaxation). See the [s = 8 open question](#open-next-questions). + +This answers the "is the one-pair-per-invocation convention costing anything?" side of the [coverage-law-change](../../docs/research/agent-task-catalog.json) card. The card's main question, two unpaid coordinates per family, is not addressed; the [TASK.json](TASK.json) scope change says so. + +## 1. What the spec requires, and two pairs in one call + +- **The contract.** `upstream/build/sections/04-swap.tex:105-123` gives: + - `W` wires and pointwise gates inducing a permutation ρ; + - one frame per gate, common to its wires; + - cost `Σ_e rank(M_head − M_tail)` with `M_out(ρ(w)) − M_in(w) = I_m`. + + The recursion (`:197-211`) charges one recursive call per unit of edge rank. "Invocation", "bank pair", "stage" and "local word" are construction-layer notions. The paper's instance is the three-stage exchange per pair (`03-motifs.tex:89-100`, ρ at `:628`). +- **Two pairs in one stage are legal.** Two local words on disjoint pairs touch disjoint wires, and every gate keeps its common frame. + - Concurrent calls share the stage's 8-dimensional window, as the replicas already do. So `m = 1 + 8s`. This is the reading most favourable to the lever. + - A stage may also mix orientations. After bridges it is `[[I, H], [E, I]]` with `HE = EH = 0`. +- **Each pair keeps its own centre path and helper network.** + - A local word's eight rank-8 centre copies (`cst = 64`) carry the eight decoder totals of its own 112 sources. + - Two pairs active together hold independent coordinates. Their 16 totals are independent functionals, and each copy pays at least its pairing rank (star floor, format-limits row 8). + - Fusing two pairs on the same labels gives a degenerate-label unit. format-limits Lemma Q (C.4) dominates it by its quotient. + - So every pair-call pays the full per-call profile. +- **Difference from centre-sharing PRs** (#1708, #1748, #1791, #1829, #1838). Those reuse one call's centre values in a *later* call on related data. Pairs in the *same* stage share no data, so a multi-pair invocation opens no new sharing route. + +## 2. Theorem S + +**Model.** This is the pair-level model of cross-shear-stage-bound, tensored with `I_v`. +- The state is `M_t ∈ GL_2K(F)` over any field. +- Bridges are arbitrary invertible block-diagonal maps. +- Stage `t` is `[[I, H_t],[E_t, I]]`, with cost `c_t = rank E_t + rank H_t` pair-calls. +- The goal is `M_s` block antidiagonal. Any pair-level signed ρ has this goal. + +**Theorem S.** `N := Σ_t c_t ≥ 2K + ⌈2K/(s − 1)⌉` for every `s ≥ 2`. + +*Proof.* + +**Setup.** +- Let `P_t, Q_t` be the row spaces of the top and bottom block rows of `M_t`. Bridges preserve them. +- Let `X = F^K ⊕ 0` and `Y = 0 ⊕ F^K`. The start is `(P, Q) = (X, Y)`; the goal is `(Y, X)`. +- A stage maps `P_{t−1}` to `P_t = {p + ψ_t p}`, where `ψ_t: P_{t−1} → Q_{t−1}` has `rank ψ_t = rank H_t =: h_t`. +- It maps `Q_{t−1}` to `Q_t = {q + φ_t q}`, where `rank φ_t = e_t`. +- Put `a = dim P∩Y`, `β = dim P∩X`, `σ^P = K − a − β ≥ 0`. +- Put `d = dim Q∩X`, `γ = dim Q∩Y`, `σ^Q = K − d − γ ≥ 0`. + +**(i)** `P_t ∩ Q_{t−1} = 0`: if `p + ψp ∈ Q_{t−1}` then `p ∈ P_{t−1} ∩ Q_{t−1} = 0`. So `P_t∩Y` and `Q_{t−1}∩Y` are independent in `Y`, giving + + `a_t ≤ K − γ_{t−1} = d_{t−1} + σ^Q_{t−1}`. + +Symmetrically, `d_t ≤ a_{t−1} + σ^P_{t−1}`. + +**(ii)** `ker ψ_t ⊆ P_t ∩ P_{t−1}`, so `dim(P_t∩P_{t−1}) ≥ K − h_t`. This gives `a_t ≤ a_{t−1} + h_t` and `β_t ≥ β_{t−1} − h_t`. Hence + + `σ^P_t ≤ σ^P_{t−1} + w^P_t`, + +with waste `w^P_t := h_t − (a_t − a_{t−1}) ≥ 0`. The same holds for `Q`. + +**(iii)** Telescoping `a` and `d` from `0` to `K` gives `N = 2K + W`, where `W = Σ_t (w^P_t + w^Q_t)`. + +**(iv)** By (i), `a_t + d_t ≤ a_{t−1} + d_{t−1} + σ_{t−1}`, where `σ = σ^P + σ^Q`. We have `σ_0 = 0` and `σ_u ≤ W`. Summing over `t = 1..s` gives `2K ≤ (s − 1)W`. ∎ + +The proof does not use `HE = EH = 0`. Replacing `K` by `Kv` gives the port-level statement. With one rank-`v` call per stage (`N = s`), it recovers `s ≥ 2K + 1`. + +**Corollary.** Per replica, `W = 2Kv` ports, `m = 1 + 8s` and `D = W − cst·N`. So per port: +- `D/W ≤ 1 − (cst/v)·s/(s − 1)`; +- the active climb mass is at least `16s/(s−1)`; +- the helper demand is at least `(s/(s−1))` times the per-call helper width per port; +- idle capacity is correspondingly at most its B_K value. + +These are the B_K values at `s = 2K + 1`, so (Dfc) becomes an inequality for every schedule. Each extra call at fixed `m` lowers `D` and replaces idle children by local children. So the packing ceiling decreases in `N/W`, and pricing at the bound dominates every schedule with `s` stages. + +## 3. Attainment and searches + +- **`chains_replay.py` (exact rationals).** It runs `t` borrowing chains `B_k` side by side, in either orientation, with `s = 2k + 1` and `K = tk`. + - This gives `N = 2K + 2K/(s−1)`, exactly the bound. + - Seven schedules replay to the exact signed exchange, on random data and on every unit vector. They include `B_4 ‖ B_4` with every stage mixed (rank 2v), unequal `B_4 ‖ B_3`, and three parallel full-rank 3-shears. + - `B_4` alone reproduces format-limits (Sch): idle windows `{8: 6, 16: 4, 32: 4, 48: 4}` per port. +- **`sched_search.py` (exhaustive over GF(2), states up to bridges).** + - The pruning uses `Φ = 2K − a − d`, which falls by at most a stage's cost (proof step (ii)), so it is admissible. + - For `K = 2`, with mixed or alternating stages, the minimum `N` over schedules with at most `s` stages is `6, 6, 5, 5` for `s = 3..6`. That is exactly the bound. +- **`K = 3, s = 4` (the smallest even case).** Equality `N = 8` would need `σ_1 = σ_2 = σ_3 = 2`. That forces stage 1 to cost exactly 2 and every later stage to be waste-free. + - Restricted to at most one word of each orientation per stage (`--maxrank 1`), no such schedule exists (`search/K3_s4_N8_equality.json`). `diag_equality.py` locates where the pattern dies (`search/K3_s4_equality_diagnostic.txt`). + - Without that restriction, the exhaustive equality search over all 2,051 stage shapes (`search/K3_s4_N8_equality_full.json`) also finds **no schedule**. So the bound is not attained at (K = 3, s = 4), and chains (`N = 9`) are optimal there. + - The same tool finds the chain value `N = 8` at `s = 5` (`search/K3_s5_N8_rank2_wastefree.json`). +- **`lemma_check.py`.** It independently checks inequalities (i), (ii) and the waste bound on 10,697 random stages over GF(2), GF(3) and GF(5), with K up to 4. Two false strengthenings must fail and do: (ii) with `h − 1`, and (i) without its σ term. + +## 4. Prices on the T74 words + +`inputs/T74-WORDS.json` holds an extract of PR #1800's provider registry (`research/capped-fusion-t74-k554/new/PLAN.json` at `46d865ab`; blob and SHA256 pinned inside): +- the two local words' per-call paid profiles; +- their helper-width histograms; +- the 417/249 call split. + +The verifier recomposes the published global profile from it exactly and reproduces the T74 complex endpoint with the retained moment engine. Each family is then priced with the same engine and with [ceiling.py](../complex-local-word-ceiling/ceiling.py). + +| id | schedule | s | K | N | m | D/replica | b (exact lower) | vs T74 | +|---|---|---|---|---|---|---|---|---| +| F00 | B_3 (any parallel B_3 chains) | 7 | 3 | 7 | 57 | hosting wall (helpers 26 156 > idle 25 088) | none | wall | +| F01 | B_4 = T74 (any parallel B_4 chains) | 9 | 4 | 9 | 73 | 320 | 0.001679754956125544521335 | 0 | +| F05 | B_4 ‖ B_4, every stage mixed (rank 2v) | 9 | 8 | 18 | 73 | 640 | 0.001679754956125544521335 | 0 | +| F06 | B_4 ‖ B_3 | 9 | 7 | 16 | 73 | 544 | 0.001610042388228235763691 | −4.15% | +| F02 | B_5 | 11 | 5 | 11 | 89 | 416 | 0.001656172228607112292838 | −1.40% | +| F03 | B_6 | 13 | 6 | 13 | 105 | 512 | 0.001617382665125020322085 | −3.71% | +| F04 | B_7 | 15 | 7 | 15 | 121 | 608 | 0.001571246396968943417717 | −6.46% | +| F07 | s = 8 by chains | 8 | 3 | 7 | 65 | 224 | 0.00159028683109454299811 | −5.33% | +| F08 | s = 8 **at the bound** (hypothetical), idle ≤ 40 | 8 | 7 | 16 | 65 | 544 | 0.00168419220807572539741 | +0.26% | +| F09 | same, idle at the guard R = 45 | 8 | 7 | 16 | 65 | 544 | 0.001691512754596525670768 | +0.70% | +| F10 | s = 10 at the bound (hypothetical) | 10 | 9 | 20 | 81 | 736 | 0.001676096670260698677048 | −0.22% | +| F11 | s = 6 at the bound (hypothetical) | 6 | 5 | 12 | 49 | hosting wall | none | wall | +| F12 | excluded: N one below the bound | 9 | 8 | 17 | 73 | 704 | 0.001950681375323732307036 | +16.1% (impossible) | +| F13 | excluded: two pairs, one centre path | 9 | 8 | 18 | 73 | 1216 | outside engine window | impossible (§1) | + +Full identities, idle windows and packing ceilings are in `FAMILIES.json`, `profiles/` and `grader/`. + +**What decides these numbers:** +- **The per-pair-call charge.** Each pair-call pays a centre path, about 3,736 of hosted helper width, and 1,792 active climbs. +- **Chain-seed waste.** Theorem S charges at least `2K/(s−1)` extra calls. +- **The hosting wall at `s ≤ 7`.** +- **Window growth at `s ≥ 10`.** + +F12 shows what the bound rules out: a waste-free parallel schedule would be worth +16%. + +## 5. Scope and limits + +**Covered:** every schedule of shear-type local words on the T74 per-call profile under the coverage law `(m − 1)W + cst·N`. That includes: +- any number of pairs per stage; +- mixed orientations; +- unequal chains; +- calls that are not pair-aligned; +- arbitrary block-diagonal bridges; +- any signed pair-level ρ. + +**Not covered:** +- even-`s` attainment beyond (K = 3, s = 4), where it fails; +- ρ through a third bank class, which changes the coverage law (the "two unpaid coordinates" lever); +- a local word that is not a shear; +- a frame-checker replay of mixed-orientation stages (their legality is argued in §1). + +**Assumptions:** +- the stage window is shared by concurrent calls; +- idle mass is packed at the stated rank cap; +- in the hypothetical families, Theorem S is attained. + +The T74 profiles are PR #1800's. Its construction is not re-verified here. + +## Reproduce + +From the repository root (standard library only): + +```sh +python3 -B research/multipair-schedule-bound/verify.py # PASS_MULTIPAIR_SCHEDULE_BOUND, about 30 s +python3 scripts/research_package.py --package research/multipair-schedule-bound +``` + +Longer searches whose committed outputs are not rerun by `verify.py`: + +```sh +python3 -B research/multipair-schedule-bound/sched_search.py 3 8 4 --maxrank 1 --wastefree-after-1 # ~6 min +python3 -B research/multipair-schedule-bound/sched_search.py 3 8 4 --wastefree-after-1 # unrestricted, ~1 h +python3 -B research/multipair-schedule-bound/sched_search.py 3 8 5 --maxrank 2 --wastefree-after-1 # ~23 min +python3 -B research/multipair-schedule-bound/diag_equality.py 3 4 +``` + +## Open next questions + +- **Is Theorem S attained at even `s`?** Only `s = 8` could pay, by at most +0.26% to +0.70%, and only with exact attainment: one extra pair-call per 35 pairs costs about 3.4%. + - The first open instance is `K = 4, s = 4` (bound 11, chains 12). It needs orbit reduction under GL(X)×GL(Y) or a compiled search. + - A proof that even `s` is never better than `s − 1` would close the lever. +- **ρ through three bank classes.** Can a cycle `X → Y → Z` leave more than one unpaid coordinate per family? This is the levers.py "two unpaid coordinates" budget (×3.77), not a scheduling question. + +## Credit + +- Theorem S generalises the stage-count proof in [cross-shear-stage-bound](../cross-shear-stage-bound/README.md) and the archived borrowing-chain campaign it audits. +- The rule table, (Sch)/(Dfc) and Lemma Q are from [format-limits-corrected](../format-limits-corrected/README.md). +- The packing ceiling is [complex-local-word-ceiling](../complex-local-word-ceiling/README.md). +- The T74 words and profile are from PR #1800 (jeremykothe2) and its lineage, credited in that PR: PR1625 (mdumitrean), PR1661 (midhatn), PR1319/PR1297 (rohanarun), and others. + +Prepared by themilkman216 with substantial Claude (Anthropic) assistance. The investigation was run as parallel fresh-context research branches. Apache-2.0. diff --git a/research/multipair-schedule-bound/SOURCES.json b/research/multipair-schedule-bound/SOURCES.json new file mode 100644 index 0000000000..9bb1c37b43 --- /dev/null +++ b/research/multipair-schedule-bound/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", + "usage": "input", + "git_blob": "7d697cb45203fe72d97037403d6da41f71f3b7fd", + "sha256": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482" + }, + { + "path": "research/complex-local-word-ceiling/ceiling.py", + "usage": "input", + "git_blob": "6c0f54527d879396f689523bfde19928a9b6157c", + "sha256": "86a1432870b3b21d8454106ec9162fddc0471472d9214c590a1420f2426cedfc" + } + ] +} diff --git a/research/multipair-schedule-bound/TASK.json b/research/multipair-schedule-bound/TASK.json new file mode 100644 index 0000000000..90f3a00b24 --- /dev/null +++ b/research/multipair-schedule-bound/TASK.json @@ -0,0 +1,69 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 3, + "base_commit": "ecc75c79c22d909fd42aa68437eb77c4c1361835", + "original_card": { + "id": "coverage-law-change", + "question": "Can a template or call contract leave two or more unpaid coordinates per live family?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/idle-axis-hosting/PROOF.md", + "certificates/selected-result.json" + ], + "methods": [ + "State a replacement for the coverage identity (mass = 72W + 64N) and the contract change that realizes it, with its implementation cost.", + "Find an obstruction: show which data-endpoint obligation forces exactly one unpaid coordinate in the current template." + ], + "acceptance_gate": "An explicit replacement identity, verified on a small complete instance with dirty inputs, priced with ceiling.ceiling(unpaid=...).", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Explain where the single unpaid coordinate per family comes from in the hosted template; propose one change and price it. Ideal budget: two unpaid coordinates per family is 3.77x (levers.py).", + "bottleneck_link": "The deficit is one coordinate per family minus the centre charge; doubling unpaid coordinates per family scales it directly.", + "allowed_variations": [ + "One template change or one endpoint-contract change.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Counting a coordinate as unpaid while leaving it unadvanced in the data endpoint." + ], + "overlap_terms": [ + "coverage identity", + "unpaid coordinate", + "deficit law", + "W - 64N" + ] + }, + "scope_status": "changed", + "actual_scope": "Does relaxing the B_K schedule conventions (one bank pair per invocation, pairwise exchange rho) change the coverage law or deficit per port enough to beat the T74 supplier? Proved bound N >= 2K + ceil(2K/(s-1)) on local-word invocations for every s-stage schedule, with exact attainment checks and prices on the T74 words.", + "scope_change_reason": "The card asks for two unpaid coordinates per family. This package instead tests the other template freedom named in format-limits-corrected (rows 5, 12, 13: non-B_K schedules), which the ceiling theorem does not cover, and shows it cannot raise D/W per port above the B-template at the same stage count. The unpaid-coordinate question itself is not addressed.", + "bottleneck_link": "The deficit per call is W - 64N; a schedule that ran fewer local-word invocations per port would raise it directly. Theorem S shows every schedule pays at least the B-template invocation density at its stage count, so the template convention is not what limits the deficit.", + "budget_minutes": 120, + "stop_rule": "Stop when every schedule family is either dominated by a proved bound or priced below the T74 baseline with the retained moment engine; leave even-s attainment as an open question with its maximum value.", + "outcome": "negative-result", + "evidence": "verify.py: proof-step inequalities on 10,697 random stages (GF(2), GF(3), GF(5)) with failing strengthening controls; exact replay of seven parallel-chain schedules; exhaustive K=2 frontier equal to the bound; recomputed exact prices for 14 schedule families on the T74 words; three negative controls.", + "author": "themilkman216", + "ai_assistance": "Substantial Claude (Anthropic, Opus 5.5) assistance: the investigation ran as fresh-context research branches in Claude Code; proof and code were reviewed and repackaged in the main session.", + "open_questions": [ + { + "question": "Is the Theorem S bound attained at even stage counts, in particular s = 8?", + "why_it_matters": "It is the only schedule left that could beat the nine-stage template: at most +0.26% (window-aligned idle) or +0.70% (packing ceiling) of b, and only with exact attainment.", + "first_step": "Decide K = 4, s = 4 (bound 11, chains 12) with orbit reduction under GL(X) x GL(Y) or a compiled search; or prove even s is never better than s - 1.", + "blocked_by": "Pure-Python state-space size beyond K = 3." + }, + { + "question": "Can an exchange through three bank classes (X -> Y -> Z) leave more than one unpaid coordinate per live family?", + "why_it_matters": "This is the levers.py two-unpaid-coordinates budget (x3.77), the card's main question, and lies outside Theorem S.", + "first_step": "Write the coverage identity for a three-class cycle on one pair and test it on a small exact instance with dirty inputs.", + "blocked_by": "A legal frame contract for the third class." + } + ] +} diff --git a/research/multipair-schedule-bound/VERIFY.json b/research/multipair-schedule-bound/VERIFY.json new file mode 100644 index 0000000000..19a36a3105 --- /dev/null +++ b/research/multipair-schedule-bound/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py", + "research/complex-local-word-ceiling/ceiling.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Theorem S proof-step inequalities with failing controls; exact chain replay; exhaustive K=2 frontier; recomputed family prices with the retained moment engine; flipped-sign, perturbed-extract and below-bound controls" + } + ] +} diff --git a/research/multipair-schedule-bound/chains_replay.py b/research/multipair-schedule-bound/chains_replay.py new file mode 100644 index 0000000000..8e922641fa --- /dev/null +++ b/research/multipair-schedule-bound/chains_replay.py @@ -0,0 +1,207 @@ +#!/usr/bin/env python3 +"""Exact replay of multi-pair schedules built from parallel borrowing chains (README section 3). + +A schedule here is a set of independent Sussman borrowing chains (research/cross-shear-stage-bound, +recipe tensored with I_v) run side by side in one replica: chain c owns k_c bank pairs, starts at +stage 0, runs 2 k_c + 1 counted calls on consecutive stages, and is FORWARD-first (Y_0 += X_0) or +BACKWARD-first (X_0 += Y_0, the X <-> Y mirror). A stage therefore runs several local words at +once (rank > v at the pair level), possibly with both orientations (a mixed stage). + +For each schedule the script checks, in exact rational arithmetic on random data and on all unit +vectors (pair level, v = 1): + * the endpoint is the signed exchange (X_p = -y_p, Y_p = x_p forward-first; mirror otherwise); + * every stage is [[I, H], [E, I]] with HE = EH = 0 (forward and backward pairs disjoint); + * N (pair-calls) = sum (2 k_c + 1), s = max(2 k_c + 1), and Theorem S: N >= 2K + ceil(2K/(s-1)), + with equality iff all chains have length s and (s-1)/2 divides K; + * per-port idle windows in units of a = 8 (a register is frame-locked whenever it is active in a + call or is read or written by a bridge; bridges sit between stages, as in format-limits (Sch)), + the largest idle child, and the outer halving guard m^2 > 2 R^2 with m = 1 + 8 s. +B_4 alone reproduces format-limits-corrected (Sch): idle windows {8: 6, 16: 4, 32: 4, 48: 4} per port. + +usage: python -B chains_replay.py (runs the built-in cases, prints one JSON line each) +""" +import json +import random +from fractions import Fraction as Fr + +A_STAGE = 8 + + +def chain_ops(k, base, forward): + """Ops of one borrowing chain on pairs base..base+k-1, in time order. + + ('call', stage, dst, src, sign, pair) means bank dst += sign * bank src on that pair + ('X','Y' banks); ('bridge', after_stage, dst_bank, dst_pair, src_bank, src_pair, sign). + Forward-first is the cross-shear-stage-bound recipe; backward-first swaps the roles of X and Y. + """ + X, Y = ('X', 'Y') if forward else ('Y', 'X') + ops = [('call', 0, Y, X, +1, base)] + st = 0 + for j in range(k): + p = base + j + st += 1 + ops.append(('call', st, X, Y, -1, p)) + if j + 1 < k: + ops.append(('bridge', st, X, p, X, p + 1, +1)) + ops.append(('bridge', st, Y, p + 1, Y, p, -1)) + st += 1 + ops.append(('call', st, Y, X, +1, p)) + if j + 1 < k: + ops.append(('bridge', st, X, p, X, p + 1, -1)) + ops.append(('bridge', st, Y, p + 1, Y, p, +1)) + for j in range(k - 2, -1, -1): + ops.append(('bridge', 'end', X, base + j + 1, X, base + j, +1)) + ops.append(('bridge', 'end', Y, base + j, Y, base + j + 1, -1)) + return ops, 2 * k + 1 + + +def build(chains): + """chains: list of (k, forward). Returns ops sorted into stages, K, s, N.""" + ops, base, s, N = [], 0, 0, 0 + for k, fwd in chains: + o, length = chain_ops(k, base, fwd) + ops.append(o) + base += k + s = max(s, length) + N += length + return ops, base, s, N + + +def replay(chain_ops_list, K, s, data): + """Apply all chains' ops stage by stage; returns final registers.""" + reg = {('X', p): data[('x', p)] for p in range(K)} + reg.update({('Y', p): data[('y', p)] for p in range(K)}) + order = [] + for o in chain_ops_list: + for op in o: + t = op[1] + if op[0] == 'call': + key = (t, 0) + else: + key = (s + 1, 0) if t == 'end' else (t, 1) + order.append((key, op)) + # within a stage all calls read the pre-stage values (parallel, disjoint pairs) + by_key = {} + for key, op in order: + by_key.setdefault(key, []).append(op) + for key in sorted(by_key): + ops = by_key[key] + if key[1] == 0 and key[0] <= s: + snap = dict(reg) + for op in ops: + _, _, dst, src, sign, p = op + reg[(dst, p)] = snap[(dst, p)] + sign * snap[(src, p)] + else: + for op in ops: # bridges of different chains touch disjoint pairs; apply in recipe order + _, _, db, dp, sb, sp, sign = op + reg[(db, dp)] = reg[(db, dp)] + sign * reg[(sb, sp)] + return reg + + +def stage_matrices(chain_ops_list, K, s): + """Per stage: forward pairs (E) and backward pairs (H); check disjointness (HE = EH = 0).""" + stages = {} + for o in chain_ops_list: + for op in o: + if op[0] == 'call': + _, t, dst, src, sign, p = op + stages.setdefault(t, {'E': set(), 'H': set()})['E' if dst == 'Y' else 'H'].add(p) + for t, d in stages.items(): + assert not (d['E'] & d['H']), ('a pair runs both orientations in one stage', t) + return stages + + +def idle_windows(chain_ops_list, K, s): + """Idle stretches (in stages) per register, split by calls and by bridge reads/writes.""" + locks = {(b, p): [] for b in 'XY' for p in range(K)} # events: ('active', t) or ('boundary', t) + for o in chain_ops_list: + for op in o: + if op[0] == 'call': + _, t, dst, src, sign, p = op + locks[(dst, p)].append(('active', t)) + locks[(src, p)].append(('active', t)) + elif op[1] != 'end': + _, t, db, dp, sb, sp, sign = op + locks[(db, dp)].append(('boundary', t)) + locks[(sb, sp)].append(('boundary', t)) + hist = {} + for r, ev in locks.items(): + active = {t for kind, t in ev if kind == 'active'} + cuts = {t for kind, t in ev if kind == 'boundary'} # lock between stage t and t+1 + run = 0 + for t in range(s): + if t in active: + if run: + hist[run * A_STAGE] = hist.get(run * A_STAGE, 0) + 1 + run = 0 + continue + run += 1 + if t in cuts: + hist[run * A_STAGE] = hist.get(run * A_STAGE, 0) + 1 + run = 0 + if run: + hist[run * A_STAGE] = hist.get(run * A_STAGE, 0) + 1 + return dict(sorted(hist.items())) + + +def r_max(m): + R = 0 + while 2 * (R + 1) ** 2 < m * m: + R += 1 + return R + + +def check(chains, seed=1): + ops, K, s, N = build(chains) + rng = random.Random(seed) + trials = [{(c, p): Fr(rng.randint(-99, 99), rng.randint(1, 9)) for c in 'xy' for p in range(K)}] + for c in 'xy': # all unit vectors: the full linear map + for p in range(K): + trials.append({(cc, pp): Fr(int(cc == c and pp == p)) for cc in 'xy' for pp in range(K)}) + owner, base = {}, 0 + for k, fwd in chains: + for p in range(base, base + k): + owner[p] = fwd + base += k + for data in trials: + reg = replay(ops, K, s, data) + for p in range(K): + if owner[p]: + assert reg[('X', p)] == -data[('y', p)] and reg[('Y', p)] == data[('x', p)], ('endpoint', p) + else: + assert reg[('Y', p)] == -data[('x', p)] and reg[('X', p)] == data[('y', p)], ('endpoint', p) + st = stage_matrices(ops, K, s) + assert len(st) == s + calls = sum(len(d['E']) + len(d['H']) for d in st.values()) + assert calls == N + bound = 2 * K + -(-2 * K // (s - 1)) + assert N >= bound, 'THEOREM S VIOLATED' + win = idle_windows(ops, K, s) + m = 1 + A_STAGE * s + largest = max(win) if win else 0 + mixed = sum(1 for d in st.values() if d['E'] and d['H']) + return dict(chains=[[k, 'forward' if f else 'backward'] for k, f in chains], K=K, s=s, N=N, m=m, + W_per_replica_ports=2 * K * 112, D_per_replica=2 * K * 112 - 64 * N, + theorem_S_bound=bound, attains_bound=(N == bound), mixed_orientation_stages=mixed, + pair_calls_per_stage=[len(st[t]['E']) + len(st[t]['H']) for t in sorted(st)], + idle_windows_per_port=win, largest_idle_child=largest, R_max_halving_guard=r_max(m), + largest_child_needs_split=largest > r_max(m), endpoint='signed exchange, exact') + + +CASES = [ + [(4, True)], # B_4 = the T74 template + [(2, True), (2, False)], # s = 5, two opposite chains: every stage mixed + [(2, True), (2, True)], # s = 5, rank-2v calls, one orientation per stage + [(4, True), (4, False)], # s = 9, K = 8: rank-2v mixed stages + [(4, True), (3, True)], # unequal chains in one window (dominated) + [(3, True), (3, False), (1, True)], # s = 7, K = 7, N = 17 (padded by one idle stage: the s = 8 chain value) + [(1, True), (1, False), (1, True)], # s = 3, full-rank 3-shear per pair +] + +if __name__ == '__main__': + out = [check(c) for c in CASES] + b4 = out[0] + assert b4['idle_windows_per_port'] == {8: 6, 16: 4, 32: 4, 48: 4}, b4['idle_windows_per_port'] + for o in out: + print(json.dumps(o)) + print('PASS_F1_CHAINS_REPLAY cases=%d' % len(out)) diff --git a/research/multipair-schedule-bound/diag_equality.py b/research/multipair-schedule-bound/diag_equality.py new file mode 100644 index 0000000000..f1d89948bd --- /dev/null +++ b/research/multipair-schedule-bound/diag_equality.py @@ -0,0 +1,57 @@ +"""Diagnostic for the (K=3, s=4) Theorem S equality pattern: (a, d, sigma_P, sigma_Q) after each stage. + +Stage 1: one forward and one backward rank-1 word (commuting); later stages: rank E = rank H = 1 with +a and d each rising by 1 (the only pattern equality allows, README Q2). Exhaustive over F2. +usage: python -B diag_equality.py K S +""" +import sys +from itertools import product +from collections import Counter +sys.path.insert(0, __import__('os').path.dirname(__import__('os').path.abspath(__file__))) +from sched_search import rref, rank +K = int(sys.argv[1]); S = int(sys.argv[2]); n = 2 * K; xm = (1 << K) - 1 +mats = list(product(range(1 << K), repeat=K)); zero = tuple([0] * K) + + +def mul(A, B): + out = [] + for a in A: + r = 0 + for j in range(K): + if (a >> j) & 1: + r ^= B[j] + out.append(r) + return tuple(out) + + +r1 = [M for M in mats if rank(M) == 1] +pairs = [(E, H) for E in r1 for H in r1 if mul(H, E) == zero and mul(E, H) == zero] + + +def combos(rows): + c = [0] * (1 << K) + for m in range(1, 1 << K): + low = (m & -m).bit_length() - 1 + c[m] = c[m & (m - 1)] ^ rows[low] + return c + + +def inv(P, Q): + a = K - rank([p & xm for p in P]); d = K - rank([q >> K for q in Q]) + b = K - rank([p >> K for p in P]); g = K - rank([q & xm for q in Q]) + return a, d, K - a - b, K - d - g + + +X = tuple(1 << i for i in range(K)); Y = tuple(1 << (K + i) for i in range(K)) +layer = {(rref(X, n), rref(Y, n))} +for s in range(1, S + 1): + nxt = set() + for (P, Q) in layer: + pc, qc = combos(P), combos(Q); a0, d0, _, _ = inv(P, Q) + for E, H in pairs: + P2 = rref([P[i] ^ qc[H[i]] for i in range(K)], n); Q2 = rref([Q[i] ^ pc[E[i]] for i in range(K)], n) + a, d, sp, sq = inv(P2, Q2) + if s == 1 or (a == a0 + 1 and d == d0 + 1): + nxt.add((P2, Q2)) + layer = nxt + print(s, len(layer), dict(Counter(inv(*st) for st in layer)), flush=True) diff --git a/research/multipair-schedule-bound/grader/F00.json b/research/multipair-schedule-bound/grader/F00.json new file mode 100644 index 0000000000..bc0a73c955 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F00.json @@ -0,0 +1,3 @@ +{ + "error": "non-positive deficit (hosting wall) or rank outside (0, m)" +} diff --git a/research/multipair-schedule-bound/grader/F01.json b/research/multipair-schedule-bound/grader/F01.json new file mode 100644 index 0000000000..bb9c654e75 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F01.json @@ -0,0 +1,11 @@ +{ + "label": "B_4 chain (s=9); t parallel B_4 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "m": 73, + "W": 66304, + "mass": 4816512, + "deficit": 23680, + "b_lower": "0.001679754956125544521335", + "b_upper": "0.001679754956125544521336", + "b_gain_over_T74_percent": 0.0, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F02.json b/research/multipair-schedule-bound/grader/F02.json new file mode 100644 index 0000000000..83d62f0745 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F02.json @@ -0,0 +1,11 @@ +{ + "label": "B_5 chain (s=11); t parallel B_5 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "m": 89, + "W": 82880, + "mass": 7345536, + "deficit": 30784, + "b_lower": "0.001656172228607112292838", + "b_upper": "0.001656172228607112292839", + "b_gain_over_T74_percent": -1.4039385585637565, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F03.json b/research/multipair-schedule-bound/grader/F03.json new file mode 100644 index 0000000000..0dcd9d6944 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F03.json @@ -0,0 +1,11 @@ +{ + "label": "B_6 chain (s=13); t parallel B_6 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "m": 105, + "W": 99456, + "mass": 10404992, + "deficit": 37888, + "b_lower": "0.001617382665125020322085", + "b_upper": "0.001617382665125020322086", + "b_gain_over_T74_percent": -3.7131779711720347, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F04.json b/research/multipair-schedule-bound/grader/F04.json new file mode 100644 index 0000000000..90899c337e --- /dev/null +++ b/research/multipair-schedule-bound/grader/F04.json @@ -0,0 +1,11 @@ +{ + "label": "B_7 chain (s=15); t parallel B_7 chains (rank-tv calls, any orientation mix) have the same per-wire profile", + "m": 121, + "W": 116032, + "mass": 13994880, + "deficit": 44992, + "b_lower": "0.001571246396968943417717", + "b_upper": "0.001571246396968943417718", + "b_gain_over_T74_percent": -6.459785027625851, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F05.json b/research/multipair-schedule-bound/grader/F05.json new file mode 100644 index 0000000000..c930a286af --- /dev/null +++ b/research/multipair-schedule-bound/grader/F05.json @@ -0,0 +1,11 @@ +{ + "label": "B_4 || B_4 mixed orientation, s=9, K=8 (every stage = one forward + one backward local word, rank 2v)", + "m": 73, + "W": 132608, + "mass": 9633024, + "deficit": 47360, + "b_lower": "0.001679754956125544521335", + "b_upper": "0.001679754956125544521336", + "b_gain_over_T74_percent": 0.0, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F06.json b/research/multipair-schedule-bound/grader/F06.json new file mode 100644 index 0000000000..fbe3a4e625 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F06.json @@ -0,0 +1,11 @@ +{ + "label": "B_4 || B_3 unequal chains, s=9, K=7, N=16", + "m": 73, + "W": 116032, + "mass": 8430080, + "deficit": 40256, + "b_lower": "0.001610042388228235763691", + "b_upper": "0.001610042388228235763692", + "b_gain_over_T74_percent": -4.150162953417025, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F07.json b/research/multipair-schedule-bound/grader/F07.json new file mode 100644 index 0000000000..4bce553b64 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F07.json @@ -0,0 +1,11 @@ +{ + "label": "s=8 by chains: B_3 plus one idle stage (best chain ratio N/K = 7/3), K=3, N=7", + "m": 65, + "W": 49728, + "mass": 3215744, + "deficit": 16576, + "b_lower": "0.00159028683109454299811", + "b_upper": "0.001590286831094542998111", + "b_gain_over_T74_percent": -5.326260518222558, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F08.json b/research/multipair-schedule-bound/grader/F08.json new file mode 100644 index 0000000000..b6d749fdac --- /dev/null +++ b/research/multipair-schedule-bound/grader/F08.json @@ -0,0 +1,11 @@ +{ + "label": "even s=8 at the Theorem S bound (K=7, N=16), idle children <= 40 (window multiple of a=8 under the guard); attainment open", + "m": 65, + "W": 116032, + "mass": 7501824, + "deficit": 40256, + "b_lower": "0.00168419220807572539741", + "b_upper": "0.001684192208075725397411", + "b_gain_over_T74_percent": 0.2641606702215461, + "beats_T74": true +} diff --git a/research/multipair-schedule-bound/grader/F09.json b/research/multipair-schedule-bound/grader/F09.json new file mode 100644 index 0000000000..7c2275cb11 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F09.json @@ -0,0 +1,11 @@ +{ + "label": "even s=8 at the Theorem S bound (K=7, N=16), idle children at R_max = 45 (ceiling-favorable); attainment open", + "m": 65, + "W": 116032, + "mass": 7501824, + "deficit": 40256, + "b_lower": "0.001691512754596525670768", + "b_upper": "0.001691512754596525670769", + "b_gain_over_T74_percent": 0.6999710539983294, + "beats_T74": true +} diff --git a/research/multipair-schedule-bound/grader/F10.json b/research/multipair-schedule-bound/grader/F10.json new file mode 100644 index 0000000000..249fb447cf --- /dev/null +++ b/research/multipair-schedule-bound/grader/F10.json @@ -0,0 +1,11 @@ +{ + "label": "even s=10 at the Theorem S bound (K=9, N=20), idle children at R_max = 57; attainment open", + "m": 81, + "W": 149184, + "mass": 12029440, + "deficit": 54464, + "b_lower": "0.001676096670260698677048", + "b_upper": "0.001676096670260698677049", + "b_gain_over_T74_percent": -0.2177868772766654, + "beats_T74": false +} diff --git a/research/multipair-schedule-bound/grader/F11.json b/research/multipair-schedule-bound/grader/F11.json new file mode 100644 index 0000000000..bc0a73c955 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F11.json @@ -0,0 +1,3 @@ +{ + "error": "non-positive deficit (hosting wall) or rank outside (0, m)" +} diff --git a/research/multipair-schedule-bound/grader/F12.json b/research/multipair-schedule-bound/grader/F12.json new file mode 100644 index 0000000000..64295c0298 --- /dev/null +++ b/research/multipair-schedule-bound/grader/F12.json @@ -0,0 +1,11 @@ +{ + "label": "excluded: waste-free parallel s=9, K=8, N=17", + "m": 73, + "W": 132608, + "mass": 9628288, + "deficit": 52096, + "b_lower": "0.001950681375323732307036", + "b_upper": "0.001950681375323732307037", + "b_gain_over_T74_percent": 16.128925127454053, + "beats_T74": true +} diff --git a/research/multipair-schedule-bound/grader/F13.json b/research/multipair-schedule-bound/grader/F13.json new file mode 100644 index 0000000000..ac1d24874c --- /dev/null +++ b/research/multipair-schedule-bound/grader/F13.json @@ -0,0 +1,3 @@ +{ + "error": "outside the engine search window [0, 0.003]" +} diff --git a/research/multipair-schedule-bound/inputs/T74-WORDS.json b/research/multipair-schedule-bound/inputs/T74-WORDS.json new file mode 100644 index 0000000000..d3711efaa7 --- /dev/null +++ b/research/multipair-schedule-bound/inputs/T74-WORDS.json @@ -0,0 +1,68 @@ +{ + "description": "Per-call paid profiles of the two T74 local words, extracted (not modified) from the provider registry of PR #1800 (jeremykothe2), research/capped-fusion-t74-k554/new/PLAN.json. Used only to price schedule families; the T74 construction itself is PR1800/PR1661/PR1625/PR1319 lineage and is not re-verified here.", + "source": { + "pr": 1800, + "repository": "jeremykothe2/integer-mult-bounds", + "commit": "46d865ab92e58098538b8c5348b6a131c99abf45", + "path": "research/capped-fusion-t74-k554/new/PLAN.json", + "git_blob_sha1": "b16926e163960af34b777382f08585252e1f91a6", + "sha256": "7d998108ccf8021e7c920a70fc81dc18a262d275c85fd20c77498a32fc6ef41d" + }, + "replicas": 74, + "stages": 9, + "idle_children": { + "48": 22748 + }, + "published_global_profile": { + "1": 1560432, + "2": 336336, + "3": 278724, + "4": 84912, + "5": 54612, + "8": 5328, + "48": 22748 + }, + "published_complex_endpoint_prefix": "0.00167975495612554452133567", + "words": { + "extra": { + "calls": 417, + "actual_paid_profile": { + "1": 2340, + "2": 508, + "3": 420, + "4": 126, + "5": 82, + "8": 8 + }, + "helper_count": 480, + "helper_width_total": 3738, + "helper_width_histogram": { + "4": 40, + "5": 48, + "7": 38, + "8": 114, + "9": 240 + } + }, + "gauge44": { + "calls": 249, + "actual_paid_profile": { + "1": 2348, + "2": 500, + "3": 416, + "4": 130, + "5": 82, + "8": 8 + }, + "helper_count": 480, + "helper_width_total": 3734, + "helper_width_histogram": { + "4": 44, + "5": 44, + "7": 38, + "8": 114, + "9": 240 + } + } + } +} diff --git a/research/multipair-schedule-bound/lemma_check.py b/research/multipair-schedule-bound/lemma_check.py new file mode 100644 index 0000000000..9ceb5f38e4 --- /dev/null +++ b/research/multipair-schedule-bound/lemma_check.py @@ -0,0 +1,124 @@ +#!/usr/bin/env python3 +"""Independent exact check of the per-stage inequalities used in the proof of Theorem S. + +Works over GF(p) (default p = 5, also p = 2 and p = 3) with random reachable states. A state is +M in GL_2K; P, Q are the row spaces of its top and bottom K rows; X = F^K + 0, Y = 0 + F^K. +A stage is [[I, H], [E, I]] (invertible) applied on the left, so the new top rows are A + H B and +the new bottom rows are E A + B. Bridges diag(S, T) are applied between stages. +For every stage the script checks, with a = dim P&Y, beta = dim P&X, d = dim Q&X, gamma = dim Q&Y, +sigma^P = K - a - beta, sigma^Q = K - d - gamma, h = rank H, e = rank E: + (i) a_t <= d_{t-1} + sigma^Q_{t-1} and d_t <= a_{t-1} + sigma^P_{t-1} + (ii) a_t <= a_{t-1} + h, beta_t >= beta_{t-1} - h, d_t <= d_{t-1} + e, gamma_t >= gamma_{t-1} - e + (ii') sigma^P_t <= sigma^P_{t-1} + h - (a_t - a_{t-1}), and the Q analogue +Controls: the strengthened (false) inequality a_t <= a_{t-1} + h - 1 for h >= 1 must fail somewhere, +and so must (i) without its sigma term. Prints one JSON line and PASS_THEOREM_S_LEMMAS. +""" +import json +import random +import sys + + +def rank(rows, p): + rows = [list(r) for r in rows] + rk, col, n = 0, 0, len(rows[0]) if rows else 0 + while rk < len(rows) and col < n: + piv = next((i for i in range(rk, len(rows)) if rows[i][col] % p), None) + if piv is None: + col += 1 + continue + rows[rk], rows[piv] = rows[piv], rows[rk] + inv = pow(rows[rk][col], p - 2, p) + rows[rk] = [x * inv % p for x in rows[rk]] + for i in range(len(rows)): + if i != rk and rows[i][col] % p: + f = rows[i][col] + rows[i] = [(x - f * y) % p for x, y in zip(rows[i], rows[rk])] + rk += 1 + col += 1 + return rk + + +def meet(U, V, p): + """dim(U & V) = dim U + dim V - dim(U + V) for row lists U, V of full row rank.""" + return rank(U, p) + rank(V, p) - rank(U + V, p) + + +def matmul(A, B, p): + return [[sum(a * b for a, b in zip(row, col)) % p for col in zip(*B)] for row in A] + + +def rand_rank(K, r, rng, p): + """Random K x K matrix of rank exactly r (product of K x r and r x K full-rank factors).""" + while True: + L = [[rng.randrange(p) for _ in range(r)] for _ in range(K)] + R = [[rng.randrange(p) for _ in range(K)] for _ in range(r)] + M = matmul(L, R, p) if r else [[0] * K for _ in range(K)] + if rank(M, p) == r: + return M + + +def rand_inv(K, rng, p): + while True: + M = [[rng.randrange(p) for _ in range(K)] for _ in range(K)] + if rank(M, p) == K: + return M + + +def invariants(M, K, p): + top, bot = M[:K], M[K:] + X = [[int(i == j) for j in range(2 * K)] for i in range(K)] + Y = [[int(i + K == j) for j in range(2 * K)] for i in range(K)] + a, beta = meet(top, Y, p), meet(top, X, p) + d, gamma = meet(bot, X, p), meet(bot, Y, p) + return a, beta, d, gamma + + +def run(K, p, walks, steps, seed): + rng = random.Random(seed) + stats = dict(stages=0, false_strengthened_failures=0, false_no_sigma_failures=0) + for _ in range(walks): + M = [[int(i == j) for j in range(2 * K)] for i in range(2 * K)] + for _ in range(steps): + if rng.random() < 0.5: # bridge + S, T = rand_inv(K, rng, p), rand_inv(K, rng, p) + top, bot = matmul(S, M[:K], p), matmul(T, M[K:], p) + M2 = top + bot + assert invariants(M2, K, p) == invariants(M, K, p), 'bridge changed an invariant' + M = M2 + h, e = rng.randrange(K + 1), rng.randrange(K + 1) + H, E = rand_rank(K, h, rng, p), rand_rank(K, e, rng, p) + stage = [[int(i == j) for j in range(K)] + H[i] for i in range(K)] + \ + [E[i] + [int(i == j) for j in range(K)] for i in range(K)] + if rank(stage, p) < 2 * K: + continue + a0, b0, d0, g0 = invariants(M, K, p) + M = matmul(stage, M, p) + assert rank(M, p) == 2 * K + a1, b1, d1, g1 = invariants(M, K, p) + sP0, sQ0 = K - a0 - b0, K - d0 - g0 + sP1, sQ1 = K - a1 - b1, K - d1 - g1 + assert sP0 >= 0 and sQ0 >= 0 and sP1 >= 0 and sQ1 >= 0 + assert a1 <= d0 + sQ0 and d1 <= a0 + sP0, '(i)' + assert a1 <= a0 + h and b1 >= b0 - h and d1 <= d0 + e and g1 >= g0 - e, '(ii)' + assert sP1 <= sP0 + h - (a1 - a0) and sQ1 <= sQ0 + e - (d1 - d0), "(ii')" + stats['stages'] += 1 + if h >= 1 and a1 > a0 + h - 1: + stats['false_strengthened_failures'] += 1 + if a1 > d0 or d1 > a0: + stats['false_no_sigma_failures'] += 1 + return stats + + +def main(): + out = [] + for K, p, walks in ((2, 2, 300), (2, 5, 300), (3, 3, 200), (3, 5, 200), (4, 5, 80)): + st = run(K, p, walks, 12, seed=1000 * K + p) + assert st['false_strengthened_failures'] > 0, 'control: strengthened (ii) never failed' + assert st['false_no_sigma_failures'] > 0, 'control: (i) without sigma never failed' + out.append(dict(K=K, p=p, **st)) + print(json.dumps(out)) + print('PASS_THEOREM_S_LEMMAS checks=%d' % sum(o['stages'] for o in out)) + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/research/multipair-schedule-bound/price_families.py b/research/multipair-schedule-bound/price_families.py new file mode 100644 index 0000000000..bd7f97e36d --- /dev/null +++ b/research/multipair-schedule-bound/price_families.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Price every multi-pair / mixed / alternative-rho schedule family on the T74 local words. + +Inputs (read, never modified): inputs/T74-WORDS.json (per-call paid profiles of the two T74 local +words, their 480 helper widths and the 417/249 call split, extracted from PR #1800's provider +registry; see its `source` pin), the retained exact moment engine +research/complex-k492-owner-repair/vendor/multicold/engines/moment.py and the packing-ceiling tool +research/complex-local-word-ceiling/ceiling.py. + +Per replica a family is (K pairs, s stages, N local-word invocations = pair-calls, cst per +invocation). Identities (README, Corollary): + W = 2 K v (v = 112), m = 1 + 8 s (k = 1, h - k = 8 per stage), + coverage: paid mass = (m - 1) W + cst_inv * N_inv, D = W - cst_inv * N_inv, + each pair-call carries the T74 local profile (active climbs 1792, centre 8 x rank 8, + 480 hosted helpers of total width ~3736, all in its paid children), + idle remainder = coverage mass - local mass, paid as children of rank + min(largest idle window, R_max(m)) with R_max the outer halving guard (m^2 > 2 R^2). +If the idle remainder is negative (hosting wall) the excess helper mass is paid on top of the +coverage law (unhosted), which lowers D one for one; the moment engine then sees D = mW - mass. + +Also evaluates the packing ceiling (ceiling.ceiling) for each family: the best b over ALL idle +histograms and hostings at the stated (local, m, W, N, cst). + +usage: python -B price_families.py [--write] (writes profiles/*.json, grader/*.json, FAMILIES.json) + python -B price_families.py --check (recomputes and compares with the committed files) +""" +import importlib.util +import json +import sys +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] +WORDS = HERE / 'inputs/T74-WORDS.json' +sys.path.insert(0, str(REPO / 'research/complex-local-word-ceiling')) +import ceiling as C # noqa: E402 + + +def _load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +MOMENT = _load(REPO / 'research/complex-k492-owner-repair/vendor/multicold/engines/moment.py', 'retained_moment') + +V, A, CST, T = 112, 8, 64, 74 +T74_M, T74_W = 73, 896 * 74 + + +def words(data=None): + data = data or json.loads(WORDS.read_text()) + w = data['words'] + split = {k: w[k]['calls'] for k in w} + prof = {k: {int(r): n for r, n in w[k]['actual_paid_profile'].items()} for k in w} + helpers = {k: w[k]['helper_width_total'] for k in w} + assert split == {'extra': 417, 'gauge44': 249}, split + assert split['extra'] + split['gauge44'] == T * 9 + for k in w: + mass = sum(r * n for r, n in prof[k].items()) + assert mass == 2 * V * A + CST + helpers[k], (k, mass) # 1792 + 64 + helper widths + assert prof[k][8] == 8 # the 8 rank-8 centre copies + hist = {int(x): c for x, c in w[k]['helper_width_histogram'].items()} + assert sum(hist.values()) == w[k]['helper_count'] == 480 and sum(x * c for x, c in hist.items()) == helpers[k] + # the two words plus the published idle children recompose the published global profile exactly + glob = {} + for k in w: + for r, n in prof[k].items(): + glob[r] = glob.get(r, 0) + n * split[k] + for r, n in data['idle_children'].items(): + glob[int(r)] = glob.get(int(r), 0) + n + assert {str(r): n for r, n in sorted(glob.items())} == data['published_global_profile'], glob + return prof, split, helpers + + +def bracket(H, m, W): + r = MOMENT.certify(Counter(H), m, W, False) + return Q(r['lower']), Q(r['upper']) + + +def r_max(m): + return C.max_idle_rank(m) + + +def bk_largest_window(k): + """B_k idle windows per port (format-limits (Sch)): pair 0 [(2k-2)a]; pair p [2pa, a, (2k-2p-2)a].""" + return (2 * k - 2) * A + + +def bk_windows(k): + w = {} + def add(x): + if x > 0: + w[x] = w.get(x, 0) + 2 # X and Y bank + add((2 * k - 2) * A) + for p in range(1, k): + add(2 * p * A); add(A); add((2 * k - 2 * p - 2) * A) + return dict(sorted(w.items())) + + +def build(fam, prof, split): + """Integer global profile over T replicas.""" + K, s, N, cst_inv, pairs_per_inv = fam['K'], fam['s'], fam['N'], fam['cst_inv'], fam.get('pairs_per_inv', 1) + m, W = 1 + A * s, 2 * K * V + n_inv = N // pairs_per_inv + assert n_inv * pairs_per_inv == N + total_pair_calls = N * T + n_extra = round(total_pair_calls * split['extra'] / (split['extra'] + split['gauge44'])) + n_g = total_pair_calls - n_extra + H = {} + for word, n in (('extra', n_extra), ('gauge44', n_g)): + for r, c in prof[word].items(): + H[r] = H.get(r, 0) + c * n + # a shared-centre invocation pays ONE centre path for its pairs_per_inv local words + H[8] -= 8 * (pairs_per_inv - 1) * n_inv * T + local_mass = sum(r * c for r, c in H.items()) + coverage = (m - 1) * W * T + cst_inv * n_inv * T + idle = coverage - local_mass + Rcap = min(fam.get('largest_window') or 10 ** 9, r_max(m)) + if idle > 0: + q, rem = divmod(idle, Rcap) + H[Rcap] = H.get(Rcap, 0) + q + if rem: + H[rem] = H.get(rem, 0) + 1 + H = {str(r): c for r, c in sorted(H.items()) if c} + return dict(m=m, W=W * T, H=H, label=fam['label']), dict(m=m, W_rep=W, R_cap=Rcap, R_max=r_max(m), + coverage_rep=Q(coverage, T), local_rep=Q(local_mass, T), idle_rep=Q(idle, T), + hosting_wall=idle < 0, D_rep=Q(W * T - cst_inv * n_inv * T + min(idle, 0), T)) + + +def grade(prof_json, base): + """Exact 1e-24 bracket of the complex exponent with the retained moment engine.""" + H = {int(r): c for r, c in prof_json['H'].items()} + m, W = prof_json['m'], prof_json['W'] + mass = sum(r * c for r, c in H.items()) + if m * W - mass <= 0 or any(not 0 < r < m for r in H): + return {'error': 'non-positive deficit (hosting wall) or rank outside (0, m)'} + try: + lo, hi = bracket(H, m, W) + except AssertionError: + return {'error': 'outside the engine search window [0, 0.003]'} + return dict(label=prof_json['label'], m=m, W=W, mass=mass, deficit=m * W - mass, + b_lower=MOMENT.decimal(lo), b_upper=MOMENT.decimal(hi), + b_gain_over_T74_percent=float((lo / base[0] - 1) * 100), beats_T74=lo > base[1]) + + +def ceiling(fam, prof, split): + """Packing ceiling: all idle mass at R_max(m); None if the local word overflows the coverage law.""" + K, s, N, cst_inv, ppi = fam['K'], fam['s'], fam['N'], fam['cst_inv'], fam.get('pairs_per_inv', 1) + tot = split['extra'] + split['gauge44'] + local = {} + for word in ('extra', 'gauge44'): + for r, c in prof[word].items(): + local[r] = local.get(r, 0) + Q(c * split[word] * ppi, tot) + local[8] -= 8 * (ppi - 1) + m = 1 + A * s + try: + lo, hi = C.ceiling(local, m, 2 * K * V, N // ppi, cst_inv) + except ValueError as e: + return {'error': str(e)} + return {'a_hi': float(hi), 'a_hi_exact': str(hi)} + + +def families(): + fams = [] + for k in (3, 4, 5, 6, 7): + s = 2 * k + 1 + fams.append(dict(label='B_%d chain (s=%d); t parallel B_%d chains (rank-tv calls, any orientation mix) ' + 'have the same per-wire profile' % (k, s, k), K=k, s=s, + N=2 * k + 1, cst_inv=CST, largest_window=bk_largest_window(k), + status='attained (chains_replay.py); Theorem S frontier at odd s')) + fams.append(dict(label='B_4 || B_4 mixed orientation, s=9, K=8 (every stage = one forward + one backward ' + 'local word, rank 2v)', K=8, s=9, N=18, cst_inv=CST, largest_window=48, + status='attained (chains_replay.py); equals two T74 replicas')) + fams.append(dict(label='B_4 || B_3 unequal chains, s=9, K=7, N=16', K=7, s=9, N=16, cst_inv=CST, + largest_window=48, status='attained (chains_replay.py); Theorem S tight (ceil)')) + fams.append(dict(label='s=8 by chains: B_3 plus one idle stage (best chain ratio N/K = 7/3), K=3, N=7', K=3, s=8, N=7, + cst_inv=CST, largest_window=40, status='attained (s=7 schedule padded by one stage)')) + for s, K, N, R, note in ((8, 7, 16, 40, 'idle children <= 40 (window multiple of a=8 under the guard)'), + (8, 7, 16, None, 'idle children at R_max = 45 (ceiling-favorable)'), + (10, 9, 20, None, 'idle children at R_max = 57'), + (6, 5, 12, None, 'idle children at R_max = 34')): + k = (s - 1) // 2 + fams.append(dict(label='even s=%d at the Theorem S bound (K=%d, N=%d), %s; attainment open' % (s, K, N, note), + K=K, s=s, N=N, cst_inv=CST, largest_window=R, + status='HYPOTHETICAL: only the lower bound is proved; chains need N=%d; F2 search ' + 'refutes the bound at (K=3, s=4)' % (2 * K + -(-K // k)))) + fams.append(dict(label='excluded: waste-free parallel s=9, K=8, N=17', K=8, s=9, N=17, cst_inv=CST, + largest_window=None, status='EXCLUDED by Theorem S (N >= 18)')) + fams.append(dict(label='excluded: s=9, K=8, two pairs per invocation, ONE centre path per invocation', + K=8, s=9, N=18, cst_inv=CST, pairs_per_inv=2, largest_window=48, + status='EXCLUDED: the two pairs carry independent totals (README Q1); the grader ' + 'window stops at b = 0.003, so only the ceiling is reported')) + return fams + + +def main(): + write = '--write' in sys.argv + check = '--check' in sys.argv + prof, split, helpers = words() + data = json.loads(WORDS.read_text()) + base = bracket({int(r): n for r, n in data['published_global_profile'].items()}, T74_M, T74_W) + assert MOMENT.decimal(base[0]).startswith(data['published_complex_endpoint_prefix'][:-2]), base + mismatches = [] + rows = [] + (HERE / 'profiles').mkdir(exist_ok=True) + (HERE / 'grader').mkdir(exist_ok=True) + for i, fam in enumerate(families()): + prof_json, info = build(fam, prof, split) + slug = 'F%02d' % i + p = HERE / 'profiles' / (slug + '.json') + g = grade(prof_json, base) + if write: + p.write_text(json.dumps(prof_json, indent=1) + '\n') + (HERE / 'grader' / (slug + '.json')).write_text(json.dumps(g, indent=1) + '\n') + if check: + for path, obj in ((p, prof_json), (HERE / 'grader' / (slug + '.json'), g)): + if json.loads(path.read_text()) != json.loads(json.dumps(obj)): + mismatches.append(str(path.relative_to(HERE))) + ce = ceiling(fam, prof, split) + row = dict(id=slug, **{k: v for k, v in fam.items()}, **{k: (str(v) if isinstance(v, Q) else v) + for k, v in info.items()}, b_lower=g.get('b_lower'), gain_percent=g.get('b_gain_over_T74_percent'), + beats_T74=g.get('beats_T74'), grader_error=g.get('error'), ceiling=ce) + if fam['label'].startswith('B_'): + row['idle_windows_per_port'] = bk_windows(fam['K']) + rows.append(row) + print(json.dumps({k: row[k] for k in ('id', 'label', 'm', 'W_rep', 'D_rep', 'idle_rep', 'R_cap', + 'hosting_wall', 'b_lower', 'gain_percent', 'ceiling')})) + fam = dict(T74_b_bracket=[MOMENT.decimal(base[0]), MOMENT.decimal(base[1])], helpers_per_call=helpers, + call_split=split, families=rows) + if write: + (HERE / 'FAMILIES.json').write_text(json.dumps(fam, indent=1) + '\n') + if check: + if json.loads((HERE / 'FAMILIES.json').read_text()) != json.loads(json.dumps(fam)): + mismatches.append('FAMILIES.json') + assert not mismatches, mismatches + print('PASS_F1_PRICES families=%d' % len(rows)) + return fam + + +if __name__ == '__main__': + main() diff --git a/research/multipair-schedule-bound/profiles/F00.json b/research/multipair-schedule-bound/profiles/F00.json new file mode 100644 index 0000000000..66824c33b0 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F00.json @@ -0,0 +1,13 @@ +{ + "m": 57, + "W": 49728, + "H": { + "1": 1213672, + "2": 261592, + "3": 216784, + "4": 66044, + "5": 42476, + "8": 4144 + }, + "label": "B_3 chain (s=7); t parallel B_3 chains (rank-tv calls, any orientation mix) have the same per-wire profile" +} diff --git a/research/multipair-schedule-bound/profiles/F01.json b/research/multipair-schedule-bound/profiles/F01.json new file mode 100644 index 0000000000..68768d52a4 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F01.json @@ -0,0 +1,14 @@ +{ + "m": 73, + "W": 66304, + "H": { + "1": 1560432, + "2": 336336, + "3": 278724, + "4": 84912, + "5": 54612, + "8": 5328, + "48": 22748 + }, + "label": "B_4 chain (s=9); t parallel B_4 chains (rank-tv calls, any orientation mix) have the same per-wire profile" +} diff --git a/research/multipair-schedule-bound/profiles/F02.json b/research/multipair-schedule-bound/profiles/F02.json new file mode 100644 index 0000000000..86bfd71232 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F02.json @@ -0,0 +1,15 @@ +{ + "m": 89, + "W": 82880, + "H": { + "1": 1907192, + "2": 411080, + "3": 340664, + "4": 103780, + "5": 66748, + "8": 6512, + "12": 1, + "62": 45052 + }, + "label": "B_5 chain (s=11); t parallel B_5 chains (rank-tv calls, any orientation mix) have the same per-wire profile" +} diff --git a/research/multipair-schedule-bound/profiles/F03.json b/research/multipair-schedule-bound/profiles/F03.json new file mode 100644 index 0000000000..e319d4979f --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F03.json @@ -0,0 +1,15 @@ +{ + "m": 105, + "W": 99456, + "H": { + "1": 2253960, + "2": 485816, + "3": 402600, + "4": 122652, + "5": 78884, + "8": 7696, + "34": 1, + "74": 67905 + }, + "label": "B_6 chain (s=13); t parallel B_6 chains (rank-tv calls, any orientation mix) have the same per-wire profile" +} diff --git a/research/multipair-schedule-bound/profiles/F04.json b/research/multipair-schedule-bound/profiles/F04.json new file mode 100644 index 0000000000..8bedc4689a --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F04.json @@ -0,0 +1,15 @@ +{ + "m": 121, + "W": 116032, + "H": { + "1": 2600720, + "2": 560560, + "3": 464540, + "4": 141520, + "5": 91020, + "8": 8880, + "10": 1, + "85": 91614 + }, + "label": "B_7 chain (s=15); t parallel B_7 chains (rank-tv calls, any orientation mix) have the same per-wire profile" +} diff --git a/research/multipair-schedule-bound/profiles/F05.json b/research/multipair-schedule-bound/profiles/F05.json new file mode 100644 index 0000000000..62ec0a3db4 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F05.json @@ -0,0 +1,14 @@ +{ + "m": 73, + "W": 132608, + "H": { + "1": 3120864, + "2": 672672, + "3": 557448, + "4": 169824, + "5": 109224, + "8": 10656, + "48": 45496 + }, + "label": "B_4 || B_4 mixed orientation, s=9, K=8 (every stage = one forward + one backward local word, rank 2v)" +} diff --git a/research/multipair-schedule-bound/profiles/F06.json b/research/multipair-schedule-bound/profiles/F06.json new file mode 100644 index 0000000000..b1e83e2955 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F06.json @@ -0,0 +1,15 @@ +{ + "m": 73, + "W": 116032, + "H": { + "1": 2774104, + "2": 597928, + "3": 495508, + "4": 150956, + "5": 97088, + "8": 9472, + "12": 1, + "48": 37678 + }, + "label": "B_4 || B_3 unequal chains, s=9, K=7, N=16" +} diff --git a/research/multipair-schedule-bound/profiles/F07.json b/research/multipair-schedule-bound/profiles/F07.json new file mode 100644 index 0000000000..bf9d7bacba --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F07.json @@ -0,0 +1,15 @@ +{ + "m": 65, + "W": 49728, + "H": { + "1": 1213672, + "2": 261592, + "3": 216784, + "4": 66044, + "5": 42476, + "8": 4144, + "28": 1, + "40": 7970 + }, + "label": "s=8 by chains: B_3 plus one idle stage (best chain ratio N/K = 7/3), K=3, N=7" +} diff --git a/research/multipair-schedule-bound/profiles/F08.json b/research/multipair-schedule-bound/profiles/F08.json new file mode 100644 index 0000000000..6bd8c3d0da --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F08.json @@ -0,0 +1,15 @@ +{ + "m": 65, + "W": 116032, + "H": { + "1": 2774104, + "2": 597928, + "3": 495508, + "4": 150956, + "5": 97088, + "8": 9472, + "20": 1, + "40": 22007 + }, + "label": "even s=8 at the Theorem S bound (K=7, N=16), idle children <= 40 (window multiple of a=8 under the guard); attainment open" +} diff --git a/research/multipair-schedule-bound/profiles/F09.json b/research/multipair-schedule-bound/profiles/F09.json new file mode 100644 index 0000000000..54895576f5 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F09.json @@ -0,0 +1,15 @@ +{ + "m": 65, + "W": 116032, + "H": { + "1": 2774104, + "2": 597928, + "3": 495508, + "4": 150956, + "5": 97088, + "8": 9472, + "10": 1, + "45": 19562 + }, + "label": "even s=8 at the Theorem S bound (K=7, N=16), idle children at R_max = 45 (ceiling-favorable); attainment open" +} diff --git a/research/multipair-schedule-bound/profiles/F10.json b/research/multipair-schedule-bound/profiles/F10.json new file mode 100644 index 0000000000..d1d3a95f05 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F10.json @@ -0,0 +1,15 @@ +{ + "m": 81, + "W": 149184, + "H": { + "1": 3467624, + "2": 747416, + "3": 619388, + "4": 188692, + "5": 121360, + "8": 11840, + "51": 1, + "57": 65833 + }, + "label": "even s=10 at the Theorem S bound (K=9, N=20), idle children at R_max = 57; attainment open" +} diff --git a/research/multipair-schedule-bound/profiles/F11.json b/research/multipair-schedule-bound/profiles/F11.json new file mode 100644 index 0000000000..b18b3514f5 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F11.json @@ -0,0 +1,13 @@ +{ + "m": 49, + "W": 82880, + "H": { + "1": 2080576, + "2": 448448, + "3": 371632, + "4": 113216, + "5": 72816, + "8": 7104 + }, + "label": "even s=6 at the Theorem S bound (K=5, N=12), idle children at R_max = 34; attainment open" +} diff --git a/research/multipair-schedule-bound/profiles/F12.json b/research/multipair-schedule-bound/profiles/F12.json new file mode 100644 index 0000000000..2daf83f890 --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F12.json @@ -0,0 +1,15 @@ +{ + "m": 73, + "W": 132608, + "H": { + "1": 2947480, + "2": 635304, + "3": 526480, + "4": 160388, + "5": 103156, + "8": 10064, + "25": 1, + "51": 50841 + }, + "label": "excluded: waste-free parallel s=9, K=8, N=17" +} diff --git a/research/multipair-schedule-bound/profiles/F13.json b/research/multipair-schedule-bound/profiles/F13.json new file mode 100644 index 0000000000..a693f6583e --- /dev/null +++ b/research/multipair-schedule-bound/profiles/F13.json @@ -0,0 +1,14 @@ +{ + "m": 73, + "W": 132608, + "H": { + "1": 3120864, + "2": 672672, + "3": 557448, + "4": 169824, + "5": 109224, + "8": 5328, + "48": 45496 + }, + "label": "excluded: s=9, K=8, two pairs per invocation, ONE centre path per invocation" +} diff --git a/research/multipair-schedule-bound/sched_search.py b/research/multipair-schedule-bound/sched_search.py new file mode 100644 index 0000000000..b4f1327f89 --- /dev/null +++ b/research/multipair-schedule-bound/sched_search.py @@ -0,0 +1,148 @@ +#!/usr/bin/env python3 +"""Exhaustive F2 check of the multi-pair stage/call frontier (Theorem S of README.md). + +Pair-level model (research/cross-shear-stage-bound tensored with I_v): data (X, Y) in F^K x F^K, +K bank pairs. One STAGE runs any set of local words in parallel on disjoint pairs, forward +(Y_p += X_p) or backward (X_q += Y_q), with arbitrary invertible block-diagonal bridges between +stages. After bridges a stage is [[I, H], [E, I]] with HE = 0 and EH = 0 (forward and backward +pairs are disjoint), and it costs N_stage = rank E + rank H local-word invocations (pair-calls). +Bridges are absorbed: the state is M modulo left block-diagonal action, i.e. the pair +(P, Q) = (row space of the top block row, row space of the bottom block row). A stage maps +top -> top + H bottom and bottom -> bottom + E top (old rows; HE = EH = 0 makes it well defined). +Start (X, Y), goal (Y, X) = block antidiagonal. `--alternating` restricts every stage to E = 0 +or H = 0 alternately (one orientation per stage, the B_K template's form). + +Prints, for each stage count s <= S, the minimum number of pair-calls N reaching the goal +in exactly s stages (None if > N_max), and compares with + Theorem S lower bound N >= 2K + ceil(2K / (s - 1)) (s >= 2) + parallel B_k chains N = 2K + ceil(K / k), k = floor((s - 1) / 2) (s >= 3). +Standard library only; exact F2 arithmetic on bitmasks. +usage: python -B sched_search.py K N_max S [--alternating] [--maxrank r] [--wastefree-after-1] + --maxrank r every stage has rank E <= r and rank H <= r (a restriction: found N are upper + bounds on the true frontier, the Theorem S assertion still applies) + --wastefree-after-1 prune every stage t >= 2 that does not lower Phi by its full cost +""" +import json +import sys +from itertools import product + + +def rref(rows, n): + """Canonical reduced row echelon basis (tuple of ints) of span(rows) in F2^n.""" + piv = {} # leading bit -> row; rows reduced at all pivots + for r in rows: + for lead in sorted(piv, reverse=True): + if (r >> lead) & 1: + r ^= piv[lead] + if r: + lead = r.bit_length() - 1 + for l2 in piv: + if (piv[l2] >> lead) & 1: + piv[l2] ^= r + piv[lead] = r + return tuple(sorted(piv.values(), reverse=True)) + + +def rank(rows): + basis = [] + for r in rows: + for b in basis: + r = min(r, r ^ b) + if r: + basis.append(r) + return len(basis) + + +def main(): + K, N_max, S = int(sys.argv[1]), int(sys.argv[2]), int(sys.argv[3]) + alternating = '--alternating' in sys.argv + maxrank = int(sys.argv[sys.argv.index('--maxrank') + 1]) if '--maxrank' in sys.argv else None + wastefree = '--wastefree-after-1' in sys.argv + n = 2 * K + xmask = (1 << K) - 1 # low K bits = X coordinates, high K bits = Y + X = tuple(1 << i for i in range(K)) + Y = tuple(1 << (K + i) for i in range(K)) + start, goal = (rref(X, n), rref(Y, n)), (rref(Y, n), rref(X, n)) + + mats = list(product(range(1 << K), repeat=K)) # matrix = tuple of K row masks (bit j = column j) + + def mul(A, B): # (AB)_i = XOR of rows B_j with A_ij = 1 + out = [] + for a in A: + r = 0 + for j in range(K): + if (a >> j) & 1: + r ^= B[j] + out.append(r) + return tuple(out) + + rk = {M: rank(M) for M in mats} + zero = tuple([0] * K) + pairs = [] # (E, H, cost) with HE = EH = 0 + for E in mats: + for H in mats: + if E == zero and H == zero: + continue + if alternating and E != zero and H != zero: + continue + if maxrank is not None and (rk[E] > maxrank or rk[H] > maxrank): + continue + if mul(H, E) == zero and mul(E, H) == zero: + pairs.append((E, H, rk[E] + rk[H])) + + def combos(rows): + c = [0] * (1 << K) + for m in range(1, 1 << K): + low = (m & -m).bit_length() - 1 + c[m] = c[m & (m - 1)] ^ rows[low] + return c + + def phi(P, Q): + return rank([p & xmask for p in P]) + rank([q >> K for q in Q]) + + layer = {start: 0} + result = {} + for s in range(1, S + 1): + nxt = {} + for (P, Q), used in layer.items(): + pc, qc = combos(P), combos(Q) + topc, botc = {}, {} + for E, H, cost in pairs: + if alternating and ((s % 2 == 1) != (E != zero)): + continue # odd stages forward (E), even backward (H) + if used + cost > N_max: + continue + if H not in topc: + topc[H] = rref([P[i] ^ qc[H[i]] for i in range(K)], n) + if E not in botc: + botc[E] = rref([Q[i] ^ pc[E[i]] for i in range(K)], n) + st = (topc[H], botc[E]) + u = used + cost + ph = phi(*st) + if u + ph > N_max: + continue + if wastefree and s >= 2 and ph != phi(P, Q) - cost: + continue + if nxt.get(st, 1 << 30) > u: + nxt[st] = u + layer = nxt + result[s] = layer.get(goal) + print(json.dumps({'K': K, 'stage': s, 'states': len(layer), 'min_N': result[s]}), flush=True) + + rows = [] + best = None # min N over schedules with AT MOST s stages + for s in range(2, S + 1): + bound = 2 * K + -(-2 * K // (s - 1)) + k = (s - 1) // 2 + chains = 2 * K + -(-K // k) if k >= 1 else None + if result[s] is not None: + best = result[s] if best is None else min(best, result[s]) + rows.append({'s': s, 'min_N_exactly_s': result[s], 'min_N_at_most_s': best, + 'theorem_S_bound': bound, 'parallel_chains': chains}) + assert result[s] is None or result[s] >= bound, ('THEOREM S VIOLATED', s, result[s], bound) + print(json.dumps({'K': K, 'N_max': N_max, 'alternating': alternating, 'maxrank': maxrank, + 'wastefree_after_1': wastefree, 'pairs': len(pairs), 'frontier': rows})) + + +if __name__ == '__main__': + main() diff --git a/research/multipair-schedule-bound/search/K2_alternating.json b/research/multipair-schedule-bound/search/K2_alternating.json new file mode 100644 index 0000000000..fda00cca52 --- /dev/null +++ b/research/multipair-schedule-bound/search/K2_alternating.json @@ -0,0 +1,7 @@ +{"K": 2, "stage": 1, "states": 15, "min_N": null} +{"K": 2, "stage": 2, "states": 225, "min_N": null} +{"K": 2, "stage": 3, "states": 526, "min_N": 6} +{"K": 2, "stage": 4, "states": 560, "min_N": 6} +{"K": 2, "stage": 5, "states": 436, "min_N": 5} +{"K": 2, "stage": 6, "states": 184, "min_N": 6} +{"K": 2, "N_max": 8, "alternating": true, "maxrank": null, "wastefree_after_1": false, "pairs": 30, "frontier": [{"s": 2, "min_N_exactly_s": null, "min_N_at_most_s": null, "theorem_S_bound": 8, "parallel_chains": null}, {"s": 3, "min_N_exactly_s": 6, "min_N_at_most_s": 6, "theorem_S_bound": 6, "parallel_chains": 6}, {"s": 4, "min_N_exactly_s": 6, "min_N_at_most_s": 6, "theorem_S_bound": 6, "parallel_chains": 6}, {"s": 5, "min_N_exactly_s": 5, "min_N_at_most_s": 5, "theorem_S_bound": 5, "parallel_chains": 5}, {"s": 6, "min_N_exactly_s": 6, "min_N_at_most_s": 5, "theorem_S_bound": 5, "parallel_chains": 5}]} diff --git a/research/multipair-schedule-bound/search/K2_mixed.json b/research/multipair-schedule-bound/search/K2_mixed.json new file mode 100644 index 0000000000..d7b79da959 --- /dev/null +++ b/research/multipair-schedule-bound/search/K2_mixed.json @@ -0,0 +1,7 @@ +{"K": 2, "stage": 1, "states": 39, "min_N": null} +{"K": 2, "stage": 2, "states": 397, "min_N": null} +{"K": 2, "stage": 3, "states": 560, "min_N": 6} +{"K": 2, "stage": 4, "states": 560, "min_N": 6} +{"K": 2, "stage": 5, "states": 436, "min_N": 5} +{"K": 2, "stage": 6, "states": 184, "min_N": 6} +{"K": 2, "N_max": 8, "alternating": false, "maxrank": null, "wastefree_after_1": false, "pairs": 39, "frontier": [{"s": 2, "min_N_exactly_s": null, "min_N_at_most_s": null, "theorem_S_bound": 8, "parallel_chains": null}, {"s": 3, "min_N_exactly_s": 6, "min_N_at_most_s": 6, "theorem_S_bound": 6, "parallel_chains": 6}, {"s": 4, "min_N_exactly_s": 6, "min_N_at_most_s": 6, "theorem_S_bound": 6, "parallel_chains": 6}, {"s": 5, "min_N_exactly_s": 5, "min_N_at_most_s": 5, "theorem_S_bound": 5, "parallel_chains": 5}, {"s": 6, "min_N_exactly_s": 6, "min_N_at_most_s": 5, "theorem_S_bound": 5, "parallel_chains": 5}]} diff --git a/research/multipair-schedule-bound/search/K3_s4_N8_equality.json b/research/multipair-schedule-bound/search/K3_s4_N8_equality.json new file mode 100644 index 0000000000..14c090eb8b --- /dev/null +++ b/research/multipair-schedule-bound/search/K3_s4_N8_equality.json @@ -0,0 +1,5 @@ +{"K": 3, "stage": 1, "states": 539, "min_N": null} +{"K": 3, "stage": 2, "states": 22736, "min_N": null} +{"K": 3, "stage": 3, "states": 116032, "min_N": null} +{"K": 3, "stage": 4, "states": 32291, "min_N": null} +{"K": 3, "N_max": 8, "alternating": false, "maxrank": 1, "wastefree_after_1": true, "pairs": 539, "frontier": [{"s": 2, "min_N_found": null, "theorem_S_bound": 12, "parallel_chains": null}, {"s": 3, "min_N_found": null, "theorem_S_bound": 9, "parallel_chains": 9}, {"s": 4, "min_N_found": null, "theorem_S_bound": 8, "parallel_chains": 9}]} diff --git a/research/multipair-schedule-bound/search/K3_s4_N8_equality_full.json b/research/multipair-schedule-bound/search/K3_s4_N8_equality_full.json new file mode 100644 index 0000000000..7e4296b115 --- /dev/null +++ b/research/multipair-schedule-bound/search/K3_s4_N8_equality_full.json @@ -0,0 +1,5 @@ +{"K": 3, "stage": 1, "states": 1127, "min_N": null} +{"K": 3, "stage": 2, "states": 46256, "min_N": null} +{"K": 3, "stage": 3, "states": 148960, "min_N": null} +{"K": 3, "stage": 4, "states": 46991, "min_N": null} +{"K": 3, "N_max": 8, "alternating": false, "maxrank": null, "wastefree_after_1": true, "pairs": 2051, "frontier": [{"s": 2, "min_N_exactly_s": null, "min_N_at_most_s": null, "theorem_S_bound": 12, "parallel_chains": null}, {"s": 3, "min_N_exactly_s": null, "min_N_at_most_s": null, "theorem_S_bound": 9, "parallel_chains": 9}, {"s": 4, "min_N_exactly_s": null, "min_N_at_most_s": null, "theorem_S_bound": 8, "parallel_chains": 9}]} diff --git a/research/multipair-schedule-bound/search/K3_s4_equality_diagnostic.txt b/research/multipair-schedule-bound/search/K3_s4_equality_diagnostic.txt new file mode 100644 index 0000000000..4c7e265ab8 --- /dev/null +++ b/research/multipair-schedule-bound/search/K3_s4_equality_diagnostic.txt @@ -0,0 +1,4 @@ +1 441 {(0, 0, 1, 1): 441} +2 7056 {(1, 1, 1, 1): 7056} +3 2352 {(2, 2, 0, 0): 784, (2, 2, 1, 0): 784, (2, 2, 0, 1): 784} +4 0 {} diff --git a/research/multipair-schedule-bound/search/K3_s5_N8_rank2_wastefree.json b/research/multipair-schedule-bound/search/K3_s5_N8_rank2_wastefree.json new file mode 100644 index 0000000000..a688fb49d2 --- /dev/null +++ b/research/multipair-schedule-bound/search/K3_s5_N8_rank2_wastefree.json @@ -0,0 +1,6 @@ +{"K": 3, "stage": 1, "states": 1127, "min_N": null} +{"K": 3, "stage": 2, "states": 46256, "min_N": null} +{"K": 3, "stage": 3, "states": 148960, "min_N": null} +{"K": 3, "stage": 4, "states": 46991, "min_N": null} +{"K": 3, "stage": 5, "states": 4656, "min_N": 8} +{"K": 3, "N_max": 8, "alternating": false, "maxrank": 2, "wastefree_after_1": true, "pairs": 1715, "frontier": [{"s": 2, "min_N_found": null, "theorem_S_bound": 12, "parallel_chains": null}, {"s": 3, "min_N_found": null, "theorem_S_bound": 9, "parallel_chains": 9}, {"s": 4, "min_N_found": null, "theorem_S_bound": 8, "parallel_chains": 9}, {"s": 5, "min_N_found": 8, "theorem_S_bound": 8, "parallel_chains": 8}]} diff --git a/research/multipair-schedule-bound/verify.py b/research/multipair-schedule-bound/verify.py new file mode 100644 index 0000000000..8982f4442e --- /dev/null +++ b/research/multipair-schedule-bound/verify.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +"""Bounded verification for research/multipair-schedule-bound (standard library only, about 1 minute). + +Checks: + 1. lemma_check.py: the per-stage inequalities of the Theorem S proof on random reachable states over + GF(2), GF(3), GF(5), with two false-strengthening controls that must fail somewhere. + 2. chains_replay.py: exact rational replay of seven parallel-chain schedules (signed exchange endpoint, + stage shapes, N = Theorem S bound where claimed, B_4 idle windows {8:6,16:4,32:4,48:4}); its stdout + must equal CHAINS-REPLAY.jsonl byte for byte. + 3. sched_search.py K = 2, mixed and alternating stages, N_max 8, s <= 6: exhaustive frontier equals + the Theorem S bound for every s >= 3; outputs equal search/K2_*.json. + 4. price_families.py --check: every family profile, its exact moment bracket and packing ceiling are + recomputed from inputs/T74-WORDS.json with the retained engine and equal the committed files. +Controls (each must be rejected): + a. a chain recipe with one call sign flipped fails the exact endpoint check; + b. a T74 extract with one rank-1 child moved to rank 2 fails the published-profile recomposition; + c. a claimed schedule with N one below the Theorem S bound (family F12) is recorded as excluded and + no attained family lies below the bound. +Long searches (K = 3) are not rerun here; their committed outputs are listed in README.md. +""" +import copy +import importlib.util +import json +import subprocess +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +PY = sys.executable + + +def run(*args): + out = subprocess.run([PY, '-B', *args], cwd=HERE, capture_output=True, text=True) + assert out.returncode == 0, (args, out.stderr[-2000:]) + return out.stdout + + +def load(name): + spec = importlib.util.spec_from_file_location(name, HERE / (name + '.py')) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + + +def bound(K, s): + return 2 * K + -(-2 * K // (s - 1)) + + +def main(): + assert __debug__, 'run with assertions enabled' + out = run('lemma_check.py') + assert out.strip().endswith('PASS_THEOREM_S_LEMMAS checks=10697'), out[-300:] + print('PASS lemma inequalities (10697 stages, both controls fail as required)') + + out = run('chains_replay.py') + assert out == (HERE / 'CHAINS-REPLAY.jsonl').read_text(), 'chain replay differs from CHAINS-REPLAY.jsonl' + rows = [json.loads(line) for line in out.splitlines()[:-1]] + assert all(r['N'] >= r['theorem_S_bound'] for r in rows) + assert rows[0]['idle_windows_per_port'] == {'8': 6, '16': 4, '32': 4, '48': 4} + print('PASS chain replay (7 schedules, exact endpoints, B_4 windows)') + + for flag, ref in (([], 'search/K2_mixed.json'), (['--alternating'], 'search/K2_alternating.json')): + out = run('sched_search.py', '2', '8', '6', *flag) + assert out == (HERE / ref).read_text(), ref + front = json.loads(out.splitlines()[-1])['frontier'] + for row in front: + if row['s'] >= 3: + assert row['min_N_at_most_s'] == row['theorem_S_bound'] == bound(2, row['s']), row + print('PASS exhaustive K=2 frontier = Theorem S bound (mixed and alternating stages)') + + out = run('price_families.py', '--check') + assert out.strip().endswith('PASS_F1_PRICES families=14'), out[-300:] + fam = json.loads((HERE / 'FAMILIES.json').read_text()) + by = {f['id']: f for f in fam['families']} + assert by['F01']['b_lower'] == fam['T74_b_bracket'][0] and by['F05']['b_lower'] == fam['T74_b_bracket'][0] + assert not any(f.get('beats_T74') for f in fam['families'] if f['status'].startswith('attained')) + print('PASS family prices recomputed (attained schedules never beat T74; best attained = T74 exactly)') + + # control a: flipped call sign + cr = load('chains_replay') + orig = cr.chain_ops + + def broken(k, base, forward): + ops, length = orig(k, base, forward) + ops = list(ops) + op = ops[1] + assert op[0] == 'call' + ops[1] = op[:4] + (-op[4],) + op[5:] + return ops, length + cr.chain_ops = broken + try: + cr.check([(4, True)]) + except AssertionError: + pass + else: + raise AssertionError('control a: flipped sign accepted') + cr.chain_ops = orig + print('PASS control a (flipped call sign rejected)') + + # control b: perturbed T74 extract + pf = load('price_families') + data = json.loads((HERE / 'inputs/T74-WORDS.json').read_text()) + bad = copy.deepcopy(data) + p = bad['words']['extra']['actual_paid_profile'] + p['1'] -= 1 + p['2'] = p['2'] + 1 + bad['words']['extra']['helper_width_total'] += 1 + try: + pf.words(bad) + except AssertionError: + pass + else: + raise AssertionError('control b: perturbed extract accepted') + print('PASS control b (perturbed T74 extract rejected)') + + # control c: below-bound schedules are only ever excluded + for f in fam['families']: + b = bound(f['K'], f['s']) + if f['N'] < b: + assert f['status'].startswith('EXCLUDED'), f['id'] + if f['status'].startswith('attained'): + assert f['N'] >= b, f['id'] + assert by['F12']['N'] == bound(8, 9) - 1 and by['F12']['status'].startswith('EXCLUDED') + print('PASS control c (F12 at bound - 1 is excluded; no attained family below the bound)') + print('PASS_MULTIPAIR_SCHEDULE_BOUND') + + +if __name__ == '__main__': + main()