Prove exact Fibonacci stable-lane cost for Gray layouts (no κ)

research/gray-layout-lane-number/PROOF.md

@@ -0,0 +1,113 @@
+# Exact stable lanes for the reflected Gray layout
+
+This scoped written proof was produced by Nick Petalas. It uses the classical
+reflected Gray order and increasing-chain characterization of stable lanes.
+No historical novelty is claimed for those general tools.
+
+## Contract
+
+There are N=2^n distinct records, initially in order 0,...,N-1, for n>=0.
+Record IDs describe positions and do not restrict payloads. One stable-lane
+pass splits the input into T ordered streams, then arbitrarily interleaves
+those streams while preserving each stream's order. Every record enters
+exactly one stream and leaves it exactly once. There are no copies, deletions,
+or reversals within a stream. Empty streams are permitted.
+
+Define g_n(x)=x XOR floor(x/2), and let G_n be its values in increasing x.
+The requested output record order is G_n. The alternative convention that
+record x moves to position g_n(x) has output order g_n^{-1}; it has the same
+answer below. Lane selection and merge decisions depend only on positions.
+Their physical preparation, storage, access and cleanup are not free costs
+certified by this abstract contract.
+
+Write F_0=0, F_1=1 and F_{j+2}=F_{j+1}+F_j.
+
+**Theorem.** The exact one-pass lane requirement of G_n and its inverse is
+F_{n+1}. Its longest increasing subsequence has length F_{n+2}, and its longest
+decreasing subsequence has length F_{n+1}. Consequently any realization using
+k stable-lane passes of capacities T_1,...,T_k must satisfy
+
+    product_i T_i >= F_{n+1}.
+
+For fixed T>=2, at least the smallest k with T^k>=F_{n+1} passes are necessary.
+This statement does not assert that this lower bound is attainable in multiple
+passes. The one-pass minimum is attained.
+
+## Reflection gives both extremal subsequences
+
+For n=0, G_0=(0), and both subsequence lengths are one. Directly from the
+binary formula, with h=2^{n-1},
+
+    G_n = G_{n-1} followed by h + reverse(G_{n-1}).        (1)
+
+The n=1 identity is immediate. For n>=2, put x=h+y in the second half and
+let z=h-1-y. In the low
+n-1 bits, complementing y to z preserves adjacent-bit XORs and flips the top
+low bit. These are exactly the low bits of g_n(h+y). Thus
+g_n(h+y)=h+g_{n-1}(h-1-y), proving (1).
+
+Let L_n and D_n be the longest increasing and decreasing lengths. Every value
+in the first block of (1) is less than every value in the second block.
+An increasing subsequence can concatenate independently optimal subsequences
+of both blocks. Reversal interchanges increasing and decreasing lengths.
+A decreasing subsequence cannot use both blocks. Therefore exactly
+
+    L_n = L_{n-1} + D_{n-1},
+    D_n = max(D_{n-1}, L_{n-1}).                         (2)
+
+Starting at L_0=D_0=1, induction in (2) gives
+L_n=F_{n+2} and D_n=F_{n+1}. The argument supplies both the upper bounds and
+attaining subsequences, rather than just bounding the recurrence.
+
+For any permutation, transposing the points (i,pi(i)) preserves increasing
+subsequence lengths. A decreasing subsequence becomes another decreasing
+subsequence after reversing its indexing order. Applying this twice proves
+that a permutation and its inverse have equal L and D. This establishes the
+alternative position-map convention.
+
+## Stable lanes attain the decreasing-subsequence lower bound
+
+Consider any output permutation pi of distinct initially increasing IDs.
+Every stream in a stable-lane pass is increasing in those IDs. A decreasing
+subsequence can take at most one record from each stream, so T>=D(pi).
+
+For the converse, process pi in its output order. Label each record by the
+length of a longest decreasing subsequence ending there. The labels lie in
+1,...,D(pi). If an earlier record a and a later record b have the same label,
+then a>b is impossible: a decreasing subsequence ending at a could extend
+by b and increase b's label. Distinctness implies a<b. Each label class is
+therefore increasing.
+
+Assign that label to the record's input position. Split the original input
+into those classes in input order. Merge by following pi's label sequence.
+The next requested record is the next item in its stream because every
+class is increasing. Every item is consumed once. This attains D(pi) lanes
+and works for arbitrary payloads. In the verifier, patience sorting constructs
+these labels, and a separate stream interpreter checks the literal split and
+merge. The proof of attainability does not depend on that implementation.
+
+Applying this fact to (2) proves the exact F_{n+1} lane requirement. For
+example, n=16 needs exactly F_17=1597 one-pass lanes.
+
+## Composition and its scope
+
+Give each record the tuple of its lane choices in all k passes. Two records
+with the same tuple preserve their relative order in the first pass and,
+inductively, in every subsequent pass. Each tuple class is increasing in
+original IDs at the final output. There are at most product_i T_i classes.
+The decreasing-subsequence lower bound proves the displayed product bound.
+This reasoning permits arbitrary position-dependent splits and merges and
+does not assume consecutive lane ranges.
+
+The Gray address map itself is a product of n-1 adjacent binary shears for
+n>=1: for bit j from low to high, update x_j by XOR with the still-original
+x_{j+1}. The resulting bit j is x_j XOR x_{j+1}. This small algebraic factor
+count therefore does not bound one-pass stable-lane requirements by a constant
+or by n. A physical implementation can use more passes, another memory model,
+or additional channels. The theorem excludes none of those alternatives.
+
+This is a layout-interface result. It does not establish a caller occurrence,
+an unconditional multitape lower bound, a paid native operator, a supplier
+admission, a new kappa or a complete multiplication theorem. All five selected
+framework assumptions remain. Independent human and formal proof-kernel
+review are unclaimed.

research/gray-layout-lane-number/README.md

@@ -0,0 +1,131 @@
+# Exact Fibonacci lane requirement of the Gray layout
+
+This scoped written proof with exact finite corroboration was produced by
+Nick Petalas. The n-bit reflected Gray address map
+
+    g_n(x) = x XOR (x >> 1),       0 <= x < 2^n,
+
+and its inverse need exactly **F_(n+1) stable lanes in one pass**, where
+F_0=0, F_1=1. For n=16 the exact requirement is 1,597 lanes. A matching
+increasing-chain assignment attains the bound for arbitrary record payloads.
+Any sequence of stable-lane passes must have capacity product at least
+F_(n+1). No optimal multi-pass depth or new kappa is claimed.
+
+The address map is a product of n-1 adjacent binary shears for n>=1. Its
+small algebraic factor count therefore does not imply a small one-pass lane
+requirement. This is an abstract layout cost, with no selected-caller
+occurrence or complete physical implementation asserted.
+
+## Proof and exact boundary
+
+Input records have distinct IDs 0,...,2^n-1 in that order. One pass splits
+them into T streams and interleaves those streams into the output. Each
+stream preserves input order, and every record moves exactly once. The output
+order is g_n(0),...,g_n(2^n-1). Placing record x at position g_n(x) instead
+gives the inverse order and the same lane requirement.
+
+[PROOF.md](PROOF.md) derives the exact recurrences
+
+    L_n = L_(n-1) + D_(n-1),     D_n = max(L_(n-1), D_(n-1)),
+    L_0 = D_0 = 1,
+
+for longest increasing and decreasing subsequences. Thus L_n=F_(n+2) and
+D_n=F_(n+1). Coloring records by decreasing-subsequence depth gives exactly
+D_n increasing streams and a literal attaining split/merge. Lane-choice
+tuples across multiple passes prove the product lower bound.
+
+The reflection formula, Fibonacci numbers, patience sorting and general
+chain-coloring argument are classical tools. The contribution is their exact
+Gray-layout lane consequence and its independently reproducible certificate
+under this explicit interface; no global historical-priority claim is made.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and only its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gray-layout-lane-number/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gray-layout-lane-number/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gray-layout-lane-number
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gray-layout-lane-number --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. The verifier checks
+both orders for n=0,...,16, producing attaining lanes and a matching decreasing
+witness. It literally splits and merges all 262,142 records in these 34
+cases. Independent quadratic subsequence DP covers 22 cases through n=10;
+an exhaustive increasing-subset partition oracle covers eight cases through
+n=3. Seven adjacent-shear compositions check the tuple-color product bound.
+Boundary and semantic controls reject malformed permutations, unstable lane
+maps and false witnesses, and distinguish increasing length and fixed XOR
+layouts from the claimed Gray quantity.
+
+The expected status is `PASS_GRAY_LAYOUT_LANE_NUMBER`. Stdout is a generated
+receipt with actual enumerated counts and SHA256 of all six package files.
+No receipt is hand-written. Default verification writes nothing and also
+works in a Git-free export. Both registered checks retain explicit guards
+under optimization. Universal quantifiers rest on the written proof, not on
+these finite computations.
+
+## Scope, sources and credit
+
+Canonical base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8.
+The `uniform-transfer-audit` card changes to this original layout side result;
+no selected framework assumption is discharged. The selected source-binding
+orientation passed. [TASK.json](TASK.json) records the scope change and
+[SOURCES.json](SOURCES.json) pins exact provenance. No predecessor executable
+or scientific receipt is imported or replayed.
+
+Credit Matarener's [PR3825](https://github.com/CrocSwap/integer-mult-bounds/pull/3825)
+for distinguishing linear address algebra from stable-pass layout costs,
+and James Reed's [PR3839](https://github.com/CrocSwap/integer-mult-bounds/pull/3839)
+for permutation-composition context. Nick Petalas's older PR4858 counts XOR
+subsequences and PR5148 constructs reversal passes. Those different endpoints
+are context, not claimed again here. Their retained native/Walsh/compiler and
+coverage predecessors keep their credit. New material is Apache-2.0.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361586)
+precedes the proof package. Live open PRs, recent account work, handoff claims,
+active Discussions, cached overlap and distinctive all-main/merged searches
+were checked. Sparse notes, non-atomic snapshots, arbitrary historical diffs
+and unpublished work remain coverage limits. No exhaustive novelty claim
+follows from those searches.
+
+No actual caller, physical lane allocation, merge controller, head movement,
+reversible scratch cleanup, native invoice, compiler, precision or analytic
+recovery is supplied. More tapes, random access or another routing model may
+escape this stable-lane bound. No selected cold replay, Lean proof, native
+suite, supplier admission or complete multiplication theorem was run or
+claimed. Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Determine optimal fixed-capacity multi-pass depth for this same Gray layout.
+  Start with exact two-lane factorizations at small dimensions and compare the
+  necessary Fibonacci product bound. The one-pass coloring does not supply a
+  factorization attaining that bound.
+- Bind an actual native producer/consumer to this layout and price the full
+  split assignment, merge control, storage, head movement and restored state.
+  A caller occurrence and physical stream implementation are missing, so the
+  abstract lane count cannot yet alter a supplier invoice.
+
+Structured relevance, first steps and blockers are in [TASK.json](TASK.json).
+
+## Verifier constraints
+
+The verifier is nonrecursive and accepts no external mathematical input.
+Arrays have at most 2^16 records. Quadratic DP is capped at 1,024 records;
+the partition oracle has at most 256 states and 256 candidate subsets per
+state. Composition checks have at most eight passes, and the registered
+shear fixtures have at most 256 records. Witness reconstruction performs
+exactly its declared number of predecessor steps. Functions are under 60
+physical lines. Explicit contracts stay enabled under optimization.
+
+Power of Ten rule 3 has a bounded managed-runtime deviation. Python allocates
+integers, tuples and queues during this terminating verifier; it is not a
+fixed-allocation runtime. Record, pass, oracle and one-MiB file-read caps bound
+live collections. Rule 9 permits only the standard-library sort callback
+for indexing a local position table; its target and table lifetime are fixed.
+Warning-strict normal/optimized replay and in-memory source compilation supply
+the available interpreter diagnostics. No repository analyzer configuration
+or shared build setting is changed.

research/gray-layout-lane-number/SOURCES.json

@@ -0,0 +1,25 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "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"
+    }
+  ],
+  "context": "No predecessor executable or scientific result is replayed. The retained README supplies the stable-lane cost model context only."
+}