diff --git a/research/uniform-fee-target-refinement/README.md b/research/uniform-fee-target-refinement/README.md new file mode 100644 index 0000000000..8d8d5d31c0 --- /dev/null +++ b/research/uniform-fee-target-refinement/README.md @@ -0,0 +1,164 @@ +# Exact uniform-fee optimum for independent target refinement + +This package was produced by Nick Petalas. + +**Claim type: scoped written proof with exact finite corroboration.** This is an +accounting theorem about one replacement step in the mixed-target invoice. It is +not a construction, a native or caller proof, a supplier admission or a κ change. +The selected record stays κ = 781451/250000000. + +## Setting + +A productive target of positive integer rank R is replaced by k ≥ 1 independent +targets of positive integer ranks r_1, …, r_k with Σ r_i = R. Each piece after +the first carries the same paid fee c ≥ 0, so the credit change is + + Δ(r) = Σ φ(r_i) − (k−1)c − φ(R), + +for a rank tariff φ on {0, …, R} that is nondecreasing, concave and has φ(0)=0. +This covers the invoice tariff φ(r) = r^t with t = 1−C, 0 < t < 1, and the cap +tariffs min(r, K) of the concave-order comparator. Write +S(k) = (R mod k)·φ(⌈R/k⌉) + (k − R mod k)·φ(⌊R/k⌋) for the balanced k-split. + +## Predecessors and the new part + +Ali Romman's [#5769](https://github.com/CrocSwap/integer-mult-bounds/pull/5769) +defines the fee-charged target-partition contract used here, with a finite +optimizer for an explicit menu of piece ranks and fees. Merged +[#5909](https://github.com/CrocSwap/integer-mult-bounds/pull/5909) (Nick +Petalas) specializes that contract to the power tariff at exponent 99/100, with +one paid rank-one child charged for each resulting piece. It proves, using +concavity, Jensen's inequality and integer balancing, that a profitable +partition exists exactly when R ≥ 288, with witness 96+96+96. That rank-288 +threshold is #5909's result and is not claimed here. + +This package adds the following: + +- the closed form of items 1–3 for every nondecreasing concave tariff with + φ(0) = 0 and every uniform fee c ≥ 0; +- concavity of the balanced credit in the piece count, via the perspective of + the interpolant; +- the halving test of item 4; +- certified thresholds at the selected exponent for fees of one paid rank-q + job, q ∈ {1, 2, 4, 8}. + +**Fee normalization.** #5909 charges one fee per resulting piece, which is k +fees. This package charges one fee per piece after the first, which is k − 1 +fees. The two credit changes differ by the constant −c. Items 1–3 therefore +apply to #5909's model with the same optimal balanced partition and the same +k*. The halving test does not apply: with k fees, a three-part split can pay +while halving does not, as #5909's first witness 96+96+96 shows. This package's +verifier evaluates only the selected exponent, not 99/100. It does not compute +#5909's quantity, so there is no number to compare. + +## Theorem + +1. For each k, the balanced partition maximizes Σ φ(r_i) among all k-part + partitions of R. +2. S(k) is concave in k on 1 ≤ k ≤ R. +3. The best refinement has credit max_k S(k) − (k−1)c. It is attained by the + balanced partition with k* = the least k such that S(k+1) − S(k) ≤ c (or + k* = R if no such k exists). +4. **Halving test.** Some refinement strictly improves the target credit if and + only if φ(⌊R/2⌋) + φ(⌈R/2⌉) − φ(R) > c. + +## Proof + +Let ψ be the piecewise-linear interpolation of φ at the integers. It is concave +on [0, R] with ψ(0) = 0, and agrees with φ at integers. + +(1) A balanced vector is majorized by every other integer vector with the same +length and sum. Karamata's inequality for the concave φ gives +Σ φ(r_i) ≤ S(k). + +(2) Write R = qk + s with 0 ≤ s < k. Since q ≤ R/k ≤ q+1, + + k·ψ(R/k) = kφ(q) + (R − kq)(φ(q+1) − φ(q)) = (k−s)φ(q) + sφ(q+1) = S(k). + +The perspective g(k) = k·ψ(R/k) of a concave function is concave for k > 0. +Restricting to integers keeps the second differences nonpositive. + +(3) By (1), the optimum over all partitions with k pieces is S(k) − (k−1)c. +This function of k is concave by (2), because the fee term is linear. A +concave sequence attains its maximum at the first k where its forward +difference S(k+1) − S(k) − c becomes nonpositive. + +(4) Refinement improves the credit iff max over k ≥ 2 of S(k) − (k−1)c exceeds +S(1) = φ(R). By concavity this happens iff the first difference S(2) − S(1) − c +is positive. S(2) is the expression in the halving test. ∎ + +The hypotheses are needed. The verifier includes a nondecreasing non-concave +tariff (0,0,1,1,1,1,2) on R = 6 with fee 0. Halving gains nothing, yet the +balanced three-way split gains 1. A convex tariff also makes an unbalanced +pair beat the balanced pair. + +## Consequence at the selected exponent + +Take φ(r) = r^t with t = 1 − 781451/250000000 and the fee of one extra paid +rank-q job per piece, c = q^t. The halving gain becomes positive at: + +| Fee job rank q | Least target rank R at which any refinement pays | +|---:|---:| +| 1 | 470 | +| 2 | 940 | +| 4 | 1880 | +| 8 | 3760 | + +The verifier checks that the halving gain is at most c for every R below each +threshold and above c for every R from the threshold up to 7520. The gap is +always at least 10^-40, evaluated with 60-digit correctly rounded `Decimal` +exponentials and logarithms. For even R = 2m the test reads +m^t(2 − 2^t) > c, so the threshold is about c/(2 − 2^t) ≈ c/(2C ln 2) pieces +of size two, which grows like 1/C. + +These numbers apply the selected value as the tariff exponent for +illustration. They are not a claim about the actual binding supplier's +normalization, any actual helper target, or the legality of any split. +Independence, chronological availability, native delivery, restoration, +and caller costs remain separate obligations. A nonuniform fee menu needs the +#5769 target-partition optimizer or a separate argument. + +## Reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -B research/uniform-fee-target-refinement/verify.py +python3 -O -B research/uniform-fee-target-refinement/verify.py +``` + +Expected output, about two seconds: + +``` +PASS_UNIFORM_FEE_TARGET_REFINEMENT exact_checks=10392 controls=2 thresholds=q1:R>=470 q2:R>=940 q4:R>=1880 q8:R>=3760 +``` + +Part A enumerates every integer partition of every R ≤ 22 under eight exact +rational concave tariffs (linear, harmonic, a concave quadratic and five caps) +and 38 distinct rational fees. It checks items 1–4 against the brute-force optimum. +Part B certifies the threshold table. The finite checks corroborate the proof; +the all-R statement rests on the written argument. + +## Open next questions + +- **Rank-dependent fees.** If the fee for a piece depends on its rank (an + adapter whose cost grows with the piece), is the optimum still balanced, and + does a halving test survive? First step: fees of the form c + d·φ(r_i). +- **Actual helper targets.** Which productive targets in the selected P104 + ledger exceed the q = 1 threshold of 470, and what is the cheapest legal + per-piece fee for them? Blocked by the selected-invoice exporter, which does + not yet support the PR6030 source. +- **Joint refinement.** When several targets share one fee (one adapter that + serves many splits), the fee is no longer additive per piece. Determine the + joint optimum for a shared fixed fee plus a per-piece fee. + +## Credit + +The general theorem, its proof, the verifier and the selected-exponent +threshold table were produced by Nick Petalas. Predecessors: Ali Romman's +#5769 fee-charged target-partition contract and optimizer, which is the object +generalized here, and #5909's unit-fee threshold at exponent 99/100, which is a +special case (up to the fee normalization above). The signed mixed-target +invoice model and the concave-order comparator are by zxv, as credited in +`docs/research/recursive-invoice-preflight.md`. Karamata's inequality and the +concavity of perspective functions are classical. Apache-2.0. diff --git a/research/uniform-fee-target-refinement/SOURCES.json b/research/uniform-fee-target-refinement/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/research/uniform-fee-target-refinement/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/uniform-fee-target-refinement/TASK.json b/research/uniform-fee-target-refinement/TASK.json new file mode 100644 index 0000000000..b0959d52b8 --- /dev/null +++ b/research/uniform-fee-target-refinement/TASK.json @@ -0,0 +1,85 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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" + ], + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "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": "Exact optimum of refining one productive target of rank R into independent integer-rank targets with a uniform per-piece paid fee, for every nondecreasing concave rank tariff with phi(0)=0; halving test and selected-exponent thresholds.", + "scope_change_reason": "The card asks for a source-bound complete construction. This package answers a narrower quantified accounting proposition that bounds when any independent-target split with a uniform fee can pay, before a construction is attempted.", + "bottleneck_link": "Revision 8 names legal independent-target splitting as the current complex-helper mechanism. The halving test and thresholds say which target ranks a uniform-fee split must reach before its signed moment can improve.", + "budget_minutes": 60, + "stop_rule": "Stop after the written proof of the four-part theorem, exhaustive exact corroboration for R<=22 and certified thresholds for q in {1,2,4,8}.", + "outcome": "completed", + "evidence": "README.md proof; verify.py exhaustive exact checks, failure controls and 60-digit Decimal threshold certificates.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the balanced optimum and a halving test survive rank-dependent per-piece fees?", + "why_it_matters": "Adapters whose cost grows with the piece are more realistic than a flat fee.", + "first_step": "Fees of the form c + d*phi(r_i).", + "blocked_by": "The perspective argument needs the fee to be linear in the piece count." + }, + { + "question": "Which selected P104 productive targets exceed the q=1 threshold of rank 470, and what is the cheapest legal per-piece fee for them?", + "why_it_matters": "Only those targets can host a profitable uniform-fee split.", + "first_step": "Extract the PR6030 target histogram.", + "blocked_by": "The selected-invoice exporter reports the PR6030 source as unsupported." + }, + { + "question": "What is the joint optimum when several targets share one fixed adapter fee plus a per-piece fee?", + "why_it_matters": "Shared adapters make fees nonadditive across splits.", + "first_step": "Two targets with one shared fixed fee.", + "blocked_by": "Not addressed here." + } + ] +} diff --git a/research/uniform-fee-target-refinement/VERIFY.json b/research/uniform-fee-target-refinement/VERIFY.json new file mode 100644 index 0000000000..7e3bb4b954 --- /dev/null +++ b/research/uniform-fee-target-refinement/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive exact partition checks for R<=22 under eight concave tariffs, two hypothesis-failure controls, certified selected-exponent thresholds." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same checks under -O; all failures raise explicitly." + } + ] +} diff --git a/research/uniform-fee-target-refinement/verify.py b/research/uniform-fee-target-refinement/verify.py new file mode 100644 index 0000000000..35fe91a95f --- /dev/null +++ b/research/uniform-fee-target-refinement/verify.py @@ -0,0 +1,186 @@ +"""Exact checks for the uniform-fee target-refinement theorem. + +Part A enumerates every integer partition of every target rank R <= R_MAX and +compares the true optimum with the closed form for exact rational concave +tariffs and fees. Part B certifies the halving thresholds for the power +tariff r**t at the selected exponent with correctly rounded decimal arithmetic. +Standard library only. +""" + +from __future__ import annotations + +import sys +from decimal import Decimal, localcontext +from fractions import Fraction +from typing import Callable, Iterator + +R_MAX = 22 +SELECTED_KAPPA = Fraction(781451, 250000000) +FEE_RANKS = (1, 2, 4, 8) +EXPECTED_THRESHOLDS = {1: 470, 2: 940, 4: 1880, 8: 3760} +DIGITS = 60 +MARGIN = Decimal("1e-40") + +Tariff = Callable[[int], Fraction] + + +def partitions(n: int, largest: int) -> Iterator[tuple[int, ...]]: + """Yield the partitions of n with parts at most `largest`, nonincreasing.""" + if n == 0: + yield () + return + for first in range(min(n, largest), 0, -1): + for rest in partitions(n - first, first): + yield (first,) + rest + + +def balanced(phi: Tariff, rank: int, pieces: int) -> Fraction: + q, r = divmod(rank, pieces) + return r * phi(q + 1) + (pieces - r) * phi(q) + + +def harmonic(n: int) -> Fraction: + return sum((Fraction(1, j) for j in range(1, n + 1)), Fraction(0)) + + +def tariffs() -> dict[str, Tariff]: + """Exact increasing concave tariffs with phi(0) = 0 on 0..R_MAX.""" + width = R_MAX + menu: dict[str, Tariff] = { + "linear": lambda n: Fraction(n), + "harmonic": harmonic, + "quadratic": lambda n: Fraction(n * (2 * width - n), width), + } + for cap in (1, 2, 3, 5, 8): + menu[f"cap{cap}"] = lambda n, cap=cap: Fraction(min(n, cap)) + return menu + + +def is_concave_increasing(phi: Tariff) -> bool: + values = [phi(n) for n in range(R_MAX + 1)] + steps = [b - a for a, b in zip(values, values[1:])] + return ( + values[0] == 0 + and all(s >= 0 for s in steps) + and all(a >= b for a, b in zip(steps, steps[1:])) + ) + + +def predicted_optimum(phi: Tariff, rank: int, fee: Fraction) -> tuple[Fraction, int]: + """Closed form: first k whose next balanced increment is at most the fee.""" + k = 1 + while k < rank and balanced(phi, rank, k + 1) - balanced(phi, rank, k) > fee: + k += 1 + return balanced(phi, rank, k) - (k - 1) * fee, k + + +def check_exact() -> int: + fees = sorted({Fraction(a, b) for a in range(0, 13) for b in (1, 2, 3, 7)}) + checks = 0 + for name, phi in tariffs().items(): + if not is_concave_increasing(phi): + raise AssertionError(f"tariff {name} is not concave increasing") + for rank in range(1, R_MAX + 1): + best_by_k: dict[int, Fraction] = {} + for part in partitions(rank, rank): + credit = sum((phi(x) for x in part), Fraction(0)) + k = len(part) + if credit > best_by_k.get(k, Fraction(-1)): + best_by_k[k] = credit + ks = sorted(best_by_k) + for k in ks: + if best_by_k[k] != balanced(phi, rank, k): + raise AssertionError(f"balanced not optimal: {name} R={rank} k={k}") + checks += 1 + for k in ks[1:-1]: + if best_by_k[k - 1] + best_by_k[k + 1] > 2 * best_by_k[k]: + raise AssertionError(f"not concave: {name} R={rank} k={k}") + checks += 1 + for fee in fees: + truth = max(best_by_k[k] - (k - 1) * fee for k in ks) + value, k_star = predicted_optimum(phi, rank, fee) + if value != truth or best_by_k[k_star] - (k_star - 1) * fee != truth: + raise AssertionError(f"optimum mismatch: {name} R={rank} fee={fee}") + halving_pays = rank >= 2 and balanced(phi, rank, 2) - phi(rank) > fee + if halving_pays != (truth > phi(rank)): + raise AssertionError(f"halving test fails: {name} R={rank} fee={fee}") + checks += 1 + return checks + + +def failure_controls() -> int: + """The theorem's hypotheses matter: a convex tariff breaks the halving test.""" + convex: Tariff = lambda n: Fraction(n * n) + if is_concave_increasing(convex): + raise AssertionError("convex control misclassified") + # Halving never pays under a convex tariff, yet the theorem's balanced + # rule is not optimal for fixed k: (R-1, 1) beats the balanced pair. + rank = 6 + if balanced(convex, rank, 2) >= convex(5) + convex(1): + raise AssertionError("convex control did not separate balanced split") + # Increasing but non-concave tariff (found by a small exhaustive search): + # halving does not pay at fee 0, yet the balanced three-way split does. + table = (0, 0, 1, 1, 1, 1, 2) + bumpy: Tariff = lambda n: Fraction(table[n]) + fee = Fraction(0) + halving = max(bumpy(a) + bumpy(rank - a) for a in range(1, rank)) - bumpy(rank) + three = 3 * bumpy(2) - 2 * fee - bumpy(rank) + steps = [b - a for a, b in zip(table, table[1:])] + concave = all(a >= b for a, b in zip(steps, steps[1:])) + if concave or min(steps) < 0 or halving > fee or three <= 0: + raise AssertionError("non-concave control did not separate the halving test") + return 2 + + +def power(n: int, t: Decimal) -> Decimal: + return Decimal(0) if n == 0 else (t * Decimal(n).ln()).exp() + + +def halving_gain(rank: int, t: Decimal) -> Decimal: + low = rank // 2 + return power(low, t) + power(rank - low, t) - power(rank, t) + + +def check_thresholds() -> dict[int, int]: + found: dict[int, int] = {} + with localcontext() as ctx: + ctx.prec = DIGITS + t = Decimal(SELECTED_KAPPA.denominator - SELECTED_KAPPA.numerator) / Decimal( + SELECTED_KAPPA.denominator + ) + limit = 2 * max(EXPECTED_THRESHOLDS.values()) + gains = [Decimal(0), Decimal(0)] + [halving_gain(r, t) for r in range(2, limit + 1)] + for q in FEE_RANKS: + fee = power(q, t) + for rank in range(2, limit + 1): + gap = gains[rank] - fee + if abs(gap) < MARGIN: + raise AssertionError(f"uncertified sign at R={rank} q={q}") + if gap > 0 and q not in found: + found[q] = rank + if q not in found: + raise AssertionError(f"no threshold for q={q}") + first = found[q] + if any(gains[r] - fee > 0 for r in range(2, first)): + raise AssertionError("threshold not least") + if any(gains[r] - fee <= 0 for r in range(first, limit + 1)): + raise AssertionError(f"profit not monotone above threshold q={q}") + if found != EXPECTED_THRESHOLDS: + raise AssertionError(f"thresholds {found} != {EXPECTED_THRESHOLDS}") + return found + + +def main() -> int: + exact = check_exact() + controls = failure_controls() + found = check_thresholds() + summary = " ".join(f"q{q}:R>={r}" for q, r in sorted(found.items())) + print( + f"PASS_UNIFORM_FEE_TARGET_REFINEMENT exact_checks={exact} " + f"controls={controls} thresholds={summary}" + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main())