diff --git a/research/owner-profile-uniform/CERTIFICATE.json b/research/owner-profile-uniform/CERTIFICATE.json new file mode 100644 index 0000000000..2eade4b7f1 --- /dev/null +++ b/research/owner-profile-uniform/CERTIFICATE.json @@ -0,0 +1,338 @@ +{ + "status": "PASS_UNIFORM_OWNER_OPTIMALITY", + "interval": "0 < b <= 1/3", + "selected": { + "helper_roles": 36288, + "widths": { + "4": 80, + "5": 32, + "7": 54, + "8": 122, + "9": 216 + }, + "capacities": { + "8": 48, + "16": 32, + "32": 32, + "48": 32 + }, + "idle": { + "44": 1, + "48": 2396, + "1": 1, + "3": 1 + }, + "local": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + } + }, + "dual": { + "upper": { + "8": 2, + "4": 1, + "3": 7, + "1": 19, + "0": 0, + "16": 4, + "12": 3, + "11": 9, + "9": -4, + "7": 8, + "6": 14, + "5": 20, + "2": 13, + "32": 8, + "28": 7, + "27": -12, + "25": 0, + "24": 6, + "23": 12, + "22": -7, + "21": -1, + "20": 5, + "19": 11, + "18": -8, + "17": -2, + "15": 10, + "14": 16, + "13": -3, + "10": 15, + "48": -13, + "44": -14, + "43": -33, + "41": -21, + "40": -15, + "39": -9, + "38": -53, + "37": -22, + "36": -16, + "35": -10, + "34": -29, + "33": -23, + "31": -11, + "30": -5, + "29": -24, + "26": -6 + }, + "base": -31136, + "excluded_two_parts": [ + { + "parts": [ + 33, + 15 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 34, + 14 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 35, + 13 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 36, + 12 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 37, + 11 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 38, + 10 + ], + "bound": -31186, + "gap": 50 + }, + { + "parts": [ + 39, + 9 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 40, + 8 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 41, + 7 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 42, + 6 + ], + "reason": "unreachable residual" + }, + { + "parts": [ + 43, + 5 + ], + "bound": -31161, + "gap": 25 + }, + { + "parts": [ + 44, + 4 + ], + "bound": -31161, + "gap": 25 + } + ] + }, + "algebraic": [ + { + "name": "two-parts", + "coefficients": { + "32": 1, + "16": 1, + "44": -1, + "3": -1, + "1": -1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "1070539374112333550159645/1208925819614629174706176" + }, + { + "name": "t2", + "coefficients": { + "48": -1, + "44": 1, + "3": -1, + "1": -1, + "8": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "13265433467971782236195/75557863725914323419136" + }, + { + "name": "t3", + "coefficients": { + "48": -2, + "44": 2, + "3": -1, + "1": -1, + "12": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "813244050306799889496749/1208925819614629174706176" + }, + { + "name": "t4", + "coefficients": { + "48": -3, + "44": 3, + "3": -1, + "1": -1, + "16": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "313254290711945792862295/302231454903657293676544" + }, + { + "name": "t5", + "coefficients": { + "48": -4, + "44": 4, + "3": -1, + "1": -1, + "20": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "1584394806870358192825329/1208925819614629174706176" + }, + { + "name": "t6", + "coefficients": { + "48": -5, + "44": 5, + "3": -1, + "1": -1, + "24": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "458939472201227875198753/302231454903657293676544" + }, + { + "name": "t7", + "coefficients": { + "48": -6, + "44": 6, + "3": -1, + "1": -1, + "28": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "1012288594906843917588143/604462909807314587353088" + }, + { + "name": "t8", + "coefficients": { + "48": -7, + "44": 7, + "3": -1, + "1": -1, + "32": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "2162571463942993672489815/1208925819614629174706176" + }, + { + "name": "t9", + "coefficients": { + "48": -8, + "44": 8, + "3": -1, + "1": -1, + "36": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "2258083290255031792895737/1208925819614629174706176" + }, + { + "name": "t10", + "coefficients": { + "48": -9, + "44": 9, + "3": -1, + "1": -1, + "40": 1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "2317317958326368722813759/1208925819614629174706176" + }, + { + "name": "t11", + "coefficients": { + "48": -10, + "44": 11, + "3": -1, + "1": -1 + }, + "sign_changes": 2, + "value_at_one": -1, + "lower_at_third": "2345049252678443293779349/1208925819614629174706176" + }, + { + "name": "t12", + "coefficients": { + "48": -11, + "44": 12, + "3": -1, + "1": -1, + "4": 1 + }, + "sign_changes": 2, + "value_at_one": 0, + "lower_at_third": "4491487945760026029508013/1208925819614629174706176" + } + ] +} diff --git a/research/owner-profile-uniform/INDEPENDENT.json b/research/owner-profile-uniform/INDEPENDENT.json new file mode 100644 index 0000000000..3f8dc90c47 --- /dev/null +++ b/research/owner-profile-uniform/INDEPENDENT.json @@ -0,0 +1,200 @@ +{ + "status": "PASS_INDEPENDENT_UNIFORM_OWNER", + "packing": { + "width_patterns": 1163, + "partitions_checked": 147266, + "dual_eligible_partitions": 147113, + "upper": { + "8": 2, + "0": 0, + "1": 19, + "3": 7, + "4": 1, + "16": 4, + "7": 8, + "9": -4, + "2": 13, + "11": 9, + "6": 14, + "12": 3, + "5": 20, + "32": 8, + "23": 12, + "14": 16, + "24": 6, + "15": 10, + "25": 0, + "17": -2, + "18": -8, + "10": 15, + "27": -12, + "19": 11, + "20": 5, + "13": -3, + "22": -7, + "28": 7, + "21": -1, + "48": -13, + "39": -9, + "30": -5, + "40": -15, + "31": -11, + "41": -21, + "33": -23, + "34": -29, + "26": -6, + "43": -33, + "35": -10, + "36": -16, + "29": -24, + "38": -53, + "44": -14, + "37": -22 + } + }, + "intervals": [ + { + "coefficients": { + "16": 1, + "32": 1, + "44": -1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "332097928005694047371148329337593444838382142112457751574631/34397602499799123100456413704189153118553003351209607692288", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 1, + "48": -1, + "8": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "263369173354951360932851071829711316196340211097761865222415/137590409999196492401825654816756612474212013404838430769152", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 2, + "48": -2, + "12": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "252280925485611373470035307941768450796419996641421903829577/34397602499799123100456413704189153118553003351209607692288", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 3, + "48": -3, + "16": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "1554821480087503836296948479912825367045671323783311031065533/137590409999196492401825654816756612474212013404838430769152", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 4, + "48": -4, + "20": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "983007715976666854020908851938423524047786122920327084101219/68795204999598246200912827408378306237106006702419215384576", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 5, + "48": -5, + "24": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "35592536688440768990097975432352884118141149476157979328641/2149850156237445193778525856511822069909562709450600480768", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 6, + "48": -6, + "28": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "104675877425841227857269090786382548010305635871673647016325/5732933749966520516742735617364858853092167225201601282048", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 7, + "48": -7, + "32": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "894484306642417488282862855520404414537353084714442773770015/45863469999732164133941884938918870824737337801612810256384", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 8, + "48": -8, + "36": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "155664995731661996558704539820250604402042126528167999196419/7643911666622027355656980823153145137456222966935468376064", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 9, + "48": -9, + "40": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "239622664705408373880125495209225737039807958855787938573945/11465867499933041033485471234729717706184334450403202564096", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 11, + "48": -10, + "3": -1, + "1": -1 + }, + "lower_bernstein": "323320298665775567962327081013740536811578001052506830270815/15287823333244054711313961646306290274912445933870936752128", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + }, + { + "coefficients": { + "44": 12, + "48": -11, + "4": 1, + "3": -1, + "1": -1 + }, + "lower_bernstein": "5573317064349052711273237109260470912891664807935254353454417/137590409999196492401825654816756612474212013404838430769152", + "tail": "21812692093918386438343299/182687704666362864775460604089535377456991567872", + "degree": 23 + } + ] +} diff --git a/research/owner-profile-uniform/README.md b/research/owner-profile-uniform/README.md new file mode 100644 index 0000000000..72b3dfa1bd --- /dev/null +++ b/research/owner-profile-uniform/README.md @@ -0,0 +1,196 @@ +# Uniform owner-profile optimum for the SW4/X4 inventory + +**Research consolidation; no new κ.** For every real `0 < b <= 1/3`, the idle +profile + +`I* = {48:2396, 44:1, 3:1, 1:1}` + +uniquely minimizes `sum_r I(r) r^(1-b)` among all whole-helper packings with +the inventory below. Different assignments with this same profile tie. +The theorem permits any fixed local paid profile: it adds the same cost to +every packing. Thus it applies to PR799 and to later local circuit changes +that preserve these packing data and admit this owner assignment. + +This extends **[chafreaky's PR795](https://github.com/CrocSwap/integer-mult-bounds/pull/795)**. That work supplies the integer prices, +packing exclusions, and eleven-step concavity reduction, and proves optimality +at PR741's single admitted endpoint. Here additional integer exclusions remove +its `[43,5]` relaxation. A uniform argument then covers an entire interval, +independently of the local paid profile. It does not improve a construction. + +For the current recurrence, the complete moment is +`M_b = sum_r (72 L(r)+I(r)) r (73/r)^b / (73*7168)`. +Fixing L makes its contribution constant across owner assignments; the +remaining factor `73^b/(73*7168)` is positive. Thus the idle optimum also +minimizes this complete moment. The theorem concerns this billed objective. + +The practical decision is specific: changing only this owner assignment cannot +improve a moment in this interval. A search must change widths, capacities, +dispatch counts, splitting rules, or another part of the hosting contract. +Local circuit changes remain useful and are explicitly allowed by this theorem. + +## Precise model and proof + +There are 72 calls. Each call supplies 80 helpers of width 4, 32 of width 5, +54 of width 7, 122 of width 8, and 216 of width 9. There are 112 bins per window, +with 48 windows of capacity 8 and 32 each of capacities 16, 32, and 48. +Every helper occupies its complete width in one bin. Bin occupancies do not +overlap. Unused capacity contributes one residual rank per bin; zero ranks +contribute nothing. The theorem covers all such integer packings, including +ones that ignore native timing and helper identities. Exclusions in this +larger class therefore apply to the native whole-call model. + +The total capacity is 387072, total helper width is 272016, and residual mass +is `S=115056=2397*48`. A positive residual is at most 48. A residual other than +48 is at most 44, because the smallest helper width is four. + +### Integer exclusions inherited and extended from PR795 + +Use helper prices + +| width | 4 | 5 | 7 | 8 | 9 | +|---|---:|---:|---:|---:|---:| +| price | -1 | -20 | -8 | -2 | 4 | + +and capacity bonuses `d(8)=2, d(16)=4, d(32)=8, d(48)=-13`. +Let `u(r)` be the maximum bonus plus helper prices over all possible fills +with residual `r`. Impossible residuals have no value. The finite integer +knapsack in `verify.py` computes every possible fill of capacities at most 48. + +Summing over all bins gives the necessary inequality + +`-31136 <= sum_r I(r) u(r)`. + +The left side counts every capacity bonus and every helper price exactly once. +The calculation gives `u(0)=0`, so zero residuals can be omitted. It also gives +`u(48)=-13, u(44)=-14, u(3)=7, u(1)=19`. The profile I* attains equality. +The all-48 profile violates this inequality by 25, as in PR795. + +The new exclusion checks all twelve two-part candidates `[r,48-r]`, +`33 <= r <= 44`, after 2396 residuals of rank 48. Each candidate either contains +an impossible residual or violates the same integer inequality. The exact +certificate lists every case and its contradiction. Thus any feasible +two-part remainder of mass 48 has largest part at most 32. + +### Reduction to twelve analytic inequalities + +Write the number of rank-48 residuals as `2397-t`. Then `0 <= t <= 2397`, +and the other residuals have total mass `48t` with each part at most 44. +Fix `0=2`, use `floor(48t/44)` copies of 44 and the remainder `48t mod 44`. + Increasing `t` by eleven adds cost `12 f(44)-11 f(48)>0`. + This follows from `12*44=11*48` and `44^-b > 48^-b`. + Thus `t=2,...,12` suffice for all larger `t`. + +Subtract I* from each relaxation. The twelve resulting functions have the form + +`D(b) = sum_r c_r r^(1-b)`. + +The certificate checks, for every one of them: + +1. `D(0)=sum c_r*r=0`. +2. The coefficients in increasing rank order have exactly two sign changes. +3. `D(1)=sum c_r <= 0`. +4. `D(1/3)>0`, using rational bounds on the cube roots of `r^2`. + +### Why these finite checks prove an interval + +We give the root-count fact used here. A nonzero generalized polynomial +`g(x)=sum_i a_i x^lambda_i`, with strictly increasing real exponents and +nonzero coefficients, has at most as many positive roots, counting +multiplicities, as coefficient sign changes. + +Proof: divide by the smallest power and induct on the number of terms. +The normalized function has constant term `a_0`; its derivative has the signs +of `a_1,...,a_n`. Rolle's theorem bounds its roots by the derivative's roots +plus one. If `a_0` and `a_1` have opposite signs, this gives the desired bound. +If they have the same sign, there is an extra derivative root before the first +function root: near zero the function has sign `a_0` and moves initially in +the direction of `a_1`, so it must turn before reaching zero. Counting this +root and the usual Rolle roots removes the extra one. Multiple roots count +with one less multiplicity in the derivative. This proves the induction; +the derivative bound also ensures there cannot be infinitely many roots. + +Apply this to `x=exp(b)` and exponents `-log(r)`. Reversing coefficient order +preserves the number of sign changes, and the factors `r` are positive. +Therefore D has at most two real zeros, counting multiplicities. +It already vanishes at zero. If it had another zero in `(0,1/3)`, its positive +value at `1/3` and nonpositive value at one would force a third zero in +`(1/3,1]`. This is impossible. Thus D is strictly positive on `(0,1/3]`. + +The exchange rule, integer exclusions, positive period, and these twelve +inequalities prove the stated optimum for every feasible profile. Strictness +holds for every different profile. No sampling of exponent values is used. + +## Independent validation + +`independent.py` imports neither the primary checker nor PR795's checker. +It enumerates integer width count vectors instead of using the knapsack +recurrence, and enumerates all capped partitions of 48 to check the new +classification. Its analytic argument uses no root-count assertion or +cube-root bounds. + +It multiplies D by `48^b`, removes the zero constant term, and divides by b. +Rational logarithm bounds give a degree-23 Taylor lower polynomial. Positive +omitted tails are discarded; negative tails receive an explicit geometric +bound, valid uniformly for `0 <= b <= 1/3`. Conversion to the Bernstein basis +on this full interval gives strictly positive coefficients in all twelve +cases. Since Bernstein basis functions are nonnegative and sum to one, this +independently certifies the crucial continuum inequalities. + +This is a different mathematical validation of the interval step and a +different enumeration of the integer fills. It is not independent human review, +a formal proof-assistant result, or an independent reconstruction of the full +native multiplication construction. Both checkers use the stated packing +model and the written concavity/period reduction. + +## Reproduce + +From the repository root, with standard-library Python 3.11 or later: + +```sh +python3 -B research/owner-profile-uniform/reproduce.py +``` + +Expected: `PASS_UNIFORM_OWNER_PACKAGE`. The command verifies pinned inputs, +recounts the archived PR799 native paid profile and all 36288 owner roles, +checks both proof models, and runs mutation and scope controls. + +`SOURCES.json` pins the imported main files. The current PR799 word comes from +`native/local/` in the retained `integrated799-replay.tar.gz`, not its older +R492 evidence snapshot. This run recounts those archived records; it does not +claim a fresh native scalar/phase/controller replay. Source PR799 is +`80e6463157cfc80b85af09e7e2f14748fe2dac60`; PR795 is +`56b626800c85026b10dada646c80c6b58179b427`. + +## Limits and credit + +The result does not cover different inventories, call counts, capacities, +split helpers, revised hosting rules, or competing local circuits themselves. +It proves no optimum outside the stated exponent interval. Any change to a +native word still needs its own complete scalar, frame, phase, owner, and +invoice validation. All-size compilation, common-label/mutable-source +realization, whole-call hosting, precision/tape and analytic-transfer +hypotheses remain inherited. No new κ or unconditional theorem is claimed. + +Credit: chafreaky supplies PR795's integer dual and concavity reduction, +PR741's frames, and the PR685/660 owner construction; Jeremy Kothe supplies +PR799's X4 exchanges and the PR699 SW4 lineage. The PR676 ends, PR664 promotions, +icekylinx's gauge, Rohan Arun's recurrence correction, DreamingOfClouds' bit +transport and eumemic's supplier retain their predecessor credit. + +Charles Bethin prepared this extension with substantial OpenAI Codex assistance +in the mathematics, code, verification, and writing. Apache-2.0 applies. +Existing source files, licenses, notices, and the selected frontier are unchanged. diff --git a/research/owner-profile-uniform/RESEARCH.json b/research/owner-profile-uniform/RESEARCH.json new file mode 100644 index 0000000000..88abe8846c --- /dev/null +++ b/research/owner-profile-uniform/RESEARCH.json @@ -0,0 +1,35 @@ +{ + "status": "research consolidation: proved finite packing theorem with a uniform real-parameter interval", + "task_id": "01a1335e-7a24-73c3-a549-9bcb5496a363", + "start": "2026-10-13T07:00:50.510Z", + "base": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "seed": 99, + "seed_source": "operating-system secrets.randbelow(100); scope selection only", + "track": "research consolidation", + "source_heads": { + "795": "56b626800c85026b10dada646c80c6b58179b427", + "799": "80e6463157cfc80b85af09e7e2f14748fe2dac60" + }, + "domain": { + "calls": 72, + "helper_width_inventory": { + "4": 80, + "5": 32, + "7": 54, + "8": 122, + "9": 216 + }, + "window_capacity_counts": { + "8": 48, + "16": 32, + "32": 32, + "48": 32 + }, + "bins_per_window": 112, + "saving_exponent": "0 < b <= 1/3" + }, + "stopping_rule": "Stop after complete interval proof and independent certificate; do not search changed inventories or wider intervals.", + "coordination": "No pinned issue; claim saved in local run capture. Final overlap refresh covers open PRs through848, with no duplicate uniform owner theorem.", + "assistance": "Substantial OpenAI Codex assistance; no independent human mathematical review.", + "library": "Hosted MCP tools and inbox unavailable. Local fallback used; records remain unreviewed pending Git incorporation." +} diff --git a/research/owner-profile-uniform/SOURCES.json b/research/owner-profile-uniform/SOURCES.json new file mode 100644 index 0000000000..008d2aa081 --- /dev/null +++ b/research/owner-profile-uniform/SOURCES.json @@ -0,0 +1,12 @@ +{ + "research/sw4-owner-optimality/PROOF.md": "6a8e72e8c6dfcfb9ba6416b985b80c93fed6a20dc498d1ffd9d8ef2a3a7b180d", + "research/sw4-owner-optimality/verify.py": "0812313b15eb1940ab20293e04a124dd3f6b5536736b0deb56bda6481cf95ace", + "research/sw4-owner-optimality/independent_check.py": "fe3b27a4999f6ac7ed94762a64e75632d9aeffa8fa763204e3b64db420eedd0b", + "research/sw4-owner-optimality/NOTICE.md": "e77a8648ca8c42e5cd4f0e8087afe2ba385c4d4f853f31efdf642f59ca3e65eb", + "research/gauge44-frames-x/data/PLAN.json": "5f40e7ccfca61f298539b4f41286d2a9d62caf947057f9cec82aa53f73f707fd", + "research/gauge44-frames-x/data/SPEC.json": "64817c60a4a2c1839bf12239cb1b7515a40bf8988229d81d4c9faa17b488c7d5", + "research/gauge44-frames-x/data/OWNERS.json.gz": "99d1c4caf85855c353d30f122d9efbd9e51562914facded13027f347b18a6082", + "research/community-frontier799-audit/integrated799-replay.tar.gz": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb", + "docs/research/community-frontier799-review.md": "bd91c10c67f2a873fd456b95cbb43f715a43dac0e0a66938737d591c6b754052", + "research/gauge44-frames-x/PROOF-NOTE-FRAMES-X4.md": "39c50420ebb6e8813706a49b2cf759f277c4afac9f6780fc0a7ac6a5fb86e036" +} diff --git a/research/owner-profile-uniform/VALIDATION.json b/research/owner-profile-uniform/VALIDATION.json new file mode 100644 index 0000000000..8769968f76 --- /dev/null +++ b/research/owner-profile-uniform/VALIDATION.json @@ -0,0 +1,31 @@ +{ + "verified_at": "2026-10-13T07:24:28.785392+00:00", + "proof_review": { + "claim": "Every feasible whole-helper packing has strictly larger idle moment than I* for every 0= 2: + x /= 2 + k += 1 + def series(z): + s = sum((2*z**(2*j+1)/(2*j+1) for j in range(64)), F(0)) + return s, s+2*z**129/(129*(1-z*z)) + a,b=series((x-1)/(x+1));c,d=series(F(1,3)) + return F(((a+k*c)*SCALE).__floor__(),SCALE), F(((b+k*d)*SCALE).__ceil__(),SCALE) + + +def bernstein(counts, limit=LIMIT): + # D(b)/b after multiplication by 48^b. Mass cancellation removes k=0. + require(sum(r*c for r,c in counts.items()) == 0, 'mass') + logs={r:log_bounds(F(48,r)) for r in counts} + coefficients=[] + for k in range(1,ORDER+1): + lower=sum(c*r*logs[r][0 if c>0 else 1]**k for r,c in counts.items())/factorial(k) + coefficients.append(F((lower*SCALE).__floor__(),SCALE)) + tail=F(0) + for r,c in counts.items(): + if c < 0: + u=logs[r][1] + require(limit*u < ORDER+2, 'tail ratio') + tail += (-c)*r*u**(ORDER+1)*limit**ORDER/factorial(ORDER+1)/(1-limit*u/(ORDER+2)) + tail=F((tail*SCALE).__ceil__(),SCALE) + # b = limit*t. Power-to-Bernstein conversion on the complete interval. + degree=ORDER-1 + beta=[sum(coefficients[k]*limit**k*F(comb(j,k),comb(degree,k)) + for k in range(j+1))-tail for j in range(degree+1)] + require(min(beta)>0, 'uniform Bernstein positivity') + return dict(lower_bernstein=str(min(beta)), tail=str(tail), degree=degree) + + +def partitions(total, cap): + if total == 0: + yield () + else: + for x in range(min(total,cap),0,-1): + for rest in partitions(total-x,x): + yield (x,)+rest + + +def packing(): + widths=(4,5,7,8,9);prices=(-1,-20,-8,-2,4) + cap_bonus={8:2,16:4,32:8,48:-13} + upper={}; patterns=0 + for cap,bonus in cap_bonus.items(): + for counts in product(*(range(cap//w+1) for w in widths)): + fill=sum(c*w for c,w in zip(counts,widths)) + if fill<=cap: + patterns+=1 + r=cap-fill;score=bonus+sum(c*p for c,p in zip(counts,prices)) + upper[r]=max(upper.get(r,-10**9),score) + require(upper[0]==0 and 2397*upper[48]<-31136,'all48 exclusion') + checked=eligible=0 + for parts in partitions(48,44): + checked+=1 + if any(r not in upper for r in parts): + continue + if 2396*upper[48]+sum(upper[r] for r in parts)<-31136: + continue + eligible+=1 + require(len(parts)>=2,'one-part residual') + if len(parts)==2: + require(parts[0]<=32,'two-part bound') + else: + require(parts[0]<=44 and parts[0]+parts[1]<=47,'majorization') + require(eligible>0,'nonempty relaxed class') + return dict(width_patterns=patterns, partitions_checked=checked, + dual_eligible_partitions=eligible, upper=upper) + + +def intervals(): + cases=[{16:1,32:1,44:-1,3:-1,1:-1}] + # Construct competitors from remaining mass, independently of primary cases(). + for mass in range(96,577,48): + q,rem=divmod(mass,44) + c={44:q,48:2397-mass//48} + if rem:c[rem]=c.get(rem,0)+1 + for r,n in ((48,2396),(44,1),(3,1),(1,1)): + c[r]=c.get(r,0)-n + cases.append({r:n for r,n in c.items() if n}) + require(len(cases)==12,'case coverage') + return [dict(coefficients=c,**bernstein(c)) for c in cases] + + +def main(): + ap=argparse.ArgumentParser(description=__doc__);ap.add_argument('--out',type=Path) + args=ap.parse_args() + result=dict(status='PASS_INDEPENDENT_UNIFORM_OWNER', packing=packing(), intervals=intervals()) + if args.out: + require(not args.out.exists(),'existing output') + args.out.write_text(json.dumps(result,indent=2)+'\n') + print('PASS_INDEPENDENT_UNIFORM_OWNER count_vectors+partitions+Bernstein interval=(0,1/3]') + +if __name__=='__main__': + main() diff --git a/research/owner-profile-uniform/reproduce.py b/research/owner-profile-uniform/reproduce.py new file mode 100644 index 0000000000..8039660738 --- /dev/null +++ b/research/owner-profile-uniform/reproduce.py @@ -0,0 +1,9 @@ +"""Run both proofs and mutation controls from any working directory.""" +from pathlib import Path +import subprocess +import sys + +p=Path(__file__).resolve().parent +for name in ('verify.py','independent.py','controls.py'): + subprocess.run([sys.executable,'-B',p/name],check=True) +print('PASS_UNIFORM_OWNER_PACKAGE') diff --git a/research/owner-profile-uniform/verify.py b/research/owner-profile-uniform/verify.py new file mode 100644 index 0000000000..1675eabc0e --- /dev/null +++ b/research/owner-profile-uniform/verify.py @@ -0,0 +1,174 @@ +"""Exact algebraic certificate for uniform whole-helper owner optimality. + +The integer prices and eleven-step reduction are due to chafreaky, PR795. +The uniform extension, additional exclusions, and algebraic checks are new. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from pathlib import Path +import argparse +import gzip +import hashlib +import json +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +WIDTHS = {4: 80, 5: 32, 7: 54, 8: 122, 9: 216} +CAPS = {8: 48, 16: 32, 32: 32, 48: 32} +PRICES = {4: -1, 5: -20, 7: -8, 8: -2, 9: 4} +BONUS = {8: 2, 16: 4, 32: 8, 48: -13} +IDLE = {48: 2396, 44: 1, 3: 1, 1: 1} +LOCAL = {1: 2548, 2: 338, 3: 430, 4: 194, 5: 56, 8: 8} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def sources(): + for name, digest in read(HERE/'SOURCES.json').items(): + need(hashlib.sha256((ROOT/name).read_bytes()).hexdigest() == digest, + 'source pin: '+name) + + +def bind_selected(): + p = ROOT/'research/gauge44-frames-x' + with tarfile.open(ROOT/'research/community-frontier799-audit/integrated799-replay.tar.gz') as archive: + word = json.loads(gzip.decompress(archive.extractfile('native/local/CANONICAL-WORD.json.gz').read())) + programs = json.loads(gzip.decompress(archive.extractfile('native/local/LOCAL-PROGRAMS.json.gz').read())) + plan, owners = read(p/'data/PLAN.json'), read(p/'data/OWNERS.json.gz') + spec = read(p/'data/SPEC.json') + need((word['v'], word['h'], word['R']) == (112, 9, 504), 'dimensions') + widths = [len(word['frames'][word['final'][h]])- + len(word['frames'][word['start'][h]]) for h in range(224, 728)] + need(Counter(widths) == WIDTHS, 'widths') + need(Counter(c for c, _ in plan['windows'].values()) == CAPS, 'capacities') + for direction in ('forward', 'backward'): + need(Counter(e[-1] for e in programs[direction] + if e[0] in ('climb', 'center')) == LOCAL, 'local moment') + calls = plan['provider_calls'] + need(len(calls) == 72 and {c['time'] for c in calls} == set(range(72)) + and all(c['provider'] == 'gauge44' for c in calls), 'dispatch') + need(plan['provider_registry']['gauge44']['widths'] == widths, 'registry') + cells, times, helpers = defaultdict(set), defaultdict(set), defaultdict(set) + for role in owners: + t, h = role['time'], role['helper'] + key = f"{role['owner_replica']},{role['child']}" + need(key in plan['windows'], 'window') + cap, allowed = plan['windows'][key] + port = role['port'] + need(t in allowed and 0 <= port < 112 and 0 <= h < 504, 'owner domain') + slot = key, port + need(t not in times[slot] and h not in helpers[t], 'duplicate role') + times[slot].add(t); helpers[t].add(h) + need(role['width'] == widths[h], 'role width') + start = role['offset']; used = set(range(start, start+widths[h])) + need(0 <= start and start+widths[h] <= cap and not used & cells[slot], 'cells') + cells[slot].update(used) + need(len(owners) == 72*504 and all(helpers[t] == set(range(504)) + for t in range(72)), 'all roles') + idle = Counter() + for key, (cap, _) in plan['windows'].items(): + for port in range(112): + remaining = cap-len(cells[key, port]) + if remaining: + idle[remaining] += 1 + need(idle == IDLE, 'attained profile') + total = Counter({r: 72*n for r, n in LOCAL.items()}); total.update(idle) + need(dict(total) == {int(r): n for r,n in plan['profile'].items()} + == {int(r): n for r,n in spec['expected']['global_profile'].items()}, 'invoice') + return dict(helper_roles=len(owners), widths=WIDTHS, capacities=CAPS, + idle=dict(idle), local=LOCAL) + + +def dual(): + upper = {} + for cap in CAPS: + dp = [0]+[None]*cap + for fill in range(1, cap+1): + choices = [dp[fill-w]+PRICES[w] for w in WIDTHS + if fill >= w and dp[fill-w] is not None] + dp[fill] = max(choices) if choices else None + for fill, value in enumerate(dp): + if value is not None: + r = cap-fill + upper[r] = max(upper.get(r, -10**9), BONUS[cap]+value) + base = 112*sum(CAPS[c]*BONUS[c] for c in CAPS)+72*sum(WIDTHS[w]*PRICES[w] for w in WIDTHS) + need(base == -31136 and upper[0] == 0, 'dual baseline') + need(2397*upper[48] < base, 'all48') + need(sum(upper[r]*n for r,n in IDLE.items()) == base, 'dual attainment') + excluded = [] + for largest in range(33, 45): + other = 48-largest + if largest not in upper or other not in upper: + excluded.append(dict(parts=[largest, other], reason='unreachable residual')) + else: + bound = 2396*upper[48]+upper[largest]+upper[other] + need(bound < base, 'two-part exclusion') + excluded.append(dict(parts=[largest, other], bound=bound, gap=base-bound)) + return dict(upper=upper, base=base, excluded_two_parts=excluded) + + +def cases(): + answer = [('two-parts', {32: 1, 16: 1, 44: -1, 3: -1, 1: -1})] + for t in range(2, 13): + q, r = divmod(48*t, 44) + counts = {48: 1-t, 44: q-1, 3: -1, 1: -1} + if r: + counts[r] = counts.get(r, 0)+1 + answer.append((f't{t}', {r:n for r,n in counts.items() if n})) + return answer + + +def cube_root_bounds(r, bits=80): + scale = 1 << bits + target = r*r*scale**3 + lo, hi = 0, r*scale+1 + while hi-lo > 1: + mid = (lo+hi)//2 + if mid**3 <= target: + lo = mid + else: + hi = mid + need(lo**3 <= target < (lo+1)**3, 'cube bracket') + return Q(lo, scale), Q(lo if lo**3 == target else lo+1, scale) + + +def algebraic(): + bounds = {r:cube_root_bounds(r) for r in range(1,49)} + result=[] + for name, counts in cases(): + need(sum(r*n for r,n in counts.items()) == 0, 'zero at b=0') + need(sum(counts.values()) <= 0, 'nonpositive at b=1') + signs = [1 if counts[r] > 0 else -1 for r in sorted(counts)] + changes = sum(a != b for a,b in zip(signs, signs[1:])) + need(changes == 2, 'two sign changes') + lower = sum(n*bounds[r][0 if n > 0 else 1] for r,n in counts.items()) + need(lower > 0, 'positive at b=1/3') + result.append(dict(name=name, coefficients=counts, sign_changes=changes, + value_at_one=sum(counts.values()), lower_at_third=str(lower))) + need(len(result) == 12, 'complete reduced cases') + return result + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + args=parser.parse_args() + sources() + result=dict(status='PASS_UNIFORM_OWNER_OPTIMALITY', interval='0 < b <= 1/3', + selected=bind_selected(), dual=dual(), algebraic=algebraic()) + if args.out: + need(not args.out.exists(), 'output already exists') + args.out.write_text(json.dumps(result,indent=2)+'\n') + print('PASS_UNIFORM_OWNER_OPTIMALITY cases=12 roles=36288 interval=(0,1/3]') + +if __name__ == '__main__': + main()