Prove sharp mixed-width CRT active-row extrema (no κ)

research/crt-active-row-extrema/PROOF.md

@@ -0,0 +1,127 @@
+# Sharp active-row counts for a mixed-width CRT tree
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Interface and claim
+
+Jerry Chen / CubeJerry's [PR7152](https://github.com/CrocSwap/integer-mult-bounds/pull/7152),
+head `66adbede4bd4ab603ba3e0a7f6708403905b753c`, defines its schedule
+in `research/crt-whole-tree-state/tree.py`, functions `commands` and
+`WholeTree.step`. Take its activity predicate as the interface premise.
+No numerical, ROM, physical-tape or traversal theorem is reproved here.
+
+Let `d=2^h`, `h>=1`, and `ell>=2`. Each axis width is `ell-1` or `ell`.
+Let `S` be the indices of the long axes, and `k=|S|`.
+For each level `j=1,...,h`, and each aligned block of `2^j` axes, the
+schedule visits rows `0,...,2ell-2`. Every row is active except that rows
+`ell-1` and `ell` are inactive when the block's right half has no long axis.
+An inactive row makes no provider invocation in that interface.
+
+Write `F(S)` for the number of aligned right halves containing a mark in S.
+Then the exact number of active invocations in one traversal is
+
+```
+A(S) = (2ell-3)(d-1) + 2F(S).
+```
+
+The sharp extrema at fixed k are
+
+```
+min F = max(0,k-1),
+max F = sum_{j=1}^h min(k,2^(h-j)).
+```
+
+Both total bounds have explicit attaining placements described below.
+One maximizing placement attains every levelwise upper bound simultaneously.
+These are scoped all-size combinatorial statements, not
+a complete CRT cost optimum or multiplication theorem.
+
+## Exact invocation count
+
+At level j there are `d/2^j` nodes. Summing over the levels gives `d-1`.
+Each node contributes `2ell-3` ordinary rows. Its two exceptional rows
+are active exactly when its right child subtree contains a marked leaf.
+This proves the displayed formula for A, including ell=2 and k=0.
+Reversing the command order changes none of these counts, since widths
+are immutable at this boundary. A forward/reverse pair has count `2A`.
+
+## Lower bound and a minimizing placement
+
+If k=0, F=0. Suppose k>0. Prune every subtree with no marked leaf from the
+complete binary tree, retaining the original root and paths to the marks.
+In this rooted tree, let b be the number of vertices with two children,
+and let u_L and u_R count vertices retaining only their left or right child.
+The number of leaves is k. Counting edges both by outgoing degree and by
+vertices minus one gives
+
+```
+2b + u_L + u_R = b + u_L + u_R + k - 1,
+```
+
+so `b=k-1`. A vertex contributes to F exactly when it retains a right child.
+Consequently
+
+```
+F(S) = k-1 + u_R >= k-1.
+```
+
+This also characterizes equality: every occupied right child must have
+an occupied left sibling. The prefix `S={0,...,k-1}` has that property at
+every node, and therefore attains the lower bound for every k>0.
+The empty prefix attains the k=0 boundary.
+
+## Upper bound and one placement attaining every level
+
+The aligned right halves at level j are disjoint and number `2^(h-j)`.
+At most k of them can contain a mark. Thus their contribution is at most
+`min(k,2^(h-j))`, proving the sum upper bound.
+
+For an integer i in `[0,d)`, let `rev_h(i)` reverse its h binary digits,
+including leading zeros. Choose
+
+```
+S_max = {d-1-rev_h(i) : 0 <= i < k}.
+```
+
+Reversal and complementation are permutations, so these are k distinct
+valid leaves. Fix a level j and put `m=2^(h-j)`.
+For each `i<m`, bit `h-j` of i is zero. In `d-1-rev_h(i)`, bit `j-1`
+is therefore one, so this leaf lies in an aligned right half at level j.
+Its upper `h-j` bits are the complemented reversal of the lower `h-j`
+bits of i. As i ranges over `[0,m)`, these upper bits run through every
+block index once. The first m leaves therefore hit every right half
+exactly once. The first k leaves hit k different right halves if k<=m,
+and already hit all m if k>m. Their contribution is exactly `min(k,m)`.
+This argument applies to every j with the same S_max, proving attainment.
+
+For a closed form when k>0, let `t=floor(log2 k)`. Splitting the sum at
+the power-of-two capacities gives
+
+```
+max F = (h-t-1)k + 2^(t+1)-1.
+```
+
+The formula includes k=d, when it reduces to d-1. For k=0 use zero.
+
+## Consequences and limits
+
+At d=16, ell=3 and k=4, the sharp active-row extrema are 51 and 67.
+The minimizing placement is `{0,1,2,3}`; the maximizing construction
+gives `{15,7,11,3}`. The finite checker computes these values, rather than
+treating them as handwritten evidence.
+
+Each actual row can have a different cost. Width placement also changes
+node precisions and coefficient geometry. This theorem therefore does not
+minimize the complete `row_bound` sum, claim a physical saving from freely
+reordering moduli, or remove the supplied-topology implementation obligation.
+Axis/modulus transport, exact numerical providers, source preservation,
+restoration, precision, binary lowering and the five selected framework
+assumptions remain separate. No new kappa or selected-frontier change is claimed.
+
+The binary-tree identities and bit reversal are elementary combinatorial
+methods. The new contribution is their exact binding to this mixed-width
+CRT activity predicate, the sharp placement extrema and the reproducer.
+Credit CubeJerry #7152 for that predicate and caller boundary; Ali Romman
+#5353/#5625, JoyboyBrian #5053/#5219/#5092/#5496/#6100, ToikY #4195,
+Cinna Davis #4100, commdata2338 #5519 and the retained numerical, row-entry,
+workspace and CRT lineage. No predecessor executable is imported.

research/crt-active-row-extrema/README.md

@@ -0,0 +1,109 @@
+# Sharp active-row extrema for mixed-width CRT schedules
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped written combinatorial proof with exact finite corroboration.
+For `d=2^h` axes, `ell>=2` and exactly k widths equal to ell, the remaining
+widths being ell-1, the balanced schedule of
+[CubeJerry #7152](https://github.com/CrocSwap/integer-mult-bounds/pull/7152)
+has sharp active-row extrema
+
+```
+A_min = (2ell-3)(d-1) + 2 max(0,k-1),
+A_max = (2ell-3)(d-1) + 2 sum_{j=1}^h min(k,2^(h-j)).
+```
+
+The prefix placement minimizes the count. Complemented bit reversal of
+the first k leaf indices maximizes it at every level simultaneously.
+[PROOF.md](PROOF.md) derives the exact count, proves both bounds, and
+gives the equality criterion at the minimum. At d=16, ell=3 and k=4,
+the extremal active counts are 51 and 67. These are provider invocation
+counts, not measured physical execution costs.
+
+The new result isolates the effect of width order in the caller's bill.
+It does not assign equal cost to the actual calls. A legal physical axis
+permutation and a complete nonuniform numerical/ROM cost comparison remain
+necessary before claiming a speed or exponent gain. No new kappa,
+supplier admission, selected-frontier change or complete multiplier is claimed.
+
+## Reproduce
+
+From the repository root, CPython 3.12, standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/crt-active-row-extrema/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/crt-active-row-extrema/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/crt-active-row-extrema
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/crt-active-row-extrema --check-source-history
+```
+
+Any CPython 3.12 installation may replace the local interpreter path.
+The direct marker is `PASS_CRT_ACTIVE_ROW_EXTREMA`. Each invocation prints
+its computed counts and a generated receipt binding all six package files
+by SHA256. No result receipt is handwritten or stored in the checkout.
+
+The verifier compares every placement at d=2,4,8,16 against a separate
+literal node-row scheduler at ell=2,3,5. A bottom-up occupied-tree engine
+checks the counting identity, and the exhaustive minima/maxima check the
+bounds. Further constructor cases cover every k through 1,024 axes,
+including every level, the closed form and empty/full boundaries.
+Explicit exceptions remain active under optimization. The universal
+quantifier rests on the written proof; independent human and formal
+proof-kernel review are unclaimed.
+
+## Source and scope
+
+Base `e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8,
+selected #7000 at kappa 0.00363005817. The contextual task picker reported
+the older catalogue context; the selected metadata orientation passed.
+TASK.json changes `joint-query-controller` to this local scheduling question.
+[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541786).
+
+The cited interface is `commands` and `WholeTree.step` in
+[the exact #7152 source](https://github.com/CubeJerry/integer-mult-bounds/blob/66adbede4bd4ab603ba3e0a7f6708403905b753c/research/crt-whole-tree-state/tree.py).
+Only its published activity rule is a premise. No predecessor executable
+or numerical output is imported, and no predecessor verification suite is
+replayed. SOURCES.json pins repository provenance; TASK.json records the
+external source head and its observed source-file SHA256. This external
+citation is not represented as a reachable Git source pin or live replay input.
+
+Credit Jerry Chen / CubeJerry for #7152 and its mixed-width interface;
+Ali Romman #5353/#5625, JoyboyBrian #5053/#5219/#5092/#5496/#6100,
+ToikY #4195, Cinna Davis #4100, commdata2338 #5519 and their retained
+CRT, numerical, row-entry and workspace lineage. Their original credit
+lines and artifacts are unchanged. Binary-tree counting and bit reversal
+are elementary methods; no general combinatorial-method priority is claimed.
+
+## Open next questions
+
+- Can a physical caller choose a minimizing width placement at a favorable
+  complete cost? Start with one legal axis/modulus permutation, charge its
+  preparation and inverse, and compare the complete row costs. Physical
+  transport and caller compatibility are missing here.
+- Which placement minimizes the complete nonuniform numerical/ROM bill?
+  Start with the actual node precision and `row_bound` rather than a unit
+  price per active row. Legal axis order and the full objective must first
+  be specified. TASK.json records these questions and blockers.
+
+## Verification design
+
+The verifier has no recursion, subprocess, network access, imports of
+scientific packages, source rewriting or receipt files. Every function is
+under 60 physical lines. Input domains are checked explicitly: arithmetic
+helpers admit at most 65,536 axes and ell at most 65,536; the literal scheduler
+admits at most 1,000 nominal commands. Exhaustive loops use the four fixed
+sizes through sixteen axes, constructors use heights one through ten, and
+file hashing reads the six named package files. The finite input bounds are
+verification limits, not restrictions on the theorem.
+
+Power of Ten rule 3 deviation: CPython allocates integers, tuples and lists
+dynamically. The finite verifier retains at most one literal schedule of
+1,000 triples, one tree of at most 1,024 leaves in constructor checks, and
+one exhaustive Boolean placement of at most sixteen leaves. Files are
+read by a process with no writes; their actual lengths bound hash memory.
+These bounds and normal/optimized checks are the compensating controls.
+A literal fixed-storage implementation would need preallocated arrays;
+that physical implementation is outside this combinatorial package.
+Warning-strict execution and in-memory AST compilation are the local
+diagnostics. No separate static type analyzer or full numerical CRT replay
+is claimed. All five selected framework assumptions remain.

research/crt-active-row-extrema/SOURCES.json

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

research/crt-active-row-extrema/TASK.json

@@ -0,0 +1,99 @@
+{
+  "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": "Sharp all-size minimum and maximum active-row counts for every placement of k long widths in the balanced mixed-width CRT schedule of PR7152.",
+  "scope_change_reason": "Original local scheduling question at the supplied-topology boundary of PR7152. This counts calls in its fixed predicate; it does not change the historical active-mode native interface or audit a provider.",
+  "bottleneck_link": "The complete CRT caller must pay each active numerical/ROM row. The theorem identifies exactly how mixed-width placement affects the number of such calls, before assigning their unequal tariffs or paying a physical permutation.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first sharp count theorem and explicit extremizers, corroborated on every placement through sixteen axes. No provider replay or construction expansion.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-size result; verify.py independently enumerates every width placement through sixteen axes against a literal row scheduler and checks explicit extremizers and controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a legal physical CRT caller choose or change width order cheaply enough to benefit from a minimizing placement?",
+      "why_it_matters": "Fewer active rows alone does not compare unequal numerical costs or pay movement.",
+      "first_step": "Bind one actual axis/modulus permutation, charge its preparation and inverse, then compare the full row_bound sum.",
+      "blocked_by": "No physical permutation, complete source-relative tariff or outer admission is supplied."
+    },
+    {
+      "question": "Which placement minimizes the complete nonuniform numerical/ROM bill?",
+      "why_it_matters": "The active count theorem does not optimize node precision, row prices or coefficient production.",
+      "first_step": "Use the fixed source row_bound together with all widths and admitted modulus constraints, rather than replacing every active row by unit price.",
+      "blocked_by": "The complete placement objective and legal axis-order constraints must first be specified."
+    }
+  ],
+  "predecessor": {
+    "pr": 7152,
+    "author": "CubeJerry",
+    "head": "66adbede4bd4ab603ba3e0a7f6708403905b753c",
+    "path": "research/crt-whole-tree-state/tree.py",
+    "usage": "Cited published activity predicate and schedule, not an imported executable or audited result.",
+    "reference_sha256": "db13d61b5bf8e2d37273fde140d7b624daf05cbf8432aad186db527ad43f3450"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541786"
+}

research/crt-active-row-extrema/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All placements through sixteen axes, literal schedules, sharp formulas, explicit placements and rejecting controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Identical finite coverage with Python assertions disabled."
+    }
+  ]
+}