Lower all five interchange entries to literal binary tapes

research/binary-elementary-interchange/README.md

@@ -0,0 +1,131 @@
+# Binary elementary interchange
+
+This package closes the first open question in the literal elementary
+interchange package: a fixed block encoding and an actual binary alignment
+program. It lowers all 4,589 source instructions and all five entries to
+58,608 binary instructions on the same 20 tapes. The program does not depend
+on the input width. Runtime instructions contain no source executor,
+numeric loop bound, allocator callback, or decoded geometry.
+
+The proof below gives exact state, cost, and retained-storage refinement.
+RESULT.json records 68 full entry comparisons over 16 sessions, including
+eight independent payload columns, caller install, and a growing then
+shrinking call history. The verifier also checks 153 local instruction cases,
+three unused codewords, and seven failure controls. Finite checks support the
+written proof; they do not replace it.
+
+Run from the repository root with Python 3.12 and the standard library:
+
+```sh
+python3 -I -W error -B research/binary-elementary-interchange/verify.py
+python3 -I -O -W error -B research/binary-elementary-interchange/verify.py
+python3 -B scripts/research_package.py --package research/binary-elementary-interchange
+```
+
+The direct result is `PASS_BINARY_ELEMENTARY_INTERCHANGE`.
+SOURCES.json pins every consumed source at
+`ff3cc58e370d0f678e529246f8c73e8094e18fcf`. The verifier checks these bytes
+before and after execution. A fresh test-only directory runs the unmodified
+source machine; the binary runtime does not call it. The complete receipt
+is compared with typed canonical JSON, including under optimized Python.
+
+## Refinement theorem
+
+Encode the five source symbols ZERO, ONE, LEFT, RIGHT, BLANK as 001, 010,
+011, 100, 000, respectively. Each allocated source cell becomes three
+allocated binary cells. A source head at h becomes a binary head at 3h.
+Unallocated source cells are BLANK; unallocated binary cells are zero.
+Thus both views have the same blank extension. Tape roles remain disjoint.
+
+At a source instruction boundary, let the source and binary states obey
+this relation. The lowered program has the following behavior.
+
+1. A test reads all three bits through a fixed depth-three decision tree.
+   Two unit moves advance the head. At each leaf, two unit moves restore
+   it. Each of the five valid leaves jumps to the matching source successor.
+   Each unused codeword halts with `rejected` after head restoration. A valid
+   test uses three reads, four moves and one jump. It changes no tape cell.
+2. A write stores all three bits. Two forward and two backward unit moves
+   restore the head. A jump reaches the next source instruction. This uses
+   three writes, four moves and one jump. If a write extends the source
+   array to h+1 cells, the last binary write extends its array to 3(h+1).
+   Every gap is zero. This also holds when the new symbol is BLANK.
+3. A legal source unit move becomes three binary unit moves and one jump.
+   It allocates no cells. Legal left moves cannot cross the binary origin.
+4. A source jump becomes one binary jump. A source halt keeps its status.
+
+These cases prove the state relation by induction at every source
+instruction boundary. All tests have a bounded depth. Every inserted path
+reaches a source successor or a halt. Compilation checks the complete
+finite instruction alphabet and rejects control-only cycles. The actual
+binary program has at most three consecutive jump instructions; its
+control factor is four. No extra head or tape is required.
+
+Suppose a terminating source entry has R reads, W writes, M moves, J jumps
+and one halt. The binary entry has exactly
+
+```text
+reads  = 3R
+writes = 3W
+moves  = 4R + 4W + 3M
+jumps  = R + W + M + J
+steps  = 8R + 8W + 4M + J + 1 <= 8(R + W + M + J + 1).
+```
+
+Allocated length is exactly three times source allocated length at each
+source boundary. During a microprogram it does not exceed the length at
+the next source boundary. Reads and moves do not allocate. All three bit
+writes are charged even for zero. Therefore erased backing remains in the
+account. For every valid sequence of calls, the binary retained-storage
+history is three times the corresponding source history. This is a
+relative theorem; it does not supply a new absolute source-space bound.
+
+Apply the theorem to the source program's valid domain: H >= 0,
+A,G,S >= 1, V = A*4^H*G*S, canonical encoded descriptors and disjoint roles.
+The source proof supplies the interchange permutation and five-entry
+lifecycle. The binary program inherits those properties on encoded states.
+If L = H + bit_length(H) + bit_length(A) + bit_length(G) + bit_length(S) + 8,
+with bit_length(0) taken as one, its complete init/run/consume/close session
+cost is at most 2^23*(H+1)*(V+1)*(L+1)^2. This follows from the source bound
+2^20*(H+1)*(V+1)*(L+1)^2 and the instruction factor eight. Caller install
+has the exact per-entry factor above; the quoted session excludes install.
+
+## Scope and limits
+
+This is a finite program plus a written uniform representation proof.
+It uses the source program's all-width correctness proof as a premise.
+The finite replay here has maximum H=3 and V=64. It does not repeat the
+predecessor's 196,608-cell source fixture or claim a new all-size acceptance.
+The proof applies to all valid widths because its induction is per opcode.
+
+Encoded descriptors and payloads are supplied at the boundary. The Python
+fixture encoder is not a free runtime adapter. A caller must provide encoded
+data directly or pay for a separate codec, its heads, storage and disposal.
+Unused codewords are rejected only when a test reads them; this is not a
+global input validator or an error rollback guarantee. State refinement
+does not cover a source move that crosses the origin.
+
+No selected file, supplier, physical stock, native operator, precision claim,
+ROM producer, whole raw/repair caller, outer recovery proof or complete
+kappa calculation changes. Selected kappa remains 60403/20000000. There is
+no independent human or proof-kernel acceptance claim.
+
+## Open next questions
+
+- Integrate the encoded callee with the complete raw/repair caller. Identify
+  the representation of every port and pay every codec and lifecycle cost.
+- Apply a source retained-backing theorem to obtain an absolute binary
+  storage grant. Include all old erased arrays and varying call histories.
+- Independently check the source all-width proof and this instruction
+  refinement. A finite execution receipt alone cannot discharge either.
+
+## Attribution
+
+JoyboyBrian supplied the literal five-symbol program, lifecycle, source
+proof and binary-lowering handoff in PR #5188. Its source notices retain
+Jose Manuel's ordinary wrapper, the PR #2809 and PR #2753 stream/cardinality
+authors, Cinna Davis, Hiroki KUMAZAKI and Douglas Colkitt. This package does
+not modify those sources. PR #5286 is related retained-backing work; it is
+not a consumed proof premise here. Ali Romman prepared this refinement
+with substantial OpenAI Codex assistance in proof, code and verification.
+Apache-2.0.

research/binary-elementary-interchange/RESULT.json

@@ -0,0 +1,43 @@
+{
+  "status": "PASS_BINARY_ELEMENTARY_INTERCHANGE",
+  "source_program_length": 4589,
+  "binary_program_length": 58608,
+  "binary_program_sha256": "38ade5f7598b0f4aa9ec23a37ce0ebb80ec917c286dacd2d9c2e36e23a4ab931",
+  "entries": {
+    "init": 0,
+    "run": 736,
+    "consume": 56493,
+    "install": 56644,
+    "close": 57256
+  },
+  "binary_control_factor": 4,
+  "tape_roles": 20,
+  "sessions": 16,
+  "entry_comparisons": 68,
+  "source_steps": 122805,
+  "binary_actions": {
+    "steps": 654512,
+    "reads": 133569,
+    "writes": 38706,
+    "moves": 359432,
+    "jumps": 122737
+  },
+  "source_states_sha256": "6f34cb280908c6ceaba0666302745d36b6136e57b38b2e0e7fa12fdad4d52580",
+  "controls": {
+    "positive": 153,
+    "invalid_codewords": 3,
+    "rejected": [
+      "left_origin_crossing",
+      "missing_alignment_move",
+      "wrong_bit",
+      "missing_tail_write",
+      "host_callback",
+      "control_only_cycle",
+      "nonbinary_write"
+    ]
+  },
+  "code_sha256": {
+    "binary_machine.py": "3fe87e8919d99ea2767db0a468e11668e337e71b7074216de756d0a4a967c977",
+    "reference.py": "2d99f27d841a57a4f0a839bf7b31ab6d9f8f7cc0306079571ecde100396367c7"
+  }
+}

research/binary-elementary-interchange/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/literal-elementary-interchange/PROOF.md",
+      "usage": "input",
+      "git_blob": "d4e14bba3fe10e0f269b0891b0e196b723b651cf",
+      "sha256": "507684173bde7865161d641bbffc6862c1e825407c42efa70747c763dadd03af"
+    },
+    {
+      "path": "research/literal-elementary-interchange/RESULT.json",
+      "usage": "input",
+      "git_blob": "d2f4588b53837d22be39636c6661772196b594e9",
+      "sha256": "a8d4746eb333ea0fcb1d6f613f09b122f7d7a029390dab0df07a4cefb7164c73"
+    },
+    {
+      "path": "research/literal-elementary-interchange/machine.py",
+      "usage": "input",
+      "git_blob": "78dc14bf1c995b5ea348d2e753cf9f56dbdb480b",
+      "sha256": "66b5c371ff4aebd4391d71b95c59769a067e0a04910521b4881f074f986327bf"
+    },
+    {
+      "path": "research/literal-elementary-interchange/program.py",
+      "usage": "input",
+      "git_blob": "c606ed51a06409a648d3fd385b0dfdaa5e096720",
+      "sha256": "3b83fbe3451000b00030ff3156222def23ce15d17d00c7d09a324aea5fd92e72"
+    }
+  ]
+}

research/binary-elementary-interchange/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "refined",
+  "actual_scope": "Fixed binary instruction lowering of all five entries in the literal elementary interchange program.",
+  "scope_change_reason": "The selected bit-mechanisms seed 73182b1ebd6c4262508b6370f43eb467 led to the explicit binary-alphabet handoff in PR #5188. This is a uniform-transfer representation obligation.",
+  "bottleneck_link": "Remove the finite five-symbol alphabet obligation at the actual interchange callee. Whole-caller integration remains open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop on an uncharged runtime codec, extra tape, failed state refinement, or source-sized replay claim without execution.",
+  "outcome": "completed",
+  "evidence": "README.md, RESULT.json, verify.py",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or kernel review.",
+  "open_questions": [
+    {
+      "question": "Integrate all encoded caller ports.",
+      "why_it_matters": "A representation theorem does not pay codecs.",
+      "first_step": "List port representations and explicit codec programs.",
+      "blocked_by": "Whole caller construction."
+    },
+    {
+      "question": "Give an absolute binary retained-storage grant.",
+      "why_it_matters": "The current bound is relative to source storage.",
+      "first_step": "Compose a verified source history bound with factor three.",
+      "blocked_by": "Source storage theorem intake."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19150847"
+}

research/binary-elementary-interchange/VERIFY.json

@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/literal-elementary-interchange/PROOF.md",
+    "research/literal-elementary-interchange/RESULT.json",
+    "research/literal-elementary-interchange/machine.py",
+    "research/literal-elementary-interchange/program.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Fixed-program state, exact cost, backing extent, source bytes, and failure controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete checks with assertions disabled."
+    }
+  ]
+}