Certify a unique positive query-tree crossing by tail sums (no κ)

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 κ.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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)."
+    }
+  ]
+}