Prove the smallest two-pass width-budget obstruction (no κ)

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.

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.

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"
+    }
+  ]
+}