diff --git a/research/tail-sum-crossing-uniqueness/PROOF.md b/research/tail-sum-crossing-uniqueness/PROOF.md new file mode 100644 index 0000000000..dda16da529 --- /dev/null +++ b/research/tail-sum-crossing-uniqueness/PROOF.md @@ -0,0 +1,80 @@ +# Proof: one tail-sum sign change gives one positive crossing + +## Lemma (Laguerre's rule of signs, tail-sum form) + +Let `F(t) = sum_{k=0..n} c_k r_k^t` with real `c_k` and ranks +`0 < r_0 < ... < r_n`. Put `B_k = c_k + ... + c_n`. Then the number of distinct +zeros of `F` on `t > 0` is at most the number `S` of sign changes in +`B_0, ..., B_n` (zeros ignored). + +This is classical: Pólya and Szegő, *Problems and Theorems in Analysis II*, +Part V, Chapter 1; Karlin, *Total Positivity*, Chapter 5. For the reader, the +reduction is as follows. + +*Proof.* Put `m_k = ln r_k` and `B_{n+1} = 0`. Since `c_k = B_k - B_{k+1}`, + +```text +F(t) = B_0 e^{m_0 t} + sum_{k=1..n} B_k (e^{m_k t} - e^{m_{k-1} t}). +``` + +For `t > 0`, `e^{m_k t} - e^{m_{k-1} t} = t * integral_{m_{k-1}}^{m_k} e^{u t} du` +and `e^{m_0 t} = t * integral_{-inf}^{m_0} e^{u t} du`. Hence + +```text +F(t) = t * integral_{-inf}^{m_n} beta(u) e^{u t} du, +``` + +where `beta = B_0` on `(-inf, m_0]` and `beta = B_k` on `(m_{k-1}, m_k]`. The +step function `beta` has `S` sign changes. The kernel `e^{ut}` is strictly +totally positive, so its transform has at most `S` zeros on `t > 0` +(variation-diminishing property; Karlin, Chapter 5). Dividing by `t > 0` +does not change zeros. ∎ + +`B_0 = F(0)`. If `S = 0`, `F` has no zero on `t > 0`. + +## Application to the binary query-tree bill + +[PR6348](https://github.com/CrocSwap/integer-mult-bounds/pull/6348) +(`research/balanced-query-tree`, Ali Romman) has 19 full calls with the local +profiles, 16 thin queries of 104 rank-one calls, the main targets +`{17:1872, 25:208, 33:832, 57:208, 65:208, 153:208}` and the paired whole idle +jobs `{16:1872, 24:208, 32:832, 56:208, 64:208}`. The checker rebuilds this bill +from the source `RESULT.json` and checks its totals, 14214 fields and 70523 +paid calls. + +Let `F(t) = sum_r (T_r - P_r) r^t`. Its nonzero coefficients, in rank order, +are + +```text +1:-43502 2:-8512 3:-9348 4:171 5:-2869 6:-114 8:342 9:7315 +16:-1872 17:1872 24:-208 25:208 32:-832 33:832 56:-208 57:208 +64:-208 65:208 153:208 +``` + +The coefficients change sign 13 times, so a Descartes count allows up to 13 +real roots. The tail sums, in the same order, are + +```text +-56309 -12807 -4295 5053 4882 7751 7865 7523 208 2080 208 416 208 1040 +208 416 208 416 208 +``` + +They change sign exactly once. By the lemma, `F` has at most one zero on +`t > 0`. Since `F(0) = -56309 < 0` and `F(1) = 808 > 0` (the rank-mass +surplus), `F` has exactly one zero `t*` on `t > 0`. It lies in `(0,1)`, and +`F < 0` on `(0, t*)` and `F > 0` on `(t*, inf)`. + +**Consequence.** With `t = 1 - C`, the complete raw target moment of this bill +strictly exceeds its paid moment exactly when `C < 1 - t*`, for every +`C < 1`. The source check proves uniqueness only for `C <= 0.0034` through a +derivative bound; this certificate excludes a second favourable window on +the rest of the range. The location of `1 - t*` is the source's enclosure +`(0.00314934401301, 0.00314934401302)`. This package does not recompute it. +A 60-digit decimal sign check at `t = 0.99685` and `t = 0.99686` is a +consistency control only; the root location is not part of the claim. + +## Scope + +This is a statement about one invoice's arithmetic. It does not touch the +construction, native maps, compiler, outer ledger or any of the five retained +framework assumptions, and claims no new κ. diff --git a/research/tail-sum-crossing-uniqueness/README.md b/research/tail-sum-crossing-uniqueness/README.md new file mode 100644 index 0000000000..de8d363901 --- /dev/null +++ b/research/tail-sum-crossing-uniqueness/README.md @@ -0,0 +1,74 @@ +# One tail-sum sign change fixes the query-tree crossing globally + +**Scoped proof with an exact finite check. No new κ; the selected frontier is unchanged.** + +The complete signed raw moment of the merged binary query-tree bill +([PR6348](https://github.com/CrocSwap/integer-mult-bounds/pull/6348), +`research/balanced-query-tree`, Ali Romman, conditional κ 0.00314933) is + +```text +F(t) = sum_r (T_r - P_r) r^t. +``` + +Its coefficients change sign 13 times, so a Descartes count allows 13 real +roots. Their tail sums `B_k = c_k + ... + c_n` change sign exactly once. +By Laguerre's classical rule, `F` then has at most one zero on all of +`t > 0`. With `F(0) = -56309` and `F(1) = 808`, it has exactly one, in +`(0,1)`. So for every saving `C < 1`, the complete raw target moment beats +the paid moment exactly when `C` is below the raw crossing. The source +package proves uniqueness only for `C <= 0.0034`, by a derivative bound. + +[PROOF.md](PROOF.md) has the lemma, a short proof sketch with references, and the +application. [verify.py](verify.py) rebuilds the bill from the pinned source +`RESULT.json` and checks every step with exact integers. + +## Reproduce + +From the repository root: + +```sh +python3.12 -I -B research/tail-sum-crossing-uniqueness/verify.py +python3.12 -I -O -B research/tail-sum-crossing-uniqueness/verify.py +python3.12 -B scripts/research_package.py --package research/tail-sum-crossing-uniqueness +``` + +Each verifier run prints `PASS_TAIL_SUM_CROSSING_UNIQUENESS` in well under +a second. Add `--json` to print the certificate. Checked: + +- the bill's 14214 fields, 70523 paid calls and rank-mass surplus 808; +- 19 nonzero signed coefficients with 13 sign changes; +- tail sums with exactly one sign change, `F(0) < 0 < F(1)`; +- a 60-digit decimal sign check on both sides of the source enclosure + (consistency control, not part of the proof). + +Three rejection controls fail closed: the two-root invoice +`6 - 4·2^t - 3·3^t + 2·6^t` from `recursive-power-variation.md`, the reversed +invoice, and the bill without its rank-153 root targets. + +## Limitations + +Only invoice arithmetic is proved. The construction, native maps, compiler, +outer ledger and the five retained framework assumptions are untouched. +The crossing's location comes from the source package and is not +recomputed here. The lemma is classical (Pólya–Szegő; Karlin); the proof +in PROOF.md reduces it to the variation-diminishing property and cites +that property rather than reproving it. No proof-kernel check was run. + +## Open next questions + +1. **Does the rule settle inconclusive power-variation reports?** The + Descartes budget of `scripts/compare_power_variation.py` also counts roots + at `t <= 0`. The tail-sum count sees only `t > 0`; here it + is 1 against 13. First step: run `certify()` on the invoices that script reports + as inconclusive. This package does not modify the shared script. +2. **A count for `(0,1)` alone.** Roots at `t > 1` (negative savings) still + consume the budget. Tail sums of `c_r r` bound the roots on `t > 1`, but + subtracting two upper bounds gives no bound. A valid combination, or a + proof that none exists, would sharpen the certificate. + +## Credit + +Produced by Nick Petalas. The invoice and its source pricing are Ali +Romman's PR6348, with the predecessor credits recorded in that package. The +general-rank Descartes certificate is Ali Romman's PR5788. Laguerre's rule and +the variation-diminishing property are classical. New work is Apache-2.0. diff --git a/research/tail-sum-crossing-uniqueness/SOURCES.json b/research/tail-sum-crossing-uniqueness/SOURCES.json new file mode 100644 index 0000000000..ce13ab7893 --- /dev/null +++ b/research/tail-sum-crossing-uniqueness/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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" + }, + { + "path": "research/balanced-query-tree/RESULT.json", + "usage": "input", + "git_blob": "61ab6b26ff40168fb0982167ac67ef4607f27717", + "sha256": "f64a30b23a92e12e5e23c3d4400e139f20cf75bb2743d15c85b89ca1839a9408" + } + ] +} diff --git a/research/tail-sum-crossing-uniqueness/TASK.json b/research/tail-sum-crossing-uniqueness/TASK.json new file mode 100644 index 0000000000..74864c92ff --- /dev/null +++ b/research/tail-sum-crossing-uniqueness/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "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": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "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": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "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": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "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": "Prove that the complete signed raw moment of the merged binary query-tree bill (research/balanced-query-tree, PR6348) has exactly one zero on all of t>0, by Laguerre's tail-sum rule of signs, with an exact reusable checker.", + "scope_change_reason": "No rewrite is constructed. The card's acceptance gate is a favourable complete signed moment; this package settles the sign of that moment for one existing bill at every exponent, which the source check settles only below the 0.0034 BIT cap. The rule is a reusable certificate where the Descartes budget used by the power-variation tools is too weak.", + "bottleneck_link": "Side result on pricing: every \u03ba claim compares complete target and paid power sums. A global sign certificate rules out a second favourable window and needs no interval engine.", + "budget_minutes": 60, + "stop_rule": "Stop after one exact certificate on one merged bill; do not survey other bills.", + "outcome": "completed", + "evidence": "research/tail-sum-crossing-uniqueness/verify.py prints PASS_TAIL_SUM_CROSSING_UNIQUENESS; PROOF.md gives the argument.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "How many merged complete bills have exactly one tail-sum sign change, and does adding this rule to the power-variation tools settle invoices they report as inconclusive?", + "why_it_matters": "The Descartes budget counts roots at t<=0 as well; the tail-sum count only sees t>0, so it can be much smaller (13 versus 1 here).", + "first_step": "Run certify() on the invoices that scripts/compare_power_variation.py reports as inconclusive.", + "blocked_by": "None; this package does not modify the shared script." + }, + { + "question": "Can a tail-sum count on (0,1) alone be obtained, for example by combining tail sums of c_r and of c_r r?", + "why_it_matters": "Roots at t>1 (negative savings) are irrelevant, yet still consume this budget.", + "first_step": "Tail sums of c_r r bound roots on t>1; find a valid way to combine the two counts or prove none exists.", + "blocked_by": "Subtracting two upper bounds does not give an upper bound." + } + ] +} diff --git a/research/tail-sum-crossing-uniqueness/VERIFY.json b/research/tail-sum-crossing-uniqueness/VERIFY.json new file mode 100644 index 0000000000..e399daf02c --- /dev/null +++ b/research/tail-sum-crossing-uniqueness/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/balanced-query-tree/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the PR6348 tree bill from its RESULT.json, check totals and surplus, the Descartes budget 13, one tail-sum sign change, the unique positive crossing, a decimal sign check on both sides of the source enclosure, and three rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat with assertions disabled (the checker uses explicit need() calls)." + } + ] +} diff --git a/research/tail-sum-crossing-uniqueness/verify.py b/research/tail-sum-crossing-uniqueness/verify.py new file mode 100644 index 0000000000..68f108b3f3 --- /dev/null +++ b/research/tail-sum-crossing-uniqueness/verify.py @@ -0,0 +1,123 @@ +"""Certify a unique positive raw crossing with Laguerre's tail-sum rule. + +For F(t) = sum_r c_r r^t with distinct positive ranks r_0 < ... < r_n, the +number of zeros of F on t > 0, counted with multiplicity, is at most the +number of sign changes in the tail sums B_k = c_k + ... + c_n. +PROOF.md gives the argument. This checker uses exact integers only. + +Apache-2.0. Produced by Nick Petalas. The invoice is Ali Romman's +research/balanced-query-tree bill (PR6348). +""" +import decimal +import json +import pathlib +import sys +from collections import Counter + +HERE = pathlib.Path(__file__).resolve().parent +SOURCE = HERE.parent / 'balanced-query-tree' / 'RESULT.json' +MARKER = 'PASS_TAIL_SUM_CROSSING_UNIQUENESS' + + +def need(condition, label): + if not condition: + raise SystemExit('FAIL: ' + label) + + +def sign(value): + return (value > 0) - (value < 0) + + +def changes(values): + """Sign changes in a sequence, ignoring zeros.""" + signs = [sign(v) for v in values if v] + return sum(1 for a, b in zip(signs, signs[1:]) if a != b) + + +def signed(targets, paid): + ranks = sorted(set(targets) | set(paid)) + need(all(isinstance(r, int) and r >= 1 for r in ranks), 'Positive integer ranks') + return [(r, targets.get(r, 0) - paid.get(r, 0)) for r in ranks + if targets.get(r, 0) != paid.get(r, 0)] + + +def tail_sums(coefficients): + """B_k = c_k + ... + c_n, listed in increasing rank order.""" + out, total = [], 0 + for _, c in reversed(coefficients): + total += c + out.append(total) + return out[::-1] + + +def certify(targets, paid): + """Return the certificate, or None if the tail-sum rule does not settle it.""" + c = signed(targets, paid) + descartes = changes([v for _, v in c]) + tails = tail_sums(c) + laguerre = changes(tails) + f0 = sum(v for _, v in c) + f1 = sum(r * v for r, v in c) + # F(0) = B_0 < 0 < F(1): at least one root in (0,1); laguerre == 1 caps all of t > 0. + unique = laguerre == 1 and f0 < 0 < f1 + return {'descartes_changes': descartes, 'tail_sum_changes': laguerre, + 'F0_count_difference': f0, 'F1_rank_mass_surplus': f1, + 'signed_coefficients': [[r, v] for r, v in c], 'tail_sums': tails, + 'unique_simple_root_in_0_1_and_none_above': unique} + + +def value_sign(c, t): + """Sign of F at t with 60-digit decimals (consistency control, not the proof).""" + with decimal.localcontext() as ctx: + ctx.prec = 60 + total = sum(v * (decimal.Decimal(r).ln() * t).exp() for r, v in c) + need(abs(total) > decimal.Decimal('1e-30'), 'Sample point away from the root') + return sign(total) + + +def load(): + data = json.loads(SOURCE.read_text()) + local, physical = data['local'], data['physical'] + helpers = {int(k): v for k, v in local['helpers'].items()} + local_paid = {int(k): v for k, v in local['paid'].items()} + calls, queries, ports = physical['full_calls'], 16, physical['ports'] + targets = Counter({r: calls * v for r, v in helpers.items()}) + targets.update({int(k): v for k, v in physical['main_targets'].items()}) + paid = Counter({r: calls * v for r, v in local_paid.items()}) + paid[1] += queries * ports + paid.update({int(k): v for k, v in physical['whole_idle_jobs'].items()}) + need((sum(targets.values()), sum(paid.values())) == (14214, 70523), 'Source field and call totals') + return dict(targets), dict(paid) + + +def main(): + targets, paid = load() + cert = certify(targets, paid) + need(cert['F1_rank_mass_surplus'] == 808, 'Rank-mass surplus 808') + need(cert['F0_count_difference'] == 14214 - 70523, 'Count difference') + need(cert['descartes_changes'] == 13, 'Descartes budget 13') + need(cert['tail_sum_changes'] == 1, 'One tail-sum sign change') + need(cert['unique_simple_root_in_0_1_and_none_above'], 'Unique simple positive root') + c = [tuple(x) for x in cert['signed_coefficients']] + # Consistency with the source enclosure (0.00314934401301, 0.00314934401302): + # F(1-k) < 0 just above the root and > 0 just below, i.e. t = 1-k. + D = decimal.Decimal + need(value_sign(c, D(1)) > 0, 'F(1) > 0') + need(value_sign(c, D('0.99685')) < 0, 'F(0.99685) < 0, above k = 0.00315') + need(value_sign(c, D('0.99686')) > 0, 'F(0.99686) > 0, below k = 0.00314') + # Controls: the rule must fail closed on invoices it cannot settle. + two = certify({1: 6, 6: 2}, {2: 4, 3: 3}) # 2(2^t-3/2)(3^t-2): two interior roots + need(two['tail_sum_changes'] >= 2 and not two['unique_simple_root_in_0_1_and_none_above'], + 'Two-root control rejected') + flipped = certify(paid, targets) + need(not flipped['unique_simple_root_in_0_1_and_none_above'], 'Reversed invoice rejected') + bumped = dict(targets) + bumped[153] -= 208 + need(not certify(bumped, paid)['unique_simple_root_in_0_1_and_none_above'], 'Removed root target rejected') + if '--json' in sys.argv: + print(json.dumps(cert, indent=1)) + print(MARKER) + + +if __name__ == '__main__': + main()