Prove rank exchanges with any rational moment threshold (no new κ)

research/rational-threshold-rank-exchange/README.md

@@ -0,0 +1,197 @@
+# Rank exchanges with an exact rational saving threshold
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration. For every
+rational threshold t in (0,1), there are two nonnegative integer child profiles
+with equal child count and rank mass whose paid power moment improves exactly
+for savings 0<a<t. The exchange reverses direction for t<a<1.
+
+The first example is
+
+```text
+4 rank-1 + 3 rank-8  ->  6 rank-2 + 1 rank-16.
+```
+
+Both sides have seven children and rank mass 28. This exchange improves the
+moment exactly when 0<a<1/2. Throughout 0.003<=a<=0.0031, 127 copies also
+pay for one additional rank-one child. Thus the fully charged comparison is
+
+```text
+{1:508, 8:381}  ->  {1:1, 2:762, 16:127}.
+```
+
+Its new rank mass is one larger, while its raw power bill is strictly smaller
+by at least 1646873/2000000000. This is a sufficient arithmetic allowance,
+not an implemented exchange, a minimum batch size or a new kappa.
+
+This answers Open next question 2 of Dugongue's
+[#3868](https://github.com/CrocSwap/integer-mult-bounds/pull/3868), which asks
+for a different stencil that helps on the intended saving interval without
+improving every exponent. That predecessor supplies all-exponent binomial
+stencils and a paid-overhead framework. Its computations are cited, not
+replayed or re-verified here.
+
+## Exact threshold theorem
+
+For a finite integer profile H, write its raw power bill as
+
+```text
+B_H(a) = sum_r H_r r^(1-a).
+```
+
+Fix integers q>=2 and 1<=s<q. Expand the integer polynomial
+
+```text
+P_qs(x) = (x-1)(x-2)(x^q-2^s) = sum_j c_j x^j.
+```
+
+At rank 2^j, put max(-c_j,0) children in H_old and max(c_j,0)
+children in H_new. Common zero coefficients are omitted. These are finite
+nonnegative integer profiles, with maximum rank 2^(q+2).
+
+Their counts agree because sum c_j=P_qs(1)=0. Their rank masses agree
+because sum 2^j c_j=P_qs(2)=0. For every real 0<a<1, put x=2^(1-a).
+Then 1<x<2 and, exactly,
+
+```text
+B_new(a)-B_old(a) = (x-1)(x-2)(x^q-2^s).
+```
+
+The first two factors have negative product. The last factor is positive
+exactly when q(1-a)>s. Therefore
+
+```text
+B_new(a) < B_old(a)  iff  a < 1-s/q;
+B_new(a) = B_old(a)  iff  a = 1-s/q;
+B_new(a) > B_old(a)  iff  a > 1-s/q.
+```
+
+Every rational t in (0,1) is 1-s/q for such integers. This proves the
+quantified threshold statement. It does not assert a smallest profile for
+that threshold. The algebraic substitution and polynomial factorization are
+elementary background; no literature-wide priority claim is made.
+
+For q=2,s=1, expansion gives P(x)=x^4-3x^3+6x-4, hence the displayed
+seven-child exchange. Its failure at larger a follows from the exact sign
+law, rather than from numerical samples.
+
+## Uniform credit and the fully paid example
+
+Let a range over [3/1000,31/10000], and put x=2^(1-a). The integer
+inequalities
+
+```text
+399^10000 < 2^9969 * 200^10000,
+2^997 * 250^1000 < 499^1000
+```
+
+give 399/200 < x < 499/250 throughout this interval. They follow by raising
+the two positive endpoint comparisons to their denominators; the verifier
+checks both displayed inequalities with integer arithmetic. Monotonicity of
+2^p covers every intermediate real exponent.
+
+The per-copy raw saving is (x-1)(2-x)(x^2-2). Each factor is positive on
+this bracket, so it is at least
+
+```text
+L = (399/200-1)(2-499/250)((399/200)^2-2)
+  = 15760999/2000000000.
+```
+
+Since 127L-1=1646873/2000000000>0, 127 copies fund an additional rank-one
+child, whose raw power bill is exactly one at every a. Expanding those
+copies gives precisely the fully charged profiles above. The old count is
+889 and the new count is 890; their rank masses are 3556 and 3557.
+
+This credit also obeys 126L<1. That only says this particular lower bound
+does not certify 126 copies. It is not a lower bound on the actual optimum.
+More generally, any complete added positive-rank bill with rank mass below
+NL is funded by N copies, since r^(1-a)<=r for every integer r>=1.
+This paid-cost implication is the framework credited to #3868 and #3863.
+
+At unchanged positive ambient rank m and normalizer W, multiplying the
+comparison by m^(a-1)/W preserves its sign. Unchanged other charges cancel.
+Consequently an already admissible complete moment remains below one if
+this replacement is legally implemented with exactly the charged cost.
+Strict child contraction requires m>16 in the first example, and m>2^(q+2)
+for the general family. Other compiler restrictions remain separate.
+
+## Evidence and reproduction
+
+The written factorization proves the universal statement. The standalone
+standard-library verifier constructs all 66 pairs q,s with 2<=q<=12.
+For each it checks count and mass conservation, four rational polynomial
+points, exact reduction modulo x^q-2^s at the threshold, and the raw profile
+signs at every distinct rational power with denominator at most ten.
+Integer bisection encloses each power at 80 binary places. The raw cost
+comparison adds the actual positive and negative profile terms separately,
+without using the factored sign formula to evaluate their costs. There are
+264 polynomial evaluations, 1,994 strict power comparisons and 52 crossing
+cases in that finite domain.
+
+It also checks the two large integer endpoint inequalities, the complete
+overhead accounting and three rational points of the fully charged bill.
+Twelve controls cover six malformed parameter pairs, an omitted rank-sixteen
+term, reversed profiles, the false all-exponent extension, reversed sign,
+the uncertified 126-copy allowance and a false upper power bracket. Every
+check uses an explicit exception and remains active under optimized Python.
+The stdout receipt is generated from actual checks and hashes every package
+file. No receipt is handwritten, and ordinary execution writes no files.
+
+From the repository root, use CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rational-threshold-rank-exchange/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rational-threshold-rank-exchange/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rational-threshold-rank-exchange
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rational-threshold-rank-exchange --check-source-history
+```
+
+Any CPython 3.12 installation may replace the displayed interpreter. Direct
+execution works in a Git-free export of these five files and prints
+`PASS_RATIONAL_THRESHOLD_RANK_EXCHANGE` inside its JSON receipt.
+
+## Scope, sources and credit
+
+Base: canonical main a5df48c55ea806d7952b65acc9c76d878ff09b13, priority
+revision 7. The independent-moment card is explicitly changed to this
+original arithmetic side question. The selected source-binding baseline
+passed as orientation only. It is not a selected operator replay.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144860)
+names this scope. SOURCES.json pins predecessor prose as provenance only;
+no predecessor executable or scientific receipt is imported or rerun.
+
+Credit Dugongue #3868 for the interval-specific question, all-exponent
+comparison and paid allowance; Dugongue #3863 for the preceding concave
+pricing framework; and their retained ranked-pair and moment-transfer
+lineage, including Avi Eisenberg, eumemic, Chafik Boukhalfa, Dominik Scholz
+and MathProof. Their source notices and credit lines remain unchanged.
+
+No current source inventory, compatible operands, native implementation,
+dirty restoration, frame changes, hosting, stock, precision, tape cost or
+complete compiler/consumer has been supplied. All missing costs are unknown.
+The result supplies neither a physical supplier nor a complete multiplication
+theorem, and changes no selected-frontier file. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and predecessor scientific
+replays were outside scope and were not run.
+
+The finite checker uses no recursion, subprocesses, network calls or dynamic
+code generation. Its functions stay below 60 physical lines. The largest
+profile has 15 coefficient slots; its family loop has 66 iterations and each
+root bisection has at most 81. The endpoint checks use fixed exponents at most
+10000. Five package reads are capped at 1 MiB each. Python's dynamic integer
+and Fraction allocation and the bounded rejection dispatcher are documented
+managed-runtime deviations from Power of Ten rules 3 and 9. Warning-strict
+normal/optimized execution and the registered replay are the available
+diagnostics. No real-time or performance claim is made.
+
+## Open next questions
+
+Can an actual producer and consumer implement this seven-child exchange with
+a favorable complete bill? Start with four rank-one and three rank-eight
+operations in one named word. Prove the replacement operator identity and
+its endpoint compatibility before counting copies. No such grouping,
+rank-sixteen recursion, physical circuit or complete paid implementation is
+known from this package. Optimizing the arithmetic batch size cannot supply
+those missing obligations.

research/rational-threshold-rank-exchange/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/charged-rank-dominance/README.md",
+      "usage": "provenance",
+      "git_blob": "037ed3f6c530872ca303c325fdf31d8b48a5d125",
+      "sha256": "789bbbcb443454e839d1a955517827dff20f95cdb95d5aff57a3d5ebd8b85b17"
+    },
+    {
+      "path": "research/higher-order-rank-exchanges/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "5438143f7a04d1ad3ce39a956f6df2edad21705c",
+      "sha256": "00144464017c74da986de73133652b8e0eddeb3bef17868e3ff2e3f68290b70d"
+    },
+    {
+      "path": "research/higher-order-rank-exchanges/README.md",
+      "usage": "provenance",
+      "git_blob": "4db8cdccf9d1b2071e1f32a1ecf8b5c7de646b39",
+      "sha256": "8c4185b42f37cfbce98f5f2ce6fb3d51559fbec48fdc77eeaff412a84ef607dc"
+    }
+  ]
+}

research/rational-threshold-rank-exchange/TASK.json

@@ -0,0 +1,120 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "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": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "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.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Integer rank-profile exchanges with any rational interior saving threshold, plus a uniformly funded rank-one overhead example.",
+  "scope_change_reason": "The donor asks for original work rather than an audit. This answers Dugongue PR3868 Open next question 2 with a new interval-specific stencil, without replaying a predecessor result.",
+  "bottleneck_link": "A moment improvement can hold only near the intended saving. These exact profiles give implementation targets outside all-exponent sufficient exchange families; actual circuits and inventory remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first exact threshold family and a bounded paid-overhead example; do not pursue circuit synthesis or optimize the overhead.",
+  "outcome": "completed",
+  "evidence": "Written all-rational-threshold proof; exact profile, power-bracket, conservation, crossing and paid-overhead checks in verify.py.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can one actual producer/consumer implement the seven-child exchange with a complete added raw bill below its saving?",
+      "why_it_matters": "Only a legal circuit with a complete favorable bill can improve a supplier.",
+      "first_step": "Name an actual set of four rank-one and three rank-eight child operations, then prove an operator replacement with compatible endpoints.",
+      "blocked_by": "No operand grouping, circuit, legal rank-sixteen recursion, hosting, dirty restoration or physical cost bound is supplied."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144860",
+  "overlap": {
+    "entry_open_prs": "Live capped list and complete cached 331-PR body scan; 60 latest handoff comments and active Discussions; account history expanded to 200 PRs.",
+    "distinctive_searches": [
+      "higher-order-rank-exchanges",
+      "rational threshold",
+      "profile stencil",
+      "single crossing",
+      "geometric stencil",
+      "rank-1/rank-8 to rank-2/rank-16"
+    ],
+    "local_note_coverage": "156 of 6918 HEAD note paths materialized; all-main README Git searches supplement the incomplete local cache. No exhaustive novelty claim.",
+    "immediate_precommit_refresh": "Live open PR and handoff refresh, distinctive origin/main README searches, and merged geometric-rank/profile-stencil searches completed before committing. No matching new result found; unpublished work is not covered."
+  },
+  "environment": {
+    "python": "3.12.15",
+    "implementation": "CPython",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  }
+}

research/rational-threshold-rank-exchange/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact new profile factorization, conservation, algebraic crossings, direct integer-root moment signs, paid overhead and negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete verifier with Python assertions disabled."
+    }
+  ]
+}