Bound the paid-fusion moment ceiling exactly (no κ)

research/paid-fusion-moment-ceiling/PROOF.md

@@ -0,0 +1,133 @@
+# Paid-fusion moment ceiling
+
+A legal rewrite that fuses paid child jobs keeps the productive multiset `T`
+fixed and replaces paid ranks `b_1,...,b_m` by their sum. This package proves
+what such a rewrite can and cannot buy at a crossing exponent `c` with
+`0 < c < 1`, and gives the exact ceiling. Nothing here is source-bound: it is a
+statement about the moment model the signed invoice uses, not about a word.
+
+## Definitions
+
+For a finite multiset `H` of positive integers (ranks) and real `c`, write
+
+  `M_H(c) = sum_{h in H} h^c`.
+
+The gate compares `M_T(c)` with `M_P(c)`; a rewrite is favourable at `c` when it
+increases `M_T(c) - M_P(c)`. The crossing exponent is the root of that
+difference on the relevant interval.
+
+## Results
+
+Throughout `0 < c < 1` and all ranks are integers `>= 1`.
+
+1. **Strict subadditivity.** `(a+b)^c < a^c + b^c` for all `a,b >= 1`.
+   Consequently every paid fusion strictly lowers the paid moment at every
+   exponent in `(0,1)`, and every productive split strictly raises the
+   productive moment at every such exponent. The sign is exactly reversed for
+   `c > 1` and everything is an equality at `c = 1`.
+
+2. **m-block form.** For `m >= 2` and `b_i >= 1`,
+   `(b_1+...+b_m)^c < b_1^c + ... + b_m^c`.
+
+3. **Sharp single-fusion cap.** With `D(a,b) = a^c + b^c - (a+b)^c`,
+
+   `0 < D(a,b) < min(a,b)^c`,
+
+   and the constant one is sharp: for fixed `a`, `D(a,b)/a^c -> 1` as
+   `b/a -> infinity`. It is never attained. For a fixed total rank `r = a+b`,
+   `D(a,r-a)` is instead maximized by the balanced split and minimized by the
+   unbalanced ones. So no single fusion is worth one full copy of its smaller
+   job's moment; very unequal pairs approach that cap when the smaller rank is
+   held fixed, while at a fixed total paid mass a balanced merge buys most.
+
+4. **Global fusion ceiling.** Let `P` be a paid multiset and let any partition
+   of `P` into blocks be replaced by the block sums. The paid moment falls, and
+   it stays at least the single-job moment of the whole paid mass:
+
+   `M_{P'}(c) >= (sum_{p in P} p)^c`,  so  `M_P(c) - M_{P'}(c) <= G(c)`,
+
+   where `G(c) = sum_{p in P} p^c - (sum_{p in P} p)^c`, with equality only for
+   the one-block (full) fusion. `G` is therefore the total budget every
+   paid-only fusion scheme shares.
+
+5. **Crossing consequence.** If a rewrite fuses paid jobs and leaves `T` fixed,
+   then at every `c` in `(0,1)`
+
+   `M_T(c) - M_{P'}(c) <= M_T(c) - (sum_{p in P} p)^c`.
+
+   Hence the crossing exponent after any paid-only fusion is at most the root
+   of `M_T(c) = (sum_P p)^c`. No choice of which jobs to fuse, and no number of
+   fusions, can pass that root. This is the stopping rule: a paid-fusion search
+   that cannot reach the root against one collapsed paid job cannot reach the
+   claim either.
+
+## Proofs
+
+1. `x -> x^c` is concave on `[0,inf)` for `0<c<1`, so its derivative is
+   strictly decreasing and
+
+   `(a+b)^c - a^c = int_a^{a+b} c x^{c-1} dx < int_0^b c x^{c-1} dx = b^c`.
+
+   Concavity also gives `(a+b)^c > b^c` and `(a+b)^c > a^c`. For `c>1` the
+   derivative is increasing and both inequalities reverse; at `c=1` the two
+   sides are equal.
+
+2. Induct on `m`, applying (1) to `(b_1+...+b_{m-1})` and `b_m`; the sum of the
+   first `m-1` terms is itself strictly greater than their `c`-power sum.
+
+3. Lower bound: `D > 0` is (1). Upper bound: assume `a <= b`; then
+   `D = a^c + b^c - (a+b)^c < a^c` because `b^c < (a+b)^c`. Sharpness: put
+   `s = b/a`; then `D/a^c = 1 + s^c - (1+s)^c`, and
+   `(1+s)^c - s^c = s^c((1+1/s)^c - 1) -> 0`, so the ratio tends to one. The
+   fixed-sum claim: `g(a) = a^c + (r-a)^c` has
+   `g''(a) = c(c-1)(a^{c-2} + (r-a)^{c-2}) < 0`, so `g` is concave and
+   symmetric; a concave symmetric function is maximized at its midpoint and
+   minimized at an endpoint, so `D = g - r^c` has the same two extrema in the
+   same order. Over integers `a >= 1` the endpoints are `a = 1` and `a = r-1`.
+
+4. Apply (2) inside every block: the merged moment is strictly smaller than
+   `M_P(c)` unless every block is a singleton. Apply (2) to the block sums
+   themselves: `(sum_j s_j)^c < sum_j s_j^c` whenever there are at least two
+   blocks, so `M_{P'}(c) > (sum_P p)^c` for every non-trivial partition. The
+   one-block partition gives `M_{P'} = (sum_P p)^c` exactly, which is the
+   smallest value any partition can reach and the ceiling `G(c)`.
+
+5. Substitute (4) into the definition of the difference; both sides are
+   monotone in `c`, so the root cannot move right of the root against the
+   collapsed paid job.
+
+## Verification
+
+`verify.py` encloses every `a^c` in an exact rational interval and then checks
+the statements above by exact rational comparison on finite grids:
+
+- subadditivity and the sharp cap for all `1 <= a <= b <= 40` at five
+  exponents, including `c = 363005817/100000000000` (the selected record's
+  exponent) and `c = 1/279`, `1/1000` (`BIT`-scale and millesimal regimes);
+- the `m`-block form for `m = 2,3,4` on five block shapes per exponent;
+- the approach of `D(1,b)` to its cap for `b = 10^2..10^12` with exact integer
+  square roots at `c = 1/2`, certifying `0.99 < D < 1` from `b = 10^4`;
+- balanced-split optimality at fixed total rank against every other split of
+  the same total for `3 <= r <= 60`;
+- the global ceiling over five explicit multisets and every partition shape,
+  with full collapse attaining the bound, plus a non-fusion control showing a
+  paid split strictly raises the moment;
+- rejection controls: `c = 1, 2, 3/2` (hypothesis fails), and non-positive
+  ranks or `c = 0` (rejected).
+
+The transcendental step is CPython `decimal` at 90 digits, correctly rounded
+per its documentation, widened by one unit in the last place; all later
+arithmetic is exact rational. A certified inequality is therefore a proof of
+that finite case, not a floating-point observation.
+
+## Limitations
+
+- The result is a statement about the moment model. It does not certify that any
+  word, caller, compiler, precision tape or outer row exists, and it does not
+  bound the productive side, where #6651 already gives the balanced-split
+  optimum for a concave tariff.
+- Lemma 1 is classical. What is new here is the quantitative cap in (3), the
+  total budget in (4) and the crossing consequence in (5), which turn the
+  classical inequality into a search-stopping rule.
+- No source-bound invoice is evaluated: the package proves a ceiling that any
+  such invoice must respect.

research/paid-fusion-moment-ceiling/README.md

@@ -0,0 +1,113 @@
+# Paid-fusion moment ceiling
+
+How much can a paid-side rewrite buy at a crossing exponent `c` with
+`0 < c < 1`? This package answers the fusion case exactly.
+
+## Scope
+
+A *paid fusion* replaces paid ranks `b_1,...,b_m` by their sum `b_1+...+b_m`
+and leaves the productive multiset `T` fixed. Write `M_H(c) = sum_{h in H} h^c`
+for a finite multiset of positive integer ranks. No word, caller, compiler,
+precision tape or outer row is claimed; this is a statement about the moment
+model that the signed invoice evaluates.
+
+## Result
+
+Claim type: scoped written proof with exact finite corroboration. No κ change.
+
+1. `(a+b)^c < a^c + b^c` strictly for all integers `a,b >= 1` and every
+   `c` in `(0,1)`; equality at `c = 1`; the inequality reverses for `c > 1`.
+   Every paid fusion therefore strictly lowers `M_P(c)` and every productive
+   split strictly raises `M_T(c)` on the whole sub-unit exponent range.
+2. The single-fusion saving `D(a,b) = a^c + b^c - (a+b)^c` obeys
+   `0 < D(a,b) < min(a,b)^c`. The constant one is sharp
+   (`D(a,b)/a^c -> 1` as `b/a -> infinity` for fixed `a`) and never attained.
+3. At a fixed total paid rank `r = a+b`, `D(a,r-a)` is maximized by the
+   balanced split and minimized by the unbalanced ones.
+4. Let any partition of a paid multiset `P` be replaced by its block sums. The
+   paid moment falls, and for every partition
+
+   `M_{P'}(c) >= (sum_{p in P} p)^c`, hence
+   `M_P(c) - M_{P'}(c) <= G(c) = sum_{p in P} p^c - (sum_{p in P} p)^c`,
+
+   with equality only for the one-block collapse. `G(c)` is the total budget
+   that all paid-only fusion schemes share.
+5. Consequently the crossing exponent after any paid-only fusion is at most the
+   root of `M_T(c) = (sum_{p in P} p)^c`. No set of fusions, and no choice of
+   which jobs to fuse, can pass that root.
+
+Point 5 is the usable form: it converts a fusion family into one scalar test
+that needs no word replay.
+
+## Evidence
+
+`verify.py` encloses each `a^c` in an exact rational interval and then compares
+exactly. It certifies, with zero inconclusive cases:
+
+- points 1 and 2 for all `1 <= a <= b <= 40` at five exponents: `1/1000`,
+  `1/279`, `363005817/100000000000` (the selected record's exponent), `1/2`
+  and `3/4`;
+- the `m`-block form for `m = 2,3,4` on five block shapes per exponent;
+- the sharpness approach `0.99 < D(1,b) < 1` for `b = 10^4..10^12` at
+  `c = 1/2`, with exact Newton enclosures of both square roots;
+- point 3 against every other split of the same total for `3 <= r <= 60`;
+- point 4 on five explicit multisets and every partition shape, with the full
+  collapse attaining the bound, plus a non-fusion control where a paid split
+  strictly raises the moment;
+- rejection controls at `c = 1, 2, 3/2` and for non-positive ranks or `c = 0`.
+
+The transcendental step is CPython `decimal` at 90 digits (correctly rounded per
+its documentation), widened by one unit in the last place; all later arithmetic
+is exact rational, so a certified inequality is a proof of that finite case.
+`RESULT.json` stores the SHA-256 of the canonical summary and of `PROOF.md`;
+`verify.py` recomputes both and fails on any mismatch.
+
+## Reproduction
+
+From the repository root with CPython 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/paid-fusion-moment-ceiling
+python3.12 -B scripts/check_research_commit.py --package research/paid-fusion-moment-ceiling --check-source-history
+```
+
+The registered command is `{python} -B {package}/verify.py`. It runs in a few
+seconds.
+
+## Limitations
+
+- The ceiling is a moment-model statement. A legal realization, native delivery,
+  dirty restoration, the compiler, the precision tape and the nine outer rows
+  remain separate obligations.
+- Only the paid side is bounded here. The productive side already has a
+  balanced-split optimum and halving test for a concave rank tariff in #6651;
+  that result is cited, not re-derived or replayed.
+- The package does not evaluate any invoice. Points 4 and 5 are a template: an
+  application needs the exact `T` and `P` the gate consumes.
+
+## Open next questions
+
+1. **Apply the ceiling to one live fusion family.** Take the exact invoice
+   histogram the interval gate consumes, collapse `P` to one job of rank
+   `sum p`, and compute the root of `M_T(c) = (sum p)^c`. Report whether the
+   family's target lies above that root. First step: read the gate's own audit
+   input rather than the `invoice` summary block of
+   `research/shared-wire-split-composition/FULL-RESULT.json`, because the
+   summary histograms are not interchangeable with the gate's argument. Why it
+   matters: one scalar decides whether more fusion exclusions are worth
+   running. Blocked by: pinning the rank convention of that audit input.
+2. **Fusion plus productive credit.** Extend to rewrites that fuse paid jobs and
+   also add productive targets. Does the budget stay separable, or does the
+   joint movement of both sides need a two-parameter bound? First step: state
+   the joint model and look for a counterexample to separability. Blocked by:
+   no joint model is fixed in the current packages.
+
+## Credit
+
+The quantitative cap, the global fusion budget and the crossing consequence,
+with the verifier and certificate, were produced by Nick Petalas. Credit
+thakrarsagar's #718 for the scoped `(5,1)`-versus-`(4,2)` paid-read comparison
+that exhibits the same subadditivity on specific ranks, and Nick Petalas's #6651
+for the balanced-split optimum and halving test on the productive side; both are
+cited background, not replayed. Concavity of `x^c` is classical. Apache-2.0.
+Independent human review and formal proof-kernel acceptance are unclaimed.

research/paid-fusion-moment-ceiling/RESULT.json

@@ -0,0 +1,10 @@
+{
+ "claim_type": "scoped written proof with exact finite corroboration",
+ "result": "For 0 < c < 1 and integer ranks, every fusion of paid child jobs strictly lowers the paid moment; a single fusion of ranks a,b saves D(a,b) with 0 < D(a,b) < min(a,b)^c and sharp constant one; at fixed total rank the balanced split maximizes D; any fusion scheme lowers the paid moment by at most G(c) = sum p^c - (sum p)^c, so a paid-only rewrite cannot push the crossing exponent past the root against one paid job of the total paid rank. No kappa change.",
+ "exponents_checked": ["1/1000", "1/279", "363005817/100000000000", "1/2", "3/4"],
+ "precision_digits": 90,
+ "receipt_sha256": "d6f45214086f34643da291c9919120f0d3bb79d41016d67386c302c174027593",
+ "proof_sha256": "127cef22ad813fe99b9ef132ce44c11786522093c9b4bd6bfa9de7717ba59bf7",
+ "interpretation": "A searching contributor can reject a whole paid-fusion family without a word replay: compute the root against one collapsed paid job; if it is below the target, no fusion scheme reaches the target.",
+ "limitations": "Moment model only. No word, caller, compiler, precision tape or outer row is certified. The productive side is not bounded; #6651 gives the balanced-split optimum there."
+}

research/paid-fusion-moment-ceiling/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}