From bbcfb869dc9069cdcb83680718521669548e1515 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 04:05:16 +0530 Subject: [PATCH 1/3] Price staged544 hosted-width changes in the fixed-T360 ideal Exact dual over all 318,840 width-1..9 bin patterns with monotone, nonpositive helper prices: free width reductions never raise the staged544 ideal ceiling 0.001730578437266246818741. Exact width-unit prices (0.987736781185353068089966 for 6..9, 1 for 5->4, >= 0.99179 for 4->3) with basis ranges; single-child staging bounds under the observed paid-rank identity; exact PR3682 -> staged544 decomposition. HiGHS cross-check recorded. No kappa claim. Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 620 +++++++++++++++++ .../staged544-width-lever-screen/PROOF.md | 160 +++++ .../staged544-width-lever-screen/README.md | 201 ++++++ .../staged544-width-lever-screen/SOURCES.json | 18 + .../staged544-width-lever-screen/TASK.json | 78 +++ .../staged544-width-lever-screen/VERIFY.json | 18 + .../crosscheck_highs.py | 141 ++++ .../evidence/HIGHS.json | 634 ++++++++++++++++++ .../evidence/VERIFY-OUTPUT.txt | 196 ++++++ .../staged544-width-lever-screen/verify.py | 413 ++++++++++++ 10 files changed, 2479 insertions(+) create mode 100644 research/staged544-width-lever-screen/CERTIFICATE.json create mode 100644 research/staged544-width-lever-screen/PROOF.md create mode 100644 research/staged544-width-lever-screen/README.md create mode 100644 research/staged544-width-lever-screen/SOURCES.json create mode 100644 research/staged544-width-lever-screen/TASK.json create mode 100644 research/staged544-width-lever-screen/VERIFY.json create mode 100644 research/staged544-width-lever-screen/crosscheck_highs.py create mode 100644 research/staged544-width-lever-screen/evidence/HIGHS.json create mode 100644 research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt create mode 100644 research/staged544-width-lever-screen/verify.py diff --git a/research/staged544-width-lever-screen/CERTIFICATE.json b/research/staged544-width-lever-screen/CERTIFICATE.json new file mode 100644 index 0000000000..f4d6ff5a22 --- /dev/null +++ b/research/staged544-width-lever-screen/CERTIFICATE.json @@ -0,0 +1,620 @@ +{ + "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 + } + } + } +} \ No newline at end of file diff --git a/research/staged544-width-lever-screen/PROOF.md b/research/staged544-width-lever-screen/PROOF.md new file mode 100644 index 0000000000..fc2c8e15c5 --- /dev/null +++ b/research/staged544-width-lever-screen/PROOF.md @@ -0,0 +1,160 @@ +# 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)` 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. Theorem (weak duality with monotone prices) + +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. + +**Reductions.** Let `s'` arise from `s` by moving `z_{w->v} >= 0` +helper-calls from width `w` to any `v < w` (`v >= 1`). The right side of (*) +equals the staged544 bound plus `sum z_{w->v} (pi_v - pi_w)` plus +`9 sum (n'_r - n_r) h_lo(r)`. If `pi` is nonincreasing in width, every +reduction term is nonnegative. + +`verify.py` takes `pi_4..pi_9` and `mu` from the basis. It sets `pi_1, pi_2, +pi_3` to the largest values that keep (D) feasible, maximizing `pi_3` first +(with `pi_1 = pi_2 = pi_3`), then `pi_2`, then `pi_1`. It then checks the +following: + +- (D) holds on all 318,840 patterns. The minimum reduced cost is exactly 0. + An unbounded-knapsack recursion over used volume gives the same minimum. +- `pi_1 >= pi_2 >= ... >= pi_9`, and every `pi_w <= 0`. Hence unhosting a + helper (width 0) is also never improving. +- the staged544 bound is `F(a_hi) >= 5.28e-20 > 0`. + +**Corollary (free reductions).** If the local profile is unchanged, no reduction +of any hosted widths raises the ideal ceiling above `a_hi`. This covers any +amount, any widths and widths down to 1 or unhosting, at zero entrance cost. +Each reduction unit costs at least `pi_v - pi_w` in `F`: + +| move | exact price at a_hi | range on the basis (helper-calls) | +|---|---|---| +| 9->8, 8->7, 7->6, 6->5 | 0.987736781185353068089966 | 28, 30, 28, 28 | +| 5->4 | 1 (exactly: `[9,9,9,5]` and `[9,9,9,4]` are both basic) | 18 | +| 4->3 | >= 0.991791369039984911721564 (dual bound) | n/a | + +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 the exact change. HiGHS gives +0.9877367811860, 1.0 and 0.9917913690369 for single units of 8->7, 5->4 +and 4->3. The 4->3 dual bound is therefore attained to about 3e-12 in floating +point; exact attainment is not claimed. + +**Why monotonicity is not automatic.** A narrower helper fits gaps that wider +ones cannot. The limiting patterns of the tight extension are exact fills: +`48 = 3 + 5*9` limits `pi_3`, `48 = 2 + 5*9` (leftover 1) limits `pi_2`, and +`32 = 1 + 4 + 3*9` limits `pi_1`. So the width-4..9 dual (2,551 patterns) does +not by itself give a monotone feasible extension. The control +`granularity_raised_pi3_infeasible_on_1_to_9` raises `pi_1..pi_3` by 1e-30 above +the tight value. The prices stay monotone and feasible on all 2,551 width-4..9 +patterns, but some width-1..9 pattern becomes infeasible. + +## 4. Paid-rank identity and what the corollary does not cover + +On three pinned T360 profiles, `sum_r n_r r = (896*73 - 320) T = 23,431,680`: + +- PR3682's finite profile (LEAD1-PRICE.json); +- PR3734's finite profile (inputs/PROFILE.json); +- PR3815's clock fill (inputs/PROFILE.json). + +The identity was observed on these three profiles; it is not proved here. If it +holds for every literal construction of this template, a free reduction is +not realizable. It adds `w - v` units of paid leftover with no offsetting local +change. A real staging move must then remove `w - v` units of local paid rank. +PR3734's change does exactly this: width 8->7 together with local +`{1:+3, 2:+1, 3:-2}`, a rank-sum change of -1 per call. So the corollary in +section 3 is **not** an upper relaxation of real staging. The correct screen is (*) +with the actual `n'`. + +**Staging screen.** Suppose one unit `w -> w-1` is paid by removing one unit +from a single local child (`r -> r-1`). That saves `h(r) - h(r-1) <= h(1) = 1` +by concavity, with equality when a rank-1 child is deleted. By (*), the change +in `F` is at least `price - 1`. The ceiling can therefore rise only if the +price is below 1: + +- w in {6..9}: gain at most 0.012263218814646931910033 per helper-call. This is + exact within the ranges above for a rank-1 deletion. +- w = 5: gain at most 0. Single-child-compensated 5->4 staging never raises + the ceiling, in any amount. +- w = 4: gain at most 0.008208630960015088278435. + +Local rewrites that also merge or split children are priced exactly by +`9 sum (n'_r - n_r) h(r)` in (*). They are a separate local-word lever. + +## 5. PR3682 -> staged544 decomposition (exact at a_hi) + +All four corners have the same optimal basis. Each primal is `y >= 0` with +dual feasibility on 2,551 patterns, and each enclosure gap is below 1e-70. +Because `(pi, mu)` depends only on `a`, the interaction term is exactly 0. The +four corners are PR3682 (inventory `{...,7:52,8:97,...}`, local +`{1:2437,2:724,3:226,...}`), width-only, local-only and staged544: + +- width part (one 8->7 per call): +8.889631030668177612809695088162 + = 9 x 0.987736781185353068089966...; +- local part: -8.919009734220261337601597266358, a saving of + 0.991001081580029037511288 per call; +- total -0.029378703552083724791902178195, or 0.003264300394675969421322 + per call. + +Under the identity neither single change is realizable. 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). PR3734's gain is the margin of its local +saving over the exact width-unit price. Against the single-child reference, its +local change gives up 0.008998918419970962488711 per call to reshaping: +`{1:+4,2:+1,3:-2}` has zero rank change and a positive cost. That is about 73% +of the 0.012263 available. + +## 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 paid-rank identity is observed, not derived. The +first-order conversion `dF/da ~ 184132` is floating point. No kappa, +supplier or admission claim is made. diff --git a/research/staged544-width-lever-screen/README.md b/research/staged544-width-lever-screen/README.md new file mode 100644 index 0000000000..e58ae1f889 --- /dev/null +++ b/research/staged544-width-lever-screen/README.md @@ -0,0 +1,201 @@ +# Staged544 width-lever screen: exact width prices for the fixed-T360 ideal + +**Scoped exact result about the clock-free fixed-bin ideal. It makes no kappa +claim, is not a construction and is not a complete multiplication theorem.** + +## Statement + +The model is PR3815's fixed-inventory ideal of the staged544 T360 template +(PR3734). Per owner replica there are 9 calls of 408 helpers with hosted widths +`{4:26,5:2,6:18,7:53,8:96,9:213}`, idle bins `{8:672,16:448,32:448,48:448}`, +local profile `{1:2440,2:725,3:224,4:102,5:20,8:8}` and 896 live rank-73 +families. Packings may be fractional and any clock is allowed. Details are in +[PROOF.md](PROOF.md). + +1. **Priced screen (exact, proved).** One dual `(pi, mu)` is feasible on **all + 318,840** bin patterns with widths 1..9, with exact minimum reduced cost 0. + Its helper prices are nonincreasing in width and nonpositive. By weak + duality, every changed inventory `s'` over widths 1..9 with these bins and + any changed local profile `n'` satisfies + + `F(a_hi) >= 9 sum n'_r h(r) + 9 sum pi_w s'_w + sum mu_c B_c - 896 h(73)` (*) + + at `a_hi = 0.001730578437266246818741`. The staged544 inventory gives + `F(a_hi) >= 5.28e-20 > 0`. +2. **Theorem (free reductions; proved negative result).** No reduction of the + hosted widths of any helpers, by any amount and down to width 1 or + unhosting, at zero entrance cost, raises the ideal ceiling above + `0.001730578437266246818741`. This holds when the local profile is + unchanged. The ceiling itself lies in + `[0.001730578437266246818740, 0.001730578437266246818741]`, which + reproduces PR3815. +3. **Exact width-unit prices** in `F` units per helper-call, at `a_hi`: + + | move | price | exact range on the basis | + |---|---|---| + | 9->8, 8->7, 7->6, 6->5 | 0.987736781185353068089966 | 28 / 30 / 28 / 28 helper-calls | + | 5->4 | 1 exactly | 18 | + | 4->3 | >= 0.991791369039984911721564 | not established (HiGHS attains it to 3e-12) | + + By convexity each price is a lower bound for every further unit. +4. **Theorem 2 does not bound real staging.** The paid rank sum is the same on + all three pinned T360 profiles: PR3682 finite, PR3734 finite and PR3815 clock + fill all give `sum n_r r = 23,431,680 = (896*73 - 320)*360`. This identity + is observed, not proved. Where it holds, a free reduction is not realizable. + A literal staging unit must remove one unit of local paid rank, which saves + up to `h(1) = 1`. With such single-child compensation, a unit can gain at most: + - **0.012263218814646931910033** per helper-call for widths 6..9. This is + exact within the ranges above when the compensation deletes a rank-1 child. + - **0** for 5->4. Single-child-compensated 5->4 staging never raises the + ceiling, in any amount. + - **0.008208630960015088278435** for 4->3. +5. **PR3682 -> staged544, exact at `a_hi`.** All four corners share one optimal + basis, so the interaction term is exactly 0. + - Width part (one 8->7 per call): `+8.889631030668177612809695088162`. + - Local part: `-8.919009734220261337601597266358`, a saving of + 0.991001081580029037511288 per call. + - Net: `-0.029378703552083724791902178195`. + + Neither single change is realizable under the identity. Width-only moves + the ideal root to about 0.0016821 and local-only to about 0.0017788 (HiGHS, + float). PR3734's ideal gain of 0.003264300394675969421322 per call is the + margin of its local saving over the exact price. Its local change gives up + 0.008998918419970962488711 per call (about 73% of the 0.012263 available) + to reshaping: `{1:+4,2:+1,3:-2}` has zero rank change and a positive cost. + +To first order, `dF/da ~ 184132` at the ceiling (floating point). Staging one +more width-6..9 helper in all nine calls with rank-1-deletion compensation would +raise the ideal ceiling by about 6.0e-7. PR3734 realized about 1.6e-7. + +## Decision informed + +This informs expansion-gate point 4 for the staged-entrance family (#3606), the +engine of #3605 and #3734. It also partly answers PR3815's open question 1. + +- Free width reduction is not a lever. +- 5->4 staging is closed under single-child compensation. +- Staging width-6..9 (and 4->3) helpers remains open in the ideal. The test for + a candidate is now one exact inequality: its local saving must exceed the + price above. +- The cheapest identified improvement is to avoid PR3734-type reshaping (up to + 0.008999 per call). +- Bin changes are priced by `mu`. The local word is priced by `h(r)`. + +## Reproduce + +``` +python3.12 -B scripts/research_package.py --package research/staged544-width-lever-screen +``` + +The verifier is standard-library only and runs in about 6 s. It can also be run +directly as `python3 -B research/staged544-width-lever-screen/verify.py`. The +expected last line is `PASS_STAGED544_WIDTH_LEVER_SCREEN`, preceded by a JSON +report with every number above. The output was identical under Python 3.12.15 +and 3.14.4. + +**Negative controls (each must fail; the verifier asserts they do):** + +- `pi_9 + 1e-30` makes the dual infeasible. +- `granularity_raised_pi3_infeasible_on_1_to_9`: raising `pi_1..pi_3` 1e-30 + above the tight extension leaves the prices monotone and feasible on the + 2,551 width-4..9 patterns, but infeasible on widths 1..9. This is why the + 318,840-pattern check is needed. +- A non-monotone extension is rejected. +- The dual bound at `a_lo` is not positive. +- One 8->9 widening per call drops the bound to `<= 0` (widening is priced as a + gain). +- A +1 change to a profile breaks the paid-rank identity. + +**Second, independent method (floating point):** `crosscheck_highs.py` used +Python 3.14.4, numpy 2.5.4 and scipy 1.18.1 HiGHS. It generates patterns as +integer partitions, uses explicit reduction columns instead of dual +monotonicity, and bisects the root. Its recorded output is +`evidence/HIGHS.json`: + +- Fixed staged544 root 0.0017305784372662612. +- Free reductions over 318,840 patterns: 0.0017305784372661503. This is not + higher; the 1.1e-16 difference is float noise. +- The stage-move variant matches the fixed root. +- PR3682 ideal root 0.0017304188997660508. +- Single-unit prices 0.9877367811860 (8->7), 1.0 (5->4) and 0.9917913690369 (4->3). + +It is not part of the registered replay. + +## What is new + +PR3815 certified the fixed staged544 inventory on 2,551 patterns. The +async505 inventory wall, PR3630 and PR3638 priced other inventories with fixed +widths. The following are new here: + +- the dual extension to all widths 1..9 with monotone prices; +- the general priced screen (*); +- exact width-unit prices and their ranges; +- the single-child staging bounds; +- the observed paid-rank identity and its consequence that free reductions do + not bound real staging (this corrects the premise of this package's task card); +- the exact PR3682 -> staged544 decomposition. + +## Sources + +The base is canonical main `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The +inputs are numbers transcribed into `verify.py` and `CERTIFICATE.json` from +unmerged PR heads. These heads are not reachable from main, so they are recorded +here by sha256 and not as `SOURCES.json` pins. The verifier cannot byte-check +them. This is a stated gap. + +| PR | head | file | sha256 | +|---|---|---|---| +| #3734 (dataisfire) | `fa041037a3374eaa08feeca0b26a5d6893194147` | `research/staged544-producer-return/PROOF.md` (inventory, local profile) | `be5fa8e381da957d52d02b154e2420f4459d7c8b30e23e82e245c11c978e3b62` | +| #3734 | same | `research/staged544-producer-return/inputs/PROFILE.json` | `06b4e2abe8d56b49bad3bdc8f8504082404b40609d548fa8de2618eb7373fd48` | +| #3815 (ChaloupeMusic) | `77ffbf287b6ca198b4a31e3835db3bae60718b93` | `research/staged544-clock-ceiling/ceiling_certificate.py` (model, bins, bracket) | `2276f1c5d341db63dcf511f6398733b1efbe9d09e2e9aa86b50d7a160a0f7d03` | +| #3815 | same | `research/staged544-clock-ceiling/inputs/PROFILE.json` | `9686df0d8e710c2e94aef3887f4bf130a05b64215faeae702cccb59e95a469d5` | +| #3682 (zxv) | `431e6c6023ef352c41696469de7fb614cd4ded8c` | `research/staged-donor-release/PROOF.md` (inventory, local profile) | `89ce2b0aa2dcf84ebcab04aedc451420815bc48af25c69998594910e9976a31b` | +| #3682 | same | `research/staged-donor-release/LEAD1-PRICE.json` (finite profile) | `217dfc6b0c243d5387f50b23d0a5a389754df702ea1d810aea46a6f3d81617bc` | + +## Scope, inherited assumptions and unresolved obligations + +- **Model.** This is the clock-free fractional ideal with fixed idle bins and + PR3815's payment rule (one rank-`l` child per remainder). Template, stock and + clock effects are out of scope. PR3815 traced PR3734's shortfall from its + ideal to the clock. +- **Paid-rank identity.** It was observed on three pinned profiles and is not + derived. The statements in item 4 that depend on it are conditional on it. +- **Admission costs not priced.** All admission costs of a changed inventory are + unknown and are not zero. These include physical stock, coverage law and + template checks, literal staging identities and clock feasibility. +- **Ranges.** Exact prices hold within the stated ranges of one basis. Outside + them they are lower bounds. The 4->3 value is a lower bound only. +- **Floating-point values.** `dF/da`, the ceiling conversions and the HiGHS + values are floating point. +- **No kappa.** No kappa, frontier or selected-result change is claimed. + +## Open next questions + +- **Does the paid-rank identity `sum n_r r = 65088 T` hold for every literal + construction of this template?** If it does, items 4 and 5 become + unconditional. First step: derive it from the owner and frame accounting in + PR3734's `owner_audit.py`, or find a construction that violates it. +- **Can a width-6..9 helper be staged with rank-1-deletion compensation and no + reshaping?** Each such helper is worth up to 0.110369 in `F` (about 6e-7 of + ceiling) within the ranges. First step: list PR3734's helpers with a rank-1 + entrance and price their literal staging local deltas with the screen (*). +- **What does the template lever (bins) offer?** `mu` gives exact bin prices + (`mu_48 = 47.679502755263063473958379`). First step: write a candidate + template's bin counts and evaluate the screen (*). Re-solve the LP for changes + outside the basis ranges. + +## Credit + +The model, bins, payment rule and basis are from PR3815 (ChaloupeMusic, head +`77ffbf28`). The staged544 inventory and local profile are from PR3734 +(dataisfire, head `fa041037`). The predecessor inventory is from PR3682 (zxv, +head `431e6c60`). The staged-entrance mechanism is from PR3605 (RossRichardson), +with lineage through PR3795/PR3802 (hexapode). The width-price method follows +`research/experiment-log/negative-searches/async505-inventory-wall` (Rohan +Arun), PR3630 (RossRichardson) and PR3638 (zxv). +No predecessor code is copied. `verify.py`'s enclosures, enumeration, knapsack +check and LP algebra are new. + +Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from +Claude (Anthropic, Claude Opus 5.5). Checked by AI review passes in the same +loop. No human or formal-kernel verification is claimed. Apache-2.0. diff --git a/research/staged544-width-lever-screen/SOURCES.json b/research/staged544-width-lever-screen/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/research/staged544-width-lever-screen/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/staged544-width-lever-screen/TASK.json b/research/staged544-width-lever-screen/TASK.json new file mode 100644 index 0000000000..8236232364 --- /dev/null +++ b/research/staged544-width-lever-screen/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "refined", + "actual_scope": "Narrowed to one helper-inventory lever of the staged544 T360 template (PR3734/PR3815): exact prices of hosted-width changes in the clock-free fixed-bin ideal. The deliverables are an exact dual over all 318,840 width-1..9 bin patterns with monotone, nonpositive helper prices; the theorem that free width reductions never raise the ideal ceiling 0.001730578437266246818741; exact width-unit prices with basis ranges; single-child staging bounds under the observed paid-rank identity; and the exact PR3682 -> staged544 decomposition. No new contract and no kappa.", + "scope_change_reason": "The card asks for a changed helper inventory. Staging (hosted-width reduction) is the engine of the pending gains in #3605 and #3734, and PR3815's open question 1 asks which changed T360 inventory raises the ceiling, so this package prices that lever exactly instead of proposing a contract. The task card's premise that a free width reduction is an upper relaxation of real staging was corrected during the work. All three pinned T360 profiles satisfy sum n_r r = 65088 T. Under that identity a literal staging unit must also remove one unit of local paid rank, so the package adds the single-child staging screen.", + "bottleneck_link": "The complex primitive binds the selected conditional kappa. The staged-entrance family's gains (#3605, #3734) are ideal-packing gains of the complex local word. This package gives the exact price at which staging a helper pays in that ideal: (*) in README/PROOF. Expansion-gate point 4 (stage more helpers versus redirect to bins or the local word) can therefore be decided per candidate by one inequality.", + "budget_minutes": 90, + "stop_rule": "Stop if the exact certificate fails and report the improving width move instead; ship without the decomposition if the PR3682 inventory is not pinned within 15 minutes; stop at the iteration deadline; stop and post nothing if a competing staged544 width or inventory pricing appears before submission.", + "outcome": "completed", + "evidence": "verify.py (stdlib, about 6 s) prints PASS_STAGED544_WIDTH_LEVER_SCREEN. Ceiling bracket [0.001730578437266246818740, ...741]: F(a_lo) <= -1.31e-19 and F(a_hi) >= 5.28e-20. Dual feasible on 318,840 patterns with minimum reduced cost exactly 0, matched by a knapsack recursion. Prices monotone and nonpositive. Width-unit prices: 0.987736781185353068089966 (6..9), 1 (5->4), >= 0.991791369039984911721564 (4->3). Single-child staging gain bounds: 0.012263218814646931910033, 0 and 0.008208630960015088278435. Decomposition: width +8.889631030668177612809695088162, local -8.919009734220261337601597266358, interaction exactly 0. Paid-rank identity holds on 3 pinned profiles. Six negative controls fail as required. Second method: HiGHS (evidence/HIGHS.json) agrees to about 1e-11 in F and 1e-16 in roots.", + "author": "Sagar Thakrar (thakrarsagar)", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for design, code, proofs and text. Checked by AI review passes in the same loop. No human or formal-kernel verification is claimed.", + "open_questions": [ + { + "question": "Does the paid-rank identity sum n_r r = 65088 T hold for every literal construction of the staged544 T360 template?", + "why_it_matters": "It turns the conditional staging statements (single-child bounds, non-realizability of free reductions) into unconditional ones.", + "first_step": "Derive the identity from the owner and frame accounting in PR3734's owner_audit.py, or exhibit a literal construction that violates it.", + "blocked_by": "Reading the unmerged PR3734 owner/frame accounting; not done in this time box." + }, + { + "question": "Can a width-6..9 helper be staged with rank-1-deletion compensation and no reshaping?", + "why_it_matters": "Each such helper (9 helper-calls, within the basis ranges) is worth up to 0.110369 in F, about 6e-7 of ideal ceiling, versus 1.6e-7 realized by PR3734.", + "first_step": "List PR3734's helpers with a rank-1 entrance and price each literal staging local delta with screen (*) before any synthesis.", + "blocked_by": "Literal staging identities, clock feasibility and the full admission of the changed word; all unpriced here." + }, + { + "question": "Which bin-template changes pass screen (*) once the bins are allowed to change?", + "why_it_matters": "The bin prices mu are exact on the current basis, and PR3815's open question 1 asks for a changed T360 inventory.", + "first_step": "Write a candidate template's bin counts, evaluate (*), and re-solve the LP for changes outside the basis ranges.", + "blocked_by": "Physical stock, coverage law and template checks of the complete admission." + } + ] +} diff --git a/research/staged544-width-lever-screen/VERIFY.json b/research/staged544-width-lever-screen/VERIFY.json new file mode 100644 index 0000000000..a0a8734a64 --- /dev/null +++ b/research/staged544-width-lever-screen/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact staged544 ceiling bracket; dual feasibility on all 318,840 width-1..9 patterns (enumeration plus knapsack); monotone nonpositive prices; free-reduction theorem; width-unit prices and ranges; paid-rank identity on 3 profiles; exact PR3682->staged544 decomposition; six negative controls must fail. Prints PASS_STAGED544_WIDTH_LEVER_SCREEN." + } + ] +} diff --git a/research/staged544-width-lever-screen/crosscheck_highs.py b/research/staged544-width-lever-screen/crosscheck_highs.py new file mode 100644 index 0000000000..e325145b45 --- /dev/null +++ b/research/staged544-width-lever-screen/crosscheck_highs.py @@ -0,0 +1,141 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Second, independent method (floating point): HiGHS LP + root bisection. + +Patterns are generated as integer partitions (descending part lists), not by the +count-vector recursion of verify.py. Reduction columns move one helper-call from +width w to any width v < w at zero cost ("free") or, for the staging move w -> w-1, +at the local entrance price h(2) - h(1) ("stage"). Prints JSON with roots and the +positive (basic) patterns, which verify.py re-checks exactly. +Requires numpy and scipy (see VERIFY.json requirements). +""" +import json +import math +import sys + +import numpy as np +import scipy.optimize as so +import scipy.sparse as sp + +BINS = {8: 672, 16: 448, 32: 448, 48: 448} +INV544 = {4: 26, 5: 2, 6: 18, 7: 53, 8: 96, 9: 213} +INV3682 = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213} +LOC544 = {1: 2440, 2: 725, 3: 224, 4: 102, 5: 20, 8: 8} +LOC3682 = {1: 2437, 2: 724, 3: 226, 4: 102, 5: 20, 8: 8} + + +def partitions(n, maxpart): + """All partitions of n with parts <= maxpart, as descending lists.""" + if n == 0: + yield [] + return + for first in range(min(n, maxpart), 0, -1): + for rest in partitions(n - first, first): + yield [first] + rest + + +def bin_patterns(wmin): + out = [] + for cap in BINS: + for used in range(cap + 1): + for part in partitions(used, 9): + if all(x >= wmin for x in part): + out.append((cap, tuple(part))) + return out + + +def h(l, a): + return l ** (1.0 - a) if l > 0 else 0.0 + + +def build(pats, widths, moves): + """Equality rows: one per width, one per bin rank. Columns: patterns, then moves.""" + row = {w: i for i, w in enumerate(widths)} + caps = list(BINS) + rows, cols, vals = [], [], [] + for j, (cap, part) in enumerate(pats): + for x in part: + rows.append(row[x]); cols.append(j); vals.append(1.0) + rows.append(len(widths) + caps.index(cap)); cols.append(j); vals.append(1.0) + n = len(pats) + for t, (w, v, _) in enumerate(moves): + rows += [row[w], row[v]]; cols += [n + t, n + t]; vals += [1.0, -1.0] + A = sp.csc_matrix((vals, (rows, cols)), shape=(len(widths) + len(caps), n + len(moves))) + return A + + +def make(inv, loc, wmin, mode): + widths = list(range(wmin, 10)) + pats = bin_patterns(wmin) + if mode == "fixed": + moves = [] + elif mode == "free": + moves = [(w, v, "free") for w in widths for v in widths if v < w] + elif mode == "stage": + moves = [(w, w - 1, "stage") for w in widths if w - 1 >= wmin] + A = build(pats, widths, moves) + b = np.array([9.0 * inv.get(w, 0) for w in widths] + [float(BINS[c]) for c in BINS]) + used = lambda p: sum(p[1]) # noqa: E731 + + def F(a): + cost = [h(cap - used(p), a) for p in pats for cap in [p[0]]] + mc = [0.0 if m[2] == "free" else h(2, a) - h(1, a) for m in moves] + r = so.linprog(np.array(cost + mc), A_eq=A, b_eq=b, bounds=(0, None), method="highs") + assert r.status == 0, r.message + local = 9.0 * sum(n * h(rk, a) for rk, n in loc.items()) + return r.fun + local - 896.0 * h(73, a), r + return pats, moves, F + + +def root(F, lo=0.0005, hi=0.005, it=56): + assert F(lo)[0] < 0 < F(hi)[0] + for _ in range(it): + mid = (lo + hi) / 2 + if F(mid)[0] > 0: + hi = mid + else: + lo = mid + return lo, hi + + +SCEN = { + "s544_fixed_w4": (INV544, LOC544, 4, "fixed"), + "s544_free_w1": (INV544, LOC544, 1, "free"), + "s544_stage_w1": (INV544, LOC544, 1, "stage"), + "pr3682_fixed": (INV3682, LOC3682, 4, "fixed"), + "width_only": (INV544, LOC3682, 4, "fixed"), + "local_only": (INV3682, LOC544, 4, "fixed"), +} +A_STAR = 0.001730578437266246818741 +# one helper-call moved (per replica RHS +-1): F differences at A_STAR give unit prices +UNIT = {"unit_8to7": (8, 7), "unit_5to4": (5, 4), "unit_4to3": (4, 3)} + +def unit_prices(): + base = make(INV544, LOC544, 1, "fixed")[2](A_STAR)[0] + out = {} + for name, (w, v) in UNIT.items(): + inv = dict(INV544) + inv[w] = inv[w] - 1 / 9 + inv[v] = inv.get(v, 0) + 1 / 9 + out[name] = make(inv, LOC544, 1, "fixed")[2](A_STAR)[0] - base + return base, out + + +if __name__ == "__main__": + names = sys.argv[1:] or list(SCEN) + res = {} + base, up = unit_prices() + res["unit_prices_at_a_star"] = dict(F_base=base, **up) + print("unit", base, up, file=sys.stderr, flush=True) + for name in names: + inv, loc, wmin, mode = SCEN[name] + pats, moves, F = make(inv, loc, wmin, mode) + lo, hi = root(F) + val, r = F(hi) + basis = [[pats[j][0], list(pats[j][1])] for j in range(len(pats)) if r.x[j] > 1e-7] + mv = {f"{m[0]}->{m[1]}": float(r.x[len(pats) + t]) for t, m in enumerate(moves) if r.x[len(pats) + t] > 1e-9} + res[name] = dict(patterns=len(pats), moves=len(moves), root_lo=repr(lo), root_hi=repr(hi), + F_at_a_star=F(A_STAR)[0], + positive_patterns=basis, positive_moves=mv, + eq_marginals=[float(x) for x in r.eqlin.marginals]) + print(name, len(pats), repr(lo), repr(hi), len(basis), mv, file=sys.stderr, flush=True) + print(json.dumps(res, indent=1)) diff --git a/research/staged544-width-lever-screen/evidence/HIGHS.json b/research/staged544-width-lever-screen/evidence/HIGHS.json new file mode 100644 index 0000000000..14d54ff5e1 --- /dev/null +++ b/research/staged544-width-lever-screen/evidence/HIGHS.json @@ -0,0 +1,634 @@ +{ + "method": "crosscheck_highs.py (float HiGHS LP + root bisection); not part of the registered replay", + "environment": { + "python": "3.14.4", + "numpy": "2.5.4", + "scipy": "1.18.1" + }, + "results": { + "unit_prices_at_a_star": { + "F_base": -7.275957614183426e-12, + "unit_8to7": 0.9877367811859585, + "unit_5to4": 1.0, + "unit_4to3": 0.991791369036946 + }, + "s544_fixed_w4": { + "patterns": 2551, + "moves": 0, + "root_lo": "0.0017305784372662612", + "root_hi": "0.0017305784372662614", + "F_at_a_star": -7.275957614183426e-12, + "positive_patterns": [ + [ + 8, + [ + 8 + ] + ], + [ + 16, + [ + 9, + 7 + ] + ], + [ + 32, + [ + 9, + 9, + 9 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 4 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 5 + ] + ], + [ + 32, + [ + 9, + 9, + 8, + 6 + ] + ], + [ + 32, + [ + 9, + 9, + 7, + 7 + ] + ], + [ + 32, + [ + 9, + 8, + 8, + 7 + ] + ], + [ + 48, + [] + ], + [ + 48, + [ + 9, + 9, + 9, + 9, + 9 + ] + ] + ], + "positive_moves": {}, + "eq_marginals": [ + -3.986093083432667, + -4.9860930834326656, + -5.973829864618018, + -6.961566645803372, + -7.9493034269887195, + -8.937040208174075, + 7.9493034269887195, + 15.89860685397744, + 31.797213707954885, + 47.679502755263044 + ] + }, + "s544_free_w1": { + "patterns": 318840, + "moves": 36, + "root_lo": "0.0017305784372661503", + "root_hi": "0.0017305784372661506", + "F_at_a_star": 7.275957614183426e-12, + "positive_patterns": [ + [ + 8, + [ + 8 + ] + ], + [ + 16, + [ + 9, + 7 + ] + ], + [ + 32, + [ + 9, + 9, + 9 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 4 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 5 + ] + ], + [ + 32, + [ + 9, + 9, + 8, + 6 + ] + ], + [ + 32, + [ + 9, + 9, + 7, + 7 + ] + ], + [ + 32, + [ + 9, + 8, + 8, + 7 + ] + ], + [ + 48, + [] + ], + [ + 48, + [ + 9, + 9, + 9, + 9, + 9 + ] + ] + ], + "positive_moves": {}, + "eq_marginals": [ + -1.000000000000003, + -1.9943017143926862, + -2.994301714392674, + -3.9860930834326656, + -4.9860930834326656, + -5.973829864618015, + -6.961566645803371, + -7.949303426988726, + -8.937040208174082, + 7.949303426988735, + 15.89860685397746, + 31.797213707954914, + 47.67950275526309 + ] + }, + "s544_stage_w1": { + "patterns": 318840, + "moves": 8, + "root_lo": "0.0017305784372662612", + "root_hi": "0.0017305784372662614", + "F_at_a_star": -7.275957614183426e-12, + "positive_patterns": [ + [ + 8, + [ + 8 + ] + ], + [ + 16, + [ + 9, + 7 + ] + ], + [ + 32, + [ + 9, + 9, + 9 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 4 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 5 + ] + ], + [ + 32, + [ + 9, + 9, + 8, + 6 + ] + ], + [ + 32, + [ + 9, + 9, + 7, + 7 + ] + ], + [ + 32, + [ + 9, + 8, + 8, + 7 + ] + ], + [ + 48, + [] + ], + [ + 48, + [ + 9, + 9, + 9, + 9, + 9 + ] + ] + ], + "positive_moves": {}, + "eq_marginals": [ + -6.9789001250486535, + -5.981297777843324, + -4.983695430637994, + -3.9860930834326638, + -4.986093083432664, + -5.973829864618017, + -6.961566645803369, + -7.949303426988722, + -8.937040208174075, + 7.949303426988722, + 15.898606853977444, + 31.79721370795489, + 47.67950275526305 + ] + }, + "pr3682_fixed": { + "patterns": 2551, + "moves": 0, + "root_lo": "0.0017304188997660508", + "root_hi": "0.001730418899766051", + "F_at_a_star": 0.029378703540714923, + "positive_patterns": [ + [ + 8, + [ + 8 + ] + ], + [ + 16, + [ + 9, + 7 + ] + ], + [ + 32, + [ + 9, + 9, + 9 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 4 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 5 + ] + ], + [ + 32, + [ + 9, + 9, + 8, + 6 + ] + ], + [ + 32, + [ + 9, + 9, + 7, + 7 + ] + ], + [ + 32, + [ + 9, + 8, + 8, + 7 + ] + ], + [ + 48, + [] + ], + [ + 48, + [ + 9, + 9, + 9, + 9, + 9 + ] + ] + ], + "positive_moves": {}, + "eq_marginals": [ + -3.98609436369052, + -4.986094363690518, + -5.973832270918492, + -6.961570178146467, + -7.949308085374438, + -8.937045992602412, + 7.949308085374438, + 15.898616170748877, + 31.797232341497754, + 47.679532202215626 + ] + }, + "width_only": { + "patterns": 2551, + "moves": 0, + "root_lo": "0.001682133808980024", + "root_hi": "0.0016821338089800242", + "F_at_a_star": 8.919009734214342, + "positive_patterns": [ + [ + 8, + [ + 8 + ] + ], + [ + 16, + [ + 9, + 7 + ] + ], + [ + 32, + [ + 9, + 9, + 9 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 4 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 5 + ] + ], + [ + 32, + [ + 9, + 9, + 8, + 6 + ] + ], + [ + 32, + [ + 9, + 9, + 7, + 7 + ] + ], + [ + 32, + [ + 9, + 8, + 8, + 7 + ] + ], + [ + 48, + [] + ], + [ + 48, + [ + 9, + 9, + 9, + 9, + 9 + ] + ] + ], + "positive_moves": {}, + "eq_marginals": [ + -3.986481857392532, + -4.9864818573925325, + -5.974560606746418, + -6.962639356100306, + -7.950718105454191, + -8.938796854808077, + 7.950718105454191, + 15.901436210908383, + 31.802872421816765, + 47.68844535499241 + ] + }, + "local_only": { + "patterns": 2551, + "moves": 0, + "root_lo": "0.0017788459357395703", + "root_hi": "0.0017788459357395705", + "F_at_a_star": -8.889631030680903, + "positive_patterns": [ + [ + 8, + [ + 8 + ] + ], + [ + 16, + [ + 9, + 7 + ] + ], + [ + 32, + [ + 9, + 9, + 9 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 4 + ] + ], + [ + 32, + [ + 9, + 9, + 9, + 5 + ] + ], + [ + 32, + [ + 9, + 9, + 8, + 6 + ] + ], + [ + 32, + [ + 9, + 9, + 7, + 7 + ] + ], + [ + 32, + [ + 9, + 8, + 8, + 7 + ] + ], + [ + 48, + [] + ], + [ + 48, + [ + 9, + 9, + 9, + 9, + 9 + ] + ] + ], + "positive_moves": {}, + "eq_marginals": [ + -3.985705761105779, + -4.985705761105778, + -5.973101899902071, + -6.960498038698365, + -7.947894177494655, + -8.935290316290951, + 7.947894177494655, + 15.89578835498931, + 31.791576709978628, + 47.67059452042079 + ] + } + } +} \ No newline at end of file diff --git a/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt b/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt new file mode 100644 index 0000000000..fd2d8a268e --- /dev/null +++ b/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt @@ -0,0 +1,196 @@ +{ + "ceiling": { + "a_lo": "0.001730578437266246818740", + "a_hi": "0.001730578437266246818741", + "F_upper_at_a_lo": "-0.000000000000000000131326522020", + "F_lower_at_a_hi": "0.000000000000000000052805837005", + "primal_min_y": "7" + }, + "free_reduction_theorem": { + "patterns_widths_1_to_9": 318840, + "patterns_widths_4_to_9": 2551, + "min_reduced_cost_all": "0.000000000000000000000000000000", + "min_reduced_cost_knapsack": "0.000000000000000000000000000000", + "min_reduced_cost_widths_4_to_9": "0.000000000000000000000000000000", + "zero_reduced_cost_patterns": 12, + "argmin_pattern": [ + 8, + [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 0 + ] + ], + "monotone": true, + "holds": true + }, + "prices_at_a_hi": { + "helper_pi": { + "1": "-3.986093083432664503980103", + "2": "-3.986093083432664503980103", + "3": "-3.986093083432664503980103", + "4": "-3.986093083432664503980103", + "5": "-4.986093083432664503980103", + "6": "-5.973829864618017572070069", + "7": "-6.961566645803370640160035", + "8": "-7.949303426988723708250001", + "9": "-8.937040208174076776339968" + }, + "bin_mu": { + "8": "7.949303426988723708250001", + "16": "15.898606853977447416500003", + "32": "31.797213707954894833000007", + "48": "47.679502755263063473958379" + }, + "width_unit_price": { + "5->4": "1.000000000000000000000000", + "6->5": "0.987736781185353068089966", + "7->6": "0.987736781185353068089966", + "8->7": "0.987736781185353068089966", + "9->8": "0.987736781185353068089966" + }, + "entrance_raise_1_to_2": "0.997602347205330147005789", + "delete_rank1_child": "-1.000000000000000000000000", + "primal_y": { + "8:000010": "672", + "16:000101": "448", + "32:000003": "12", + "32:100003": "234", + "32:010003": "18", + "32:001012": "162", + "32:000202": "7", + "32:000121": "15", + "48:000000": "1916/5", + "48:000005": "324/5" + }, + "tight_small_width_pi": { + "1": "-1.000000000000000000000000", + "2": "-1.994301714392679592258538", + "3": "-2.994301714392679592258538" + }, + "width_unit_price_lower_bound_4_to_v": { + "4->3": "0.991791369039984911721564", + "4->2": "1.991791369039984911721564", + "4->1": "2.986093083432664503980103" + }, + "explicit_4_to_3_move_cost_lower_enclosure": "0.997602347205330147005789", + "exact_range_helper_calls_per_replica": { + "5->4": "18", + "6->5": "28", + "7->6": "28", + "8->7": "30", + "9->8": "28" + }, + "tight_extension_min_reduced_cost": "0.000000000000000000000000000000", + "tight_extension_limiting_patterns": { + "3": [ + 48, + [ + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 5 + ] + ], + "2": [ + 48, + [ + 0, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 5 + ] + ], + "1": [ + 32, + [ + 1, + 0, + 0, + 1, + 0, + 0, + 0, + 0, + 3 + ] + ] + } + }, + "staging_screen_per_helper_call": { + "single_child_compensation_upper_reference": { + "5->4": "0.000000000000000000000000", + "6->5": "0.012263218814646931910033", + "7->6": "0.012263218814646931910033", + "8->7": "0.012263218814646931910033", + "9->8": "0.012263218814646931910033", + "4->3": "0.008208630960015088278435" + }, + "pr3734_local_saving": "0.991001081580029037511288", + "pr3734_net_gain": "0.003264300394675969421322", + "pr3734_reshaping_cost": "0.008998918419970962488711" + }, + "first_order_float": { + "dF_da_at_ceiling": 184132.35902592752, + "ceiling_change_per_unit_F_decrease": 5.430875948638614e-06 + }, + "paid_rank_identity": { + "pr3682_finite": { + "T": 360, + "paid_rank_sum": 23431680, + "identity": true + }, + "pr3734_finite": { + "T": 360, + "paid_rank_sum": 23431680, + "identity": true + }, + "pr3815_clock_fill": { + "T": 360, + "paid_rank_sum": 23431680, + "identity": true + } + }, + "decomposition_at_a_hi": { + "F_lower": { + "pr3682": "0.029378703552083724844708015201", + "width_only": "8.919009734220261337654403103364", + "local_only": "-8.889631030668177612756889251156", + "staged544": "0.000000000000000000052805837005" + }, + "width_part": "8.889631030668177612809695088162", + "local_part": "-8.919009734220261337601597266358", + "interaction": "0.000000000000000000000000000000", + "total": "-0.029378703552083724791902178195", + "width_part_per_call": "0.987736781185353068089966120906", + "local_saving_per_call": "0.991001081580029037511288585150", + "local_part_exact": "-8.919009734220261337601597266358" + }, + "controls_failed_as_required": { + "perturb_pi9_up_1e-30": true, + "granularity_raised_pi3_infeasible_on_1_to_9": true, + "non_monotone_extension_rejected": true, + "bound_at_a_lo_not_positive": true, + "one_8_to_9_widening_per_call_breaks_bound": true, + "volume_identity_detects_plus_one": true + }, + "status": "PASS", + "failures": [] +} +PASS_STAGED544_WIDTH_LEVER_SCREEN diff --git a/research/staged544-width-lever-screen/verify.py b/research/staged544-width-lever-screen/verify.py new file mode 100644 index 0000000000..f786f90243 --- /dev/null +++ b/research/staged544-width-lever-screen/verify.py @@ -0,0 +1,413 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact width-lever screen of the staged544 fixed-T360 ideal (standard library only). + +Model (PR3815 ceiling_certificate.py, PR3734 inventory): per owner replica, 9 calls of +408 helpers; idle bins {8:672,16:448,32:448,48:448}; each helper occupies its hosted +width in one bin and each bin remainder l>0 is paid as one rank-l child; local paid +profile per call; 896 live rank-73 families. F(a) = sum n_r r^(1-a) - 896*73^(1-a) per +replica has the sign of a strictly increasing function, so "ceiling < a" iff F(a) > 0. + +Checks (all exact rational arithmetic; h(l) = l^(1-a) enclosed by series with +remainder bounds, rounded outward to 1e-90): + 1. staged544 ceiling bracket (a_lo, a_hi) from an exact primal/dual pair. + 2. free width reductions: dual over ALL 318,840 bin patterns with widths 1..9 + plus monotone helper prices => no reduction of any widths, by any amount, + to any width >= 1, at zero cost, gives F(a_hi) <= 0. Cross-checked by an + unbounded-knapsack recursion (different algorithm, same claim). + 3. exact width-unit prices p(w->v) = pi_v - pi_w at a_hi. + 4. paid-rank (volume) identity on three pinned profiles. + 5. PR3682 -> staged544 exact 2x2 decomposition of F at a_hi (four optimal LPs). + 6. negative controls (each must fail). +""" +import json +import math +import sys +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CERT = json.loads((HERE / "CERTIFICATE.json").read_text()) +BINS = {8: 672, 16: 448, 32: 448, 48: 448} +CAPS = (8, 16, 32, 48) +WIDTHS = tuple(range(1, 10)) +CALLS, LIVE, LIVE_RANK = 9, 896, 73 +INV = {"staged544": {4: 26, 5: 2, 6: 18, 7: 53, 8: 96, 9: 213}, + "pr3682": {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213}} +LOC = {"staged544": {1: 2440, 2: 725, 3: 224, 4: 102, 5: 20, 8: 8}, + "pr3682": {1: 2437, 2: 724, 3: 226, 4: 102, 5: 20, 8: 8}} +DEN = 10 ** 90 + + +# ---------- outward rational enclosures of h(l) = l^(1-a) ---------- +def atanh_enc(t, n=110): + """sum_{k (lower, upper) enclosure of l^(1-a) for l in 0..48 and 73.""" + a = Q(a) + assert 0 < a < Q(1, 100) + tab = {0: (Q(0), Q(0)), 1: (Q(1), Q(1))} + for l, (llo, lhi) in LN.items(): + lo = l * exp_neg(ceil_d(a * lhi), True) + hi = l * exp_neg(floor_d(a * llo), False) + tab[l] = (floor_d(lo), ceil_d(hi)) + assert tab[l][0] < tab[l][1] and hi - lo < Q(1, 10 ** 85) + return tab + + +# ---------- patterns ---------- +def patterns(cap, widths): + """All count vectors (indexed by WIDTHS) of helpers of the given widths fitting cap.""" + out = [] + + def rec(i, rest, cur): + if i == len(widths): + v = [0] * 9 + for w, k in zip(widths, cur): + v[w - 1] = k + out.append(tuple(v)) + return + for k in range(rest // widths[i] + 1): + rec(i + 1, rest - k * widths[i], cur + [k]) + rec(0, cap, []) + return out + + +def left(cap, p): + return cap - sum(k * w for k, w in zip(p, WIDTHS)) + + +def solve(A, b): + 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)] + + +# ---------- LP pieces ---------- +def basis_of(name): + return [(c, tuple(p)) for c, p in CERT["bases"][name]] + + +def used_widths(basis): + return sorted({WIDTHS[i] for _, p in basis for i, k in enumerate(p) if k}) + + +def primal(inv, basis): + """Exact y on the basis: widths rows (=9 s_w) and bin rows (=B_c).""" + ws = used_widths(basis) + assert set(inv) == set(ws) and len(ws) + len(CAPS) == len(basis) + A = [[p[w - 1] for _, p in basis] for w in ws] + [[1 if c == cap else 0 for c, _ in basis] for cap in CAPS] + b = [CALLS * inv[w] for w in ws] + [BINS[c] for c in CAPS] + y = solve(A, b) + return y + + +def dual(basis, tab): + """Exact (pi, mu) with pi.p + mu_c = h_lo(l_p) on the basis; pi_1..3 := pi_4.""" + ws = used_widths(basis) + A = [[p[w - 1] for w in ws] + [1 if c == cap else 0 for cap in CAPS] for c, p in basis] + b = [tab[left(c, p)][0] for c, p in basis] + sol = solve(A, b) + pi = dict(zip(ws, sol[:len(ws)])) + for w in WIDTHS: + if w not in pi: + pi[w] = pi[min(ws)] # cheapest monotone extension + return pi, dict(zip(CAPS, sol[len(ws):])) + + +def local_sum(loc, tab, k): + return CALLS * sum(n * tab[r][k] for r, n in loc.items()) + + +def min_reduced_cost_enum(pi, mu, tab, widths): + """Exact minimum of h_lo(l_p) - pi.p - mu_c over every pattern (integer arithmetic).""" + vals = list(pi.values()) + list(mu.values()) + [tab[l][0] for l in range(49)] + L = 1 + for v in vals: + L = L * v.denominator // math.gcd(L, v.denominator) + P = [int(pi[w] * L) for w in widths] + H = [int(tab[l][0] * L) for l in range(49)] + worst, count, tight = None, 0, 0 + for cap in CAPS: + M = int(mu[cap] * L) + + def rec(i, rest, acc, cur): + nonlocal worst, count, tight + if i == len(widths): + rc = H[rest] - M - acc + count += 1 + tight += rc == 0 + if worst is None or rc < worst[0]: + worst = (rc, cap, tuple(cur)) + return + w = widths[i] + for k in range(rest // w + 1): + rec(i + 1, rest - k * w, acc + k * P[i], cur + [k]) + rec(0, cap, 0, []) + return Q(worst[0], L), worst[1:], count, tight + + +def min_reduced_cost_knapsack(pi, mu, tab, widths): + """Same minimum by an unbounded-knapsack recursion on used volume (independent).""" + best = {0: Q(0)} + for v in range(1, 49): + c = [best[v - w] + pi[w] for w in widths if v - w in best] + if c: + best[v] = max(c) + return min(tab[cap - v][0] - mu[cap] - best[v] for cap in CAPS for v in best if v <= cap) + + +def max_uniform_price(pi, mu, tab, free): + """Largest t such that pi_w := t for w in free keeps every widths-1..9 pattern dual feasible.""" + vals = [pi[w] for w in WIDTHS if w not in free] + list(mu.values()) + [tab[l][0] for l in range(49)] + L = 1 + for v in vals: + L = L * v.denominator // math.gcd(L, v.denominator) + P = [0 if w in free else int(pi[w] * L) for w in WIDTHS] + H = [int(tab[l][0] * L) for l in range(49)] + best = None # (numerator, s, cap, counts) of the minimal bound + + for cap in CAPS: + M = int(mu[cap] * L) + + def rec(i, rest, acc, s, cur): + nonlocal best + if i == len(WIDTHS): + if s and (best is None or (H[rest] - M - acc) * best[1] < best[0] * s): + best = (H[rest] - M - acc, s, cap, tuple(cur)) + return + w = WIDTHS[i] + for k in range(rest // w + 1): + rec(i + 1, rest - k * w, acc + k * P[i], s + (k if w in free else 0), cur + [k]) + rec(0, cap, 0, 0, []) + return Q(best[0], best[1] * L), (best[2], list(best[3])) + + +def ranging(inv, basis, d): + """Largest k >= 0 keeping y(k) = B^-1 (b + k d) >= 0 (d per replica on widths).""" + ws = used_widths(basis) + A = [[p[w - 1] for _, p in basis] for w in ws] + [[1 if c == cap else 0 for c, _ in basis] for cap in CAPS] + y = primal(inv, basis) + dy = solve(A, [d.get(w, 0) for w in ws] + [0] * len(CAPS)) + ks = [yy / -g for yy, g in zip(y, dy) if g < 0] + return min(ks) if ks else None + + +def F_bounds(inv, loc, basis, a): + """Exact optimal-LP enclosure of F(a): primal (upper) and dual (lower) on one basis.""" + tab = h_table(a) + y = primal(inv, basis) + pi, mu = dual(basis, tab) + ws = sorted(inv) + rc, worst, n, tight = min_reduced_cost_enum(pi, mu, tab, tuple(ws)) + upper = local_sum(loc, tab, 1) + sum(yy * tab[left(c, p)][1] for yy, (c, p) in zip(y, basis)) - LIVE * tab[LIVE_RANK][0] + lower = local_sum(loc, tab, 0) + sum(mu[c] * BINS[c] for c in CAPS) + sum(pi[w] * CALLS * inv[w] for w in ws) - LIVE * tab[LIVE_RANK][1] + return dict(y_min=min(y), dual_min_rc=rc, patterns=n, lower=lower, upper=upper, pi=pi, mu=mu, tab=tab, y=y) + + +def dec(x, d=24): + s = "-" if x < 0 else "" + x = abs(x) + q, r = divmod(x.numerator * 10 ** d, x.denominator) + return f"{s}{q // 10 ** d}.{q % 10 ** d:0{d}d}" + + +def main(): + out, fails = {}, [] + + def need(cond, msg): + if not cond: + fails.append(msg) + + a_lo, a_hi = Q(CERT["ceiling"]["a_lo"]), Q(CERT["ceiling"]["a_hi"]) + B = basis_of("staged544") + inv, loc = INV["staged544"], LOC["staged544"] + + # 1. fixed-inventory ceiling bracket + lo_side = F_bounds(inv, loc, B, a_lo) + need(lo_side["y_min"] >= 0, "primal infeasible") + need(lo_side["upper"] < 0, "F(a_lo) upper bound not negative") + tab = h_table(a_hi) + y = primal(inv, B) + pi, mu = dual(B, tab) + + # 2. free reductions: all patterns of widths 1..9 + monotone prices + rc_all, worst_all, n_all, tight_all = min_reduced_cost_enum(pi, mu, tab, WIDTHS) + rc_kn = min_reduced_cost_knapsack(pi, mu, tab, WIDTHS) + rc_w4, _, n_w4, _ = min_reduced_cost_enum(pi, mu, tab, (4, 5, 6, 7, 8, 9)) + mono = all(pi[w - 1] >= pi[w] for w in WIDTHS[1:]) + lower = local_sum(loc, tab, 0) + sum(mu[c] * BINS[c] for c in CAPS) \ + + sum(pi[w] * CALLS * inv[w] for w in inv) - LIVE * tab[LIVE_RANK][1] + need(n_all == 318840 and n_w4 == 2551, "pattern counts") + need(rc_all >= 0 and rc_kn == rc_all, "dual infeasible over widths 1..9 or knapsack mismatch") + need(mono, "helper prices not monotone") + need(lower > 0, "F(a_hi) lower bound not positive") + out["ceiling"] = dict(a_lo=dec(a_lo), a_hi=dec(a_hi), F_upper_at_a_lo=dec(lo_side["upper"], 30), + F_lower_at_a_hi=dec(lower, 30), primal_min_y=str(min(y))) + out["free_reduction_theorem"] = dict( + patterns_widths_1_to_9=n_all, patterns_widths_4_to_9=n_w4, + min_reduced_cost_all=dec(rc_all, 30), min_reduced_cost_knapsack=dec(rc_kn, 30), + min_reduced_cost_widths_4_to_9=dec(rc_w4, 30), zero_reduced_cost_patterns=tight_all, + argmin_pattern=[worst_all[0], list(worst_all[1])], monotone=mono, + holds=rc_all >= 0 and mono and lower > 0) + + # 3. prices at a_hi (F units per replica; one helper-call = one unit of 9 s_w) + out["prices_at_a_hi"] = dict( + helper_pi={w: dec(pi[w]) for w in WIDTHS}, bin_mu={c: dec(mu[c]) for c in CAPS}, + width_unit_price={f"{w}->{w - 1}": dec(pi[w - 1] - pi[w]) for w in range(5, 10)}, + entrance_raise_1_to_2=dec(tab[2][0] - 1), delete_rank1_child=dec(Q(-1)), + primal_y={f"{c}:{''.join(str(k) for k in p[3:])}": str(v) for (c, p), v in zip(B, y)}) + unit = {w: pi[w - 1] - pi[w] for w in range(5, 10)} + need(all(0 <= u <= 1 for u in unit.values()), "width-unit price outside [0,1]") + + # 3b. tightest monotone prices for widths 3, 2, 1 (sequential maximisation), re-checked + pt, limiting = dict(pi), {} + for free in ((1, 2, 3), (1, 2), (1,)): + t, limiting[max(free)] = max_uniform_price(pt, mu, tab, free) + for w in free: + pt[w] = t + rc_t = min_reduced_cost_enum(pt, mu, tab, WIDTHS)[0] + mono_t = all(pt[w - 1] >= pt[w] for w in WIDTHS[1:]) + need(rc_t >= 0 and mono_t and min_reduced_cost_knapsack(pt, mu, tab, WIDTHS) == rc_t, "tight extension") + swap43 = tab[2][0] - tab[1][1] # [9,9,9,4] -> [9,9,9,3]: explicit primal move + need(pt[3] - pt[4] <= tab[2][1] - tab[1][0], "4->3 dual bound above explicit move") + ranges = {f"{w}->{w - 1}": ranging(inv, B, {w: -1, w - 1: 1}) for w in range(5, 10)} + out["prices_at_a_hi"]["tight_small_width_pi"] = {w: dec(pt[w]) for w in (1, 2, 3)} + out["prices_at_a_hi"]["width_unit_price_lower_bound_4_to_v"] = {f"4->{v}": dec(pt[v] - pt[4]) for v in (3, 2, 1)} + out["prices_at_a_hi"]["explicit_4_to_3_move_cost_lower_enclosure"] = dec(swap43) + out["prices_at_a_hi"]["exact_range_helper_calls_per_replica"] = {k: str(v) for k, v in ranges.items()} + out["prices_at_a_hi"]["tight_extension_min_reduced_cost"] = dec(rc_t, 30) + out["prices_at_a_hi"]["tight_extension_limiting_patterns"] = limiting + need(all(pt[w] <= 0 for w in WIDTHS), "a helper price is positive (unhosting would then be priced)") + + # 3c. volume-neutral staging screen: gain per helper-call = saving - price + out["staging_screen_per_helper_call"] = dict( + single_child_compensation_upper_reference=dict( + {f"{w}->{w - 1}": dec(1 - unit[w]) for w in range(5, 10)}, **{"4->3": dec(1 - (pt[3] - pt[4]))}), + pr3734_local_saving=dec(Q(-1, CALLS) * CALLS * sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9))), + pr3734_net_gain=dec(Q(-1) * sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9)) - unit[8]), + pr3734_reshaping_cost=dec(1 + sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9)))) + # first-order conversion of F to the ceiling (float, envelope theorem on the optimal basis) + dFda = -(CALLS * sum(n * float(tab[r][0]) * math.log(r) for r, n in loc.items()) + + sum(float(yy) * float(tab[left(c, p)][0]) * math.log(left(c, p)) for yy, (c, p) in zip(y, B) if left(c, p) > 1)) \ + + LIVE * float(tab[LIVE_RANK][0]) * math.log(LIVE_RANK) + out["first_order_float"] = dict(dF_da_at_ceiling=dFda, + ceiling_change_per_unit_F_decrease=1 / dFda) + + # 4. paid-rank identity (sum n_r r = (896*73 - 320) T) on pinned profiles + vol = {} + for k, prof in CERT["profiles"].items(): + T = prof["T"] + hist = {int(r): n for r, n in prof["histogram"].items()} + if prof.get("add_local"): + for r, n in LOC[prof["add_local"]].items(): + hist[r] = hist.get(r, 0) + CALLS * T * n + vol[k] = dict(T=T, paid_rank_sum=sum(r * n for r, n in hist.items()), + identity=sum(r * n for r, n in hist.items()) == (LIVE * LIVE_RANK - 320) * T) + need(vol[k]["identity"], f"volume identity fails for {k}") + out["paid_rank_identity"] = vol + + # 5. 2x2 decomposition at a_hi (each corner: own optimal basis, exact) + corners = {"pr3682": ("pr3682", "pr3682"), "width_only": ("staged544", "pr3682"), + "local_only": ("pr3682", "staged544"), "staged544": ("staged544", "staged544")} + Fc = {} + for name, (i, l) in corners.items(): + r = F_bounds(INV[i], LOC[l], basis_of(name), a_hi) + need(r["y_min"] >= 0 and r["dual_min_rc"] >= 0, f"corner {name} basis not optimal") + need(r["upper"] - r["lower"] < Q(1, 10 ** 70), f"corner {name} gap") + Fc[name] = r["lower"] + d_w, d_l = Fc["width_only"] - Fc["pr3682"], Fc["local_only"] - Fc["pr3682"] + total = Fc["staged544"] - Fc["pr3682"] + out["decomposition_at_a_hi"] = dict( + F_lower={k: dec(v, 30) for k, v in Fc.items()}, + width_part=dec(d_w, 30), local_part=dec(d_l, 30), interaction=dec(total - d_w - d_l, 30), + total=dec(total, 30), + width_part_per_call=dec(d_w / CALLS, 30), local_saving_per_call=dec(-d_l / CALLS, 30), + local_part_exact=dec(CALLS * sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9)), 30)) + need(total < 0 and d_w > 0 and d_l < 0, "decomposition signs") + + # 6. negative controls (each must FAIL the corresponding check) + ctl = {} + pi_bad = dict(pi) + pi_bad[9] += Q(1, 10 ** 30) + ctl["perturb_pi9_up_1e-30"] = min_reduced_cost_enum(pi_bad, mu, tab, WIDTHS)[0] < 0 + pi_nm = dict(pi) + for w in (1, 2, 3): + pi_nm[w] = pi[4] - Q(1, 10 ** 30) + pg = dict(pt) + for w in (1, 2, 3): + pg[w] = pt[3] + Q(1, 10 ** 30) # monotone, feasible on widths 4..9, too high for 1..9 + ctl["granularity_raised_pi3_infeasible_on_1_to_9"] = min_reduced_cost_enum(pg, mu, tab, WIDTHS)[0] < 0 \ + and min_reduced_cost_enum(pg, mu, tab, (4, 5, 6, 7, 8, 9))[0] >= 0 and all(pg[w - 1] >= pg[w] for w in WIDTHS[1:]) + ctl["non_monotone_extension_rejected"] = not all(pi_nm[w - 1] >= pi_nm[w] for w in WIDTHS[1:]) + lo_tab = h_table(a_lo) + pl, ml = dual(B, lo_tab) + lb_lo = local_sum(loc, lo_tab, 0) + sum(ml[c] * BINS[c] for c in CAPS) \ + + sum(pl[w] * CALLS * inv[w] for w in inv) - LIVE * lo_tab[LIVE_RANK][1] + ctl["bound_at_a_lo_not_positive"] = lb_lo <= 0 + widened = dict(inv) + widened[8] -= 1 + widened[9] += 1 + lb_wide = local_sum(loc, tab, 0) + sum(mu[c] * BINS[c] for c in CAPS) \ + + sum(pi[w] * CALLS * widened.get(w, 0) for w in WIDTHS) - LIVE * tab[LIVE_RANK][1] + ctl["one_8_to_9_widening_per_call_breaks_bound"] = lb_wide <= 0 + vol_bad = sum(int(r) * n for r, n in CERT["profiles"]["pr3734_finite"]["histogram"].items()) + 1 + ctl["volume_identity_detects_plus_one"] = vol_bad != (LIVE * LIVE_RANK - 320) * 360 + for k, v in ctl.items(): + need(v, f"control {k} did not fail as required") + out["controls_failed_as_required"] = ctl + + out["status"] = "PASS" if not fails else "FAIL" + out["failures"] = fails + print(json.dumps(out, indent=1)) + print("PASS_STAGED544_WIDTH_LEVER_SCREEN" if not fails else "FAIL_STAGED544_WIDTH_LEVER_SCREEN") + return 0 if not fails else 1 + + +if __name__ == "__main__": + sys.exit(main()) From 5f54d92daf2d00d3aaf6009be44247e262e58f06 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 04:46:17 +0530 Subject: [PATCH 2/3] Revise staged544 width prices: credit prior art, exact 4->3, staging screens Lead with exact width-unit prices and staging screens; demote free reductions to a monotone-price lemma with a slack-lemma proof. Credit PR3815's dual, PR3682's 8->7 shadow and PR3605's staging signature. Add the exact 4->3 price h(5)-h(3)-1 on 324/5 helper-calls, the documented-signature screen, per-call conservation 1856 and routed controls. Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 42 ++- .../staged544-width-lever-screen/PROOF.md | 213 ++++++------- .../staged544-width-lever-screen/README.md | 279 +++++++++++------- .../staged544-width-lever-screen/TASK.json | 30 +- .../staged544-width-lever-screen/VERIFY.json | 2 +- .../crosscheck_highs.py | 10 +- .../evidence/VERIFY-OUTPUT.txt | 57 ++-- .../staged544-width-lever-screen/verify.py | 109 ++++--- 8 files changed, 458 insertions(+), 284 deletions(-) diff --git a/research/staged544-width-lever-screen/CERTIFICATE.json b/research/staged544-width-lever-screen/CERTIFICATE.json index f4d6ff5a22..0e1eb50233 100644 --- a/research/staged544-width-lever-screen/CERTIFICATE.json +++ b/research/staged544-width-lever-screen/CERTIFICATE.json @@ -616,5 +616,43 @@ "48": 137952 } } - } -} \ No newline at end of file + }, + "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-width-lever-screen/PROOF.md b/research/staged544-width-lever-screen/PROOF.md index fc2c8e15c5..6640b18626 100644 --- a/research/staged544-width-lever-screen/PROOF.md +++ b/research/staged544-width-lever-screen/PROOF.md @@ -38,9 +38,11 @@ The ten patterns found by HiGHS equal PR3815's basis. Their exact primal is This reproduces PR3815's bracket with an independent enclosure. It is not a new result. -## 3. Theorem (weak duality with monotone prices) +## 3. Weak-duality screen, prices and the monotone-price lemma -Let `pi_w` (w = 1..9) and `mu_c` satisfy +`(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). @@ -51,110 +53,121 @@ 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. - -**Reductions.** Let `s'` arise from `s` by moving `z_{w->v} >= 0` -helper-calls from width `w` to any `v < w` (`v >= 1`). The right side of (*) -equals the staged544 bound plus `sum z_{w->v} (pi_v - pi_w)` plus -`9 sum (n'_r - n_r) h_lo(r)`. If `pi` is nonincreasing in width, every -reduction term is nonnegative. - -`verify.py` takes `pi_4..pi_9` and `mu` from the basis. It sets `pi_1, pi_2, -pi_3` to the largest values that keep (D) feasible, maximizing `pi_3` first -(with `pi_1 = pi_2 = pi_3`), then `pi_2`, then `pi_1`. It then checks the -following: - -- (D) holds on all 318,840 patterns. The minimum reduced cost is exactly 0. - An unbounded-knapsack recursion over used volume gives the same minimum. -- `pi_1 >= pi_2 >= ... >= pi_9`, and every `pi_w <= 0`. Hence unhosting a - helper (width 0) is also never improving. -- the staged544 bound is `F(a_hi) >= 5.28e-20 > 0`. - -**Corollary (free reductions).** If the local profile is unchanged, no reduction -of any hosted widths raises the ideal ceiling above `a_hi`. This covers any -amount, any widths and widths down to 1 or unhosting, at zero entrance cost. -Each reduction unit costs at least `pi_v - pi_w` in `F`: - -| move | exact price at a_hi | range on the basis (helper-calls) | -|---|---|---| -| 9->8, 8->7, 7->6, 6->5 | 0.987736781185353068089966 | 28, 30, 28, 28 | -| 5->4 | 1 (exactly: `[9,9,9,5]` and `[9,9,9,4]` are both basic) | 18 | -| 4->3 | >= 0.991791369039984911721564 (dual bound) | n/a | - -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 the exact change. HiGHS gives -0.9877367811860, 1.0 and 0.9917913690369 for single units of 8->7, 5->4 -and 4->3. The 4->3 dual bound is therefore attained to about 3e-12 in floating -point; exact attainment is not claimed. - -**Why monotonicity is not automatic.** A narrower helper fits gaps that wider -ones cannot. The limiting patterns of the tight extension are exact fills: -`48 = 3 + 5*9` limits `pi_3`, `48 = 2 + 5*9` (leftover 1) limits `pi_2`, and -`32 = 1 + 4 + 3*9` limits `pi_1`. So the width-4..9 dual (2,551 patterns) does -not by itself give a monotone feasible extension. The control -`granularity_raised_pi3_infeasible_on_1_to_9` raises `pi_1..pi_3` by 1e-30 above -the tight value. The prices stay monotone and feasible on all 2,551 width-4..9 -patterns, but some width-1..9 pattern becomes infeasible. - -## 4. Paid-rank identity and what the corollary does not cover - -On three pinned T360 profiles, `sum_r n_r r = (896*73 - 320) T = 23,431,680`: - -- PR3682's finite profile (LEAD1-PRICE.json); -- PR3734's finite profile (inputs/PROFILE.json); -- PR3815's clock fill (inputs/PROFILE.json). - -The identity was observed on these three profiles; it is not proved here. If it -holds for every literal construction of this template, a free reduction is -not realizable. It adds `w - v` units of paid leftover with no offsetting local -change. A real staging move must then remove `w - v` units of local paid rank. -PR3734's change does exactly this: width 8->7 together with local -`{1:+3, 2:+1, 3:-2}`, a rank-sum change of -1 per call. So the corollary in -section 3 is **not** an upper relaxation of real staging. The correct screen is (*) -with the actual `n'`. - -**Staging screen.** Suppose one unit `w -> w-1` is paid by removing one unit -from a single local child (`r -> r-1`). That saves `h(r) - h(r-1) <= h(1) = 1` -by concavity, with equality when a rank-1 child is deleted. By (*), the change -in `F` is at least `price - 1`. The ceiling can therefore rise only if the -price is below 1: - -- w in {6..9}: gain at most 0.012263218814646931910033 per helper-call. This is - exact within the ranges above for a rank-1 deletion. -- w = 5: gain at most 0. Single-child-compensated 5->4 staging never raises - the ceiling, in any amount. -- w = 4: gain at most 0.008208630960015088278435. - -Local rewrites that also merge or split children are priced exactly by -`9 sum (n'_r - n_r) h(r)` in (*). They are a separate local-word lever. - -## 5. PR3682 -> staged544 decomposition (exact at a_hi) - -All four corners have the same optimal basis. Each primal is `y >= 0` with -dual feasibility on 2,551 patterns, and each enclosure gap is below 1e-70. -Because `(pi, mu)` depends only on `a`, the interaction term is exactly 0. The -four corners are PR3682 (inventory `{...,7:52,8:97,...}`, local -`{1:2437,2:724,3:226,...}`), width-only, local-only and staged544: - -- width part (one 8->7 per call): +8.889631030668177612809695088162 - = 9 x 0.987736781185353068089966...; +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 exact fills: + `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 never raises the ideal ceiling. 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). + 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. + per call (the documented-signature gain). -Under the identity neither single change is realizable. 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). PR3734's gain is the margin of its local -saving over the exact width-unit price. Against the single-child reference, its -local change gives up 0.008998918419970962488711 per call to reshaping: -`{1:+4,2:+1,3:-2}` has zero rank change and a positive cost. That is about 73% -of the 0.012263 available. +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 paid-rank identity is observed, not derived. The -first-order conversion `dF/da ~ 184132` is floating point. No kappa, -supplier or admission claim is made. +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-width-lever-screen/README.md b/research/staged544-width-lever-screen/README.md index e58ae1f889..a3058274e5 100644 --- a/research/staged544-width-lever-screen/README.md +++ b/research/staged544-width-lever-screen/README.md @@ -1,4 +1,4 @@ -# Staged544 width-lever screen: exact width prices for the fixed-T360 ideal +# Staged544 width-unit prices: the exact staging break-even in the fixed-T360 ideal **Scoped exact result about the clock-free fixed-bin ideal. It makes no kappa claim, is not a construction and is not a complete multiplication theorem.** @@ -10,76 +10,108 @@ The model is PR3815's fixed-inventory ideal of the staged544 T360 template `{4:26,5:2,6:18,7:53,8:96,9:213}`, idle bins `{8:672,16:448,32:448,48:448}`, local profile `{1:2440,2:725,3:224,4:102,5:20,8:8}` and 896 live rank-73 families. Packings may be fractional and any clock is allowed. Details are in -[PROOF.md](PROOF.md). +[PROOF.md](PROOF.md). A "width unit" is one helper-call (one helper in one of +the nine calls) moved one width step; prices are in `F` units per replica at +`a_hi = 0.001730578437266246818741`, the upper end of the staged544 ceiling +bracket `[0.001730578437266246818740, ...741]` (this bracket reproduces PR3815). -1. **Priced screen (exact, proved).** One dual `(pi, mu)` is feasible on **all - 318,840** bin patterns with widths 1..9, with exact minimum reduced cost 0. - Its helper prices are nonincreasing in width and nonpositive. By weak - duality, every changed inventory `s'` over widths 1..9 with these bins and - any changed local profile `n'` satisfies +1. **Exact width-unit prices, within basis ranges.** PR3815's basis dual + `(pi_4..pi_9, mu)`, evaluated exactly at `a_hi`, gives: + + | move | price per width unit | exact for up to (helper-calls per replica) | + |---|---|---| + | 9->8, 8->7, 7->6, 6->5 | `(h(48)-h(3)-5h(5))/20` = 0.987736781185353068089966 | 28 / 30 / 28 / 28 | + | 5->4 | `h(1)-h(0)` = 1 | 18 | + | 4->3 | `h(5)-h(3)-1` = 0.991791369039984911721564 | 324/5 = 64.8 | + + The 6..9 closed form is PR3682's 8->7 width shadow (zxv, `price.py`); the + new content is that the same price holds for every step on 6..9 (the dual + is affine on widths 5..9), the exact 5->4 and 4->3 prices and all the + ranges. The 4->3 price is exact because the column `[3,9^5]` in a 48-bin + is tight under the tight extension of `pi_1..pi_3`, which is dual feasible + on all 318,840 width-1..9 patterns; `verify.py` checks the four-column + move and its range exactly. Outside a range the price is a lower bound + for every further unit (convexity of the LP value). +2. **Staging screens (exact arithmetic, per width unit).** A literal staging + move must also change the local profile (item 4). Its net change in `F` is + (local saving) minus (price): + - **Documented signature.** All three observed staging units (644 and 660 + in PR3605, 544 in PR3734) change the local profile by `{1:+3,2:+1,3:-2}` + per unit (PR3605 PROOF: `3H1 + H2 - 2H3`), saving + 0.991001081580029037511288. Gain: **+0.003264300394675969421322** for + 6..9, **-0.008998918419970962488711** for 5->4 and + **-0.000790287459955874210276** for 4->3. So with this signature only + width-6..9 staging pays, and 5->4 and 4->3 staging lose. + - **Hypothetical rank-1 deletion** (single-child compensation, saving + `h(1) = 1`, the most any single-child decrement `r -> r-1` saves). 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 cost is not priced; these are + upper references, not leads. A local rewrite that also merges children + can save more than 1 and is priced by the local term of (*) below. + - The gap between the two is 0.008998918419970962488711 per unit. Whether + any literal staging achieves a smaller gap is open. +3. **General screen (*).** By weak duality with the same `(pi, mu)`, any + changed inventory `s'` over widths 1..9 with these bins and any local + profile `n'` satisfies `F(a_hi) >= 9 sum n'_r h(r) + 9 sum pi_w s'_w + sum mu_c B_c - 896 h(73)` (*) - at `a_hi = 0.001730578437266246818741`. The staged544 inventory gives - `F(a_hi) >= 5.28e-20 > 0`. -2. **Theorem (free reductions; proved negative result).** No reduction of the - hosted widths of any helpers, by any amount and down to width 1 or - unhosting, at zero entrance cost, raises the ideal ceiling above - `0.001730578437266246818741`. This holds when the local profile is - unchanged. The ceiling itself lies in - `[0.001730578437266246818740, 0.001730578437266246818741]`, which - reproduces PR3815. -3. **Exact width-unit prices** in `F` units per helper-call, at `a_hi`: - - | move | price | exact range on the basis | - |---|---|---| - | 9->8, 8->7, 7->6, 6->5 | 0.987736781185353068089966 | 28 / 30 / 28 / 28 helper-calls | - | 5->4 | 1 exactly | 18 | - | 4->3 | >= 0.991791369039984911721564 | not established (HiGHS attains it to 3e-12) | - - By convexity each price is a lower bound for every further unit. -4. **Theorem 2 does not bound real staging.** The paid rank sum is the same on - all three pinned T360 profiles: PR3682 finite, PR3734 finite and PR3815 clock - fill all give `sum n_r r = 23,431,680 = (896*73 - 320)*360`. This identity - is observed, not proved. Where it holds, a free reduction is not realizable. - A literal staging unit must remove one unit of local paid rank, which saves - up to `h(1) = 1`. With such single-child compensation, a unit can gain at most: - - **0.012263218814646931910033** per helper-call for widths 6..9. This is - exact within the ranges above when the compensation deletes a rank-1 child. - - **0** for 5->4. Single-child-compensated 5->4 staging never raises the - ceiling, in any amount. - - **0.008208630960015088278435** for 4->3. -5. **PR3682 -> staged544, exact at `a_hi`.** All four corners share one optimal - basis, so the interaction term is exactly 0. - - Width part (one 8->7 per call): `+8.889631030668177612809695088162`. - - Local part: `-8.919009734220261337601597266358`, a saving of - 0.991001081580029037511288 per call. - - Net: `-0.029378703552083724791902178195`. - - Neither single change is realizable under the identity. Width-only moves - the ideal root to about 0.0016821 and local-only to about 0.0017788 (HiGHS, - float). PR3734's ideal gain of 0.003264300394675969421322 per call is the - margin of its local saving over the exact price. Its local change gives up - 0.008998918419970962488711 per call (about 73% of the 0.012263 available) - to reshaping: `{1:+4,2:+1,3:-2}` has zero rank change and a positive cost. - -To first order, `dF/da ~ 184132` at the ceiling (floating point). Staging one -more width-6..9 helper in all nine calls with rank-1-deletion compensation would -raise the ideal ceiling by about 6.0e-7. PR3734 realized about 1.6e-7. + This is the screen PR3815's open question 1 suggests; here it is extended + to widths 1..9. The staged544 inventory gives `F(a_hi) >= 5.28e-20 > 0`. + `mu` (`mu_48 = 47.679502755263063473958379`) gives subgradient bin prices + only: no bin-row ranging was done. +4. **Per-call conservation (observed).** Local paid rank minus hosted helper + width is 1856 per call on both pinned (inventory, local) pairs, PR3682 and + staged544, so the total paid rank is `9*1856 + sum c B_c = 896*73 - 320` + per replica. PR3605 states the same conservation for its staging ("the + local rank mass falls by 2, exactly matching the owned-width decrease"). + The PR3734 finite and PR3815 clock-fill profiles share one pair, so their + total of 23,431,680 at `T = 360` is implied, not independent. The + conservation is observed, not derived. Where it holds, a width reduction + with an unchanged local profile is not realizable, which is why item 2 + prices staging with a local change. +5. **Monotone-price lemma (free reductions).** With `pi_1 = pi_2 = pi_3 = + pi_4`, the prices are nonincreasing and nonpositive and still dual feasible + on all width-1..9 patterns. This follows from PR3815's 2,551-pattern dual + and `pi_4 <= -3` by a two-line slack lemma (PROOF section 3); `verify.py` + also checks it on all 318,840 patterns. Hence a width reduction (to any + width `>= 1`, or unhosting) with an unchanged local profile never raises + the ideal ceiling. Under item 4 such a move is not realizable, so this is a + consistency statement about the model, not a staging closure. +6. **PR3682 -> staged544 split at `a_hi`.** `F` is additively separable in + inventory and local profile at fixed `a`, so the 2x2 interaction is + identically 0. Width part (one 8->7 per call, inside the range 30): + `+8.889631030668177612809695088162` = 9 x the price. Local part: + `-8.919009734220261337601597266358`. Net + `-0.029378703552083724791902178195`, i.e. the documented-signature gain + 0.003264300394675969421322 per call. Either change alone breaks the + conservation: width-only moves the ideal root to about 0.0016821, + local-only to about 0.0017788 (HiGHS, float). + +To first order, `dF/da ~ 184132` at the ceiling (floating point). One more +width-6..9 staging in all nine calls with the documented signature would raise +the ideal ceiling by about 1.6e-7 (9 x 0.003264 / 184132); a hypothetical +rank-1 deletion would give about 6.0e-7. For comparison, the staged544 +inventory's ideal gain over PR3682 is about 1.6e-7 (realized on a literal clock +by PR3815 and PR3802); PR3734's own finite fill realized about 2.9e-8. ## Decision informed This informs expansion-gate point 4 for the staged-entrance family (#3606), the -engine of #3605 and #3734. It also partly answers PR3815's open question 1. - -- Free width reduction is not a lever. -- 5->4 staging is closed under single-child compensation. -- Staging width-6..9 (and 4->3) helpers remains open in the ideal. The test for - a candidate is now one exact inequality: its local saving must exceed the - price above. -- The cheapest identified improvement is to avoid PR3734-type reshaping (up to - 0.008999 per call). -- Bin changes are priced by `mu`. The local word is priced by `h(r)`. +engine of #3605 and #3734, and partly answers PR3815's open question 1. The +family is tracked in #3606; it is not a revision-6 lead. + +- With the documented staging signature, only width-6..9 staging pays + (+0.003264 per width unit); 5->4 and 4->3 staging lose. +- A candidate staging is decided by one exact inequality: its local saving per + width unit must exceed the price in item 1 (within the ranges). +- Even a hypothetical rank-1-deletion compensation cannot make 5->4 staging + pay. +- The largest identified slack is the 0.008999 per unit between the documented + signature and a rank-1 deletion. Whether a literal staging can avoid it is + open. +- Free width reduction is not a lever (item 5). ## Reproduce @@ -90,21 +122,23 @@ python3.12 -B scripts/research_package.py --package research/staged544-width-lev The verifier is standard-library only and runs in about 6 s. It can also be run directly as `python3 -B research/staged544-width-lever-screen/verify.py`. The expected last line is `PASS_STAGED544_WIDTH_LEVER_SCREEN`, preceded by a JSON -report with every number above. The output was identical under Python 3.12.15 +report with every exact number above. The output was identical under Python 3.12.15 and 3.14.4. **Negative controls (each must fail; the verifier asserts they do):** - `pi_9 + 1e-30` makes the dual infeasible. -- `granularity_raised_pi3_infeasible_on_1_to_9`: raising `pi_1..pi_3` 1e-30 - above the tight extension leaves the prices monotone and feasible on the - 2,551 width-4..9 patterns, but infeasible on widths 1..9. This is why the - 318,840-pattern check is needed. -- A non-monotone extension is rejected. -- The dual bound at `a_lo` is not positive. +- Raising the tight `pi_1..pi_3` by 1e-30 makes some width-1..9 pattern + infeasible (the tight extension, and so the exact 4->3 price, is tight). +- A non-monotone extension is rejected by the same `monotone` check the lemma + uses. - One 8->9 widening per call drops the bound to `<= 0` (widening is priced as a gain). -- A +1 change to a profile breaks the paid-rank identity. +- A +1 change to the PR3734 histogram fails the same `paid_rank_ok` check the + profiles pass. + +One consistency check (not a mutation): the dual bound at `a_lo` is not +positive, as implied by `F_upper(a_lo) < 0` and weak duality. **Second, independent method (floating point):** `crosscheck_highs.py` used Python 3.14.4, numpy 2.5.4 and scipy 1.18.1 HiGHS. It generates patterns as @@ -115,25 +149,38 @@ monotonicity, and bisects the root. Its recorded output is - Fixed staged544 root 0.0017305784372662612. - Free reductions over 318,840 patterns: 0.0017305784372661503. This is not higher; the 1.1e-16 difference is float noise. -- The stage-move variant matches the fixed root. - PR3682 ideal root 0.0017304188997660508. -- Single-unit prices 0.9877367811860 (8->7), 1.0 (5->4) and 0.9917913690369 (4->3). +- Single-unit prices 0.9877367811860 (8->7), 1.0 (5->4) and 0.9917913690369 + (4->3), agreeing with the exact values to about 3e-12. +- The `stage` variant (`s544_stage_w1`) charges each move `h(2)-h(1)`. That + is the superseded task-card model, which adds local rank; it is not the + staging accounting used here and is kept only as recorded output. It is not part of the registered replay. ## What is new -PR3815 certified the fixed staged544 inventory on 2,551 patterns. The -async505 inventory wall, PR3630 and PR3638 priced other inventories with fixed -widths. The following are new here: - -- the dual extension to all widths 1..9 with monotone prices; -- the general priced screen (*); -- exact width-unit prices and their ranges; -- the single-child staging bounds; -- the observed paid-rank identity and its consequence that free reductions do - not bound real staging (this corrects the premise of this package's task card); -- the exact PR3682 -> staged544 decomposition. +Prior art, credited: PR3815 (ChaloupeMusic) solves the basis dual +`(pi_4..pi_9, mu)` in `ceiling_certificate.py` and suggests pricing changed +inventories with it (open question 1). PR3682's `price.py` (zxv) has the +closed-form 8->7 width shadow `(h(48)-h(3)-5h(5))/20` and the "staged net = +local delta + width shadow" calibration of PR3605. PR3605's PROOF +(RossRichardson) derives the per-helper staging delta `3H1 + H2 - 2H3` and +states that local rank mass falls with the owned width. The async505 inventory +wall, PR3630 and PR3638 priced other inventories with fixed widths. + +New here: + +- evaluation of that dual exactly at `a_hi`, the common 6..9 price (affine dual + on widths 5..9), `5->4 = 1` and the exact `4->3 = h(5)-h(3)-1`; +- the basis ranges (18 to 30, and 324/5 for 4->3); +- the extension of the dual to widths 1..9 (cheapest and tight), with the slack + lemma; +- the two staging screens per width (documented signature and rank-1 + reference), including that 5->4 and 4->3 staging lose under the documented + signature; +- the per-call conservation 1856 checked on both pinned pairs; +- the exact PR3682 -> staged544 split with the per-width break-even. ## Sources @@ -158,44 +205,56 @@ them. This is a stated gap. PR3815's payment rule (one rank-`l` child per remainder). Template, stock and clock effects are out of scope. PR3815 traced PR3734's shortfall from its ideal to the clock. -- **Paid-rank identity.** It was observed on three pinned profiles and is not - derived. The statements in item 4 that depend on it are conditional on it. +- **Per-call conservation.** Observed on two pinned (inventory, local) pairs + and stated by PR3605 for its staging; not derived. The non-realizability of + free reductions depends on it. +- **Staging signature.** The documented signature is what the three observed + staging units use; it is not proved to be forced. The rank-1-deletion + reference has no known realization. - **Admission costs not priced.** All admission costs of a changed inventory are unknown and are not zero. These include physical stock, coverage law and template checks, literal staging identities and clock feasibility. -- **Ranges.** Exact prices hold within the stated ranges of one basis. Outside - them they are lower bounds. The 4->3 value is a lower bound only. +- **Ranges.** Exact prices hold within the stated ranges. Outside them they are + lower bounds. `mu` is a subgradient (lower-bound) bin price only. - **Floating-point values.** `dF/da`, the ceiling conversions and the HiGHS values are floating point. - **No kappa.** No kappa, frontier or selected-result change is claimed. ## Open next questions -- **Does the paid-rank identity `sum n_r r = 65088 T` hold for every literal - construction of this template?** If it does, items 4 and 5 become - unconditional. First step: derive it from the owner and frame accounting in - PR3734's `owner_audit.py`, or find a construction that violates it. -- **Can a width-6..9 helper be staged with rank-1-deletion compensation and no - reshaping?** Each such helper is worth up to 0.110369 in `F` (about 6e-7 of - ceiling) within the ranges. First step: list PR3734's helpers with a rank-1 - entrance and price their literal staging local deltas with the screen (*). -- **What does the template lever (bins) offer?** `mu` gives exact bin prices - (`mu_48 = 47.679502755263063473958379`). First step: write a candidate - template's bin counts and evaluate the screen (*). Re-solve the LP for changes - outside the basis ranges. +- **Is the staging signature `{1:+3,2:+1,3:-2}` forced?** A literal width-6..9 + staging with a smaller gap to a rank-1 deletion would gain up to 0.008999 per + width unit more. First step: in PR3734's frames, check whether PR3682's + delayed donor release (`{1:-2,2:-2,3:+2}`, worth about 0.0066 per call) can be + re-applied on top of the staged544 local profile; then price the result + with (*). +- **Does the per-call conservation (local paid rank minus hosted width = 1856) + hold for every literal construction of this template?** First step: derive it + from the owner and frame accounting in PR3734's `owner_audit.py`, or find a + construction that violates it. +- **What do bin-count changes offer?** `mu` gives subgradient bin prices. First + step: write a candidate template's bin counts and evaluate (*), re-solving the + LP outside the (unknown) bin ranges. New bin ranks are constrained by + concurrent PR3836 (Matarener), which shows the idle alphabet is forced within + bridge-based nine-stage schedules; changing bin counts stays open. ## Credit -The model, bins, payment rule and basis are from PR3815 (ChaloupeMusic, head -`77ffbf28`). The staged544 inventory and local profile are from PR3734 -(dataisfire, head `fa041037`). The predecessor inventory is from PR3682 (zxv, -head `431e6c60`). The staged-entrance mechanism is from PR3605 (RossRichardson), -with lineage through PR3795/PR3802 (hexapode). The width-price method follows +The model, bins, payment rule, basis and basis dual are from PR3815 +(ChaloupeMusic, head `77ffbf28`). The staged544 inventory and local profile are +from PR3734 (dataisfire, head `fa041037`). The predecessor inventory, the +closed-form 8->7 width shadow and the staged-net calibration are from PR3682 +(zxv, head `431e6c60`, `price.py`). The staged-entrance mechanism, the +per-helper staging delta `3H1 + H2 - 2H3` and the rank-mass/width statement are +from PR3605 (RossRichardson, head `3efbb5de`, PROOF lines 146-164), with lineage +through PR3795/PR3802 (hexapode). The width-price method follows `research/experiment-log/negative-searches/async505-inventory-wall` (Rohan -Arun), PR3630 (RossRichardson) and PR3638 (zxv). -No predecessor code is copied. `verify.py`'s enclosures, enumeration, knapsack -check and LP algebra are new. +Arun), PR3630 (RossRichardson) and PR3638 (zxv). PR3836 (Matarener) is cited +for the idle alphabet. No predecessor code is copied. `verify.py`'s +enclosures, enumeration, knapsack check and LP algebra are new. Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from -Claude (Anthropic, Claude Opus 5.5). Checked by AI review passes in the same -loop. No human or formal-kernel verification is claimed. Apache-2.0. +Claude (Anthropic, Claude Opus 5.5). Reviewed by four AI review passes in the +same loop (reproducibility, mathematical audit, provenance, referee), followed +by one revision; no human or formal-kernel verification is claimed. +Apache-2.0. diff --git a/research/staged544-width-lever-screen/TASK.json b/research/staged544-width-lever-screen/TASK.json index 8236232364..92625be6c5 100644 --- a/research/staged544-width-lever-screen/TASK.json +++ b/research/staged544-width-lever-screen/TASK.json @@ -46,32 +46,32 @@ ] }, "scope_status": "refined", - "actual_scope": "Narrowed to one helper-inventory lever of the staged544 T360 template (PR3734/PR3815): exact prices of hosted-width changes in the clock-free fixed-bin ideal. The deliverables are an exact dual over all 318,840 width-1..9 bin patterns with monotone, nonpositive helper prices; the theorem that free width reductions never raise the ideal ceiling 0.001730578437266246818741; exact width-unit prices with basis ranges; single-child staging bounds under the observed paid-rank identity; and the exact PR3682 -> staged544 decomposition. No new contract and no kappa.", - "scope_change_reason": "The card asks for a changed helper inventory. Staging (hosted-width reduction) is the engine of the pending gains in #3605 and #3734, and PR3815's open question 1 asks which changed T360 inventory raises the ceiling, so this package prices that lever exactly instead of proposing a contract. The task card's premise that a free width reduction is an upper relaxation of real staging was corrected during the work. All three pinned T360 profiles satisfy sum n_r r = 65088 T. Under that identity a literal staging unit must also remove one unit of local paid rank, so the package adds the single-child staging screen.", + "actual_scope": "Narrowed to one helper-inventory lever of the staged544 T360 template (PR3734/PR3815): exact prices of hosted-width changes in the clock-free fixed-bin ideal. Deliverables: exact width-unit prices at a_hi = 0.001730578437266246818741 with basis ranges (0.987736781185353068089966 for 6..9, 1 for 5->4, h(5)-h(3)-1 = 0.991791369039984911721564 for 4->3 on 324/5 helper-calls); two staging screens per width (documented PR3605 signature {1:+3,2:+1,3:-2}: +0.003264300394675969421322 for 6..9, -0.008998918419970962488711 for 5->4, -0.000790287459955874210276 for 4->3; hypothetical rank-1 deletion: at most 0.012263218814646931910033, 0 and 0.008208630960015088278435); the weak-duality screen (*) over widths 1..9; the monotone-price lemma for free reductions; the per-call conservation 1856 on both pinned pairs; and the PR3682 -> staged544 split. No new contract and no kappa.", + "scope_change_reason": "The card asks for a changed helper inventory. Staging (hosted-width reduction) is the engine of the pending gains in #3605 and #3734, and PR3815's open question 1 asks which changed T360 inventory raises the ceiling, so this package prices that lever exactly instead of proposing a contract. The task card's premise that a free width reduction is an upper relaxation of real staging was corrected: on both pinned (inventory, local) pairs, local paid rank minus hosted width is 1856 per call (PR3605 states the same conservation), so a literal staging unit also changes the local profile. The package therefore prices staging with its local change.", "bottleneck_link": "The complex primitive binds the selected conditional kappa. The staged-entrance family's gains (#3605, #3734) are ideal-packing gains of the complex local word. This package gives the exact price at which staging a helper pays in that ideal: (*) in README/PROOF. Expansion-gate point 4 (stage more helpers versus redirect to bins or the local word) can therefore be decided per candidate by one inequality.", "budget_minutes": 90, "stop_rule": "Stop if the exact certificate fails and report the improving width move instead; ship without the decomposition if the PR3682 inventory is not pinned within 15 minutes; stop at the iteration deadline; stop and post nothing if a competing staged544 width or inventory pricing appears before submission.", "outcome": "completed", - "evidence": "verify.py (stdlib, about 6 s) prints PASS_STAGED544_WIDTH_LEVER_SCREEN. Ceiling bracket [0.001730578437266246818740, ...741]: F(a_lo) <= -1.31e-19 and F(a_hi) >= 5.28e-20. Dual feasible on 318,840 patterns with minimum reduced cost exactly 0, matched by a knapsack recursion. Prices monotone and nonpositive. Width-unit prices: 0.987736781185353068089966 (6..9), 1 (5->4), >= 0.991791369039984911721564 (4->3). Single-child staging gain bounds: 0.012263218814646931910033, 0 and 0.008208630960015088278435. Decomposition: width +8.889631030668177612809695088162, local -8.919009734220261337601597266358, interaction exactly 0. Paid-rank identity holds on 3 pinned profiles. Six negative controls fail as required. Second method: HiGHS (evidence/HIGHS.json) agrees to about 1e-11 in F and 1e-16 in roots.", + "evidence": "verify.py (stdlib, about 6 s) prints PASS_STAGED544_WIDTH_LEVER_SCREEN. Ceiling bracket [0.001730578437266246818740, ...741]: F(a_lo) <= -1.31e-19 and F(a_hi) >= 5.28e-20 (reproduces PR3815). Cheapest and tight dual extensions feasible on 318,840 patterns with minimum reduced cost exactly 0, matched by a knapsack recursion; slack-lemma premises hold (margin 0.986093083432664503980103). Width-unit prices: 0.987736781185353068089966 (6..9, ranges 28/30/28/28), 1 (5->4, range 18), 0.991791369039984911721564 (4->3, range 324/5). Documented-signature gains +0.003264300394675969421322 / -0.008998918419970962488711 / -0.000790287459955874210276; rank-1-deletion references 0.012263218814646931910033 / 0 / 0.008208630960015088278435. Split: width +8.889631030668177612809695088162, local -8.919009734220261337601597266358 (interaction identically 0 by separability). Per-call conservation 1856 on both pairs. Five negative controls fail as required. Second method: HiGHS (evidence/HIGHS.json) agrees to about 3e-12 in prices and 1e-16 in roots.", "author": "Sagar Thakrar (thakrarsagar)", - "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for design, code, proofs and text. Checked by AI review passes in the same loop. No human or formal-kernel verification is claimed.", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for design, code, proofs and text. Reviewed by four AI review passes in the same loop (reproducibility, mathematical audit, provenance, referee), followed by one revision. No human or formal-kernel verification is claimed.", "open_questions": [ { - "question": "Does the paid-rank identity sum n_r r = 65088 T hold for every literal construction of the staged544 T360 template?", - "why_it_matters": "It turns the conditional staging statements (single-child bounds, non-realizability of free reductions) into unconditional ones.", - "first_step": "Derive the identity from the owner and frame accounting in PR3734's owner_audit.py, or exhibit a literal construction that violates it.", - "blocked_by": "Reading the unmerged PR3734 owner/frame accounting; not done in this time box." + "question": "Is the staging signature {1:+3,2:+1,3:-2} forced for width-6..9 staging of this template?", + "why_it_matters": "A literal staging with a smaller gap to a rank-1 deletion would gain up to 0.008999 more per width unit; with the signature the gain is 0.003264.", + "first_step": "In PR3734's frames, check whether PR3682's delayed donor release {1:-2,2:-2,3:+2} can be re-applied on top of the staged544 local profile, then price it with (*).", + "blocked_by": "Reading PR3734's literal frames and staging identities; not done in this time box." }, { - "question": "Can a width-6..9 helper be staged with rank-1-deletion compensation and no reshaping?", - "why_it_matters": "Each such helper (9 helper-calls, within the basis ranges) is worth up to 0.110369 in F, about 6e-7 of ideal ceiling, versus 1.6e-7 realized by PR3734.", - "first_step": "List PR3734's helpers with a rank-1 entrance and price each literal staging local delta with screen (*) before any synthesis.", - "blocked_by": "Literal staging identities, clock feasibility and the full admission of the changed word; all unpriced here." + "question": "Does the per-call conservation (local paid rank minus hosted width = 1856) hold for every literal construction of this template?", + "why_it_matters": "It makes the non-realizability of free reductions unconditional.", + "first_step": "Derive it from the owner and frame accounting in PR3734's owner_audit.py, or exhibit a literal construction that violates it.", + "blocked_by": "Reading the unmerged PR3734 owner/frame accounting." }, { - "question": "Which bin-template changes pass screen (*) once the bins are allowed to change?", - "why_it_matters": "The bin prices mu are exact on the current basis, and PR3815's open question 1 asks for a changed T360 inventory.", - "first_step": "Write a candidate template's bin counts, evaluate (*), and re-solve the LP for changes outside the basis ranges.", + "question": "Which bin-count changes pass screen (*)?", + "why_it_matters": "mu gives subgradient bin prices; PR3815's open question 1 asks for a changed T360 inventory. New bin ranks are constrained by concurrent PR3836 (Matarener) within bridge-based nine-stage schedules.", + "first_step": "Write a candidate template's bin counts, evaluate (*), and re-solve the LP outside the unknown bin ranges.", "blocked_by": "Physical stock, coverage law and template checks of the complete admission." } ] diff --git a/research/staged544-width-lever-screen/VERIFY.json b/research/staged544-width-lever-screen/VERIFY.json index a0a8734a64..46c36267c3 100644 --- a/research/staged544-width-lever-screen/VERIFY.json +++ b/research/staged544-width-lever-screen/VERIFY.json @@ -12,7 +12,7 @@ "{package}/verify.py" ], "timeout_seconds": 300, - "checks": "Exact staged544 ceiling bracket; dual feasibility on all 318,840 width-1..9 patterns (enumeration plus knapsack); monotone nonpositive prices; free-reduction theorem; width-unit prices and ranges; paid-rank identity on 3 profiles; exact PR3682->staged544 decomposition; six negative controls must fail. Prints PASS_STAGED544_WIDTH_LEVER_SCREEN." + "checks": "Exact staged544 ceiling bracket; PR3815 basis dual with cheapest and tight width-1..9 extensions feasible on all 318,840 patterns (enumeration plus knapsack) and the slack-lemma premises; exact width-unit prices with basis ranges, including 4->3 = h(5)-h(3)-1 on 324/5 helper-calls; documented-signature and rank-1-deletion staging screens; per-call conservation 1856 on both pinned pairs and total paid rank on 3 profiles; PR3682->staged544 split; five negative controls must fail plus one consistency check. Prints PASS_STAGED544_WIDTH_LEVER_SCREEN." } ] } diff --git a/research/staged544-width-lever-screen/crosscheck_highs.py b/research/staged544-width-lever-screen/crosscheck_highs.py index e325145b45..c9a60e3f06 100644 --- a/research/staged544-width-lever-screen/crosscheck_highs.py +++ b/research/staged544-width-lever-screen/crosscheck_highs.py @@ -3,10 +3,12 @@ Patterns are generated as integer partitions (descending part lists), not by the count-vector recursion of verify.py. Reduction columns move one helper-call from -width w to any width v < w at zero cost ("free") or, for the staging move w -> w-1, -at the local entrance price h(2) - h(1) ("stage"). Prints JSON with roots and the -positive (basic) patterns, which verify.py re-checks exactly. -Requires numpy and scipy (see VERIFY.json requirements). +width w to any width v < w at zero cost ("free") or, for the move w -> w-1, at +h(2) - h(1) ("stage"). The "stage" mode is the superseded task-card model, which +adds local rank; it is NOT the staging accounting of README/PROOF and is kept only +as recorded output. Prints JSON with roots and the positive (basic) patterns. +Requires numpy 2.5.4 and scipy 1.18.1 (as used for evidence/HIGHS.json); not part +of the registered replay, see README. """ import json import math diff --git a/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt b/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt index fd2d8a268e..1861dac9dd 100644 --- a/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt +++ b/research/staged544-width-lever-screen/evidence/VERIFY-OUTPUT.txt @@ -6,7 +6,11 @@ "F_lower_at_a_hi": "0.000000000000000000052805837005", "primal_min_y": "7" }, - "free_reduction_theorem": { + "monotone_price_lemma": { + "slack_lemma_premises": { + "dual_feasible_widths_4_to_9": true, + "margin_minus_pi4_minus_3": "0.986093083432664503980103" + }, "patterns_widths_1_to_9": 318840, "patterns_widths_4_to_9": 2551, "min_reduced_cost_all": "0.000000000000000000000000000000", @@ -28,7 +32,8 @@ ] ], "monotone": true, - "holds": true + "holds": true, + "note": "free reductions keep F(a_hi) > 0; under the per-call conservation (section 5) such a move is not realizable" }, "prices_at_a_hi": { "helper_pi": { @@ -55,7 +60,6 @@ "8->7": "0.987736781185353068089966", "9->8": "0.987736781185353068089966" }, - "entrance_raise_1_to_2": "0.997602347205330147005789", "delete_rank1_child": "-1.000000000000000000000000", "primal_y": { "8:000010": "672", @@ -79,13 +83,14 @@ "4->2": "1.991791369039984911721564", "4->1": "2.986093083432664503980103" }, - "explicit_4_to_3_move_cost_lower_enclosure": "0.997602347205330147005789", + "width_unit_price_4_to_3_exact": "0.991791369039984911721564", "exact_range_helper_calls_per_replica": { "5->4": "18", "6->5": "28", "7->6": "28", "8->7": "30", - "9->8": "28" + "9->8": "28", + "4->3": "324/5" }, "tight_extension_min_reduced_cost": "0.000000000000000000000000000000", "tight_extension_limiting_patterns": { @@ -133,24 +138,40 @@ ] } }, - "staging_screen_per_helper_call": { - "single_child_compensation_upper_reference": { + "staging_screen_per_width_unit": { + "single_child_rank1_deletion_upper_reference": { + "4->3": "0.008208630960015088278435", "5->4": "0.000000000000000000000000", "6->5": "0.012263218814646931910033", "7->6": "0.012263218814646931910033", "8->7": "0.012263218814646931910033", - "9->8": "0.012263218814646931910033", - "4->3": "0.008208630960015088278435" + "9->8": "0.012263218814646931910033" + }, + "documented_signature": { + "1": 3, + "2": 1, + "3": -2 + }, + "documented_signature_saving": "0.991001081580029037511288", + "documented_signature_gain": { + "4->3": "-0.000790287459955874210276", + "5->4": "-0.008998918419970962488711", + "6->5": "0.003264300394675969421322", + "7->6": "0.003264300394675969421322", + "8->7": "0.003264300394675969421322", + "9->8": "0.003264300394675969421322" }, - "pr3734_local_saving": "0.991001081580029037511288", - "pr3734_net_gain": "0.003264300394675969421322", - "pr3734_reshaping_cost": "0.008998918419970962488711" + "gap_signature_vs_rank1_deletion": "0.008998918419970962488711" }, "first_order_float": { "dF_da_at_ceiling": 184132.35902592752, "ceiling_change_per_unit_F_decrease": 5.430875948638614e-06 }, - "paid_rank_identity": { + "per_call_local_rank_minus_hosted_width": { + "staged544": 1856, + "pr3682": 1856 + }, + "paid_rank_total": { "pr3682_finite": { "T": 360, "paid_rank_sum": 23431680, @@ -184,11 +205,13 @@ }, "controls_failed_as_required": { "perturb_pi9_up_1e-30": true, - "granularity_raised_pi3_infeasible_on_1_to_9": true, - "non_monotone_extension_rejected": true, - "bound_at_a_lo_not_positive": true, + "tight_extension_raised_1e-30_infeasible": true, + "non_monotone_extension_rejected_by_monotone_check": true, "one_8_to_9_widening_per_call_breaks_bound": true, - "volume_identity_detects_plus_one": true + "paid_rank_check_detects_plus_one": true + }, + "consistency_checks": { + "bound_at_a_lo_not_positive": true }, "status": "PASS", "failures": [] diff --git a/research/staged544-width-lever-screen/verify.py b/research/staged544-width-lever-screen/verify.py index f786f90243..73dece2075 100644 --- a/research/staged544-width-lever-screen/verify.py +++ b/research/staged544-width-lever-screen/verify.py @@ -10,15 +10,20 @@ Checks (all exact rational arithmetic; h(l) = l^(1-a) enclosed by series with remainder bounds, rounded outward to 1e-90): - 1. staged544 ceiling bracket (a_lo, a_hi) from an exact primal/dual pair. - 2. free width reductions: dual over ALL 318,840 bin patterns with widths 1..9 - plus monotone helper prices => no reduction of any widths, by any amount, - to any width >= 1, at zero cost, gives F(a_hi) <= 0. Cross-checked by an - unbounded-knapsack recursion (different algorithm, same claim). - 3. exact width-unit prices p(w->v) = pi_v - pi_w at a_hi. - 4. paid-rank (volume) identity on three pinned profiles. - 5. PR3682 -> staged544 exact 2x2 decomposition of F at a_hi (four optimal LPs). - 6. negative controls (each must fail). + 1. staged544 ceiling bracket (a_lo, a_hi) from an exact primal/dual pair (reproduces PR3815). + 2. monotone-price lemma: PR3815's basis dual (pi_4..9, mu) with the cheapest extension + pi_1..3 := pi_4 is feasible on ALL 318,840 width-1..9 patterns (enumeration and an + unbounded-knapsack recursion); also the two premises of the PROOF slack lemma + (feasible on widths 4..9 and pi_4 <= -3), which imply the same. + 3. exact width-unit prices p(w->v) = pi_v - pi_w at a_hi with basis ranges; the tight + extension of pi_1..3 and the exact 4->3 price h(5)-h(3)-1 on [0, 324/5] helper-calls. + 4. staging screens: single-child (rank-1 deletion) upper reference and the documented + PR3605 staging signature {1:+3,2:+1,3:-2}. + 5. per-call conservation: local paid rank - hosted width = 1856 on both pinned + (inventory, local) pairs; total paid rank on three pinned T360 profiles. + 6. PR3682 -> staged544 2x2 split of F at a_hi (four optimal LPs; interaction is + identically 0 by separability). + 7. negative controls (each must fail) and one consistency check. """ import json import math @@ -250,6 +255,15 @@ def F_bounds(inv, loc, basis, a): return dict(y_min=min(y), dual_min_rc=rc, patterns=n, lower=lower, upper=upper, pi=pi, mu=mu, tab=tab, y=y) +def monotone(pi): + return all(pi[w - 1] >= pi[w] for w in WIDTHS[1:]) + + +def paid_rank_ok(hist, T): + """Total paid rank of a T-replica profile equals (896*73 - 320) T.""" + return sum(r * n for r, n in hist.items()) == (LIVE * LIVE_RANK - 320) * T + + def dec(x, d=24): s = "-" if x < 0 else "" x = abs(x) @@ -280,7 +294,7 @@ def need(cond, msg): rc_all, worst_all, n_all, tight_all = min_reduced_cost_enum(pi, mu, tab, WIDTHS) rc_kn = min_reduced_cost_knapsack(pi, mu, tab, WIDTHS) rc_w4, _, n_w4, _ = min_reduced_cost_enum(pi, mu, tab, (4, 5, 6, 7, 8, 9)) - mono = all(pi[w - 1] >= pi[w] for w in WIDTHS[1:]) + mono = monotone(pi) lower = local_sum(loc, tab, 0) + sum(mu[c] * BINS[c] for c in CAPS) \ + sum(pi[w] * CALLS * inv[w] for w in inv) - LIVE * tab[LIVE_RANK][1] need(n_all == 318840 and n_w4 == 2551, "pattern counts") @@ -289,18 +303,22 @@ def need(cond, msg): need(lower > 0, "F(a_hi) lower bound not positive") out["ceiling"] = dict(a_lo=dec(a_lo), a_hi=dec(a_hi), F_upper_at_a_lo=dec(lo_side["upper"], 30), F_lower_at_a_hi=dec(lower, 30), primal_min_y=str(min(y))) - out["free_reduction_theorem"] = dict( + need(rc_w4 >= 0 and pi[4] <= -3, "slack-lemma premises") + out["monotone_price_lemma"] = dict( + slack_lemma_premises=dict(dual_feasible_widths_4_to_9=rc_w4 >= 0, + margin_minus_pi4_minus_3=dec(-pi[4] - 3)), patterns_widths_1_to_9=n_all, patterns_widths_4_to_9=n_w4, min_reduced_cost_all=dec(rc_all, 30), min_reduced_cost_knapsack=dec(rc_kn, 30), min_reduced_cost_widths_4_to_9=dec(rc_w4, 30), zero_reduced_cost_patterns=tight_all, argmin_pattern=[worst_all[0], list(worst_all[1])], monotone=mono, - holds=rc_all >= 0 and mono and lower > 0) + holds=rc_all >= 0 and mono and lower > 0, + note="free reductions keep F(a_hi) > 0; under the per-call conservation (section 5) such a move is not realizable") # 3. prices at a_hi (F units per replica; one helper-call = one unit of 9 s_w) out["prices_at_a_hi"] = dict( helper_pi={w: dec(pi[w]) for w in WIDTHS}, bin_mu={c: dec(mu[c]) for c in CAPS}, width_unit_price={f"{w}->{w - 1}": dec(pi[w - 1] - pi[w]) for w in range(5, 10)}, - entrance_raise_1_to_2=dec(tab[2][0] - 1), delete_rank1_child=dec(Q(-1)), + delete_rank1_child=dec(Q(-1)), primal_y={f"{c}:{''.join(str(k) for k in p[3:])}": str(v) for (c, p), v in zip(B, y)}) unit = {w: pi[w - 1] - pi[w] for w in range(5, 10)} need(all(0 <= u <= 1 for u in unit.values()), "width-unit price outside [0,1]") @@ -314,24 +332,40 @@ def need(cond, msg): rc_t = min_reduced_cost_enum(pt, mu, tab, WIDTHS)[0] mono_t = all(pt[w - 1] >= pt[w] for w in WIDTHS[1:]) need(rc_t >= 0 and mono_t and min_reduced_cost_knapsack(pt, mu, tab, WIDTHS) == rc_t, "tight extension") - swap43 = tab[2][0] - tab[1][1] # [9,9,9,4] -> [9,9,9,3]: explicit primal move - need(pt[3] - pt[4] <= tab[2][1] - tab[1][0], "4->3 dual bound above explicit move") ranges = {f"{w}->{w - 1}": ranging(inv, B, {w: -1, w - 1: 1}) for w in range(5, 10)} + # exact 4->3 price: add column [3,9^5] (48-bin); move k units along + # +[3,9^5] -[4,9,9,9] +[9,9,9] -[9^5]; all four columns have reduced cost 0 under (pt, mu) + c3 = (48, (0, 0, 1, 0, 0, 0, 0, 0, 5)) + path = [(c3, 1), ((32, (0, 0, 0, 1, 0, 0, 0, 0, 3)), -1), ((32, (0, 0, 0, 0, 0, 0, 0, 0, 3)), 1), + ((48, (0, 0, 0, 0, 0, 0, 0, 0, 5)), -1)] + rc_path = [tab[left(c, q)][0] - mu[c] - sum(pt[w] * q[w - 1] for w in WIDTHS) for (c, q), _ in path] + need(all(r == 0 for r in rc_path), "4->3 path columns not all tight") + yb = dict(zip(B, y)) + range43 = min(yb[cq] for cq, g in path if g < 0) + cost43 = sum(g * tab[left(c, q)][0] for (c, q), g in path) + need(cost43 == pt[3] - pt[4] and range43 == Q(324, 5), "4->3 exact price or range") + need(abs(cost43 - (tab[5][0] - tab[3][0] - 1)) == 0, "4->3 closed form") + ranges["4->3"] = range43 out["prices_at_a_hi"]["tight_small_width_pi"] = {w: dec(pt[w]) for w in (1, 2, 3)} out["prices_at_a_hi"]["width_unit_price_lower_bound_4_to_v"] = {f"4->{v}": dec(pt[v] - pt[4]) for v in (3, 2, 1)} - out["prices_at_a_hi"]["explicit_4_to_3_move_cost_lower_enclosure"] = dec(swap43) + out["prices_at_a_hi"]["width_unit_price_4_to_3_exact"] = dec(cost43) out["prices_at_a_hi"]["exact_range_helper_calls_per_replica"] = {k: str(v) for k, v in ranges.items()} out["prices_at_a_hi"]["tight_extension_min_reduced_cost"] = dec(rc_t, 30) out["prices_at_a_hi"]["tight_extension_limiting_patterns"] = limiting + unit[4] = cost43 need(all(pt[w] <= 0 for w in WIDTHS), "a helper price is positive (unhosting would then be priced)") - # 3c. volume-neutral staging screen: gain per helper-call = saving - price - out["staging_screen_per_helper_call"] = dict( - single_child_compensation_upper_reference=dict( - {f"{w}->{w - 1}": dec(1 - unit[w]) for w in range(5, 10)}, **{"4->3": dec(1 - (pt[3] - pt[4]))}), - pr3734_local_saving=dec(Q(-1, CALLS) * CALLS * sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9))), - pr3734_net_gain=dec(Q(-1) * sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9)) - unit[8]), - pr3734_reshaping_cost=dec(1 + sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9)))) + # 3c. staging screens, gain in F per width unit (one helper-call moved one width step) + sig = {r: LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0) for r in range(1, 9)} + sig = {r: d for r, d in sig.items() if d} + need(sig == {1: 3, 2: 1, 3: -2}, "PR3682 -> PR3734 local delta is not the PR3605 signature") + sig_saving = -sum(d * tab[r][0] for r, d in sig.items()) + out["staging_screen_per_width_unit"] = dict( + single_child_rank1_deletion_upper_reference={f"{w}->{w - 1}": dec(1 - unit[w]) for w in range(4, 10)}, + documented_signature={str(r): d for r, d in sig.items()}, + documented_signature_saving=dec(sig_saving), + documented_signature_gain={f"{w}->{w - 1}": dec(sig_saving - unit[w]) for w in range(4, 10)}, + gap_signature_vs_rank1_deletion=dec(1 - sig_saving)) # first-order conversion of F to the ceiling (float, envelope theorem on the optimal basis) dFda = -(CALLS * sum(n * float(tab[r][0]) * math.log(r) for r, n in loc.items()) + sum(float(yy) * float(tab[left(c, p)][0]) * math.log(left(c, p)) for yy, (c, p) in zip(y, B) if left(c, p) > 1)) \ @@ -339,7 +373,12 @@ def need(cond, msg): out["first_order_float"] = dict(dF_da_at_ceiling=dFda, ceiling_change_per_unit_F_decrease=1 / dFda) - # 4. paid-rank identity (sum n_r r = (896*73 - 320) T) on pinned profiles + # 5. per-call conservation: local paid rank - hosted width = 1856 on both pinned pairs + cons = {k: sum(r * n for r, n in LOC[k].items()) - sum(w * s for w, s in INV[k].items()) for k in INV} + need(all(v == 1856 for v in cons.values()), "per-call conservation") + need(CALLS * 1856 + sum(c * b for c, b in BINS.items()) == LIVE * LIVE_RANK - 320, "deficit 320") + out["per_call_local_rank_minus_hosted_width"] = cons + # total paid rank (= (896*73 - 320) T) on three pinned profiles; two share one (inventory, local) pair vol = {} for k, prof in CERT["profiles"].items(): T = prof["T"] @@ -347,10 +386,9 @@ def need(cond, msg): if prof.get("add_local"): for r, n in LOC[prof["add_local"]].items(): hist[r] = hist.get(r, 0) + CALLS * T * n - vol[k] = dict(T=T, paid_rank_sum=sum(r * n for r, n in hist.items()), - identity=sum(r * n for r, n in hist.items()) == (LIVE * LIVE_RANK - 320) * T) + vol[k] = dict(T=T, paid_rank_sum=sum(r * n for r, n in hist.items()), identity=paid_rank_ok(hist, T)) need(vol[k]["identity"], f"volume identity fails for {k}") - out["paid_rank_identity"] = vol + out["paid_rank_total"] = vol # 5. 2x2 decomposition at a_hi (each corner: own optimal basis, exact) corners = {"pr3682": ("pr3682", "pr3682"), "width_only": ("staged544", "pr3682"), @@ -371,7 +409,7 @@ def need(cond, msg): local_part_exact=dec(CALLS * sum((LOC["staged544"].get(r, 0) - LOC["pr3682"].get(r, 0)) * tab[r][0] for r in range(1, 9)), 30)) need(total < 0 and d_w > 0 and d_l < 0, "decomposition signs") - # 6. negative controls (each must FAIL the corresponding check) + # 7. negative controls (each must FAIL the corresponding check) ctl = {} pi_bad = dict(pi) pi_bad[9] += Q(1, 10 ** 30) @@ -382,25 +420,26 @@ def need(cond, msg): pg = dict(pt) for w in (1, 2, 3): pg[w] = pt[3] + Q(1, 10 ** 30) # monotone, feasible on widths 4..9, too high for 1..9 - ctl["granularity_raised_pi3_infeasible_on_1_to_9"] = min_reduced_cost_enum(pg, mu, tab, WIDTHS)[0] < 0 \ - and min_reduced_cost_enum(pg, mu, tab, (4, 5, 6, 7, 8, 9))[0] >= 0 and all(pg[w - 1] >= pg[w] for w in WIDTHS[1:]) - ctl["non_monotone_extension_rejected"] = not all(pi_nm[w - 1] >= pi_nm[w] for w in WIDTHS[1:]) + ctl["tight_extension_raised_1e-30_infeasible"] = min_reduced_cost_enum(pg, mu, tab, WIDTHS)[0] < 0 + ctl["non_monotone_extension_rejected_by_monotone_check"] = not monotone(pi_nm) lo_tab = h_table(a_lo) pl, ml = dual(B, lo_tab) lb_lo = local_sum(loc, lo_tab, 0) + sum(ml[c] * BINS[c] for c in CAPS) \ + sum(pl[w] * CALLS * inv[w] for w in inv) - LIVE * lo_tab[LIVE_RANK][1] - ctl["bound_at_a_lo_not_positive"] = lb_lo <= 0 + consistency = {"bound_at_a_lo_not_positive": lb_lo <= 0} # implied by F_upper(a_lo) < 0 and weak duality widened = dict(inv) widened[8] -= 1 widened[9] += 1 lb_wide = local_sum(loc, tab, 0) + sum(mu[c] * BINS[c] for c in CAPS) \ + sum(pi[w] * CALLS * widened.get(w, 0) for w in WIDTHS) - LIVE * tab[LIVE_RANK][1] ctl["one_8_to_9_widening_per_call_breaks_bound"] = lb_wide <= 0 - vol_bad = sum(int(r) * n for r, n in CERT["profiles"]["pr3734_finite"]["histogram"].items()) + 1 - ctl["volume_identity_detects_plus_one"] = vol_bad != (LIVE * LIVE_RANK - 320) * 360 - for k, v in ctl.items(): + hist_bad = {int(r): n for r, n in CERT["profiles"]["pr3734_finite"]["histogram"].items()} + hist_bad[1] = hist_bad.get(1, 0) + 1 + ctl["paid_rank_check_detects_plus_one"] = not paid_rank_ok(hist_bad, 360) + for k, v in list(ctl.items()) + list(consistency.items()): need(v, f"control {k} did not fail as required") out["controls_failed_as_required"] = ctl + out["consistency_checks"] = consistency out["status"] = "PASS" if not fails else "FAIL" out["failures"] = fails From b12d58d7b391b0d8490d6ebebe5cd0d4f57653b6 Mon Sep 17 00:00:00 2001 From: Sagar Thakrar <18622288+thakrarsagar@users.noreply.github.com> Date: Mon, 19 Oct 2026 05:02:53 +0530 Subject: [PATCH 3/3] Staged544 width prices: round-2 review text fixes, 4->3 direction assert State that the documented staging signature was observed only on 8->7 units and is assumed for other widths; credit PR3815 for evaluating the dual at a_hi (new: reading it as width-unit prices); fix the tight pi_3 control to raise only pi_3; lemma keeps the ceiling below a_hi; N_r for the full paid histogram; add the global k x 0.003264 weak-duality bound; reword OQ1, the PR3836 citation and the AI-review provenance line. verify.py asserts the 4->3 path's net direction; output unchanged. Co-Authored-By: Claude Opus 5.5 --- .../staged544-width-lever-screen/PROOF.md | 8 ++- .../staged544-width-lever-screen/README.md | 65 +++++++++++-------- .../staged544-width-lever-screen/TASK.json | 12 ++-- .../staged544-width-lever-screen/verify.py | 8 ++- 4 files changed, 55 insertions(+), 38 deletions(-) diff --git a/research/staged544-width-lever-screen/PROOF.md b/research/staged544-width-lever-screen/PROOF.md index 6640b18626..8cb38dbe7d 100644 --- a/research/staged544-width-lever-screen/PROOF.md +++ b/research/staged544-width-lever-screen/PROOF.md @@ -15,7 +15,8 @@ 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)` and every paid rank +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`. @@ -62,7 +63,7 @@ by `z (pi_v - pi_w)`; changing the local profile changes it by - 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 exact fills: + 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. @@ -83,7 +84,7 @@ 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 never raises the ideal ceiling. Under the +`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. @@ -129,6 +130,7 @@ 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 diff --git a/research/staged544-width-lever-screen/README.md b/research/staged544-width-lever-screen/README.md index a3058274e5..d710dd7814 100644 --- a/research/staged544-width-lever-screen/README.md +++ b/research/staged544-width-lever-screen/README.md @@ -32,16 +32,17 @@ bracket `[0.001730578437266246818740, ...741]` (this bracket reproduces PR3815). on all 318,840 width-1..9 patterns; `verify.py` checks the four-column move and its range exactly. Outside a range the price is a lower bound for every further unit (convexity of the LP value). -2. **Staging screens (exact arithmetic, per width unit).** A literal staging - move must also change the local profile (item 4). Its net change in `F` is - (local saving) minus (price): +2. **Staging screens (exact arithmetic, per width unit).** Under the observed + conservation (item 4), a literal staging move must also change the local + profile. Its net change in `F` is (local saving) minus (price): - **Documented signature.** All three observed staging units (644 and 660 in PR3605, 544 in PR3734) change the local profile by `{1:+3,2:+1,3:-2}` per unit (PR3605 PROOF: `3H1 + H2 - 2H3`), saving 0.991001081580029037511288. Gain: **+0.003264300394675969421322** for 6..9, **-0.008998918419970962488711** for 5->4 and - **-0.000790287459955874210276** for 4->3. So with this signature only - width-6..9 staging pays, and 5->4 and 4->3 staging lose. + **-0.000790287459955874210276** for 4->3. All three observed units are 8->7 moves; for the other widths the screen assumes the same signature. + So with this signature only width-6..9 staging pays, and 5->4 and 4->3 + staging lose; a candidate's own local saving should be priced with (*). - **Hypothetical rank-1 deletion** (single-child compensation, saving `h(1) = 1`, the most any single-child decrement `r -> r-1` saves). Gain at most **0.012263218814646931910033** for 6..9, **0** for 5->4 (in any @@ -72,12 +73,12 @@ bracket `[0.001730578437266246818740, ...741]` (this bracket reproduces PR3815). with an unchanged local profile is not realizable, which is why item 2 prices staging with a local change. 5. **Monotone-price lemma (free reductions).** With `pi_1 = pi_2 = pi_3 = - pi_4`, the prices are nonincreasing and nonpositive and still dual feasible + pi_4`, the helper duals `pi_w` are nonincreasing in `w`, nonpositive and still dual feasible on all width-1..9 patterns. This follows from PR3815's 2,551-pattern dual and `pi_4 <= -3` by a two-line slack lemma (PROOF section 3); `verify.py` also checks it on all 318,840 patterns. Hence a width reduction (to any - width `>= 1`, or unhosting) with an unchanged local profile never raises - the ideal ceiling. Under item 4 such a move is not realizable, so this is a + width `>= 1`, or unhosting) with an unchanged local profile keeps the + ideal ceiling below `a_hi = 0.001730578437266246818741`. Under item 4 such a move is not realizable, so this is a consistency statement about the model, not a staging closure. 6. **PR3682 -> staged544 split at `a_hi`.** `F` is additively separable in inventory and local profile at fixed `a`, so the 2x2 interaction is @@ -103,14 +104,19 @@ engine of #3605 and #3734, and partly answers PR3815's open question 1. The family is tracked in #3606; it is not a revision-6 lead. - With the documented staging signature, only width-6..9 staging pays - (+0.003264 per width unit); 5->4 and 4->3 staging lose. + (+0.003264 per width unit); 5->4 and 4->3 staging lose. The signature was + observed only on 8->7 units; for other widths it is an assumption. +- By weak duality (*), `k` width-6..9 units with the documented signature, in + any number and mix and also outside the ranges, leave + `F(a_hi) >= 5.28e-20 - k x 0.003264300394675969421322`. To first order this + is at most about 1.6e-7 of ideal ceiling per fully staged helper (nine + units), before clock and admission costs. - A candidate staging is decided by one exact inequality: its local saving per width unit must exceed the price in item 1 (within the ranges). - Even a hypothetical rank-1-deletion compensation cannot make 5->4 staging pay. -- The largest identified slack is the 0.008999 per unit between the documented - signature and a rank-1 deletion. Whether a literal staging can avoid it is - open. +- The gap between the documented signature and a hypothetical rank-1 deletion + is 0.008999 per unit; whether a literal staging can narrow it is open. - Free width reduction is not a lever (item 5). ## Reproduce @@ -128,8 +134,8 @@ and 3.14.4. **Negative controls (each must fail; the verifier asserts they do):** - `pi_9 + 1e-30` makes the dual infeasible. -- Raising the tight `pi_1..pi_3` by 1e-30 makes some width-1..9 pattern - infeasible (the tight extension, and so the exact 4->3 price, is tight). +- Raising the tight `pi_3` by 1e-30 makes the pattern `[3,9^5]` infeasible + (the tight extension, and so the exact 4->3 price, is tight). - A non-monotone extension is rejected by the same `monotone` check the lemma uses. - One 8->9 widening per call drops the bound to `<= 0` (widening is priced as a @@ -138,7 +144,8 @@ and 3.14.4. profiles pass. One consistency check (not a mutation): the dual bound at `a_lo` is not -positive, as implied by `F_upper(a_lo) < 0` and weak duality. +positive, as implied by `F_upper(a_lo) < 0` and weak duality. The `pi_9` +control and this check reproduce PR3815's two controls. **Second, independent method (floating point):** `crosscheck_highs.py` used Python 3.14.4, numpy 2.5.4 and scipy 1.18.1 HiGHS. It generates patterns as @@ -171,8 +178,9 @@ wall, PR3630 and PR3638 priced other inventories with fixed widths. New here: -- evaluation of that dual exactly at `a_hi`, the common 6..9 price (affine dual - on widths 5..9), `5->4 = 1` and the exact `4->3 = h(5)-h(3)-1`; +- reading PR3815's `a_hi` dual (which PR3815 already solves exactly at + `a_hi`) as width-unit prices: the common 6..9 price (affine dual on widths + 5..9), `5->4 = 1` and the exact `4->3 = h(5)-h(3)-1`; - the basis ranges (18 to 30, and 324/5 for 4->3); - the extension of the dual to widths 1..9 (cheapest and tight), with the slack lemma; @@ -209,7 +217,8 @@ them. This is a stated gap. and stated by PR3605 for its staging; not derived. The non-realizability of free reductions depends on it. - **Staging signature.** The documented signature is what the three observed - staging units use; it is not proved to be forced. The rank-1-deletion + staging units use; all three are 8->7 moves, so for other widths it is an + assumption. It is not proved to be forced. The rank-1-deletion reference has no known realization. - **Admission costs not priced.** All admission costs of a changed inventory are unknown and are not zero. These include physical stock, coverage law and @@ -224,10 +233,11 @@ them. This is a stated gap. - **Is the staging signature `{1:+3,2:+1,3:-2}` forced?** A literal width-6..9 staging with a smaller gap to a rank-1 deletion would gain up to 0.008999 per - width unit more. First step: in PR3734's frames, check whether PR3682's - delayed donor release (`{1:-2,2:-2,3:+2}`, worth about 0.0066 per call) can be - re-applied on top of the staged544 local profile; then price the result - with (*). + width unit more. The PR3682 -> staged544 local delta equals the signature, + which suggests PR3682's delayed donor release (`{1:-2,2:-2,3:+2}`, worth + about 0.0066 per call) survives in PR3734. First step: check in PR3734's + frames whether that release survives, or whether an analogous release applies + to helper 544's donors; then price the result with (*). - **Does the per-call conservation (local paid rank minus hosted width = 1856) hold for every literal construction of this template?** First step: derive it from the owner and frame accounting in PR3734's `owner_audit.py`, or find a @@ -235,8 +245,9 @@ them. This is a stated gap. - **What do bin-count changes offer?** `mu` gives subgradient bin prices. First step: write a candidate template's bin counts and evaluate (*), re-solving the LP outside the (unknown) bin ranges. New bin ranks are constrained by - concurrent PR3836 (Matarener), which shows the idle alphabet is forced within - bridge-based nine-stage schedules; changing bin counts stays open. + concurrent PR3836 (Matarener, unmerged), which reports, by a census within + its class, that the idle alphabet is forced within bridge-based nine-stage + schedules; changing bin counts stays open. ## Credit @@ -255,6 +266,8 @@ enclosures, enumeration, knapsack check and LP algebra are new. Prepared by Sagar Thakrar (thakrarsagar) with substantial AI assistance from Claude (Anthropic, Claude Opus 5.5). Reviewed by four AI review passes in the -same loop (reproducibility, mathematical audit, provenance, referee), followed -by one revision; no human or formal-kernel verification is claimed. +same loop (reproducibility, mathematical audit, provenance, referee), then one +revision, a re-verification round by two of them (mathematical audit, referee) +and a second, text-level revision; no human or formal-kernel verification is +claimed. Apache-2.0. diff --git a/research/staged544-width-lever-screen/TASK.json b/research/staged544-width-lever-screen/TASK.json index 92625be6c5..3ff750801b 100644 --- a/research/staged544-width-lever-screen/TASK.json +++ b/research/staged544-width-lever-screen/TASK.json @@ -46,20 +46,20 @@ ] }, "scope_status": "refined", - "actual_scope": "Narrowed to one helper-inventory lever of the staged544 T360 template (PR3734/PR3815): exact prices of hosted-width changes in the clock-free fixed-bin ideal. Deliverables: exact width-unit prices at a_hi = 0.001730578437266246818741 with basis ranges (0.987736781185353068089966 for 6..9, 1 for 5->4, h(5)-h(3)-1 = 0.991791369039984911721564 for 4->3 on 324/5 helper-calls); two staging screens per width (documented PR3605 signature {1:+3,2:+1,3:-2}: +0.003264300394675969421322 for 6..9, -0.008998918419970962488711 for 5->4, -0.000790287459955874210276 for 4->3; hypothetical rank-1 deletion: at most 0.012263218814646931910033, 0 and 0.008208630960015088278435); the weak-duality screen (*) over widths 1..9; the monotone-price lemma for free reductions; the per-call conservation 1856 on both pinned pairs; and the PR3682 -> staged544 split. No new contract and no kappa.", - "scope_change_reason": "The card asks for a changed helper inventory. Staging (hosted-width reduction) is the engine of the pending gains in #3605 and #3734, and PR3815's open question 1 asks which changed T360 inventory raises the ceiling, so this package prices that lever exactly instead of proposing a contract. The task card's premise that a free width reduction is an upper relaxation of real staging was corrected: on both pinned (inventory, local) pairs, local paid rank minus hosted width is 1856 per call (PR3605 states the same conservation), so a literal staging unit also changes the local profile. The package therefore prices staging with its local change.", + "actual_scope": "Narrowed to one helper-inventory lever of the staged544 T360 template (PR3734/PR3815): exact prices of hosted-width changes in the clock-free fixed-bin ideal. Deliverables: exact width-unit prices at a_hi = 0.001730578437266246818741 with basis ranges (0.987736781185353068089966 for 6..9, 1 for 5->4, h(5)-h(3)-1 = 0.991791369039984911721564 for 4->3 on 324/5 helper-calls); two staging screens per width (documented PR3605 signature {1:+3,2:+1,3:-2}, observed only on 8->7 units and assumed for the other widths: +0.003264300394675969421322 for 6..9, -0.008998918419970962488711 for 5->4, -0.000790287459955874210276 for 4->3; hypothetical rank-1 deletion: at most 0.012263218814646931910033, 0 and 0.008208630960015088278435); the weak-duality screen (*) over widths 1..9; the monotone-price lemma for free reductions; the per-call conservation 1856 on both pinned pairs; and the PR3682 -> staged544 split. No new contract and no kappa.", + "scope_change_reason": "The card asks for a changed helper inventory. Staging (hosted-width reduction) is the engine of the pending gains in #3605 and #3734, and PR3815's open question 1 asks which changed T360 inventory raises the ceiling, so this package prices that lever exactly instead of proposing a contract. The task card's premise that a free width reduction is an upper relaxation of real staging was corrected: on both pinned (inventory, local) pairs, local paid rank minus hosted width is 1856 per call (PR3605 states the same conservation), so under that observed conservation a literal staging unit also changes the local profile. The package therefore prices staging with its local change.", "bottleneck_link": "The complex primitive binds the selected conditional kappa. The staged-entrance family's gains (#3605, #3734) are ideal-packing gains of the complex local word. This package gives the exact price at which staging a helper pays in that ideal: (*) in README/PROOF. Expansion-gate point 4 (stage more helpers versus redirect to bins or the local word) can therefore be decided per candidate by one inequality.", "budget_minutes": 90, "stop_rule": "Stop if the exact certificate fails and report the improving width move instead; ship without the decomposition if the PR3682 inventory is not pinned within 15 minutes; stop at the iteration deadline; stop and post nothing if a competing staged544 width or inventory pricing appears before submission.", "outcome": "completed", - "evidence": "verify.py (stdlib, about 6 s) prints PASS_STAGED544_WIDTH_LEVER_SCREEN. Ceiling bracket [0.001730578437266246818740, ...741]: F(a_lo) <= -1.31e-19 and F(a_hi) >= 5.28e-20 (reproduces PR3815). Cheapest and tight dual extensions feasible on 318,840 patterns with minimum reduced cost exactly 0, matched by a knapsack recursion; slack-lemma premises hold (margin 0.986093083432664503980103). Width-unit prices: 0.987736781185353068089966 (6..9, ranges 28/30/28/28), 1 (5->4, range 18), 0.991791369039984911721564 (4->3, range 324/5). Documented-signature gains +0.003264300394675969421322 / -0.008998918419970962488711 / -0.000790287459955874210276; rank-1-deletion references 0.012263218814646931910033 / 0 / 0.008208630960015088278435. Split: width +8.889631030668177612809695088162, local -8.919009734220261337601597266358 (interaction identically 0 by separability). Per-call conservation 1856 on both pairs. Five negative controls fail as required. Second method: HiGHS (evidence/HIGHS.json) agrees to about 3e-12 in prices and 1e-16 in roots.", + "evidence": "verify.py (stdlib, about 6 s) prints PASS_STAGED544_WIDTH_LEVER_SCREEN. Ceiling bracket [0.001730578437266246818740, ...741]: F(a_lo) <= -1.31e-19 and F(a_hi) >= 5.28e-20 (reproduces PR3815). Cheapest and tight dual extensions feasible on 318,840 patterns with minimum reduced cost exactly 0, matched by a knapsack recursion; slack-lemma premises hold (margin 0.986093083432664503980103). Width-unit prices: 0.987736781185353068089966 (9->8/8->7/7->6/6->5, ranges 28/30/28/28), 1 (5->4, range 18), 0.991791369039984911721564 (4->3, range 324/5). Documented-signature gains +0.003264300394675969421322 / -0.008998918419970962488711 / -0.000790287459955874210276; rank-1-deletion references 0.012263218814646931910033 / 0 / 0.008208630960015088278435. Split: width +8.889631030668177612809695088162, local -8.919009734220261337601597266358 (interaction identically 0 by separability). Per-call conservation 1856 on both pairs. Five negative controls fail as required. Second method: HiGHS (evidence/HIGHS.json) agrees to about 3e-12 in prices and 1e-16 in roots.", "author": "Sagar Thakrar (thakrarsagar)", - "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for design, code, proofs and text. Reviewed by four AI review passes in the same loop (reproducibility, mathematical audit, provenance, referee), followed by one revision. No human or formal-kernel verification is claimed.", + "ai_assistance": "Substantial AI assistance from Claude (Anthropic, Claude Opus 5.5) for design, code, proofs and text. Reviewed by four AI review passes in the same loop (reproducibility, mathematical audit, provenance, referee), then one revision, a re-verification round by two of them (mathematical audit, referee) and a second, text-level revision. No human or formal-kernel verification is claimed.", "open_questions": [ { "question": "Is the staging signature {1:+3,2:+1,3:-2} forced for width-6..9 staging of this template?", "why_it_matters": "A literal staging with a smaller gap to a rank-1 deletion would gain up to 0.008999 more per width unit; with the signature the gain is 0.003264.", - "first_step": "In PR3734's frames, check whether PR3682's delayed donor release {1:-2,2:-2,3:+2} can be re-applied on top of the staged544 local profile, then price it with (*).", + "first_step": "The PR3682 -> staged544 local delta equals the signature, which suggests PR3682's delayed donor release {1:-2,2:-2,3:+2} survives in PR3734. Check in PR3734's frames whether it survives, or whether an analogous release applies to helper 544's donors; then price the result with (*).", "blocked_by": "Reading PR3734's literal frames and staging identities; not done in this time box." }, { @@ -70,7 +70,7 @@ }, { "question": "Which bin-count changes pass screen (*)?", - "why_it_matters": "mu gives subgradient bin prices; PR3815's open question 1 asks for a changed T360 inventory. New bin ranks are constrained by concurrent PR3836 (Matarener) within bridge-based nine-stage schedules.", + "why_it_matters": "mu gives subgradient bin prices; PR3815's open question 1 asks for a changed T360 inventory. New bin ranks are constrained by concurrent PR3836 (Matarener, unmerged), which reports by a census within its class that the alphabet is forced within bridge-based nine-stage schedules.", "first_step": "Write a candidate template's bin counts, evaluate (*), and re-solve the LP outside the unknown bin ranges.", "blocked_by": "Physical stock, coverage law and template checks of the complete admission." } diff --git a/research/staged544-width-lever-screen/verify.py b/research/staged544-width-lever-screen/verify.py index 73dece2075..537e7d05ca 100644 --- a/research/staged544-width-lever-screen/verify.py +++ b/research/staged544-width-lever-screen/verify.py @@ -5,7 +5,7 @@ Model (PR3815 ceiling_certificate.py, PR3734 inventory): per owner replica, 9 calls of 408 helpers; idle bins {8:672,16:448,32:448,48:448}; each helper occupies its hosted width in one bin and each bin remainder l>0 is paid as one rank-l child; local paid -profile per call; 896 live rank-73 families. F(a) = sum n_r r^(1-a) - 896*73^(1-a) per +profile per call; 896 live rank-73 families. F(a) = sum N_r r^(1-a) - 896*73^(1-a) over the full paid histogram N per replica has the sign of a strictly increasing function, so "ceiling < a" iff F(a) > 0. Checks (all exact rational arithmetic; h(l) = l^(1-a) enclosed by series with @@ -340,6 +340,9 @@ def need(cond, msg): ((48, (0, 0, 0, 0, 0, 0, 0, 0, 5)), -1)] rc_path = [tab[left(c, q)][0] - mu[c] - sum(pt[w] * q[w - 1] for w in WIDTHS) for (c, q), _ in path] need(all(r == 0 for r in rc_path), "4->3 path columns not all tight") + net = [sum(g * q[i] for (c, q), g in path) for i in range(9)] + net_bins = {cap: sum(g for (c, q), g in path if c == cap) for cap in CAPS} + need(net == [0, 0, 1, -1, 0, 0, 0, 0, 0] and not any(net_bins.values()), "4->3 path direction") yb = dict(zip(B, y)) range43 = min(yb[cq] for cq, g in path if g < 0) cost43 = sum(g * tab[left(c, q)][0] for (c, q), g in path) @@ -418,8 +421,7 @@ def need(cond, msg): for w in (1, 2, 3): pi_nm[w] = pi[4] - Q(1, 10 ** 30) pg = dict(pt) - for w in (1, 2, 3): - pg[w] = pt[3] + Q(1, 10 ** 30) # monotone, feasible on widths 4..9, too high for 1..9 + pg[3] += Q(1, 10 ** 30) ctl["tight_extension_raised_1e-30_infeasible"] = min_reduced_cost_enum(pg, mu, tab, WIDTHS)[0] < 0 ctl["non_monotone_extension_rejected_by_monotone_check"] = not monotone(pi_nm) lo_tab = h_table(a_lo)