From dbd82ad59d8fa0f346bb7f34b5baa731dc994880 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 23:44:56 +0100 Subject: [PATCH] feat(research): prove optimal circular Schur ordering --- research/cycle-schur-optimal-order/PROOF.md | 101 ++++++++++ research/cycle-schur-optimal-order/README.md | 127 ++++++++++++ .../cycle-schur-optimal-order/SOURCES.json | 36 ++++ research/cycle-schur-optimal-order/TASK.json | 81 ++++++++ .../cycle-schur-optimal-order/VERIFY.json | 32 +++ research/cycle-schur-optimal-order/verify.py | 190 ++++++++++++++++++ 6 files changed, 567 insertions(+) create mode 100644 research/cycle-schur-optimal-order/PROOF.md create mode 100644 research/cycle-schur-optimal-order/README.md create mode 100644 research/cycle-schur-optimal-order/SOURCES.json create mode 100644 research/cycle-schur-optimal-order/TASK.json create mode 100644 research/cycle-schur-optimal-order/VERIFY.json create mode 100644 research/cycle-schur-optimal-order/verify.py diff --git a/research/cycle-schur-optimal-order/PROOF.md b/research/cycle-schur-optimal-order/PROOF.md new file mode 100644 index 0000000000..dc7710aef0 --- /dev/null +++ b/research/cycle-schur-optimal-order/PROOF.md @@ -0,0 +1,101 @@ +# Optimal ordering of a one-arc circular Schur complement + +Let n >= 3, 1 <= w <= floor(n/2), and let a nonempty proper contiguous arc +of the n-cycle be eliminated. Write M >= 1 for the surviving count. Label +the surviving path by 0,...,M-1 in its inherited cyclic orientation. +Half-bandwidth in an order p is max |p(i)-p(j)| over nonzero off-diagonal +entries, with value zero for a singleton. + +**Theorem.** For any matrix supported on the circular radius-w band, if +the eliminated principal block is invertible, its Schur complement admits a +simultaneous row/column order of half-bandwidth at most min(M-1,2w). +For the full negative host H=I-E, where E has zero diagonal, strictly positive +entries at every circular distance 1,...,w, zero entries outside the band, +and every row sum is less than one, this is the exact minimum over all orders. +Equal off-diagonal magnitudes are unnecessary. + +The new result is the optimal ordering and its matching lower bound. The +negative-sign/no-cancellation argument is credited to James Reed / jwr404's +[PR #4289](https://github.com/CrocSwap/integer-mult-bounds/pull/4289), following +[#4286](https://github.com/CrocSwap/integer-mult-bounds/pull/4286). +Those packages leave survivor reordering open. This theorem makes no claim +about the physical price of the permutation or the Gaussian caller's order. + +## 1. Identify the survivor support graph + +Put B={0,...,min(w,M)-1} union {max(0,M-w),...,M-1}. +The survivors touching the eliminated arc are exactly B. A path from a +survivor to the arc first crosses one of the two surviving endpoints, so +the minimum circular distance to the arc is min(i+1,M-i). + +For an arbitrary band-supported matrix, the Schur update can couple only +pairs in B. An original coupling between i=0) E_A^k. All terms are nonnegative, and every entry is positive: +the arc is connected by the strictly positive nearest-neighbor entries. +Therefore each pair in B receives a strictly negative Schur update. Every +original in-band edge is strictly negative and cannot cancel this update. +Edges with j-i <= w are original edges. Hence this host's support is exactly +G_(M,w). This uses the predecessor's sign argument as a premise and derives +the explicit path-plus-end-clique graph needed for the new ordering theorem. + +## 2. A folded order attains the upper bound + +Use the vertex order + + 0, M-1, 1, M-2, 2, M-3, ... + +with the middle vertex written only once. If p(i) is its zero-based position, + + p(i)=2i if i < ceil(M/2), + p(i)=2(M-1-i)+1 otherwise. + +Consecutive surviving-path vertices have position differences at most two, +including the central pair. Summing these adjacent differences gives +|p(i)-p(j)| <= 2|i-j|. Every path-power edge therefore spans at most 2w. + +If M >= 2w, B occupies exactly the first 2w positions of this order, so its +clique spans at most 2w-1. If M < 2w, B is the entire graph and every edge +spans at most M-1. These bounds prove min(M-1,2w) for all edges. A simultaneous +permutation changes entries' locations only, so it preserves this support +bound for arbitrary coefficients and any cancellations. + +## 3. No order improves the constant on the full negative host + +In any linear vertex order of half-bandwidth b, the first vertex has degree +at most b. Thus b is at least the graph's minimum degree. + +If M <= 2w, B contains every vertex, so G_(M,w) is complete and its minimum +degree is M-1. + +If M >= 2w+1, B consists of two disjoint w-vertex strips. A vertex outside B +has exactly 2w path-power neighbors. A vertex in B has 2w-1 other clique +vertices and at least one neighbor outside B: vertex w for the left strip, +or vertex M-w-1 for the right strip. Its degree is therefore at least 2w. +There is at least one vertex outside B, so the minimum degree is exactly 2w. +The folded upper bound and this degree lower bound coincide. + +For example, M=9 and w=2 give exact minimum four, while the inherited linear +survivor order has bandwidth eight. The same graph shows that the linear +separated-carve constant 2w-1 cannot replace 2w in this circular problem. +This is an optimal reordering result, not a disagreement with the +predecessor's bandwidth measured in circular distance. + +## Scope + +The proof covers all sizes in the stated matrix class. Finite checks only +corroborate the graph identification and ordering; they are not a proof of +these quantifiers. An arbitrary invertible arc block gives the upper bound; +full negative support and the row-sum condition give the sharp lower bound. +Zero or signed couplings can have smaller minima. Multiple eliminated arcs +can join different support components and are outside this theorem. Row/column +routing costs, ownership, inverse norms, rounded arithmetic, tape layout, +compiler/hosting, supplier admission and a new kappa are unclaimed. No +independent human or formal proof-kernel review is claimed. No literature +priority is claimed for folding a path or the minimum-degree bandwidth bound. diff --git a/research/cycle-schur-optimal-order/README.md b/research/cycle-schur-optimal-order/README.md new file mode 100644 index 0000000000..24a84a7646 --- /dev/null +++ b/research/cycle-schur-optimal-order/README.md @@ -0,0 +1,127 @@ +# Exact optimal ordering after a circular arc is eliminated + +**Scoped proof with finite corroboration.** For a full negative circular band +of radius w, eliminate one nonempty proper arc and retain M vertices. The +exact minimum Schur half-bandwidth over simultaneous row/column orders is + + min(M-1, 2w). + +The order `0, M-1, 1, M-2, ...` attains it. In the resulting support graph, +the minimum degree gives the matching lower bound. With M=9 and w=2, this +changes the inherited linear survivor bandwidth from eight to four. No +ordering reaches three. For arbitrary coefficients supported on the same +circular band and any invertible arc pivot, the same order gives the upper +bound; cancellations can reduce the optimum. + +This answers the survivor-reordering question left open by James Reed / +jwr404's [PR #4289](https://github.com/CrocSwap/integer-mult-bounds/pull/4289). +The new contribution is an optimal linear order and its sharp constant. +The predecessor's sign/no-cancellation argument is a credited premise, not a +validation deliverable. [PROOF.md](PROOF.md) gives the complete all-size +argument and precise negative-host hypotheses. No predecessor executable is +imported or replayed. No literature-priority claim is made for path folding +or the elementary minimum-degree bandwidth bound. + +## Evidence and reproduction + +From the repository root, CPython 3.12, standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cycle-schur-optimal-order +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/cycle-schur-optimal-order/verify.py +``` + +On another checkout, substitute its Python 3.12 interpreter. Both registered +commands, warning-strict normal and optimized execution, emit +`PASS_CYCLE_SCHUR_OPTIMAL_ORDER`. Normal verification writes no files. Each +execution prints a generated receipt with SHA256 hashes of all six package +files. `verify.py --write-receipt NEW_PATH` additionally writes it to a new +external path and refuses overwrite. No hand-written receipt is committed. +The direct verifier is self-contained and works without Git or repository +inputs. Generic metadata/source-history checks require the pinned Git history. + +The bounded checks enumerate: + +- 4,656 graph/radius pairs through M=96, including 8,403,952 edge occurrences, + checking the folded order and exact minimum-degree floor. +- All 362,879 vertex permutations for all 36 graph/radius pairs through M=8. + This separate direct evaluator uses no folded-order or degree-bound pruning. +- 651 circular layouts through n=16, one representative for each radius and + eliminated-arc length. Literal graph vertex elimination independently checks + the new path-power-plus-end-clique support identification and folded order. +- Nine invalid-input rejections and four semantic controls for the old order, + an incorrect `2w-1` cap, omitted clique fill, and saturation at M-1. + +These are finite corroboration of the new theorem. No numeric matrix census, +predecessor reproduction, physical schedule, benchmark or full selected replay +is claimed. The all-size claim rests on the written proof. The selected +conditional kappa remains 0.00302015. + +## Scope and source closure + +The negative host is H=I-E with zero diagonal in E, strictly positive entries +at every circular distance from one through w, zero entries elsewhere, and +row sums less than one. This guarantees connected positive inverse fill and +prevents cancellation. Arbitrary invertible arc pivots need only the stated +support condition for the upper bound. Signed or missing couplings do not +inherit the sharp lower bound. + +The original `uniform-transfer-audit` card is explicitly changed to this +ordering theorem, following another contributor's open question. It is a local +interface result, not an audit of #4100. Physical row and right-hand-side +permutations, routing, restoration, multiple arcs, inverse norms, precision, +tape access, compiler/hosting and complete supplier costs remain open. No +supplier admission, new kappa or complete multiplication theorem is supplied. +Independent human and formal proof-kernel review are unclaimed. + +Base canonical main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. [SOURCES.json](SOURCES.json) pins historical task/selected provenance +and the exact credited predecessor notes. No external executable or data input +is required by the new verifier. The selected-source metadata orientation +passed; it was not the selected scientific cold replay. + +Entry overlap used live open PRs, this account's recent submissions, current +handoffs, local question locks, distinctive all-main README searches and merged +PR searches. The cached card scan reported sparse-note omissions. Arbitrary +diffs and unpublished work remain outside coverage; no-match searches do not +establish novelty. [The claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134026) +preceded the substantive work. Research stops at this first proved result. + +## Verification design + +Build the Lever led to a rerunnable ordering and exhaustive optimum checker. +Prove It Works led to independent direct permutation evaluation and literal +circular graph elimination. Power of Ten bounds graph size at 96 vertices, +permutation enumeration at eight, and circular elimination at sixteen. Every +loop has a bound from those constants; functions remain below 60 lines; +rejection checks remain active under optimization. Python's managed allocation +is a documented deviation from fixed allocation: one graph has at most 4,560 +edge tuples, the literal adjacency table has at most 256 booleans, and brute +orders are streamed. Package source files are fixed local inputs. Python's +allocator and standard-library internals are outside inspection. There is no +recursion, dynamic code generation, shared mutable state or native dependency. +Warning-strict Python and the repository metadata/publication checks are the +available diagnostics; no separate linter is installed in the supplied venv. + +## Open next questions + +Can the folded order be realized in one actual circular Gaussian boundary +solve within its complete paid routing allowance? First bind both permutation +directions, all right-hand sides and eventual restoration in a literal caller. +This matters because a smaller algebraic band does not pay for moving data. +No physical conversion or complete caller is constructed here. + +Which multiple-arc elimination layouts retain an O(w) optimal linear bandwidth? +First specify a separation rule and derive the survivor support. This matters +because merged eliminated components can create larger cliques. The present +one-arc theorem does not decide that case. Structured versions of both questions +are in [TASK.json](TASK.json). + +## Credit + +This contribution is produced by Nick Petalas. James Reed / jwr404's #4289, +following #4286, supplies the circular-arc sign/support argument and the explicit +open reordering question. Cinna Davis's #4100 supplies the Gaussian boundary +motivation. unpaidmoon's #4373 and Ryanson Jonathan's #4407 address linear +separated carves and support fill; their `2w-1` constant has different +hypotheses. Their source files and credit lines are unchanged. Apache-2.0. diff --git a/research/cycle-schur-optimal-order/SOURCES.json b/research/cycle-schur-optimal-order/SOURCES.json new file mode 100644 index 0000000000..30c10f3857 --- /dev/null +++ b/research/cycle-schur-optimal-order/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/equal-weight-cycle-diameter/README.md", + "usage": "provenance", + "git_blob": "2f7c1c001caa12a26fcdafd0f060f9cbeb210502", + "sha256": "c41e951fa788783c522a2c223a850534b0a86ff04c60690409d1eb658f86a130" + }, + { + "path": "research/gaussian-carve-schur-bandwidth/README.md", + "usage": "provenance", + "git_blob": "cebb6a30cc0859822dd256dee78f54ca97fa238d", + "sha256": "31b2930d6c140c526ff2fe0a68216b1ff17d22df9ef4a3c518079037e86b232a" + }, + { + "path": "research/carve-schur-bandwidth-census/README.md", + "usage": "provenance", + "git_blob": "525387652dfb847f05b76d3e98aea653ee35749e", + "sha256": "e95963d7bcae7c052ddb16d086f6405b8aaee628930528d6799cc965d85b8dc9" + } + ] +} diff --git a/research/cycle-schur-optimal-order/TASK.json b/research/cycle-schur-optimal-order/TASK.json new file mode 100644 index 0000000000..f7926b0650 --- /dev/null +++ b/research/cycle-schur-optimal-order/TASK.json @@ -0,0 +1,81 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact minimum linear-order Schur half-bandwidth after one nonempty proper circular arc: min(M-1,2w).", + "scope_change_reason": "Original all-size caller-audit card changed to an original graph/order theorem answering the survivor-reordering question in another contributor's PR4289. No predecessor replay or audit is the deliverable.", + "bottleneck_link": "A circular-distance fill can grow with arc length; an explicit simultaneous permutation restores a sharp O(w) linear band. Physical permutation cost and actual Gaussian caller integration remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved optimal order and bounded exact corroboration; do not extend to multiple arcs or a physical implementation.", + "outcome": "completed", + "evidence": "PROOF.md and the source-hash-bound runtime receipt emitted by verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the folded order be realized in one actual circular Gaussian boundary solve within its paid routing allowance?", + "why_it_matters": "An algebraic bandwidth improvement does not pay for rearranging the data.", + "first_step": "Choose one literal caller, bind both permutation directions and all right-hand sides, then price their complete movement and restoration.", + "blocked_by": "No physical order conversion or complete caller is supplied here." + }, + { + "question": "Which multiple-arc elimination layouts retain an O(w) optimal linear bandwidth?", + "why_it_matters": "Merged eliminated components may create larger survivor cliques.", + "first_step": "Specify a separation rule and derive its exact survivor support before searching for an order.", + "blocked_by": "The present theorem has exactly one eliminated arc." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134026" +} diff --git a/research/cycle-schur-optimal-order/VERIFY.json b/research/cycle-schur-optimal-order/VERIFY.json new file mode 100644 index 0000000000..cb8f15ec35 --- /dev/null +++ b/research/cycle-schur-optimal-order/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact folded orders and degree floors through M=96; every permutation through M=8; independent circular graph elimination through n=16; invalid-input and semantic controls; source-hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact folded orders and degree floors through M=96; every permutation through M=8; independent circular graph elimination through n=16; invalid-input and semantic controls; source-hash-bound receipt." + } + ] +} diff --git a/research/cycle-schur-optimal-order/verify.py b/research/cycle-schur-optimal-order/verify.py new file mode 100644 index 0000000000..f9196c4c13 --- /dev/null +++ b/research/cycle-schur-optimal-order/verify.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the new ordering theorem; standard library only.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +MAX_VERTICES = 96 +MAX_BRUTE_VERTICES = 8 +MAX_CYCLE_VERTICES = 16 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def domain(m, w): + require(type(m) is int and type(w) is int, "integer dimensions required") + require(1 <= m <= MAX_VERTICES, "survivor count outside verifier domain") + require(1 <= w <= MAX_VERTICES, "radius outside verifier domain") + + +def graph(m, w): + """Path power plus the clique on the two end strips.""" + domain(m, w) + boundary = set(range(min(w, m))) | set(range(max(0, m - w), m)) + return tuple( + (i, j) + for i in range(m) + for j in range(i + 1, m) + if j - i <= w or (i in boundary and j in boundary) + ) + + +def folded_order(m): + domain(m, 1) + return tuple(k // 2 if k % 2 == 0 else m - 1 - k // 2 for k in range(m)) + + +def bandwidth(order, edges): + m = len(order) + require(1 <= m <= MAX_VERTICES, "ordering size outside verifier domain") + require(all(type(v) is int for v in order), "ordering entries must be integers") + require(sorted(order) == list(range(m)), "ordering is not a permutation") + require(all(0 <= i < j < m for i, j in edges), "invalid undirected edge") + positions = [0] * m + for rank, vertex in enumerate(order): + positions[vertex] = rank + return max((abs(positions[i] - positions[j]) for i, j in edges), default=0) + + +def ordering_checks(): + count = 0 + edge_count = 0 + for m in range(1, MAX_VERTICES + 1): + for w in range(1, m + 1): + edges = graph(m, w) + target = min(m - 1, 2 * w) + degrees = [0] * m + for i, j in edges: + degrees[i] += 1 + degrees[j] += 1 + require(min(degrees) == target, f"minimum-degree floor: {m},{w}") + require(bandwidth(folded_order(m), edges) == target, + f"folded upper bound: {m},{w}") + count += 1 + edge_count += len(edges) + return {"graphs": count, "undirected_edges": edge_count} + + +def brute_checks(): + """All orders, with no degree bound or folded-order pruning.""" + graphs = 0 + orders = 0 + for m in range(1, MAX_BRUTE_VERTICES + 1): + for w in range(1, m + 1): + edges = graph(m, w) + best = m + for order in itertools.permutations(range(m)): + # Independent direct evaluation, without bandwidth(). + labels = dict(zip(order, range(m), strict=True)) + measured = 0 + for i, j in edges: + measured = max(measured, abs(labels[i] - labels[j])) + best = min(best, measured) + orders += 1 + require(best == min(m - 1, 2 * w), f"exhaustive optimum: {m},{w}") + graphs += 1 + return {"graphs": graphs, "permutations": orders} + + +def literal_fill(n, w, killed): + """Combinatorial vertex elimination on the original circular graph.""" + require(3 <= n <= MAX_CYCLE_VERTICES and 1 <= w <= n // 2, + "invalid circular graph") + require(1 <= killed < n, "the eliminated arc must be nonempty and proper") + adjacent = [[False] * n for _ in range(n)] + for i in range(n): + for j in range(n): + distance = min(abs(i - j), n - abs(i - j)) + adjacent[i][j] = 0 < distance <= w + for k in range(killed): + remaining_neighbors = [i for i in range(k + 1, n) if adjacent[k][i]] + for i in remaining_neighbors: + for j in remaining_neighbors: + if i != j: + adjacent[i][j] = True + return tuple( + (i - killed, j - killed) + for i in range(killed, n) + for j in range(i + 1, n) + if adjacent[i][j] + ) + + +def support_checks(): + layouts = 0 + for n in range(3, MAX_CYCLE_VERTICES + 1): + for w in range(1, n // 2 + 1): + for killed in range(1, n): + edges = literal_fill(n, w, killed) + require(edges == graph(n - killed, w), + f"circular support identification: {n},{w},{killed}") + require(bandwidth(folded_order(n - killed), edges) + == min(n - killed - 1, 2 * w), "circular ordering") + layouts += 1 + return {"circular_layouts": layouts} + + +def controls(): + invalid = ((0, 1), (97, 1), (3, 0), (3, 97), (True, 1), (3, 1.0)) + rejected = 0 + for m, w in invalid: + try: + graph(m, w) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid graph domain accepted") + for order, edges in (((0, 0), ()), ((0, True), ()), ((0, 1), ((1, 0),))): + try: + bandwidth(order, edges) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid ordering or edge accepted") + # Semantic mutants: retaining the path, the old order, or a 2w-1 cap. + edges = graph(9, 2) + require(bandwidth(tuple(range(9)), edges) == 8, "old-order control") + require(bandwidth(folded_order(9), edges) == 4, "changed-order control") + require(bandwidth(folded_order(9), edges) > 2 * 2 - 1, "sharp constant") + require(bandwidth(tuple(range(9)), tuple((i, j) for i, j in edges if j-i <= 2)) + == 2, "omitted-fill control") + # Saturation uses M-1, rather than 2w, when M <= 2w. + require(bandwidth(folded_order(4), graph(4, 2)) == 3, "saturation control") + return {"invalid_inputs_rejected": rejected, "semantic_controls": 4} + + +def receipt(): + package = Path(__file__).resolve().parent + checks = { + "ordering": ordering_checks(), + "exhaustive": brute_checks(), + "support": support_checks(), + "controls": controls(), + } + names = ("verify.py", "PROOF.md", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in names} + return {"claim_type": "scoped proof with finite corroboration", "checks": checks, + "source_sha256": hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + encoded = json.dumps(receipt(), indent=2, sort_keys=True) + "\n" + if args.write_receipt is not None: + with args.write_receipt.open("x", encoding="utf-8") as stream: + written = stream.write(encoded) + require(written == len(encoded), "short receipt write") + print(encoded, end="") + print("PASS_CYCLE_SCHUR_OPTIMAL_ORDER") + + +if __name__ == "__main__": + main()