From d1ce9aa4bd17cc6196463c4f28719ad8dfc8d281 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 04:50:28 -0700 Subject: [PATCH 1/3] Realize stable three-lane reversal with paid local control --- .../physical-three-lane-reversal/PROOF.md | 119 ++++++++++++ .../physical-three-lane-reversal/README.md | 55 ++++++ .../physical-three-lane-reversal/RESULT.json | 49 +++++ .../physical-three-lane-reversal/SOURCES.json | 32 ++++ .../physical-three-lane-reversal/TASK.json | 95 ++++++++++ .../physical-three-lane-reversal/VERIFY.json | 32 ++++ .../inputs/pr5148-PROOF.md | 115 ++++++++++++ .../physical-three-lane-reversal/machine.py | 177 ++++++++++++++++++ .../physical-three-lane-reversal/verify.py | 128 +++++++++++++ 9 files changed, 802 insertions(+) create mode 100644 research/physical-three-lane-reversal/PROOF.md create mode 100644 research/physical-three-lane-reversal/README.md create mode 100644 research/physical-three-lane-reversal/RESULT.json create mode 100644 research/physical-three-lane-reversal/SOURCES.json create mode 100644 research/physical-three-lane-reversal/TASK.json create mode 100644 research/physical-three-lane-reversal/VERIFY.json create mode 100644 research/physical-three-lane-reversal/inputs/pr5148-PROOF.md create mode 100644 research/physical-three-lane-reversal/machine.py create mode 100644 research/physical-three-lane-reversal/verify.py diff --git a/research/physical-three-lane-reversal/PROOF.md b/research/physical-three-lane-reversal/PROOF.md new file mode 100644 index 0000000000..6039e5b543 --- /dev/null +++ b/research/physical-three-lane-reversal/PROOF.md @@ -0,0 +1,119 @@ +# A paid fixed-three-lane reversal + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +## Contract and scope + +For every n>=0 and B>=1, SOURCE contains n consecutive B-bit records and +BD contains the canonical least-significant-first positive binary encoding +of B. These are supplied ports, each with a left marker, head at its first +payload cell, and blank tail. OUTPUT and the work ports are blank after +their left markers. All15 ports are distinct. Ports1,2,3 are untouched. +The local alphabet is {0,1,blank,left}; the compiled instruction table is +independent of n and B. The interpreter executes only single-cell reads, +writes, unit head moves and finite jumps. Its host step cap is a verifier +stop, not an input to the mathematical machine. + +On a valid call OUTPUT contains the same records in reverse order, preserving +bit order within every record. SOURCE and BD retain their payloads. All heads +return to their own origin+1; all work cells are blank. Output is caller-owned; +its later disposal is a separate caller obligation, bounded by a linear scan +of its nB cells if requested. Inputs may be based at independently translated +origins. This is a valid-input service; malformed encodings can reject with +partially written work and displaced heads. There is no transactional failure +restoration claim. + +This realizes the fixed-T=3 instance of Nick Petalas's PR5148 construction, +with the physical costs that its abstract stable-lane model leaves unpaid. +Credit Matarener's PR3825 pass obstruction, James Reed's PR3839 finite census, +and the retained PR5090 local instruction Builder/Tape semantics. No universal +multitape lower bound, full bit-free supplier gain, or selected-frontier update +follows. + +## Local control and refinement + +The retained unary routine copies BD to TEMP, decrements its canonical binary +value until zero, and appends one unit to B per decrement. It preserves BD, +erases TEMP, and returns both descriptor heads. The initial scan copies one +B-bit record at a time from SOURCE to DATA and appends one unit to N. A blank +SOURCE cell is accepted only at a record boundary. Thus N has length n and +DATA is the original record sequence. S starts at unary1. + +At stage i, put s=3^i. The invariant is: DATA is partitioned into consecutive +original-index blocks of length s, with the final block possibly shorter; +each block is internally reversed, and blocks are in original order. Heads +start at their origins and every lane is empty. The coverage loop compares +N and S by local synchronous scans. If s>=n it terminates. + +Otherwise split transfers consecutive chunks of at most s records cyclically +to lane0, lane1, lane2. Chunks remain ordered within each lane, so this is an +actual stable split. Each transferred source cell is erased. The unary S and +B tapes drive every chunk and record loop. No payload record is fabricated for +an absent position. After rewinding the empty DATA and populated lanes, merge +transfers one chunk from lane2, then lane1, then lane0 to DATA. Absent tail +chunks are skipped by reading their blank current cells. Every full group +becomes the reversal of the corresponding three original blocks. A final +one- or two-block group is also reversed because only its real lane chunks +are emitted. Each lane is consumed in its own stream order: the merge is stable. + +Hence DATA has the same invariant with block size3s. The literal tripling +loop consumes S and writes three units to NEXT per unit, then consumes NEXT +back to S. Induction proves the invariant at every stage. The first s>=n +occurs after k=ceil(log_3 n) stages for n>=2, with k=0 for n=0,1. DATA is then +one reversed block. Final transfer consumes it into OUTPUT; fixed cleanup +scans erase N, S, B and all auxiliary cells and return the heads. + +For n7, s1 gives records2,1,0,5,4,3,6, and s3 gives6,5,4,3,2,1,0, +exactly PR5148's first example. The digit-complement and block-reversal +constructions agree because complementing the next ternary digit reverses +the order of these three already-reversed subblocks, including the last +incomplete group. + +## Complete local-action bound + +Let L=floor(log_2 B)+1 and k as above. Count each table instruction, including +reads, jumps, writes and head moves, as one action. A conservative bound is + + T <= 256 ((n+1)(B+1)(k+1) + B(L+1) + 1). + +This is a written upper bound, not a fitted measured slope. The following +summands account for the whole execution. A rewind over h payload positions +costs at most3h+5. A row copy/consume, including the B rewind, costs at most +16B+12. Unary conversion costs at most32B(L+1)+16L+32. Initial copy/counting, +source/data/N rewind, and final payload transfer are together at most +40nB+24n+32. At one nonterminal stage, the2n row transfers and chunk dispatch +cost at most40nB+48n+48; the lane/DATA rewinds cost at most12nB+40. +Coverage scans across the run cost at most12n(k+1)+16(k+1). Tripling and its +transfer cost at most48s+32 per stage. Since sum_{i=2, all tripling costs are at most72n+32k. Final cleanup costs at most +16(B+n+3^k+L+1)+80; n0/1 uses3^k=1. These deliberately loose summands fit the +displayed bound (including B=1,n=0). In particular runtime width is paid; +there is no constant-time B-bit word operation or free lane interleaving. + +## Retained backing, setup and output + +The15 role objects and fixed419-instruction program are constant setup. +No tape is allocated during execution. If K0 counts already allocated tape +backing, newly visited storage is bounded by + + 6nB + 7n + B + 2L + 60. + +This conservatively counts SOURCE, DATA, OUTPUT and each of three lanes at +nB individually. It does not sum only simultaneously live lane payloads: +each lane can retain a different historical high-water mark. N costs n; +S and NEXT each reach3^k<3n for n>=2 (at most1 for n<=1); B costs B; BD and +TEMP cost L each. Markers, terminal blank visits and the n<=1 exception fit +the60 allowance. Thus retained backing is at most K0 plus this expression, +even though the dictionary simulator retains blank written cells after erasure. +This is a tape-cell statement, not a Python allocator-byte claim. Borrowed +input production, input descriptor production and later output disposal are +explicit caller costs, not hidden inside this service. + +## Open next questions + +A complete bit-free supplier must compose this reversal with its other +permutations and numerical consumers and pay their combined bank and costs. +First bind one actual supplier endpoint to the present record layout; pass +optimality alone does not establish a numerical gain. Heterogeneous runtime +lane capacities would require a separate fixed-bank encoding and scheduling +contract; this theorem fixes three lanes. diff --git a/research/physical-three-lane-reversal/README.md b/research/physical-three-lane-reversal/README.md new file mode 100644 index 0000000000..d39528a6a0 --- /dev/null +++ b/research/physical-three-lane-reversal/README.md @@ -0,0 +1,55 @@ +# Physical three-lane record reversal + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. + +One fixed419-instruction local-symbol program reverses n records of runtime +width B on15 fixed tape ports. It realizes PR5148's three-lane stable route +on actual records, including incomplete final blocks, with no host sorting, +per-record tape allocation, decoded loop bounds or virtual payload padding. +The input and binary width descriptor are borrowed; output is distinct and +caller-owned. All work is erased and heads return. This is a valid-input +contract, not a rollback guarantee for malformed input. + +For L=floor(log2 B)+1 and k=ceil(log3 n) (k0 for n0/1), the complete instruction +count is at most256((n+1)(B+1)(k+1)+B(L+1)+1). Retained tape backing is at most +K0+6nB+7n+B+2L+60, including historical high-water capacity. [PROOF.md](PROOF.md) +gives the all-n refinement, full invoice, supplied-input costs and limitations. +The abstract pass count alone is not a physical tariff or a numerical gain. + +The verifier checks492 cases with independent record-array expectations, +translated origins, full borrowed/unused frames, every work tape and head, +written action/backing bounds, and the exact seven-record two-pass source +example. Eight controls include actual output-bit and guide corruption. +These are finite corroboration of the scoped proof, not a proof kernel or a +complete multiplication theorem. + +Reproduce from the repository root with Python3.12: + +```sh +python3.12 -I -B research/physical-three-lane-reversal/verify.py +python3.12 -I -O -B research/physical-three-lane-reversal/verify.py +python3.12 scripts/research_package.py --package research/physical-three-lane-reversal --check-only +python3.12 scripts/research_package.py --package research/physical-three-lane-reversal +``` + +`--write-result` is the explicit receipt-generation mode. Normal replay +requires both SOURCES.json and RESULT.json; frozen receipts use typed canonical +JSON equality. The source proof from PR5148 is retained byte-for-byte and +hash-checked with exact public head/path metadata. It is external publication +provenance, not a local Git-history assertion. The retained local instruction +source is authenticated by the base Git blob and SHA256 and declared as a live +export input. No predecessor source is modified. + +Credit Nick Petalas's PR5148 construction, Matarener's PR3825 obstruction, +James Reed's PR3839 finite census, and the PR5090 physical instruction semantics +following Jose Manuel PR2786 and Nick Petalas PR3503. The canonical claim is +[discussion1166 comment19144825](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144825). + +## Open next questions + +Can an actual bit-free supplier consume this layout with its complete numerical, +movement and backing budget? First bind one real supplier call and its other +permutations; this standalone reversal does not establish supplier admission. +Can heterogeneous runtime lane capacities be encoded on a fixed bank with a +complete tariff? That is separate from the present fixed-three-lane theorem. +The selected frontier is unchanged. diff --git a/research/physical-three-lane-reversal/RESULT.json b/research/physical-three-lane-reversal/RESULT.json new file mode 100644 index 0000000000..c1f6261dde --- /dev/null +++ b/research/physical-three-lane-reversal/RESULT.json @@ -0,0 +1,49 @@ +{ + "schema_version": 1, + "claim": "fixed-three-lane physical valid-input reversal", + "cases": 492, + "cases_sha256": "534d2e2b3f5888900fc2297bf1e3e57a6e038d5c572d75bee9d5bff26c4b6e95", + "program_instructions": 419, + "max_steps": 126932, + "seven": { + "n": 7, + "B": 3, + "origin": 0, + "steps": 3579, + "backing": 164, + "stage_records": [ + [ + "101", + "000", + "011", + "100", + "111", + "010", + "001" + ], + [ + "001", + "100", + "111", + "010", + "101", + "000", + "011" + ] + ] + }, + "controls": [ + "bad-width:", + "bad-width:0", + "bad-width:10", + "bad-width:1x", + "partial-row", + "port-alias", + "actual-mutant:output-bit", + "actual-mutant:tripled-guide" + ], + "unrun": [ + "production bit-free supplier composition", + "heterogeneous runtime lane counts" + ] +} diff --git a/research/physical-three-lane-reversal/SOURCES.json b/research/physical-three-lane-reversal/SOURCES.json new file mode 100644 index 0000000000..bf18b7943e --- /dev/null +++ b/research/physical-three-lane-reversal/SOURCES.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "files": [ + { + "path": "research/bit-row-padding-physical/machine.py", + "usage": "input", + "git_blob": "1e3533efa92c3bab35916ae6844290586d18ff27", + "sha256": "24270408e87b028791670cd63908adeb03162f0919237e8644065c5898fecf2f" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + } + ], + "external_public_input": { + "local_path": "inputs/pr5148-PROOF.md", + "source_pr": 5148, + "source_head": "7a49d01908933e044acf96f040b15818ef748051", + "source_path": "research/reversal-stable-lane-tariff/PROOF.md", + "sha256": "98b6d670ae019c3c9365e20f80b872a764d4b0dfc2a7f76d5ce24c50c7c19c39", + "coverage": "Unmodified exact public proof; constructive predecessor, not physical-cost evidence." + } +} diff --git a/research/physical-three-lane-reversal/TASK.json b/research/physical-three-lane-reversal/TASK.json new file mode 100644 index 0000000000..1742f8d05f --- /dev/null +++ b/research/physical-three-lane-reversal/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Physical fixed-three-lane realization of PR5148 reversal for all n and encoded runtime record width B.", + "scope_change_reason": "The public PR5148 handoff leaves stable routing, metadata, movement and cleanup unpriced. This supplies their actual finite program and complete tape tariff.", + "bottleneck_link": "Closes one concrete physical record-layout contract without inferring a full bit-free supplier gain.", + "budget_minutes": 60, + "stop_rule": "Stop if local control, partial tails, restoration or whole cost needs an unpriced host oracle.", + "outcome": "completed", + "evidence": "PROOF.md; machine.py; verify.py and RESULT.json; canonical claim19144825;492 frame/action cases and8 controls.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; finite corroboration, not human or proof-kernel review.", + "open_questions": [ + { + "question": "Can a complete bit-free supplier consume this physical reversal?", + "why_it_matters": "Pass optimality does not establish a numerical improvement.", + "first_step": "Bind one actual supplier endpoint and add all other routing and numerical costs.", + "blocked_by": "Whole supplier composition and budget remain outside scope." + } + ] +} diff --git a/research/physical-three-lane-reversal/VERIFY.json b/research/physical-three-lane-reversal/VERIFY.json new file mode 100644 index 0000000000..a8fa34b2a3 --- /dev/null +++ b/research/physical-three-lane-reversal/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-row-padding-physical/machine.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Source-bound full frames, exact stages, action/backing and mutants" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same explicit guards and typed receipt without assertions" + } + ] +} diff --git a/research/physical-three-lane-reversal/inputs/pr5148-PROOF.md b/research/physical-three-lane-reversal/inputs/pr5148-PROOF.md new file mode 100644 index 0000000000..487f024811 --- /dev/null +++ b/research/physical-three-lane-reversal/inputs/pr5148-PROOF.md @@ -0,0 +1,115 @@ +# Exact reversal capacity of stable-lane passes + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Model and statement + +There are n distinct records, initially in order 0,...,n-1, with n >= 1. +A pass with capacity T >= 1 assigns each record to one of at most T lanes. +Each lane preserves its input order. The output can be any interleaving of +the lane streams that preserves that order. Empty lanes are permitted. +The record payloads are transported intact, without copying or deletion. +Lane assignments and interleavings are unrestricted routing descriptions. +No cost for selecting or executing them is included in a pass count. + +**Theorem.** For nonnegative k and positive integers T_1,...,T_k, exactly +reversing n records is possible in those k passes if and only if + + n <= T_1 ... T_k. + +The empty product is one. Consequently, with fixed T >= 2 the minimum pass +count is the smallest integer k with T^k >= n, namely ceil(log_T n). +For T=1, only n=1 can be reversed, and its minimum is zero passes. + +This is a scoped combinatorial routing theorem. In particular, a lane is +not an assertion that a physical tape or its head can provide this service +at unit cost. Splitting, merge control, movement, return, storage and +reversible cleanup are separate obligations. + +## Necessity + +Assign each record its k-tuple of lane choices along the route. If two +records have the same tuple, their relative order is preserved in the +first pass. Inductively, it is preserved in every later pass, because +the two records again enter the same order-preserving lane. Full reversal +reverses every pair of distinct records. Thus no two records can have +the same tuple. There are at most product(T_i) tuples, proving necessity. + +This argument permits arbitrary splitting and merge choices. It is the +reversal instance of the decreasing-subsequence obstruction used by +Matarener in #3825. We credit that obstruction and do not claim it as new. + +## Attainment by mixed-radix coordinates + +Set N = product(T_i), and let s_i = product(T_j for j < i), so s_1=1. +Every integer z in [0,N) has a unique mixed-radix representation + + z = sum_i d_i s_i, 0 <= d_i < T_i. + +Use only the actual records x in [0,n), assigning each the initial virtual +coordinate z=x. Coordinates in [n,N) are absent; no padding records or +payload operations on them are required. + +At pass i, assign a record to lane d_i of its current coordinate. Replace +that coordinate by + + z' = z + (T_i - 1 - 2 d_i) s_i. + +This complements exactly digit i. All other digits remain unchanged, +so the operation is a bijection of [0,N). For a fixed lane d_i, the +coordinate change is a constant translation. It therefore preserves the +relative order of every pair in that lane. Output records in increasing +order of z'. Their restriction to each lane is exactly its input stream, +so this is an allowed merge. Only the n real records are sorted or routed. + +After all k passes every digit is complemented, and a record initially +at x has coordinate + + sum_i (T_i - 1 - d_i) s_i = N - 1 - x. + +Here sum_i (T_i-1)s_i = N-1 follows by telescoping +T_i s_i - s_i = s_(i+1) - s_i. Increasing final coordinates therefore give +the record order n-1,...,0. This proves attainment and the theorem. +When k=0, the hypothesis forces n=1 and the empty route already suffices. +Radix-one stages are identity passes and cause no exception. + +For example, n=7 and (T_1,T_2)=(3,3) give the actual record orders + + 0 1 2 3 4 5 6 + 2 1 0 5 4 3 6 + 6 5 4 3 2 1 0. + +The first lane assignments are 0,1,2,0,1,2,0. The second assignments, in +the displayed intermediate order, are 0,0,0,1,1,1,2. No eighth or ninth +record is present. This attains the two-pass lower bound with three lanes. + +## Independent finite minimum check + +For a permutation p, let w(p) be its longest decreasing-subsequence length. +One pass with T lanes exists exactly when w(p) <= T. Necessity holds since +a decreasing subsequence uses different lanes. For sufficiency, label each +entry by the longest decreasing-subsequence length ending at that entry. +If two entries have equal labels, their order in p agrees with their +natural increasing order: an inverted pair would increase the latter +entry's label. Thus each label class is an increasing subsequence, and +these classes give at most T stable lanes. This is the classical chain +partition argument, included to specify the finite check's full alphabet. + +The independent shortest-path checker enumerates every permutation of +orders one through six. It permits every generator with w(p) <= T for +T=2,3,4 and breadth-first searches for reversal. It does not use the +mixed-radix constructor to choose generators or determine distances. +Its finite agreement corroborates the theorem; the proof above supplies +the unrestricted quantifiers. James Reed's #3839 finite composition +census is a credited predecessor and is not replayed. + +## Scope and remaining obligations + +The added step is attainment of the reversal pass obstruction, including +heterogeneous lane counts and arbitrary incomplete virtual grids. No +claim of historical novelty for radix routing, chain partitioning or the +lower-bound method is made. The theorem does not classify the optimal +pass depth of other permutations. It does not price an admitted supplier, +give an unconditional multitape lower bound, alter a selected ledger or +prove a complete multiplication theorem. Independent human and formal +proof-kernel review are unclaimed. diff --git a/research/physical-three-lane-reversal/machine.py b/research/physical-three-lane-reversal/machine.py new file mode 100644 index 0000000000..4d687da7d5 --- /dev/null +++ b/research/physical-three-lane-reversal/machine.py @@ -0,0 +1,177 @@ +"""Fixed three-lane local program; JoyboyBrian with OpenAI assistance, Apache-2.0. +Builder/Tape instruction semantics credited to retained PR5090. +""" +import importlib.util +from pathlib import Path +_spec = importlib.util.spec_from_file_location('reversal_instruction_source', Path(__file__).resolve().parents[1] / 'bit-row-padding-physical/machine.py') +source = importlib.util.module_from_spec(_spec) +import sys +sys.modules[_spec.name] = source +_spec.loader.exec_module(source) +Builder, Tape, BLANK, LEFT, need = source.Builder, source.Tape, source.BLANK, source.LEFT, source.need +SOURCE, BD, B, TEMP = 0, 4, 8, 10 +LANES = (5, 6, 7) +S, N, DATA, NEXT, OUTPUT = 9, 11, 12, 13, 14 +WORK = (*LANES, B, TEMP, S, N, DATA, NEXT) + + +class Control(Builder): + def row(self, src, dst, consume=False): + loop, bit, zero, one, end = [self.fresh('row') for _ in range(5)] + self.mark(loop) + self.read(B, {'1': bit, BLANK: end}) + self.mark(bit) + self.read(src, {'0': zero, '1': one}) + self.mark(zero) + self.write(dst, '0') + self.go(one + 'written') + self.mark(one) + self.write(dst, '1') + self.mark(one + 'written') + if consume: + self.write(src, BLANK) + self.move(src, 1) + self.move(dst, 1) + self.move(B, 1) + self.go(loop) + self.mark(end) + self.rewind(B) + + def chunk(self, src, dst): + loop, available, record, end = [self.fresh('chunk') for _ in range(4)] + self.mark(loop) + self.read(S, {'1': available, BLANK: end}) + self.mark(available) + self.read(src, {'0': record, '1': record, BLANK: end}) + self.mark(record) + self.row(src, dst, True) + self.move(S, 1) + self.go(loop) + self.mark(end) + self.rewind(S) + + def transfer(self, src, dst, consume=False): + loop, zero, one, end = [self.fresh('transfer') for _ in range(4)] + self.mark(loop) + self.read(src, {'0': zero, '1': one, BLANK: end}) + self.mark(zero) + self.write(dst, '0') + self.go(one + 'written') + self.mark(one) + self.write(dst, '1') + self.mark(one + 'written') + if consume: + self.write(src, BLANK) + self.move(src, 1) + self.move(dst, 1) + self.go(loop) + self.mark(end) + self.rewind(src) + self.rewind(dst) + + +def program(): + global STAGE_PC + c = Control() + c.unary(BD, B) + scan, record, copied = [c.fresh('input') for _ in range(3)] + c.mark(scan) + c.read(SOURCE, {'0': record, '1': record, BLANK: copied}) + c.mark(record) + c.row(SOURCE, DATA) + c.write(N, '1') + c.move(N, 1) + c.go(scan) + c.mark(copied) + for t in (SOURCE, DATA, N): c.rewind(t) + c.write(S, '1') + test, nmore, pair, covered, route = [c.fresh('cover') for _ in range(5)] + c.mark(test) + c.read(N, {'1': nmore, BLANK: covered}) + c.mark(nmore) + c.read(S, {'1': pair, BLANK: route}) + c.mark(pair) + c.move(N, 1) + c.move(S, 1) + c.go(test) + c.mark(route) + c.rewind(N) + c.rewind(S) + split, splitmore, splitend = [c.fresh('split') for _ in range(3)] + c.mark(split) + c.read(DATA, {'0': splitmore, '1': splitmore, BLANK: splitend}) + c.mark(splitmore) + for lane in LANES: c.chunk(DATA, lane) + c.go(split) + c.mark(splitend) + for t in (DATA, *LANES): c.rewind(t) + merge, mergemore, mergeend = [c.fresh('merge') for _ in range(3)] + c.mark(merge) + c.read(LANES[0], {'0': mergemore, '1': mergemore, BLANK: mergeend}) + c.mark(mergemore) + for lane in reversed(LANES): c.chunk(lane, DATA) + c.go(merge) + c.mark(mergeend) + STAGE_PC = len(c.code) + for t in (DATA, *LANES): c.rewind(t) + triple, unit, tripled = [c.fresh('triple') for _ in range(3)] + c.mark(triple) + c.read(S, {'1': unit, BLANK: tripled}) + c.mark(unit) + c.write(S, BLANK) + c.move(S, 1) + for _ in range(3): + c.write(NEXT, '1') + c.move(NEXT, 1) + c.go(triple) + c.mark(tripled) + c.rewind(S) + c.rewind(NEXT) + c.transfer(NEXT, S, True) + c.go(test) + c.mark(covered) + c.rewind(N) + c.rewind(S) + c.transfer(DATA, OUTPUT, True) + for t in WORK: c.clear(t) + c.code.append(('done',)) + c.mark('reject') + c.code.append(('rejected',)) + c.mark('quarantine') + c.code.append(('quarantined',)) + return c.finish() + + +PROGRAM = program() + + +class Machine: + def __init__(self, tapes): + need(len(tapes) == 15 and len({id(t) for t in tapes}) == 15, 'fifteen distinct ports') + self.tapes, self.pc, self.steps = tapes, 0, 0 + + def run(self, budget=10000000): + while self.steps < budget: + ins = PROGRAM[self.pc] + op = ins[0] + self.steps += 1 + if op == 'done': return + if op in ('rejected', 'quarantined'): raise ValueError(op) + if op == 'goto': + self.pc = ins[1] + continue + t = self.tapes[ins[1]] + if op == 'read': + symbol = t.read() + need(symbol in ins[2], 'local symbol') + self.pc = ins[2][symbol] + continue + if op == 'write': + t.read() + t.cells[t.head] = ins[2] + elif op == 'move': + t.head += ins[2] + t.read() + else: raise ValueError('unknown opcode') + self.pc += 1 + raise ValueError('execution budget') diff --git a/research/physical-three-lane-reversal/verify.py b/research/physical-three-lane-reversal/verify.py new file mode 100644 index 0000000000..dbb10163f0 --- /dev/null +++ b/research/physical-three-lane-reversal/verify.py @@ -0,0 +1,128 @@ +"""Exact finite corroboration, full frames and fail-closed frozen inputs.""" +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + +def need(ok, message): + if not ok: raise ValueError(message) + + +def pins(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + for row in manifest['files']: + if row['usage'] != 'input': continue + need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], 'source pin: '+row['path']) + row = manifest['external_public_input'] + need(hashlib.sha256((HERE / row['local_path']).read_bytes()).hexdigest() == row['sha256'], 'PR5148 exact proof') + + +def load(): + spec=importlib.util.spec_from_file_location('reversal_science', HERE/'machine.py') + m=importlib.util.module_from_spec(spec) + spec.loader.exec_module(m) + return m + + +def fixture(m,n,width,shift=0): + rows=[format((i*37+11)%(1<=origins[i], 'no visit before marker') + if i in (m.SOURCE,m.BD,1,2,3):need((t.cells,t.head)==saved[i], 'borrowed/unused full frame') + elif i!=m.OUTPUT:need(all(v==m.BLANK for p,v in t.cells.items() if p!=origins[i]),'work erased') + k=0;s=1 + while s Date: Fri, 23 Oct 2026 04:51:45 -0700 Subject: [PATCH 2/3] Check reversal stage boundaries and runtime width carries --- .../physical-three-lane-reversal/PROOF.md | 4 +- .../physical-three-lane-reversal/README.md | 3 +- .../physical-three-lane-reversal/RESULT.json | 66 +++++++++++++++++++ .../physical-three-lane-reversal/verify.py | 3 +- 4 files changed, 73 insertions(+), 3 deletions(-) diff --git a/research/physical-three-lane-reversal/PROOF.md b/research/physical-three-lane-reversal/PROOF.md index 6039e5b543..8f7bc20526 100644 --- a/research/physical-three-lane-reversal/PROOF.md +++ b/research/physical-three-lane-reversal/PROOF.md @@ -10,7 +10,9 @@ of B. These are supplied ports, each with a left marker, head at its first payload cell, and blank tail. OUTPUT and the work ports are blank after their left markers. All15 ports are distinct. Ports1,2,3 are untouched. The local alphabet is {0,1,blank,left}; the compiled instruction table is -independent of n and B. The interpreter executes only single-cell reads, +independent of n and B. The interpreter's step counter and low/high water diagnostics are observers, +not control registers of the mathematical program. The interpreter executes +only single-cell reads, writes, unit head moves and finite jumps. Its host step cap is a verifier stop, not an input to the mathematical machine. diff --git a/research/physical-three-lane-reversal/README.md b/research/physical-three-lane-reversal/README.md index d39528a6a0..04972b5a5e 100644 --- a/research/physical-three-lane-reversal/README.md +++ b/research/physical-three-lane-reversal/README.md @@ -18,7 +18,8 @@ The abstract pass count alone is not a physical tariff or a numerical gain. The verifier checks492 cases with independent record-array expectations, translated origins, full borrowed/unused frames, every work tape and head, -written action/backing bounds, and the exact seven-record two-pass source +written action/backing bounds, eight additional power-of-three/binary-carry +cases through n244 and B1024, and the exact seven-record two-pass source example. Eight controls include actual output-bit and guide corruption. These are finite corroboration of the scoped proof, not a proof kernel or a complete multiplication theorem. diff --git a/research/physical-three-lane-reversal/RESULT.json b/research/physical-three-lane-reversal/RESULT.json index c1f6261dde..245a8ce3f1 100644 --- a/research/physical-three-lane-reversal/RESULT.json +++ b/research/physical-three-lane-reversal/RESULT.json @@ -3,6 +3,72 @@ "claim": "fixed-three-lane physical valid-input reversal", "cases": 492, "cases_sha256": "534d2e2b3f5888900fc2297bf1e3e57a6e038d5c572d75bee9d5bff26c4b6e95", + "carry_and_stage_boundaries": [ + { + "n": 80, + "B": 2, + "origin": 31, + "steps": 43315, + "backing": 933, + "stage_records": [] + }, + { + "n": 81, + "B": 2, + "origin": 31, + "steps": 43770, + "backing": 942, + "stage_records": [] + }, + { + "n": 82, + "B": 2, + "origin": 31, + "steps": 59151, + "backing": 1381, + "stage_records": [] + }, + { + "n": 242, + "B": 1, + "origin": 31, + "steps": 103806, + "backing": 1744, + "stage_records": [] + }, + { + "n": 243, + "B": 1, + "origin": 31, + "steps": 104155, + "backing": 1749, + "stage_records": [] + }, + { + "n": 244, + "B": 1, + "origin": 31, + "steps": 139928, + "backing": 2887, + "stage_records": [] + }, + { + "n": 7, + "B": 129, + "origin": 31, + "steps": 97401, + "backing": 3956, + "stage_records": [] + }, + { + "n": 3, + "B": 1024, + "origin": 31, + "steps": 235098, + "backing": 13388, + "stage_records": [] + } + ], "program_instructions": 419, "max_steps": 126932, "seven": { diff --git a/research/physical-three-lane-reversal/verify.py b/research/physical-three-lane-reversal/verify.py index dbb10163f0..7bff452801 100644 --- a/research/physical-three-lane-reversal/verify.py +++ b/research/physical-three-lane-reversal/verify.py @@ -87,6 +87,7 @@ def rejected(call): def science(): m=load() cases=[check(m,n,w,shift) for shift in (0,19,-23) for n in range(41) for w in (1,3,7,17)] + stress=[check(m,n,w,31) for n,w in ((80,2),(81,2),(82,2),(242,1),(243,1),(244,1),(7,129),(3,1024))] seven=check(m,7,3,trace=True) rows=fixture(m,7,3)[0] need(seven['stage_records']==[[rows[i] for i in p] for p in ([2,1,0,5,4,3,6],[6,5,4,3,2,1,0])], 'source seven-record stages') @@ -109,7 +110,7 @@ def science(): finally:m.PROGRAM=original data=json.dumps(cases,sort_keys=True,separators=(',',':')).encode() return {'schema_version':1,'claim':'fixed-three-lane physical valid-input reversal','cases':len(cases), - 'cases_sha256':hashlib.sha256(data).hexdigest(),'program_instructions':len(m.PROGRAM), + 'cases_sha256':hashlib.sha256(data).hexdigest(),'carry_and_stage_boundaries':stress,'program_instructions':len(m.PROGRAM), 'max_steps':max(x['steps'] for x in cases),'seven':seven,'controls':controls, 'unrun':['production bit-free supplier composition','heterogeneous runtime lane counts']} From 9fb200b4d556ec47905e871ab108d3b3ea74190a Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Fri, 23 Oct 2026 04:58:19 -0700 Subject: [PATCH 3/3] State initial head contract for every reversal port --- research/physical-three-lane-reversal/PROOF.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/research/physical-three-lane-reversal/PROOF.md b/research/physical-three-lane-reversal/PROOF.md index 8f7bc20526..39dc08f7c4 100644 --- a/research/physical-three-lane-reversal/PROOF.md +++ b/research/physical-three-lane-reversal/PROOF.md @@ -8,7 +8,9 @@ For every n>=0 and B>=1, SOURCE contains n consecutive B-bit records and BD contains the canonical least-significant-first positive binary encoding of B. These are supplied ports, each with a left marker, head at its first payload cell, and blank tail. OUTPUT and the work ports are blank after -their left markers. All15 ports are distinct. Ports1,2,3 are untouched. +their reliable left markers. Every port, including unused ports1,2,3, +starts with its head at its own origin+1. All15 ports are distinct. +Ports1,2,3 may contain arbitrary payload after their markers and are untouched. The local alphabet is {0,1,blank,left}; the compiled instruction table is independent of n and B. The interpreter's step counter and low/high water diagnostics are observers, not control registers of the mathematical program. The interpreter executes