petalas · Nov 11, 2026
diff --git a/research/p104-five-stage-rank-budget/README.md 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
@@ -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
@@ -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
@@ -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"
+  }
+}