diff --git a/research/consecutive-query-detour/README.md b/research/consecutive-query-detour/README.md new file mode 100644 index 0000000000..6d4e5f8c52 --- /dev/null +++ b/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=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. diff --git a/research/consecutive-query-detour/SOURCES.json b/research/consecutive-query-detour/SOURCES.json new file mode 100644 index 0000000000..fdb80ada25 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/consecutive-query-detour/TASK.json b/research/consecutive-query-detour/TASK.json new file mode 100644 index 0000000000..84a345b03a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/consecutive-query-detour/VERIFY.json b/research/consecutive-query-detour/VERIFY.json new file mode 100644 index 0000000000..ee7d581468 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/consecutive-query-detour/verify.py b/research/consecutive-query-detour/verify.py new file mode 100644 index 0000000000..162bb8ace0 --- /dev/null +++ b/research/consecutive-query-detour/verify.py @@ -0,0 +1,269 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the consecutive-query detour theorem. + +Produced by Nick Petalas. Apache-2.0. No predecessor code is imported. +""" + +import hashlib +import itertools +import json +import math +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def check_tariff(table): + require(2 <= len(table) <= 32, "tariff size outside finite check domain") + require(table[0] == 0, "nonzero zero-rank tariff") + increments = [table[i + 1] - table[i] for i in range(len(table) - 1)] + require(all(x >= 0 for x in increments), "decreasing tariff") + require(all(a >= b for a, b in zip(increments, increments[1:])), + "nonconcave tariff") + + +def check_chain(distance, chain): + require(3 <= len(chain) <= 10, "need two to nine positive queries") + require(len(set(chain)) == len(chain), "repeated original chart") + require(all(0 <= c < len(distance) for c in chain), "chart outside domain") + positions = [0] + for a, b in zip(chain, chain[1:]): + q = distance[a][b] + require(q > 0, "nonpositive query length") + positions.append(positions[-1] + q) + for i, a in enumerate(chain): + for j, b in enumerate(chain): + require(distance[a][b] == abs(positions[i] - positions[j]), + "original queries do not form a geodesic") + return positions + + +def chain_cost(distance, path, tariff): + return sum(tariff[distance[a][b]] for a, b in zip(path, path[1:])) + + +def literal_gain(distance, chain, path, tariff): + require(1 <= len(path) <= 3, "finite checker supports one to three cuts") + old_target = tariff[distance[chain[0]][chain[-1]]] + old_paid = chain_cost(distance, chain, tariff) + new_target = chain_cost(distance, (chain[0], *path, chain[-1]), tariff) + new_paid = sum(chain_cost(distance, (a, *path, b), tariff) + for a, b in zip(chain, chain[1:])) + return new_target - old_target - new_paid + old_paid + + +def cancelled_gain(distance, chain, path, tariff): + baseline = chain_cost(distance, chain, tariff) + baseline -= tariff[distance[chain[0]][chain[-1]]] + first = sum(tariff[distance[c][path[0]]] for c in chain[1:-1]) + last = sum(tariff[distance[c][path[-1]]] for c in chain[1:-1]) + interior = chain_cost(distance, path, tariff) + return baseline - first - last - (len(chain) - 2) * interior + + +def optimum(distance, chain, tariff): + costs = [sum(tariff[distance[a][b]] for a in chain[1:-1]) + for b in chain[1:-1]] + index = costs.index(min(costs)) + 1 + value = chain_cost(distance, chain, tariff) + value -= tariff[distance[chain[0]][chain[-1]]] + 2 * min(costs) + return value, chain[index] + + +def internal_subsets(t): + require(2 <= t <= 9, "finite partition bound") + return [tuple(i for i in range(1, t) if mask >> (i - 1) & 1) + for mask in range(1, 1 << (t - 1))] + + +def one_point_extensions(): + """Every bounded integer metric extension of unit paths of lengths 2..5.""" + candidates = extensions = median_checks = 0 + for t in range(2, 6): + subsets = internal_subsets(t) + pairs = list(itertools.combinations(range(t + 1), 2)) + for radii in itertools.product(range(t + 2), repeat=t + 1): + candidates += 1 + if any(not (abs(radii[i] - radii[j]) <= j - i <= radii[i] + radii[j]) + for i, j in pairs): + continue + extensions += 1 + for sites in subsets: + low = max(sites[0], max(i - radii[i] for i in sites)) + high = min(sites[-1], min(i + radii[i] for i in sites)) + require(low <= high, "interval projection failed") + require(all(abs(low - i) <= radii[i] for i in sites), + "projection did not dominate every coordinate") + for h in range(1, t + 2): + ambient = sum(min(radii[i], h) for i in sites) + endpoint = min(sum(min(abs(i - j), h) for i in sites) + for j in sites) + require(ambient >= endpoint, "ambient median beats endpoint") + median_checks += 1 + return {"candidate_vectors": candidates, "metric_extensions": extensions, + "hinge_median_checks": median_checks} + + +def symplectic(a, b, n): + mask = (1 << n) - 1 + return (((a & mask) & (b >> n)).bit_count() + + ((b & mask) & (a >> n)).bit_count()) & 1 + + +def span(basis): + values = {0} + for v in basis: + values |= {x ^ v for x in values} + return frozenset(values) + + +def lagrangians(n): + require(n in (2, 3), "finite symplectic domain") + spaces = set() + for basis in itertools.combinations(range(1, 1 << (2 * n)), n): + if any(symplectic(a, b, n) for a, b in itertools.combinations(basis, 2)): + continue + space = span(basis) + if len(space) == 1 << n: + spaces.add(space) + return sorted(spaces, key=lambda s: tuple(sorted(s))) + + +def chart_fixture(n): + spaces = lagrangians(n) + require(len(spaces) == (15 if n == 2 else 135), "wrong chart enumeration") + distance = [[n - (len(a & b).bit_length() - 1) for b in spaces] + for a in spaces] + chain = [] + for j in range(n + 1): + basis = [1 << (i if i < j else n + i) for i in range(n)] + chain.append(spaces.index(span(basis))) + require(check_chain(distance, chain) == list(range(n + 1)), + "canonical chain distances") + for i, row in enumerate(distance): + require(row[i] == 0, "nonzero chart self-distance") + for j, dij in enumerate(row): + require(dij == distance[j][i], "asymmetric chart distance") + require(all(dij <= row[k] + distance[k][j] for k in range(len(spaces))), + "chart distance violates triangle inequality") + return distance, tuple(chain) + + +def verify_paths(distance, chain, max_cuts): + check_chain(distance, chain) + maximum_distance = max(max(row) for row in distance) + paths = invoice_checks = attainments = 0 + for h in range(1, maximum_distance + 1): + tariff = tuple(min(r, h) for r in range(maximum_distance + 1)) + check_tariff(tariff) + best, endpoint = optimum(distance, chain, tariff) + for m in range(1, max_cuts + 1): + observed = None + for path in itertools.product(range(len(distance)), repeat=m): + literal = literal_gain(distance, chain, path, tariff) + reduced = cancelled_gain(distance, chain, path, tariff) + require(literal == reduced, "literal invoice multiplicity differs") + require(literal <= best, "path beats predicted maximum") + observed = literal if observed is None else max(observed, literal) + paths += 1 + invoice_checks += 1 + require(observed == best, "enumerated maximum differs") + require(literal_gain(distance, chain, (endpoint,) * m, tariff) == best, + "constant endpoint path fails to attain") + attainments += 1 + return {"path_tariff_checks": paths, "literal_cancellations": invoice_checks, + "maxima_and_attainments": attainments} + + +def rank_nine_corollary(): + require(44 ** 100 < 9 ** 99 * 5 ** 100, "exact power threshold fails") + partitions = 0 + for t in range(3, 10): + for sites in internal_subsets(t): + if len(sites) < 2: + continue + require(all(any(abs(i - j) >= 1 for i in sites) for j in sites), + "missing unit median penalty") + positions = (0, *sites, t) + lengths = [b - a for a, b in zip(positions, positions[1:])] + require(min(lengths) >= 1 and sum(lengths) == t, "partition defect") + partitions += 1 + scale = 10 ** 12 + root = math.isqrt(19 * scale * scale) + require(root * root < 19 * scale * scale < (root + 1) ** 2, + "positive example radical enclosure") + lower = 5 * scale - root - 1 + upper = 5 * scale - root + require(lower > 0, "larger-rank positive example lost") + return {"positive_integer_partitions_k_at_least_three": partitions, + "rank_nine_gain_strict_upper": "-9/5", + "sqrt_positive_gain_interval": [f"{lower}/{scale}", f"{upper}/{scale}"]} + + +def boundary_controls(): + controls = 0 + for tariff in ((1, 2), (0, -1), (0, 1, 3), (0,)): + try: + check_tariff(tariff) + except ValueError: + controls += 1 + else: + raise ValueError("invalid tariff was accepted") + line = [[abs(i - j) for j in range(4)] for i in range(4)] + tariff = tuple(range(4)) + chain, path = (0, 1, 2, 3), (1, 2) + exact = literal_gain(line, chain, path, tariff) + wrong_interior = chain_cost(line, chain, tariff) - tariff[3] + wrong_interior -= sum(tariff[line[c][f]] for c in chain[1:-1] for f in path) + require(exact != wrong_interior, "omitted interior multiplicity escaped") + wrong_debit = chain_cost(line, (chain[0], *path, chain[-1]), tariff) + wrong_debit -= sum(chain_cost(line, (a, *path, b), tariff) + for a, b in zip(chain, chain[1:])) + wrong_debit += chain_cost(line, chain, tariff) + require(exact != wrong_debit, "omitted original target debit escaped") + controls += 2 + # Nongeodesic internal sites: three leaves, then their star center. + star = [[0 if i == j else 1 if 3 in (i, j) else 2 for j in range(4)] + for i in range(4)] + leaf_min = min(sum(star[i][j] for i in range(3)) for j in range(3)) + require(sum(star[i][3] for i in range(3)) == 3 < leaf_min == 4, + "nongeodesic counterexample") + require(1 ** 2 + 1 ** 2 < 0 ** 2 + 2 ** 2, + "convex-tariff interior counterexample") + controls += 2 + try: + check_chain(star, (0, 1, 2)) + except ValueError: + controls += 1 + else: + raise ValueError("nongeodesic query chain accepted") + return controls + + +def main(): + require(len(sys.argv) == 1, "this bounded verifier accepts no arguments") + result = {"status": "PASS_CONSECUTIVE_QUERY_DETOUR", + "claim_type": "scoped proof with finite corroboration"} + result["one_point_extensions"] = one_point_extensions() + distance, chain = chart_fixture(3) + result["three_qubit_lagrangians"] = len(distance) + profiles = ((chain[0], chain[1], chain[3]), + (chain[0], chain[2], chain[3]), chain) + result["three_qubit_profiles"] = [verify_paths(distance, c, 2) for c in profiles] + small_distance, small_chain = chart_fixture(2) + result["two_qubit_three_cut_paths"] = verify_paths(small_distance, small_chain, 3) + result["power_corollary"] = rank_nine_corollary() + result["boundary_controls"] = boundary_controls() + package = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result["sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()