Prove the sharp direct higher-moment integer split charge (no κ)

research/direct-higher-moment-split/PROOF.md

@@ -0,0 +1,142 @@
+# The sharp direct higher-moment split coefficient
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+## Theorem
+
+Fix real numbers `0<t<1` and `sigma>1`. For positive integers `R>J`, write
+`R=qJ+r`, where `q>=1` and `0<=r<J`, and set
+
+```
+split_t(R,J) = q J^t + r^t.
+```
+
+There is exactly one `s=s_(t,sigma)` in `(0,1)` satisfying
+
+```
+t s^(t-1) + (t-sigma)s^t - sigma = 0.
+```
+
+The least coefficient valid for every such integer split is
+
+```
+K(t,sigma) = (1+s^t)/(1+s)^sigma
+           = (t/sigma) s^(t-1) (1+s)^(1-sigma).
+
+split_t(R,J) <= K(t,sigma) R^sigma J^(t-sigma).
+```
+
+It satisfies `1<K(t,sigma)<K(t,1)<2`, where `K(t,1)` is the coefficient
+of PR4832. Equality at finite integers occurs exactly when `q=1` and
+`r/J=s_(t,sigma)`. The supremum is sharp even when that remainder is irrational.
+
+## Proof
+
+Divide the split charge by `R^sigma J^(t-sigma)` and put `s=r/J`. The ratio is
+
+```
+F_q(s) = (q+s^t)/(q+s)^sigma.
+```
+
+For a fixed `s` in `[0,1)`, extend `q` temporarily to a real variable `q>=1`.
+Its derivative has the sign of
+
+```
+(1-sigma)q + s - sigma s^t < 0.
+```
+
+Indeed `s<=s^t` and `sigma>1`. Thus every integer `q>1` is strictly worse
+than `q=1`. This step retains the denominator's full higher moment, unlike
+the linear-rank estimate followed by a separate moment comparison in PR4832.
+
+For `F_1`, the derivative on `(0,1)` has the sign of
+
+```
+h(s) = t s^(t-1) + (t-sigma)s^t - sigma,
+h'(s) = t(t-1)s^(t-2) + t(t-sigma)s^(t-1) < 0.
+```
+
+The function `h` tends to positive infinity at zero and has
+`h(1)=2(t-sigma)<0`. It has one zero, and this is the unique maximum of
+`F_1` on `[0,1]`. Its stationary equation gives the second expression for K.
+Since `F_1(0)=1` and the derivative is positive before that maximum, `K>1`.
+At its positive maximizer, division by `(1+s)^(sigma-1)>1` gives
+`K(t,sigma)<(1+s^t)/(1+s)<=K(t,1)`. PR4832 supplies `K(t,1)<2`.
+
+For sharpness over integers, let `J` tend to infinity and choose
+`r=floor(s_(t,sigma) J)`, `R=J+r`. Eventually `0<r<J`, and continuity makes
+the ratio tend to K. Every coefficient smaller than K therefore fails for
+some integer split. Strict quotient monotonicity and the unique maximum
+also give the stated equality characterization. This proves the theorem.
+
+## An exactly attaining rational-power example
+
+Take `t=1/2`, `sigma=17/10`. Substitution gives `h(1/16)=0`, so
+
+```
+s = 1/16,
+K = (5/4) (16/17)^(17/10),
+K^10 = (5/4)^10 (16/17)^17.
+```
+
+Every `J=16n`, `R=17n`, for positive integer n, attains the coefficient.
+Exact integer comparisons show `9/8<K<8/7<6/5`. In contrast,
+PR4832's cited coefficient `K(1/2,1)=(1+sqrt(2))/2` is greater than `6/5`.
+This is a strict improvement of the direct higher-moment coefficient.
+It does not by itself specify a realizable productive/paid profile.
+
+## Consequence for retained strictification
+
+Retain every chronological product, native, completion, splitting and compiler
+hypothesis of zxv's PR4433, section 2. Let `C=1-t`, `u>C`, `sigma=t+u>1`,
+`J=c^v` and `L=b^v`, with `1<c<b<m` and positive integer v. Write `P_x,T_x`
+for the raw paid and productive rank moments and B for its productive count.
+For every original paid rank R exceeding J, the theorem gives
+
+```
+split_t(R,J) <= K(t,t+u) R^(t+u) J^(-u).
+```
+
+The predecessor's moment multiplication and its unchanged unsplit overcount
+therefore bound the original-paid charge by
+
+```
+P_t^v + K(t,t+u) P_(t+u)^v / J^u.
+```
+
+Keep its full separate completion bound `2 B^v L J^(-C)` and the lower bound
+`T_t^v` on the completed productive moment. The complete sufficient charge is
+
+```
+alpha^v + K(t,t+u) gamma_u^v + 2 delta^v,
+alpha=P_t/T_t,
+gamma_u=P_(t+u)/(c^u T_t),
+delta=B b/(c^C T_t).
+```
+
+This strictly lowers the coefficient `K(t,1)` in PR4832 whenever `u>C`.
+The completion coefficient, unsplit overcount and all realization premises
+are retained. No particular inventory, tensor power or admitted supplier is
+certified here. The direct compiler of zxv's PR4483 can avoid strictification
+for profiles satisfying its own gates; this result makes no comparison to
+that compiler's sufficient sizes.
+
+## Exact finite certificate
+
+For rational `t=a/b`, `sigma=c/d`, put `y=s^(1/b)`. The critical equation
+becomes the strictly decreasing polynomial
+
+```
+ad + (ad-bc)y^b - bc y^(b-a) = 0.
+```
+
+The verifier bisects this polynomial using rational arithmetic. At any rational
+y, the normalized ratio's d-th power is exactly
+
+```
+F_q(y^b)^d = (q+y^a)^d / (q+y^b)^c.
+```
+
+Thus its root enclosures, finite split checks and attaining example require
+neither floating-point tolerances nor algebraic-number libraries. These checks
+corroborate the proof; they are not a universal census or proof-kernel acceptance.

research/direct-higher-moment-split/README.md

@@ -0,0 +1,141 @@
+# Sharp direct higher-moment split charge
+
+For every real `0<t<1` and `sigma>1`, the least coefficient in
+
+```
+split_t(R,J) <= K(t,sigma) R^sigma J^(t-sigma),
+R=qJ+r>J,  0<=r<J,
+split_t(R,J)=q J^t+r^t,
+```
+
+is
+
+```
+K(t,sigma) = (1+s^t)/(1+s)^sigma,
+t s^(t-1)+(t-sigma)s^t-sigma=0,  0<s<1.
+```
+
+The defining equation has one solution, and the coefficient is sharp over
+integer jobs. This answers Open next question 2 of
+[PR4832](https://github.com/CrocSwap/integer-mult-bounds/pull/4832).
+The claim type is a scoped written proof with exact finite corroboration.
+
+The coefficient is strictly smaller than the linear-rank coefficient
+`K(t,1)` transferred to the higher moment. At `t=1/2, sigma=17/10`,
+
+```
+K = (5/4)(16/17)^(17/10),
+9/8 < K < 8/7 < 6/5 < K(1/2,1).
+```
+
+Every `J=16n, R=17n`, with positive integer n, attains this new coefficient.
+[PROOF.md](PROOF.md) proves the universal optimization, integer sharpness and
+its exact strictification consequence. No new kappa or selected-frontier change
+is claimed.
+
+## What changes in the retained compiler estimate
+
+Retain all hypotheses of zxv's
+[PR4433 higher-moment construction](https://github.com/CrocSwap/integer-mult-bounds/pull/4433).
+With `C=1-t` and `u>C`, its complete sufficient charge improves as follows.
+
+```diff
+-alpha^v + K(t,1)   gamma_u^v + 2 delta^v
++alpha^v + K(t,t+u) gamma_u^v + 2 delta^v
+```
+
+The full completion charge and unsplit overcount remain. The proof derives
+this consequence from the credited moment-product premise, without replaying
+predecessor programs or numbers. This is a sharp coefficient for the full
+split charge, not a net-tax optimum, a smaller demonstrated tensor power or
+a newly admitted supplier. PR4483's different direct compiler can avoid
+strictification under its own gates.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/direct-higher-moment-split/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/direct-higher-moment-split/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/direct-higher-moment-split
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/direct-higher-moment-split --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 path. The last check requires
+committed publication bytes. The scientific command prints a JSON receipt with
+`PASS_DIRECT_HIGHER_MOMENT_SPLIT`; the runner prints
+`PASS_REGISTERED_RESEARCH_PACKAGE`. To save a generated receipt, append
+`--receipt /absolute/path/outside/the/checkout.json` to a direct command.
+Normal replay writes no files. Receipts bind all six package files and both
+source documents by SHA256; no receipt is hand-written or treated as an oracle.
+
+The finite verifier checks 30 rational parameter pairs, 7,650 exact integer
+splits, 6,720 strict quotient comparisons and 30 near-maximizing integer
+witnesses. It also checks the exactly attaining family representative and
+13 rejecting controls. Rational polynomial bisection encloses each maximizing
+remainder; comparisons use powers of positive rational numbers. No floating
+point or predecessor executable is used. The written proof covers arbitrary
+real parameters; finite examples do not supply that universal quantification.
+Checks remain enabled under Python optimization.
+
+## Scope and overlap
+
+The `uniform-transfer-audit` card is changed from assumption audit to a new
+compiler coefficient theorem. This side result tightens one sufficient
+accounting bound; it does not discharge any of the five framework assumptions.
+The documented first source-binding control passes against selected PR6030.
+Source provenance is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+
+[The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358948)
+records the exact question. Entry checks inspected live open PRs, recent handoff
+claims, merged titles/bodies and distinctive formulas in all tracked main
+package READMEs. The question source predates the recent contribution series.
+Search coverage does not certify novelty; sparse notes, arbitrary historical
+diffs and unpublished work remain limits.
+
+Native semantics, dirty restoration, paid placement, chronological compiler
+closure, precision, stock, tape access and exact recovery remain inherited
+obligations. No physical caller, selected cold replay, native suite, Lean or
+Docker run is supplied. No independent human or proof-kernel acceptance is
+claimed.
+
+## Verification design
+
+The verifier has no recursion, subprocesses, callbacks or imported predecessor
+code. All scientific loops have explicit finite bounds. Its census uses six
+exponents, five higher moments, 32 remainder parameters and eight quotients;
+root isolation takes 72 steps. Rational parameters have denominators at most
+16, `0<t<1` and `1<sigma<=4`. Functions stay below 60 physical lines. Input
+source documents must match the declared hashes.
+
+Power of Ten deviation, rule 3: Python's integers, fractions and JSON serializer
+allocate dynamically. The fixed census, root precision, parameter limits and
+2 MB per-file check bound this verifier's mathematical workload. The reviewed
+local metadata files and synchronous standard-library reads are trusted inputs;
+this is not an allocation-free or hostile-filesystem parser. A fixed-memory
+port would be needed if that execution contract becomes a requirement.
+
+## Open next questions
+
+- Apply the coefficient to one fully charged supplier that still uses
+  strictification. First reuse its exact moment enclosures and replace only
+  this coefficient. A smaller sufficient tensor power must retain all native,
+  completion, compiler and outer premises.
+- Determine the least direct coefficient for the net splitting tax. Start with
+  `(q+s^t-(q+s)^t)/(q+s)^sigma`, and inspect PR4480's net-tax bounds. The quotient
+  monotonicity here concerns a different objective and cannot be transferred.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.
+
+PR4832 supplies the question and linear-rank predecessor. zxv's PR4433 supplies
+the higher-moment splitting/completion framework; PR4480 and PR4483 retain their
+net-tax and direct-compiler results. Cinna Davis's PR4412/4414/4416 supplies the
+chronological tensor product and padding construction. Jacob Alan Sussman
+supplies the integer compiler. Their native, helper, controller and outer
+predecessors retain their existing credit. Elementary one-variable calculus
+is classical; no literature-priority claim is made.

research/direct-higher-moment-split/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/higher-moment-strictification/README.md",
+      "usage": "input",
+      "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3",
+      "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d"
+    },
+    {
+      "path": "research/sharp-integer-split-charge/README.md",
+      "usage": "input",
+      "git_blob": "224381ce045536f526282437cd2d4faffbbf01d3",
+      "sha256": "522439b2265b6a497a0d432e0911eb3e52e360650583c5469bc948da0cf6572d"
+    }
+  ]
+}