Prove sharp unit-fee target threshold at rank 288 (no new κ)

research/unit-fee-target-threshold/PROOF.md

@@ -0,0 +1,116 @@
+# The sharp unit-fee target-rank threshold
+
+This scoped proof is produced by Nick Petalas. New material is Apache-2.0.
+The fee-charged partition contract comes from Ali Romman's PR #5769. Strict
+concavity, Jensen's inequality and balancing are classical ingredients.
+
+## Contract and theorem
+
+Fix `p=99/100`. Replace one productive target of integer rank `R` by `k>=2`
+independent productive targets with positive integer ranks `r_1,...,r_k`, whose
+sum is `R`. Charge **one additional paid rank-one recursive child per piece**.
+Keep every other paid child, productive target and fee fixed. Under the raw
+power tariff, the improvement in paid cost minus productive credit is
+
+```text
+G(R;r_1,...,r_k) = sum_i r_i^p - R^p - k.
+```
+
+A positive `G` means a strictly cheaper complete invoice. The `R^p` debit is
+essential. The charge is `k`, including every resulting piece. This theorem
+uses neither `k-1` fees nor a free distinguished piece. A scalar addition is
+not assumed to cost a recursive rank-one child.
+
+**Theorem.** Such a strictly improving partition exists if and only if
+`R>=288`. At the first rank, `(96,96,96)` has improvement strictly between
+`6289/1000000` and `6290/1000000`. Every proper partition with `R<=287` loses.
+In fact its improvement is less than `-4077/1000000`.
+
+This is an arithmetic screening result for the declared fee. It does not assert
+that arbitrary target partitions are physically realizable or useful.
+
+## Rejecting every smaller rank
+
+For any fixed `R,k`, Jensen's inequality gives
+
+```text
+sum_i r_i^p <= k(R/k)^p = R^p k^(1/100),
+G <= J(R,k) = R^p (k^(1/100)-1) - k.
+```
+
+For every `k>=2`, `J(R,k)` strictly increases with positive real `R`.
+Consequently, for `R<=287` and `2<=k<=R`, it suffices to bound `J(287,k)` for
+the complete finite list `k=2,...,287`. No integer partitions are omitted by
+this reduction; it even grants arbitrary positive real piece sizes at each k.
+
+The standalone checker supplies an exact dyadic certificate for each of those
+286 inequalities. Let `D=2^128`. To bound a positive `n^(a/100)`, compute
+
+```text
+L = floor_root_100(n^a D^100),
+U = L if L^100=n^a D^100, else L+1.
+```
+
+The checker verifies `L^100 <= n^a D^100 < (L+1)^100` using integers.
+Thus `L/D <= n^(a/100) <= U/D`. Use `a=99` for `287^p` and `a=1` for each
+`k^(1/100)`. With their respective upper numerators `U_287,U_k`,
+
+```text
+D^2 J(287,k) <= U_287 (U_k-D) - k D^2 < 0.
+```
+
+Every right-hand numerator is present in the generated receipt. The largest
+Jensen upper bound occurs at `k=3` and is strictly negative. Monotonicity proves
+the stated rejection for every smaller integer rank and every proper partition.
+
+The stronger integer margin uses balancing, proved below. The checker also
+encloses the balanced integer partition's profit at rank 287 for every one of
+the same 286 piece counts. The largest upper bound occurs at `k=3`, with parts
+`(95,96,96)`, and is below `-4077/1000000`. Balanced profit strictly increases
+with R at fixed k, as shown below, so this integer margin applies to every
+proper partition at every smaller rank too. Jensen's real-size relaxation is
+used only for the sign, not for this stronger integer margin.
+
+## Attainment and all larger ranks
+
+At `R=288`, take three rank-96 pieces. The exact root enclosures above, with
+`a=99`, give
+
+```text
+6289/1000000 < 3*96^p - 288^p - 3 < 6290/1000000.
+```
+
+All comparisons are integer cross-multiplications. This proves attainment at
+288 independently of any floating-point approximation or source executable.
+
+For completeness, the witness extends to every larger rank. For fixed k,
+strict concavity implies that a maximizing integer partition has parts differing
+by at most one. Indeed, if `b>=a+2`, replace `(a,b)` by `(a+1,b-1)`.
+The decreasing increments of `x^p` make the credit strictly larger.
+
+Write `B_k(R)` for the balanced partition's improvement. When `R` increases by
+one, increase a smallest piece `q=floor(R/k)` by one. Then
+
+```text
+B_k(R+1)-B_k(R) = ((q+1)^p-q^p) - ((R+1)^p-R^p) > 0,
+```
+
+since `q<R` and `x^p` has strictly decreasing increments. Apply this with
+`k=3` for every integer `R>=288`. The positive rank-288 witness and this strict
+monotonicity establish existence at every larger rank. No additional search or
+new supplier premise is used.
+
+## What the executable proves
+
+The written argument reduces the infinite claim to 286 root-enclosed Jensen
+inequalities and one positive witness. `verify.py` checks those inequalities
+and rational margins with integer arithmetic. It also checks the balancing
+lemma on every proper sorted integer partition of ranks 2 through 24, uses an
+independently implemented bisection oracle for eleven decisive powers, and
+rejects forged certificates and invalid partitions. These finite checks
+corroborate the written proof; they are not proof-kernel verification.
+
+The receipt is generated on stdout and binds every package file by SHA256.
+No receipt is hand-written or stored as an assumed mathematical input. Normal
+and optimized modes must emit identical receipts. A supplied `--check-receipt`
+file is checked against a fresh computation and fresh source hashes.

research/unit-fee-target-threshold/README.md

@@ -0,0 +1,92 @@
+# First profitable target rank with one paid unit per piece
+
+This contribution is produced by Nick Petalas. Claim type: **scoped proof with
+exact finite corroboration**. It does not improve kappa or change the selected
+frontier. New material is Apache-2.0.
+
+At power exponent `99/100`, replacing one rank-R productive target by a proper
+positive integer partition, while adding one paid rank-one recursive child for
+each resulting target, can improve the complete signed bill **exactly when
+R>=288**. The first witness is `288=96+96+96`.
+
+```text
+profit = sum_i r_i^(99/100) - R^(99/100) - number_of_pieces
+R <= 287: every proper partition has profit < -0.004077
+R  = 288: (96,96,96) has 0.006289 < profit < 0.006290
+```
+
+[PROOF.md](PROOF.md) reduces the all-partition lower bound to 286 explicit
+Jensen inequalities at rank 287. Integer-root enclosures certify each one and
+the positive witness. Balancing and strictly decreasing power increments extend
+the witness to all larger ranks. The proof has no piece-count or menu limit.
+
+This specializes Ali Romman's [PR #5769](https://github.com/CrocSwap/integer-mult-bounds/pull/5769)
+complete fee-charged target-partition contract. That finite optimizer caps the
+replaced rank at 256. The present unit-fee model has no profitable rank inside
+that cap at this exponent; the first opportunity is 288. This is a new arithmetic
+screen, rather than a replay or audit of the optimizer. The result tells a
+contributor using this fee model to seek lower or shared fees before searching
+small target partitions. It grants independent targets and adds no other fees,
+so extra nonnegative costs can only strengthen the rejection below 288.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/unit-fee-target-threshold
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/unit-fee-target-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/unit-fee-target-threshold/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/unit-fee-target-threshold --check-source-history
+```
+
+Another CPython 3.12 interpreter can replace the absolute path. Expected marker
+in the JSON stdout receipt: `PASS_UNIT_FEE_TARGET_THRESHOLD`. The receipt
+contains all 286 dyadic rejection bounds, the witness bounds, finite coverage
+counts and SHA256 of every package file. Redirect stdout outside the checkout
+if retaining it. `verify.py --check-receipt PATH` recomputes the result and checks
+both the supplied receipt and the current source hashes. Replay writes no files.
+
+## Scope and limitations
+
+The exponent is fixed at 99/100, a one-percent raw power-saving screen. It is
+not the selected supplier exponent or the nine-row outer budget. One recursive
+rank-one child per resulting piece is an explicit additional-fee hypothesis;
+ordinary scalar ADD charges and shared fees are different models. The result
+does not exclude no-fee target refinements, including selected #5599, or any
+construction with paid removals, other productive credits or changed boundaries.
+
+Independent useful targets, native/source maps, chronological delivery, dirty
+restoration, owned lifetimes, complete compiler/precision/tape/outer admission
+and the full multiplication theorem are unproved here. No predecessor verifier,
+selected cold replay, Lean proof or physical supplier was run. Independent human
+and formal proof-kernel review are unclaimed. The five selected framework
+assumptions remain.
+
+## Open next questions
+
+- At the actual source-bound supplier exponent, what is the first profitable
+  rank under the same fee? Start with balanced partitions and certify the two
+  adjacent rank signs. This would tailor the screen to a real caller; the
+  correct tariff and exponent must first be pinned.
+- Can a real helper split share one paid route across its targets, rather than
+  paying one child per piece? Start with one literal helper/cut and derive its
+  complete invoice. Independent target realization and dirty restoration are
+  the blockers; this arithmetic theorem supplies neither.
+
+## Credit and provenance
+
+Credit Ali Romman #5769, head `a869fed1b3ab00ffcddd3791c579c408594325f8`,
+for the fee-charged partition definition, original-target debit and finite
+optimizer. Credit classical concavity, Jensen and integer balancing, and the
+signed-invoice framework, mightyOil's T16 audit and their retained predecessors.
+[SOURCES.json](SOURCES.json) records exact reference-document bytes and the
+base catalogue/selected-record pins. The source document is reference-only;
+this self-contained theorem has no unmerged runtime or Git-object dependency.
+
+Related work includes Charan . #5702's thirteen fixed H9 helpers funding one
+shared extra child, Arham Tahir #1605 and Aaron Wang #3110's paid-child reblocking
+contracts, and Ali Romman #5341's paid-increment fragmentation. Those models and
+quantities differ; their reported numbers are not replayed as this deliverable.
+The account's #5901 concerns incomparable invoice pools, rather than existence
+of an improving unit-fee partition. It supplies no premise used here.

research/unit-fee-target-threshold/SOURCES.json

@@ -0,0 +1,29 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ],
+  "reference_only": [
+    {
+      "pr": 5769,
+      "head": "a869fed1b3ab00ffcddd3791c579c408594325f8",
+      "path": "docs/research/target-partition-optimization.md",
+      "sha256": "3a8dc58083cb4d9d8b0f92764c93f2a8dfcd42b703565d944be63a48df8446a9",
+      "git_blob": "a1d612450907ec34bf99747929da04276aac2e80",
+      "url": "https://github.com/aliromman/integer-mult-bounds/blob/a869fed1b3ab00ffcddd3791c579c408594325f8/docs/research/target-partition-optimization.md",
+      "usage": "Definition/motivation citation only. No runtime or Git-object dependency."
+    }
+  ]
+}

research/unit-fee-target-threshold/TASK.json

@@ -0,0 +1,123 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp first profitable integer target rank at exponent 99/100 with one additional paid rank-one child per resulting piece, over every positive integer partition.",
+  "scope_change_reason": "Specialize the complete fee-charged target-partition contract of Ali Romman PR5769 to a uniform explicit fee. This arithmetic screen precedes, and does not supply, a physical decoder or supplier.",
+  "bottleneck_link": "A complete target refinement must beat all added recursive charges. This theorem identifies the first rank that can do so under the declared one-unit-per-piece fee; the exponent is a target one-percent raw screen, not selected supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first exact threshold with a complete all-partition rejection below it and a positive witness at it. No wider exponent or mechanism search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md all-rank proof; 286 exact Jensen and integer-balanced rejection bounds; positive rank-288 witness; 7313 complete small proper integer partitions; eleven independent bisection checks; eight forged certificates and five invalid partitions rejected. Warning-strict normal and optimized receipts agree.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the first profitable rank at a pinned actual supplier exponent under the same fee?",
+      "why_it_matters": "This would specialize the arithmetic screen to a real complete caller bill.",
+      "first_step": "Use balanced fixed-count partitions and certify the two adjacent rank signs.",
+      "blocked_by": "The correct source tariff and supplier exponent must be pinned first."
+    },
+    {
+      "question": "Can a literal helper split share paid routes across its independent targets?",
+      "why_it_matters": "Shared or lower fees change this scoped threshold.",
+      "first_step": "Choose one source helper and causal cut; derive all target credits and paid routes.",
+      "blocked_by": "Independent useful target delivery and dirty restoration are not realized here."
+    }
+  ],
+  "predecessor": {
+    "pr": 5769,
+    "head": "a869fed1b3ab00ffcddd3791c579c408594325f8",
+    "author": "Ali Romman",
+    "usage": "Reference-only fee-charged partition definition; no source executable or result is replayed."
+  },
+  "scope_key": "target-partition/unit-per-piece-fee/exponent-99-100/all-positive-integer-ranks",
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216793"
+  },
+  "engineering": {
+    "playbook": "autonomous local run",
+    "principles": [
+      "Build the Lever: standalone verifier emits a source-bound receipt.",
+      "Prove It Works: integer endpoint powers check every bound; normal and optimized replay.",
+      "Power of Ten: no recursion; fixed domains, bounded root iterations and enumeration; functions below 60 lines."
+    ],
+    "deviations": [
+      "Python integer/JSON allocation is runtime-managed. Ranks are at most 288; root radicands are below 15000 bits, table size is 288 and small-partition depth is at most 24. No fixed-allocation runtime claim.",
+      "No Python static analyzer is configured for this package. Warning-strict normal and optimized execution plus AST and function-size inspection are used."
+    ]
+  },
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  },
+  "overlap": {
+    "open_prs": {
+      "fetched_at": "2026-10-27T12:31:48.049401+00:00",
+      "complete_pagination": true,
+      "records": 459
+    },
+    "discussions": {
+      "fetched_at": "2026-10-27T12:32:49.937283+00:00",
+      "complete_pagination": true,
+      "records": 5400
+    },
+    "limits": "Sparse helper searched 184 local notes of 7845 HEAD note paths. Distinctive searches across all origin/main research README blobs and live merged PR searches supplemented that incomplete local corpus. No keyword search proves novelty. PR5769 reference and related PR5702/5341/3110/1605/1888 bodies read.",
+    "canonical_main": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+    "refreshed_before_publication": true
+  }
+}