diff --git a/research/staged544-joint-price-region/MODEL.json b/research/staged544-joint-price-region/MODEL.json new file mode 100644 index 0000000000..d2e07225e3 --- /dev/null +++ b/research/staged544-joint-price-region/MODEL.json @@ -0,0 +1,181 @@ +{ + "a": "1730578437266246818741/1000000000000000000000000", + "widths": [ + 4, + 5, + 6, + 7, + 8, + 9 + ], + "capacities": [ + 8, + 16, + 32, + 48 + ], + "demands": [ + 234, + 18, + 162, + 477, + 864, + 1917 + ], + "bins": [ + 672, + 448, + 448, + 448 + ], + "basis": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 5 + ] + ] + ], + "extras": [ + [ + 16, + [ + 0, + 0, + 0, + 0, + 2, + 0 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 4, + 0 + ] + ] + ], + "flows": [ + 5, + 6, + 7, + 8, + 9 + ], + "expected_axis_ranges": [ + "18", + "48", + "88/3", + "30", + "48" + ] +} diff --git a/research/staged544-joint-price-region/ORIGINS.json b/research/staged544-joint-price-region/ORIGINS.json new file mode 100644 index 0000000000..1a257baeee --- /dev/null +++ b/research/staged544-joint-price-region/ORIGINS.json @@ -0,0 +1,26 @@ +[ + { + "file": "retained/3815-ceiling_certificate.py", + "pr": 3815, + "head": "77ffbf287b6ca198b4a31e3835db3bae60718b93", + "path": "research/staged544-clock-ceiling/ceiling_certificate.py", + "sha256": "2276f1c5d341db63dcf511f6398733b1efbe9d09e2e9aa86b50d7a160a0f7d03", + "git_blob": "e447b15b8bc341b4234c60d23c099a3215492dec" + }, + { + "file": "retained/3862-PROOF.md", + "pr": 3862, + "head": "b12d58d7b391b0d8490d6ebebe5cd0d4f57653b6", + "path": "research/staged544-width-lever-screen/PROOF.md", + "sha256": "559cf2463627f91e107ed5cb09e52009d79c18865c8eac9d1cab80d4b54e985b", + "git_blob": "8cb38dbe7d9f31322c5589fdab592fe7db8b8956" + }, + { + "file": "retained/3862-CERTIFICATE.json", + "pr": 3862, + "head": "b12d58d7b391b0d8490d6ebebe5cd0d4f57653b6", + "path": "research/staged544-width-lever-screen/CERTIFICATE.json", + "sha256": "712f3be06cf1425dd6640f390b78623dfda1de353370c3a28afa60dc4de1dbd7", + "git_blob": "0e1eb502339ce52d97688afcff535e540b36a577" + } +] diff --git a/research/staged544-joint-price-region/PROOF.md b/research/staged544-joint-price-region/PROOF.md new file mode 100644 index 0000000000..850fc31a43 --- /dev/null +++ b/research/staged544-joint-price-region/PROOF.md @@ -0,0 +1,170 @@ +# Complete sharp-price region in the frozen ideal + +All statements here use the fixed exponent +`a = 1730578437266246818741/10^24` and `h(l)=l^(1-a)`, with `h(0)=0`. +This is the upper endpoint used by Erwan Secousses in PR3815 and Sagar Thakrar +in PR3862. It is not a new root enclosure or a new kappa. + +## Model and exact dual face + +Per owner replica, demands for widths `(4,5,6,7,8,9)` are +`(234,18,162,477,864,1917)` and bin counts for capacities `(8,16,32,48)` are +`(672,448,448,448)`. Each helper fits wholly in one bin; the remainder is +paid as one child. Counts may be fractional. No clock, per-call collision, +restoration or physical staging condition is imposed in this relaxation. + +The objective is the sum of `h(remainder)` over all bins. The local paid +profile and live normalizer stay outside this objective and must be added +when pricing any real change. The model is retained from PR3815, following +dataisfire's PR3734 and zxv's PR3682. + +The ten columns of `MODEL.json` form an invertible matrix A: six helper +count rows followed by four bin count rows. The basis dual is the unique +solution `A^T lambda = h(remainders)`. Its closed form is independently +reconstructed in `independent.py`. Equivalently, with helper prices pi: + +``` +pi9 = (h(3)-h(48))/5 +pi8 = (3*pi9-h(5))/4 +pi7 = 2*pi8-pi9; pi6 = 3*pi8-2*pi9 +pi5 = -h(5); pi4 = 1-h(5) +mu8 = -pi8; mu16 = -2*pi8; mu32 = -4*pi8; mu48 = h(48) +``` + +For every feasible pattern p in a bin c its reduced cost is +`h(c-w.p)-pi.p-mu_c`. Both checkers enumerate all 2,551 integer count +patterns of widths 4..9 in these bins. Exactly twelve have identically zero +symbolic reduced cost: the ten basis columns plus `[8,8]@16` and +`[8,8,8,8]@32`. Every other pattern has a strictly positive outward rational +lower bound at this fixed exponent (minimum exceeds 0.0040545). This proves +both dual feasibility and completeness of this tight face. The check uses +symbolic identities for the zero cases, never a floating tolerance. + +PR3815/3862 solve a dual for outward rational lower approximations to h. +Here the symbolic dual uses the exact function h and interval arithmetic +certifies its inequalities. Its prices are consistent with their enclosures; +we do not claim bit-identical rational proxy prices or re-certify their root. + +The primary checker uses rational matrix elimination, Cartesian count-vector +enumeration and alternating negative-exponential bounds. The second uses +closed-form dual coordinates, ascending multisets and positive exponential +series followed by reciprocals. Neither imports or executes predecessor +code or the other checker. Logarithms use reduced atanh series with explicit +geometric tails; all rounding is outward. No numerical optimizer is needed. + +By weak duality, the common dual gives a lower bound for every packing of +any changed inventory with these bins. Equality occurs exactly when all +positive-count patterns belong to these twelve. Therefore feasibility on this +face is necessary and sufficient for the common price to be attained. + +## Eliminate the two extra columns + +For a changed demand vector d, let `y=A^-1(d,B)`. The extra `[8,8]@16` +column has basis coordinates `(0,1,0,0,0,1,0,-1,0,0)` and the extra +`[8,8,8,8]@32` column has coordinates `(0,0,0,0,0,2,0,-1,0,0)`. +If their counts are z1,z2, the basic counts are `y-D1*z1-D2*z2`. +All y coordinates except indices 1,5,7 must be nonnegative. The remaining +conditions are + +``` +z1,z2 >= 0; z1 <= y1; z1+2*z2 <= y5; y7+z1+z2 >= 0. +``` + +They are feasible exactly when +`y1>=0`, `y5>=0`, `y7+y5>=0`, `2*y7+y1+y5>=0`. +For sufficiency put `L=max(0,-y7)`, `z1=min(L,y1)`, `z2=L-z1`. +The last two inequalities respectively give `L<=y5` and `2L<=y1+y5`, +which imply `z1+2*z2<=y5`. This supplies an explicit rational packing. +Necessity follows by adding the displayed inequalities. The independent +checker eliminates the same face in a different set of direct count variables. + +## Joint adjacent inventory flows + +Let xj be the nonnegative number of helper-calls moved from width j to j-1, +for j=5,6,7,8,9, per owner replica. These are net inventory flows; if a literal +rewrite can touch each original helper only once it has additional availability +constraints. In particular x5<=18 must then be imposed separately. + +The changed demands are + +``` +(234+x5, 18-x5+x6, 162-x6+x7, 477-x7+x8, 864-x8+x9, 1917-x9). +``` + +Writing `S=x6+x7+x8+x9`, exact matrix elimination gives + +``` +y0=672; y1=448; y2=234+x5; y3=162-x6+x7; y4=18-x5+x6 +y5=15+(x6-x7-x8+x9)/2; y6=12-S/4 +y7=7-S/4+x8; y8=1916/5+S/20; y9=324/5-S/20. +``` + +Substituting into the previous feasibility conditions gives exactly + +``` +S <= 48 +x5 <= 18+x6 +x7+x8 <= 30+x6+x9 +3*x7 <= 88+x6+x8+x9. +``` + +All flows must also be nonnegative. There are no hidden additional inequalities: +the first makes y3>=114, y8>0, y9>=312/5, and +`2*y7+y1+y5=477-x7+x8>=429`. Other nontrivial conditions are exactly the +four displayed ones. The constructive formula above proves sufficiency for +every rational point, not merely the finite comparison grid. The argument +extends to real counts in the same fractional relaxation. + +If V0 is the incumbent idle cost and +`q=(h(48)-h(3)-5*h(5))/20`, throughout this region + +`V(d)-V0 = x5 + (x6+x7+x8+x9)*q`. + +Outside it no packing attains that common-dual value. The value remains a +lower bound; the model itself may also be infeasible for extreme inventories. +This is not a claim that PR3862 asserted simultaneous exactness outside its +ranges. Its single-basis ranges and global lower bound remain valid. + +## Sharp axial ranges and integral controls + +Setting all other flows to zero gives maximal xj: + +| Move | PR3862 sufficient single-basis range | Complete tight-face range | +|---|---:|---:| +| 5 to 4 | 18 | 18 | +| 6 to 5 | 28 | 48 | +| 7 to 6 | 28 | 88/3 | +| 8 to 7 | 30 | 30 | +| 9 to 8 | 28 | 48 | + +Each upper endpoint is attained by a nonnegative rational packing in +`RESULT.json`; each is forced by one of the joint inequalities, so it is +sharp for this price. At T360 all five endpoint witnesses have integer +aggregate helper and bin counts. This checks integrality of the clock-free +aggregate only, not a chronological owner assignment or per-call matching. + +## An actual coupled counterexample and a strict gap + +Take x6=x7=28, all other flows zero. Each change lies within the old individual +range, but S=56 and y6=-2. Since row 6 of A^-1 is nonnegative on every tight +column, this separates the changed demand from the whole twelve-column face. +An explicit feasible packing nevertheless exists: in 28 original +`[6,8,9,9]@32` bins shrink the 6 to 5, and in 28 `[7,9]@16` bins shrink +the 7 to 6. Both new remainders are 1. The resulting rational pattern counts +and all ten conservation equations are checked exactly; T360 clears them. + +Let delta be the certified minimum strictly positive reduced cost and M the +maximum negative magnitude of row 6 on any of the 2,551 columns. The row sum +-2 forces at least 2/M units of non-tight patterns. Consequently every feasible +packing has idle cost at least `common_dual + 2*delta/M`, strictly above the +putative linear price. `RESULT.json` supplies exact delta, M and this gap. +Thus the rejection is an objective obstruction, not a failed packing search. + +## Limits + +Only widths 4..9, fixed bins, fixed exponent and the paid-remainder objective +are certified. No all-concave or all-exponent optimality is asserted. Actual +staging signatures, circuit identities, dirty restoration, stock, source +access, chronology, collision rules, native/recursive invoices and both +supplier caps require their own admission. No full multiplication theorem, +formal proof-kernel check, selected-frontier change or new kappa is claimed. diff --git a/research/staged544-joint-price-region/README.md b/research/staged544-joint-price-region/README.md new file mode 100644 index 0000000000..916c25638b --- /dev/null +++ b/research/staged544-joint-price-region/README.md @@ -0,0 +1,138 @@ +# Exact joint width-price region for the staged544 ideal + +**New scoped result; no new kappa.** The complete optimal face at PR3815's +fixed exponent contains twelve packing patterns. The two columns outside +its chosen basis enlarge three of PR3862's sufficient price ranges: + +| Width move | Previous basis range | Sharp range, helper-calls per owner replica | +|---|---:|---:| +| 5 to 4 | 18 | 18 | +| 6 to 5 | 28 | 48 | +| 7 to 6 | 28 | 88/3 | +| 8 to 7 | 30 | 30 | +| 9 to 8 | 28 | 48 | + +For nonnegative adjacent inventory flows x5..x9, the common width prices are +attained exactly when + +``` +x6+x7+x8+x9 <= 48 +x5 <= 18+x6 +x7+x8 <= 30+x6+x9 +3*x7 <= 88+x6+x8+x9. +``` + +This is a complete region in the fractional, clock-free, fixed-bin relaxation, +at `a=0.001730578437266246818741`. It supplies constructive rational packings, +not a physical supplier. The counterexample x6=x7=28 fits each old individual +range but violates the joint region. An explicit feasible packing and a +strict positive objective gap certify the failure of simultaneous sharpness. +The original screen's global lower bound remains valid outside the region. + +This helps screen combinations of prospective staging changes before circuit +implementation. It does not establish that any extra staging exists or pays +its full physical costs. Net inventory flows can reuse newly produced widths; +disjoint changes to original helpers must additionally respect availability. + +## Evidence and reproducibility + +From the repository root, Python 3.12 standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/staged544-joint-price-region +``` + +Expected markers: `PASS_STAGED544_JOINT_PRICE_REGION`, +`PASS_INDEPENDENT_STAGED544_JOINT_PRICE_REGION` in the second JSON status, +`PASS_STAGED544_JOINT_REAL_CLI`, and registered outcome `completed`. +The package commands run with `-I -O -Werror -B`; no dependencies are installed. + +For one inventory query: + +```sh +python3.12 -I -O -B research/staged544-joint-price-region/verify.py --flows 0 48 0 0 0 +``` + +The JSON reports `sharp_common_price: true` and a twelve-column witness. +`--flows 0 28 28 0 0` reports false. Negative inventory or negative flows +are rejected. The script first checks the frozen complete certificate. + +[PROOF.md](PROOF.md) gives the universal linear elimination argument. +[RESULT.json](RESULT.json) contains exact outward bounds, boundary witnesses, +the separator, a non-tight feasible counterexample and semantic controls. +Two implementations separately classify all 2,551 patterns, with exactly +12 symbolic zero reduced costs and 2,539 strictly positive certificates. +They use different dual reconstruction, enumeration and exponential bounds; +neither imports the other checker or executes predecessor code. +Finite rational grids and actual CLI mutations are controls, not the proof +of the continuous region. All five axial boundary packings have integral +aggregate counts at T360; chronology and per-call ownership are untested. + +## Source pins, independence and overlap + +Canonical base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6; +repository OS assignment `a1fddd441a9e9145c53ad1534170023f`, independent +verification, refined card `independent-moment`. The older card's #2979 +mechanism now has live downstream audits; this session checks a new sharpness +implication in the changed-inventory relaxation rather than another moment root. + +Exact retained bytes, Git blob IDs, SHA256 and paths are in [ORIGINS.json](ORIGINS.json): + +- Erwan Secousses / ChaloupeMusic [PR3815](https://github.com/CrocSwap/integer-mult-bounds/pull/3815), + `77ffbf287b6ca198b4a31e3835db3bae60718b93`, basis/model source. +- Sagar Thakrar [PR3862](https://github.com/CrocSwap/integer-mult-bounds/pull/3862), + `b12d58d7b391b0d8490d6ebebe5cd0d4f57653b6`, proof and certificate for the + individual basis ranges and width-unit screen. +- The model comes through dataisfire [PR3734](https://github.com/CrocSwap/integer-mult-bounds/pull/3734), + `fa041037a3374eaa08feeca0b26a5d6893194147`, and zxv's PR3682. Their native + provider, owner fill and full admission are inherited context, not rerun here. + +Source constants are parsed with `ast.literal_eval` and compared to the model; +byte hashes are checked before mathematical execution. Retained source files +are data, never imported. All replay bytes are self-contained; no pending +Git objects or network access are required by the standalone checkers. +SOURCES.json pins the catalogue and selected record as historical provenance. + +Entry overlap checked all six pages of 592 live open PR bodies, recent #1166 +handoffs, the staging thread and the local overlap helper. The helper's remote +cache was missing; live API/browser reads supplied current coverage. Search API +results alone were incomplete, so the paginated inventory was used. This is +not exhaustive historical code-diff or every Discussion reply coverage. +PR3815 proves the incumbent ceiling; PR3862 prices widths and sufficient basis +ranges; PR3857/3875 refine/certify endpoints; PR3883 audits admission; PR3886 +excludes a single-ADD retiming class. None is relabelled as this joint-region +contribution. Frozen predecessors are unchanged. No record priority is claimed. + +## Scope and remaining obligations + +The completed claim concerns one fixed-exponent ideal packing LP and the exact +region where its common dual is sharp. It adds no endpoint digits or kappa. +Literal staging identities, local-profile compensation, arbitrary dirty +restoration, source access, stock, chronology, per-call collisions, physical +and recursive costs, inherited all-size/compiler/precision/analytic/BIT +assumptions, human review and proof-kernel acceptance remain open. +The selected construction and frontier are unchanged. The existing selected +baseline binding check was run; its full cold replay was unnecessary and unrun. + +## Open next questions + +1. Construct one actual width-6..9 staging inside the enlarged region. First + supply before/after words and the local-profile delta, then price them with + these constraints. Dirty restoration and the full physical bill are blockers. +2. Certify the next optimal face outside the region. The explicit coupled + counterexample supplies a feasible starting point and a separating row. + Its successor optimum and any physical implementation remain unknown. + +Structured relevance, first steps and blockers are in [TASK.json](TASK.json). + +## Credit and license + +New independent reconstruction and joint-region analysis by ToikY, with +substantial OpenAI Codex assistance, including a separate AI implementation +and adversarial review. No independent human or proof-kernel review is claimed. +Apache-2.0. Credit Erwan Secousses / ChaloupeMusic for PR3815's model and dual; +Sagar Thakrar for PR3862's width-price screen and basis ranges; dataisfire for +PR3734; zxv for PR3682; Ross Richardson for PR3605 staging; Jeremy Kothe and +the retained supplier lineage. hexapode's PR3795/3802 chronological allocations +retain their separate result and priority. Retained predecessor headers and +notices remain intact. diff --git a/research/staged544-joint-price-region/RESULT.json b/research/staged544-joint-price-region/RESULT.json new file mode 100644 index 0000000000..34661e1c3f --- /dev/null +++ b/research/staged544-joint-price-region/RESULT.json @@ -0,0 +1,306 @@ +{ + "status": "PASS_STAGED544_JOINT_PRICE_REGION", + "a": "1730578437266246818741/1000000000000000000000000", + "patterns": 2551, + "tight_patterns": 12, + "non_tight_patterns": 2539, + "strict_reduced_cost_lower": "8109175709263687263197190800539934312243687517013516117147554512876788079516669/2000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "axis_ranges_helper_calls_per_replica": [ + "18", + "48", + "88/3", + "30", + "48" + ], + "axis_witnesses": [ + { + "flow": [ + "18", + "0", + "0", + "0", + "0" + ], + "counts": [ + "672", + "448", + "252", + "162", + "0", + "15", + "12", + "7", + "1916/5", + "324/5", + "0", + "0" + ] + }, + { + "flow": [ + "0", + "48", + "0", + "0", + "0" + ], + "counts": [ + "672", + "443", + "234", + "114", + "66", + "34", + "0", + "0", + "1928/5", + "312/5", + "5", + "0" + ] + }, + { + "flow": [ + "0", + "0", + "88/3", + "0", + "0" + ], + "counts": [ + "672", + "1343/3", + "234", + "574/3", + "18", + "0", + "14/3", + "0", + "1154/3", + "190/3", + "1/3", + "0" + ] + }, + { + "flow": [ + "0", + "0", + "0", + "30", + "0" + ], + "counts": [ + "672", + "448", + "234", + "162", + "18", + "0", + "9/2", + "59/2", + "3847/10", + "633/10", + "0", + "0" + ] + }, + { + "flow": [ + "0", + "0", + "0", + "0", + "48" + ], + "counts": [ + "672", + "443", + "234", + "162", + "18", + "34", + "0", + "0", + "1928/5", + "312/5", + "5", + "0" + ] + } + ], + "sampled_flow_vectors": 6048, + "controls": [ + "outside-axis-5", + "outside-axis-6", + "outside-axis-7", + "outside-axis-8", + "outside-axis-9", + "joint-box-counterexample", + "extra-bin-count", + "negative-flow" + ], + "universal_affine_coefficients_checked": true, + "T360_integral_axis_boundaries": 5, + "box_counterexample": { + "flows": [ + "0", + "28", + "28", + "0", + "0" + ], + "separator": "-2", + "non_tight_separator_magnitude_bound": "12", + "idle_cost_gap_above_common_dual_lower": "8109175709263687263197190800539934312243687517013516117147554512876788079516669/12000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "feasible_patterns": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 5 + ] + ], + [ + 32, + [ + 0, + 1, + 0, + 0, + 1, + 2 + ] + ], + [ + 16, + [ + 0, + 0, + 1, + 0, + 0, + 1 + ] + ] + ], + "feasible_counts": [ + "672", + "420", + "234", + "134", + "18", + "15", + "12", + "7", + "1916/5", + "324/5", + "28", + "28" + ] + }, + "scope": "Fixed-exponent fractional fixed-bin ideal only; no physical implementation or new kappa." +} diff --git a/research/staged544-joint-price-region/SOURCES.json b/research/staged544-joint-price-region/SOURCES.json new file mode 100644 index 0000000000..0593d8fbd1 --- /dev/null +++ b/research/staged544-joint-price-region/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] +} diff --git a/research/staged544-joint-price-region/TASK.json b/research/staged544-joint-price-region/TASK.json new file mode 100644 index 0000000000..ab52ceb73a --- /dev/null +++ b/research/staged544-joint-price-region/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "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", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "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": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "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.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently source-bind and classify the complete fixed-exponent optimal packing face of PR3815; derive the simultaneous adjacent-width price-sharpness region and sharp axial ranges beyond PR3862 single-basis ranges.", + "scope_change_reason": "The historical2979 coordinated groups have downstream checks; live3815/3862 expose a new exactness obligation for changed inventories. This checks/completes a specific physical-ledger relaxation, not more digits or supplier admission.", + "bottleneck_link": "Determines when the staged544 width-price planning screen is attainable and when it is only a lower bound, before implementing changed helper inventories.", + "budget_minutes": 60, + "stop_rule": "Exactly the frozen widths4..9, bins8/16/32/48, fixed exponent and nonnegative adjacent inventory flows; no exploratory work after2026-10-19T03:33:02Z. No new endpoint/physical supplier claim.", + "outcome": "completed", + "evidence": "RESULT.json; verify.py; independent.py; exact rational witnesses and semantic/real-CLI controls.", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex assistance, including a separately implemented AI checker; no independent human or proof-kernel review claimed.", + "seed": "a1fddd441a9e9145c53ad1534170023f", + "open_questions": [ + { + "question": "Can a literal width-6..9 staging reach one of the newly sharp boundary inventories?", + "why_it_matters": "The price remains attainable in a larger relaxation domain, but only a physical circuit can exploit it.", + "first_step": "Supply one before/after literal word and local paid-profile change, then test the joint inequalities.", + "blocked_by": "Arbitrary dirty restoration, chronological owner hosting and complete physical invoice are unproved." + }, + { + "question": "What is the next optimal face outside this joint region?", + "why_it_matters": "The old dual remains a lower bound; a changed inventory outside the region needs a different sharp price.", + "first_step": "Use the explicit (x6,x7)=(28,28) feasible packing and separating row as calibration for an independently certified new dual.", + "blocked_by": "No successor-face optimum or physical construction is claimed." + } + ] +} diff --git a/research/staged544-joint-price-region/VERIFY.json b/research/staged544-joint-price-region/VERIFY.json new file mode 100644 index 0000000000..1afb8c4d7e --- /dev/null +++ b/research/staged544-joint-price-region/VERIFY.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-binding, complete tight-face classification, joint-region witnesses, strict coupled gap, exact axial boundaries and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Independent closed-form/multiset/positive-exponential proof and constructive region, T360 integer boundaries and controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_cli.py" + ], + "timeout_seconds": 120, + "checks": "Actual optimized CLI source/model/receipt mutations in disposable owned copies; original bytes unchanged." + } + ] +} diff --git a/research/staged544-joint-price-region/independent.py b/research/staged544-joint-price-region/independent.py new file mode 100644 index 0000000000..7ebd90ec99 --- /dev/null +++ b/research/staged544-joint-price-region/independent.py @@ -0,0 +1,322 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent fixed-exponent tight-face and adjacent-inventory-flow audit. + +The mathematical model and original dual are due to Erwan Secousses/PR3815, +dataisfire/PR3734 and zxv/PR3682. Sagar Thakrar/PR3862 supplies the individual +basis-range interpretation. This checker imports no predecessor or companion +checker. It uses closed-form dual coordinates, ascending multiset enumeration, +positive exponential series with reciprocals, and a constructive closed-form +description of every feasible point on the twelve-column tight face. +""" +from fractions import Fraction as Q +from functools import lru_cache +import json +from pathlib import Path + +WIDTHS = (4, 5, 6, 7, 8, 9) +CAPACITIES = (8, 16, 32, 48) +EXPONENT = Q(1730578437266246818741, 10**24) +SCALE = 10**100 +EXPECTED_TIGHT = { + (8, (0, 0, 0, 0, 1, 0)), + (16, (0, 0, 0, 0, 2, 0)), + (16, (0, 0, 0, 1, 0, 1)), + (32, (0, 0, 0, 0, 0, 3)), + (32, (0, 0, 0, 0, 4, 0)), + (32, (0, 0, 0, 1, 2, 1)), + (32, (0, 0, 0, 2, 0, 2)), + (32, (0, 0, 1, 0, 1, 2)), + (32, (0, 1, 0, 0, 0, 3)), + (32, (1, 0, 0, 0, 0, 3)), + (48, (0, 0, 0, 0, 0, 0)), + (48, (0, 0, 0, 0, 0, 5)), +} + + +def require(ok, why): + if not ok: + raise ValueError(why) + + +def check_model(model): + expected = {'a', 'widths', 'capacities', 'demands', 'bins', 'basis', + 'extras', 'flows', 'expected_axis_ranges'} + require(type(model) is dict and set(model) == expected, 'model fields') + require(Q(model['a']) == EXPONENT, 'fixed exponent source') + require(model['widths'] == list(WIDTHS), 'model widths') + require(model['capacities'] == list(CAPACITIES), 'model capacities') + require(model['demands'] == [234, 18, 162, 477, 864, 1917], 'model inventory') + require(model['bins'] == [672, 448, 448, 448], 'model bins') + require(model['flows'] == [5, 6, 7, 8, 9], 'model adjacent flows') + require(model['expected_axis_ranges'] == ['18', '48', '88/3', '30', '48'], + 'model claimed ranges') + extras = {(16, (0, 0, 0, 0, 2, 0)), (32, (0, 0, 0, 0, 4, 0))} + for key, wanted in [('extras', extras), ('basis', EXPECTED_TIGHT-extras)]: + require(type(model[key]) is list and len(model[key]) == len(wanted), + 'model column count') + converted = set() + for cap, counts in model[key]: + require(type(cap) is int and type(counts) is list + and len(counts) == 6 and all(type(v) is int and v >= 0 for v in counts), + 'model column domain') + converted.add((cap, tuple(counts))) + require(converted == wanted, 'model tight columns') + + +def rounded_interval(lo, hi): + require(lo <= hi, 'interval order') + return Q(lo.numerator * SCALE // lo.denominator, SCALE), Q( + -((-hi.numerator * SCALE) // hi.denominator), SCALE) + + +def logarithm(x): + """Atanh expansion: 120 positive terms and a geometric tail bound.""" + require(Q(1) <= x <= Q(2), 'log reduction domain') + z = (x - 1) / (x + 1) + term, total = z, Q(0) + for j in range(120): + total += 2 * term / (2*j + 1) + term *= z*z + return total, total + 2 * term / (241 * (1-z*z)) + + +def exponential(x): + """Positive Taylor terms; bound the remaining ratios by x/42.""" + require(Q(0) <= x < Q(1, 100), 'positive exp domain') + term = total = Q(1) + for j in range(1, 41): + term *= x / j + total += term + next_term = term * x / 41 + return total, total + next_term / (1 - x / 42) + + +@lru_cache(None) +def power_interval(rank): + require(type(rank) is int and 0 <= rank <= 48, 'power rank') + if rank in (0, 1): + return Q(rank), Q(rank) + shift = rank.bit_length() - 1 + a, b = logarithm(Q(rank, 1 << shift)) + c, d = logarithm(Q(2)) + low, high = rounded_interval(a + shift*c, b + shift*d) + el, _ = exponential(EXPONENT * low) + _, eh = exponential(EXPONENT * high) + return rounded_interval(Q(rank) / eh, Q(rank) / el) + + +def add(*terms): + result = {} + for factor, vector in terms: + for rank, coefficient in vector.items(): + result[rank] = result.get(rank, Q(0)) + factor * coefficient + return {rank: value for rank, value in result.items() if value} + + +def atom(rank): + return {rank: Q(1)} if rank else {} + + +def dual(): + p9 = add((Q(1, 5), atom(3)), (-Q(1, 5), atom(48))) + p8 = add((Q(3, 4), p9), (-Q(1, 4), atom(5))) + pi = { + 9: p9, 8: p8, 7: add((2, p8), (-1, p9)), + 6: add((3, p8), (-2, p9)), + 5: add((-1, atom(5))), 4: add((1, atom(1)), (-1, atom(5))), + } + mu = {8: add((-1, p8)), 16: add((-2, p8)), + 32: add((-4, p8)), 48: atom(48)} + return pi, mu + + +def multiset_patterns(capacity): + """Emit each ascending width multiset once, without count-bound recursion.""" + counts = [0] * len(WIDTHS) + + def visit(start, used): + yield tuple(counts) + for index in range(start, len(WIDTHS)): + width = WIDTHS[index] + if used + width <= capacity: + counts[index] += 1 + yield from visit(index, used + width) + counts[index] -= 1 + yield from visit(0, 0) + + +def residual(capacity, counts, pi, mu): + remaining = capacity - sum(w*n for w, n in zip(WIDTHS, counts)) + return add((1, atom(remaining)), (-1, mu[capacity]), + *((-n, pi[w]) for w, n in zip(WIDTHS, counts))) + + +def evaluate(vector): + lo = hi = Q(0) + for rank, coefficient in vector.items(): + a, b = power_interval(rank) + lo += coefficient * (a if coefficient >= 0 else b) + hi += coefficient * (b if coefficient >= 0 else a) + return lo, hi + + +def demand(flow): + x5, x6, x7, x8, x9 = map(Q, flow) + return (234+x5, 18-x5+x6, 162-x6+x7, + 477-x7+x8, 864-x8+x9, 1917-x9) + + +def region(flow): + x5, x6, x7, x8, x9 = map(Q, flow) + return (min(flow) >= 0 and x5 <= 18+x6 + and x6+x7+x8+x9 <= 48 + and x7+x8 <= 30+x6+x9 + and 3*x7 <= 88+x6+x8+x9) + + +def face_parameters(d): + a, b, c, d7, d8, d9 = map(Q, d) + k = d7 - 448 + ell = (d8 - 672 - c) / 2 + g = 448 - a - b - c - (k + ell)/2 + z = (d9 - d7 - 3*a - 3*b - 2*c - 3*g) / 5 + feasible = (min(a, b, c, g) >= 0 and 0 <= z <= 448 + and max(Q(0), -k) <= min(Q(448), ell)) + return feasible, (a, b, c, k, ell, g, z) + + +def check_witness(rows, d): + require(set(rows) == EXPECTED_TIGHT, 'witness support') + require(min(rows.values()) >= 0, 'nonnegative witness') + require(tuple(sum(value*pattern[i] for (_, pattern), value in rows.items()) + for i in range(6)) == tuple(d), 'helper demand witness') + require({cap: sum(value for (c0, _), value in rows.items() if c0 == cap) + for cap in CAPACITIES} == {8: 672, 16: 448, 32: 448, 48: 448}, + 'bin demand witness') + + +def witness(d): + feasible, (a, b, c, k, ell, g, z) = face_parameters(d) + require(feasible, 'demand outside twelve-column face') + u = max(Q(0), -k) + e = max(Q(0), u + (k-ell)/2) + rows = { + (8, (0, 0, 0, 0, 1, 0)): Q(672), + (16, (0, 0, 0, 0, 2, 0)): u, + (16, (0, 0, 0, 1, 0, 1)): 448-u, + (32, (0, 0, 0, 0, 0, 3)): g, + (32, (0, 0, 0, 0, 4, 0)): (ell-k)/2-u+e, + (32, (0, 0, 0, 1, 2, 1)): k+u-2*e, + (32, (0, 0, 0, 2, 0, 2)): e, + (32, (0, 0, 1, 0, 1, 2)): c, + (32, (0, 1, 0, 0, 0, 3)): b, + (32, (1, 0, 0, 0, 0, 3)): a, + (48, (0, 0, 0, 0, 0, 0)): 448-z, + (48, (0, 0, 0, 0, 0, 5)): z, + } + check_witness(rows, d) + return rows + + +def rejected(call, message): + try: + call() + except ValueError: + return message + raise ValueError('control accepted: ' + message) + + +def main(): + package = Path(__file__).resolve().parent + model = json.loads((package / 'MODEL.json').read_text()) + check_model(model) + pi, mu = dual() + tight, strict, total = set(), [], 0 + for cap in CAPACITIES: + seen = set() + for p in multiset_patterns(cap): + require(p not in seen, 'duplicate multiset') + seen.add(p) + total += 1 + rc = residual(cap, p, pi, mu) + if not rc: + tight.add((cap, p)) + else: + lo, hi = evaluate(rc) + require(lo > 0, 'strict reduced cost enclosure') + strict.append((lo, hi, cap, p)) + require(total == 2551 and tight == EXPECTED_TIGHT, 'complete tight face') + maxima = (Q(18), Q(48), Q(88, 3), Q(30), Q(48)) + tested = whole_bin_boundaries = 0 + for i, maximum in enumerate(maxima): + for value in (Q(0), maximum/2, maximum): + flow = [Q(0)]*5 + flow[i] = value + require(region(flow), 'axis boundary region') + require(face_parameters(demand(flow))[0], 'axis closed-form feasibility') + rows = witness(demand(flow)) + tested += 1 + if value == maximum: + require(all((360*count).denominator == 1 for count in rows.values()), + 'T360 whole-bin axis boundary') + require(all((360*count).denominator == 1 for count in demand(flow)), + 'T360 whole-helper axis boundary') + whole_bin_boundaries += 1 + flow[i] = maximum + Q(1, 1000) + require(not region(flow) and not face_parameters(demand(flow))[0], + 'axis beyond maximum rejected') + simultaneous = (Q(0), Q(28), Q(28), Q(0), Q(0)) + require(not region(simultaneous), 'simultaneous individual ranges control') + require(face_parameters(demand(simultaneous))[1][5] == -2, + 'simultaneous obstruction is minus two rank32 triple9 columns') + controls = [rejected(lambda: witness(demand(simultaneous)), + 'joint_28_28_outside_tight_face')] + altered = dict(pi) + altered[9] = add((1, pi[9]), (Q(1, 10**30), atom(1))) + lo, hi = evaluate(residual(16, (0, 0, 0, 1, 0, 1), altered, mu)) + require(hi < 0, 'dual perturbation semantic rejection') + controls.append('width9_dual_increased_1e-30') + for key, value, label in [ + ('a', '1/2', 'changed_exponent'), + ('demands', [234, 18, 162, 478, 864, 1917], 'changed_inventory'), + ('expected_axis_ranges', ['18', '49', '88/3', '30', '48'], 'inflated_range'), + ('extras', model['extras'][:1], 'missing_extra_tight_column'), + ]: + changed = dict(model) + changed[key] = value + controls.append(rejected(lambda changed=changed: check_model(changed), label)) + zero = (Q(0),)*5 + changed_rows = witness(demand(zero)) + changed_rows[(8, (0, 0, 0, 0, 1, 0))] += Q(1, 2) + controls.append(rejected(lambda: check_witness(changed_rows, demand(zero)), + 'changed_witness_half_bin')) + # Exhaust finite rational test points of the equivalence and constructive map. + from itertools import product + grid = (Q(0), Q(1), Q(18), Q(28), Q(30), Q(48)) + inside = outside = 0 + for flow in product(grid, repeat=5): + accepted = region(flow) + require(accepted == face_parameters(demand(flow))[0], 'region equivalence grid') + if accepted: + witness(demand(flow)) + inside += 1 + else: + outside += 1 + minimum = min(strict) + result = { + 'status': 'PASS_INDEPENDENT_STAGED544_JOINT_PRICE_REGION', + 'exponent': str(EXPONENT), 'patterns': total, + 'symbolically_tight_patterns': len(tight), + 'strict_patterns': len(strict), + 'minimum_strict_reduced_cost_lower': str(minimum[0]), + 'axis_maxima_x5_to_x9': [str(x) for x in maxima], + 'axis_witnesses': tested, + 'T360_integral_axis_boundaries': whole_bin_boundaries, + 'region_grid_inside': inside, 'region_grid_outside': outside, + 'negative_controls': controls, + } + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/staged544-joint-price-region/retained/3815-ceiling_certificate.py b/research/staged544-joint-price-region/retained/3815-ceiling_certificate.py new file mode 100644 index 0000000000..e447b15b8b --- /dev/null +++ b/research/staged544-joint-price-region/retained/3815-ceiling_certificate.py @@ -0,0 +1,90 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact dual certificate: no owner fill of the staged544 inventory beats the ideal root. + +Inventory per owner replica (PR3734 template and native supplier, any clock, any replica +count T): nine calls of 408 helpers with widths {4:26, 5:2, 6:18, 7:53, 8:96, 9:213}; idle +bins 672 of rank 8, 448 of rank 16, 448 of rank 32, 448 of rank 48; local paid profile +{1:2440, 2:725, 3:224, 4:102, 5:20, 8:8} per call; 896 live families of rank 73. Every +helper occupies its width in one idle bin and each bin's remainder l > 0 is paid as one +rank-l child (owner_audit.py). + +The root is unique: F(a) = sum n_r r^(1-a) - 896 T 73^(1-a) has the sign of +G(a) = sum n_r r (73/r)^a - 65408 T, strictly increasing because every paid rank is < 73. +So "root < a_hi" is "F(a_hi) > 0". F(a_hi) is linear in the bin pattern counts y, so for +any dual (pi, mu) with pi . p + mu_c <= h(l_p) for every pattern p of every rank c, weak +duality gives sum y h(l) >= sum_c mu_c B_c + sum_w pi_w 9 s_w for every packing, integer or +not, with or without time windows or the one-helper-per-call-per-bin rule. The dual is the +exact solution on the ten patterns of the fixed-inventory ideal, with outward rational +enclosures of r^(1-a) from PR3734 rational_price.py. Standard library only. +""" +from fractions import Fraction as Q + +W = (4, 5, 6, 7, 8, 9) +SUPPLY = (26, 2, 18, 53, 96, 213) # helpers per call +BINS = {8: 672, 16: 448, 32: 448, 48: 448} # idle bins per owner replica +LOCAL = {1: 2440, 2: 725, 3: 224, 4: 102, 5: 20, 8: 8} +CAPS = (8, 16, 32, 48) +# the ten patterns of the fixed-inventory ideal (counts of widths 4..9) +BASIS = [(8, (0, 0, 0, 0, 1, 0)), (16, (0, 0, 0, 1, 0, 1)), (32, (1, 0, 0, 0, 0, 3)), + (32, (0, 0, 1, 0, 1, 2)), (32, (0, 1, 0, 0, 0, 3)), (32, (0, 0, 0, 1, 2, 1)), + (32, (0, 0, 0, 0, 0, 3)), (32, (0, 0, 0, 2, 0, 2)), (48, (0, 0, 0, 0, 0, 0)), + (48, (0, 0, 0, 0, 0, 5))] + + +def patterns(cap): + out = [] + + def rec(i, rest, cur): + if i == len(W): + out.append(tuple(cur)) + return + for k in range(rest // W[i] + 1): + rec(i + 1, rest - k * W[i], cur + [k]) + rec(0, cap, []) + return out + + +def left(cap, p): + return cap - sum(k * w for k, w in zip(p, W)) + + +def solve(A, b): + """Exact Gaussian elimination over the rationals.""" + n = len(A) + M = [[Q(x) for x in row] + [Q(y)] for row, y in zip(A, b)] + for c in range(n): + piv = next(r for r in range(c, n) if M[r][c] != 0) + M[c], M[piv] = M[piv], M[c] + for r in range(n): + if r != c and M[r][c] != 0: + f = M[r][c] / M[c][c] + M[r] = [x - f * y for x, y in zip(M[r], M[c])] + return [M[i][n] / M[i][i] for i in range(n)] + + +def certify(R, a, perturb=Q(0)): + """Lower bound on min over all packings of F(a) per owner replica, with its dual. + + R is PR3734 rational_price module; lower enclosures of h keep the bound valid. + perturb shifts the width-9 dual after solving (a control: feasibility must then fail).""" + a = Q(a) + h = {l: R.h_bounds(l, a)[0] for l in range(1, 49)} + cost = lambda cap, p: h[left(cap, p)] if left(cap, p) else Q(0) # noqa: E731 + rows, rhs = [], [] + for cap, p in BASIS: + rows.append(list(p) + [1 if cap == c else 0 for c in CAPS]) + rhs.append(cost(cap, p)) + sol = solve(rows, rhs) + pi, mu = sol[:6], dict(zip(CAPS, sol[6:])) + pi[5] += perturb + worst = None + for cap in CAPS: + for p in patterns(cap): + rc = cost(cap, p) - sum(x * k for x, k in zip(pi, p)) - mu[cap] + if worst is None or rc < worst[0]: + worst = (rc, cap, p) + dual = sum(mu[c] * BINS[c] for c in CAPS) + sum(x * 9 * s for x, s in zip(pi, SUPPLY)) + local = sum(9 * n * R.h_bounds(r, a)[0] for r, n in LOCAL.items()) + live = 896 * R.h_bounds(73, a)[1] + return dict(min_reduced_cost=worst[0], worst_pattern=(worst[1], worst[2]), dual_feasible=worst[0] >= 0, + lower_bound=local + dual - live, patterns=sum(len(patterns(c)) for c in CAPS)) diff --git a/research/staged544-joint-price-region/retained/3862-CERTIFICATE.json b/research/staged544-joint-price-region/retained/3862-CERTIFICATE.json new file mode 100644 index 0000000000..0e1eb50233 --- /dev/null +++ b/research/staged544-joint-price-region/retained/3862-CERTIFICATE.json @@ -0,0 +1,658 @@ +{ + "note": "Bases found by the HiGHS cross-check (crosscheck_highs.py); verify.py re-derives primal and dual exactly and checks optimality. Count vectors are indexed by widths 1..9.", + "ceiling": { + "a_lo": "0.001730578437266246818740", + "a_hi": "0.001730578437266246818741", + "source": "PR3815 ceiling_certificate.py root_upper / PR3734 ideal root, rechecked here" + }, + "bases": { + "staged544": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 5 + ] + ] + ], + "pr3682": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 5 + ] + ] + ], + "width_only": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 5 + ] + ] + ], + "local_only": [ + [ + 8, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + [ + 16, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 1, + 0, + 0, + 0, + 3 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 1, + 0, + 1, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 0, + 2 + ] + ], + [ + 32, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2, + 1 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ], + [ + 48, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 5 + ] + ] + ] + }, + "profiles": { + "pr3682_finite": { + "T": 360, + "source": "PR3682 431e6c60 research/staged-donor-release/LEAD1-PRICE.json profile", + "histogram": { + "1": 7980120, + "2": 2345760, + "3": 755730, + "4": 330480, + "5": 69930, + "8": 25920, + "48": 137790 + } + }, + "pr3734_finite": { + "T": 360, + "source": "PR3734 fa041037 research/staged544-producer-return/inputs/PROFILE.json", + "histogram": { + "1": 7990332, + "2": 2349000, + "3": 748971, + "4": 330480, + "5": 69479, + "8": 25920, + "32": 1, + "48": 137911 + } + }, + "pr3815_clock_fill": { + "T": 360, + "source": "PR3815 77ffbf28 research/staged544-clock-ceiling/inputs/PROFILE.json", + "histogram": { + "1": 7989840, + "2": 2349000, + "3": 749088, + "4": 330480, + "5": 69120, + "8": 25920, + "48": 137952 + } + } + }, + "predecessor_sources": [ + { + "pr": 3734, + "head": "fa041037a3374eaa08feeca0b26a5d6893194147", + "path": "research/staged544-producer-return/PROOF.md", + "sha256": "be5fa8e381da957d52d02b154e2420f4459d7c8b30e23e82e245c11c978e3b62" + }, + { + "pr": 3734, + "head": "fa041037a3374eaa08feeca0b26a5d6893194147", + "path": "research/staged544-producer-return/inputs/PROFILE.json", + "sha256": "06b4e2abe8d56b49bad3bdc8f8504082404b40609d548fa8de2618eb7373fd48" + }, + { + "pr": 3815, + "head": "77ffbf287b6ca198b4a31e3835db3bae60718b93", + "path": "research/staged544-clock-ceiling/ceiling_certificate.py", + "sha256": "2276f1c5d341db63dcf511f6398733b1efbe9d09e2e9aa86b50d7a160a0f7d03" + }, + { + "pr": 3815, + "head": "77ffbf287b6ca198b4a31e3835db3bae60718b93", + "path": "research/staged544-clock-ceiling/inputs/PROFILE.json", + "sha256": "9686df0d8e710c2e94aef3887f4bf130a05b64215faeae702cccb59e95a469d5" + }, + { + "pr": 3682, + "head": "431e6c6023ef352c41696469de7fb614cd4ded8c", + "path": "research/staged-donor-release/PROOF.md", + "sha256": "89ce2b0aa2dcf84ebcab04aedc451420815bc48af25c69998594910e9976a31b" + }, + { + "pr": 3682, + "head": "431e6c6023ef352c41696469de7fb614cd4ded8c", + "path": "research/staged-donor-release/LEAD1-PRICE.json", + "sha256": "217dfc6b0c243d5387f50b23d0a5a389754df702ea1d810aea46a6f3d81617bc" + } + ] +} diff --git a/research/staged544-joint-price-region/retained/3862-PROOF.md b/research/staged544-joint-price-region/retained/3862-PROOF.md new file mode 100644 index 0000000000..8cb38dbe7d --- /dev/null +++ b/research/staged544-joint-price-region/retained/3862-PROOF.md @@ -0,0 +1,175 @@ +# Proof: priced width screen for the staged544 fixed-T360 ideal + +All numbers are printed by `verify.py`. Units are per owner replica; one +"helper-call" is one helper in one of the nine calls. + +## 1. Model and sign lemma + +Inventory per replica (PR3734 head `fa041037`, PR3815 head `77ffbf28`): `9 s_w` +helper-calls of hosted width `w`, with `s = {4:26,5:2,6:18,7:53,8:96,9:213}`; +idle bins `B = {8:672,16:448,32:448,48:448}`; local per-call profile +`n = {1:2440,2:725,3:224,4:102,5:20,8:8}`; 896 live rank-73 families. A +packing puts each helper-call into one bin; a bin pattern `p` (counts `p_w`) of +capacity `c` leaves `l_p = c - sum_w w p_w >= 0`, paid as one rank-`l_p` child +when `l_p > 0`. With `h(l) = l^(1-a)` and `h(0) = 0`, + +`F(a) = 9 sum_r n_r h(r) + sum_p y_p h(l_p) - 896 h(73)`. + +As in PR3815, `F(a) = 73^(-a) (sum N_r r (73/r)^a - 65408)`, where `N_r` is +the full paid histogram (local children and bin remainders), and every paid rank +is below 73, so `F` has one root and "root < a" iff `F(a) > 0`. This holds for +every inventory and local profile below (all paid ranks stay at most 48), for +integer or fractional `y`, and for any clock: the clock only restricts `y`. + +`V(s', a) = min sum_p y_p h(l_p)` over `y >= 0` with `sum_p y_p p_w = 9 s'_w` +for every width and `sum_{p in c} y_p = B_c`. The ideal ceiling of an +inventory `s'` and profile `n'` is the root of +`9 sum n'_r h(r) + V(s', a) - 896 h(73)`. + +`h` is enclosed outwardly (`h_lo <= h <= h_hi`, width below 1e-85): `ln l` +from the `atanh` series with a geometric tail bound, `exp(-u)` from alternating +partial sums, and outward rounding to 1e-90. + +## 2. Staged544 ceiling bracket + +The ten patterns found by HiGHS equal PR3815's basis. Their exact primal is +`y >= 0`; the smallest entry is 7. With `h_hi`, `F(a_lo) <= -1.31e-19` at +`a_lo = 0.001730578437266246818740`. Solving the same basis for `(pi, mu)` with +`h_lo` at `a_hi = 0.001730578437266246818741` gives `F(a_hi) >= 5.28e-20`. +This reproduces PR3815's bracket with an independent enclosure. It is not a +new result. + +## 3. Weak-duality screen, prices and the monotone-price lemma + +`(pi_4..pi_9, mu)` is PR3815's basis dual (its `ceiling_certificate.py` solves +it), here solved exactly with `h_lo` at `a_hi`. Let `pi_w` (w = 1..9) and +`mu_c` satisfy + +(D) `sum_w pi_w p_w + mu_c <= h_lo(l_p)` for **every** pattern of widths 1..9 +in every bin (318,840 patterns). + +Then for any inventory `s'` over widths 1..9 (fractional or not) and any +local profile `n'`, every packing satisfies + +`F'(a_hi) >= 9 sum_r n'_r h_lo(r) + 9 sum_w pi_w s'_w + sum_c mu_c B_c - 896 h_hi(73).` (*) + +Proof: multiply (D) by `y_p >= 0`, sum, and use the two equality constraints. +Moving `z` helper-calls from width `w` to `v < w` changes the right side of (*) +by `z (pi_v - pi_w)`; changing the local profile changes it by +`9 sum (n'_r - n_r) h_lo(r)`. + +**Two extensions.** `verify.py` uses two duals that agree on widths 4..9: + +- the *cheapest* extension `pi_1 = pi_2 = pi_3 = pi_4` (printed as + `helper_pi`), used for the lemma below; +- the *tight* extension: `pi_3`, then `pi_2`, then `pi_1` raised to the + largest values keeping (D). Its limiting patterns are: + `3 + 5*9 = 48` limits `pi_3`, `2 + 5*9 = 47` (leftover 1) limits `pi_2`, and + `1 + 4 + 3*9 = 32` limits `pi_1`. It gives the 4->v prices. + +Both satisfy (D) on all 318,840 patterns with minimum reduced cost exactly 0, +by enumeration and by an unbounded-knapsack recursion over used volume. + +**Slack lemma.** If (D) holds on the 2,551 width-4..9 patterns and +`pi_4 <= -3`, the cheapest extension satisfies (D) on all width-1..9 patterns. +Proof: take a pattern `p` with `s` helpers of width at most 3 and total width +`v <= 3s`, leftover `l`. Removing them gives a width-4..9 pattern `p'` with +leftover `l + v`. Since `h` is concave with `h(0) = 0` and `h(1) = 1`, +`h(l + v) - h(l) <= h(v) <= v`. So +`RC(p) = RC(p') + h(l) - h(l + v) - s pi_4 >= RC(p') + s(-pi_4 - 3) >= 0`. +Here `pi_4 = 1 - h(5)` and the margin `-pi_4 - 3 = 0.986093083432664503980103` +dwarfs the enclosure width. The 318,840-pattern enumeration is a second check +of this lemma and is needed only for the tight extension. + +**Monotone-price lemma (free reductions).** The cheapest extension is +nonincreasing in width and every `pi_w <= 0`. So any width reduction (to any +width `>= 1`, or unhosting) with an unchanged local profile keeps +`F(a_hi) >= 5.28e-20 > 0`: it keeps the ideal ceiling below `a_hi`. Under the +conservation of section 4 such a move is not realizable; the lemma is a +statement about the model, not a staging closure. + +**Prices.** The value `V` is convex in the right-hand side, so a price is a lower +bound for every further unit in that direction; inside the listed range the +same basis stays primal feasible and the price is exact. + +| move | exact price at a_hi | closed form | range (helper-calls per replica) | +|---|---|---|---| +| 9->8, 8->7, 7->6, 6->5 | 0.987736781185353068089966 | `(h(48)-h(3)-5h(5))/20` | 28, 30, 28, 28 | +| 5->4 | 1 | `h(1)-h(0)`; `[9,9,9,5]` and `[9,9,9,4]` are both basic | 18 | +| 4->3 | 0.991791369039984911721564 | `h(5)-h(3)-1` | 324/5 | + +The 6..9 closed form is PR3682's 8->7 width shadow (`price.py`); the dual is +affine on widths 5..9, so the same price holds for every step there. For 4->3, +add the column `[3,9^5]` (48-bin), which has reduced cost 0 under the tight +extension. Moving `k` units along `+[3,9^5] - [4,9,9,9] + [9,9,9] - [9^5]` +keeps every bin and width row except `3` and `4` fixed, all four columns are +tight, and the basic entries `y[4,9,9,9] = 234` and `y[9^5] = 324/5` stay +nonnegative for `k <= 324/5`. By complementary slackness the change in `V` is +exactly `k (pi_3 - pi_4) = k (h(5) - h(3) - 1)`. `verify.py` checks the +tightness, the cost and the range in exact arithmetic. HiGHS gives +0.9877367811860, 1.0 and 0.9917913690369 for single units of 8->7, 5->4 and +4->3, agreeing to about 3e-12. + +## 4. Per-call conservation and staging screens + +Per call, local paid rank minus hosted helper width is 1856 on both pinned +(inventory, local) pairs: staged544 `5134 - 3278` and PR3682 `5135 - 3279`. +With the bins this gives total paid rank `9*1856 + sum c B_c = 65088 = +896*73 - 320` per replica. PR3605 states the same conservation for its two +staging units ("the local rank mass falls by 2, exactly matching the +owned-width decrease"). The three pinned T360 profiles (PR3682 finite, PR3734 +finite, PR3815 clock fill) all total 23,431,680 = 65088 x 360; the last two +share one (inventory, local) pair, so for them this is implied arithmetic. +The conservation is observed, not proved. Where it holds, a reduction with an +unchanged local profile is not realizable: each width unit must remove one unit +of local paid rank. + +**Screens.** By (*), a width unit `w -> w-1` together with a local change of +saving `S` changes `F` by at least `price - S`, exactly within the ranges: + +- *Documented signature.* PR3605 derives the per-helper staging delta + `3H1 + H2 - 2H3`, i.e. `{1:+3,2:+1,3:-2}` (one pivot and two donor climbs). + PR3734's local change from PR3682 is the same delta (`verify.py` checks it). + All three observed units are 8->7 moves; for the other widths the screen assumes the same signature. + Its saving is `2h(3) - 3 - h(2) = 0.991001081580029037511288`. The gain per + width unit is +0.003264300394675969421322 for 6..9, + -0.008998918419970962488711 for 5->4 and -0.000790287459955874210276 for + 4->3. +- *Rank-1 deletion (hypothetical).* A single-child decrement `r -> r-1` + saves `h(r) - h(r-1) <= h(1) = 1` by concavity, with equality for deleting a + rank-1 child. Gain at most 0.012263218814646931910033 for 6..9, 0 for 5->4 + (in any amount) and 0.008208630960015088278435 for 4->3. No staging with this + compensation is known and its realization is not priced. + +The gap between the two is `1 - 0.991001... = 0.008998918419970962488711` per +unit. Local rewrites that also merge children (for example PR3682's +`{1:-2,2:-2,3:+2}`) save at zero rank change and are priced by the local term +of (*); they are a separate local-word lever. + +## 5. PR3682 -> staged544 split (exact at a_hi) + +At fixed `a`, `F(s, n) = 9 sum n_r h(r) + V(s) - 896 h(73)` is additively +separable in inventory and local profile, so the 2x2 interaction is +identically 0. `verify.py` solves all four corners exactly (each primal +`y >= 0`, dual feasible on 2,551 patterns, enclosure gap below 1e-70). They +share one basis, so the width part (one 8->7 per call, inside the range 30) +equals 9 x the price: + +- width part: +8.889631030668177612809695088162; +- local part: -8.919009734220261337601597266358, a saving of + 0.991001081580029037511288 per call; +- total -0.029378703552083724791902178195, or 0.003264300394675969421322 + per call (the documented-signature gain). + +Either change alone breaks the conservation. The width-only change moves the +ideal root down to about 0.0016821 and the local-only change moves it up to +about 0.0017788 (HiGHS, float). + +## 6. Scope + +This is a clock-free, fractional relaxation with fixed idle bins. Sections 3 and 4 +are exact statements about it. Template, stock and clock (chronological) +effects are not modeled. The conservation is observed, not derived, and the +documented signature is observed, not proved forced. `mu` is used only as a +subgradient bin price. The first-order conversion `dF/da ~ 184132` is floating +point. No kappa, supplier or admission claim is made. diff --git a/research/staged544-joint-price-region/test_cli.py b/research/staged544-joint-price-region/test_cli.py new file mode 100644 index 0000000000..cb503fa1b5 --- /dev/null +++ b/research/staged544-joint-price-region/test_cli.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Actual optimized CLI controls in disposable copies; original inputs stay intact.""" +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def hashes(root): + return {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file() and '__pycache__' not in p.parts} + + +def main(): + before = hashes(HERE) + controls = [] + with tempfile.TemporaryDirectory(prefix='staged544-joint-cli-') as temporary: + work = Path(temporary) / 'package' + + def reset(): + if work.exists(): + shutil.rmtree(work) + shutil.copytree(HERE, work, ignore=shutil.ignore_patterns('__pycache__')) + work.chmod(0o755) + for path in work.rglob('*'): + path.chmod(0o755 if path.is_dir() else 0o644) + + def run(script='verify.py', *args): + return subprocess.run([sys.executable, '-I', '-O', '-Werror', '-B', + str(work / script), *args], capture_output=True, + text=True, timeout=90) + + def reject(label, script='verify.py'): + result = run(script) + need(result.returncode != 0, label + ' was accepted') + controls.append(label) + + reset() + result = run() + need(result.returncode == 0 and 'PASS_STAGED544_JOINT_PRICE_REGION' in result.stdout, + 'positive primary CLI') + need(run('independent.py').returncode == 0, 'positive independent CLI') + for key, value, label, script in [ + ('a', '1/2', 'changed exponent', 'verify.py'), + ('demands', [234,18,162,478,864,1917], 'changed inventory', 'verify.py'), + ('extras', [[16,[0,0,0,0,2,0]]], 'removed extra column', 'verify.py'), + ('expected_axis_ranges', ['18','49','88/3','30','48'], 'inflated range', 'independent.py'), + ]: + reset() + path = work / 'MODEL.json' + data = json.loads(path.read_text()) + data[key] = value + path.write_text(json.dumps(data)) + reject(label, script) + reset() + path = work / 'retained/3815-ceiling_certificate.py' + path.write_bytes(path.read_bytes() + b'\n# corrupted source\n') + reject('source bytes') + reset() + path = work / 'RESULT.json' + data = json.loads(path.read_text()) + data['axis_witnesses'][0]['counts'][0] = '673' + path.write_text(json.dumps(data)) + reject('corrupted result witness') + reset() + yes = run('verify.py', '--flows', '0','48','0','0','0') + no = run('verify.py', '--flows', '0','28','28','0','0') + need(yes.returncode == no.returncode == 0, 'classification CLI exit') + need(json.loads(yes.stdout)['sharp_common_price'] is True, 'boundary CLI classification') + need(json.loads(no.stdout)['sharp_common_price'] is False, 'coupled CLI classification') + need(before == hashes(HERE), 'original bytes changed') + print('PASS_STAGED544_JOINT_REAL_CLI controls=' + str(len(controls)) + + ' positives=4 original_bytes_unchanged no_new_kappa') + + +if __name__ == '__main__': + main() diff --git a/research/staged544-joint-price-region/verify.py b/research/staged544-joint-price-region/verify.py new file mode 100644 index 0000000000..3e5774581b --- /dev/null +++ b/research/staged544-joint-price-region/verify.py @@ -0,0 +1,324 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent tight-face certificate, not a physical supplier or kappa result. + +ToikY, with substantial OpenAI Codex assistance. Predecessor source credit in README. +No predecessor executable is imported or executed. +""" +import argparse +import ast +from fractions import Fraction as Q +import hashlib +from itertools import product +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_model(root=HERE): + origins = json.loads((root / 'ORIGINS.json').read_text()) + for row in origins: + raw = (root / row['file']).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row['sha256'], 'source SHA256') + blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(blob == row['git_blob'], 'source Git blob') + tree = ast.parse((root / 'retained/3815-ceiling_certificate.py').read_text()) + constants = {} + for node in tree.body: + if isinstance(node, ast.Assign) and len(node.targets) == 1 and isinstance(node.targets[0], ast.Name): + try: + constants[node.targets[0].id] = ast.literal_eval(node.value) + except (ValueError, TypeError): + pass + m = json.loads((root / 'MODEL.json').read_text()) + cert = json.loads((root / 'retained/3862-CERTIFICATE.json').read_text()) + need(m['widths'] == list(constants['W']), 'width source binding') + need(m['capacities'] == list(constants['CAPS']), 'capacity source binding') + need(m['bins'] == [constants['BINS'][c] for c in m['capacities']], 'bin source binding') + need(m['demands'] == [9 * x for x in constants['SUPPLY']], 'inventory source binding') + need(m['basis'] == [[c, list(p)] for c, p in constants['BASIS']], 'basis source binding') + need(Q(m['a']) == Q(cert['ceiling']['a_hi']), 'exponent source binding') + need(m['flows'] == [5, 6, 7, 8, 9], 'flow schema') + need(m['extras'] == [[16, [0, 0, 0, 0, 2, 0]], [32, [0, 0, 0, 0, 4, 0]]], 'extra patterns') + return m + + +def solve(matrix, rhs): + n = len(rhs) + need(len(matrix) == n and all(len(row) == n for row in matrix), 'square system') + a = [[Q(x) for x in row] + [Q(v)] for row, v in zip(matrix, rhs)] + for i in range(n): + pivot = next((j for j in range(i, n) if a[j][i]), None) + need(pivot is not None, 'singular basis') + a[i], a[pivot] = a[pivot], a[i] + q = a[i][i] + a[i] = [v / q for v in a[i]] + for j in range(n): + if j != i: + q = a[j][i] + a[j] = [v - q * w for v, w in zip(a[j], a[i])] + return [row[-1] for row in a] + + +def dot(a, b): + return sum((x * y for x, y in zip(a, b)), Q(0)) + + +def column(m, item): + cap, p = item + return list(p) + [int(cap == c) for c in m['capacities']] + + +def remainder(m, item): + c, p = item + return c - dot(m['widths'], p) + + +def all_patterns(m): + for cap in m['capacities']: + for p in product(*(range(cap // w + 1) for w in m['widths'])): + if dot(p, m['widths']) <= cap: + yield [cap, list(p)] + + +def log_bounds(n): + # log(n) = k log(2) + 2 atanh((n-2^k)/(n+2^k)); geometric tail. + def series(t): + t = Q(t) + total, term = Q(0), t + for j in range(100): + total += term / (2 * j + 1) + term *= t * t + return 2 * total, 2 * (total + term / (201 * (1 - t * t))) + k = n.bit_length() - 1 + two, rem = series(Q(1, 3)), series(Q(n - 2**k, n + 2**k)) + return tuple(k * two[i] + rem[i] for i in (0, 1)) + + +def h_bounds(n, a): + if n in (0, 1): + return Q(n), Q(n) + lo, hi = log_bounds(n) + need(0 <= a * lo <= a * hi < 1, 'series domain') + # Alternating e^-x: odd degree 61 lower, even degree 60 upper. + def partial(x, degree): + term = total = Q(1) + for j in range(1, degree + 1): + term *= -x / j + total += term + return n * total + lower, upper = partial(a * hi, 61), partial(a * lo, 60) + den = 10**80 + return Q(lower.numerator * den // lower.denominator, den), Q(-((-upper.numerator * den) // upper.denominator), den) + + +def interval(expression, table): + lo = hi = Q(0) + for rank, coeff in expression.items(): + lo += coeff * table[rank][0 if coeff >= 0 else 1] + hi += coeff * table[rank][1 if coeff >= 0 else 0] + return lo, hi + + +def algebra(m): + columns = [column(m, b) for b in m['basis']] + matrix = [list(row) for row in zip(*columns)] + inverse = [solve(matrix, [int(i == j) for i in range(10)]) for j in range(10)] + inverse = [list(row) for row in zip(*inverse)] + return matrix, inverse + + +def linear_certificate(m, inv): + """Check all coefficients of the universal affine elimination identities.""" + base = [Q(x) for x in ('672','448','234','162','18','15','12','7','1916/5','324/5')] + need([dot(row, m['demands'] + m['bins']) for row in inv] == base, + 'affine baseline coefficients') + expected = [ + [0,0,1,0,-1,0,0,0,0,0], + [0,0,0,-1,1,Q(1,2),-Q(1,4),-Q(1,4),Q(1,20),-Q(1,20)], + [0,0,0,1,0,-Q(1,2),-Q(1,4),-Q(1,4),Q(1,20),-Q(1,20)], + [0,0,0,0,0,-Q(1,2),-Q(1,4),Q(3,4),Q(1,20),-Q(1,20)], + [0,0,0,0,0,Q(1,2),-Q(1,4),-Q(1,4),Q(1,20),-Q(1,20)], + ] + for w, target in zip(m['flows'], expected): + rhs = [0]*10 + rhs[w-4] = -1 + rhs[w-5] = 1 + need([dot(row, rhs) for row in inv] == target, 'affine flow coefficients') + for item, target in zip(m['extras'], + ([0,1,0,0,0,1,0,-1,0,0], [0,0,0,0,0,2,0,-1,0,0])): + need([dot(row, column(m, item)) for row in inv] == target, + 'extra-column elimination coefficients') + + +def classify(m): + matrix, inv = algebra(m) + linear_certificate(m, inv) + residuals = [int(remainder(m, b)) for b in m['basis']] + table = {r: h_bounds(r, Q(m['a'])) for r in range(49)} + tight, gaps, rows = [], [], [] + for item in all_patterns(m): + coords = [dot(row, column(m, item)) for row in inv] + rank = int(remainder(m, item)) + expression = {rank: Q(1)} if rank else {} + for coeff, r in zip(coords, residuals): + if r: + expression[r] = expression.get(r, Q(0)) - coeff + expression = {r: q for r, q in expression.items() if q} + if not expression: + tight.append(item) + else: + low, high = interval(expression, table) + need(low > 0, 'non-tight pattern lacks strict positive certificate') + gaps.append(low) + rows.append((item, coords)) + need(len(rows) == 2551 and len(tight) == 12, 'complete pattern classification') + key = lambda b: (b[0], tuple(b[1])) + need(set(map(key, tight)) == set(map(key, m['basis'] + m['extras'])), 'tight face differs') + return matrix, inv, min(gaps), rows + + +def demands(m, flows): + need(len(flows) == 5 and all(x >= 0 for x in flows), 'five nonnegative flows required') + d = list(map(Q, m['demands'])) + for w, x in zip(m['flows'], flows): + d[w - 4] -= x + d[w - 5] += x + need(min(d) >= 0, 'negative changed inventory') + return d + + +def facets(flows): + x5, x6, x7, x8, x9 = flows + return [48 - x6 - x7 - x8 - x9, 18 + x6 - x5, + 30 + x6 + x9 - x7 - x8, 88 + x6 + x8 + x9 - 3 * x7] + + +def packing(m, inv, flows): + rhs = demands(m, flows) + list(map(Q, m['bins'])) + y = [dot(row, rhs) for row in inv] + # General two-extra-column elimination; not an axis-only test. + feasible = all(y[j] >= 0 for j in range(10) if j != 7) and y[7] + y[5] >= 0 and 2*y[7] + y[1] + y[5] >= 0 + need(feasible == all(s >= 0 for s in facets(flows)), 'projected facet mismatch') + if not feasible: + return None + needed = max(Q(0), -y[7]) + z1 = min(needed, y[1]) + z2 = needed - z1 + y[1] -= z1 + y[5] -= z1 + 2*z2 + y[7] += z1 + z2 + answer = y + [z1, z2] + validate_packing(m, flows, answer) + return answer + + +def validate_packing(m, flows, answer): + need(len(answer) == 12 and min(answer) >= 0, 'nonnegative face counts') + cols = [column(m, b) for b in m['basis'] + m['extras']] + target = demands(m, flows) + list(map(Q, m['bins'])) + need([sum(v * c[i] for v, c in zip(answer, cols)) for i in range(10)] == target, 'packing conservation') + + +def result(m): + matrix, inv, gap, rows = classify(m) + expected_ranges = [Q(18), Q(48), Q(88, 3), Q(30), Q(48)] + need([str(v) for v in expected_ranges] == m['expected_axis_ranges'], 'range certificate') + witnesses, controls = [], [] + for i, bound in enumerate(expected_ranges): + flow = [Q(0)] * 5 + flow[i] = bound + answer = packing(m, inv, flow) + need(answer is not None, 'axis boundary not attained') + need(all((360*v).denominator == 1 for v in answer + demands(m, flow)), + 'T360 integral boundary witness') + witnesses.append({'flow': list(map(str, flow)), 'counts': list(map(str, answer))}) + flow[i] += Q(1, 1000) + try: + outside = packing(m, inv, flow) + except ValueError as exc: + need(str(exc) == 'negative changed inventory', 'unexpected axis rejection') + outside = None + need(outside is None, 'outside axis accepted') + controls.append('outside-axis-' + str(m['flows'][i])) + bad = [Q(0), Q(28), Q(28), Q(0), Q(0)] + need(packing(m, inv, bad) is None, 'independent range box incorrectly accepted') + controls.append('joint-box-counterexample') + # Row 6 separates the bad inventory from every tight column. + need(dot(inv[6], demands(m, bad) + list(map(Q, m['bins']))) == -2, 'separator value') + tight_keys = {(b[0], tuple(b[1])) for b in m['basis'] + m['extras']} + need(all(coords[6] >= 0 for item, coords in rows if (item[0], tuple(item[1])) in tight_keys), 'separator tight face') + mass_cap = max(-coords[6] for _, coords in rows) + need(mass_cap > 0, 'separator bound') + # A feasible non-tight packing for the same changed demand: shrink 28 + # distinct width-6 and 28 width-7 helpers in their original bins. + original = [dot(row, list(map(Q, m['demands'] + m['bins']))) for row in inv] + original[3] -= 28 # [6,8,9,9] -> [5,8,9,9] + original[1] -= 28 # [7,9] -> [6,9] + items = m['basis'] + [[32, [0, 1, 0, 0, 1, 2]], [16, [0, 0, 1, 0, 0, 1]]] + counts = original + [Q(28), Q(28)] + need(min(counts) >= 0, 'counterexample feasible counts') + cols = [column(m, b) for b in items] + need([sum(v * c[i] for v, c in zip(counts, cols)) for i in range(10)] == demands(m, bad) + list(map(Q, m['bins'])), 'counterexample conservation') + corrupt = list(map(Q, witnesses[0]['counts'])) + corrupt[0] += 1 + try: + validate_packing(m, list(map(Q, witnesses[0]['flow'])), corrupt) + except ValueError: + controls.append('extra-bin-count') + else: + raise ValueError('corrupt packing accepted') + try: + demands(m, [Q(-1), Q(0), Q(0), Q(0), Q(0)]) + except ValueError: + controls.append('negative-flow') + else: + raise ValueError('negative flow accepted') + # Deterministic boundary/interior coverage, not a global search theorem. + checked = 0 + for flow in product((Q(0), Q(7), Q(18), Q(24), Q(28), Q(48)), repeat=5): + try: + packing(m, inv, flow) + checked += 1 + except ValueError as exc: + if str(exc) != 'negative changed inventory': + raise + return {'status': 'PASS_STAGED544_JOINT_PRICE_REGION', 'a': m['a'], 'patterns': 2551, + 'tight_patterns': 12, 'non_tight_patterns': 2539, 'strict_reduced_cost_lower': str(gap), + 'axis_ranges_helper_calls_per_replica': list(map(str, expected_ranges)), + 'axis_witnesses': witnesses, 'sampled_flow_vectors': checked, 'controls': controls, + 'universal_affine_coefficients_checked': True, 'T360_integral_axis_boundaries': 5, + 'box_counterexample': {'flows': list(map(str, bad)), 'separator': '-2', + 'non_tight_separator_magnitude_bound': str(mass_cap), + 'idle_cost_gap_above_common_dual_lower': str(2 * gap / mass_cap), + 'feasible_patterns': items, 'feasible_counts': list(map(str, counts))}, + 'scope': 'Fixed-exponent fractional fixed-bin ideal only; no physical implementation or new kappa.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--flows', nargs=5, type=Q, metavar=('X5','X6','X7','X8','X9')) + parser.add_argument('--write-result', action='store_true') + args = parser.parse_args() + m = load_model() + report = result(m) + if args.flows is not None: + answer = packing(m, algebra(m)[1], args.flows) + print(json.dumps({'flows': list(map(str, args.flows)), 'sharp_common_price': answer is not None, + 'face_counts': None if answer is None else list(map(str, answer))})) + return + if args.write_result: + (HERE / 'RESULT.json').write_text(json.dumps(report, indent=2) + '\n') + else: + need(report == json.loads((HERE / 'RESULT.json').read_text()), 'result differs') + print(report['status'] + ' patterns=2551 tight=12 axis_ranges=18,48,88/3,30,48 no_new_kappa') + + +if __name__ == '__main__': + main()