diff --git a/research/gray-layout-lane-number/PROOF.md b/research/gray-layout-lane-number/PROOF.md new file mode 100644 index 0000000000..648227a334 --- /dev/null +++ b/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=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. diff --git a/research/gray-layout-lane-number/README.md b/research/gray-layout-lane-number/README.md new file mode 100644 index 0000000000..2496eeff32 --- /dev/null +++ b/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. diff --git a/research/gray-layout-lane-number/SOURCES.json b/research/gray-layout-lane-number/SOURCES.json new file mode 100644 index 0000000000..3a0e848010 --- /dev/null +++ b/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." +} diff --git a/research/gray-layout-lane-number/TASK.json b/research/gray-layout-lane-number/TASK.json new file mode 100644 index 0000000000..e6dc01ea96 --- /dev/null +++ b/research/gray-layout-lane-number/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "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_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 one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "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": "Exact one-pass stable-lane minimum F_(n+1) for the n-bit reflected Gray address permutation and its inverse, with a necessary multi-pass product bound.", + "scope_change_reason": "An original algebraic-layout side question replaces a selected-caller assumption audit. The result distinguishes small binary shear count from the stable-stream cost of the complete map; no selected assumption is discharged.", + "bottleneck_link": "The precision_tape and compiler assumptions need actual address movement costs. This supplies an exact abstract layout cost for one simple linear address family, without claiming a selected occurrence or a physical invoice.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved and independently corroborated one-pass formula; do not extend the family or claim optimal multi-pass depth.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py warning-strict normal/optimized replay and generated hash-bound stdout receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the optimal number of fixed-capacity stable-lane passes for the Gray layout?", + "why_it_matters": "The product bound here is necessary; a matching construction could replace a long adjacent-shear route.", + "first_step": "Compare the Fibonacci product lower bound with exact two-lane factorizations at small dimensions; keep the same no-copy stable-lane contract.", + "blocked_by": "The one-pass coloring does not supply a factorization at the product lower bound." + }, + { + "question": "Does a concrete native caller require this Gray address layout, and at what complete physical cost?", + "why_it_matters": "An abstract lane count alone cannot improve or invalidate a supplier invoice.", + "first_step": "Pin a producer/consumer pair and account for split assignment, merge control, payload storage, head movement and restored state.", + "blocked_by": "No selected-caller occurrence or physical stream implementation is supplied." + } + ], + "credit": { + "result": "produced by Nick Petalas", + "context": [ + "Matarener / PR3825 for the stable-pass layout obstruction and bit-free supplier question.", + "James Reed / PR3839 for permutation-composition context.", + "Nick Petalas / PR4858 and PR5148 for older XOR-layout and reversal context; neither is an executable dependency." + ], + "classical_tools": "Reflected binary Gray order, Fibonacci recurrence, increasing-chain partition and patience sorting." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19361586", + "overlap": { + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "scope": "Live open PR titles, account last-200 PRs, recent handoff comments, active Discussions, main README and merged-PR searches for Gray/subsequence/Fibonacci/stable-lane terms. Cached uniform-transfer-audit search additionally inspected.", + "limitations": "Sparse local note inventory, non-atomic remote snapshots, arbitrary historical diffs and unpublished work are not exhaustive novelty coverage.", + "related_recent_account": "PR6028 uses a one-scratch-record physical XOR tape model, not the stable-lane model. PR6393 uses a reflected Gray walk to schedule multilinear evaluations, not record routing." + }, + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "implementation": "CPython", + "version": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + } +} diff --git a/research/gray-layout-lane-number/VERIFY.json b/research/gray-layout-lane-number/VERIFY.json new file mode 100644 index 0000000000..9779d434c0 --- /dev/null +++ b/research/gray-layout-lane-number/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": "Gray/inverse extrema, attaining stable streams, independent quadratic and subset oracles, adjacent-shear composition and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete bounded checks with optimization; explicit contracts remain active." + } + ] +} diff --git a/research/gray-layout-lane-number/verify.py b/research/gray-layout-lane-number/verify.py new file mode 100644 index 0000000000..071dc46287 --- /dev/null +++ b/research/gray-layout-lane-number/verify.py @@ -0,0 +1,284 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the Gray-layout stable-lane theorem.""" + +import argparse +from bisect import bisect_left +from collections import deque +import hashlib +import json +from pathlib import Path +import sys + + +MAX_BITS = 16 +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py" +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def integer(value, lo, hi): + require(type(value) is int and lo <= value <= hi, "integer outside domain") + + +def fibonacci(index): + integer(index, 0, MAX_BITS + 2) + a, b = 0, 1 + for _ in range(index): + a, b = b, a + b + return a + + +def gray_order(bits): + integer(bits, 0, MAX_BITS) + return tuple(x ^ (x >> 1) for x in range(1 << bits)) + + +def permutation(order): + require(type(order) is tuple, "permutation must be a tuple") + integer(len(order), 1, 1 << MAX_BITS) + require(all(type(x) is int for x in order), "record IDs must be integers") + require(sorted(order) == list(range(len(order))), "invalid permutation") + + +def inverse_order(order): + permutation(order) + result = [0] * len(order) + for position, record in enumerate(order): + result[record] = position + return tuple(result) + + +def patience_certificate(order): + """Return lane of each record and a decreasing position witness.""" + permutation(order) + tails, ends = [], [] + previous = [-1] * len(order) + lane_of = [-1] * len(order) + for position, record in enumerate(order): + lane = bisect_left(tails, -record) + lane_of[record] = lane + if lane: + previous[position] = ends[lane - 1] + if lane == len(tails): + tails.append(-record) + ends.append(position) + else: + tails[lane] = -record + ends[lane] = position + witness, position = [], ends[-1] + for _ in range(len(tails)): + require(position >= 0, "short predecessor chain") + witness.append(position) + position = previous[position] + require(position == -1, "long predecessor chain") + return tuple(lane_of), tuple(reversed(witness)), len(tails) + + +def check_decreasing(order, witness, width): + permutation(order) + integer(width, 1, len(order)) + require(type(witness) is tuple and len(witness) == width, "wrong witness size") + for position in witness: + integer(position, 0, len(order) - 1) + for left, right in zip(witness, witness[1:]): + require(left < right and order[left] > order[right], "not decreasing") + + +def replay_lanes(order, lane_of, width): + """Split in input order, then merge whole symbolic records literally.""" + permutation(order) + integer(width, 1, len(order)) + require(type(lane_of) is tuple and len(lane_of) == len(order), "bad lane map") + for lane in lane_of: + integer(lane, 0, width - 1) + queues = [deque() for _ in range(width)] + for record, lane in enumerate(lane_of): + queues[lane].append((record, (record * 37) ^ 0x5A5A)) + output = [] + for record in order: + queue = queues[lane_of[record]] + require(bool(queue), "read from empty lane") + actual = queue.popleft() + require(actual == (record, (record * 37) ^ 0x5A5A), "unstable lane") + output.append(actual[0]) + require(tuple(output) == order, "wrong output") + require(all(not queue for queue in queues), "unconsumed record") + return len(output) + + +def quadratic_extrema(order): + """Independent predecessor DP, without patience sorting or reflection.""" + permutation(order) + require(len(order) <= 1024, "quadratic oracle capacity") + increasing, decreasing = [1] * len(order), [1] * len(order) + for right in range(len(order)): + for left in range(right): + if order[left] < order[right]: + increasing[right] = max(increasing[right], increasing[left] + 1) + else: + decreasing[right] = max(decreasing[right], decreasing[left] + 1) + return max(increasing), max(decreasing) + + +def exhaustive_lane_minimum(order): + """Independent subset DP over every increasing chain and partition.""" + permutation(order) + require(len(order) <= 8, "subset oracle capacity") + size = 1 << len(order) + chains = [False] * size + chains[0] = True + for mask in range(1, size): + values = [value for i, value in enumerate(order) if mask & (1 << i)] + chains[mask] = all(a < b for a, b in zip(values, values[1:])) + costs = [len(order) + 1] * size + costs[0] = 0 + for mask in range(1, size): + for chain in range(1, size): + if chain & mask == chain and chains[chain]: + costs[mask] = min(costs[mask], costs[mask ^ chain] + 1) + return costs[-1] + + +def composition_bound(order, passes): + """Check tuple coloring of a literal sequence of stable passes.""" + permutation(order) + require(1 <= len(passes) <= 8, "bad pass list") + incoming = tuple(range(len(order))) + histories = [()] * len(order) + product = 1 + for outgoing, lane_of, width in passes: + permutation(outgoing) + require(len(outgoing) == len(order), "pass changes record set") + integer(width, 1, len(order)) + require(len(lane_of) == len(order), "bad intermediate lane map") + queues = [deque() for _ in range(width)] + for record in incoming: + integer(lane_of[record], 0, width - 1) + queues[lane_of[record]].append(record) + histories[record] += (lane_of[record],) + for record in outgoing: + queue = queues[lane_of[record]] + require(bool(queue) and queue.popleft() == record, "unstable pass") + require(all(not queue for queue in queues), "pass loses records") + incoming = outgoing + product *= width + require(incoming == order, "wrong final order") + last = {} + for record in incoming: + history = histories[record] + require(last.get(history, -1) < record, "tuple class reverses input") + last[history] = record + require(len(last) <= product, "too many tuple classes") + return product + + +def shear_passes(bits): + """Low-to-high adjacent address shears give a two-lane factorization.""" + integer(bits, 1, 8) + positions = list(range(1 << bits)) + incoming = tuple(positions) + passes = [] + for bit in range(bits - 1): + positions = [x ^ (((x >> (bit + 1)) & 1) << bit) for x in positions] + outgoing = tuple(sorted(range(len(positions)), key=positions.__getitem__)) + relative_position = [0] * len(positions) + for index, record in enumerate(incoming): + relative_position[record] = index + relative = tuple(relative_position[record] for record in outgoing) + lane_relative, _, width = patience_certificate(relative) + require(width == 2, "shear does not use two lanes") + lane_of = tuple(lane_relative[relative_position[x]] for x in range(len(positions))) + passes.append((outgoing, lane_of, width)) + incoming = outgoing + require(tuple(positions) == gray_order(bits), "wrong shear product") + return tuple(passes), incoming + + +def theorem_checks(): + counts = {"orders": 0, "routed_records": 0, "quadratic_oracles": 0, + "subset_oracles": 0, "shear_compositions": 0} + for bits in range(MAX_BITS + 1): + order = gray_order(bits) + if bits: + lower = gray_order(bits - 1) + reflected = lower + tuple((1 << (bits - 1)) + x for x in reversed(lower)) + require(order == reflected, "reflection identity fails") + for candidate in (order, inverse_order(order)): + lanes, witness, width = patience_certificate(candidate) + require(width == fibonacci(bits + 1), "wrong Fibonacci lane count") + check_decreasing(candidate, witness, width) + counts["routed_records"] += replay_lanes(candidate, lanes, width) + counts["orders"] += 1 + if bits <= 10: + require(quadratic_extrema(candidate) == + (fibonacci(bits + 2), fibonacci(bits + 1)), "DP disagrees") + counts["quadratic_oracles"] += 1 + if bits <= 3: + require(exhaustive_lane_minimum(candidate) == width, "partition disagrees") + counts["subset_oracles"] += 1 + if 2 <= bits <= 8: + passes, final = shear_passes(bits) + product = composition_bound(final, passes) + require(product >= fibonacci(bits + 1), "composition violates lower bound") + counts["shear_compositions"] += 1 + return counts + + +def rejection_checks(): + bad_cases = ( + ("bits", -1), ("bits", True), ("bits", MAX_BITS + 1), + ("order", (0, 0)), ("order", (False, 1)), ("order", (0, 2)), + ("lanes", (0, 0, 0, 0)), ("lanes", (0, 1, 0, 2)), + ("lanes", (0, 1, 0)), ("witness", (0, 1)), + ("witness", (2, 1)), ("witness", (2, 4)), + ) + order = gray_order(2) + for kind, value in bad_cases: + rejected = False + try: + if kind == "bits": + gray_order(value) + elif kind == "order": + permutation(value) + elif kind == "lanes": + replay_lanes(order, value, 2) + else: + check_decreasing(order, value, 2) + except ValueError: + rejected = True + require(rejected, "invalid fixture accepted") + require(quadratic_extrema(gray_order(1)) == (2, 1), "LIS/LDS distinction lost") + xor_order = tuple(x ^ 7 for x in range(8)) + require(quadratic_extrema(xor_order)[1] == 8, "XOR control incorrect") + require(quadratic_extrema(gray_order(3))[1] == 3, "Gray control incorrect") + return len(bad_cases) + 2 + + +def receipt(counts): + package = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + with (package / name).open("rb") as source: + payload = source.read(1024 * 1024 + 1) + require(len(payload) <= 1024 * 1024, "package file capacity") + hashes[name] = hashlib.sha256(payload).hexdigest() + return {"status": "PASS_GRAY_LAYOUT_LANE_NUMBER", "counts": counts, + "python": sys.version.split()[0], "file_sha256": hashes, + "claim_type": "scoped written proof with finite corroboration"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.parse_args() + counts = theorem_checks() + counts["controls"] = rejection_checks() + print(json.dumps(receipt(counts), sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()