Independently check #4541's packed IO codec: separate codec from the spec, all bit orders, caps, shared tape, mutations (no new κ)

research/pr4541-packed-io-check/.gitattributes

@@ -0,0 +1 @@
+PR4541-PACKED-IO.md -text

research/pr4541-packed-io-check/PR4541-PACKED-IO.md

@@ -0,0 +1,159 @@
+# Packed binary IO without a linear bit-by-bit RAM bottleneck
+
+Prepared by Dugongue with substantial OpenAI Codex assistance. Apache-2.0.
+This is a constructive bounded-word algorithm and an informal universal proof,
+with finite operational-model checks. It is not an emitted RamStd program,
+a fresh Lean theorem, or an improved multitape-TM exponent.
+
+## Protocol and sufficient theorem
+
+Fix c>=2, a power of two, and r>=1, also a power of two. The simulated tape
+alphabet uses blank symbol 0 and logical bit codes 1,2. Other symbols may exist
+internally, but an output binary prefix contains only 1 and 2 before its first
+blank. Let beta=2^r. An n-bit operand arrives in exactly ceil(n/r) little-endian
+base-beta digit words; the final digit's unused high bits must be zero. The
+length header n, table arenas, input/output arrays and all pointers fit in
+bounded w-bit words. Require 2cr+8<w and enough arena space for the tables plus
+the actual buffers. The table-address envelope itself is O(2^(cr)) words; this
+is an explicit memory requirement, not a zero-cost table oracle.
+
+There are generated tables and one uniform additive/Boolean algorithm with:
+
+- setup at most 100 r 2^(cr) charged word operations;
+- input expansion at most 100(ceil(n/r)+1) charged operations, producing either
+  LSB-first or the usual MSB-first binary symbol stream in packed c-bit cells;
+- output conversion at most 160(ceil(m/r)+1) charged operations, reading a
+  usual MSB-first coded binary prefix of at most m cells until blank or the
+  m-cell cap, and emitting exactly ceil(m/r) little-endian beta digits with
+  all unused high bits zero.
+
+Input/output setup, table indexing, chunk reversals, partial chunks and high
+zero padding are all included. Each external input digit is read O(1) times,
+and each external output digit is written once. No external bit-per-word stream
+is introduced. Every variable scaling by c or r is a shift because those
+parameters are powers of two. Multiplication and division instructions are not
+used. The constants above are operational-model envelopes, not certified exact
+RamStd instruction counts; the finite loop bodies admit constant-size lowering.
+
+## Table construction
+
+For every 0<=x<2^r, enumerate its r logical bits and generate
+
+    E[x]  = sum_j (1 + bit_j(x)) << (cj),
+    Er[x] = sum_j (1 + bit_(r-1-j)(x)) << (cj).
+
+The displayed sums describe the object. The constructor uses a bounded loop,
+bit tests, shifts and OR, never a multiplication instruction. For every
+0<=y<2^(cr), enumerate its c-bit cells from low to high. Stop at the first blank.
+Reject a cell outside {1,2} only if it occurs before that blank. Record
+(length, value, valid), where value is the ordinary integer represented by the
+MSB-first logical prefix seen. Its recurrence is value <- (value<<1) OR (cell-1).
+Consequently its little-endian bits are exactly the reverse of that prefix.
+Use a fixed power-of-two row stride for these metadata triples.
+
+Enumeration takes O(r 2^(cr)) operations and O(2^(cr)) words. Invalid table
+keys have defined entries and do not require a promise that every row is valid.
+Only entries reached by actual valid input/output data must have valid=true.
+All table keys and outputs use at most cr+O(1) bits, so the stated word width
+and a disjoint arena prevent address/value wrap. Setup is recomputed from r,c;
+it is neither supplied as advice nor generated by an unpriced root/bit oracle.
+
+## Input correctness
+
+For LSB-first TM input, traverse input digits from low to high and use E[x].
+For the highest partial digit of ell bits, retain only its low c*ell encoded
+bits so that unused tape cells remain genuinely blank, rather than coded
+logical zero.
+
+For MSB-first input, traverse digits from high to low and use Er[x]. The highest
+partial digit has ell bits, so shift Er[x] right by c(r-ell): this removes its
+coded leading zero fields and retains exactly bits ell-1,...,0. Every remaining
+digit has r bits and needs no adjustment. No unbounded bit reversal is assumed.
+
+Append each at-most-r-cell result to a reservoir holding fewer than r cells.
+If at least r cells are present, flush the low r to the packed output stream
+and shift the residual down. At most one flush is needed per append. The
+invariant is that flushed fields followed by the reservoir are exactly the
+processed logical prefix, in the selected bit order. At the end, emit any
+remaining fields with zero high padding. This proves both bit orders and
+ensures that after the n input symbols every uninitialized tape cell is blank.
+At every step the reservoir contains fewer than 2r cells, hence fewer than
+2cr bits. The supplied width bound pays for every intermediate shift.
+
+The packed simulated-tape representation may hold 4r cells per RAM word, as
+in the companion tabulation backend. Each produced r-cell chunk is inserted
+by at most two masked word writes at an arbitrary starting alignment; this is
+O(1) actual word work. An origin aligned to 4r simplifies it to one word per
+chunk plus retention of the other subchunks. No per-symbol initialization is
+needed. The overwritten fields represent input symbols; neighboring initially
+blank fields and all other tapes remain unchanged.
+
+## Output correctness and termination
+
+Read the simulated tape in r-cell chunks, masking the last chunk to the m-cell
+cap. Lookup its decoder entry. Stop immediately after the first blank or after
+m payload cells; later chunks are not read. Retain its at-most-r-bit value and
+its actual prefix length. Valid earlier chunks have length r, and only the
+last can have a shorter payload. The all-blank output prefix represents zero.
+If the output has m bits, its terminator may lie beyond the scanned cap and
+need not be read. An absent stream that supplies neither enough payload nor a
+terminator is a malformed protocol and rejects.
+
+Traverse the retained chunk descriptors in reverse order. For each descriptor,
+append its value and length to a binary reservoir. Its low-to-high bits are
+the reversal of that chunk's original MSB prefix. Reversing the chunk order
+therefore reverses the entire original bit prefix, including partial chunks
+and leading logical zeros. The same reservoir invariant as for input proves
+that the emitted low-to-high digit bits represent exactly the original integer.
+Append zero digits until exactly ceil(m/r) output words exist, and mask any
+unused high bits in the final output word. This is padding at the high end of
+an LSB encoding, so it preserves the value. Appending zeros to the original MSB
+word would not preserve it and is not used.
+
+Descriptor storage, its reverse traversal and the final padding use
+O(ceil(m/r)) words and operations. Zero cap emits no word and reads no tape
+chunk. Dirty symbols after the first terminator are irrelevant. The decoder
+rejects invalid symbols before it, rather than silently treating a marker as
+a logical bit. A distinct fixed end marker can be added to the decoder's
+termination test at constant cost; the checked version specifically uses 0.
+
+## Combination with the full local-configuration table
+
+For a fixed k-tape machine and polynomial running-time envelope, choose the
+common epoch/chunk r=Theta(log(n+2)) small enough that
+
+    Q * 2^(kc(2r+1)) <= (n+2)^epsilon
+
+for one fixed 0<epsilon<1. Rounding r down to a power of two changes only its
+constant factor. The codec's 2^(cr) rows are dominated by this complete machine
+configuration table (up to fixed constants). Their setup costs are therefore
+O(n^epsilon polylog n), and their active IO costs are O(n/log n).
+
+A complete r-step macro simulation costing O(1) word operations per epoch
+then combines with these codecs to give
+
+    O(T(n)/log(n+2) + n/log(n+2) + n^epsilon polylog n)
+
+bounded-word RAM operations on the packed protocol. For a complete conditional
+multitape multiplication theorem T(n)=O(n log^(1-kappa)(n+2)), 0<kappa<1, this
+is O(n/log^kappa(n+2)) word operations. The former bit-per-word wrapper's O(n)
+term is genuinely removed: the implementation consumes and produces
+Theta(n/log n) digit words instead. This is a model-relative consequence with
+inherited hypotheses; it is not an improvement to the multitape κ or a claim
+of novelty for classical tabulation. It depends on the companion simulator's
+fully paid table and macro correctness, which are not proved by codec tests.
+
+## Evidence and provenance
+
+`python3 -I -O -B packed_codec.py` checks 4,277 cases across r=1,2,4,8 and c=2,4
+(where finite table sizes permit), both bit orders, partial chunks, leading
+zeros, capped full outputs, zero outputs, and dirty post-terminator cells.
+Seven actual decoder-entry mutations produce an incorrect represented integer
+and are detected; invalid pre-terminator symbols reject. The tests compare
+ordinary integer values and literal symbol streams independently of the tables.
+
+This extends the prior Word RAM deliverable's explicit restricted-RamStd model,
+packed-tape access and fixed-length LSB output contract. It retains their
+Problem 1.8 machine/compiler provenance. The uniform local-configuration
+simulation and its main proof are separate root-owned work. No canonical Lean
+module, shared DAG, selected frontier or prior research source was changed.

research/pr4541-packed-io-check/README.md

@@ -0,0 +1,43 @@
+# Independent check of #4541: packed IO codec (§4, `PACKED-IO.md`)
+
+**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.**
+
+This completes my coverage of Dugongue's #4541 (head `46ca24a8`). #4552 checked its §1 parameters and §§2–3 macro steps. This package checks the packed IO codec that the `O(n/(log n)^κ)` corollary needs. Without the codec, bit-per-word IO costs `Θ(n)`.
+
+The codec here was written from #4541's `PACKED-IO.md` text alone, vendored as `PR4541-PACKED-IO.md` with blob `675e520c` and its SHA256 pinned. Nothing is imported from #4541's `packed_codec.py`.
+
+## Results
+
+All checked claims are confirmed for `(r, c) ∈ {1,2,4,8}×{2} ∪ {1,2,4}×{4}`. That is 131,620 decoder rows built in full and 3,372 codec cases compared with direct binary encoding.
+
+- **Tables.** `E[x]` and `Er[x]` are built for `x < 2^r`, and the decoder `(length, value, valid)` for every `y < 2^(cr)` with `value ← (value≪1) | (cell−1)`. All keys and entries fit in `cr` bits.
+- **Input expansion.** Both bit orders produce exactly the operand's coded bit stream, followed by genuine blanks. Operand lengths include 0, `r±1`, `2r`, `2r+1`, `3r−1` and random lengths; values include 0, all-ones and random values. For an MSB-first partial top digit, `Er[x] ≫ c(r−ℓ)` gives exactly its ℓ bits.
+- **Reservoir.** It always holds fewer than `2r` cells (below `2^(2cr)` as a value), and at most one flush happens per append.
+- **Output.** Each run decodes an MSB-first coded prefix under caps `m ∈ {n, n+1, n+r, n+3}`, with dirty cells after the terminator. It emits exactly `⌈m/r⌉` LSB digit words of the right integer.
+  - When `m = n` the cap is full, and the terminator is not read.
+  - Leading logical zeros are preserved.
+  - An invalid cell before the blank rejects.
+  - A zero cap emits nothing.
+- **Shared tape.** A continuous reservoir across two operands and a delimiter gives the exact concatenated stream. Concatenating separately padded chunk streams differs, inserting blanks, in all 37 runs where `n₁` is not a multiple of `r`. This confirms #4541's warning.
+- **Controls.** All 25 sampled single-entry decoder mutations are detected by the round trip.
+- **Binding.** 7 formulas and statements are bound verbatim to the vendored spec.
+
+## Verify
+
+```text
+python3 -B research/pr4541-packed-io-check/verify.py
+```
+
+This runs in about 1 s with the standard library only.
+
+## Limitations
+
+- The operation-count envelopes (100 and 160 per digit, `100·r·2^(cr)` setup) are model constants, and they are not re-derived here. Only the structural facts behind them are checked: one flush per append, O(1) work per chunk and table size.
+- The corollary still needs a complete TM multiplier with the stated envelope, as #4541 says.
+- These are finite tests. The universal statement rests on the written reservoir and reversal invariants, which these tests corroborate.
+
+## Open next questions
+
+- An emitted RamStd lowering of the codec loops, to turn the operation envelopes into certified instruction counts. First step: lower `expand` for one fixed `(r, c)` and count instructions.
+
+Credit: Dugongue (#4541). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance.

research/pr4541-packed-io-check/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    }
+  ]
+}

research/pr4541-packed-io-check/TASK.json

@@ -0,0 +1,100 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 7,
+  "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/staged544-mixed-fourth-entry/README.md",
+      "research/staged-fourth-mixture-ceiling/README.md",
+      "research/r437-two-window-carrier/README.md"
+    ],
+    "methods": [
+      "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+      "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification.",
+      "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering",
+      "4088",
+      "4091",
+      "4067",
+      "staged544-mixed-fourth-entry",
+      "staged-fourth-mixture-ceiling",
+      "r437-two-window-carrier"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+        "evidence": "research/staged544-mixed-fourth-entry/README.md",
+        "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+        "status": "author-checked",
+        "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+        "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+        "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+        "status": "author-checked",
+        "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+        "evidence": "research/r437-two-window-carrier/README.md",
+        "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+        "status": "author-checked",
+        "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "unchanged",
+  "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "scope_change_reason": null,
+  "bottleneck_link": "Completes independent coverage of #4541's RAM transfer: the packed IO codec is what removes the Θ(n) IO term from the O(n/log^κ n) corollary.",
+  "budget_minutes": 40,
+  "stop_rule": "Stop at PACKED-IO.md's codec claims; operation-count constants not re-derived.",
+  "outcome": "completed",
+  "evidence": "Independent codec from the spec text: 131,620 decoder rows, 3,372 codec cases vs direct binary for 7 (r,c) configs; reservoir <2r cells with one flush per append; shared-tape continuity with padded-concatenation control (37); 25/25 decoder mutations detected; 7 statements bound to vendored spec.",
+  "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance",
+  "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+  "open_questions": [
+    {
+      "question": "Emitted RamStd lowering of the codec loops with certified instruction counts.",
+      "why_it_matters": "Turns the stated 100/160-per-digit envelopes into checked constants.",
+      "first_step": "Lower expand for one fixed (r,c) and count instructions.",
+      "blocked_by": "None."
+    }
+  ]
+}

research/pr4541-packed-io-check/VERIFY.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Independent packed IO codec from vendored PACKED-IO.md (sha256): tables, LSB/MSB expansion, reservoir bound, capped output decoding with reversal/padding, shared-tape delimiter, padded-concatenation control, decoder mutation controls."
+    }
+  ]
+}