diff --git a/research/p104-endpoint-saturation/README.md b/research/p104-endpoint-saturation/README.md new file mode 100644 index 0000000000..60ba24f5e5 --- /dev/null +++ b/research/p104-endpoint-saturation/README.md @@ -0,0 +1,174 @@ +# P104 endpoint demand saturation + +The 253 cheap / 147 unit-step, 400-lifetime control in [PR2896][2896] cannot +realize the frozen X-only monotone correction. Even granting independent, +arbitrary endpoint assignments, it can cover at most **3,972 of 4,656** +residual demands in each orientation. The deficit is **684**. + +This closes PR2896's explicit endpoint-specific assignment handoff. Its +aggregate calculation `253 + 30*147 = 4663` is correct as a necessary screen. +The new condition accounts for demand saturation at each endpoint. Capacity +left over at one endpoint cannot cover another endpoint's missing labels. + +For a budget of 400 lifetimes using only these two history types, at least +**192 unit-step lifetimes** are necessary. This threshold is sharp for the +separate endpoint-count relaxations. With 191 units, at least 219 cheap +lifetimes are needed, totaling 410. With 192 units, 204 cheap lifetimes +suffice in each relaxation, totaling 396. Four further cheap lifetimes may +be left unproductive to give the stated 400 budget. No actual geometric, +chronological or simultaneous source/target construction is supplied. + +## Contract and inherited implication + +Use the same PR1972/1991 104-port correction `C = I-G/2` as PR2889 and +PR2896. Sources X are immutable, targets Y are unread, and their fixed frame +paths increase by inclusion. New helpers start source-independent at ZERO, +end at FULL with their logical dirt restored, and follow increasing frame +paths. Reinitialization starts another lifetime. Original helper/private +reads, target feedback, source writes, descending transport and changed +original paths are outside this model. Equal-frame rational mixing, relays, +singular mixing and cancellation remain allowed. + +The two types are the dimension-jump histories `(1,7,1)`, called cheap below, +and `(1,1,1,1,1,1,1,1,1)`, called unit-step. Both visit dimension one and +dimension eight exactly once. A nested lifetime can meet at most one +specified source line and one specified target hyperplane. + +We use PR2896's written dependency-path implication. Every residual source +label at a target endpoint must arrive on a new helper from a proper +subspace. The dual statement applies to residual target normals after a +source departure. A cheap lifetime carries at most one such label in each +orientation. A unit-step lifetime carries at most the endpoint's proper +subspace capacity. Logical dirt and cancellation cannot create a missing +source-dependence path. This package adds demand saturation to that necessary +implication, rather than claiming a new proof of the full network interface. + +The checker reconstructs the original chronological X/Y paths and the +ordered root Gram correction directly from the two main-branch inputs. It +reconstructs all residual sets and enumerates all 510 ambient functionals +other than the endpoint annihilator. These give the 255 proper hyperplanes +inside each eight-dimensional endpoint, each twice. Every proper subspace +extends to one of these hyperplanes. The resulting 208 records exactly +match the pinned PR2896 receipt, without importing its implementation. + +Both orientations have the same multiset of demand/capacity pairs: + +| Demand d | Unit capacity b | Endpoint count | +|---:|---:|---:| +| 36 | 24 | 12 | +| 44 | 28 | 24 | +| 45 | 30 | 8 | +| 46 | 29 | 24 | +| 47 | 30 | 24 | +| 48 | 30 | 12 | + +## Exact allocation bound + +At endpoint i let `u_i` and `c_i` count assigned unit and cheap lifetimes. +Every permitted network satisfies the relaxed necessary inequalities + +```text +d_i <= b_i*u_i + c_i +sum_i u_i <= U +sum_i c_i <= C. +``` + +An endpoint can usefully receive at most `d_i` distinct demands. Its first +unit therefore contributes at most `b_i`, its second at most `d_i-b_i`, +and later units contribute zero. Here `b_i < d_i <= 2*b_i`. The marginal +contributions decrease within every endpoint. + +Sort all 208 marginals in decreasing order, placing a first unit before +its second in a tie. Let `F(U)` be the sum of the first `min(U,208)` entries. +The selected entries respect every endpoint prefix, so their allocation is +valid in this relaxation. Any U units have useful contribution at most +F(U), since no U entries can exceed the U largest. Therefore the exact +minimum number of cheap lifetimes in this relaxation is + +```text +C_min(U) = 4656 - F(U). +``` + +The lower bound follows by summing the remaining demands. It is attained +in the relaxed count problem by placing one cheap lifetime on each remaining +demand. This attainment does not assert that actual subspaces realize the +capacities or that the assignments in opposite orientations can be joined. + +For U=147, the first 104 marginals sum to 2,976. The next 43 are +`12*18 + 31*17 = 743`, so `F(147)=3719` and `C_min(147)=937`. +With C=253, the total useful contribution is at most 3,972. This is already +an obstruction in either orientation separately. + +A second implementation uses integer dynamic programming. After each +endpoint it minimizes the cheap count for each exact unit count, considering +zero, one or two units there. It does not use the sorted marginals. The two +methods agree at all 209 budgets in both orientations. RESULT.json records +the complete curve and explicit relaxed allocations at the 192-unit threshold. + +## Reproduce and evidence + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-endpoint-saturation +``` + +The main command prints +`PASS_P104_ENDPOINT_SATURATION deficit=684 minimum_units_at_400=192`. +Use `verify.py --emit` to print the recomputed receipt without changing files. +The registered normal and optimized checks compare the complete typed receipt. +Five behavioral test groups cover 780 exhaustive small allocation problems, +the literal rejection/threshold, invalid domain bounds, a semantic mutant +that removes demand saturation, a Git-free export, source corruption and an +integer-to-float receipt corruption. Subprocesses have 30-second timeouts. + +Evidence is author-checked. The allocation algorithms are separate +implementations, while both use the same reconstructed geometry and inherited +program-to-endpoint implication. No independent human or formal-kernel review +is claimed. Source hashes, the exact PR2896 snapshot and main provenance are +in SOURCES.json; scope and freshness are in TASK.json. + +No moment or new exponent is claimed for any replacement profile. The +selected frontier and frozen predecessors are unchanged. Native execution, +rounded restoration, physical hosting/movement, all-size lifting and a complete +consumer/supplier invoice remain open. The selected cold replay is not run +because this package does not change the selected construction. + +Engineering choices follow Build the Lever, through the reproducible integer +certificate, and Prove It Works, through original-input reconstruction and +rejecting controls. All functions are below 60 lines. Loop bounds come from +104 endpoints, 4,058 events, 512 frame vectors, 209 DP states and the explicitly +enumerated 780 toy cases. The input boundary limits each JSON file to 2 MB. +Python's managed allocation is a Power of Ten rule 3 deviation; the fixed +finite domains bound live collections, and temporary test exports are cleaned +on success and failure. A fixed-array port would be appropriate if this checker +became a resident or streaming service. The inherited source contract and +all-size theorem are not strengthened by these implementation checks. + +## Open next questions + +Can a named two-type profile with at least 192 unit-step lifetimes satisfy +actual subspace-union coverage, joint source/target incidence and chronology, +while retaining a favorable complete cost? First price a concrete candidate +against the inherited optimistic budget, then test its actual endpoint sets. +The count relaxation supplies neither that budget nor a construction. + +Family decision: stop after the endpoint-assignment audit. Do not start another +construction round merely because the 192-unit count threshold passes. Any +continuation needs a stated candidate, complete boundary/cost ledger and an +identified geometric or chronological constraint that can change the decision. + +## Credit and provenance + +Nick Petalas. New work is Apache-2.0. The source-bound allocation implication +and checker are the contribution here. Credit Nick Petalas/PR2896 for the +residual endpoint capacities and handoff, Hiroki Kumazaki/PR2889/2353 for the +endpoint-span and monotone-history model, ywz65/PR2614 for source-departure +handling, Arham Tahir/PR2675/2682 for coupled screens, Sagar Thakrar for the +mixer handoff, and Philippe Van Velzen for the relay construction/window bill. +Retain Rohan Arun/PR1972, Chafik Boukhalfa/PR1991, Adam Gall/PR1940, +Josie Elliston/PR1071, Ali Romman/PR1125 and the geometry/native lineage. +The byte-exact predecessor RESULT.json is data from PR2896, not a new result +of this package. Substantial AI assistance was used; details are in TASK.json. + +[2896]: https://github.com/CrocSwap/integer-mult-bounds/pull/2896 diff --git a/research/p104-endpoint-saturation/RESULT.json b/research/p104-endpoint-saturation/RESULT.json new file mode 100644 index 0000000000..d9d3f38c88 --- /dev/null +++ b/research/p104-endpoint-saturation/RESULT.json @@ -0,0 +1,1340 @@ +{ + "arrival": { + "endpoint_types": [ + [ + 36, + 24, + 12 + ], + [ + 44, + 28, + 24 + ], + [ + 45, + 30, + 8 + ], + [ + 46, + 29, + 24 + ], + [ + 47, + 30, + 24 + ], + [ + 48, + 30, + 12 + ] + ], + "minimum_cheap_by_units": [ + 4656, + 4626, + 4596, + 4566, + 4536, + 4506, + 4476, + 4446, + 4416, + 4386, + 4356, + 4326, + 4296, + 4266, + 4236, + 4206, + 4176, + 4146, + 4116, + 4086, + 4056, + 4026, + 3996, + 3966, + 3936, + 3906, + 3876, + 3846, + 3816, + 3786, + 3756, + 3726, + 3696, + 3666, + 3636, + 3606, + 3576, + 3546, + 3516, + 3486, + 3456, + 3426, + 3396, + 3366, + 3336, + 3307, + 3278, + 3249, + 3220, + 3191, + 3162, + 3133, + 3104, + 3075, + 3046, + 3017, + 2988, + 2959, + 2930, + 2901, + 2872, + 2843, + 2814, + 2785, + 2756, + 2727, + 2698, + 2669, + 2640, + 2612, + 2584, + 2556, + 2528, + 2500, + 2472, + 2444, + 2416, + 2388, + 2360, + 2332, + 2304, + 2276, + 2248, + 2220, + 2192, + 2164, + 2136, + 2108, + 2080, + 2052, + 2024, + 1996, + 1968, + 1944, + 1920, + 1896, + 1872, + 1848, + 1824, + 1800, + 1776, + 1752, + 1728, + 1704, + 1680, + 1662, + 1644, + 1626, + 1608, + 1590, + 1572, + 1554, + 1536, + 1518, + 1500, + 1482, + 1464, + 1447, + 1430, + 1413, + 1396, + 1379, + 1362, + 1345, + 1328, + 1311, + 1294, + 1277, + 1260, + 1243, + 1226, + 1209, + 1192, + 1175, + 1158, + 1141, + 1124, + 1107, + 1090, + 1073, + 1056, + 1039, + 1022, + 1005, + 988, + 971, + 954, + 937, + 920, + 903, + 886, + 869, + 852, + 835, + 818, + 801, + 784, + 767, + 750, + 733, + 716, + 699, + 682, + 665, + 648, + 632, + 616, + 600, + 584, + 568, + 552, + 536, + 520, + 504, + 488, + 472, + 456, + 440, + 424, + 408, + 392, + 376, + 360, + 344, + 328, + 312, + 296, + 280, + 264, + 249, + 234, + 219, + 204, + 189, + 174, + 159, + 144, + 132, + 120, + 108, + 96, + 84, + 72, + 60, + 48, + 36, + 24, + 12, + 0 + ], + "minimum_units_at_400": 192, + "profile_253_147": { + "deficit": 684, + "maximum_coverage": 3972 + }, + "relaxed_assignment_at_threshold": [ + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ] + ], + "threshold_cheap": 204 + }, + "departure": { + "endpoint_types": [ + [ + 36, + 24, + 12 + ], + [ + 44, + 28, + 24 + ], + [ + 45, + 30, + 8 + ], + [ + 46, + 29, + 24 + ], + [ + 47, + 30, + 24 + ], + [ + 48, + 30, + 12 + ] + ], + "minimum_cheap_by_units": [ + 4656, + 4626, + 4596, + 4566, + 4536, + 4506, + 4476, + 4446, + 4416, + 4386, + 4356, + 4326, + 4296, + 4266, + 4236, + 4206, + 4176, + 4146, + 4116, + 4086, + 4056, + 4026, + 3996, + 3966, + 3936, + 3906, + 3876, + 3846, + 3816, + 3786, + 3756, + 3726, + 3696, + 3666, + 3636, + 3606, + 3576, + 3546, + 3516, + 3486, + 3456, + 3426, + 3396, + 3366, + 3336, + 3307, + 3278, + 3249, + 3220, + 3191, + 3162, + 3133, + 3104, + 3075, + 3046, + 3017, + 2988, + 2959, + 2930, + 2901, + 2872, + 2843, + 2814, + 2785, + 2756, + 2727, + 2698, + 2669, + 2640, + 2612, + 2584, + 2556, + 2528, + 2500, + 2472, + 2444, + 2416, + 2388, + 2360, + 2332, + 2304, + 2276, + 2248, + 2220, + 2192, + 2164, + 2136, + 2108, + 2080, + 2052, + 2024, + 1996, + 1968, + 1944, + 1920, + 1896, + 1872, + 1848, + 1824, + 1800, + 1776, + 1752, + 1728, + 1704, + 1680, + 1662, + 1644, + 1626, + 1608, + 1590, + 1572, + 1554, + 1536, + 1518, + 1500, + 1482, + 1464, + 1447, + 1430, + 1413, + 1396, + 1379, + 1362, + 1345, + 1328, + 1311, + 1294, + 1277, + 1260, + 1243, + 1226, + 1209, + 1192, + 1175, + 1158, + 1141, + 1124, + 1107, + 1090, + 1073, + 1056, + 1039, + 1022, + 1005, + 988, + 971, + 954, + 937, + 920, + 903, + 886, + 869, + 852, + 835, + 818, + 801, + 784, + 767, + 750, + 733, + 716, + 699, + 682, + 665, + 648, + 632, + 616, + 600, + 584, + 568, + 552, + 536, + 520, + 504, + 488, + 472, + 456, + 440, + 424, + 408, + 392, + 376, + 360, + 344, + 328, + 312, + 296, + 280, + 264, + 249, + 234, + 219, + 204, + 189, + 174, + 159, + 144, + 132, + 120, + 108, + 96, + 84, + 72, + 60, + 48, + 36, + 24, + 12, + 0 + ], + "minimum_units_at_400": 192, + "profile_253_147": { + "deficit": 684, + "maximum_coverage": 3972 + }, + "relaxed_assignment_at_threshold": [ + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 1, + 12 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 15 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ], + [ + 2, + 0 + ] + ], + "threshold_cheap": 204 + } +} diff --git a/research/p104-endpoint-saturation/SOURCES.json b/research/p104-endpoint-saturation/SOURCES.json new file mode 100644 index 0000000000..eb4593f34c --- /dev/null +++ b/research/p104-endpoint-saturation/SOURCES.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "base_commit": "62285350100dcb5c4f3638135a58692caea9e289", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "889b95d936746df124872133ae1e7cc339adcb92", + "sha256": "7d185cd8c2af35988d638d969748ad7b670f902606444dbfc748e4402c340df6" + }, + { + "path": "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "usage": "input", + "git_blob": "86beaf424e9f0f800ae3a62797d94ec9386b7706", + "sha256": "0f541bef7f19fdeffd67157684e9f03d785f42c89973632f508fc1a0452b580e" + }, + { + "path": "research/p104-native-channel/inputs/P104-FIXTURE.json", + "usage": "input", + "git_blob": "2e16f99b295bb386fd13bd8fbd57b42ef54143a9", + "sha256": "516c06f6ec3cb84be588c546108de897650288576dd5fbf5fe44b9c5546ad8a4" + } + ], + "predecessor": { + "pr": 2896, + "commit": "d33e8066de4d3e3b8230f2b3635d7bdcd80155ad", + "path": "research/p104-endpoint-support-capacity/RESULT.json", + "snapshot": "predecessor/RESULT.json", + "git_blob": "d838abbe5523ff044b63fd6fbc2f1811b9d4b1ae", + "sha256": "40bce664e5e6677d30ee1b7100c9443292eaaad6d1640dd991a2178977e27431" + } +} diff --git a/research/p104-endpoint-saturation/TASK.json b/research/p104-endpoint-saturation/TASK.json new file mode 100644 index 0000000000..12e6314840 --- /dev/null +++ b/research/p104-endpoint-saturation/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 5, + "base_commit": "62285350100dcb5c4f3638135a58692caea9e289", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json" + ], + "methods": [ + "Reconstruct the rank ledger from original operations rather than trusting its aggregate.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure" + ] + }, + "scope_status": "refined", + "actual_scope": "Audit the PR2896 253/147 profile by exact demand-saturated endpoint allocation, reconstructing its geometric inputs.", + "scope_change_reason": "Take the released central endpoint-specific assignment handoff. The new implication concerns rank/capacity accounting rather than recalculating an unchanged root.", + "bottleneck_link": "Rejecting an unrealizable favorable helper inventory prevents spending a construction round on a profile that cannot deliver the P104 correction.", + "budget_minutes": 60, + "stop_rule": "Stop after a written necessary bound, independently computed allocation optimum, original-input reconstruction and failure controls. Do not start a supplier construction campaign.", + "outcome": "negative-result", + "evidence": "RESULT.json; verify.py; test_verify.py", + "author": "Nick Petalas", + "ai_assistance": "Substantial AI assistance used for the proof, implementation and checking. Separate allocation implementations do not constitute independent human review.", + "open_questions": [ + { + "question": "Can an explicitly priced two-type profile passing the saturated allocation bound realize actual endpoint unions and chronological source/target assignments?", + "why_it_matters": "A favorable count relaxation is insufficient to justify a physical correction campaign.", + "first_step": "Price one concrete profile with at least 192 unit-step lifetimes under a complete declared boundary, then test exact endpoint subsets.", + "blocked_by": "No joint geometric/chronological assignment or complete cost ledger is supplied." + } + ], + "seed": "640eceab1ba88033d27922fdda8ab7b2", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2245#discussioncomment-18969339", + "overlap": { + "checked_at": "2026-10-16T10:06:40.473177+00:00", + "coverage": { + "open_prs": { + "fetched_at": "2026-10-16T10:05:52.230465+00:00", + "complete_pagination": true, + "records": 488 + }, + "discussions": { + "fetched_at": "2026-10-16T10:06:18.865290+00:00", + "complete_pagination": true, + "records": 1581 + }, + "closed_prs": { + "fetched_at": "2026-10-16T10:06:40.334499+00:00", + "complete_pagination": true, + "records": 2114 + } + }, + "warnings": [], + "matched": "The credited PR2896 handoff and this package's local notes; arbitrary diffs and unpublished work are outside coverage." + }, + "freshness": { + "main": "11720ce76c6d5e3e355d14f194f0e9bce90adbc1", + "priority_revision": 5, + "checked_at": "2026-10-16T10:05:19Z", + "predecessor": "d33e8066de4d3e3b8230f2b3635d7bdcd80155ad", + "relevant_change": "No change to guidance, selected record or either original scientific input; preserve the 622853501 scientific/provenance base." + } +} diff --git a/research/p104-endpoint-saturation/VERIFY.json b/research/p104-endpoint-saturation/VERIFY.json new file mode 100644 index 0000000000..cc8da85e52 --- /dev/null +++ b/research/p104-endpoint-saturation/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-native-channel/inputs/LOWRANK-WITNESS.json", + "research/p104-native-channel/inputs/P104-FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Original-input geometric reconstruction, exact marginal bound, independent integer DP, typed receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-Werror", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same invariant checks remain active under optimization." + }, + { + "argv": [ + "{python}", + "-B", + "-Werror", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "780 exhaustive toy allocations; literal threshold; domain, semantic mutant, export and source/receipt corruption controls." + } + ] +} diff --git a/research/p104-endpoint-saturation/geometry.py b/research/p104-endpoint-saturation/geometry.py new file mode 100644 index 0000000000..a08360057f --- /dev/null +++ b/research/p104-endpoint-saturation/geometry.py @@ -0,0 +1,108 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Reconstruct endpoint demands without importing predecessor implementations.""" + +from itertools import combinations, product + + +def require(condition, reason): + if not condition: + raise ValueError(reason) + + +def frame(vectors): + require(len(vectors) <= 9, 'at most nine basis vectors') + points = [0] + for vector in vectors: + require(type(vector) is int and 0 < vector < 512, 'binary vector') + require(vector not in points, 'independent frame basis') + points += [point ^ vector for point in points] + return sum(1 << point for point in points) + + +def paths(witness): + require(len(witness['program']) == 4058, 'frozen 4058-event word') + names = [f'{kind}{i}' for kind in 'XY' for i in range(104)] + result = {name: [frame(witness['initial_frames'][name])] for name in names} + for event in witness['program']: + op, destination = event[:2] + require(op in {'transport', 'add', 'copy', 'zero', 'erase'}, 'known event') + if op in {'add', 'copy'}: + require(not destination.startswith('X') and not event[2].startswith('Y'), + 'immutable sources and unread targets') + if op in {'zero', 'erase'}: + require(destination not in result, 'no data reinitialization') + if op == 'transport' and destination in result: + before, after = frame(event[2]), frame(event[3]) + require(result[destination][-1] == before and before != after + and before & after == before, 'increasing chronological path') + require(event[4] == len(event[3]) - len(event[2]), 'transport rank') + result[destination].append(after) + for name, chain in result.items(): + require(len(chain) <= 10 and chain[-1] == frame(witness['final_frames'][name]), + 'complete data path') + return result + + +def ports(fixture): + roots = [] + for i, j in combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + roots.append(tuple(row)) + roots += [(1, *signs) for signs in product((-1, 1), repeat=7) + if sum(sign < 0 for sign in signs) % 2 == 0] + removed = fixture['section4_explicit_P104'] + excluded = {tuple(row) for row in removed['F0'] + removed['C']} + result = sorted(set(roots) - excluded) + require(len(roots) == 120 and len(result) == 104, 'ordered P104 roots') + return result + + +def endpoint_data(chain, roots): + source = [chain[f'X{i}'] for i in range(104)] + target = [chain[f'Y{i}'] for i in range(104)] + require(all(c[0].bit_count() == 2 and c[-1].bit_count() == 512 for c in source) + and all(c[0] == 1 and c[-1].bit_count() == 256 for c in target), + 'line-to-FULL and ZERO-to-hyperplane endpoints') + labels = [c[0].bit_length() - 1 for c in source] + normals = [] + for c in target: + candidates = [a for a in range(1, 512) + if all(not (q & a).bit_count() % 2 for q in range(512) + if c[-1] >> q & 1)] + require(len(candidates) == 1, 'unique endpoint normal') + normals.append(candidates[0]) + require(len(set(labels)) == len(set(normals)) == 104, 'distinct endpoints') + arrivals, departures = [[] for _ in range(104)], [[] for _ in range(104)] + demands = 0 + for t, left in enumerate(roots): + for s, right in enumerate(roots): + gram = sum(a * b for a, b in zip(left, right, strict=True)) + require(bool(target[t][-1] >> labels[s] & 1) == (gram % 8 == 4), + 'root-to-frame binding') + if gram == 8 * int(t == s): + continue + demands += 1 + require(target[t][-1] not in source[s], 'no direct endpoint bypass') + require(source[s][0] not in target[t], 'no target visits source line') + if not any(c >> labels[s] & 1 for c in target[t][:-1]): + arrivals[t].append(labels[s]) + if not any(c.bit_count() > 2 and c & target[t][-1] == c for c in source[s]): + departures[s].append(normals[t]) + require(demands == 4992, '4992 correction coefficients') + return (arrivals, normals), (departures, labels) + + +def census(residuals, annihilators): + result = [] + for points, normal in zip(residuals, annihilators, strict=True): + require(0 < len(points) == len(set(points)) <= 48, 'residual size') + require(all(not (point & normal).bit_count() % 2 for point in points), + 'residual belongs to endpoint') + maximum = max(sum(not (point & a).bit_count() % 2 for point in points) + for a in range(1, 512) if a != normal) + require(maximum < len(points), 'residual spans endpoint') + result.append((len(points), maximum)) + require(sum(d for d, _ in result) == 4656, '4656 residual demands') + return result diff --git a/research/p104-endpoint-saturation/predecessor/RESULT.json b/research/p104-endpoint-saturation/predecessor/RESULT.json new file mode 100644 index 0000000000..d838abbe55 --- /dev/null +++ b/research/p104-endpoint-saturation/predecessor/RESULT.json @@ -0,0 +1,2109 @@ +{ + "arrival_endpoints": [ + { + "proper_max": 30, + "residual": 45, + "witness": 425 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 397 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 173 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 432 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 444 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 287 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 311 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 432 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 123 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 425 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 306 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 120 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 311 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 173 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 452 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 349 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 340 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 216 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 219 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 510 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 483 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 210 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 238 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 464 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 473 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 505 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 397 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 397 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 237 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 204 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 448 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 423 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 425 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 264 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 337 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 471 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 425 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 373 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 366 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 354 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 387 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 383 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 397 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 425 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 397 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 397 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 439 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 425 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 326 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 335 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 452 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 391 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 354 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 347 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 403 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 326 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 405 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 505 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 489 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 486 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 492 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 492 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 498 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 492 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 504 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 413 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 486 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 495 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 470 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 498 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 301 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 387 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 399 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 464 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 476 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 470 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 265 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 470 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 462 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 450 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 423 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 424 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 498 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 492 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 503 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 441 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 438 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 440 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 425 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 425 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 197 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 232 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 246 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 172 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 438 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 411 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + } + ], + "departure_endpoints": [ + { + "proper_max": 30, + "residual": 45, + "witness": 479 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 503 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 509 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 509 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 506 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 509 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 509 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 493 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 508 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 508 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 509 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 508 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 422 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 359 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 339 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 438 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 508 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 380 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 509 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 422 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 422 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 493 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 462 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 469 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 255 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 496 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 495 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 479 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 495 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 509 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 493 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 493 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 509 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 506 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 509 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 493 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 495 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 509 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 366 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 438 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 371 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 373 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 436 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 496 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 436 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 479 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 479 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 479 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 422 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 223 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 455 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 476 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 493 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 496 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 436 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 436 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 115 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 436 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 510 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 510 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 479 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 510 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 422 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 115 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 495 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 510 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 510 + }, + { + "proper_max": 24, + "residual": 36, + "witness": 510 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 509 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 493 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 223 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 495 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 509 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 255 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 509 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 495 + }, + { + "proper_max": 30, + "residual": 45, + "witness": 495 + }, + { + "proper_max": 28, + "residual": 44, + "witness": 503 + }, + { + "proper_max": 29, + "residual": 46, + "witness": 493 + }, + { + "proper_max": 30, + "residual": 47, + "witness": 493 + }, + { + "proper_max": 30, + "residual": 48, + "witness": 493 + } + ], + "history_weights": [ + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 8 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 4 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 8 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 2 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 8 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 4 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 8 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 16 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 0, + 30 + ], + [ + 0, + 0 + ], + [ + 1, + 1 + ], + [ + 2, + 0 + ], + [ + 2, + 30 + ], + [ + 4, + 0 + ], + [ + 4, + 30 + ], + [ + 4, + 0 + ], + [ + 4, + 30 + ], + [ + 8, + 0 + ], + [ + 8, + 16 + ], + [ + 8, + 0 + ], + [ + 8, + 30 + ], + [ + 8, + 0 + ], + [ + 8, + 30 + ], + [ + 8, + 0 + ], + [ + 8, + 30 + ], + [ + 16, + 0 + ], + [ + 16, + 8 + ], + [ + 16, + 0 + ], + [ + 16, + 30 + ], + [ + 16, + 0 + ], + [ + 16, + 30 + ], + [ + 16, + 0 + ], + [ + 16, + 30 + ], + [ + 16, + 0 + ], + [ + 16, + 16 + ], + [ + 16, + 0 + ], + [ + 16, + 30 + ], + [ + 16, + 0 + ], + [ + 16, + 30 + ], + [ + 16, + 0 + ], + [ + 16, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 4 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 16 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 8 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 16 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 2 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 16 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 8 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 16 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 4 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 16 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 8 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 16 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ], + [ + 30, + 0 + ], + [ + 30, + 30 + ] + ], + "profiles": [ + { + "cheap": 329, + "cut_capacity": 4873, + "ideal_idle_mass": 744, + "lifetimes": 400, + "moment_upper": "0.999470826199440", + "span_total": 826, + "support_rows_pass": false, + "support_total": 2459, + "unit": 71 + }, + { + "cheap": 335, + "cut_capacity": 4879, + "ideal_idle_mass": 690, + "lifetimes": 406, + "moment_upper": "0.999503341067906", + "span_total": 832, + "support_rows_pass": false, + "support_total": 2465, + "unit": 71 + }, + { + "cheap": 253, + "cut_capacity": 9661, + "ideal_idle_mass": 744, + "lifetimes": 400, + "moment_upper": "0.999729278053145", + "span_total": 1282, + "support_rows_pass": true, + "support_total": 4663, + "unit": 147 + } + ], + "proper_capacity": 30, + "required_per_orientation": 4656 +} diff --git a/research/p104-endpoint-saturation/test_verify.py b/research/p104-endpoint-saturation/test_verify.py new file mode 100644 index 0000000000..8a5ab19d83 --- /dev/null +++ b/research/p104-endpoint-saturation/test_verify.py @@ -0,0 +1,111 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral controls for allocation, source binding and published CLI checks.""" + +import itertools +import json +import shutil +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +import verify + +PACKAGE = Path(__file__).resolve().parent + + +class AllocationTests(unittest.TestCase): + def test_exhaustive_small_allocations(self): + options = [(2, 1), (3, 2), (4, 2), (5, 3), (6, 3)] + cases = 0 + for size in range(1, 5): + for endpoints in itertools.product(options, repeat=size): + expected = [10**6] * (2 * size + 1) + for assigned in itertools.product(range(3), repeat=size): + cheap = sum(max(0, d - c * u) for u, (d, c) in + zip(assigned, endpoints, strict=True)) + expected[sum(assigned)] = min(expected[sum(assigned)], cheap) + _, coverage = verify.marginal_certificate(endpoints) + self.assertEqual([sum(d for d, _ in endpoints) - x for x in coverage], + expected) + self.assertEqual(verify.dynamic_minimum_cheap(endpoints), expected) + cases += 1 + self.assertEqual(cases, 780) + + def test_exact_threshold_assignment_and_rejection(self): + result = verify.calculate() + for row in result.values(): + self.assertEqual(row['profile_253_147'], + {'maximum_coverage': 3972, 'deficit': 684}) + self.assertEqual(row['minimum_cheap_by_units'][191:193], [219, 204]) + assigned = row['relaxed_assignment_at_threshold'] + self.assertEqual(sum(u for u, _ in assigned), 192) + self.assertEqual(sum(c for _, c in assigned), 204) + self.assertEqual(sum(u + c for u, c in assigned), 396) + + def test_invalid_allocation_boundaries(self): + for endpoints in [[], [(0, 0)], [(5, 2)], [(2, 2)], [(31, 31)], [(3.0, 2)]]: + with self.subTest(endpoints=endpoints), self.assertRaises(ValueError): + verify.marginal_certificate(endpoints) + with self.assertRaises(ValueError): + verify.marginal_certificate([(2, 1)] * 105) + + def test_semantic_unsaturated_mutant(self): + # Without truncating a second helper's useful contribution at its endpoint, + # the credited 253/147 aggregate erroneously passes. + original = (PACKAGE / 'verify.py').read_text() + old = 'value = costs[used] + max(0, demand - added * capacity)' + new = 'value = costs[used] + demand - added * capacity' + self.assertEqual(original.count(old), 1) + with tempfile.TemporaryDirectory() as directory: + root, package = export(Path(directory)) + (package / 'verify.py').write_text(original.replace(old, new)) + run = cli(root, package, '-O') + self.assertNotEqual(run.returncode, 0) + self.assertIn('DP endpoint cases', run.stderr) + + def test_export_and_integrity_failures(self): + with tempfile.TemporaryDirectory() as directory: + root, package = export(Path(directory)) + for option in (None, '-O'): + run = cli(root, package, option) + self.assertEqual(run.returncode, 0, run.stderr) + self.assertIn('deficit=684 minimum_units_at_400=192', run.stdout) + source = root / 'research/p104-native-channel/inputs/LOWRANK-WITNESS.json' + original = source.read_bytes() + source.write_bytes(original + b' ') + rejected = cli(root, package) + self.assertNotEqual(rejected.returncode, 0) + self.assertIn('source SHA256 mismatch', rejected.stderr) + source.write_bytes(original) + receipt = json.loads((package / 'RESULT.json').read_text()) + receipt['arrival']['minimum_units_at_400'] = 192.0 + (package / 'RESULT.json').write_text(json.dumps(receipt)) + rejected = cli(root, package, '-O') + self.assertNotEqual(rejected.returncode, 0) + self.assertIn('typed receipt equality', rejected.stderr) + + +def export(root): + package = root / 'research/p104-endpoint-saturation' + shutil.copytree(PACKAGE, package, ignore=shutil.ignore_patterns('__pycache__')) + for name in ('LOWRANK-WITNESS.json', 'P104-FIXTURE.json'): + relative = Path('research/p104-native-channel/inputs') / name + target = root / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(verify.ROOT / relative, target) + return root, package + + +def cli(root, package, option=None): + arguments = [sys.executable, '-B', '-Werror'] + if option: + arguments.append(option) + arguments.append(str(package / 'verify.py')) + return subprocess.run(arguments, cwd=root, capture_output=True, text=True, + timeout=30, check=False) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/p104-endpoint-saturation/verify.py b/research/p104-endpoint-saturation/verify.py new file mode 100644 index 0000000000..6d5a628e97 --- /dev/null +++ b/research/p104-endpoint-saturation/verify.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Certify the demand-saturated endpoint allocation relaxation using integers.""" + +import argparse +import hashlib +import json +from collections import Counter +from pathlib import Path + +from geometry import census, endpoint_data, paths, ports, require + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def read_json(path): + require(path.stat().st_size <= 2_000_000, 'input byte bound') + return json.loads(path.read_bytes()) + + +def authenticated_inputs(): + manifest = read_json(PACKAGE / 'SOURCES.json') + require(len(manifest['files']) <= 10, 'manifest record bound') + inputs = {} + for row in manifest['files']: + if row['usage'] != 'input': + continue + require(row['path'] in { + 'research/p104-native-channel/inputs/LOWRANK-WITNESS.json', + 'research/p104-native-channel/inputs/P104-FIXTURE.json'}, 'input path') + path = ROOT / row['path'] + require(path.stat().st_size <= 2_000_000, 'source byte bound') + require(hashlib.sha256(path.read_bytes()).hexdigest() == row['sha256'], + 'source SHA256 mismatch') + inputs[path.name] = read_json(path) + require(len(inputs) == 2, 'two original geometric inputs') + snapshot = PACKAGE / 'predecessor/RESULT.json' + require(snapshot.stat().st_size <= 2_000_000, 'predecessor byte bound') + require(hashlib.sha256(snapshot.read_bytes()).hexdigest() + == manifest['predecessor']['sha256'], 'predecessor snapshot SHA256') + return inputs, read_json(snapshot) + + +def marginal_certificate(endpoints): + require(0 < len(endpoints) <= 104, 'endpoint count') + gains = [] + for index, (demand, capacity) in enumerate(endpoints): + require(type(demand) is int and type(capacity) is int + and 0 < capacity < demand <= 2 * capacity <= 60, 'endpoint bounds') + gains.extend([(capacity, index, 0), (demand - capacity, index, 1)]) + gains.sort(key=lambda row: (-row[0], row[1], row[2])) + require(all(gains.index((c, i, 0)) < gains.index((d - c, i, 1)) + for i, (d, c) in enumerate(endpoints)), + 'prefix-feasible marginal order') + coverage = [0] + for gain, _, _ in gains: + coverage.append(coverage[-1] + gain) + require(coverage[-1] == sum(d for d, _ in endpoints), 'complete coverage') + return gains, coverage + + +def dynamic_minimum_cheap(endpoints): + """Independent allocation DP: no marginal sorting or primary curve input.""" + require(0 < len(endpoints) <= 104, 'DP endpoint count') + limit = 2 * len(endpoints) + unreachable = 1 + sum(d for d, _ in endpoints) + costs = [0] + [unreachable] * limit + for index, (demand, capacity) in enumerate(endpoints): + require(0 < capacity < demand <= 2 * capacity <= 60, 'DP endpoint bounds') + updated = [unreachable] * (limit + 1) + for used in range(2 * index + 1): + for added in range(3): + value = costs[used] + max(0, demand - added * capacity) + updated[used + added] = min(updated[used + added], value) + costs = updated + require(costs[0] == sum(d for d, _ in endpoints) and costs[-1] == 0, + 'DP endpoint cases') + return costs + + +def allocation(gains, units, endpoints): + require(0 <= units <= len(gains) == 2 * len(endpoints), 'allocation size') + assigned = [0] * len(endpoints) + for _, index, _ in gains[:units]: + assigned[index] += 1 + return [[u, max(0, demand - capacity * u)] + for u, (demand, capacity) in zip(assigned, endpoints, strict=True)] + + +def calculate(): + inputs, predecessor = authenticated_inputs() + data = endpoint_data(paths(inputs['LOWRANK-WITNESS.json']), + ports(inputs['P104-FIXTURE.json'])) + result = {} + for orientation, pair in zip(('arrival', 'departure'), data, strict=True): + endpoints = census(*pair) + old = predecessor[orientation + '_endpoints'] + require(endpoints == [(x['residual'], x['proper_max']) for x in old], + 'original word agrees with every predecessor endpoint') + gains, coverage = marginal_certificate(endpoints) + costs = dynamic_minimum_cheap(endpoints) + require(costs == [4656 - c for c in coverage], 'all 209 DP and greedy values') + minimum = min(u for u, cheap in enumerate(costs) if u + cheap <= 400) + require(minimum == 192 and costs[147] == 937 and coverage[147] == 3719, + 'literal rejection and threshold') + require(253 + 30 * 147 == 4663 and 3719 + 253 == 3972 < 4656, + 'aggregate passes while saturation fails') + result[orientation] = { + 'endpoint_types': [list(k) + [v] + for k, v in sorted(Counter(endpoints).items())], + 'minimum_cheap_by_units': costs, + 'profile_253_147': {'maximum_coverage': 3972, 'deficit': 684}, + 'minimum_units_at_400': minimum, + 'relaxed_assignment_at_threshold': allocation(gains, minimum, endpoints), + 'threshold_cheap': costs[minimum], + } + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = calculate() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + require(json.dumps(result, sort_keys=True) == json.dumps( + read_json(PACKAGE / 'RESULT.json'), sort_keys=True), + 'typed receipt equality') + print('PASS_P104_ENDPOINT_SATURATION deficit=684 minimum_units_at_400=192') + + +if __name__ == '__main__': + main()