Realize stable three-lane reversal with a paid fixed local program

research/physical-three-lane-reversal/PROOF.md

@@ -0,0 +1,123 @@
+# 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 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
+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<k}3^i=(3^k-1)/2<3n/2
+for n>=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.

research/physical-three-lane-reversal/README.md

@@ -0,0 +1,56 @@
+# 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, 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.
+
+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.

research/physical-three-lane-reversal/RESULT.json

@@ -0,0 +1,115 @@
+{
+  "schema_version": 1,
+  "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": {
+    "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"
+  ]
+}

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