diff --git a/research/t74-diagonal-window-bound/CERTIFICATE.json b/research/t74-diagonal-window-bound/CERTIFICATE.json new file mode 100644 index 0000000000..93c5e64167 --- /dev/null +++ b/research/t74-diagonal-window-bound/CERTIFICATE.json @@ -0,0 +1,1161 @@ +{ + "controls": { + "positive": [ + "all_rank8_windows_two_derivations", + "integer_shift_closed_form", + "stable_order_after_shift70", + "linear_square_root_constant_costs", + "predecessor_endpoint_not_rejected", + "window_free_primal_accepts_excluded_threshold" + ], + "rejected": [ + "changed_source_bytes", + "reversed_replica_stages", + "inclusive_pre_bridge_endpoint", + "omitted_source_bridge", + "duplicate_cut_group", + "overstated_defect_115", + "unbound_inventory_79", + "inflated_rank8_dual", + "inflated_defect_penalty", + "unbalanced_relaxed_primal" + ] + }, + "critical_groups": [ + [ + 0, + 1 + ], + [ + 1, + 1 + ], + [ + 2, + 1 + ], + [ + 3, + 1 + ], + [ + 4, + 1 + ], + [ + 5, + 1 + ], + [ + 6, + 1 + ], + [ + 7, + 1 + ], + [ + 8, + 1 + ], + [ + 9, + 1 + ], + [ + 10, + 1 + ], + [ + 11, + 1 + ], + [ + 12, + 1 + ], + [ + 13, + 1 + ], + [ + 14, + 1 + ], + [ + 15, + 1 + ], + [ + 16, + 1 + ], + [ + 17, + 1 + ], + [ + 18, + 1 + ], + [ + 19, + 1 + ], + [ + 20, + 1 + ], + [ + 21, + 1 + ], + [ + 22, + 1 + ], + [ + 23, + 1 + ], + [ + 24, + 1 + ], + [ + 0, + 3 + ], + [ + 1, + 3 + ], + [ + 2, + 3 + ], + [ + 3, + 3 + ], + [ + 4, + 3 + ], + [ + 5, + 3 + ], + [ + 6, + 3 + ], + [ + 7, + 3 + ], + [ + 8, + 3 + ], + [ + 9, + 3 + ], + [ + 10, + 3 + ], + [ + 11, + 3 + ], + [ + 12, + 3 + ], + [ + 13, + 3 + ], + [ + 14, + 3 + ], + [ + 15, + 3 + ], + [ + 16, + 3 + ], + [ + 17, + 3 + ], + [ + 18, + 3 + ], + [ + 19, + 3 + ], + [ + 20, + 3 + ], + [ + 21, + 3 + ], + [ + 22, + 3 + ], + [ + 23, + 3 + ], + [ + 24, + 3 + ], + [ + 0, + 5 + ], + [ + 1, + 5 + ], + [ + 2, + 5 + ], + [ + 3, + 5 + ], + [ + 4, + 5 + ], + [ + 5, + 5 + ], + [ + 6, + 5 + ], + [ + 7, + 5 + ], + [ + 8, + 5 + ], + [ + 9, + 5 + ], + [ + 10, + 5 + ], + [ + 11, + 5 + ], + [ + 12, + 5 + ], + [ + 13, + 5 + ], + [ + 14, + 5 + ], + [ + 15, + 5 + ], + [ + 16, + 5 + ], + [ + 0, + 7 + ], + [ + 1, + 7 + ], + [ + 2, + 7 + ], + [ + 3, + 7 + ], + [ + 4, + 7 + ], + [ + 5, + 7 + ], + [ + 6, + 7 + ], + [ + 7, + 7 + ], + [ + 8, + 7 + ], + [ + 9, + 7 + ], + [ + 10, + 7 + ], + [ + 11, + 7 + ], + [ + 12, + 7 + ], + [ + 13, + 7 + ], + [ + 14, + 7 + ], + [ + 15, + 7 + ], + [ + 16, + 7 + ], + [ + 0, + 9 + ], + [ + 1, + 9 + ], + [ + 2, + 9 + ], + [ + 3, + 9 + ], + [ + 4, + 9 + ], + [ + 5, + 9 + ], + [ + 6, + 9 + ], + [ + 7, + 9 + ], + [ + 8, + 9 + ], + [ + 0, + 11 + ], + [ + 1, + 11 + ], + [ + 2, + 11 + ], + [ + 3, + 11 + ], + [ + 4, + 11 + ], + [ + 5, + 11 + ], + [ + 6, + 11 + ], + [ + 7, + 11 + ], + [ + 8, + 11 + ] + ], + "minimum_defect": 114, + "model": { + "bins": [ + 49728, + 33152, + 33152, + 33152 + ], + "calls": 666, + "inventory": [ + 33, + 9, + 62, + 78, + 240 + ], + "live": 66304, + "local_profile": { + "1": 2369, + "2": 632, + "3": 320, + "4": 118, + "5": 26, + "7": 8 + }, + "replicas": 74, + "width": 73, + "widths": [ + 4, + 5, + 7, + 8, + 9 + ] + }, + "price": { + "bin_dual_repairs": [ + "0", + "0", + "0", + "0" + ], + "chronological_lower": "303823776028836913583490663046666239558496559206382671201055828727/4582284266832276957600126278941596483754719474458745194414080", + "defect": 114, + "dual": [ + "1005399011524958486083700157447767180951339208651448813510229/9164568533664553915200252557883192967509438948917490388828160", + "1005399011524958486083700157447767180951339208651448813510229/4582284266832276957600126278941596483754719474458745194414080", + "1005399011524958486083700157447767180951339208651448813510229/2291142133416138478800063139470798241877359737229372597207040", + "2355605427864450923593959136836610289253360240343553193435/3579909583462716373125098655423122252933374589420894683136", + "-12603320037611890457912212911904534777539094810874678496185/229114213341613847880006313947079824187735973722937259720704", + "-15765038135296846169421864119842240396235216933446527643415/229114213341613847880006313947079824187735973722937259720704", + "-440233258076965136490712479948203996292014515773459788792843/4582284266832276957600126278941596483754719474458745194414080", + "-1005399011524958486083700157447767180951339208651448813510229/9164568533664553915200252557883192967509438948917490388828160", + "-282582876723996674796493838749781592329662346438994512358693/2291142133416138478800063139470798241877359737229372597207040" + ], + "live": 66304, + "local_lower": "1380822945389815178370701474287299826912471732559468516633115429/28639276667701730985000789243384978023466996715367157465088", + "pattern_count": 1163, + "penalty_per_defect": "1536228536370015358110850766149036380534707798344729964657/9164568533664553915200252557883192967509438948917490388828160", + "strict_margin": "789622186771890247722626299623639171870029830624668407/4582284266832276957600126278941596483754719474458745194414080", + "threshold": "107132981/62500000000", + "window_free_lower": "151911844231905170246307625364086284531711434364019082775723921639/2291142133416138478800063139470798241877359737229372597207040", + "window_free_primal_counts": [ + "49728", + "33152", + "555", + "1110", + "3515", + "5994", + "21978", + "132793/5", + "32967/5" + ], + "window_free_primal_upper": "151911844231905170246307625364086284531711434364019082775748004199/2291142133416138478800063139470798241877359737229372597207040" + }, + "schema_version": 1, + "scope": "Fixed whole-helper inventory and uniform initial stage shifts only; no new kappa or supplier admission.", + "shift_cases": [ + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 6, + "last_call": 150, + "shift": 0, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 7, + "last_call": 151, + "shift": 1, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 8, + "last_call": 152, + "shift": 2, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 9, + "last_call": 153, + "shift": 3, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 10, + "last_call": 154, + "shift": 4, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 11, + "last_call": 155, + "shift": 5, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 12, + "last_call": 156, + "shift": 6, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 13, + "last_call": 157, + "shift": 7, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 14, + "last_call": 158, + "shift": 8, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 15, + "last_call": 159, + "shift": 9, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 16, + "last_call": 160, + "shift": 10, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 17, + "last_call": 161, + "shift": 11, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 18, + "last_call": 162, + "shift": 12, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 19, + "last_call": 163, + "shift": 13, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 20, + "last_call": 164, + "shift": 14, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 21, + "last_call": 165, + "shift": 15, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 22, + "last_call": 166, + "shift": 16, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 23, + "last_call": 167, + "shift": 17, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 24, + "last_call": 168, + "shift": 18, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 25, + "last_call": 169, + "shift": 19, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 26, + "last_call": 170, + "shift": 20, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 27, + "last_call": 171, + "shift": 21, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 28, + "last_call": 172, + "shift": 22, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 29, + "last_call": 173, + "shift": 23, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 30, + "last_call": 174, + "shift": 24, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 31, + "last_call": 175, + "shift": 25, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 32, + "last_call": 176, + "shift": 26, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 33, + "last_call": 177, + "shift": 27, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 34, + "last_call": 178, + "shift": 28, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 35, + "last_call": 179, + "shift": 29, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 36, + "last_call": 180, + "shift": 30, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 37, + "last_call": 181, + "shift": 31, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 38, + "last_call": 182, + "shift": 32, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 39, + "last_call": 183, + "shift": 33, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 40, + "last_call": 184, + "shift": 34, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 41, + "last_call": 185, + "shift": 35, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 42, + "last_call": 186, + "shift": 36, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 43, + "last_call": 187, + "shift": 37, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 44, + "last_call": 188, + "shift": 38, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 45, + "last_call": 189, + "shift": 39, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 46, + "last_call": 190, + "shift": 40, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 114, + "eligible_calls": 145, + "first_call": 47, + "last_call": 191, + "shift": 41, + "width8_supply": 11310 + }, + { + "bins": 11424, + "defect": 192, + "eligible_calls": 144, + "first_call": 48, + "last_call": 191, + "shift": 42, + "width8_supply": 11232 + }, + { + "bins": 11424, + "defect": 270, + "eligible_calls": 143, + "first_call": 49, + "last_call": 191, + "shift": 43, + "width8_supply": 11154 + }, + { + "bins": 11424, + "defect": 348, + "eligible_calls": 142, + "first_call": 50, + "last_call": 191, + "shift": 44, + "width8_supply": 11076 + }, + { + "bins": 11424, + "defect": 426, + "eligible_calls": 141, + "first_call": 51, + "last_call": 191, + "shift": 45, + "width8_supply": 10998 + }, + { + "bins": 11424, + "defect": 504, + "eligible_calls": 140, + "first_call": 52, + "last_call": 191, + "shift": 46, + "width8_supply": 10920 + }, + { + "bins": 11424, + "defect": 582, + "eligible_calls": 139, + "first_call": 53, + "last_call": 191, + "shift": 47, + "width8_supply": 10842 + }, + { + "bins": 11424, + "defect": 660, + "eligible_calls": 138, + "first_call": 54, + "last_call": 191, + "shift": 48, + "width8_supply": 10764 + }, + { + "bins": 11424, + "defect": 738, + "eligible_calls": 137, + "first_call": 55, + "last_call": 191, + "shift": 49, + "width8_supply": 10686 + }, + { + "bins": 11424, + "defect": 816, + "eligible_calls": 136, + "first_call": 56, + "last_call": 191, + "shift": 50, + "width8_supply": 10608 + }, + { + "bins": 11424, + "defect": 894, + "eligible_calls": 135, + "first_call": 57, + "last_call": 191, + "shift": 51, + "width8_supply": 10530 + }, + { + "bins": 11424, + "defect": 972, + "eligible_calls": 134, + "first_call": 58, + "last_call": 191, + "shift": 52, + "width8_supply": 10452 + }, + { + "bins": 11424, + "defect": 1050, + "eligible_calls": 133, + "first_call": 59, + "last_call": 191, + "shift": 53, + "width8_supply": 10374 + }, + { + "bins": 11424, + "defect": 1128, + "eligible_calls": 132, + "first_call": 60, + "last_call": 191, + "shift": 54, + "width8_supply": 10296 + }, + { + "bins": 11424, + "defect": 1206, + "eligible_calls": 131, + "first_call": 61, + "last_call": 191, + "shift": 55, + "width8_supply": 10218 + }, + { + "bins": 11424, + "defect": 1284, + "eligible_calls": 130, + "first_call": 62, + "last_call": 191, + "shift": 56, + "width8_supply": 10140 + }, + { + "bins": 11424, + "defect": 1362, + "eligible_calls": 129, + "first_call": 63, + "last_call": 191, + "shift": 57, + "width8_supply": 10062 + }, + { + "bins": 11424, + "defect": 1440, + "eligible_calls": 128, + "first_call": 64, + "last_call": 191, + "shift": 58, + "width8_supply": 9984 + }, + { + "bins": 11424, + "defect": 1518, + "eligible_calls": 127, + "first_call": 65, + "last_call": 191, + "shift": 59, + "width8_supply": 9906 + }, + { + "bins": 11424, + "defect": 1596, + "eligible_calls": 126, + "first_call": 66, + "last_call": 191, + "shift": 60, + "width8_supply": 9828 + }, + { + "bins": 11424, + "defect": 1674, + "eligible_calls": 125, + "first_call": 67, + "last_call": 191, + "shift": 61, + "width8_supply": 9750 + }, + { + "bins": 11424, + "defect": 1752, + "eligible_calls": 124, + "first_call": 68, + "last_call": 191, + "shift": 62, + "width8_supply": 9672 + }, + { + "bins": 11424, + "defect": 1830, + "eligible_calls": 123, + "first_call": 69, + "last_call": 191, + "shift": 63, + "width8_supply": 9594 + }, + { + "bins": 11424, + "defect": 1908, + "eligible_calls": 122, + "first_call": 70, + "last_call": 191, + "shift": 64, + "width8_supply": 9516 + }, + { + "bins": 11424, + "defect": 1986, + "eligible_calls": 121, + "first_call": 71, + "last_call": 191, + "shift": 65, + "width8_supply": 9438 + }, + { + "bins": 11424, + "defect": 2064, + "eligible_calls": 120, + "first_call": 72, + "last_call": 191, + "shift": 66, + "width8_supply": 9360 + }, + { + "bins": 11424, + "defect": 2142, + "eligible_calls": 119, + "first_call": 73, + "last_call": 191, + "shift": 67, + "width8_supply": 9282 + }, + { + "bins": 11424, + "defect": 2220, + "eligible_calls": 118, + "first_call": 74, + "last_call": 191, + "shift": 68, + "width8_supply": 9204 + }, + { + "bins": 11424, + "defect": 2298, + "eligible_calls": 117, + "first_call": 75, + "last_call": 191, + "shift": 69, + "width8_supply": 9126 + }, + { + "bins": 11424, + "defect": 2298, + "eligible_calls": 117, + "first_call": 75, + "last_call": 191, + "shift": 70, + "width8_supply": 9126 + } + ], + "source_sha256": { + "inputs/PR2435-TEMPLATE.json.gz": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "inputs/PR2530-ORDER.json": "e48b51a7d6a315971fff8b8e51748251750ff4ed8fe30b8b023de1a1a8019783", + "inputs/PR2530-PROVIDERS.json": "13d5abb0f5dccf32703a04334209d0d47516e985db4a51809a593538f45c1f45", + "inputs/PR2571-CLAIM.json": "a57f5f27c4fb250f4aabde29bbb738f16e05bd73940b381918de2eb928dbec65", + "inputs/PR2571-ORDER.json": "e3702fbcaff7491bbeca6b0a5a9301778a816fa69329761b09b013e289c71c2b" + }, + "status": "PASS_T74_DIAGONAL_WINDOW_BOUND", + "union_formula": "117 + max(0, min(28, 69-s)), for integer s >= 0" +} diff --git a/research/t74-diagonal-window-bound/INPUTS.json b/research/t74-diagonal-window-bound/INPUTS.json new file mode 100644 index 0000000000..153629a6c5 --- /dev/null +++ b/research/t74-diagonal-window-bound/INPUTS.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "inputs/PR2530-PROVIDERS.json", + "commit": "b4012098048e12500b2d33d2e84be281915a27ac", + "source_path": "research/source-partner-lifetimes/evidence/eight-providers.json", + "git_blob": "a678492aece195bf9b3e35a72cc518dd1e2ada31", + "sha256": "13d5abb0f5dccf32703a04334209d0d47516e985db4a51809a593538f45c1f45" + }, + { + "path": "inputs/PR2530-ORDER.json", + "commit": "b4012098048e12500b2d33d2e84be281915a27ac", + "source_path": "research/source-partner-lifetimes/evidence/eight-order.json", + "git_blob": "a7de9f93b6b95a4f8b0b65459e135cd73836a9dd", + "sha256": "e48b51a7d6a315971fff8b8e51748251750ff4ed8fe30b8b023de1a1a8019783" + }, + { + "path": "inputs/PR2571-ORDER.json", + "commit": "faff03cf5c29dadd6e0eb51e406efdc921bfa683", + "source_path": "research/source-partner-repack/evidence/repack-order.json", + "git_blob": "eebac3de3bd91def724db70a8a0dff6d58afc606", + "sha256": "e3702fbcaff7491bbeca6b0a5a9301778a816fa69329761b09b013e289c71c2b" + }, + { + "path": "inputs/PR2571-CLAIM.json", + "commit": "faff03cf5c29dadd6e0eb51e406efdc921bfa683", + "source_path": "research/source-partner-repack/CLAIM.json", + "git_blob": "359a2f186ca874a8424f325994cc95356b5dc0ae", + "sha256": "a57f5f27c4fb250f4aabde29bbb738f16e05bd73940b381918de2eb928dbec65" + }, + { + "path": "inputs/PR2435-TEMPLATE.json.gz", + "commit": "b4012098048e12500b2d33d2e84be281915a27ac", + "source_path": "research/t74-owner-consolidation/source-pr2435.tar.gz", + "archive_git_blob": "94878b26080479788d0870b4e536a2f2e111a996", + "archive_sha256": "f8937eabaa59667831f21ecbcb68eb163de02dd3154c5c51dd3f814a949ae0ff", + "member": "research/gmx-t74-borrow43-handoff/inputs/GLOBAL-TEMPLATE.json.gz", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "source_credit": "Jeremy Kothe, PR2435, retained by zxv in PR2530", + "archive_origin_pr": 2435, + "archive_origin_commit": "324d7d3590dc21003940a44cb0cbdc32b3620f25" + } + ] +} diff --git a/research/t74-diagonal-window-bound/README.md b/research/t74-diagonal-window-bound/README.md new file mode 100644 index 0000000000..9f41195329 --- /dev/null +++ b/research/t74-diagonal-window-bound/README.md @@ -0,0 +1,264 @@ +# A chronological packing bound for every uniform initial shift of the source-partner T74 schedule + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +**Scoped proof and exact finite certificate; no new κ.** For PR2530's fixed +422-helper words and the uniform initial-shift order family containing PR2571, +every legal whole-helper fill has complex primitive endpoint + +\[ + b < \boxed{0.001714127696}. +\] + +The source's window-free estimate is about 0.00171422836. The new bound comes +from an unavoidable shortage of width-eight roles in a named collection of +windows. It applies to **every nonnegative integer uniform shift**, including +the original order (`s=0`) and PR2571's shifted order (`s=4`). It does not claim +an attainable optimum, a better supplier, or a bound on other local words. + +The exact rational certificate is [CERTIFICATE.json](CERTIFICATE.json). +The code uses the standard library, exact rational arithmetic, explicit +logarithm/exponential remainder bounds, and no LP solver or predecessor checker. +Evidence is author-checked, with no independent human review claimed. + +## Statement and fixed inputs + +There are 74 replicas, 666 calls, 112 ports per idle-child group, ambient width +73 and 66,304 live families. The per-call helper inventory is +`{4:33, 5:9, 7:62, 8:78, 9:240}`, and the local paid profile in **both** providers +is `{1:2369, 2:632, 3:320, 4:118, 5:26, 7:8}`. There are respectively +49,728, 33,152, 33,152 and 33,152 bins of capacities 8, 16, 32 and 48. +The resulting rank mass is 4,816,512 and deficit 23,680, independently recounted +from these quantities. + +For integer `s >= 0`, sort calls `(stage, replica)` by + +``` +(4*stage + replica + s*[stage >= 1], stage, replica). +``` + +A helper occurrence must be placed whole into one bin inside its strict +source-event window. The bin's unused capacity contributes its remaining rank +to the global profile. These are necessary conditions of the physical +contract. The proof drops family, port-assignment and other admission +restrictions, so it applies to every fill satisfying the stronger contract. +Adding nonnegative charges cannot weaken this obstruction. + +Source pins and provenance are in [INPUTS.json](INPUTS.json): + +- PR2530, zxv, `b4012098048e12500b2d33d2e84be281915a27ac`: provider inventories, + paid profiles and original call order. +- PR2571, Rohan Arun, `faff03cf5c29dadd6e0eb51e406efdc921bfa683`: shifted call + order and comparison endpoint. Its actual README/build/order files use + `s=4`; this package binds the bytes, rather than the older PR description. +- The immutable PR2435 source archive (`324d7d3590dc21003940a44cb0cbdc32b3620f25`) retained by PR2530, from Jeremy Kothe's + supplier: its `inputs/GLOBAL-TEMPLATE.json.gz` supplies the 30-event recipe, + idle-child capacities and 112 ports. Its historical replica count and bank + stock are not substituted for the declared 74-replica, 66,304-live model. + Both container and extracted-member hashes are recorded. The raw member is + retained verbatim so no network access or historical archive unpacking is + needed during verification. + +The new work starts at main `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`. +The selected record is unchanged. The claim is in [discussion #2608](https://github.com/CrocSwap/integer-mult-bounds/discussions/2608). + +## 1. A cut forces 114 non-width-eight bins + +Take this fixed set of 102 rank-eight groups: + +| Idle children | Owner replicas, inclusive | Groups | +| --- | --- | ---: | +| 1, 3 | 0 through 24 | 50 | +| 5, 7 | 0 through 16 | 34 | +| 9, 11 | 0 through 8 | 18 | + +For children 1/3, a legal call is strictly after that replica's stage-1 +bridge and no later than its stage-2 call. For 5/7 replace stages 1/2 by 3/4; +for 9/11 use 5/6. The event interpreter reconstructs these strict windows and +a separate stage-position calculation checks all 444 rank-eight windows. + +The union of the 102 groups' eligible calls is the interval strictly after +call `(1,0)` through call `(6,8)`, inclusive. For each pair of children, +consecutive owner windows overlap: their opening keys increase by one while +the closing key is four larger. The three resulting intervals also overlap. +Their last closing keys all equal `32+s`, with stage 6 ordered last. + +Inside this union the counts from stages 1 through 8 are + +``` +28 + 25 + 21 + 17 + 13 + 9 + 4 + 0 = 117. +``` + +The stage-zero calls have replica indices from `s+5` through `s+32`, +intersected with `0..73`. Thus the number of eligible calls is exactly + +\[ + U_s=117+\max(0,\min(28,69-s))\le145. +\] + +Each eligible call supplies only 78 width-eight roles. Each of the 102 groups +has 112 distinct bins, and a rank-eight bin can contain at most one +width-eight role. Therefore at least + +\[ + 102\cdot112-145\cdot78 = \boxed{114} +\] + +of these bins must contain **no width-eight role**. The exact bound at shift +`s` is `11424 - 78*U_s`; it is 114 for `0 <= s <= 41` and only grows later. +For `s=0` the interval is call indices `[6,150]`; for `s=4` it is `[10,154]`. + +The checker enumerates shifts 0 through 70. For `s >= 70`, every stage-zero +key is smaller than every later-stage key, and later stages all receive the +same shift. The entire call order is consequently constant. This proves the +infinite tail; the large-shift replay is an additional control. + +This is **not a claim of 114 empty bins**. A bin without a width-eight role +may, for example, contain two width-four roles. Its cost is charged through +the full width-inventory dual below. + +## 2. Convert the cut into a complete moment lower bound + +Let `h_a(r)=(r/73)^(1-a)` for positive `r`, and `h_a(0)=0`. Enumerate every +whole-helper pattern `p=(R,n4,n5,n7,n8,n9)` with total width at most `R`. +There are exactly 1,163 patterns. Let `rem(p)` be the remaining capacity. +Find bin prices `y_R`, width prices `z_w`, and a positive `delta` such that + +\[ + y_R+\sum_w n_wz_w+ + \delta\,\mathbf1_{R=8,\ n_8=0}\le h_a(\operatorname{rem}(p)) +\] + +for **all** 1,163 patterns. Sum over all physical bins. All helper roles are +used exactly once, and the cut supplies at least 114 indicator terms. Hence + +\[ + 66304\,\mu(a)\ \ge\ + 666\sum_r P_rh_a(r)+\sum_R N_Ry_R+ + 666\sum_w I_wz_w+114\delta. +\] + +This includes the complete fixed local profile and every residual bin. +It does not infer a moment gain from scalar operation counts. + +A convenient dual nomination has `t=(h_a(3)-h_a(48))/5` and +`Y=h_a(5)-3t`, with + +``` +(y8,y16,y32,y48) = (Y/4,Y/2,Y,h_a(48)) +(z4,z5,z7,z8,z9) = (h_a(1)-h_a(5),-h_a(5),(t-h_a(5))/2,-Y/4,t). +``` + +The checker derives this both by exact elimination and by these formulas. +It then uses rational **lower** enclosures for the costs, repairs each bin +price downwards if needed, and checks every inequality. `delta` is the +smallest remaining slack of a rank-eight pattern without width eight; no +floating-point optimizer is trusted. Exact prices and repairs are saved in +the certificate. + +At `a=0.001714127696`, the following displayed decimals are only summaries +of the exact rational comparisons: + +| Certified quantity | Value, approximately | +| --- | ---: | +| Per-defect penalty `delta` | 0.000167626935270 | +| Window-free dual lower bill | 66303.9808907017 | +| Chronological lower bill | 66304.0000001723 | +| Strict excess above 66304 | 0.000000172320646 | + +Thus `mu(a)>1`. Every positive-rank cost is increasing in `a`, so no fill in +the stated family can have endpoint `b >= a`. + +The strengthening is genuine even against the window-free **fractional** +pattern LP. A separate exact feasible primal, on the nine patterns used in +the dual nomination, has counts + +``` +49728, 33152, 555, 1110, 3515, 5994, 21978, 132793/5, 32967/5. +``` + +The checker verifies all bin and width equations. Using **upper** cost +enclosures, its total bill is below 66304 at the excluded threshold. This +primal is an LP witness, not a physical fill. It violates the chronological +cut because every rank-eight bin uses a width-eight role. + +The pinned PR2571 complex endpoint is +`428508074646920477229/250000000000000000000000`. It is below the new cap by +less than `9.54e-8`, and the checker confirms that this bound does not reject +that endpoint. Its construction and native admission are not reverified here. + +## Reproduction and controls + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3 -B scripts/research_package.py --package research/t74-diagonal-window-bound +python3 -I -O -B research/t74-diagonal-window-bound/verify.py +``` + +Expected output includes: + +``` +PASS_T74_DIAGONAL_WINDOW_BOUND shifts=71+stable_tail groups=102 deficit>=114 patterns=1163 b<0.001714127696 controls=10 no_new_kappa +``` + +The default replay is read-only and compares every field of the regenerated +certificate, including JSON types. `--write-certificate` explicitly regenerates +it. Input pins check the retained bytes; direct Git-source inputs also carry +Git blob identities. + +Positive checks include the two window derivations, the closed-form union +count, the exact primal/dual equations, square-root/linear/constant identities +for the transcendental bounds, and non-rejection of the predecessor endpoint. +Ten failure controls reject changed source bytes, reversed replica stages, +an inclusive bridge endpoint, an omitted source bridge, a duplicate cut group, +a claimed defect of 115, unbound width-eight supply 79, an inflated bin dual, +an inflated defect penalty, and an unbalanced fractional primal. The checks +remain enabled under `python -O`. + +## Limits + +This is a lower bound for fixed whole-helper widths, the named source recipe, +fixed live stock and this order family. It neither constructs nor optimizes +a physical fill. Arbitrary nonuniform shifts, other interleavings, split +helper reservations, different stocks and changed local profiles are outside +its numerical theorem. In particular, PR2588 changes the local profile: its +claimed endpoint is not contradicted by this bound. The reusable 114-bin cut +can be repriced for a changed profile only after binding the new inputs. + +The provider profiles are pinned declared inputs, not an independent replay +of their scalar/native words. No complete cold supplier replay, physical +hosting admission, all-size/compiler proof, precision/exact-recovery audit, +outer transfer audit, bit-supplier audit, Lean proof, or full multiplication +theorem is claimed. + +## Open next questions + +- **Escape the cut with a nonuniform stage shift.** It matters because every + uniform initial delay retains the shortage. Start by giving the named 102 + groups at least 147 eligible calls, or deriving a different inventory-aware + cut if the groups change. This only removes this necessary obstruction; + any candidate still needs a fully charged fill and native/global admission. +- **Tighten the fixed-order bound with coupled width constraints.** Width-seven + shortages alone do not imply a positive reduced cost: a rank-16 bin can use + two width-eight roles at zero reduced cost. A feasible first step is to + couple that substitution to the rank-eight cut in one exact dual. The + blocker is a checked stronger inequality, not another moment root search. + +Structured versions of these questions are in [TASK.json](TASK.json). + +## Credit + +Rohan Arun's PR2571 supplies the shifted-order question; zxv's PR2530 supplies +the source-partner words, diagonal order, interval search and owner pipeline. +Jeremy Kothe's PR2435 and T74 supplier lineage supply the retained source +recipe. The window-free pattern-dual method is due to Ali Romman (PR1129), +Jeremy Diviney (PR2360), and Sagar Thakrar (PR2387/PR2442). This contribution +adds the named chronological cut, its uniform-shift formula, the strengthened +exact dual and a separately written standard-library checker. + +Jeremy Kothe/PR2575 and PR2588, Philippe Van Velzen/PR2559, Tekalign/PR2436, +Vlado Vojdanovski/PR2322, Cinna Davis/PR2226, and the retained supplier authors +are credited for the neighboring constructions and mechanisms. No such +construction is imported as a newly proved result. Retained input bytes keep +their repository Apache-2.0 provenance; the new work is also Apache-2.0. diff --git a/research/t74-diagonal-window-bound/SOURCES.json b/research/t74-diagonal-window-bound/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/t74-diagonal-window-bound/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/t74-diagonal-window-bound/TASK.json b/research/t74-diagonal-window-bound/TASK.json new file mode 100644 index 0000000000..89f0b7270d --- /dev/null +++ b/research/t74-diagonal-window-bound/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "selected-packing", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "selected-packing", + "question": "Is there a genuinely unsearched, explicitly bounded improvement to the selected packing?", + "starting_points": [ + "certificates/selected-result.json", + "research/heterogeneous-owner-assembly/README.md", + "research/complex-local-word-ceiling/README.md" + ], + "methods": [ + "Search a named unclaimed canonical candidate domain with a reproducible partition.", + "Prove a stronger scoped relaxation or exact optimum for one named residual subproblem." + ], + "acceptance_gate": "Check live PR overlap first, price both suppliers and distinguish a search best from an optimum. Report the word's packing cap from ceiling.ceiling() and the fraction of it realized; label packing gains as such.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Locate the selected packing source in the review and check live PRs for the same residual problem.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Define an unclaimed canonical domain and a favorable bound before starting a new search.", + "bottleneck_link": "An actual paid-profile gain can improve the frontier up to the other supplier cap.", + "allowed_variations": [ + "One bounded residual packing instance or exact relaxation.", + "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": [ + "Rerunning an existing search with only a different seed as a separate mathematical contribution." + ], + "overlap_terms": [ + "T16", + "owner exchange", + "packing" + ] + }, + "scope_status": "changed", + "actual_scope": "A chronology-aware packing bound for PR2571 and every nonnegative integer uniform initial shift of the unchanged PR2530 whole-helper inventory: a 102-group Hall cut, exact per-pattern cost dual, and strictly stronger ceiling than the window-free fractional pattern LP.", + "scope_change_reason": "The selected-packing card is refined from the historical selected T16 packing to the live explicit owner-order residual in PR2571, following PR2530. The fetched PR2571 order is shifted by four; the bounded extension covers its entire nonnegative integer uniform-shift family.", + "bottleneck_link": "A 114-bin width-eight shortage survives every uniform initial delay. Pricing it closes about 1e-7 of the primitive-endpoint relaxation gap and identifies nonuniform scheduling or a changed inventory as necessary to escape this cut.", + "budget_minutes": 60, + "stop_rule": "Stop after an exact strengthened bound with source binding, positive primal control and rejecting controls, or hand off a precise failed implication. No new supplier or kappa claim.", + "outcome": "completed", + "evidence": "README.md scoped proof; CERTIFICATE.json exact replay; INPUTS.json immutable predecessor pins; verify.py standard-library checker.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex (GPT-6 Astra) assistance in derivation, implementation, checking and writing. No independent human review is claimed.", + "open_questions": [ + { + "question": "Can a nonuniform stage shift escape the named 102-group cut while retaining a favorable complete bill?", + "why_it_matters": "Every nonnegative uniform initial shift has at least 114 bins without a width-eight role.", + "first_step": "Give these groups at least 147 eligible calls, then recheck all other window and inventory cuts before physical realization.", + "blocked_by": "A changed order, literal whole-helper fill and complete native/global admission." + }, + { + "question": "Can coupled width-seven and width-eight cut constraints strengthen the bound?", + "why_it_matters": "A width-seven shortage alone admits zero-reduced-cost substitution by two width-eight roles.", + "first_step": "Combine that substitution with the rank-eight availability inequality in one rational dual.", + "blocked_by": "An exact feasible stronger dual; this package does not claim a packing optimum." + } + ], + "seed": "2ab87a123c529f26e4178a126f56a586", + "track": "incumbent-optimization", + "scope_key": "ab5d8f0f0d19bbab8625", + "refined_scope_key": "PR2571/uniform-initial-shifts/102-group-window-cut/exact-pattern-dual", + "coordination_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2608", + "upstream_refresh": { + "checked_at_utc": "2026-10-15T16:29:48Z", + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "changes_since_base": "none; guidance, selected record and relevant sources unchanged", + "decision": "Continue the fixed-source scoped bound; no selected-frontier change." + } +} diff --git a/research/t74-diagonal-window-bound/VERIFY.json b/research/t74-diagonal-window-bound/VERIFY.json new file mode 100644 index 0000000000..f8eba2f218 --- /dev/null +++ b/research/t74-diagonal-window-bound/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact source pins, 71 orders and stable-tail proof interface, two window derivations, 1163 exact pattern inequalities, a feasible fractional primal, rational moment exclusion, and ten rejecting controls." + } + ] +} diff --git a/research/t74-diagonal-window-bound/inputs/PR2435-TEMPLATE.json.gz b/research/t74-diagonal-window-bound/inputs/PR2435-TEMPLATE.json.gz new file mode 100644 index 0000000000..114808c32b Binary files /dev/null and b/research/t74-diagonal-window-bound/inputs/PR2435-TEMPLATE.json.gz differ diff --git a/research/t74-diagonal-window-bound/inputs/PR2530-ORDER.json b/research/t74-diagonal-window-bound/inputs/PR2530-ORDER.json new file mode 100644 index 0000000000..a7de9f93b6 --- /dev/null +++ b/research/t74-diagonal-window-bound/inputs/PR2530-ORDER.json @@ -0,0 +1 @@ +[[0, 0], [0, 1], [0, 2], [0, 3], [0, 4], [1, 0], [0, 5], [1, 1], [0, 6], [1, 2], [0, 7], [1, 3], [0, 8], [1, 4], [2, 0], [0, 9], [1, 5], [2, 1], [0, 10], [1, 6], [2, 2], [0, 11], [1, 7], [2, 3], [0, 12], [1, 8], [2, 4], [3, 0], [0, 13], [1, 9], [2, 5], [3, 1], [0, 14], [1, 10], [2, 6], [3, 2], [0, 15], [1, 11], [2, 7], [3, 3], [0, 16], [1, 12], [2, 8], [3, 4], [4, 0], [0, 17], [1, 13], [2, 9], [3, 5], [4, 1], [0, 18], [1, 14], [2, 10], [3, 6], [4, 2], [0, 19], [1, 15], [2, 11], [3, 7], [4, 3], [0, 20], [1, 16], [2, 12], [3, 8], [4, 4], [5, 0], [0, 21], [1, 17], [2, 13], [3, 9], [4, 5], [5, 1], [0, 22], [1, 18], [2, 14], [3, 10], [4, 6], [5, 2], [0, 23], [1, 19], [2, 15], [3, 11], [4, 7], [5, 3], [0, 24], [1, 20], [2, 16], [3, 12], [4, 8], [5, 4], [6, 0], [0, 25], [1, 21], [2, 17], [3, 13], [4, 9], [5, 5], [6, 1], [0, 26], [1, 22], [2, 18], [3, 14], [4, 10], [5, 6], [6, 2], [0, 27], [1, 23], [2, 19], [3, 15], [4, 11], [5, 7], [6, 3], [0, 28], [1, 24], [2, 20], [3, 16], [4, 12], [5, 8], [6, 4], [7, 0], [0, 29], [1, 25], [2, 21], [3, 17], [4, 13], [5, 9], [6, 5], [7, 1], [0, 30], [1, 26], [2, 22], [3, 18], [4, 14], [5, 10], [6, 6], [7, 2], [0, 31], [1, 27], [2, 23], [3, 19], [4, 15], [5, 11], [6, 7], [7, 3], [0, 32], [1, 28], [2, 24], [3, 20], [4, 16], [5, 12], [6, 8], [7, 4], [8, 0], [0, 33], [1, 29], [2, 25], [3, 21], [4, 17], [5, 13], [6, 9], [7, 5], [8, 1], [0, 34], [1, 30], [2, 26], [3, 22], [4, 18], [5, 14], [6, 10], [7, 6], [8, 2], [0, 35], [1, 31], [2, 27], [3, 23], [4, 19], [5, 15], [6, 11], [7, 7], [8, 3], [0, 36], [1, 32], [2, 28], [3, 24], [4, 20], [5, 16], [6, 12], [7, 8], [8, 4], [0, 37], [1, 33], [2, 29], [3, 25], [4, 21], [5, 17], [6, 13], [7, 9], [8, 5], [0, 38], [1, 34], [2, 30], [3, 26], [4, 22], [5, 18], [6, 14], [7, 10], [8, 6], [0, 39], [1, 35], [2, 31], [3, 27], [4, 23], [5, 19], [6, 15], [7, 11], [8, 7], [0, 40], [1, 36], [2, 32], [3, 28], [4, 24], [5, 20], [6, 16], [7, 12], [8, 8], [0, 41], [1, 37], [2, 33], [3, 29], [4, 25], [5, 21], [6, 17], [7, 13], [8, 9], [0, 42], [1, 38], [2, 34], [3, 30], [4, 26], [5, 22], [6, 18], [7, 14], [8, 10], [0, 43], [1, 39], [2, 35], [3, 31], [4, 27], [5, 23], [6, 19], [7, 15], [8, 11], [0, 44], [1, 40], [2, 36], [3, 32], [4, 28], [5, 24], [6, 20], [7, 16], [8, 12], [0, 45], [1, 41], [2, 37], [3, 33], [4, 29], [5, 25], [6, 21], [7, 17], [8, 13], [0, 46], [1, 42], [2, 38], [3, 34], [4, 30], [5, 26], [6, 22], [7, 18], [8, 14], [0, 47], [1, 43], [2, 39], [3, 35], [4, 31], [5, 27], [6, 23], [7, 19], [8, 15], [0, 48], [1, 44], [2, 40], [3, 36], [4, 32], [5, 28], [6, 24], [7, 20], [8, 16], [0, 49], [1, 45], [2, 41], [3, 37], [4, 33], [5, 29], [6, 25], [7, 21], [8, 17], [0, 50], [1, 46], [2, 42], [3, 38], [4, 34], [5, 30], [6, 26], [7, 22], [8, 18], [0, 51], [1, 47], [2, 43], [3, 39], [4, 35], [5, 31], [6, 27], [7, 23], [8, 19], [0, 52], [1, 48], [2, 44], [3, 40], [4, 36], [5, 32], [6, 28], [7, 24], [8, 20], [0, 53], [1, 49], [2, 45], [3, 41], [4, 37], [5, 33], [6, 29], [7, 25], [8, 21], [0, 54], [1, 50], [2, 46], [3, 42], [4, 38], [5, 34], [6, 30], [7, 26], [8, 22], [0, 55], [1, 51], [2, 47], [3, 43], [4, 39], [5, 35], [6, 31], [7, 27], [8, 23], [0, 56], [1, 52], [2, 48], [3, 44], [4, 40], [5, 36], [6, 32], [7, 28], [8, 24], [0, 57], [1, 53], [2, 49], [3, 45], [4, 41], [5, 37], [6, 33], [7, 29], [8, 25], [0, 58], [1, 54], [2, 50], [3, 46], [4, 42], [5, 38], [6, 34], [7, 30], [8, 26], [0, 59], [1, 55], [2, 51], [3, 47], [4, 43], [5, 39], [6, 35], [7, 31], [8, 27], [0, 60], [1, 56], [2, 52], [3, 48], [4, 44], [5, 40], [6, 36], [7, 32], [8, 28], [0, 61], [1, 57], [2, 53], [3, 49], [4, 45], [5, 41], [6, 37], [7, 33], [8, 29], [0, 62], [1, 58], [2, 54], [3, 50], [4, 46], [5, 42], [6, 38], [7, 34], [8, 30], [0, 63], [1, 59], [2, 55], [3, 51], [4, 47], [5, 43], [6, 39], [7, 35], [8, 31], [0, 64], [1, 60], [2, 56], [3, 52], [4, 48], [5, 44], [6, 40], [7, 36], [8, 32], [0, 65], [1, 61], [2, 57], [3, 53], [4, 49], [5, 45], [6, 41], [7, 37], [8, 33], [0, 66], [1, 62], [2, 58], [3, 54], [4, 50], [5, 46], [6, 42], [7, 38], [8, 34], [0, 67], [1, 63], [2, 59], [3, 55], [4, 51], [5, 47], [6, 43], [7, 39], [8, 35], [0, 68], [1, 64], [2, 60], [3, 56], [4, 52], [5, 48], [6, 44], [7, 40], [8, 36], [0, 69], [1, 65], [2, 61], [3, 57], [4, 53], [5, 49], [6, 45], [7, 41], [8, 37], [0, 70], [1, 66], [2, 62], [3, 58], [4, 54], [5, 50], [6, 46], [7, 42], [8, 38], [0, 71], [1, 67], [2, 63], [3, 59], [4, 55], [5, 51], [6, 47], [7, 43], [8, 39], [0, 72], [1, 68], [2, 64], [3, 60], [4, 56], [5, 52], [6, 48], [7, 44], [8, 40], [0, 73], [1, 69], [2, 65], [3, 61], [4, 57], [5, 53], [6, 49], [7, 45], [8, 41], [1, 70], [2, 66], [3, 62], [4, 58], [5, 54], [6, 50], [7, 46], [8, 42], [1, 71], [2, 67], [3, 63], [4, 59], [5, 55], [6, 51], [7, 47], [8, 43], [1, 72], [2, 68], [3, 64], [4, 60], [5, 56], [6, 52], [7, 48], [8, 44], [1, 73], [2, 69], [3, 65], [4, 61], [5, 57], [6, 53], [7, 49], [8, 45], [2, 70], [3, 66], [4, 62], [5, 58], [6, 54], [7, 50], [8, 46], [2, 71], [3, 67], [4, 63], [5, 59], [6, 55], [7, 51], [8, 47], [2, 72], [3, 68], [4, 64], [5, 60], [6, 56], [7, 52], [8, 48], [2, 73], [3, 69], [4, 65], [5, 61], [6, 57], [7, 53], [8, 49], [3, 70], [4, 66], [5, 62], [6, 58], [7, 54], [8, 50], [3, 71], [4, 67], [5, 63], [6, 59], [7, 55], [8, 51], [3, 72], [4, 68], [5, 64], [6, 60], [7, 56], [8, 52], [3, 73], [4, 69], [5, 65], [6, 61], [7, 57], [8, 53], [4, 70], [5, 66], [6, 62], [7, 58], [8, 54], [4, 71], [5, 67], [6, 63], [7, 59], [8, 55], [4, 72], [5, 68], [6, 64], [7, 60], [8, 56], [4, 73], [5, 69], [6, 65], [7, 61], [8, 57], [5, 70], [6, 66], [7, 62], [8, 58], [5, 71], [6, 67], [7, 63], [8, 59], [5, 72], [6, 68], [7, 64], [8, 60], [5, 73], [6, 69], [7, 65], [8, 61], [6, 70], [7, 66], [8, 62], [6, 71], [7, 67], [8, 63], [6, 72], [7, 68], [8, 64], [6, 73], [7, 69], [8, 65], [7, 70], [8, 66], [7, 71], [8, 67], [7, 72], [8, 68], [7, 73], [8, 69], [8, 70], [8, 71], [8, 72], [8, 73]] \ No newline at end of file diff --git a/research/t74-diagonal-window-bound/inputs/PR2530-PROVIDERS.json b/research/t74-diagonal-window-bound/inputs/PR2530-PROVIDERS.json new file mode 100644 index 0000000000..a678492aec --- /dev/null +++ b/research/t74-diagonal-window-bound/inputs/PR2530-PROVIDERS.json @@ -0,0 +1 @@ +{"gauge44": {"widths": [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 8, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 8, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 8, 8, 7, 7, 7, 7, 9, 9, 9, 9, 9, 9, 7, 7, 7, 7, 7, 7, 9, 9, 9, 9, 9, 9, 8, 8, 8, 9, 8, 8, 9, 9, 9, 9, 8, 9, 7, 7, 8, 9, 8, 8, 9, 9, 9, 9, 8, 9, 8, 8, 7, 7, 7, 7, 7, 7, 7, 7, 9, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 7, 8, 8, 9, 9, 9, 9, 8, 8, 8, 8, 7, 7, 7, 7, 9, 8, 9, 8, 8, 8, 8, 8, 7, 7, 9, 8, 9, 8, 7, 7, 7, 7, 8, 8, 8, 8, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8, 8, 5, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 5, 8, 5, 5, 5, 8, 8, 4, 8, 8, 8, 5, 8, 5, 5, 5, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8], "actual_paid_profile": {"1": 2369, "2": 632, "3": 320, "4": 118, "5": 26, "7": 8}}, "extra": {"widths": [9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 8, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 8, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 4, 9, 4, 9, 4, 9, 9, 9, 9, 4, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 7, 7, 7, 7, 7, 7, 7, 7, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 9, 8, 8, 7, 7, 7, 7, 9, 9, 9, 9, 9, 9, 7, 7, 7, 7, 7, 7, 9, 9, 9, 9, 9, 9, 8, 8, 8, 9, 8, 8, 9, 9, 9, 9, 8, 9, 7, 7, 8, 9, 8, 8, 9, 9, 9, 9, 8, 9, 8, 8, 7, 7, 7, 7, 7, 7, 7, 7, 9, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 9, 7, 8, 8, 9, 9, 9, 9, 8, 8, 8, 8, 7, 7, 7, 7, 9, 8, 9, 8, 8, 8, 8, 8, 7, 7, 9, 8, 9, 8, 7, 7, 7, 7, 8, 8, 8, 8, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 7, 8, 8, 8, 8, 8, 8, 8, 8, 5, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 5, 8, 5, 5, 5, 8, 8, 4, 8, 8, 8, 5, 8, 5, 5, 5, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8, 8], "actual_paid_profile": {"1": 2369, "2": 632, "3": 320, "4": 118, "5": 26, "7": 8}}} \ No newline at end of file diff --git a/research/t74-diagonal-window-bound/inputs/PR2571-CLAIM.json b/research/t74-diagonal-window-bound/inputs/PR2571-CLAIM.json new file mode 100644 index 0000000000..359a2f186c --- /dev/null +++ b/research/t74-diagonal-window-bound/inputs/PR2571-CLAIM.json @@ -0,0 +1,11 @@ +{ + "status": "CONDITIONAL_FINITE_CONSTRUCTION_AND_EXACT_OUTER", + "kappa": "17140322985876819089159999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "kappa_decimal": "0.0017140322985876819089159999999999999999999998999999999999999999999999", + "complex_lower": "428508074646920477229/250000000000000000000000", + "comparison_pr": 2530, + "comparison_kappa": "17137379215475043467519999999999999999999998999999999999999999999999/10000000000000000000000000000000000000000000000000000000000000000000000", + "gain_over_pr2530": "73594260044390541/250000000000000000000000", + "gain_over_pr2530_decimal": "2.94377040177562164E-7", + "scope": "Conditional finite construction; inherited unresolved multiplication-theorem obligations remain. Only the owner fill of PR2530 changes. No independent human review. Selected frontier unchanged." +} diff --git a/research/t74-diagonal-window-bound/inputs/PR2571-ORDER.json b/research/t74-diagonal-window-bound/inputs/PR2571-ORDER.json new file mode 100644 index 0000000000..eebac3de3b --- /dev/null +++ b/research/t74-diagonal-window-bound/inputs/PR2571-ORDER.json @@ -0,0 +1 @@ +[[0, 0], [0, 1], [0, 2], [0, 3], [0, 4], [0, 5], [0, 6], [0, 7], [0, 8], [1, 0], [0, 9], [1, 1], [0, 10], [1, 2], [0, 11], [1, 3], [0, 12], [1, 4], [2, 0], [0, 13], [1, 5], [2, 1], [0, 14], [1, 6], [2, 2], [0, 15], [1, 7], [2, 3], [0, 16], [1, 8], [2, 4], [3, 0], [0, 17], [1, 9], [2, 5], [3, 1], [0, 18], [1, 10], [2, 6], [3, 2], [0, 19], [1, 11], [2, 7], [3, 3], [0, 20], [1, 12], [2, 8], [3, 4], [4, 0], [0, 21], [1, 13], [2, 9], [3, 5], [4, 1], [0, 22], [1, 14], [2, 10], [3, 6], [4, 2], [0, 23], [1, 15], [2, 11], [3, 7], [4, 3], [0, 24], [1, 16], [2, 12], [3, 8], [4, 4], [5, 0], [0, 25], [1, 17], [2, 13], [3, 9], [4, 5], [5, 1], [0, 26], [1, 18], [2, 14], [3, 10], [4, 6], [5, 2], [0, 27], [1, 19], [2, 15], [3, 11], [4, 7], [5, 3], [0, 28], [1, 20], [2, 16], [3, 12], [4, 8], [5, 4], [6, 0], [0, 29], [1, 21], [2, 17], [3, 13], [4, 9], [5, 5], [6, 1], [0, 30], [1, 22], [2, 18], [3, 14], [4, 10], [5, 6], [6, 2], [0, 31], [1, 23], [2, 19], [3, 15], [4, 11], [5, 7], [6, 3], [0, 32], [1, 24], [2, 20], [3, 16], [4, 12], [5, 8], [6, 4], [7, 0], [0, 33], [1, 25], [2, 21], [3, 17], [4, 13], [5, 9], [6, 5], [7, 1], [0, 34], [1, 26], [2, 22], [3, 18], [4, 14], [5, 10], [6, 6], [7, 2], [0, 35], [1, 27], [2, 23], [3, 19], [4, 15], [5, 11], [6, 7], [7, 3], [0, 36], [1, 28], [2, 24], [3, 20], [4, 16], [5, 12], [6, 8], [7, 4], [8, 0], [0, 37], [1, 29], [2, 25], [3, 21], [4, 17], [5, 13], [6, 9], [7, 5], [8, 1], [0, 38], [1, 30], [2, 26], [3, 22], [4, 18], [5, 14], [6, 10], [7, 6], [8, 2], [0, 39], [1, 31], [2, 27], [3, 23], [4, 19], [5, 15], [6, 11], [7, 7], [8, 3], [0, 40], [1, 32], [2, 28], [3, 24], [4, 20], [5, 16], [6, 12], [7, 8], [8, 4], [0, 41], [1, 33], [2, 29], [3, 25], [4, 21], [5, 17], [6, 13], [7, 9], [8, 5], [0, 42], [1, 34], [2, 30], [3, 26], [4, 22], [5, 18], [6, 14], [7, 10], [8, 6], [0, 43], [1, 35], [2, 31], [3, 27], [4, 23], [5, 19], [6, 15], [7, 11], [8, 7], [0, 44], [1, 36], [2, 32], [3, 28], [4, 24], [5, 20], [6, 16], [7, 12], [8, 8], [0, 45], [1, 37], [2, 33], [3, 29], [4, 25], [5, 21], [6, 17], [7, 13], [8, 9], [0, 46], [1, 38], [2, 34], [3, 30], [4, 26], [5, 22], [6, 18], [7, 14], [8, 10], [0, 47], [1, 39], [2, 35], [3, 31], [4, 27], [5, 23], [6, 19], [7, 15], [8, 11], [0, 48], [1, 40], [2, 36], [3, 32], [4, 28], [5, 24], [6, 20], [7, 16], [8, 12], [0, 49], [1, 41], [2, 37], [3, 33], [4, 29], [5, 25], [6, 21], [7, 17], [8, 13], [0, 50], [1, 42], [2, 38], [3, 34], [4, 30], [5, 26], [6, 22], [7, 18], [8, 14], [0, 51], [1, 43], [2, 39], [3, 35], [4, 31], [5, 27], [6, 23], [7, 19], [8, 15], [0, 52], [1, 44], [2, 40], [3, 36], [4, 32], [5, 28], [6, 24], [7, 20], [8, 16], [0, 53], [1, 45], [2, 41], [3, 37], [4, 33], [5, 29], [6, 25], [7, 21], [8, 17], [0, 54], [1, 46], [2, 42], [3, 38], [4, 34], [5, 30], [6, 26], [7, 22], [8, 18], [0, 55], [1, 47], [2, 43], [3, 39], [4, 35], [5, 31], [6, 27], [7, 23], [8, 19], [0, 56], [1, 48], [2, 44], [3, 40], [4, 36], [5, 32], [6, 28], [7, 24], [8, 20], [0, 57], [1, 49], [2, 45], [3, 41], [4, 37], [5, 33], [6, 29], [7, 25], [8, 21], [0, 58], [1, 50], [2, 46], [3, 42], [4, 38], [5, 34], [6, 30], [7, 26], [8, 22], [0, 59], [1, 51], [2, 47], [3, 43], [4, 39], [5, 35], [6, 31], [7, 27], [8, 23], [0, 60], [1, 52], [2, 48], [3, 44], [4, 40], [5, 36], [6, 32], [7, 28], [8, 24], [0, 61], [1, 53], [2, 49], [3, 45], [4, 41], [5, 37], [6, 33], [7, 29], [8, 25], [0, 62], [1, 54], [2, 50], [3, 46], [4, 42], [5, 38], [6, 34], [7, 30], [8, 26], [0, 63], [1, 55], [2, 51], [3, 47], [4, 43], [5, 39], [6, 35], [7, 31], [8, 27], [0, 64], [1, 56], [2, 52], [3, 48], [4, 44], [5, 40], [6, 36], [7, 32], [8, 28], [0, 65], [1, 57], [2, 53], [3, 49], [4, 45], [5, 41], [6, 37], [7, 33], [8, 29], [0, 66], [1, 58], [2, 54], [3, 50], [4, 46], [5, 42], [6, 38], [7, 34], [8, 30], [0, 67], [1, 59], [2, 55], [3, 51], [4, 47], [5, 43], [6, 39], [7, 35], [8, 31], [0, 68], [1, 60], [2, 56], [3, 52], [4, 48], [5, 44], [6, 40], [7, 36], [8, 32], [0, 69], [1, 61], [2, 57], [3, 53], [4, 49], [5, 45], [6, 41], [7, 37], [8, 33], [0, 70], [1, 62], [2, 58], [3, 54], [4, 50], [5, 46], [6, 42], [7, 38], [8, 34], [0, 71], [1, 63], [2, 59], [3, 55], [4, 51], [5, 47], [6, 43], [7, 39], [8, 35], [0, 72], [1, 64], [2, 60], [3, 56], [4, 52], [5, 48], [6, 44], [7, 40], [8, 36], [0, 73], [1, 65], [2, 61], [3, 57], [4, 53], [5, 49], [6, 45], [7, 41], [8, 37], [1, 66], [2, 62], [3, 58], [4, 54], [5, 50], [6, 46], [7, 42], [8, 38], [1, 67], [2, 63], [3, 59], [4, 55], [5, 51], [6, 47], [7, 43], [8, 39], [1, 68], [2, 64], [3, 60], [4, 56], [5, 52], [6, 48], [7, 44], [8, 40], [1, 69], [2, 65], [3, 61], [4, 57], [5, 53], [6, 49], [7, 45], [8, 41], [1, 70], [2, 66], [3, 62], [4, 58], [5, 54], [6, 50], [7, 46], [8, 42], [1, 71], [2, 67], [3, 63], [4, 59], [5, 55], [6, 51], [7, 47], [8, 43], [1, 72], [2, 68], [3, 64], [4, 60], [5, 56], [6, 52], [7, 48], [8, 44], [1, 73], [2, 69], [3, 65], [4, 61], [5, 57], [6, 53], [7, 49], [8, 45], [2, 70], [3, 66], [4, 62], [5, 58], [6, 54], [7, 50], [8, 46], [2, 71], [3, 67], [4, 63], [5, 59], [6, 55], [7, 51], [8, 47], [2, 72], [3, 68], [4, 64], [5, 60], [6, 56], [7, 52], [8, 48], [2, 73], [3, 69], [4, 65], [5, 61], [6, 57], [7, 53], [8, 49], [3, 70], [4, 66], [5, 62], [6, 58], [7, 54], [8, 50], [3, 71], [4, 67], [5, 63], [6, 59], [7, 55], [8, 51], [3, 72], [4, 68], [5, 64], [6, 60], [7, 56], [8, 52], [3, 73], [4, 69], [5, 65], [6, 61], [7, 57], [8, 53], [4, 70], [5, 66], [6, 62], [7, 58], [8, 54], [4, 71], [5, 67], [6, 63], [7, 59], [8, 55], [4, 72], [5, 68], [6, 64], [7, 60], [8, 56], [4, 73], [5, 69], [6, 65], [7, 61], [8, 57], [5, 70], [6, 66], [7, 62], [8, 58], [5, 71], [6, 67], [7, 63], [8, 59], [5, 72], [6, 68], [7, 64], [8, 60], [5, 73], [6, 69], [7, 65], [8, 61], [6, 70], [7, 66], [8, 62], [6, 71], [7, 67], [8, 63], [6, 72], [7, 68], [8, 64], [6, 73], [7, 69], [8, 65], [7, 70], [8, 66], [7, 71], [8, 67], [7, 72], [8, 68], [7, 73], [8, 69], [8, 70], [8, 71], [8, 72], [8, 73]] \ No newline at end of file diff --git a/research/t74-diagonal-window-bound/verify.py b/research/t74-diagonal-window-bound/verify.py new file mode 100644 index 0000000000..619fc449cb --- /dev/null +++ b/research/t74-diagonal-window-bound/verify.py @@ -0,0 +1,430 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact chronological packing obstruction; standard library, read-only by default. + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +The pattern relaxation credits Ali Romman (#1129), Jeremy Diviney (#2360), +and Sagar Thakrar (#2387/#2442). No predecessor checker is imported. +""" +import argparse +from bisect import bisect_left, bisect_right +from collections import Counter +import copy +from fractions import Fraction as F +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +WIDTHS = (4, 5, 7, 8, 9) +RANKS = (8, 16, 32, 48) +INVENTORY = (33, 9, 62, 78, 240) +BINS = (49728, 33152, 33152, 33152) +LOCAL = {1: 2369, 2: 632, 3: 320, 4: 118, 5: 26, 7: 8} +REPLICAS, CALLS, PORTS, M, LIVE = 74, 666, 112, 73, 66304 +THRESHOLD = F('0.001714127696') +DYADIC = 1 << 192 +CRITICAL = tuple((replica, child) + for children, last in (((1, 3), 24), ((5, 7), 16), ((9, 11), 8)) + for child in children for replica in range(last + 1)) +SUPPORT = ((8, (0, 0, 0, 1, 0)), (16, (0, 0, 1, 0, 1)), + (32, (0, 0, 0, 0, 3)), (32, (0, 0, 1, 2, 1)), + (32, (0, 0, 2, 0, 2)), (32, (0, 1, 0, 0, 3)), + (32, (1, 0, 0, 0, 3)), (48, (0, 0, 0, 0, 0)), + (48, (0, 0, 0, 0, 5))) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, indent=2, sort_keys=True) + '\n' + + +def authenticate(data, pin): + need(hashlib.sha256(data).hexdigest() == pin['sha256'], 'input SHA256 mismatch') + if 'git_blob' in pin: + blob = hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + need(blob == pin['git_blob'], 'input Git blob mismatch') + + +def load_inputs(): + manifest = json.loads((HERE / 'INPUTS.json').read_text()) + out = {} + for pin in manifest['files']: + path = Path(pin['path']) + need(path.parts[0] == 'inputs' and len(path.parts) == 2, 'input path shape') + need(path.name not in out, 'duplicate input') + data = (HERE / path).read_bytes() + authenticate(data, pin) + out[path.name] = json.loads(gzip.decompress(data) if path.suffix == '.gz' else data) + need(set(out) == {'PR2435-TEMPLATE.json.gz', 'PR2530-PROVIDERS.json', + 'PR2530-ORDER.json', 'PR2571-ORDER.json', 'PR2571-CLAIM.json'}, + 'complete input set') + return out, manifest + + +def source_context(parent): + need(parent['m'] == M, 'source ambient width') + ports = parent['port_restriction']['new_to_old'] + need(len(ports) == len(set(ports)) == PORTS, '112 source ports') + need(Counter(c['child'] for c in parent['idle_children']) == + {child: PORTS for child in range(18)}, 'source child multiplicities') + ranks = {} + for child in parent['idle_children']: + key, rank = child['child'], child['rank'] + need(key not in ranks or ranks[key] == rank, 'replica child-rank disagreement') + ranks[key] = rank + need(set(ranks) == set(range(18)), 'idle child set') + need(Counter(ranks.values()) == {8: 6, 16: 4, 32: 4, 48: 4}, 'bin inventory') + need(tuple(REPLICAS * PORTS * Counter(ranks.values())[r] for r in RANKS) == BINS, + 'physical bin counts') + pairs = {e['stage']: e['pair'] for e in parent['recipe'] if e['kind'] == 'local'} + need(pairs == {0: 0, 1: 0, 2: 0, 3: 1, 4: 1, 5: 2, 6: 2, 7: 3, 8: 3}, + 'source stage pairs') + blocks, stage, source_index = {}, None, 0 + for event in parent['execution_schedule']: + if event['kind'] in ('bank_padding_cover_sweep', 'translate_every_live_family'): + continue + if event['kind'] == 'local_cover_sweep': + stage = event['stage'] + need(stage not in blocks, 'duplicate stage') + blocks[stage] = [] + need(stage is not None, 'event before first call') + blocks[stage].append((source_index, event)) + source_index += 1 + need(set(blocks) == set(range(9)) and source_index == 30, 'thirty-event source') + return ranks, pairs, blocks + + +def diagonal_order(shift): + need(type(shift) is int and shift >= 0, 'nonnegative integer shift') + return sorted(((stage, replica) for stage in range(9) for replica in range(REPLICAS)), + key=lambda c: (4*c[0] + c[1] + shift*(c[0] >= 1), c[0], c[1])) + + +def event_windows(order, context): + """Rebuild strict windows from the original bridge-aware source events.""" + ranks, pairs, blocks = context + need(len(order) == CALLS and set(order) == set(diagonal_order(0)), 'call permutation') + for replica in range(REPLICAS): + need([s for s, r in order if r == replica] == list(range(9)), 'replica stage order') + last, intervals, call_positions, projection = {}, {}, [], [[] for _ in range(REPLICAS)] + position = 0 + for stage, replica in order: + for source_index, event in blocks[stage]: + projection[replica].append(source_index) + kind = event['kind'] + if kind == 'local_cover_sweep': + call_positions.append(position) + last[replica, pairs[stage]] = position + elif kind == 'bridge': + last[replica, event['src']] = last[replica, event['dst']] = position + elif kind == 'idle_cover_sweep': + for child in event['child_indices']: + if child in ranks: + key = replica, child + need(key not in intervals, 'duplicate idle window') + intervals[key] = last.get((replica, event['pair']), -1), position + position += 1 + need(all(p == list(range(30)) for p in projection), 'per-replica event projection') + need(len(intervals) == 1332 and len(call_positions) == CALLS, 'window count') + return {key: tuple(range(bisect_right(call_positions, lo), bisect_left(call_positions, hi))) + for key, (lo, hi) in intervals.items()} + + +def direct_rank8_windows(order): + """Independent stage-position derivation for all 444 rank-eight windows.""" + at = {call: index for index, call in enumerate(order)} + return {(replica, child): tuple(range(at[stage, replica] + 1, at[stage + 1, replica] + 1)) + for stage, children in ((1, (1, 3)), (3, (5, 7)), (5, (9, 11))) + for child in children for replica in range(REPLICAS)} + + +def compare_windows(order, windows): + for key, direct in direct_rank8_windows(order).items(): + need(windows[key] == direct, 'independent window derivations disagree') + + +def cut(windows, groups=CRITICAL, width8_supply=78): + need(len(groups) == len(set(groups)) == 102, '102 distinct cut groups') + need(all(child in (1, 3, 5, 7, 9, 11) for _, child in groups), 'rank-eight cut groups') + times = set(t for group in groups for t in windows[group]) + need(bool(times) and times == set(range(min(times), max(times) + 1)), 'contiguous cut union') + demand, supply = len(groups) * PORTS, len(times) * width8_supply + return dict(first_call=min(times), last_call=max(times), eligible_calls=len(times), + bins=demand, width8_supply=supply, defect=max(0, demand - supply)) + + +def check_chronology(context, source): + need([list(c) for c in diagonal_order(0)] == source['PR2530-ORDER.json'], 'PR2530 order binding') + need([list(c) for c in diagonal_order(4)] == source['PR2571-ORDER.json'], 'PR2571 order binding') + cases = [] + for shift in range(71): + order = diagonal_order(shift) + windows = event_windows(order, context) + compare_windows(order, windows) + result = cut(windows) + # 117 calls from stages 1..8; at most 28 stage-zero calls intervene. + expected = 117 + max(0, min(28, 69 - shift)) + need(result['eligible_calls'] == expected, 'closed-form union size') + need(result['defect'] >= 114, 'universal 114-bin defect') + cases.append(dict(shift=shift, **result)) + need(diagonal_order(70) == diagonal_order(71) == diagonal_order(10**6), 'stable terminal order') + need(cases[0]['first_call'] == 6 and cases[0]['last_call'] == 150, 'original cut endpoints') + need(cases[4]['first_call'] == 10 and cases[4]['last_call'] == 154, 'shifted cut endpoints') + return cases + + +def dyadic_lower(x): + return F((x.numerator * DYADIC) // x.denominator, DYADIC) + + +def dyadic_upper(x): + return -dyadic_lower(-x) + + +@lru_cache(maxsize=None) +def log_bounds(x): + """Atanh series, range reduction, explicit positive tail; exact rationals.""" + need(x >= 1, 'log domain') + k = 0 + while x >= 2: + x /= 2 + k += 1 + + def series(v): + z = (v - 1) / (v + 1) + total, power = F(0), z + for j in range(64): + total += 2 * power / (2*j + 1) + power *= z*z + tail = 2 * power / (129 * (1 - z*z)) + return total, total + tail + + lo, hi = series(x) + lo2, hi2 = series(F(2)) + return dyadic_lower(lo + k*lo2), dyadic_upper(hi + k*hi2) + + +def exp_bounds(lo, hi): + need(0 <= lo <= hi < 5, 'exponential domain') + + def polynomial(x): + term = total = F(1) + for j in range(1, 65): + term = term*x/j + total += term + next_term = term*x/65 + return total, total + next_term/(1 - x/66) + + lower, _ = polynomial(lo) + _, upper = polynomial(hi) + return dyadic_lower(lower), dyadic_upper(upper) + + +@lru_cache(maxsize=None) +def h_bounds(rank, a): + need(0 <= rank <= M and 0 <= a <= 1, 'moment domain') + if rank == 0: + return F(0), F(0) + lo, hi = log_bounds(F(M, rank)) + el, eu = exp_bounds(a*lo, a*hi) + return F(rank, M)*el, F(rank, M)*eu + + +def patterns(): + out = [] + for rank in RANKS: + def visit(i, remainder, counts): + if i == len(WIDTHS): + out.append((rank, tuple(counts), remainder)) + return + for n in range(remainder // WIDTHS[i] + 1): + visit(i + 1, remainder - n*WIDTHS[i], counts + [n]) + visit(0, rank, []) + need(len(out) == 1163 and len(set(out)) == 1163, 'complete pattern enumeration') + return out + + +def solve(matrix, rhs): + """Exact Gaussian elimination; used only to propose a subsequently checked dual.""" + n = len(rhs) + rows = [[F(v) for v in row] + [rhs[i]] for i, row in enumerate(matrix)] + for j in range(n): + pivot = next(i for i in range(j, n) if rows[i][j]) + rows[j], rows[pivot] = rows[pivot], rows[j] + d = rows[j][j] + rows[j] = [x/d for x in rows[j]] + for i in range(n): + if i != j: + d = rows[i][j] + rows[i] = [x-d*y for x, y in zip(rows[i], rows[j])] + return [row[-1] for row in rows] + + +def dual_slack(pattern, dual, lower): + rank, counts, remainder = pattern + return lower[remainder] - dual[RANKS.index(rank)] - sum(n*z for n, z in zip(counts, dual[4:])) + + +def validate_dual(pats, dual, lower, penalty): + need(penalty > 0, 'positive defect penalty') + for pattern in pats: + rank, counts, _ = pattern + need(dual_slack(pattern, dual, lower) >= + (penalty if rank == 8 and counts[3] == 0 else 0), 'dual pattern inequality') + + +def validate_primal(counts): + need(len(counts) == len(SUPPORT) and all(x >= 0 for x in counts), 'primal nonnegativity') + for rank, bins in zip(RANKS, BINS): + need(sum(x for x, (r, _) in zip(counts, SUPPORT) if r == rank) == bins, + 'primal bin balance') + for j, supply in enumerate(INVENTORY): + need(sum(x*ns[j] for x, (_, ns) in zip(counts, SUPPORT)) == CALLS*supply, + 'primal width balance') + + +def certify(a, defect=114): + pats = patterns() + lower = {r: h_bounds(r, a)[0] for r in range(49)} + matrix = [[int(rank == r) for r in RANKS] + list(counts) for rank, counts in SUPPORT] + rhs = [lower[rank - sum(w*n for w, n in zip(WIDTHS, counts))] for rank, counts in SUPPORT] + dual = solve(matrix, rhs) + # A separate closed-form derivation of the same nine equality constraints. + t = (lower[3] - lower[48])/5 + y32 = lower[5] - 3*t + closed = [y32/4, y32/2, y32, lower[48], lower[1]-lower[5], + -lower[5], (t-lower[5])/2, -y32/4, t] + need(dual == closed, 'closed-form and elimination duals disagree') + repairs = [] + for i, rank in enumerate(RANKS): + repair = min(F(0), min(dual_slack(p, dual, lower) for p in pats if p[0] == rank)) + dual[i] += repair + repairs.append(str(repair)) + penalty = min(dual_slack(p, dual, lower) for p in pats if p[0] == 8 and p[1][3] == 0) + validate_dual(pats, dual, lower, penalty) + local = CALLS * sum(n*lower[r] for r, n in LOCAL.items()) + relaxed = local + sum(n*y for n, y in zip(BINS, dual[:4])) + CALLS*sum(n*z for n, z in zip(INVENTORY, dual[4:])) + total = relaxed + defect*penalty + primal_rhs = list(BINS) + [CALLS*n for n in INVENTORY] + primal = solve(list(map(list, zip(*matrix))), list(map(F, primal_rhs))) + validate_primal(primal) + primal_upper = CALLS*sum(n*h_bounds(r, a)[1] for r, n in LOCAL.items()) + primal_upper += sum(x*h_bounds(rank-sum(w*n for w, n in zip(WIDTHS, ns)), a)[1] + for x, (rank, ns) in zip(primal, SUPPORT)) + need(relaxed <= primal_upper, 'weak duality control') + result = dict(threshold=str(a), pattern_count=len(pats), dual=[str(v) for v in dual], + bin_dual_repairs=repairs, + window_free_primal_counts=[str(x) for x in primal], + window_free_primal_upper=str(primal_upper), + penalty_per_defect=str(penalty), defect=defect, + local_lower=str(local), window_free_lower=str(relaxed), + chronological_lower=str(total), live=LIVE, strict_margin=str(total-LIVE)) + return result, pats, dual, lower, penalty + + +def failure_controls(source, context, manifest): + rejected = [] + + def rejects(name, fn, expected): + try: + fn() + except ValueError as exc: + need(str(exc) == expected, 'wrong control failure: ' + name) + rejected.append(name) + else: + raise ValueError('accepted negative control: ' + name) + + pin = manifest['files'][0] + data = (HERE / pin['path']).read_bytes() + rejects('changed_source_bytes', lambda: authenticate(data + b' ', pin), 'input SHA256 mismatch') + order = diagonal_order(4) + wrong = order[:] + i, j = wrong.index((0, 0)), wrong.index((1, 0)) + wrong[i], wrong[j] = wrong[j], wrong[i] + rejects('reversed_replica_stages', lambda: event_windows(wrong, context), 'replica stage order') + windows = event_windows(order, context) + wrong_windows = dict(windows) + wrong_windows[0, 1] = (windows[0, 1][0] - 1,) + windows[0, 1] + rejects('inclusive_pre_bridge_endpoint', lambda: compare_windows(order, wrong_windows), + 'independent window derivations disagree') + bad_context = copy.deepcopy(context) + bad_context[2][1] = [(i, e) for i, e in bad_context[2][1] if e['kind'] != 'bridge'] + rejects('omitted_source_bridge', lambda: event_windows(order, bad_context), 'per-replica event projection') + rejects('duplicate_cut_group', lambda: cut(windows, CRITICAL[:-1] + (CRITICAL[0],)), '102 distinct cut groups') + rejects('overstated_defect_115', lambda: need(cut(windows)['defect'] >= 115, 'cut deficiency'), 'cut deficiency') + rejects('unbound_inventory_79', lambda: need(cut(windows, width8_supply=79)['defect'] >= 114, 'cut deficiency'), 'cut deficiency') + result, pats, dual, lower, penalty = certify(THRESHOLD) + bad_dual = dual[:] + bad_dual[0] += F(1, 100) + rejects('inflated_rank8_dual', lambda: validate_dual(pats, bad_dual, lower, penalty), 'dual pattern inequality') + rejects('inflated_defect_penalty', lambda: validate_dual(pats, dual, lower, penalty + F(1, 10**6)), 'dual pattern inequality') + primal = list(map(F, result['window_free_primal_counts'])) + primal[0] += 1 + rejects('unbalanced_relaxed_primal', lambda: validate_primal(primal), 'primal bin balance') + need(F(result['window_free_primal_upper']) < LIVE < F(result['chronological_lower']), 'cut is essential') + below, *_ = certify(F(source['PR2571-CLAIM.json']['complex_lower'])) + need(F(below['chronological_lower']) < LIVE, 'does not reject predecessor endpoint') + # Separate arithmetic controls use algebraic identities, not a second exp implementation. + for rank in (1, 7, 8, 16, 48, 73): + lo, hi = h_bounds(rank, F(0)) + need(lo <= F(rank, M) <= hi, 'linear-cost control') + lo, hi = h_bounds(rank, F(1, 2)) + need(lo*lo <= F(rank, M) <= hi*hi, 'square-root control') + lo, hi = h_bounds(rank, F(1)) + need(lo <= 1 <= hi, 'constant-cost control') + return dict(rejected=rejected, positive=['all_rank8_windows_two_derivations', + 'integer_shift_closed_form', 'stable_order_after_shift70', + 'linear_square_root_constant_costs', 'predecessor_endpoint_not_rejected', + 'window_free_primal_accepts_excluded_threshold']) + + +def verify(): + source, manifest = load_inputs() + providers = source['PR2530-PROVIDERS.json'] + need(set(providers) == {'gauge44', 'extra'}, 'two source providers') + for provider in providers.values(): + need(Counter(provider['widths']) == dict(zip(WIDTHS, INVENTORY)), 'source width inventory') + need({int(r): n for r, n in provider['actual_paid_profile'].items()} == LOCAL, 'source local profile') + need(sum(INVENTORY) == 422 and LIVE == REPLICAS*8*PORTS, 'whole-helper and live stock') + total_mass = CALLS*sum(r*n for r, n in LOCAL.items()) + sum(r*n for r, n in zip(RANKS, BINS)) - CALLS*sum(w*n for w, n in zip(WIDTHS, INVENTORY)) + need(total_mass == 4816512 and M*LIVE-total_mass == 23680, 'complete rank mass and deficit') + context = source_context(source['PR2435-TEMPLATE.json.gz']) + cases = check_chronology(context, source) + result, *_ = certify(THRESHOLD) + need(F(result['strict_margin']) > 0, 'strict moment exclusion') + controls = failure_controls(source, context, manifest) + return dict(schema_version=1, status='PASS_T74_DIAGONAL_WINDOW_BOUND', + model=dict(replicas=REPLICAS, calls=CALLS, width=M, live=LIVE, + widths=list(WIDTHS), inventory=list(INVENTORY), bins=list(BINS), + local_profile={str(r): n for r, n in LOCAL.items()}), + critical_groups=[list(g) for g in CRITICAL], shift_cases=cases, + union_formula='117 + max(0, min(28, 69-s)), for integer s >= 0', + minimum_defect=114, price=result, controls=controls, + source_sha256={p['path']: p['sha256'] for p in manifest['files']}, + scope='Fixed whole-helper inventory and uniform initial stage shifts only; no new kappa or supplier admission.') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write-certificate', action='store_true') + args = parser.parse_args() + result = verify() + path = HERE / 'CERTIFICATE.json' + if args.write_certificate: + path.write_text(canonical(result)) + else: + need(canonical(json.loads(path.read_text())) == canonical(result), + 'stored certificate differs from exact replay') + print(result['status'], 'shifts=71+stable_tail groups=102 deficit>=114 patterns=1163', + 'b<0.001714127696 controls=' + str(len(result['controls']['rejected'])), 'no_new_kappa') + + +if __name__ == '__main__': + main()