From 6bc26ee287c074011576f067d19c1e97ef1344ff Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 14:43:53 +0000 Subject: [PATCH] feat(research): prove the query-price threshold for the #5554 path reduction Charge each QUERY stage w*v. The canonical one-invoice-per-FULL-count reduction and its price frontier transfer exactly for 1 <= w <= b^t+(2b+1)^t-(3b)^t; above that a merged 11 pair beats the canonical invoice at every n >= 6, and below w=1 the family is unbounded. --- research/path-query-price-threshold/README.md | 148 ++++++++++++++++++ .../path-query-price-threshold/SOURCES.json | 24 +++ research/path-query-price-threshold/TASK.json | 96 ++++++++++++ .../path-query-price-threshold/VERIFY.json | 20 +++ research/path-query-price-threshold/verify.py | 136 ++++++++++++++++ 5 files changed, 424 insertions(+) create mode 100644 research/path-query-price-threshold/README.md create mode 100644 research/path-query-price-threshold/SOURCES.json create mode 100644 research/path-query-price-threshold/TASK.json create mode 100644 research/path-query-price-threshold/VERIFY.json create mode 100644 research/path-query-price-threshold/verify.py diff --git a/research/path-query-price-threshold/README.md b/research/path-query-price-threshold/README.md new file mode 100644 index 0000000000..330a8a4d98 --- /dev/null +++ b/research/path-query-price-threshold/README.md @@ -0,0 +1,148 @@ +# Query-price threshold for the productive-helper path reduction + +zxv's [PR5554](https://github.com/CrocSwap/integer-mult-bounds/pull/5554) +(`research/kappa-architecture-frontier`) reduces every FULL/QUERY mask of the +rank-b productive-helper path to one canonical invoice per FULL count. That +reduction assumes each QUERY stage costs `v` rank-one jobs. Its Open next +question 3 asks what happens under a changed query law. This package answers +that question for one changed law: each QUERY stage costs `w*v` rank-power +units, with every other term of #5554's equation (1) unchanged. + +**Result (scoped proof).** Write `f(z)=z^t` with `f(0)=0`, `t=1-C` in `(0,1)`, +`b>1`, and + +`g_k(b,t) = b^t + (bk+b+1)^t - (bk+2b)^t`, so `w*(b,t) := g_1 = b^t + (2b+1)^t - (3b)^t`. + +1. If `1 <= w <= w*`, the canonical reduction holds at every FULL count `n`, + for all pair counts, splits and masks, with minimum + `C_n^w = C_n + (w-1) v Q_n`, where `C_n` is #5554's (2)/(3) and + `Q_n = |n-3|` is its query count. Convexity, the three-sign exclusion (4), + the price frontier (5)/(6) and the three-value ratio gate all transfer + with `c_n` replaced by `c_n + (w-1)|n-3|`. +2. If `w > w*`, the canonical invoice is strictly beaten at every `n >= 6`, + by at least `2v(w - w*)`. #5554's cap and frontier must not be transferred. +3. If `w < 1`, the infimum is `-infinity` at every `n`: each empty pair + inserted next to a side end bit 0 gains `2v(1-w)`. + +At b=8 the tolerance `w*-1` is small: + +| C | `w* = 8^t+17^t-24^t` | +|---:|---:| +| .0031 | 1.03522543106 | +| .0034 | 1.03859829952 | +| .004 | 1.04532506534 | +| .01 | 1.11121543014 | + +So at C=.0034 a per-QUERY surcharge above about .0386 rank-one units per port +already breaks the canonical form. In that case 11 side pairs survive. A +rank-two query (`w=2^t`, near 2) is far outside this range for t near one. +No new κ, supplier admission or selected-frontier change is claimed. + +## Proof + +Use #5554's notation. With query price `w`, the bill is + +`E_w = E_1 + (w-1) v Q`, with `Q = 2p+1-n` QUERY stages, + +because only the rank-one query term changes. Every move of #5554's §2 keeps +`n` fixed. Classify each move by its effect on `Q`. + +* **Delete a 00 pair, and move a side FULL into an empty unpaired + position.** Each deletes one pair and two QUERY stages: `Q` falls by 2. #5554 + shows `Delta E_1 <= 0`. Hence `Delta E_w = Delta E_1 - 2v(w-1) <= 0` for `w >= 1`. +* **Replace 01 by 10, and balance the sides.** `Q` is unchanged, so the + #5554 signs hold verbatim. +* **Split 11 into 10,10** at preceding FULL count `k`. `Q` rises by 2. Divided + by `2v` the change is `w + f(bk+2b) - f(bk+b+1) - f(b) = w - g_k`. + +`g_k` is strictly increasing in k. Indeed +`g_k = f(b) - integral over [bk+b+1, bk+2b] of t z^(t-1) dz`; the integrand +decreases and the interval moves right. So the split is non-increasing for +every `k >= 1` exactly when `w <= g_1`. Only `k=0` needs a new move. + +After the 00 deletions and 01 replacements, a side pair with `k=0` is the +first pair on a side whose end bit is 0. **New move:** replace end bit 0 and +first pair 11 by end bit 1 and first pair 10. `n`, `Q`, and the FULL count +preceding every later window are unchanged. The window term changes from +`2f(b) - f(1+2b)` to `f(2b) - f(1+2b)`. The change `2v(f(2b) - 2f(b))` is +negative by strict subadditivity. Apply it once per side, then split every +remaining 11 pair; each now has `k >= 1`. None of these moves creates a 00 or +01 pair or a `k=0` 11 pair. Then #5554's FULL relocation and balancing +finish at the canonical mask. Its query count is `n-3` for `n >= 3` (p=n-2), +and `3-n` for `n <= 2` (p=1). This proves part 1's minimum. + +For convexity, `D_n` gains `(w-1)v(Q_(n+1)-Q_n)`: `-(w-1)v` for `n<3`, and +`+(w-1)v` for `n>=3`. Only `D_3-D_2` changes, and it gains `2(w-1)v >= 0`. So +`C_n^w` stays strictly convex. #5554's ratio argument uses only strict +increase of `D_n`. The maximum defining `lambda` still exists: +`c_1^w = 2w - 2(1+b)^t < 0` because `w <= g_1 < b^t`, and `c_n^w/n -> w > 0`. + +**Sharpness (part 2).** For `n >= 6` the canonical right side has +`ceil((n-3)/2) >= 2` pairs. Its outer pairs, read inward, are 10 at `k=1` +then 10 at `k=2`. Merge them into one 11 pair at `k=1`. Later windows keep +preceding count 3. The window terms change from `W(2,0)+W(3,0)` to `W(2,1)`, +with `W(h,e)=f(bh)+e f(b)-f(1+b(h+e))`. This is a change of `f(b)+f(2b+1)-f(3b) += g_1` per `2v`. Two QUERY stages disappear. The total change is +`2v(g_1 - w) < 0`. + +**Part 3.** Insert a 00 pair between a side's end bit 0 and its first pair. +Its window has `h=e=0` and contributes `-f(1) = -1`; earlier counts are +unchanged; two QUERY stages are added. The change is `2v(w-1)`, negative for +`w<1`, and the insertion repeats without bound. Every n has a mask whose +left end bit is 0, so the infimum is `-infinity` at every n. The verifier +checks this gain for `n <= 2` only. + +## Evidence and reproduction + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/path-query-price-threshold/verify.py +``` + +Expected: `PASS_PATH_QUERY_PRICE_THRESHOLD masks_p_le=6 block_ranks=2 exponents=4 checks=456` +(about 7 s on CPython 3.12). The script pins the bytes of #5554's `PROOF.md` +and its equation (1). For b in {2, 8} and t in {1/2, 9/10, 4983/5000, +999/1000}, it does the following with 60-digit decimal arithmetic: + +* evaluates the literal equation (1), with QUERY price w, on every mask with + p <= 6 pairs and every split; +* at w in {1, (1+g_1)/2, g_1 - 10^-40}, confirms that no such mask beats the + canonical invoice, and that the canonical value is attained whenever its own + p fits; +* at w = g_1 + 1/100, confirms the n=6 merge identity `2(w-g_1)` and a gap of + at least that size for each `6 <= n <= 9`; +* confirms that `g_k` increases for `k < 64` and that the outer 00 pair gains + `2(1-w)` at w = 99/100. + +These are finite controls on the written proof. They are not an all-p search +or a proof-kernel check. + +## Limitations + +* This is a scoped proof about #5554's relaxed raw invoice family with one + changed tariff. It covers no native word, compiler closure, BIT/outer + funding or physical query realization. +* It changes only the query price. Query rank as a target, query helper + credit, the idle law and nonautonomous outputs remain outside scope. +* #5554's exchange proof, inherited from #5405/#5409, is cited as a premise + and not re-verified here. Independent human or proof-kernel review has not + been run. + +## Open next questions + +1. **Minimum for w > w\*.** Which masks are optimal once 11 pairs survive? A + guess is that the outer pairs become 11 up to an index fixed by + `g_k >= w`. First step: extend the exchange argument with 11 pairs ordered + by `k` and compare with the brute-force minima. +2. **Query law with target credit.** If a rank-q query also earns a rank-q + target, the per-pair balance changes. Does the reduction survive? +3. **Fee at the frontier.** At C=.0034, does a surcharge below `w*-1` move + #5554's optimal FULL count 16 for the #5551 bill? Its ratio gate now + includes `(w-1)|n-3|`. + +## Credit + +Produced by Nick Petalas. The path family, equation (1), the canonical +reduction and the price frontier are zxv's #5554. It builds on Ali Romman's +#5405/#5409 exchange and convexity proofs and the credited predecessors listed +there. The query-price parameter, the threshold `w*`, the new k=0 move, the +sharpness witness and the unboundedness below `w=1` are new here. Apache-2.0. diff --git a/research/path-query-price-threshold/SOURCES.json b/research/path-query-price-threshold/SOURCES.json new file mode 100644 index 0000000000..f6a28d13f2 --- /dev/null +++ b/research/path-query-price-threshold/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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" + }, + { + "path": "research/kappa-architecture-frontier/PROOF.md", + "usage": "input", + "git_blob": "619859b95985f4034c901fa54e7cd365f49726c0", + "sha256": "c16fd82b009e9ec2a1f2bea5543cce8318f13f70ed062b29b2c425c03e3534e1" + } + ] +} diff --git a/research/path-query-price-threshold/TASK.json b/research/path-query-price-threshold/TASK.json new file mode 100644 index 0000000000..e30834e288 --- /dev/null +++ b/research/path-query-price-threshold/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Changed query law for zxv's PR5554 productive-helper path (Open next question 3): each QUERY stage costs w*v instead of v, all else in equation (1) unchanged. Exact range of w for which the canonical one-invoice-per-FULL-count reduction, convexity and price frontier transfer, with a sharp witness beyond it.", + "scope_change_reason": "The card asks about changed query demands on a real caller. PR5554 leaves 'one changed query law' explicitly open for its path family; this answers that relaxed-invoice question before any native construction, so a proposal with a surcharged query knows whether #5554's cap applies.", + "bottleneck_link": "Side result for the complex path architecture: it states exactly when #5554's all-length controller cap and per-FULL price frontier may be reused under a query surcharge, and when they must not be.", + "budget_minutes": 60, + "stop_rule": "Stop at the sharp threshold w*=g_1 with a written proof, finite mask controls and a merge witness; leave the optimal mask family above w* as an open question.", + "outcome": "completed", + "evidence": "README.md written proof; verify.py checks literal equation (1) with query price w on every mask with p<=6 pairs for b in {2,8} and four exponents (PASS_PATH_QUERY_PRICE_THRESHOLD checks=456).", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which masks are optimal for w > w* once 11 side pairs survive?", + "why_it_matters": "Gives the transferable cap and frontier for a surcharged query law.", + "first_step": "Extend the exchange argument with 11 pairs ordered by k and compare with brute-force minima.", + "blocked_by": "none" + }, + { + "question": "Does the reduction survive a rank-q query that also earns a rank-q target?", + "why_it_matters": "A query that is productive changes the per-pair balance, not only its price.", + "first_step": "Rewrite equation (1) with the target term and redo the four moves.", + "blocked_by": "none" + }, + { + "question": "Does a surcharge below w*-1 move #5554's optimal FULL count 16 for the #5551 bill at C=.0034?", + "why_it_matters": "The ratio gate now includes (w-1)|n-3|.", + "first_step": "Evaluate J_n with c_n+(w-1)|n-3| at the #5551 profile.", + "blocked_by": "none" + } + ] +} diff --git a/research/path-query-price-threshold/VERIFY.json b/research/path-query-price-threshold/VERIFY.json new file mode 100644 index 0000000000..4c9a60cd4a --- /dev/null +++ b/research/path-query-price-threshold/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-architecture-frontier/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal equation (1) with QUERY price w on every mask with p<=6: canonical minimal for 1<=w<=g_1, n=6 merge witness above g_1, g_k monotone, 00-pair gain below w=1; source PROOF.md bytes pinned." + } + ] +} diff --git a/research/path-query-price-threshold/verify.py b/research/path-query-price-threshold/verify.py new file mode 100644 index 0000000000..7863731d71 --- /dev/null +++ b/research/path-query-price-threshold/verify.py @@ -0,0 +1,136 @@ +"""Finite controls for the query-price threshold of the #5554 path family. + +The theorem is the written proof in README.md. This script checks it on every +mask with p <= P_MAX pairs, at several exponents, block ranks and query +prices, using 60-digit decimal arithmetic. It is a finite control, not a proof. +""" +import hashlib +import functools +import itertools +import sys +from decimal import Decimal, getcontext +from fractions import Fraction as F +from pathlib import Path + +getcontext().prec = 60 +TOL = Decimal('1e-45') +P_MAX = 6 +HERE = Path(__file__).resolve().parent +SOURCE = HERE.parent / 'kappa-architecture-frontier' / 'PROOF.md' +SOURCE_SHA256 = 'c16fd82b009e9ec2a1f2bea5543cce8318f13f70ed062b29b2c425c03e3534e1' +EQUATION_1 = 'E=v(2p+1)+(L-v)n-2v f(1+bn)' + + +def require(condition, message): + if not condition: + raise SystemExit('FAIL: ' + message) + + +def dec(x): + return Decimal(x.numerator) / Decimal(x.denominator) + + +@functools.lru_cache(maxsize=None) +def f(z, t): + """f(z)=z^t with f(0)=0, for integer z >= 0.""" + if z == 0: + return Decimal(0) + return (dec(t) * Decimal(z).ln()).exp() + + +def path_cost(bits, p, a, b, t, w): + """Equation (1) of #5554 with v=1, L=0 and QUERY price w per stage.""" + n = sum(bits) + total = dec(w) * (2 * p + 1 - n) - 2 * f(1 + b * n, t) + for j in range(1, p): + h = sum(bits[:2 * j]) if j <= a else sum(bits[2 * j + 1:]) + e = bits[2 * j] + total += 2 * (f(b * h, t) + e * f(b, t) - f(1 + b * (h + e), t)) + return total + + +def canonical(n, b, t, w): + """Canonical invoice (2)-(3) of #5554 with v=1, L=0 and query price w.""" + def delta(z): + return f(z + 1, t) - f(z, t) + if n < 3: + return dec(w) * (3 - n) - 2 * f(1 + b * n, t) + a = (n - 3) // 2 + d = n - 3 - a + side = sum(delta(b * k) for k in range(2, a + 2)) + side += sum(delta(b * k) for k in range(2, d + 2)) + return dec(w) * (n - 3) - 2 * f(1 + b * n, t) - 2 * side + + +def g(k, b, t): + return f(b, t) + f(b * k + b + 1, t) - f(b * k + 2 * b, t) + + +def minima(b, t, w): + best = {} + for p in range(1, P_MAX + 1): + for a in range(p): + for bits in itertools.product((0, 1), repeat=2 * p + 1): + n = sum(bits) + cost = path_cost(bits, p, a, b, t, w) + if n not in best or cost < best[n]: + best[n] = cost + return best + + +def main(): + data = SOURCE.read_bytes() + require(hashlib.sha256(data).hexdigest() == SOURCE_SHA256, 'source bytes') + require(EQUATION_1 in data.decode(), 'source equation (1) not found') + exponents = (F(1, 2), F(9, 10), F(4983, 5000), F(999, 1000)) + blocks = (2, 8) + checks = 0 + for b in blocks: + for t in exponents: + gs = [g(k, b, t) for k in range(0, 64)] + require(all(x < y for x, y in zip(gs, gs[1:])), 'g_k not increasing') + require(gs[0] > 1, 'g_0 <= 1') + g1 = gs[1] + g1_frac = F(str(g1)) # 60-digit decimal, used only to place w + inside = (F(1), (1 + g1_frac) / 2, g1_frac - F(1, 10**40)) + for w in inside: + got = minima(b, t, w) + for n, value in got.items(): + # No mask with p <= P_MAX beats the canonical invoice; it is + # attained in range when its own p=max(1,n-2) <= P_MAX. + c = canonical(n, b, t, w) + require(value > c - TOL, + f'canonical beaten b={b} t={t} w={float(w)} n={n}') + if n <= P_MAX + 2: + require(value < c + TOL, f'canonical not attained n={n}') + checks += 1 + w = g1_frac + F(1, 100) + got = minima(b, t, w) + for n, value in got.items(): + gap = canonical(n, b, t, w) - value + if 6 <= n <= P_MAX + 3: + require(gap >= 2 * (dec(w) - g1) - TOL, + f'n={n} gap below the merge witness') + checks += 1 + # Explicit n=6 merge witness: right side 10,10 -> 11 at k=1. + canon6 = (1, 1, 0, 1, 0, 1, 0, 1, 1) # p=4, a=1, canonical + merged = (1, 1, 0, 1, 1, 1, 1) # p=3, a=1, one 11 pair + c0 = path_cost(canon6, 4, 1, b, t, w) + c1 = path_cost(merged, 3, 1, b, t, w) + require(abs(c0 - canonical(6, b, t, w)) < TOL, 'n=6 canonical mask') + require(abs((c0 - c1) - 2 * (dec(w) - g1)) < TOL, 'merge identity') + require(c1 < c0, 'merge witness does not win above g_1') + # Below w=1 an outer 00 pair is profitable at every n: unbounded. + w = F(99, 100) + for n in range(0, 3): + base = (0,) * (3 - n) + (1,) * n + ext = (0, 0, 0) + base[1:] + drop = path_cost(base, 1, 0, b, t, w) - path_cost(ext, 2, 1, b, t, w) + require(abs(drop - 2 * (1 - dec(w))) < TOL, '00 pair gain') + checks += 1 + print(f'PASS_PATH_QUERY_PRICE_THRESHOLD masks_p_le={P_MAX} ' + f'block_ranks={len(blocks)} exponents={len(exponents)} checks={checks}') + + +if __name__ == '__main__': + sys.exit(main())