Prove exact tariffs for consecutive queries sharing a detour

research/consecutive-query-detour/README.md

@@ -0,0 +1,217 @@
+# Exact tariffs for consecutive queries sharing a detour
+
+For consecutive queries that partition a geodesic helper target, a common
+detour of any finite length has an exact tariff optimum at an existing internal
+query endpoint. Extra charts cannot improve it. This holds for every
+nondecreasing concave tariff with value zero at zero, in any metric or
+pseudometric space. It answers a restricted part of Open next question 2 in
+[Ali Romman's PR #5779](https://github.com/CrocSwap/integer-mult-bounds/pull/5779).
+
+The result is a **scoped mathematical proof with finite corroboration**.
+It does not supply physical independent targets, dirty-state restoration,
+a shared correction, a new kappa or a complete multiplication theorem.
+
+## Contract and result
+
+Let `C_0,...,C_k`, with `k >= 2`, be metric charts on a geodesic in that order.
+Put `s_0=0`, `q_i=d(C_{i-1},C_i)>0`, `s_i=sum_{a=1}^i q_a`, and `t=s_k`.
+The geodesic hypothesis means
+
+```
+d(C_i,C_j) = |s_i-s_j|  for every i,j.
+```
+
+Let `phi:[0,infinity) -> [0,infinity)` be nondecreasing and concave, with
+`phi(0)=0`. The old invoice has one productive target `C_0 -> C_k` and the
+`k` paid queries `C_{i-1} -> C_i`.
+
+Choose a nonempty finite sequence `F_1,...,F_m`. The new productive target
+chain is `C_0,F_1,...,F_m,C_k`. Each of the `k` paid queries is replaced by
+`C_{i-1},F_1,...,F_m,C_i`. Each occurrence of an edge is charged, including
+repeated edges across different query replacements. Productive edges are
+credits and paid edges are debits. Define the gain as new minus old signed
+credit. This is a declared tariff relaxation; realizability is not assumed.
+
+Write
+
+```
+M = min_{1 <= j < k} sum_{i=1}^{k-1} phi(|s_i-s_j|).
+```
+
+**Theorem.** The maximum gain over every such path, including all ambient
+charts and all finite lengths, is exactly
+
+```
+G_max = sum_{i=1}^k phi(q_i) - phi(t) - 2 M.
+```
+
+It is attained with `m=1` and `F_1=C_j` for a minimizing internal endpoint.
+If a fixed length `m>1` is required, repeat that endpoint at every position.
+Repeated charts have zero distance. The theorem asserts attainment, not
+uniqueness. Flat tariffs can have other maximizing paths.
+
+For `k=2`, `M=0`. For `k=3`, `M=phi(q_2)`, so the exact formula is
+`phi(q_1)+phi(q_2)+phi(q_3)-phi(t)-2phi(q_2)`.
+
+## Proof
+
+For any chart F, put `S(F)=sum_{i=1}^{k-1} phi(d(C_i,F))`.
+Literal cancellation of the first and last boundary edges gives
+
+```
+G = sum_i phi(q_i) - phi(t) - S(F_1) - S(F_m)
+    - (k-1) sum_{a=1}^{m-1} phi(d(F_a,F_{a+1})).                 (1)
+```
+
+The common interior edges receive one productive credit and `k` paid debits,
+hence their coefficient is `-(k-1)`. In particular, they do not cancel as in
+the single-query contract. For `m=1`, the final sum is empty and the two
+boundary sums refer to the same chart.
+
+We prove `S(F) >= M`. Set `r_i=d(C_i,F)` for the internal endpoints. The
+triangle inequality gives `|s_i-s_j| <= r_i+r_j`. Therefore the real intervals
+`[s_i-r_i,s_i+r_i]` intersect pairwise. Finitely many intervals on the real
+line have a common point: their largest left endpoint is at most their
+smallest right endpoint. This common intersection also meets
+`[s_1,s_{k-1}]`, since each interval contains its own center in that segment.
+Choose x in both intersections. Then `|x-s_i| <= r_i` for every i, so
+
+```
+S(F) >= sum_i phi(|x-s_i|).                                  (2)
+```
+
+Between consecutive internal endpoint positions, every absolute value is an
+affine function of x with constant sign. The sum on the right of (2) is
+concave on each such segment. A concave function has a minimum at one of
+the segment's endpoints. Consequently its global minimum on
+`[s_1,s_{k-1}]` is M. A single internal endpoint is the trivial one-point
+case. Thus `S(F) >= M` for every ambient chart, including charts outside
+the original geodesic.
+
+All costs in the final sum of (1) are nonnegative. Substitution proves the
+upper bound. The constant path at a minimizing `C_j` has `S(F_1)=S(F_m)=M`
+and all interior costs zero. It attains the bound. This proves the theorem
+for arbitrary finite path length and arbitrary ambient dimension.
+
+The interval argument and concave minimization are elementary classical
+facts. The contribution here is their application to the changed multi-query
+invoice and its exact optimum, not priority for those general facts.
+
+## Consequence at rank at most nine
+
+Suppose all `q_i` are positive integers, `t<=9`, `k>=3`, and
+`phi(r)=r^(1-C)` with `0<C<=1/100`. Then **every common detour has gain
+strictly less than `-9/5`** in unnormalized rank-one tariff units.
+
+There are at least two distinct internal endpoints. At any minimizing
+endpoint at least one other endpoint has integer distance at least one,
+so `M>=1`. Write `p=1-C`. Since `q_i^p<=q_i`, the theorem gives
+
+```
+G <= t-t^p-2 <= 9-9^p-2 <= 9-9^(99/100)-2 < -9/5.
+```
+
+The middle inequality follows because `r-r^p` increases for `r>=1`.
+The last inequality is the exact integer comparison
+`44^100 < 9^99 * 5^100`. The verifier checks it directly.
+Thus this particular multi-query path contract cannot fund an improvement
+in the positive integer rank-nine domain through saving .01. No statement
+about other query graphs, unchanged source calls or different target credits
+follows from this calculation. This package does not inventory the actual
+queries of any supplier or claim that a specific caller satisfies the contract.
+
+The rank restriction matters. At `phi(r)=sqrt(r)` and query lengths `(9,1,9)`,
+the optimum is `5-sqrt(19)>0`. The verifier encloses this positive value using
+integer square roots. Nongeodesic endpoints also matter: three leaves of a
+unit-edge star have linear distance sum four at each leaf and three at the
+center. For a convex tariff, even two line terminals can have a cheaper
+interior center. These controls rule out broader median claims.
+
+## Reproduction and finite evidence
+
+Use CPython 3.12 and the standard library from the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B scripts/research_package.py --package research/consecutive-query-detour
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/consecutive-query-detour/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/consecutive-query-detour/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/consecutive-query-detour --check-source-history
+```
+
+The verifier emits a generated JSON receipt containing enumerated counts and
+SHA256 hashes of every package file. It writes no files. Redirect stdout to
+an external scratch directory to retain a receipt. Normal and optimized runs
+are registered separately. Their mathematical checks use explicit exceptions,
+so optimization does not disable them.
+
+Finite checks exhaust all integer one-point pseudometric extensions of the
+unit paths of lengths two through five with every new distance in
+`0..t+1`, and every nonempty subset of internal query endpoints. They also
+exhaust all one- and two-cut paths through the 135 three-qubit binary
+Lagrangian charts for query profiles `(1,2)`, `(2,1)` and `(1,1,1)`.
+All one-, two- and three-cut paths are checked on the 15 two-qubit charts
+for profile `(1,1)`. Every distance in the latter fixtures is computed as
+`n-log2(|L intersect L'|)` from explicit isotropic subspaces of `F_2^(2n)`.
+
+The checks compare literal paid/target invoices with (1), test the predicted
+optimum and its attaining endpoint, and test every hinge tariff on those
+integer distance domains. Every nondecreasing concave tariff on
+`0..D` with value zero at zero is a nonnegative combination of the hinges
+`min(r,h)`, `1<=h<=D`. Indeed, for successive increments `a_h`,
+its coefficients are `a_h-a_{h+1}`, with `a_{D+1}=0`.
+The coordinate domination check applies to all nondecreasing tariffs. The
+endpoint attaining M may depend on the tariff. Hinge objective checks are
+finite corroboration, not a numerical exhaustion of the nonlinear minimum
+formula over all mixtures. The written proof covers those mixtures.
+The printed counts enumerate exactly what ran. The unbounded theorem is
+proved above.
+
+The standalone checker needs no Git, network, predecessor code or selected
+supplier replay. The two source pins in SOURCES.json preserve task-selection
+provenance only. The pending predecessor README is cited at the exact head
+below and is not a runtime or proof premise of the metric theorem.
+
+All enumeration bounds are constants in the checker: path lengths at most
+three, at most 135 ambient charts, dimensions two and three, and unit paths
+of length at most five for one-point extensions. The latter enumerate
+126,114 candidate vectors. Python allocates managed objects within these
+finite domains; fixed allocation is not claimed. There is no recursion,
+network access, subprocess, or output-file mutation. All functions fit within
+60 physical lines. Standard-library warning-strict runs provide the available
+diagnostics; no separate Python static analyzer is configured for this package.
+
+## Open next questions
+
+1. Can nonconsecutive original queries, with unqueried gaps or overlaps,
+   profit from a shared replacement path? Start by retaining the signed
+   multiplicity of every boundary and interior edge. The cancellation in
+   (1) need not hold, so the present theorem does not answer that question.
+2. Can a physically legal shared graph realize independent target credits
+   with a better fully charged invoice? Start with explicit arbitrary-input
+   maps and restoration, then price each shared edge once per actual use.
+   This theorem supplies neither that graph nor its native implementation.
+
+These are also recorded in TASK.json. Native execution, phase conventions,
+independent helper inputs, retention, dirty restoration, stock/precision,
+fixed-tape movement, all-size compilation, outer admission and independent
+human/formal proof-kernel review remain unclaimed. The selected frontier and
+its five framework assumptions are unchanged.
+
+## Credit and exact predecessor
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Credit Ali Romman's
+[PR #5779 README at 071e4b8f17992846dc555502f6a38ad3dc98be08](https://github.com/aliromman/integer-mult-bounds/blob/071e4b8f17992846dc555502f6a38ad3dc98be08/research/p104-helper-detour-projection/README.md)
+for the single-query geodesic rank-metric invoice, its common-edge
+cancellation and the explicit several-query question. That source's
+single-query bound is cited, not rechecked or claimed as this result.
+The present contract changes the number of old queries to a complete
+consecutive partition, makes all of them share the replacement path, and
+retains their full edge multiplicities.
+
+Credit Joel Pulikkan/GamingPuzzled #5756/#5739, #5751, flyingviper #5718,
+zxv's moment arithmetic, #5772's canonical rank formula and the retained
+P104/native/Clifford/compiler lineage for the motivating model. No source
+code or predecessor evidence is copied or changed. Independent human and
+formal proof-kernel review are unclaimed.

research/consecutive-query-detour/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}

research/consecutive-query-detour/TASK.json

@@ -0,0 +1,111 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact signed-tariff optimum for consecutive geodesic queries sharing a common replacement path of arbitrary finite length.",
+  "scope_change_reason": "The formal-interface card is used for a new written metric interface theorem answering PR5779 Open next question 2, rather than a proof-kernel binding or an audit. The result supplies a scoped tariff obstruction; no selected assumption is discharged.",
+  "bottleneck_link": "A proposed helper split must pay for every replacement query edge. The theorem gives an exact optimistic bill for a changed multi-query contract, and excludes gain at positive integer total rank at most nine through saving .01. Physical realization remains separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact independently reproducible scoped theorem; stop if the metric formula fails. Do not extend into a source inventory or physical construction.",
+  "outcome": "completed",
+  "evidence": "README.md contains the universal proof; verify.py enumerates bounded new ambient metric, Lagrangian and signed-invoice fixtures and emits file-hash-bound JSON receipts.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can nonconsecutive queries with gaps or overlaps profit from a shared replacement path?",
+      "why_it_matters": "Their signed boundary multiplicities differ from the exact consecutive-partition cancellation.",
+      "first_step": "Write the complete signed edge invoice for two separated query intervals.",
+      "blocked_by": "No exact physical contract or shared correction bill is supplied here."
+    },
+    {
+      "question": "Can a physically legal shared graph realize independent target credits with a favorable complete invoice?",
+      "why_it_matters": "A tariff optimum does not create independent helper inputs or restore borrowed data.",
+      "first_step": "Give explicit arbitrary-input maps and dirty-restoration equations, then price each actual shared edge use.",
+      "blocked_by": "Native implementation, endpoint compatibility and complete caller costs remain unproved."
+    }
+  ],
+  "predecessors": [
+    {
+      "pr": 5779,
+      "author": "Ali Romman",
+      "head": "071e4b8f17992846dc555502f6a38ad3dc98be08",
+      "question": "Open next question 2: several original queries or non-path target graph",
+      "relationship": "Cited single-query invoice and source question; not audited, replayed or used as an executable dependency.",
+      "readme_sha256": "ee6e9559d0e730fa9ea208a8a33f188759a2434bb30697e101aaabffd93cbf06"
+    }
+  ]
+}

research/consecutive-query-detour/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact multi-query invoice cancellation and optimum, complete bounded metric extensions and Lagrangian paths, rank-nine power inequality, and hypothesis/cost controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact multi-query invoice cancellation and optimum, complete bounded metric extensions and Lagrangian paths, rank-nine power inequality, and hypothesis/cost controls."
+    }
+  ]
+}