From f1e50cbb9accabbece976a2a07c509966b696afb Mon Sep 17 00:00:00 2001 From: Dugongue <49054532+Dugongue@users.noreply.github.com> Date: Sun, 18 Oct 2026 23:47:06 +0000 Subject: [PATCH] Certify sufficient higher-order rank exchanges and paid budgets --- .../higher-order-rank-exchanges/.gitignore | 2 + .../higher-order-rank-exchanges/INPUTS.json | 3 + research/higher-order-rank-exchanges/NOTICE | 18 +++ .../higher-order-rank-exchanges/OVERLAP.md | 34 +++++ research/higher-order-rank-exchanges/PROOF.md | 141 ++++++++++++++++++ .../higher-order-rank-exchanges/README.md | 95 ++++++++++++ .../higher-order-rank-exchanges/RESULT.json | 92 ++++++++++++ .../higher-order-rank-exchanges/SOURCES.json | 63 ++++++++ .../higher-order-rank-exchanges/TASK.json | 77 ++++++++++ .../VALIDATION.json | 16 ++ .../higher-order-rank-exchanges/VERIFY.json | 37 +++++ .../certificate.py | 71 +++++++++ .../inputs/current-profile.json | 1 + .../higher-order-rank-exchanges/oracle.py | 32 ++++ .../test_certificate.py | 72 +++++++++ .../higher-order-rank-exchanges/verify.py | 33 ++++ 16 files changed, 787 insertions(+) create mode 100644 research/higher-order-rank-exchanges/.gitignore create mode 100644 research/higher-order-rank-exchanges/INPUTS.json create mode 100644 research/higher-order-rank-exchanges/NOTICE create mode 100644 research/higher-order-rank-exchanges/OVERLAP.md create mode 100644 research/higher-order-rank-exchanges/PROOF.md create mode 100644 research/higher-order-rank-exchanges/README.md create mode 100644 research/higher-order-rank-exchanges/RESULT.json create mode 100644 research/higher-order-rank-exchanges/SOURCES.json create mode 100644 research/higher-order-rank-exchanges/TASK.json create mode 100644 research/higher-order-rank-exchanges/VALIDATION.json create mode 100644 research/higher-order-rank-exchanges/VERIFY.json create mode 100644 research/higher-order-rank-exchanges/certificate.py create mode 100644 research/higher-order-rank-exchanges/inputs/current-profile.json create mode 100644 research/higher-order-rank-exchanges/oracle.py create mode 100644 research/higher-order-rank-exchanges/test_certificate.py create mode 100644 research/higher-order-rank-exchanges/verify.py diff --git a/research/higher-order-rank-exchanges/.gitignore b/research/higher-order-rank-exchanges/.gitignore new file mode 100644 index 0000000000..3673a99c42 --- /dev/null +++ b/research/higher-order-rank-exchanges/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/higher-order-rank-exchanges/INPUTS.json b/research/higher-order-rank-exchanges/INPUTS.json new file mode 100644 index 0000000000..f44942787e --- /dev/null +++ b/research/higher-order-rank-exchanges/INPUTS.json @@ -0,0 +1,3 @@ +{ + "inputs/current-profile.json": "9686df0d8e710c2e94aef3887f4bf130a05b64215faeae702cccb59e95a469d5" +} diff --git a/research/higher-order-rank-exchanges/NOTICE b/research/higher-order-rank-exchanges/NOTICE new file mode 100644 index 0000000000..61d285f805 --- /dev/null +++ b/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. diff --git a/research/higher-order-rank-exchanges/OVERLAP.md b/research/higher-order-rank-exchanges/OVERLAP.md new file mode 100644 index 0000000000..727c868f4c --- /dev/null +++ b/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. diff --git a/research/higher-order-rank-exchanges/PROOF.md b/research/higher-order-rank-exchanges/PROOF.md new file mode 100644 index 0000000000..5438143f7a --- /dev/null +++ b/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. diff --git a/research/higher-order-rank-exchanges/README.md b/research/higher-order-rank-exchanges/README.md new file mode 100644 index 0000000000..4db8cdccf9 --- /dev/null +++ b/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. diff --git a/research/higher-order-rank-exchanges/RESULT.json b/research/higher-order-rank-exchanges/RESULT.json new file mode 100644 index 0000000000..bf6725d0c0 --- /dev/null +++ b/research/higher-order-rank-exchanges/RESULT.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "status": "PASS_HIGHER_ORDER_RANK_EXCHANGES", + "scope": "Sufficient power-profile and paid-cost comparison, not a circuit or new kappa.", + "current_profile_head": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "examples": [ + { + "saving_interval": [ + "17/10000", + "9/5000" + ], + "boxes": 16, + "moves": [ + { + "order": 3, + "start": 1, + "step": 1, + "copies": 3502, + "signed_stencil": { + "1": 1, + "2": -3, + "3": 3, + "4": -1 + }, + "capped_sums": { + "1": 0, + "2": -1, + "3": 1, + "4": 0 + }, + "unit_raw_credit": "36775345939977274800986997676964321539302763439700272777718720478475206351507700723102949100216286922215778977102715133587872180584458708217527415897706465272349533103861029925411702232184624928572280117274256939169/128752070062341838180414169976108576833004925346777366680977680968703645357672037347674717957081027093894307616038912460355937706428856103086497632173443021434801465883165430640630554957071603183527146688512000000000000" + } + ], + "total_raw_credit": "3787860631817659304501660760727325118548184634289128096105028209282946254205293174479603757322277552988225234641579658759550834600199246946405323837463765923052001909697686082317405329915016367642944852079248464734407/3786825590068877593541593234591428730382497804316981372969931793197166039931530510225726998737677267467479635765850366481056991365554591267249930358042441806905925467151924430606781028149164799515504314368000000000000", + "overhead_rank_mass": 1, + "net_raw_credit": "1035041748781710960067526135896388165686829972146723135096416085780214273762664253876758584600285520745598875729292278493843234644655679155393479421324116146076442545761651710624301765851568127440537711248464734407/3786825590068877593541593234591428730382497804316981372969931793197166039931530510225726998737677267467479635765850366481056991365554591267249930358042441806905925467151924430606781028149164799515504314368000000000000", + "charged_profile": { + "1": 7993343, + "2": 2338494, + "3": 759594, + "4": 326978, + "5": 69120, + "8": 25920, + "48": 137952 + }, + "largest_inventory_feasible_copies": 330480 + }, + { + "saving_interval": [ + "17/10000", + "9/5000" + ], + "boxes": 16, + "moves": [ + { + "order": 4, + "start": 1, + "step": 1, + "copies": 7099, + "signed_stencil": { + "1": 1, + "2": -4, + "3": 6, + "4": -4, + "5": 1 + }, + "capped_sums": { + "1": 0, + "2": -1, + "3": 2, + "4": -1, + "5": 0 + }, + "unit_raw_credit": "37681280082020139280148031670936035941854423555370740386733104417535141744871586884868808947067865691444590445868477546711779701088437405655206048038581827041993488046970653056183537011997557700412281434559852033461414843357111373493992240260352866015986016978536685960103804689510310477783481215159351443874879917/267478588416242272536418790040601416629485025088664340677922740304026280925640767837326611976006180853630594168933746873248029679506455380371416451154372275805321591031070503003473616455575960014600832717619415240554385120561614256386942668109457938249578215708261844178765159472076199233281868496896000000000000000000" + } + ], + "total_raw_credit": "8629013138782611895153899252644352230684662994179899548561880911615547459575593396634957248878541243340811212103881358196997551549252165895042185000835238392616508762756279549866029975747440713394412448514206115662663999128778504530124223019620806317660797888084901084863771273897861099412417198271491480647347500993/8628341561814266856013509356148432794499516938344010989610410977549234868569057027010535870193747769471954650610766028169291279984079205818432788746915234703397470678421629129144310208244385806922607507019981136792076939372955298593127182842240578653212200506718124005766618047486329007525221564416000000000000000000", + "overhead_rank_mass": 1, + "net_raw_credit": "671576968345039140389896495919436185146055835888558951469934066312591006536369624421378684793473868856561493115330027706271565172960076609396253920003689219038084334650420721719767503054906471804941494224978870587059755823205936997040177380227664448597381366777079097153226411532091887195633855491480647347500993/8628341561814266856013509356148432794499516938344010989610410977549234868569057027010535870193747769471954650610766028169291279984079205818432788746915234703397470678421629129144310208244385806922607507019981136792076939372955298593127182842240578653212200506718124005766618047486329007525221564416000000000000000000", + "charged_profile": { + "1": 7996940, + "2": 2320604, + "3": 791682, + "4": 302084, + "5": 76219, + "8": 25920, + "48": 137952 + }, + "largest_inventory_feasible_copies": 82620 + } + ] +} diff --git a/research/higher-order-rank-exchanges/SOURCES.json b/research/higher-order-rank-exchanges/SOURCES.json new file mode 100644 index 0000000000..c4370aa364 --- /dev/null +++ b/research/higher-order-rank-exchanges/SOURCES.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "research/ranked-pair-verification/concave_dominance.py", + "usage": "provenance", + "git_blob": "97cd3ea3a0fcb1adbb8886578179d26c859fda78", + "sha256": "ab3b45820b2e59a173444739887c438620a1c7cedf9909122fbd049b7078a709" + }, + { + "path": "research/outer-bernstein-certificate/README.md", + "usage": "provenance", + "git_blob": "beee81cbae65975bd02408a921c8461db5c30a0b", + "sha256": "964f4cb1314485853581bbd5e12815c73e2f336676c3f64d88fde68cd11f1880" + }, + { + "path": "research/coded-helper-early-end8/binomial.py", + "usage": "provenance", + "git_blob": "70ab18c465e136d39b7f7e73f8b5781b78d53c48", + "sha256": "8fa965f901947a1b3c9d63bda466093c1fb3257a22c443e73a4d21f06620ef3c" + } + ], + "external_public_inputs": [ + { + "local_path": "inputs/current-profile.json", + "source_pr": 3857, + "source_head": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "source_path": "research/staged544-certified-endpoint/vendor/staged544-clock-ceiling/inputs/PROFILE.json", + "sha256": "9686df0d8e710c2e94aef3887f4bf130a05b64215faeae702cccb59e95a469d5", + "coverage": "Byte-identical histogram retained from public PR3857; source hash checked by standalone verifier; no foreign Git dependency." + } + ], + "reused_oracle": { + "source_pr": 3863, + "head": "635fe84596c19016f3d0316a5cf7abbe48285490", + "path": "research/charged-rank-dominance/test_certificate.py", + "source_sha256": "1dbd32cb4c6fec989d65411b06b152250bfc6647e6445395079992c748e46fe4", + "local_path": "oracle.py", + "extraction": "log_interval, raw_power_interval and gap_interval functions, with necessary imports; no primary credit arithmetic reused." + }, + "mathproof_precedent": { + "module": "Mathproof.Computability.IntegerKappaMomentTransfer20261015", + "sha256": "68e89786008dd3f222632920a00eafd6fc64661e08548c5325a3daa4ba964522", + "theorems": [ + "admission_with_reserve", + "normalized_admission" + ], + "scope": "Discovery framework only; no imported Lean or new formal result." + } +} diff --git a/research/higher-order-rank-exchanges/TASK.json b/research/higher-order-rank-exchanges/TASK.json new file mode 100644 index 0000000000..0a3ecfcefe --- /dev/null +++ b/research/higher-order-rank-exchanges/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "changed", + "scope_change_reason": "The donor requests another short positive mathematics contribution. PR3863 covers paid concave-order moves; this result admits universally power-improving higher-order stencils whose capped sums have both signs, with a quantitative paid-cost certificate. No root repricing or physical realization is claimed.", + "actual_scope": "All-order sufficient power-profile exchange theorem and rational uniform paid credits outside all-concave dominance.", + "bottleneck_link": "Implementation searches need sufficient fully priced targets that are not silently excluded by a narrower concave-order screen.", + "budget_minutes": 12, + "author": "Dugongue", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, implementation, cross-checking and packaging; no independent human review.", + "outcome": "completed", + "evidence": "Complete informal arbitrary-order proof; current-source inventory and paid profiles; independent exact radicals and full-profile power enclosures; rejecting controls.", + "stop_rule": "Finish the all-order theorem, rational certificate, two current-source targets and bounded arithmetic/source checks. Do not launch a physical search or publish an exact new kappa.", + "upstream_checkpoint": { + "utc": "2026-10-18T23:45:10.589Z", + "main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6 + }, + "open_questions": [ + { + "question": "Can an actual compatible rank-2/rank-4 operator group realize an order-3 exchange below the certified overhead?", + "why_it_matters": "Would turn a sufficient profile target into an actual improved paid construction.", + "first_step": "Freeze operands and ABI, prove an explicit matrix identity and then price gathering, cleanup and chronology.", + "blocked_by": "No compatible circuit realization is supplied by histogram counts." + }, + { + "question": "Which signed profile exchanges admit an intended-interval proof without all-exponent improvement?", + "why_it_matters": "Could further broaden useful sufficient search certificates.", + "first_step": "Freeze a signed profile and rigorously bound its derivative-sign domain.", + "blocked_by": "No specific source-compatible interval-only exchange is proposed here." + } + ] +} diff --git a/research/higher-order-rank-exchanges/VALIDATION.json b/research/higher-order-rank-exchanges/VALIDATION.json new file mode 100644 index 0000000000..a0c6183cfb --- /dev/null +++ b/research/higher-order-rank-exchanges/VALIDATION.json @@ -0,0 +1,16 @@ +{ + "status": "PASS", + "python": "3.12.10", + "registered_command": "python3.12 -B scripts/research_package.py --package research/higher-order-rank-exchanges", + "coverage": [ + "Both exact current-profile signed changes and paid overhead budgets", + "Count/rank mass and lower polynomial-moment cancellations", + "42 exact radical cases and 168 rational grid bounds/refinements", + "Six independently enclosed current full-profile real-power differences", + "Positive capped sums and explicit concave cost increase controls", + "Insufficient source inventory, excessive paid overhead, illegal ranks and malformed domain rejects", + "Actual read-only Git-free CLI plus immutable-input/result corruption rejects", + "Arithmetic/control suite under Python -O" + ], + "proof_scope": "Written elementary all-order and all-real-interval proof; finite checks corroborate implementation. No Lean proof, physical realization or new kappa." +} diff --git a/research/higher-order-rank-exchanges/VERIFY.json b/research/higher-order-rank-exchanges/VERIFY.json new file mode 100644 index 0000000000..15bf0f248a --- /dev/null +++ b/research/higher-order-rank-exchanges/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Reconstruct both current complete paid profiles and exact higher-order rational certificates." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_certificate.py" + ], + "timeout_seconds": 60, + "checks": "Independent radical and full-profile power bounds, conservation/refinement identities and semantic controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/test_certificate.py" + ], + "timeout_seconds": 60, + "checks": "Same sufficient arithmetic and rejecting controls with assertions disabled." + } + ] +} diff --git a/research/higher-order-rank-exchanges/certificate.py b/research/higher-order-rank-exchanges/certificate.py new file mode 100644 index 0000000000..9e9f3366fd --- /dev/null +++ b/research/higher-order-rank-exchanges/certificate.py @@ -0,0 +1,71 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Sufficient higher-order power-profile exchanges and paid interval credits. +Dugongue with substantial OpenAI Codex assistance. See PROOF.md. +""" +from fractions import Fraction as F +from math import comb, prod + +def need(ok,message): + if not ok:raise ValueError(message) + +def stencil(order,start=1,step=1): + need(type(order) is int and 2<=order<=12,'implementation order domain 2..12') + need(type(start) is int and start>=1 and type(step) is int and step>=1,'positive integer grid') + return {start+j*step:(-1)**j*comb(order,j) for j in range(order+1)} + +def sum_distribution(order,boxes): + need(type(order) is int and 2<=order<=12,'order') + need(type(boxes) is int and 1<=boxes<=128,'bounded grid 1..128') + coefficients=[1] + for _ in range(order): + out=[0]*(len(coefficients)+boxes-1) + for i,c in enumerate(coefficients): + for j in range(boxes):out[i+j]+=c + coefficients=out + need(sum(coefficients)==boxes**order,'cube-cell count') + return coefficients + +def credit(order,start,step,lower,upper,boxes=16): + stencil(order,start,step) + need(type(lower) is F and type(upper) is F and 01,'dimension') + need(type(profile) is dict and profile and all(type(r) is int and 0=0 for r,n in profile.items()),'legal finite profile') + need(type(moves) is list and moves,'nonempty positive stencil list') + new=dict(profile);total=F(0);records=[] + for move in moves: + need(type(move) is dict and set(move)=={'order','start','step','copies'},'exact move schema') + n,x,h,copies=(move[k] for k in ('order','start','step','copies')) + need(type(copies) is int and copies>0,'positive integer copies') + d=stencil(n,x,h) + need(max(d)=0 for v in new.values()),'insufficient aggregate source inventory') + need(sum(r*n for r,n in new.items())==sum(r*n for r,n in profile.items()),'aggregate rank mass') + extra={} if overhead is None else overhead + need(type(extra) is dict and all(type(r) is int and 0=0 for r,n in extra.items()),'overhead profile') + Q=sum(r*n for r,n in extra.items()) + need(Q= 2**(k+1): k+=1 + def unit(a,b): + t=F(a-b,a+b);N=48 + s=2*sum((t**(2*j+1)/F(2*j+1) for j in range(N)),F(0)) + return s,s+2*t**(2*N+1)/(F(2*N+1)*(1-t*t)) + lo,hi=unit(n,2**k);l2,u2=unit(2,1) + return lo+k*l2,hi+k*u2 + +def raw_power_interval(r,a): + if r==0:return F(0),F(0) + lo,hi=log_interval(r);lo*=a;hi*=a + need(0<=lo<=hi=0 else u);hi+=d*(u if d>=0 else l) + return lo,hi + diff --git a/research/higher-order-rank-exchanges/test_certificate.py b/research/higher-order-rank-exchanges/test_certificate.py new file mode 100644 index 0000000000..9f2bc4e24f --- /dev/null +++ b/research/higher-order-rank-exchanges/test_certificate.py @@ -0,0 +1,72 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact radical/power checks and rejecting controls.""" +from fractions import Fraction as F +from math import isqrt +from pathlib import Path +import json,subprocess,sys,tempfile,shutil +from certificate import stencil,credit,certify,capped_sums,need +from oracle import gap_interval +from verify import result +ROOT=Path(__file__).resolve().parent + +def reject(fn): + try:fn() + except ValueError:return + raise RuntimeError('invalid input accepted') + +def main(): + data=result();S=10**50;cases=0;refinements=0 + for order in range(2,9): + for start in range(1,4): + for step in (1,2): + d=stencil(order,start,step) + for power in range(order): + need(sum(v*r**power for r,v in d.items())==0,'lower polynomial moments') + gap=F(0) + for r,v in d.items(): + z=isqrt(r*S*S);lo,hi=F(z,S),F(z+1,S) + gap+= -v*(hi if v>0 else lo) + previous=F(0) + for boxes in (1,2,4,8): + L=credit(order,start,step,F(1,2),F(1,2),boxes) + need(0=previous,'nested lower-grid refinement') + previous=L;refinements+=1 + cases+=1 + source={int(r):n for r,n in json.loads((ROOT/'inputs/current-profile.json').read_text()).items()} + for row in data['examples']: + move=row['moves'][0];n=move['order'];N=move['copies'] + size=max(source)+1;old=[source.get(r,0) for r in range(size)];new=list(old) + for r,v in stencil(n).items():new[r]+=N*v + for a in (F(17,10000),F(7,4000),F(18,10000)): + lo,hi=gap_interval(old,new,a) + need(lo>F(row['total_raw_credit'])>1,'independent actual paid-power sign') + # A positive capped sum gives an explicit concave cost that gets worse. + caps=capped_sums(stencil(n));k=next(k for k,c in caps.items() if c>0) + need(sum(v*min(r,k) for r,v in stencil(n).items())>0,'outside the all-concave cone') + over=row['largest_inventory_feasible_copies']+1 + reject(lambda:certify(source,73,[{'order':n,'start':1,'step':1,'copies':over}],F(17,10000),F(18,10000))) + reject(lambda:certify(source,73,[{'order':n,'start':1,'step':1,'copies':N}],F(17,10000),F(18,10000),{1:2})) + for n in (1,13,True):reject(lambda:stencil(n)) + reject(lambda:stencil(3,0,1));reject(lambda:stencil(3,1,0)) + reject(lambda:credit(3,1,1,F(0),F(1,2))) + reject(lambda:credit(3,1,1,F(1,2),F(1))) + reject(lambda:credit(3,1,1,F(3,4),F(1,4))) + reject(lambda:credit(3,1,1,F(1,4),F(1,2),0)) + reject(lambda:certify(source,73,[],F(1,4),F(1,2))) + reject(lambda:certify(source,73,[{'order':3,'start':1,'step':1,'copies':-1}],F(1,4),F(1,2))) + reject(lambda:certify(source,73,[{'order':3,'start':71,'step':1,'copies':1}],F(1,4),F(1,2))) + reject(lambda:certify(source,73,[{'order':3,'start':1,'step':1,'copies':1}],F(1,4),F(1,2),{0:1})) + # Read-only exported CLI and proof-relevant input/result corruption controls. + with tempfile.TemporaryDirectory() as temporary: + copied=Path(temporary)/'package';shutil.copytree(ROOT,copied,ignore=shutil.ignore_patterns('__pycache__')) + command=[sys.executable,'-B',str(copied/'verify.py')] + need(subprocess.run(command,capture_output=True).returncode==0,'standalone positive CLI') + target=copied/'inputs/current-profile.json';raw=target.read_bytes();target.write_bytes(raw+b' ') + need(subprocess.run(command,capture_output=True).returncode!=0,'changed input accepted');target.write_bytes(raw) + target=copied/'RESULT.json';value=json.loads(target.read_text());value['examples'][0]['net_raw_credit']='100' + target.write_text(json.dumps(value),encoding='utf-8') + need(subprocess.run(command,capture_output=True).returncode!=0,'false paid credit accepted') + print('PASS_HIGHER_ORDER_CONTROLS',cases,'radical cases,',refinements,'grid bounds, 6 exact-power signs, inventory/overhead/domain and CLI controls') + +if __name__=='__main__':main() diff --git a/research/higher-order-rank-exchanges/verify.py b/research/higher-order-rank-exchanges/verify.py new file mode 100644 index 0000000000..25a5cf86b2 --- /dev/null +++ b/research/higher-order-rank-exchanges/verify.py @@ -0,0 +1,33 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Read-only, Git-free source-bound higher-order exchange certificate.""" +from pathlib import Path +from fractions import Fraction as F +import hashlib,json +from certificate import certify,credit,need,stencil +ROOT=Path(__file__).resolve().parent + +def result(): + pins=json.loads((ROOT/'INPUTS.json').read_text(encoding='utf-8')) + for name,digest in pins.items(): + need(hashlib.sha256((ROOT/name).read_bytes()).hexdigest()==digest,'source hash '+name) + profile={int(r):n for r,n in json.loads((ROOT/'inputs/current-profile.json').read_text()).items()} + lower,upper=F(17,10000),F(18,10000) + rows=[] + for order in (3,4): + L=credit(order,1,1,lower,upper,16) + copies=L.denominator//L.numerator+1 + row=certify(profile,73,[{'order':order,'start':1,'step':1,'copies':copies}], + lower,upper,{1:1},16) + caps=row['moves'][0]['capped_sums'] + need(any(v>0 for v in caps.values()) and any(v<0 for v in caps.values()), + 'example must lie outside all-concave capped-mass dominance') + row['largest_inventory_feasible_copies']=min(profile.get(r,0)//(-v) + for r,v in stencil(order).items() if v<0) + rows.append(row) + return {'schema_version':1,'status':'PASS_HIGHER_ORDER_RANK_EXCHANGES', + 'scope':'Sufficient power-profile and paid-cost comparison, not a circuit or new kappa.', + 'current_profile_head':'ef4315b8caa605e47a2515004845eb2d2ed71a86','examples':rows} + +if __name__=='__main__': + actual=result();need(actual==json.loads((ROOT/'RESULT.json').read_text(encoding='utf-8')),'result drift') + print(actual['status'])