From a30cb01ae877386d0ede459491100fc55cc28c83 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 08:03:06 +0000 Subject: [PATCH] feat(research): prove a five-stage rank floor of 13q --- .../p104-five-stage-rank-budget/README.md | 198 +++++++++++++++++ .../p104-five-stage-rank-budget/RESULT.json | 31 +++ .../p104-five-stage-rank-budget/SOURCES.json | 42 ++++ .../p104-five-stage-rank-budget/TASK.json | 110 +++++++++ .../p104-five-stage-rank-budget/VERIFY.json | 37 +++ .../p104-five-stage-rank-budget/verify.py | 210 ++++++++++++++++++ 6 files changed, 628 insertions(+) create mode 100644 research/p104-five-stage-rank-budget/README.md create mode 100644 research/p104-five-stage-rank-budget/RESULT.json create mode 100644 research/p104-five-stage-rank-budget/SOURCES.json create mode 100644 research/p104-five-stage-rank-budget/TASK.json create mode 100644 research/p104-five-stage-rank-budget/VERIFY.json create mode 100644 research/p104-five-stage-rank-budget/verify.py diff --git a/research/p104-five-stage-rank-budget/README.md b/research/p104-five-stage-rank-budget/README.md new file mode 100644 index 0000000000..7066b1171f --- /dev/null +++ b/research/p104-five-stage-rank-budget/README.md @@ -0,0 +1,198 @@ +# A 13q lower bound for five commuting full stages + +This package proves a **scoped coefficient-space rank bound**. Five distinct +compatible, pairwise commuting full stages in a shortest coupled query root +have total rank at least `13q`. Attainment is unresolved. The contribution is +the five-stage aggregation and its equality conditions, using the credited +predecessor inequalities below. It supplies no new leakage lemma or query +normal form. + +Averaging the five inherited four-stage bounds gives only `25q/2`. +The directed leakage rows raise this uniform floor to `13q`; for example, +they exclude total rank 25 at q=2 in every allowed even dimension. + +## Contract and result + +Let K be a commutative field with characteristic different from two, n >= 4 +even, and q >= 1. On nq arbitrary independent coordinates let the rank-q +square-zero queries R_0,...,R_n satisfy + +```text +(I - 2R_n) ... (I - 2R_0) = -I. +B_i = (I - 2R_i) ... (I - 2R_0). +``` + +At five distinct selected sites require idempotents P_i satisfying +`P_i R_i = R_i P_i = R_i`, `[P_i,B_i] = 0`, and pairwise commutation. +The prefix is the actual complete chronological prefix. Ordinary constant +changes of coefficient basis are allowed, including coupling of the q ports. +No assumption that internal coefficient blocks commute is added. + +Write r_i = rank(P_i). Then + +```text +sum r_i >= 13q. +``` + +If a selected site is even interior, the stronger bound is `14q`. If there +is no even interior and at most one endpoint is selected, it is `40q/3`. +Integer ranks permit rounding each bound upward. + +Equality at `13q` therefore requires both endpoints and three odd interior +sites. Their ranks, in chronological order, must be +`(2q,3q,3q,3q,2q)`. These conditions are necessary, not a construction. + +## Cited tools + +All mathematical premises in this paragraph are predecessor results, not +reproved or independently certified here. The complete coupled normal form, +the compatible-stage floor `r_i >= 2q`, and the even-interior floor +`r_i >= 4q` are in thu-nmrc's [#6717 proof](../p104-coupled-three-stage-rank-budget/PROOF.md). +CubeJerry's [#6773 note](../p104-four-stage-rigidity/FOUR-STAGE-NOTE.md) +gives the four-stage floor `10q` and the directed inequalities + +```text +2e_i + e_j >= 2q for distinct odd interior i,j, +2e_i + f_t >= 2q for a far endpoint t, +e_i = r_i - 2q, f_t = r_t - 2q, e_i,f_t >= 0. +``` + +The left endpoint 0 is far from odd i >= 3; the right endpoint n is far +from odd i <= n-3. The leakage argument originates in #6717, with ToikY's +#6721 and #6734 providing related verification and one-prefix extensions. +The normal form and image/row method retain Ali Romman's #6398 credit and +the preceding Cinna Davis query/controller lineage. Exact input blobs and +SHA256 pins are in [SOURCES.json](SOURCES.json). + +## Proof of the new aggregation + +If an even interior is selected, its rank is at least 4q and the remaining +four selected stages have total rank at least 10q. This gives 14q. + +Otherwise each selected site is an endpoint or odd interior. Let t be the +number of selected endpoints. It is 0, 1 or 2. Every case starts with base +rank 10q, so it remains to bound the extra ranks. + +For t = 0 there are five odd sites. Add both directed inequalities for +each pair to get `e_i + e_j >= 4q/3`. Summing the ten pairs counts each +extra rank four times, giving total extra rank at least 10q/3. + +For t = 1 there are four odd sites. At most one can be near the selected +endpoint. Name its extra rank a if present, and otherwise choose any odd +site's extra rank as a. Name the other three extra ranks b,c,d, all far +from the endpoint, whose extra rank is f. One third of the sum of the +three odd-pair bounds involving a gives + +```text +a + (b+c+d)/3 >= 4q/3. +``` + +One third of the sum of the three far-endpoint inequalities gives +`2(b+c+d)/3 + f >= 2q`. Adding proves total extra rank at least 10q/3. + +For t = 2, write the three odd sites as i < j < k and their extra ranks +as a,b,c. Site i is far from n, site k is far from 0, and j is far from +both endpoints. The following is an exact nonnegative combination: + +```text +(1/2)(2a + f_n >= 2q) ++ (1/2)(2c + f_0 >= 2q) ++ (1/4)(2b + f_0 >= 2q) ++ (1/4)(2b + f_n >= 2q) +--------------------------------- +a+b+c + (3/4)(f_0+f_n) >= 3q. +``` + +Nonnegativity of the endpoint extras proves the 13q bound. For equality, +the unused quarter of each endpoint extra must vanish. Thus f_0=f_n=0. +Each odd site is far from an endpoint, so each of a,b,c is at least q. +Their sum is 3q, forcing a=b=c=q. This proves the stated necessity. + +These are inequalities between integer dimensions, viewed in the real +numbers. Their rational multipliers do not divide by 3 inside K. The +argument therefore adds no characteristic restriction to the cited tools. + +## What the linear relaxation does and does not settle + +In normalized rank variables x_i = r_i/q, the directed rows are +`2x_i+x_j >= 8` and `2x_i+x_t >= 8`. The two-endpoint certificate uses +the four weights displayed above and weight 1/4 on each endpoint floor +`x_t >= 2`. Every rank coefficient becomes exactly one and the right side +is exactly 13. The zero-endpoint certificate weights every ordered odd +pair by 1/12. The one-endpoint certificate weights both directions of +each pair involving a by 1/9 and each of the three endpoint rows by 1/3. +These produce exactly 40/3. + +For two endpoints and any three odd sites, the abstract assignment +`x_end = 2`, `x_odd = 3` satisfies all these inequalities, all three-stage +floors 7 and all four-stage floors 10. Thus their linear relaxation has +minimum 13. This assignment is **not** a tuple of projectors. A stronger +uniform floor needs an additional structural implication beyond this +listed system, or a stronger inequality not listed here. + +Earlier [#6398](https://github.com/CrocSwap/integer-mult-bounds/pull/6398), +`mixed-projector-root-headroom/PROOF.md`, section 5, already gives total +rank at least 14 for five scalar stages on six fields in characteristic +zero. It excludes three rank-three interiors when both endpoints have +rank two. That stronger, narrower result is not claimed here. Likewise +[#6781](https://github.com/CrocSwap/integer-mult-bounds/pull/6781) gives +the sharp four-field four-stage value `ceil(21q/2)`. Together with the +even-site floor it already implies `4q+ceil(21q/2)` for all five sites +at n=4. The displayed 14q bound is deliberately weaker there. Neither +predecessor is replayed by this package. + +## Reproduce and verification limits + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/p104-five-stage-rank-budget/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B research/p104-five-stage-rank-budget/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-five-stage-rank-budget +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-five-stage-rank-budget --check-source-history +``` + +The absolute path records the local interpreter. A reviewer's CPython 3.12 +can replace it. The expected direct marker is `PASS_FIVE_STAGE_RANK_BUDGET`. +The receipt is generated by the verifier's explicit `--write-result` option; +ordinary replay is read-only and binds the package and cited proof hashes. + +The verifier checks exact dual sums for every five-site placement at +n=4,6,8,10,12, checks feasible abstract rank assignments in the cases +without an even interior, and rejects six false-certificate controls. +The universal proof is the case analysis above, not this finite coverage. +The checks certify the new aggregation conditional on the cited lemmas; +they do not re-audit those lemmas or verify a physical query word. + +All loops have fixed bounds from five sites and n <= 12. Files are capped +at 64 KiB. There is no recursion, dynamic code, subprocess, network or +solver in the verifier. Its checks remain enabled under `-O`. Python's +managed allocations are a Power of Ten rule-3 deviation, bounded here by +fixed fixture dimensions and file sizes; lower-level allocation control +would require a different runtime. Functions remain below 60 lines. +Validation uses warnings-as-errors and the registered normal/optimized +replays. Shared diagnostic configuration is outside this package. + +No attainment proof, search exclusion, paid invoice, physical supplier, +new κ, selected-frontier change or complete multiplication theorem is +claimed. Native routing, ownership, compiler, precision/tape and analytic +recovery obligations are outside this coefficient-space result. Independent +human and formal proof-kernel review are unclaimed. + +## Open next questions + +- Is 13q attainable for any even n >= 8 and q >= 1? Start with the forced + rank pattern above and impose compatibility and the actual prefixes + exactly. The displayed relaxation cannot decide this. A floating-point + residual alone would establish neither attainment nor exclusion. +- Can a structural argument improve the uniform lower bound above 13q? + Start with the two-endpoint equality pattern and seek a coupled analogue + of the credited scalar six-field obstruction. Arbitrary internal blocks + must remain allowed. This is not settled by the finite certificates here. + +## Credit + +New five-stage aggregation and package produced by Nick Petalas. +Predecessor credit is retained above for Ali Romman, thu-nmrc, CubeJerry, +ToikY, Cinna Davis and their query/controller lineage. No predecessor +source text or notice is edited. New work is Apache-2.0. diff --git a/research/p104-five-stage-rank-budget/RESULT.json b/research/p104-five-stage-rank-budget/RESULT.json new file mode 100644 index 0000000000..3e4aac06c6 --- /dev/null +++ b/research/p104-five-stage-rank-budget/RESULT.json @@ -0,0 +1,31 @@ +{ + "attainment": "unresolved; relaxation witnesses are not projectors", + "claim_type": "scoped-proof", + "finite_dimensions": [ + 4, + 6, + 8, + 10, + 12 + ], + "package_sha256": { + "README.md": "cb21d3ee9421fce4e585da88b2c45093127e131764ac498b6defb3456db65393", + "SOURCES.json": "5f702285cfe0ce211bd858a7e19d455793063400db6cb3c5d599da92a7cfa0c9", + "TASK.json": "947f5e5468eb2647b32d39edeb9600b6390081b22d62a60d7dd51629f0968d39", + "VERIFY.json": "6fae4c421938132fc96710cd2ced0bd3b29b780fd9e9590d39e5b9556f790bb4", + "verify.py": "d573fae2128ea54ed22326625130e936e9f472919763ab8c75c47e784170d75c" + }, + "placement_counts": { + "even": 1813, + "one-endpoint": 42, + "two-endpoints": 35, + "zero-endpoints": 7 + }, + "rejection_controls": 6, + "relaxation_primal_checks": 84, + "source_sha256": { + "research/p104-coupled-three-stage-rank-budget/PROOF.md": "9e108fdf827ffe92215be5e782f763a18968ce7613b66dfdd25a38f94958ce18", + "research/p104-four-stage-rigidity/FOUR-STAGE-NOTE.md": "952c25f3f7e211887f2bfb98d426dc8f3510d291e84ea6e9668511a06a99bf3f" + }, + "uniform_rank_lower_bound": "13q" +} diff --git a/research/p104-five-stage-rank-budget/SOURCES.json b/research/p104-five-stage-rank-budget/SOURCES.json new file mode 100644 index 0000000000..2db6db8071 --- /dev/null +++ b/research/p104-five-stage-rank-budget/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-coupled-three-stage-rank-budget/PROOF.md", + "usage": "input", + "git_blob": "7e3b89f085f1fe1f15098b75e22e370efc6ce4ce", + "sha256": "9e108fdf827ffe92215be5e782f763a18968ce7613b66dfdd25a38f94958ce18" + }, + { + "path": "research/p104-four-stage-rigidity/FOUR-STAGE-NOTE.md", + "usage": "input", + "git_blob": "b9c8f20ef73398ef1834e237e3198ceb0173e13f", + "sha256": "952c25f3f7e211887f2bfb98d426dc8f3510d291e84ea6e9668511a06a99bf3f" + }, + { + "path": "research/mixed-projector-root-headroom/PROOF.md", + "usage": "provenance", + "git_blob": "f910b5fbf9a9d519fa7d7c7503de51df5a796368", + "sha256": "68be52ab098ff9dd6edfe938e5bf36d14d5f49aa1cac94a3d0784566c05363e9" + }, + { + "path": "research/p104-four-field-sharp-rank/SHARP-BOUND.md", + "usage": "provenance", + "git_blob": "39dc118e2cab0cdeaf72bbef7a34c3692c551c18", + "sha256": "41aa74357a06eab4bcd0985dbe189b43d07cfcba4f3a091a12d3a5589d15f4e3" + } + ] +} diff --git a/research/p104-five-stage-rank-budget/TASK.json b/research/p104-five-stage-rank-budget/TASK.json new file mode 100644 index 0000000000..aac02a6e15 --- /dev/null +++ b/research/p104-five-stage-rank-budget/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "A uniform 13q lower bound and necessary equality ranks for five commuting compatible full-stage projectors in a shortest n+1-query root on nq independent inputs, n even and characteristic not two.", + "scope_change_reason": "This is a coefficient-space side result on the larger-stage rank-budget question of PR #6717, continuing the four-stage inequalities of PR #6773. It does not construct or price a native caller.", + "bottleneck_link": "A necessary aggregate stage-dimension inventory for shortest-query callers. It can rule out rank budgets below 13q within this model; no physical invoice or kappa consequence is inferred.", + "budget_minutes": 60, + "stop_rule": "Ship the five-stage lower bound with exact aggregation certificates; leave construction and sharper structural exclusions open.", + "outcome": "partial", + "evidence": "README.md gives the universal case analysis. verify.py checks exact rational dual certificates, abstract relaxation witnesses and rejection controls; RESULT.json binds its outputs to source and package hashes.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is 13q attained for any even n >= 8 and q >= 1?", + "why_it_matters": "The bound is a lower bound, not the exact projector optimum.", + "first_step": "Use both endpoints and three odd interior sites with ranks (2q,3q,3q,3q,2q), imposing exact actual-prefix commutation.", + "blocked_by": "The displayed linear rank relaxation has value 13 but does not construct projectors." + }, + { + "question": "Can a structural argument raise the uniform 13q floor?", + "why_it_matters": "No nonnegative combination of the displayed rank rows can give a larger floor at a two-endpoint placement.", + "first_step": "Analyze the forced equality profile with arbitrary coupled blocks, retaining the credited scalar six-field obstruction as a narrower predecessor.", + "blocked_by": "The scalar argument does not itself establish the all-n all-q extension." + } + ], + "environment": { + "python": "CPython 3.12.15", + "requirements": "standard library only" + }, + "overlap": { + "canonical_main": "e54523517d0f03e58352e647c403a5af3e525a57", + "priority_revision": 8, + "checked_utc": "2026-11-11T08:02:33.212790+00:00", + "open_pr_records": 467, + "discussion_records": 7089, + "local_note_coverage": "Sparse cache incomplete; additional git grep over canonical main and live merged-PR searches performed. No novelty certificate.", + "predecessors": [ + "#6717, thu-nmrc", + "#6773, CubeJerry", + "#6398, aliromman", + "#6781, CubeJerry" + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19529952", + "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19537548" + } +} diff --git a/research/p104-five-stage-rank-budget/VERIFY.json b/research/p104-five-stage-rank-budget/VERIFY.json new file mode 100644 index 0000000000..8faf8fb5ed --- /dev/null +++ b/research/p104-five-stage-rank-budget/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-coupled-three-stage-rank-budget/PROOF.md", + "research/p104-four-stage-rigidity/FOUR-STAGE-NOTE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact rank-aggregation duals on all five-site placements for n=4,6,8,10,12; feasible abstract rank assignments, six rejection controls, source and generated-receipt hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same checks with optimized Python; explicit invariant checks stay enabled." + } + ] +} diff --git a/research/p104-five-stage-rank-budget/verify.py b/research/p104-five-stage-rank-budget/verify.py new file mode 100644 index 0000000000..355e0b5f41 --- /dev/null +++ b/research/p104-five-stage-rank-budget/verify.py @@ -0,0 +1,210 @@ +#!/usr/bin/env python3 +"""Check exact aggregation certificates, not the cited projector lemmas.""" + +import argparse +import hashlib +import itertools +import json +import math +from collections import Counter +from fractions import Fraction as F +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +MAX_BYTES = 65536 +SCIENTIFIC_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def read_bytes(path): + with path.open("rb") as stream: + data = stream.read(MAX_BYTES + 1) + require(len(data) <= MAX_BYTES, f"oversized input: {path}") + return data + + +def digest(path): + return hashlib.sha256(read_bytes(path)).hexdigest() + + +def source_hashes(): + sources = json.loads(read_bytes(PACKAGE / "SOURCES.json")) + require(len(sources["files"]) == 6, "unexpected source inventory") + result = {} + for row in sources["files"]: + if row["usage"] == "input": + name = row["path"] + require(name.startswith("research/") and ".." not in name, "source path") + result[name] = digest(ROOT / name) + require(result[name] == row["sha256"], f"source mismatch: {name}") + require(len(result) == 2, "expected two cited proof inputs") + return result + + +def rank_rows(n, sites): + """Rows mean coefficient dot (rank(P_i)/q) >= rhs.""" + require(n in range(4, 13, 2), "finite fixture dimension outside declared bound") + require(len(sites) == 5 and tuple(sorted(set(sites))) == sites, "five distinct sites") + require(all(0 <= i <= n for i in sites), "site out of range") + rows = {} + for i in sites: + rows[f"floor:{i}"] = ({i: 1}, 2) + if 0 < i < n and i % 2 == 0: + rows[f"even:{i}"] = ({i: 1}, 4) + for size, floor in ((3, 7), (4, 10)): + for subset in itertools.combinations(sites, size): + rows["subset:" + ",".join(map(str, subset))] = (dict.fromkeys(subset, 1), floor) + odds = [i for i in sites if 0 < i < n and i % 2] + for i in odds: + for j in odds: + if i != j: + rows[f"odd:{i}:{j}"] = ({i: 2, j: 1}, 8) + for endpoint in (0, n): + far = (endpoint == 0 and i >= 3) or (endpoint == n and i <= n - 3) + if endpoint in sites and far: + rows[f"far:{i}:{endpoint}"] = ({i: 2, endpoint: 1}, 8) + return rows + + +def certificate(n, sites): + evens = [i for i in sites if 0 < i < n and i % 2 == 0] + if evens: + i = evens[0] + rest = ",".join(str(j) for j in sites if j != i) + return {f"even:{i}": F(1), f"subset:{rest}": F(1)}, F(14), "even" + odds = [i for i in sites if 0 < i < n and i % 2] + ends = [i for i in sites if i in (0, n)] + if not ends: + weights = {f"odd:{i}:{j}": F(1, 12) for i in odds for j in odds if i != j} + return weights, F(40, 3), "zero-endpoints" + if len(ends) == 1: + endpoint = ends[0] + near = 1 if endpoint == 0 else n - 1 + a = near if near in odds else odds[0] + far = [i for i in odds if i != a] + weights = {f"odd:{a}:{i}": F(1, 9) for i in far} + weights.update({f"odd:{i}:{a}": F(1, 9) for i in far}) + weights.update({f"far:{i}:{endpoint}": F(1, 3) for i in far}) + return weights, F(40, 3), "one-endpoint" + a, b, c = odds + weights = {f"far:{a}:{n}": F(1, 2), f"far:{c}:0": F(1, 2), + f"far:{b}:0": F(1, 4), f"far:{b}:{n}": F(1, 4), + "floor:0": F(1, 4), f"floor:{n}": F(1, 4)} + return weights, F(13), "two-endpoints" + + +def check_dual(rows, sites, weights, target): + require(len(weights) <= 20, "certificate too large") + coefficients = dict.fromkeys(sites, F(0)) + rhs = F(0) + for name, weight in weights.items(): + require(name in rows, f"uncited or inapplicable inequality: {name}") + require(weight >= 0, "negative dual weight") + row, bound = rows[name] + for site, coefficient in row.items(): + coefficients[site] += weight * coefficient + rhs += weight * bound + require(all(0 <= x <= 1 for x in coefficients.values()), "overweight rank variable") + require(rhs >= target, "overstated lower bound") + return rhs, coefficients + + +def check_primal(rows, sites, ranks, target): + require(set(ranks) == set(sites), "primal site inventory") + require(all(x >= 0 for x in ranks.values()), "negative rank") + for row, bound in rows.values(): + require(sum(coefficient * ranks[i] for i, coefficient in row.items()) >= bound, + "primal violates a cited rank inequality") + require(sum(ranks.values()) == target, "wrong primal objective") + + +def must_reject(kind, *args): + try: + if kind == "dual": + check_dual(*args) + elif kind == "primal": + check_primal(*args) + else: + raise RuntimeError("unknown rejection-control kind") + except ValueError: + return + raise ValueError("a false-certificate control was accepted") + + +def controls(): + sites = (0, 1, 3, 5, 6) + rows = rank_rows(6, sites) + weights, target, _ = certificate(6, sites) + bad = dict(weights) + bad["floor:0"] = F(-1) + must_reject("dual", rows, sites, bad, target) + bad = {name: 2 * weight for name, weight in weights.items()} + must_reject("dual", rows, sites, bad, target) + bad = dict(weights) + bad["far:1:0"] = F(1, 4) + must_reject("dual", rows, sites, bad, target) + must_reject("dual", rows, sites, weights, target + F(1, 100)) + bad_rows = dict(rows) + bad_rows["far:1:6"] = ({1: 2, 6: 1}, 7) + must_reject("dual", bad_rows, sites, weights, target) + bad_ranks = {0: F(2), 1: F(2), 3: F(3), 5: F(3), 6: F(2)} + must_reject("primal", rows, sites, bad_ranks, F(12)) + return 6 + + +def finite_checks(): + counts = Counter() + primal_count = 0 + for n in range(4, 13, 2): + for sites in itertools.combinations(range(n + 1), 5): + rows = rank_rows(n, sites) + weights, target, kind = certificate(n, sites) + rhs, coefficients = check_dual(rows, sites, weights, target) + require(rhs == target and all(x == 1 for x in coefficients.values()), + "certificate must give the displayed exact sum") + require(target >= 13, "uncovered five-stage placement") + counts[kind] += 1 + if kind != "even": + ranks = {i: F(2 if i in (0, n) else 3) for i in sites} + if kind != "two-endpoints": + ranks = dict.fromkeys(sites, F(8, 3)) + check_primal(rows, sites, ranks, target) + primal_count += 1 + require(sum(counts.values()) == sum(math.comb(n + 1, 5) for n in range(4, 13, 2)), + "placement coverage") + return dict(sorted(counts.items())), primal_count + + +def make_result(): + inputs = source_hashes() + counts, primals = finite_checks() + return {"claim_type": "scoped-proof", "uniform_rank_lower_bound": "13q", + "attainment": "unresolved; relaxation witnesses are not projectors", + "finite_dimensions": list(range(4, 13, 2)), "placement_counts": counts, + "relaxation_primal_checks": primals, "rejection_controls": controls(), + "source_sha256": inputs, + "package_sha256": {name: digest(PACKAGE / name) for name in SCIENTIFIC_FILES}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + result = make_result() + path = PACKAGE / "RESULT.json" + if args.write_result: + serialized = json.dumps(result, indent=2, sort_keys=True) + "\n" + require(path.write_text(serialized, encoding="utf-8") == len(serialized), "short receipt write") + else: + require(json.loads(read_bytes(path)) == result, "receipt mismatch") + print("PASS_FIVE_STAGE_RANK_BUDGET", json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()