From 17e0213f31725315c476792fd282bd201ff4c4ac Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 12:52:20 +0000 Subject: [PATCH] feat(research): prove the minimum two-pass width obstruction --- research/two-pass-width-obstruction/PROOF.md | 136 +++++++++++ research/two-pass-width-obstruction/README.md | 140 +++++++++++ .../two-pass-width-obstruction/SOURCES.json | 30 +++ research/two-pass-width-obstruction/TASK.json | 88 +++++++ .../two-pass-width-obstruction/VERIFY.json | 34 +++ research/two-pass-width-obstruction/verify.py | 220 ++++++++++++++++++ 6 files changed, 648 insertions(+) create mode 100644 research/two-pass-width-obstruction/PROOF.md create mode 100644 research/two-pass-width-obstruction/README.md create mode 100644 research/two-pass-width-obstruction/SOURCES.json create mode 100644 research/two-pass-width-obstruction/TASK.json create mode 100644 research/two-pass-width-obstruction/VERIFY.json create mode 100644 research/two-pass-width-obstruction/verify.py diff --git a/research/two-pass-width-obstruction/PROOF.md b/research/two-pass-width-obstruction/PROOF.md new file mode 100644 index 0000000000..0db9da4ba1 --- /dev/null +++ b/research/two-pass-width-obstruction/PROOF.md @@ -0,0 +1,136 @@ +# A minimum-order failure of the width-product test + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Model and exact statement + +Records are distinct, initially ordered 0,...,n-1. A stable two-lane pass +assigns each record to one of two lanes and produces any interleaving of +the resulting streams that preserves each lane's incoming order. Empty +lanes are allowed. Records cannot be copied, deleted or modified. Routing +descriptions are unrestricted; this model charges passes only. + +For a target record order p, let w(p) be its longest decreasing-subsequence +length. The following claims have different evidence: + +1. The ten-record order p=(3,2,1,6,5,4,9,8,7,0) has w(p)=4 and needs + exactly three stable two-lane passes. The arguments below are written + combinatorial proofs; two separate finite exclusion engines corroborate + the lower bound. +2. No order of at most nine records with w<=4 needs more than two passes. + This is an exhaustive finite certificate at n=9, followed by restriction + of its routes. Thus ten is the minimum possible order of an obstruction + to sufficiency of the two-pass width-product bound four. + +The universal width-product necessity and its general failure of +sufficiency are prior work. In particular Mark Karpilovskij, +[Composability of Permutation Classes, Theorem 15 and Question 16](https://www.combinatorics.org/ojs/index.php/eljc/article/view/v26i1p41), +Electronic Journal of Combinatorics 26(1), P1.41, 2019, already states +I_k I_l is strictly smaller than I_(kl), where I_k is the class of +permutations partitionable into k increasing subsequences. That known +noninclusion is not claimed as new. The new repository result is this +explicit minimum-order certificate and routing obstruction. No historical +priority claim is made for the example or elementary methods. + +## One-pass alphabet + +A record order can be produced in one pass if and only if w<=2. +Necessity follows because a decreasing triple cannot share two stable +lanes. For sufficiency, assign each entry its longest decreasing-subsequence +length ending there. If an inverted pair had the same depth, appending +the second entry to a decreasing subsequence ending at the first would +increase its depth. Each of the at most two depth classes is therefore +in increasing record order and is a legal incoming lane stream. + +If the first pass outputs record order a and the second uses the sequence +b of indices into that order, the final record order is a[b[i]]. Both a +and b must avoid a decreasing triple. Conversely any such pair supplies +two legal passes. This fixes the composition convention used by the checker. + +## A forced four-cycle rules out two passes + +Suppose a two-pass route exists for the displayed p. Give each record +its ordered pair of lane choices. Two records with the same pair retain +their initial relative order through both passes. Relabel the lanes of +each pass so that record 0 has pair 00. Every other record finishes before +0, although it starts after 0. Consequently none can have pair 00. + +Each of the blocks {1,2,3}, {4,5,6} and {7,8,9} is reversed in p. +Its three records must have distinct pairs. They therefore use exactly +01,10,11, once each. Choose A with pair 01 in the first block, C with +pair 11 in the second block, and B with pair 10 in the third block. +Write <_M for the total order after the first pass. + +- Record 0 and A share first lane 0. Their initial order forces 0 <_M A. +- A and C share second lane 1. Their final block order forces A <_M C. +- C and B share first lane 1. Their initial block order forces C <_M B. +- B and 0 share second lane 0. Their final order forces B <_M 0. + +This is the impossible cycle 0 <_M A <_M C <_M B <_M 0. +It covers every lane assignment and every intermediate merge, including +empty lanes and choices dependent on the complete layout. No search +assumption or restriction on merge positions enters the argument. + +The width is exactly four. A decreasing subsequence before the terminal +0 stays inside one of the three value-separated blocks, so it has at most +three records. Appending 0 permits four, for example 3,2,1,0. + +## Three passes attain the endpoint + +The following complete orders and lane-1 record sets describe the route. +The other lane contains every remaining record. + +| Pass | Output record order | Lane-1 records | +|---|---|---| +| 1 | 1,2,3,4,5,6,7,8,9,0 | 0 | +| 2 | 2,1,3,5,4,6,8,7,9,0 | 2,5,8 | +| 3 | 3,2,1,6,5,4,9,8,7,0 | 3,6,9 | + +For each row, both lane subsequences in the preceding order are identical +to those in the output. Hence every pass is legal. All record payloads +are transported intact. The lower bound makes this three-pass route optimal. + +## Finite certificate that smaller obstructions do not exist + +The checker generates the complete one-pass alphabet at order nine by +inserting the largest record into every smaller generated permutation. +A new decreasing triple must begin with that largest record. It exists +exactly when the suffix following the insertion contains a decreasing +pair. Thus the insertion is permitted precisely when that suffix is +increasing. Removing the largest record gives a unique predecessor, so +induction proves completeness and absence of duplicates. + +A separately implemented scan of all 9!=362,880 permutations tests every +literal triple. Its one-pass set agrees exactly with the 4,862 generated +factors. The checker composes all 4,862^2=23,639,044 ordered factor pairs +and retains their complete set of final orders. Independently, a quadratic +longest-decreasing-subsequence dynamic program scans all 362,880 orders +and retains those of width at most four. The two sets are exactly equal, +with 261,808 elements. This set equality is the finite minimum-order +certificate; the count alone would not establish coverage. + +For an order on n<9 records, append the remaining larger records in +increasing order. Its width stays at most four. The nine-record certificate +provides a two-pass route for this extension. Remove the appended records +from the initial, intermediate and final orders and from both lane streams. +Restriction preserves their relative orders, giving two passes on the +original records. Hence no smaller order is an obstruction. This argument +does not construct a uniform all-size routing controller from a width test. + +As a second exclusion engine, every one of the 16,796 complete one-pass +factors a at order ten is tested. The unique possible second factor is +b=a^-1 p, and its decreasing width is always greater than two. This +corroborates the four-cycle proof without depending on the lane-type +argument. The verifier also visits all 4^9 normalized two-pass lane +assignments for p. Exactly 216 survive the necessary inverted-pair test; +every survivor has the displayed four-cycle, and an independently built +order graph is cyclic in every case. + +## Scope + +This is a finite routing certificate and a scoped combinatorial proof. +It supplies no physical stream controller, tape/head cost, workspace or +reversible cleanup implementation. More lanes, additional passes, record +copies, random access, a different routing model or a changed layout can +escape this obstruction. It is not an unconditional multitape lower bound, +a native supplier, an improved kappa, or a complete multiplication theorem. diff --git a/research/two-pass-width-obstruction/README.md b/research/two-pass-width-obstruction/README.md new file mode 100644 index 0000000000..d948bcdea7 --- /dev/null +++ b/research/two-pass-width-obstruction/README.md @@ -0,0 +1,140 @@ +# Smallest failure of the two-pass width budget + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: finite certificate with a scoped combinatorial proof. The layout + +```text +3,2,1,6,5,4,9,8,7,0 +``` + +has decreasing-subsequence width four but requires exactly **three** stable +two-lane passes. A forced four-cycle excludes every possible two-pass +intermediate order. Three explicit passes attain the endpoint. Every layout +of at most nine records with width at most four does admit two passes, so +ten records is the minimum size of a failure of the width-product test. + +A pass assigns each intact record to one of two order-preserving streams, +then merges them in any stable interleaving. Empty lanes and arbitrary +routing choices are allowed. No payload copies, deletions, extra lanes or +random access are supplied. This is an abstract pass count, with no physical +unit-time assertion about streams or tapes. + +[PROOF.md](PROOF.md) gives the four-cycle argument and the exact finite +minimum-order reduction. It also gives the full attaining route: + +```text +0 1 2 3 4 5 6 7 8 9 +1 2 3 4 5 6 7 8 9 0 +2 1 3 5 4 6 8 7 9 0 +3 2 1 6 5 4 9 8 7 0 +``` + +## Reproduction and evidence + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/two-pass-width-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/two-pass-width-obstruction/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/two-pass-width-obstruction +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/two-pass-width-obstruction --check-source-history +``` + +Another CPython 3.12 path can replace the displayed interpreter. The direct +marker is `PASS_TWO_PASS_WIDTH_OBSTRUCTION`; the runner returns +`PASS_REGISTERED_RESEARCH_PACKAGE`. The verifier writes no files. Its stdout +receipt is generated from the actual calculations and hashes all six package +files. Normal and optimized executions perform the same checks. + +The minimum-order certificate compares complete sets, not only counts. +It enumerates all 362,880 permutations of nine records, independently +identifies the 4,862 one-pass factors, composes all 23,639,044 ordered pairs, +and obtains exactly the 261,808 width-at-most-four layouts. Restriction of +those routes settles every smaller size. All ten single-record deletions +of the new obstruction also lie in that complete two-pass set. + +Two different exclusion checks corroborate the written proof. Every one +of the 16,796 ten-record first factors has a unique residual second factor +of width greater than two. Separately, all 262,144 lane assignments normalized +at record 0 are considered; exactly 216 pass the necessary inverted-pair +condition. Each has the forced cycle, and an independently built directed +order graph is cyclic. The actual lane streams of all three upper-bound +passes are checked. Six malformed or unstable route controls reject, and +four-record reversal provides a width-four layout that does fit two passes. + +## Credit and scope + +Matarener's [#3825](https://github.com/CrocSwap/integer-mult-bounds/pull/3825) +supplies the abstract stable-lane pass obstruction in the bit-free complex +supplier context. James Reed / jwr404's +[#3839](https://github.com/CrocSwap/integer-mult-bounds/pull/3839) supplies the +earlier finite forward-composition evidence through seven records. Their +results are cited premises and context; their scientific code and counts +are not replayed as the deliverable. Retain their Walsh, native, adapter, +coverage and supplier predecessor credit. + +Mark Karpilovskij's published +[Composability of Permutation Classes](https://www.combinatorics.org/ojs/index.php/eljc/article/view/v26i1p41), +Theorem 15 and Question 16, already establishes the general failure of +sufficiency of the product-width bound. That broad noninclusion is prior +work. The explicit smallest-order certificate, four-cycle proof in this +routing contract, and standalone checker are the new repository contribution. +No historical priority claim is made for the example or standard methods. +Nick Petalas's older reversal and Gray-layout packages are related background; +their constructions, formulas and scientific code are not used as the main step. + +The `bit-new-register-model` card changes scope to this local layout side +result. Its register-algebra and supplier acceptance gate is not met here. +The source-binding first example passed at canonical base +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8, selected #7000. +The catalogue's assessed selection context is historical. The selected +frontier and its five assumptions are unchanged. The +[advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541783) +records the bounded question. Live open/account PRs, recent claims, active +Discussions, local reservations, cached overlap, main README searches and +merged searches were checked. The cache covered 545 open PRs and 7,200 +Discussion records, but only 218 of 10,178 main note paths. Main-tree searches +supplement that sparse coverage; unpublished work and arbitrary diffs remain +outside it. Search absence is not a novelty certificate. + +Minimum order is established by a finite exhaustive computation. The +four-cycle exclusion and route correctness are written proofs, not formal +proof-kernel results. Independent human and formal proof-kernel review are +unclaimed. A complete forbidden-pattern basis, arbitrary-layout recognition +algorithm, actual physical caller, merge controller, movement, stock, +precision, native cost, reversible cleanup and complete supplier bill remain +outside scope. No new kappa or multiplication theorem is claimed. Selected +scientific cold replay, predecessor scientific suites, Lean and Docker are unrun. + +[SOURCES.json](SOURCES.json) pins all source documents as historical +provenance. No predecessor implementation or live external mathematical +input is required by the direct verifier, including in a standalone export. + +## Open next questions + +- Which further minimal forbidden patterns characterize two stable two-lane + passes? Test the displayed four-cycle against one named layout before + seeking a constructive factorization. The complete basis and a general + recognition algorithm remain missing. +- Does one current physical producer/consumer layout contain this obstruction + as a record-order pattern? Pin its splitting and merging contract, then + price its controller, movement and cleanup. No actual caller is bound here. + +## Implementation bounds + +The checker has no recursion, solver, subprocess, network access, dynamic +code execution or shared mutable state. Mathematical inputs are fixed. +Dimensions are at most ten. The largest pair loop has exactly 4,862 squared +iterations; the normalized lane loop has exactly four to the ninth. All +functions fit within sixty physical lines. Explicit exceptions preserve +all checks under optimized Python. Warning-strict execution and in-memory +AST compilation provide the available interpreter diagnostics. No separate +lint/type analyzer or shared build configuration is changed. + +Power of Ten rule 3 requires a managed-runtime deviation. CPython allocates +integers, tuples, sets and bytes during this terminating certificate replay. +Two sets of at most 362,880 nine-byte layouts and catalogues of at most 16,796 +ten-record tuples bound live collections. The joined hash payload has at +most 9 times 362,880 bytes. This is not a fixed-allocation online controller; +a native online implementation would require a separate capacity contract. diff --git a/research/two-pass-width-obstruction/SOURCES.json b/research/two-pass-width-obstruction/SOURCES.json new file mode 100644 index 0000000000..b9d477a102 --- /dev/null +++ b/research/two-pass-width-obstruction/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/bit-free-complex-supplier/README.md", + "usage": "provenance", + "git_blob": "86ef9ad3871b39b2c5f90da1682ddf635b0082de", + "sha256": "ecf46acd8300adf05ef5cd2eee39264511d32c29b433fa60bc7e80e2206757cb" + }, + { + "path": "research/permutation-lds-product/README.md", + "usage": "provenance", + "git_blob": "1dac3b7b6b4b85d4ce8ec3b29be5d33ea25d835e", + "sha256": "7ce8ab3caffa4846c000806981993b5f0b3f7984a43f54982c59e564f179cd7d" + } + ] +} diff --git a/research/two-pass-width-obstruction/TASK.json b/research/two-pass-width-obstruction/TASK.json new file mode 100644 index 0000000000..4c8289cdd6 --- /dev/null +++ b/research/two-pass-width-obstruction/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Minimum-order failure of sufficiency of the two-pass width-product test in unrestricted stable two-lane routing.", + "scope_change_reason": "An original inverse-composition layout question replaces the card's register-algebra construction; only an abstract routing boundary is settled.", + "bottleneck_link": "A width-product bound alone cannot fund a two-pass implementation of a proposed layout. This is a side result at the bit-free layout boundary, without a paid native improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first explicit verified obstruction; package its minimum-order certificate and an optimal route without classifying further obstructions.", + "outcome": "negative-result", + "evidence": "PROOF.md and verify.py establish an explicit width-four ten-record layout with exact pass optimum three, and complete two-pass coverage of all width-at-most-four orders through nine records.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which further minimal forbidden patterns are needed to characterize two stable two-lane passes?", + "why_it_matters": "The width bound does not recognize feasible routes, while a complete obstruction test could support controller design.", + "first_step": "Use the displayed four-cycle as a rejection certificate for one named candidate layout, then seek a constructive factorization when it is absent.", + "blocked_by": "This package proves minimum order and one obstruction, not a complete basis or recognition algorithm." + }, + { + "question": "Does a current physical caller require this obstruction as a record-order pattern?", + "why_it_matters": "Only an actual layout occurrence with a priced stream contract can affect a supplier budget.", + "first_step": "Pin one producer/consumer layout and its permitted splitting and merging operations.", + "blocked_by": "No actual caller, tape controller, movement bill or reversible cleanup is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541783", + "prior_work": [ + { + "author": "Matarener", + "pr": 3825, + "role": "abstract stable-lane pass obstruction and bit-free supplier context" + }, + { + "author": "James Reed / jwr404", + "pr": 3839, + "role": "finite forward composition evidence; cited without replay" + }, + { + "author": "Mark Karpilovskij", + "url": "https://www.combinatorics.org/ojs/index.php/eljc/article/view/v26i1p41", + "role": "known general noninclusion; not a new theorem here" + } + ] +} diff --git a/research/two-pass-width-obstruction/VERIFY.json b/research/two-pass-width-obstruction/VERIFY.json new file mode 100644 index 0000000000..091bc825fb --- /dev/null +++ b/research/two-pass-width-obstruction/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": "Complete nine-record inverse-composition coverage, ten-record factor exclusion, all normalized lane types, literal optimal route and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete finite certificate with assertions disabled." + } + ] +} diff --git a/research/two-pass-width-obstruction/verify.py b/research/two-pass-width-obstruction/verify.py new file mode 100644 index 0000000000..17428711ab --- /dev/null +++ b/research/two-pass-width-obstruction/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Exact finite minimum-order certificate for two stable two-lane passes.""" + +import hashlib +import itertools +import json +import math +from pathlib import Path +import sys + + +TARGET = (3, 2, 1, 6, 5, 4, 9, 8, 7, 0) +FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def permutation(value): + require(isinstance(value, tuple) and 1 <= len(value) <= 10, + "permutation length must lie in 1..10") + require(all(type(x) is int for x in value), "integer records required") + require(sorted(value) == list(range(len(value))), "invalid record set") + return value + + +def width(value): + """Quadratic longest-decreasing-subsequence dynamic program.""" + permutation(value) + depths = [1] * len(value) + for j in range(len(value)): + for i in range(j): + if value[i] > value[j]: + depths[j] = max(depths[j], depths[i] + 1) + return max(depths) + + +def avoids_321(value): + """Independent literal forbidden-triple predicate.""" + for i, j, k in itertools.combinations(range(len(value)), 3): + if value[i] > value[j] > value[k]: + return False + return True + + +def catalogue(n): + require(type(n) is int and 1 <= n <= 10, "unsupported catalogue size") + words = [()] + for size in range(1, n + 1): + following = [] + for word in words: + for cut in range(size): + if all(word[i] < word[i + 1] + for i in range(cut, size - 2)): + following.append(word[:cut] + (size - 1,) + word[cut:]) + words = following + require(len(words) == len(set(words)), "duplicate catalogue entry") + require(len(words) <= 16796, "catalogue capacity exceeded") + return words + + +def pass_check(before, after, lane_one): + permutation(before) + permutation(after) + require(len(before) == len(after), "record count changed") + require(isinstance(lane_one, frozenset) and lane_one <= set(before), + "invalid lane assignment") + for selected in (False, True): + incoming = tuple(x for x in before if (x in lane_one) == selected) + outgoing = tuple(x for x in after if (x in lane_one) == selected) + require(incoming == outgoing, "lane order changed") + + +def upper_route(): + orders = (tuple(range(10)), (1, 2, 3, 4, 5, 6, 7, 8, 9, 0), + (2, 1, 3, 5, 4, 6, 8, 7, 9, 0), TARGET) + lanes = (frozenset({0}), frozenset({2, 5, 8}), frozenset({3, 6, 9})) + for i in range(3): + pass_check(orders[i], orders[i + 1], lanes[i]) + require(width(TARGET) == 4, "wrong obstruction width") + return {"orders": orders, "lane_one_records": [sorted(x) for x in lanes]} + + +def acyclic(labels): + """Kahn elimination on all first/second-pass order requirements.""" + positions = {x: i for i, x in enumerate(TARGET)} + edges = [set() for _ in range(10)] + for x in range(10): + for y in range(x + 1, 10): + if labels[x] // 2 == labels[y] // 2: + edges[x].add(y) + if labels[x] % 2 == labels[y] % 2: + a, b = (x, y) if positions[x] < positions[y] else (y, x) + edges[a].add(b) + remaining = set(range(10)) + for _ in range(10): + roots = [x for x in remaining + if all(x not in edges[y] for y in remaining)] + if not roots: + return False + remaining.difference_update(roots) + if not remaining: + return True + raise ValueError("topological capacity exhausted") + + +def cycle_certificate(): + positions = {x: i for i, x in enumerate(TARGET)} + inversions = [(x, y) for x in range(10) for y in range(x + 1, 10) + if positions[x] > positions[y]] + admissible = 0 + for tail in itertools.product(range(4), repeat=9): + labels = (0,) + tail + if any(labels[x] == labels[y] for x, y in inversions): + continue + admissible += 1 + a = next(x for x in (1, 2, 3) if labels[x] == 1) + c = next(x for x in (4, 5, 6) if labels[x] == 3) + b = next(x for x in (7, 8, 9) if labels[x] == 2) + require(labels[0] // 2 == labels[a] // 2 and 0 < a, + "first cycle edge missing") + require(labels[a] % 2 == labels[c] % 2 + and positions[a] < positions[c], "second cycle edge missing") + require(labels[c] // 2 == labels[b] // 2 and c < b, + "third cycle edge missing") + require(labels[b] % 2 == labels[0] % 2 + and positions[b] < positions[0], "fourth cycle edge missing") + require(not acyclic(labels), "an acyclic intermediate order exists") + require(admissible == math.factorial(3) ** 3, "incomplete type census") + return {"normalized_assignments": 4 ** 9, "forced_cycles": admissible} + + +def factor_exclusion(): + counts = {} + factors = catalogue(10) + require(len(factors) == 16796, "wrong ten-record catalogue size") + for first in factors: + require(avoids_321(first), "invalid first factor") + inverse = [0] * 10 + for i, x in enumerate(first): + inverse[x] = i + second = tuple(inverse[x] for x in TARGET) + require(tuple(first[x] for x in second) == TARGET, + "factor reconstruction failed") + value = width(second) + require(value > 2, "two-pass factorization found") + counts[value] = counts.get(value, 0) + 1 + return {"first_factors": len(factors), "second_width_counts": counts} + + +def minimal_order(): + factors = catalogue(9) + require(len(factors) == 4862, "wrong nine-record catalogue size") + direct_factors = set() + possible = set() + visited = 0 + for word in itertools.permutations(range(9)): + visited += 1 + if avoids_321(word): + direct_factors.add(word) + if width(word) <= 4: + possible.add(bytes(word)) + require(visited == math.factorial(9), "incomplete permutation scan") + require(set(factors) == direct_factors, "independent catalogues disagree") + reached = {bytes(first[x] for x in second) + for first in factors for second in factors} + require(reached == possible, "nine-record inverse completeness failed") + require(len(reached) == 261808, "unexpected nine-record product class") + for removed in range(10): + raw = [x for x in TARGET if x != removed] + reduced = bytes(x - (x > removed) for x in raw) + require(reduced in reached, "a deletion remains obstructed") + digest = hashlib.sha256(b"".join(sorted(reached))).hexdigest() + return {"permutations": visited, "one_pass_factors": len(factors), + "factor_pairs": len(factors) ** 2, "two_pass_layouts": len(reached), + "deletions": 10, "sorted_layouts_sha256": digest} + + +def expect_invalid(before, after, lanes): + try: + pass_check(before, after, lanes) + except ValueError: + return + raise ValueError("invalid routing control was accepted") + + +def controls(): + expect_invalid((0, 1), (1, 0), frozenset()) + expect_invalid((0, 1), (0, 0), frozenset({0})) + expect_invalid((0, 1), (0,), frozenset({0})) + expect_invalid((0, 1), (0, 1), frozenset({2})) + expect_invalid((0, 1, 2), (2, 1, 0), frozenset({0})) + expect_invalid(tuple(range(10)), TARGET, frozenset({0})) + pass_check((0, 1, 2, 3), (1, 0, 3, 2), frozenset({1, 3})) + pass_check((1, 0, 3, 2), (3, 2, 1, 0), frozenset({2, 3})) + require(width((3, 2, 1, 0)) == 4, "width-four boundary changed") + return {"invalid_routes_rejected": 6, "width_four_two_pass_control": True} + + +def main(): + require(len(sys.argv) == 1, "this verifier takes no arguments") + result = {"route": upper_route(), "cycle": cycle_certificate(), + "exclusion": factor_exclusion(), "minimal_order": minimal_order(), + "controls": controls()} + directory = Path(__file__).resolve().parent + sources = {} + for name in FILES: + payload = (directory / name).read_bytes() + require(len(payload) <= 1048576, "package source capacity exceeded") + sources[name] = hashlib.sha256(payload).hexdigest() + receipt = {"status": "PASS_TWO_PASS_WIDTH_OBSTRUCTION", "result": result, + "python": sys.version.split()[0], "package_sha256": sources} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()