Certify higher-order rank exchanges beyond concave dominance

research/higher-order-rank-exchanges/.gitignore

@@ -0,0 +1,2 @@
+__pycache__/
+*.pyc

research/higher-order-rank-exchanges/INPUTS.json

@@ -0,0 +1,3 @@
+{
+  "inputs/current-profile.json": "9686df0d8e710c2e94aef3887f4bf130a05b64215faeae702cccb59e95a469d5"
+}

research/higher-order-rank-exchanges/NOTICE

@@ -0,0 +1,18 @@
+New higher-order exchange proof and implementation: Dugongue with substantial OpenAI Codex assistance. Apache-2.0.
+The separate exact-power oracle is retained from PR3863, by the same author, under Apache-2.0.
+The finite-difference identity and alternating derivative signs are classical mathematics.
+
+Retained predecessor notices:
+
+Apache-2.0. New work by Dugongue with substantial OpenAI Codex assistance.
+
+Retained attribution from canonical main research/ranked-pair-verification/PROOF.md:
+
+
+The interval strips and core-aware pair graph are [Avi Eisenberg / ikeboy's PR62](https://github.com/CrocSwap/integer-mult-bounds/pull/62), with disclosed Anthropic Claude assistance. The joint-frame compiler and paid reclamation are [eumemic's PR57](https://github.com/CrocSwap/integer-mult-bounds/pull/57), with OpenAI Codex assistance. Descending-current-frame-rank slot priority is [Chafik Boukhalfa's PR60](https://github.com/CrocSwap/integer-mult-bounds/pull/60), with OpenAI Codex assistance. Dominik Scholz's concurrent PR63 discloses substantial OpenAI GPT-6 Astra / Codex assistance. This independent verification and formalization was developed with substantial OpenAI Codex assistance.
+
+The inherited work of Rohan Arun, RaD / hipotures, icekylinx, Zhihao Chen, James Chang, Dominik Scholz, Aurel Prosz / Paureel, Swapnil Jain, Douglas Colkitt and other credited contributors remains attributed in the pinned source notices. The dirty-wrapper argument is inherited mathematics, newly formalized here. Alejandro Zarzuelo Urdiales's Gaussian finite-tensor/precision work and PR61 refinements, and Ryan S's historical Lean certificates, retain their separate credit. The [original OpenAI work](https://github.com/openai/math) and Harvey–van der Hoeven analytic results remain foundational dependencies. Retain all source-specific notices and Apache-2.0 terms.
+
+The displayed multiplication exponent is conditional on the inherited all-size framed/residual compiler, physical routing and finite-alphabet multitape implementation, analytic resampling, precision, prime setup and exact recovery. Finite replay, rational arithmetic and the listed formal statements do not discharge that complete chain. No practical speedup, global optimality or human peer-review claim is made.
+
+Current-profile calibration: ChaloupeMusic (PR3815), hexapode (PR3802), dataisfire (PR3734) and the retained staged supplier native/owner/hosting lineage, as credited in PR3857. Only the 92-byte histogram is copied; no native source or word is imported.

research/higher-order-rank-exchanges/OVERLAP.md

@@ -0,0 +1,34 @@
+# Overlap and source checkpoint
+
+Canonical main fetched at entry and before submission:
+`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6.
+Current AGENTS.md, autoresearch.md and CONTRIBUTING.md match the preceding
+round's authenticated bytes; current priorities, catalogue and selected record
+were refreshed. The independent-moment selector card is retained verbatim with
+a changed scope and explicit reason, not rerolled.
+
+Fresh full pagination scanned 571 open PR titles/bodies, including drafts.
+The repository find_overlap.py searched that snapshot and local package notes
+with finite difference, higher order rank, Bernstein and complete monotonicity
+terms. It reports possible overlap and incomplete Discussion coverage.
+The latest 100 all-state updated PR records and final 30-record delta through
+PR3866 were scanned. No arbitrary-diff, full historical closed-PR or unpublished
+coverage is claimed. Start-here and handoff Discussion HTML was retrieved,
+with partial possible reply coverage and no complete GraphQL cache.
+
+Actual compared sources include ranked-pair-verification's capped-mass test,
+PR3863's paid concave-order theorem and oracle, coded-helper-early-end8's
+binomial power-series evaluator and outer-bernstein-certificate's polynomial
+positivity certificate. The latter two use different binomial/Bernstein methods;
+the present statement is an alternating finite-difference exchange of child
+ranks, not another series root calculation or Bernstein polynomial certificate.
+Main-tree path search and a bounded MathProof Computability text search were
+also used. This is not a search of the entire federated library or live DAG.
+
+The signed examples have a positive capped sum and hence provably fall outside
+the all-concave order. Their power-moment sign follows from higher derivatives.
+The contribution is that sufficient rank-profile family, a uniform rational
+paid budget, and actual-current inventory calibrations. The finite-difference
+identity and complete alternation of sublinear powers are classical facts;
+no global mathematical novelty or exclusive application priority is claimed.
+No new supplier or selected-frontier change follows without a physical program.

research/higher-order-rank-exchanges/PROOF.md

@@ -0,0 +1,141 @@
+# Higher-order exchanges that improve every rank power
+
+## Exact universal statement
+
+Let n ≥ 2 be an integer, x ≥ 1 and h ≥ 1 be integers, and let 0 < a < 1.
+Define the signed profile on the n+1 ranks x,x+h,…,x+nh by
+
+    d_(x+jh) = (−1)^j binomial(n,j),       0 ≤ j ≤ n.
+
+Positive coefficients are children added; negative coefficients are children
+removed. Then the change in raw recursive bill is strictly negative:
+
+    Σ_{j=0}^n (−1)^j binomial(n,j) (x+jh)^(1−a) < 0.        (1)
+
+The stencil preserves both child count and rank mass. It also annihilates every
+polynomial of degree less than n. A finite nonempty sum of these stencils with
+positive multiplicities again strictly improves the bill for every 0 < a < 1,
+provided the resulting finite child counts are nonnegative. For unchanged
+positive dimension m and positive live normalizer W, multiplying by
+`m^(a−1)/W` proves the same strict comparison of normalized moments.
+This is a sufficient profile theorem, not an implementation of the exchanges.
+
+## Proof for every order
+
+Write q = 1−a and f(t) = t^q for t > 0. The n-th derivative is
+
+    f^(n)(t) = (−1)^(n−1) A_n(a) t^(−(n−1+a)),
+    A_n(a) = a(1−a) ∏_{j=1}^{n−2}(a+j) > 0.
+
+The product is empty for n = 2. Iterating the fundamental theorem of calculus,
+
+    Δ_h^n f(x) = ∫_[0,h]^n f^(n)(x+t_1+…+t_n) dt_1…dt_n.
+
+All evaluation points are positive. The negative of the signed bill in (1)
+is therefore exactly
+
+    S_n(x,h,a) = A_n(a) ∫_[0,h]^n
+                  (x+t_1+…+t_n)^(−(n−1+a)) dt > 0.        (2)
+
+The integrand and coefficient are strictly positive and the cube has positive
+volume. This proves (1). The stencil sum on a polynomial is `(-1)^n Δ_h^n`
+of that polynomial, hence zero for degree less than n; taking degrees 0 and 1
+proves count and rank-mass conservation. Sum the strict inequalities for a
+finite nonempty positive collection, then normalize by a positive factor.
+No implicit gadget, rounding operation or physical implementation enters this
+argument. The iterated finite-difference identity is classical; novelty is not
+claimed for that identity or complete alternation of sublinear powers.
+
+## A uniform rational credit that pays positive costs
+
+Fix rational 0 < ℓ ≤ u < 1, a positive integer B, and n,x,h as above.
+Let `c_s` be the coefficient of z^s in `(1+z+…+z^(B−1))^n`. Put
+
+    A_* = ℓ(1−u) ∏_{j=1}^{n−2}(ℓ+j),
+    R_s = x + (s+n)h/B,
+    L_B = A_* (h/B)^n Σ_{s=0}^{n(B−1)}
+                     c_s / (R_s^(n−1)(1+u(R_s−1))).        (3)
+
+**Theorem (uniform paid replacement).** For every real a ∈ [ℓ,u],
+`S_n(x,h,a) ≥ L_B > 0`. For any collection of these stencils with positive
+integer multiplicities N_i, any complete additional positive-integer-rank
+histogram e_r of rank mass Q = Σ r e_r satisfying
+
+    Q < Σ_i N_i L_(B,i)
+
+leaves the fully charged new moment strictly below the old moment throughout
+[ℓ,u], at unchanged m,W and unchanged other costs. Wherever the old moment
+is below 1, the fully charged new moment is also below 1. Legal recursion
+separately requires all used ranks < m and all relevant halving/compiler rules.
+
+Proof: partition each cube coordinate into B equal intervals. If the sum of
+their zero-based indices is s, the sum argument is at most R_s, and there are
+exactly c_s such cells. For a ∈ [ℓ,u], `A_n(a) ≥ A_*`. For any cell argument
+t ≥ 1 with t ≤ R_s, the concave tangent bound at 1 gives
+
+    t^(n−1+a) ≤ R_s^(n−1) R_s^a
+                 ≤ R_s^(n−1)(1+a(R_s−1))
+                 ≤ R_s^(n−1)(1+u(R_s−1)).
+
+Thus each cell's integrand is at least the reciprocal in (3); multiplying by
+the cell volume `(h/B)^n`, its coefficient and A_* proves the lower bound.
+Every summand in (3) is positive, so the bound is strict above zero.
+The extra raw bill is at most Q because `r^(1−a) ≤ r` for every integer r ≥ 1.
+Subtract Q from the total certified saving and normalize, proving the paid rule.
+Any independently proved uniform upper bound for the actual extra raw cost can
+replace Q; omitted costs cannot.
+
+The implementation computes c_s by polynomial convolution, with only
+`n(B−1)+1` coefficients rather than enumerating B^n cells. The coefficient
+sum is exactly B^n. For nested grids B,2B,4B,… the lower credits are
+nondecreasing: each refined cell has an upper argument no larger than its
+parent, and the rational lower-envelope function in (3) decreases with R.
+This is a proof-preserving way to refine a difficult credit without pricing
+an entire moment root. The theorem holds for every finite order and B; the
+bounded implementation intentionally supports orders 2 through 12 and B ≤ 128.
+
+## Why this adds coverage beyond concave order
+
+For n = 3, x = h = 1, the stencil is
+
+    3 children of rank 2 + 1 of rank 4
+      → 1 child of rank 1 + 3 of rank 3.
+
+Its capped sums `C_k = Σ d_r min(r,k)` for k = 1,…,4 are `(0,−1,1,0)`.
+The positive C_3 means this move fails the all-concave sufficient test used by
+`ranked-pair-verification` and PR3863. Indeed the concave function `min(r,3)`
+gets strictly more expensive. In contrast every power `r^(1−a)`, 0 < a < 1,
+strictly decreases by the third-derivative identity above. This establishes a
+strict extension of that sufficient certificate domain, rather than merely
+another estimate for a move it already accepts.
+
+For n = 4 the move is
+
+    4 children of rank 2 + 4 of rank 4
+      → 1 child of rank 1 + 6 of rank 3 + 1 of rank 5.
+
+Its capped sums are `(0,−1,2,−1,0)`. The same distinction applies. Both moves
+preserve count and mass and use ranks already present in the current histogram.
+
+## Source-bound current pricing targets
+
+Using PR3857's retained complete PR3815 T360 histogram, ℓ = 17/10000,
+u = 18/10000 and B = 16:
+
+| order | raw saving per copy, certified approximately | copies that pay one additional rank-1 child | largest independent batch supported by source counts |
+| --- | ---: | ---: | ---: |
+| 3 | 0.0002856291624839168 | 3,502 | 330,480 |
+| 4 | 0.0001408758746078832 | 7,099 | 82,620 |
+
+All proof-relevant comparisons use the exact rational fractions in RESULT.json.
+The source has 2,349,000 rank-2 and 330,480 rank-4 children, so both batches
+pass the literal aggregate inventory test. These two examples are separate
+comparisons against the original source, not simultaneously claimed batches.
+Both certify a fully charged moment improvement *if* the displayed exchange is
+implemented with that complete extra cost, the same normalizers and ABI.
+The source counts do not establish operand compatibility, legal grouping,
+chronology, stock, frames, dirty restoration, gathering or an actual circuit.
+No new physical supplier, κ, selected-frontier change or full multiplication
+theorem is claimed. The result supplies broader exact sufficient targets for
+that implementation search. The proof is informal; Python replays finite
+identities and rational budgets, not a Lean kernel proof.

research/higher-order-rank-exchanges/README.md

@@ -0,0 +1,95 @@
+# Higher-order rank exchanges beyond concave dominance
+
+**A new sufficient family of power-moment improvements with explicit paid budgets.
+No physical supplier or new κ.**
+
+The previous capped-mass test accepts changes that lower every concave cost.
+It misses some changes that lower every relevant rank power. For example,
+
+```text
+3 rank-2 children + 1 rank-4 child → 1 rank-1 child + 3 rank-3 children
+4 rank-2 children + 4 rank-4 children → 1 rank-1 + 6 rank-3 + 1 rank-5 child
+```
+
+Both strictly lower `Σ r^(1−a)` for **every real 0 < a < 1**, while preserving
+count and rank mass. Their capped sums have both signs: an explicit concave
+cost actually increases. Thus they supply useful sufficient search targets
+outside the earlier test's domain, rather than repricing already accepted moves.
+These are profile transformations; a compatible circuit implementation remains
+separate. Child ranks cannot be changed by relabelling existing operations.
+
+[PROOF.md](PROOF.md) proves the arbitrary-order binomial-stencil theorem by an
+iterated derivative integral. It also proves a uniform rational lower credit,
+using an aggregated cube partition with only `n(B−1)+1` coefficient buckets.
+The credit can pay any complete positive-rank overhead bill with smaller rank
+mass. Grid refinement improves the bound without re-evaluating an entire root.
+The finite-difference identity is classical; no broad novelty claim is made.
+
+On the actual current PR3815/3857 complete histogram, for saving a between
+0.0017 and 0.0018 and a 16-part grid:
+
+| profile exchange | copies that pay one added rank-1 child | aggregate inventory available |
+| --- | ---: | ---: |
+| order 3 | 3,502 | 330,480 copies |
+| order 4 | 7,099 | 82,620 copies |
+
+These are separate sufficient implementation targets, each with one additional
+rank-1 cost explicitly paid. They do not prove grouping, source/consumer
+compatibility, stock, chronology, dirty restoration or any new multiplication
+exponent. No current frontier change or actual speedup is claimed.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3.12 -B research/higher-order-rank-exchanges/verify.py
+python3.12 -B research/higher-order-rank-exchanges/test_certificate.py
+python3.12 -O -B research/higher-order-rank-exchanges/test_certificate.py
+python3.12 -B scripts/research_package.py --package research/higher-order-rank-exchanges
+```
+
+Ordinary replay is read-only and works without Git. It checks the immutable
+current histogram hash, reconstructs the full proposed paid profiles, and
+compares every rational receipt field. Controls use exact independent radical
+bounds in 42 cases, 168 grid bounds, six separately enclosed full-profile power
+gaps and rejecting inventory, overhead, domain and actual CLI corruptions.
+The all-real statement follows from the written proof, not those finite samples.
+No Lean formalization, full native replay or independent human review is claimed.
+
+`certificate.stencil` constructs the signed profile; `certificate.credit` gives
+a rational uniform saving; `certificate.certify` checks aggregate availability,
+legal ranks and the proposed paid histogram. The implementation bounds order
+at 12 and grid subdivisions at 128; the proof has no such finite-order cap.
+A failed quantitative test is inconclusive, since its credit is only sufficient.
+
+## Open next questions
+
+1. Can one actual source-level program implement an order-3 or order-4 exchange
+   with a complete physical bill below the certificate? Start with a compatible
+   set of rank-2/rank-4 operands, freeze the exact caller ABI and check an explicit
+   matrix identity before searching hosting. Counts alone cannot answer this.
+2. Can a different stencil family improve the power bill on an intended saving
+   interval without satisfying all-exponent improvement? Start with an exact
+   signed profile and a separately proved derivative-sign domain; do not infer
+   a theorem from a sampled root or impose this certificate as a universal barrier.
+
+## Credit and comparison
+
+PR3863 (`635fe84596c19016f3d0316a5cf7abbe48285490`) supplies the immediate paid
+concave-profile framework and the retained separate exact-power test oracle.
+The earlier ranked-pair package supplies the min-basis order certificate and its
+formal finite identity. The new higher-order family goes beyond that order;
+it does not claim the finite-difference identity as newly invented mathematics.
+MathProof's `IntegerKappaMomentTransfer20261015` provides the sufficient
+replacement-with-reserve and normalized-admission precedent; no local Lean file
+is imported or counted as a new kernel result.
+
+Current-profile credit stays with ChaloupeMusic/PR3815, hexapode/PR3802,
+dataisfire/PR3734 and the retained native/owner/hosting lineage; PR3857 retained
+that exact histogram and its finite analytic certificate. Preceding rank-pair
+credit includes Avi Eisenberg/PR62, eumemic/PR57, Chafik Boukhalfa/PR60 and
+Dominik Scholz/PR63, with the full inherited notices retained in NOTICE.
+SOURCES.json pins the live scientific provenance. OVERLAP.md states search limits.
+
+Dugongue, with substantial OpenAI Codex assistance. Apache-2.0.