Execute and price the CRT radix consumer in literal bit control

research/crt-binary-radix-consumer/PROOF.md

@@ -0,0 +1,170 @@
+# A literal binary pass at the CRT repair consumer
+
+JoyboyBrian, substantial OpenAI Codex assistance; Apache-2.0.
+
+## Boundary and quantified claim
+
+Take any n>=0 records `(v_i,k_i)` with `0<=v_i<4096` and nonempty finite
+binary key strings k_i. Set K=sum |k_i| and D=n+K. The bad tape is
+`< (R,v_1) k_1 ... (R,v_n) k_n >`, followed by blank cells. Each bucket
+has just the permanent `<` at cell zero and is otherwise blank. All three
+heads start at cell zero. Source symbols use the exact 4104-symbol alphabet
+of #4982; in particular, the other eight symbols are `_ L 0 1 R < > =`.
+The physical input consists of those symbols' thirteen-bit predecessor
+codewords, source cell j at physical cells 13j..13j+12. Codes 8..4095 are
+unused and excluded from this entry contract. Misaligned heads, dirty
+buckets, missing/duplicate outer markers and arbitrary unused binary codewords are
+not admitted inputs. Finite control may initially be arbitrary bits.
+
+The emitted fixed program returns the stable concatenation of the records
+with last key bit zero and then those with last key bit one. Each output
+key is rotated from a_1...a_l to a_l a_1...a_(l-1). The payload bits are
+opaque and unchanged. The bad tape has exactly the same occupied extent;
+its final END stays in source cell D+1. Both buckets become blank except
+for their permanent `<`. All heads and all finite-control bits return to
+zero. There are three physical tape roles, 72 one-bit control registers,
+180 source instructions and 3885 static binary instructions. This is one
+fixed program for all n and key lengths, not one program per test input.
+
+For a finite stream with exactly one LEFT (at cell zero), exactly one
+final END, and other symbols in the declared alphabet, validation rejects
+any malformed record/key structure before
+writing output. It returns the bad head and clears finite control, while
+bad and the empty buckets remain unchanged. Missing/duplicate LEFT or END and a nonzero initial head are outside
+the contract, not promised rejection cases. Unique LEFT is essential to
+the rewind invariant: an interior LEFT would stop a rejection rewind early.
+
+## Stable symbolic algorithm
+
+`radix.py` assembles the source algorithm in the unchanged #4752 Builder.
+The eight reserved-symbol comparisons recognize a record because the
+entry alphabet is precisely the eight reserved symbols plus 4096 records.
+No payload value is inspected or used as an address. First validate every
+record, followed by at least one key bit, and the final END; all validation
+reads only bad. Rewind bad before starting the output. Thus failure cannot
+partially change either stream.
+
+During partition the main invariant is that bad points to the next record
+or END, the completed records have appeared in order in their chosen
+buckets, and both bucket heads point to the next unused cell. Hold the
+payload in one finite register. Walk to the next record/END, step back to
+the final key bit, save it, and walk back across the key to its payload.
+The key is nonempty, so both scans terminate without crossing LEFT.
+Append payload and final bit to its chosen bucket. Hold the first original
+key bit; before each further key bit is consumed, append the held bit and
+replace it by the current bit. On the first nonbit, the final held bit is
+the original final key bit and is deliberately not appended again. This
+appends precisely the other l-1 bits and returns bad to the next payload.
+This also covers l=1: the inner append loop has no iteration.
+
+The invariant gives stable order within each bucket, including repeated
+keys and repeated payloads. Write an END on each bucket, rewind, and copy
+bucket zero followed by bucket one to bad. Exactly D data cells are copied;
+write the final END in D+1, then rewind all three. Erase bucket data and
+END, return their heads, preserve permanent LEFT. This proves the endpoint
+by induction on records and cells. It is the same endpoint as the retained
+`bridge.one_pass`, although validation and fixed-control branching have
+additional paid work. No assertion about an identical event trace is made.
+
+If all keys have length L>=1, repeat this same program L times on the same
+tapes. Pass j stably sorts on original bit L-j+1 and rotates it to the
+front. Induction is the standard stable LSD radix invariant; after L
+passes key orientation is restored and order is stable lexicographic
+ascending on the original keys. Buckets and control satisfy the next
+invocation's entry contract after each pass. The n=0 case also returns.
+
+## Full source-control and bit-action bill
+
+A source instruction is one read, write, unit symbol-head move, finite
+assignment/copy, equality, branch, jump or halt. There is no host integer
+key, length, address lookup, source-cell dictionary access or sort inside
+the emitted program. The assembler sees only the predecessor Builder;
+it receives no record, parameter n or L. Tape dictionaries, PC indices
+and counters in the emulator are observer metadata.
+
+For the 180-instruction source program, call a transfer backward when its
+next PC is no greater than its current PC. Between two backward transfers
+the PC strictly increases, so at most 180 instructions execute. The
+following are **all** backward transfers on a legal invocation. Bucket
+stream lengths D0,D1 satisfy D0+D1=D. Each rewind counts a jump for each
+source-cell step left, including the final END position.
+
+| Control section | Backward transfers |
+|---|---:|
+| Validation key/next-record branches | K |
+| Validation rewind from END | D+1 |
+| Right and left key scans | 2K |
+| Key rotation append loops | K-n |
+| Return to next record | n |
+| First three rewinds | 2D+3 |
+| Bucket copies | D |
+| Second three rewinds | 2D+3 |
+| Forward bucket erasure loops | D |
+| Final bucket rewinds | D+2 |
+
+Summing gives exactly B=4K+8D+9, including B=9 for the empty stream.
+The rejection rewind is unreachable on a legal input; it is not omitted
+from the program. Therefore source execution T satisfies
+
+`T <= 180*(B+1) = 180*(8n+12K+10)`.
+
+This bound is constructive and covers validation, comparisons, both
+choices of bucket, marker writes, all explicit branches/jumps, merge,
+erasure and return. It is deliberately conservative because increasing
+PC segments often skip instructions. No measured runtime is used to
+prove it. The verifier checks the independent source execution at every
+compiled instruction boundary in three fixtures and corroborates the
+exact B formula there.
+
+Use #4982's unchanged `compile_program(..., lifecycle=True)` and bit
+machine. Its fourteen-bit tagged registers distinguish symbols from
+Booleans. Each core source instruction expands to at most 43 actions:
+single-bit read/write, unit physical head move, one-bit assignment/copy,
+Boolean operation, branch, jump or halt. The exact local simulation is
+retained in its pinned PROOF.md: writes set every one of thirteen bits;
+read/write returns to the aligned cell start; a source move is thirteen
+unit physical moves; full tagged equality handles destination aliasing.
+Our source uses only read/write/move/copy/eq/branch/jump/halt and its
+private names avoid `$different` and `$xor`. Every reachable branch
+operand is the Boolean result of equality. Hence its induction applies
+for every input here, including arbitrary initially dirty finite control.
+
+Initialization and the reached halt suffix each assign all 72 one-bit
+control registers. These 144 actions are paid, not emulator allocation.
+Consequently one complete pass costs at most
+
+`43*180*(8n+12K+10)+144 = 7740*(8n+12K+10)+144`
+
+literal actions. For fixed width L this is
+`7740*(n*(12L+8)+10)+144`. L repeated passes cost at most L times that
+quantity. This is a sequential finite-tape bit program bill, not merely a
+symbol-cell meter. Static code construction and initial serialization
+are outside the invocation contract. They have not become free globally.
+
+## Actual caller and remaining ledger
+
+The actual fixture retains #4982's original `bridge.split`, actual raw
+middle-layer payloads/mask, two complete bit-level key executions and
+continuation to the third marked address. The predecessor fixture closes
+the captured completed prefix with END as explicit verifier setup. Our
+adapter replaces its subsequent `bridge.one_pass` call, receiving the
+**same** `bad.raw`, `b0.raw`, `b1.raw` objects. It neither decodes a key
+into a program parameter nor materializes a replacement tape. The
+original caller's postchecks inspect payloads, rotated keys and heads;
+we also check bucket and control erasure. The enclosing split's symbol
+facades remain an unlowered outer boundary. This demonstrates one actual
+local connection, not complete repair or production geometry admission.
+
+| Obligation | Status |
+|---|---|
+| Stable consumer action and cleanup for all valid finite encoded streams | proved here; explicit finite upper bound |
+| Inherited thirteen-bit compiler's block simulation | retained pinned premise; observer corroboration here |
+| Original two key calls and continuation before new consumer | executed bounded fixture, predecessor source proof retained |
+| Full 2944-hole layer and complete sort/reinsert | unrun; not discharged by the captured prefix |
+| Split/reinsert binary control, uniform geometry and descriptor/ROM construction | unknown here |
+| Physical tape placement, whole CRT tariff E(p,ell), compiler creation cost and all-size supplier transfer | unknown here |
+
+No new kappa, selected supplier, complete multiplication theorem, native
+implementation or formal proof-kernel acceptance follows. The declared
+family decision is narrow: close this explicit consumer boundary and
+stop, rather than authorize an automatic full-repair expansion.

research/crt-binary-radix-consumer/README.md

@@ -0,0 +1,128 @@
+# A literal binary radix consumer for the CRT repair stream
+
+This closes **Open next question 1 of [PR4982](https://github.com/CrocSwap/integer-mult-bounds/pull/4982)**:
+execute the next actual sparse-repair consumer in bit control. The fixed
+[program](radix.py) uses the unchanged predecessor compiler/bit machine to
+lower the retained `bridge.one_pass` stable-radix algorithm. The entry
+representation, payload semantics and actual caller are preserved.
+
+The [written proof](PROOF.md) covers **every finite stream** with n opaque
+12-bit payloads and nonempty binary keys of total length K. One pass has
+complete literal bit-action bound
+
+```
+7740 * (8*n + 12*K + 10) + 144.
+```
+
+It includes framing validation, all bit reads/writes and unit head moves,
+finite Boolean/control steps, stable bucket partition/merge, bucket erasure,
+head return, and initialization/erasure of all 72 finite-control bits.
+For equal key width L, L repeated passes stably sort the full keys and
+restore their orientation. This is an explicit finite-tape program and a
+uniform source-control proof, not an extrapolation of a symbolic cell meter.
+
+The program is static: 180 source instructions, 3885 binary instructions,
+three tape roles, and no input n, L, key integer or decoded stream in the
+assembler/executor. It recognizes opaque records using the declared source
+alphabet, without inspecting their payload value. Entry requires aligned
+13-bit predecessor codewords and clean owned buckets. Unused codewords,
+dirty buckets, missing/duplicate outer markers and misaligned entry heads are outside this
+port contract. Record/key grammar errors inside a uniquely LEFT/END-framed
+stream reject
+before output, preserving the borrowed input and clearing finite control.
+
+## Evidence
+
+[RESULT.json](RESULT.json) records these independent endpoint/representation
+checks, executed in both ordinary and optimized Python:
+
+- All 371 streams with up to four one-bit-key records, or two keys of width
+  one through four; both empty buckets, all-zero/all-one partitions and
+  duplicate keys are covered. Distinct payloads detect loss of stability.
+- Three complete source-instruction-boundary simulations against the
+  predecessor's independently represented source semantics. Every physical
+  head scale, register result and written codeword matches. The exact
+  backward-transfer counts corroborate the all-size control proof.
+- Complete stable sorting through three and 37 passes, width-one keys,
+  payload boundary values 0/4095 and variable positive key lengths for a
+  single pass. Every legal endpoint also matches the original literal
+  `bridge.one_pass` and an independent stable sort/rotation oracle.
+- Five faults reject: reverse bucket order, wrong key rotation, retained
+  bucket data, short physical cell strides and omitted control erasure.
+  Eight malformed uniquely framed packets reject with borrowed data and bucket
+  preservation, returned heads and cleared control.
+- **Actual source caller connection:** original `bridge.split` emits two
+  completed pairs through the real bit-level key service, then continues
+  to the third marked address. Its completed prefix is explicitly closed
+  by verifier setup. The new radix consumer receives those **same physical
+  tape objects**, uses 37,969 actions, and returns the expected payloads,
+  key rotations, heads, blank buckets and cleared control. The outer
+  caller's facades remain an unlowered boundary. No whole layer is implied.
+
+Finite tests corroborate the quantified written proof; they are not formal
+kernel verification. The static 43-action compiler-block simulation is a
+pinned predecessor premise. This package adds source-control proof and
+consumer/caller checks instead of rerunning its complete alphabet census.
+
+## Reproduce
+
+From the repository root, Python 3.12, standard library only:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/crt-binary-radix-consumer --check-only
+python3.12 -B scripts/research_package.py --package research/crt-binary-radix-consumer
+```
+
+The registered hook runs ordinary and optimized checks, authenticates all
+thirteen live inputs and compares every proof-relevant receipt field.
+Direct `verify.py` replay also works in the package's standard Git-free
+export; `--write-result` alone regenerates its receipt.
+
+## Family decision, sources and overlap
+
+**Narrow, then stop:** this is one named actual-consumer obligation. Full
+binary split/reinsert, physical descriptor and ROM production, variable CRT
+geometry, compiler creation/serialization and whole CRT E(p,ell) remain
+unknown. The inherited fixed key fixture does not become a uniform key
+compiler. No complete 2944-hole layer, historical suite, Lean/Docker or
+selected supplier replay is run. No new kappa or selected-frontier change
+is claimed.
+
+[SOURCES.json](SOURCES.json) pins canonical base
+`bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority revision 7, and all
+imported source bytes. The key/binary predecessor is PR4982 at
+`67154122b2867e6dee5b9b25f2f1c862a3e81e95`; its PROOF.md supplies the
+compiler simulation. The original bridge and key/source lineage remain
+unchanged. Pending PR4990 supplies a two-target unary stencil, a different
+producer boundary. Symbol-level repair and abstract radix predecessors
+already supply stable sorting; that algorithm is not claimed as new.
+
+Initial overlap covered all 6690 current tracked notes, 310 open/draft PR
+bodies at 2026-10-23 06:05:59 UTC and 4096 Discussion records at 06:06:48
+UTC, with complete inventory/pagination. The targeted `one_pass`/`binary`
+search found only PR4982's README/TASK and its canonical result. Arbitrary
+diffs and unpublished work remain outside coverage; no novelty guarantee
+is claimed. Canonical coordination is [Discussion4709](https://github.com/CrocSwap/integer-mult-bounds/discussions/4709#discussioncomment-19139345); [TASK.json](TASK.json)
+retains the scoped card, stopping rule and next questions.
+
+## Open next questions
+
+1. Specify one complete actual encoded split/sort/reinsert caller, with its
+   transport and restoration obligations, before expanding implementation.
+   This decides whether local stages can share one complete paid invoice.
+2. Specify the encoded variable-geometry key/ROM producer and its lifecycle
+   allowance. A different finite key seed would not resolve the current
+   uniform producer/serialization gap.
+
+The structured questions and blockers are in TASK.json. Neither is claimed
+or implicitly assigned by this package.
+
+## Credit
+
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+Retain PR4982/PR4795/PR4752 authorship and the original PR4637 scanner/repair
+lineage: Cinna Davis, ToikY, Hiroki KUMAZAKI, Ryanson Jonathan, unpaidmoon,
+Jose Manuel, Douglas Colkitt and John-Michael Smith (PR763 lineage). The
+[source-specific notice](../unconditional-batched-crt/NOTICE.md) remains in
+its declared source inputs. All frozen predecessors are unchanged. No
+independent human or formal proof-kernel acceptance is claimed.