From 6555bd480b70f63bfdcc9ce63f203b0061b7f242 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 12:50:41 +0000 Subject: [PATCH] feat(research): prove sharp CRT active-row placement bounds --- research/crt-active-row-extrema/PROOF.md | 127 ++++++++++++ research/crt-active-row-extrema/README.md | 109 ++++++++++ research/crt-active-row-extrema/SOURCES.json | 18 ++ research/crt-active-row-extrema/TASK.json | 99 ++++++++++ research/crt-active-row-extrema/VERIFY.json | 34 ++++ research/crt-active-row-extrema/verify.py | 197 +++++++++++++++++++ 6 files changed, 584 insertions(+) create mode 100644 research/crt-active-row-extrema/PROOF.md create mode 100644 research/crt-active-row-extrema/README.md create mode 100644 research/crt-active-row-extrema/SOURCES.json create mode 100644 research/crt-active-row-extrema/TASK.json create mode 100644 research/crt-active-row-extrema/VERIFY.json create mode 100644 research/crt-active-row-extrema/verify.py diff --git a/research/crt-active-row-extrema/PROOF.md b/research/crt-active-row-extrema/PROOF.md new file mode 100644 index 0000000000..04094e3366 --- /dev/null +++ b/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 `im. 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. diff --git a/research/crt-active-row-extrema/README.md b/research/crt-active-row-extrema/README.md new file mode 100644 index 0000000000..eec8d56414 --- /dev/null +++ b/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. diff --git a/research/crt-active-row-extrema/SOURCES.json b/research/crt-active-row-extrema/SOURCES.json new file mode 100644 index 0000000000..5335fa97d9 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/crt-active-row-extrema/TASK.json b/research/crt-active-row-extrema/TASK.json new file mode 100644 index 0000000000..da24b4c57e --- /dev/null +++ b/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" +} diff --git a/research/crt-active-row-extrema/VERIFY.json b/research/crt-active-row-extrema/VERIFY.json new file mode 100644 index 0000000000..f804162fd7 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/crt-active-row-extrema/verify.py b/research/crt-active-row-extrema/verify.py new file mode 100644 index 0000000000..fcc420fa96 --- /dev/null +++ b/research/crt-active-row-extrema/verify.py @@ -0,0 +1,197 @@ +"""Exact finite corroboration of the new CRT placement theorem. + +The all-size theorem is in PROOF.md. No predecessor executable is imported. +""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +MAX_AXES = 1 << 16 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def domain(d, ell, k): + need(type(d) is int and 2 <= d <= MAX_AXES, "axis count range") + need(d & (d - 1) == 0, "dyadic axis count") + need(type(ell) is int and 2 <= ell <= MAX_AXES, "width range") + need(type(k) is int and 0 <= k <= d, "long-axis count") + + +def extrema(d, ell, k): + """Sharp active-row extrema; integer arithmetic and no logarithm rounding.""" + domain(d, ell, k) + height = d.bit_length() - 1 + right_max = sum(min(k, d >> j) for j in range(1, height + 1)) + base = (2 * ell - 3) * (d - 1) + return base + 2 * max(0, k - 1), base + 2 * right_max + + +def placements(d, k): + domain(d, 2, k) + height = d.bit_length() - 1 + high = [] + for i in range(k): + value, reversed_bits = i, 0 + for _ in range(height): + reversed_bits = 2 * reversed_bits + (value & 1) + value >>= 1 + high.append(d - 1 - reversed_bits) + need(len(set(high)) == k, "distinct extremizing leaves") + return tuple(range(k)), tuple(high) + + +def tree_statistics(marks): + """Build the occupied tree bottom up, without the scheduler predicate.""" + d = len(marks) + domain(d, 2, 0) + need(all(type(x) is bool for x in marks), "Boolean marks") + occupied = tuple(marks) + right, branch, right_only = 0, 0, 0 + for _ in range(d.bit_length() - 1): + parents = [] + for a in range(0, len(occupied), 2): + left, child = occupied[a], occupied[a + 1] + right += child + branch += left and child + right_only += child and not left + parents.append(left or child) + occupied = tuple(parents) + return right, branch, right_only + + +def literal_schedule(widths, ell, reverse=False): + """Independent direct row/node loops implementing the declared interface.""" + d = len(widths) + domain(d, ell, 0) + need(all(type(w) is int and w in (ell - 1, ell) for w in widths), + "declared widths") + need(type(reverse) is bool, "direction flag") + need((2 * ell - 1) * (d - 1) <= 1000, "literal command capacity") + commands = [] + for level in range(1, d.bit_length()): + size = 1 << level + for row in range(2 * ell - 1): + for start in range(0, d, size): + active = False + for i in range(start + size // 2, start + size): + if widths[i] == ell or row not in (ell - 1, ell): + active = True + if active: + commands.append((level, start, row)) + return tuple(reversed(commands)) if reverse else tuple(commands) + + +def exhaustive_placements(): + placement_cases, schedule_cases, active_commands = 0, 0, 0 + for d in (2, 4, 8, 16): + minima, maxima = [None] * (d + 1), [None] * (d + 1) + for marks in product((False, True), repeat=d): + k = sum(marks) + right, branches, right_only = tree_statistics(marks) + need(branches == max(0, k - 1), "occupied branch identity") + need(right == branches + right_only, "right-only identity") + minima[k] = right if minima[k] is None else min(minima[k], right) + maxima[k] = right if maxima[k] is None else max(maxima[k], right) + for ell in (2, 3, 5): + widths = tuple(ell if x else ell - 1 for x in marks) + actual = len(literal_schedule(widths, ell)) + expected = (2 * ell - 3) * (d - 1) + 2 * right + need(actual == expected, "literal activity count") + low, high = extrema(d, ell, k) + need(low <= actual <= high, "extremal bound") + active_commands += actual + schedule_cases += 1 + placement_cases += 1 + for k in range(d + 1): + low, high = extrema(d, 2, k) + need(low == d - 1 + 2 * minima[k], "enumerated minimum") + need(high == d - 1 + 2 * maxima[k], "enumerated maximum") + return placement_cases, schedule_cases, active_commands + + +def constructive_cases(): + cases, level_cases = 0, 0 + for height in range(1, 11): + d = 1 << height + for k in range(d + 1): + low, high = placements(d, k) + for selected, expected in ((low, max(0, k - 1)), + (high, sum(min(k, d >> j) + for j in range(1, height + 1)))): + mark_set = set(selected) + marks = tuple(i in mark_set for i in range(d)) + need(tree_statistics(marks)[0] == expected, + "explicit extremizer") + for level in range(1, height + 1): + # Count distinct blocks hit by a marked right-half leaf. + hit = {x >> level for x in high if x & (1 << (level - 1))} + need(len(hit) == min(k, d >> level), "simultaneous level maximum") + level_cases += 1 + t = k.bit_length() - 1 + closed = 0 if k == 0 else (height - t - 1) * k + (1 << (t + 1)) - 1 + need(extrema(d, 2, k)[1] == d - 1 + 2 * closed, + "closed form") + cases += 1 + return cases, level_cases + + +def boundary_and_controls(): + controls = 0 + invalid = ((True, 2, 0), (1, 2, 0), (3, 2, 0), + (MAX_AXES + 1, 2, 0), (4, True, 1), (4, 1, 1), + (4, MAX_AXES + 1, 1), (4, 2, True), (4, 2, -1), (4, 2, 5)) + for args in invalid: + try: + extrema(*args) + except ValueError: + controls += 1 + else: + raise ValueError("invalid domain accepted") + for marks in ((0, 1), (False, False, False)): + try: + tree_statistics(marks) + except ValueError: + controls += 1 + else: + raise ValueError("invalid marks accepted") + need(extrema(MAX_AXES, MAX_AXES, 0)[0] == + (2 * MAX_AXES - 3) * (MAX_AXES - 1), "maximum arithmetic domain") + for d in (2, 4, 8, 16): + widths = (2,) * d + forward = literal_schedule(widths, 2) + need(literal_schedule(widths, 2, True) == tuple(reversed(forward)), + "reverse command order") + need(len(forward) == 3 * (d - 1), "all-long boundary") + need(len(literal_schedule((1,) * d, 2)) == d - 1, + "all-short boundary") + return controls + + +def main(): + placements_count, schedules, commands = exhaustive_placements() + constructors, levels = constructive_cases() + controls = boundary_and_controls() + example = extrema(16, 3, 4) + need(example == (51, 67), "displayed example") + package = Path(__file__).resolve().parent + files = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() + for name in files} + receipt = {"status": "PASS_CRT_ACTIVE_ROW_EXTREMA", + "placement_cases": placements_count, "literal_schedules": schedules, + "literal_active_commands": commands, "constructive_cases": constructors, + "constructive_level_cases": levels, "rejection_controls": controls, + "example_active_extrema": example, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()