Implement a literal runtime affine shear and source-bound half leaf

research/fixed-tape-affine-shear/PROOF.md

@@ -0,0 +1,199 @@
+# Literal runtime affine shear and its source half-coefficient leaf
+
+This is an algorithmic proof for the supplied finite programs. It is not a
+proof-kernel result, a native operator proof or a complete supplier admission.
+The split/merge idea and the local machine/counter/copy macros are David Arias's
+PR2776. Charles Bethin's unit-carry kernel is the closest fixed-carry successor.
+The new feature is an arbitrary **runtime** coefficient and offset, with their
+complete conversion, wrap, reset and cleanup costs.
+
+## Contract and fixed machine
+
+For every positive integer `P,Q,G,S` and `0<=c,C<Q`, let `V=P Q^2 G S`.
+Canonical positive LSB-first binary words encode `P,Q,G,S,c+1,C+1` on six
+separate preserved input tapes. The source tape contains every Boolean payload
+bit in lexicographic order on `[P] x [Q] x [G] x [Q] x [S]`, between distinct
+LEFT/RIGHT markers. Input heads begin on the first symbol. Output and eleven
+private tapes are completely blank and have independently supplied origins.
+No input/output/private roles alias. Arbitrary bit values, gap/suffix extents
+and different translated tape origins are allowed.
+
+The two 877-instruction programs have nineteen tapes and seven symbols. Their
+only operations are one scanned-symbol branch, one-cell write, one unit move,
+fixed jump, halt and reject. Assembly consumes **no** runtime extent, coefficient,
+payload or Python callback. Each executed microinstruction costs one transition.
+All sources and descriptors return byte-for-byte with their original heads.
+Output is a separately owned marked stream with its head on its first bit.
+Every private symbol, marker and head returns to its original blank state.
+Their permutation is
+
+```
+(p,x,g,y,z) -> (p,x,g, y +/- (c*x+C) mod Q, z).
+```
+
+The total cost, including descriptor conversion, all carries, rewinds and
+cleanup, is at most `1024V` transitions and `64V` visited tape cells. The space
+bill includes visited cells subsequently cleared; it is not a final live-space
+count. Invalid inputs need not be cleaned up on rejection. This is a valid-input
+contract; inspecting one initial cell does not certify an otherwise unbounded
+scratch tape is empty.
+
+## Split invariant and termination
+
+PR2776's retained binary-to-unary macro preserves its canonical input and
+returns its work tape blank. Convert seven values: `P,Q,G,S,Q,c+1,C+1`.
+The second Q copy is a genuine independent x-traversal counter. Remove one
+unary mark from each last counter, and compare each with the Q counter to
+reject `c>=Q` or `C>=Q`. These comparisons are literal finite loops.
+
+At a boundary the two split tapes have lengths `(L,R)=(Q-r,r)` with `0<=r<Q`,
+both heads on their right markers. Transferring one mark changes `(L,R)` to
+`(L-1,R+1)`. When `L=0`, transfer all Q right marks back, erasing old right-marker
+tails, so the representation becomes `(Q,0)`. Thus one completed transfer is
+exactly `r -> r+1 mod Q`. The transient `(0,Q)` is reset before any payload.
+Initialization advances by C. At the start of the x-th group, therefore,
+
+```
+r = C + c*x mod Q,  (L,R) = (Q-r,r).
+```
+
+For every gap g, gather the first L source records into A and the remaining R
+into B; a record has S opaque bits. Advance the split by exactly c mark transfers
+and advance the **separate** Q counter once. This works for zero and nonunit c:
+traversal does not depend on the order or period of the offsets. After Q groups,
+`C+cQ = C mod Q`, so no prefix reset or reconstructed coefficient is needed.
+The same invariant applies to each next prefix and to the emission pass.
+
+Forward emission consumes B's next R records, then A's next L. This moves each
+source y to y+r modulo Q. Inverse compilation reverses the two gather segments
+and the two emission segments: it gathers R then L and emits L then R, giving
+`y-r`. Both are permutations for **every** c; c need not be a unit because x is
+preserved. Every copied bucket cell is consumed exactly once. Rewinds preserve
+source and descriptors. The retained eraser clears each private region back
+through its temporary LEFT origin marker and returns that head to its origin.
+
+All loops use finite positive unary counters or finite segments. Each x iteration
+finishes c transfers; each wrap finishes Q transfers; P,Q,G,S are finite. This
+proves termination and all endpoints for every permitted shape and payload.
+Finite coefficient grids corroborate this argument; they do not replace it.
+
+## Complete uniform transition ledger
+
+The retained positive conversion takes
+`24n - 7 popcount(n) + 15 bit_length(n) + 12 <= 44n` transitions.
+A rewind from a right marker after h symbols costs `3h+3`; scanning/deleting one
+unary suffix marker uses the actual local instructions in the retained source.
+The following conservative blocks are upper bounds obtained by summing those
+instructions. Every extent monomial displayed is at most V.
+
+| Executed block | Transition bound |
+|---|---:|
+| Initialize output and eleven private marked tapes | `36 <= 36V` |
+| Seven conversions | `44(P+G+S+2Q+c+C+2) <= 308V` |
+| Decode c+1,C+1 by one-mark removal | `6c+6C+22 <= 22Q <= 22V` |
+| Two strict coefficient/Q comparisons, including rewinds | `11c+11C+22 <= 22Q <= 22V` |
+| Initialize the split and advance C (no wrap) | `14C+3Q+6 <= 17Q <= 17V` |
+| Two payload/traversal phases, excluding coefficient advancement | `23V+20PQ^2G+28PQG+20PQ+20P+8 <= 119V` |
+| All coefficient advancements and cyclic resets in both phases | `2P[Q(17c+4)+c(10Q+3)] <= 54PQ^2 <= 54V` |
+| Finish gather and rewind both buckets | `3V+9 <= 12V` |
+| Finish output, source/output rewinds and all eleven complete erasures | `<=111V` |
+| Final halt | `1 <= V` |
+
+Their sum is at most `802V`, below the stated `1024V` allowance.
+
+For the phase row, one record copy costs at most `(11+consume)S+4`, and a segment
+of length l costs at most `(11+consume)Sl+10l+4`, including its length rewind.
+The two segment lengths sum to Q regardless of gcd(c,Q). Summing the actual
+P/x/G loop branches and unit moves gives the displayed two-phase polynomial.
+No uniform distribution of offsets is used in this bound.
+
+For the advancement row, a coefficient rewind costs at most `3c+3`; c ordinary
+transfers plus loop tests cost at most `14c+1`. Each cyclic reset adds at most
+`10Q+3`. Across all Q x-groups at one prefix there are exactly c resets, since
+the total advance is cQ starting at C<Q. Therefore that entire prefix costs at
+most `Q(17c+4)+c(10Q+3)`. In particular, even `c=(Q+1)/2` incurs `O(Q^2)`,
+which is absorbed by the actual complete-pair payload volume Q^2GS. Repeating
+whole unit-shear invocations would instead cost O(cV); this program does not.
+
+The last cleanup row includes both consumed bucket regions (total at most V
+cells), P/G/S counters, both split lengths, binary work, c/C counters and the
+x counter. At their current right heads, the retained eraser costs `4h+2`.
+This gives at most `98V` for private erasure, `6V+7` for output/source returns,
+and the extra output end-marker write; the stated 111V is conservative.
+
+## Space, including cleared work
+
+Let M be the maximum bit length of the seven converted integers and let B be
+the sum of the six input descriptor bit lengths. The union of visited intervals
+has size at most
+
+```
+3V + P+G+S + 3Q + c+C + B+M + 40
+ <= 3V + P+G+S + 5Q + B+M + 38 <= 56V < 64V.
+```
+
+Source, output and the two buckets contribute `3V+8`. The remaining terms pay
+all unary counters, both potentially Q-long split intervals, the maximum binary
+work interval, all six input intervals and every marker. The bucket lengths
+may be very unequal (for example c=C=0); only their sum V is used. Each
+positive descriptor has bit length at most its value, and each such value is at
+most V. Tape translations change no interval length. No cell outside these
+intervals is accessed.
+
+## Literal half descriptor and actual source leaf
+
+PR4989's retained actual frame506 schedule includes
+`ordered_shift(addresses=[3,0], coefficient=[1,2])`. Its interpreter defines
+address0 as source and address3 as target. For every source odd prime q and
+`e=w-1>=1`, the complete high fields have common extent `Q=q^e`, and
+
+```
+2 * ((Q+1)/2) = Q+1 = 1 mod Q.
+```
+
+Thus the runtime multiplier is c=(Q+1)/2. The negative half leaf is the inverse
+program. This grows with e; treating the rational factor as a fixed number of
+unit shears would be an invalid uniform-time argument.
+
+The complete linked half program includes a **literal** preparer on the same
+nineteen-tape bank. It checks that Q's low bit is one and at least one further
+bit exists, copies the remaining bits into an owned blank coefficient tape,
+then performs a ripple increment beginning at its second bit. The copied
+integer is floor(Q/2); the result is `floor(Q/2)+2=(Q+3)/2=c+1`. The final
+high-bit check enforces canonical encoding. It returns Q and both input heads.
+After the generic kernel, a literal scan erases every coefficient bit and its
+markers, returning its tape to its original blank origin. These tables are
+retained in TABLE.json.gz together with the generic programs; linking adjusts
+only finite state destinations, not runtime addresses.
+
+Preparation costs at most `40 bit_length(Q)+80 <= 67Q` for Q>=3. Complete owned
+descriptor erasure costs at most `8 bit_length(Q)+8 <= 11Q`. Their tape cells
+already lie within the generic space ledger. The linked half call therefore
+costs less than `880V`, still within `1024V` and `64V`, including preparation and
+cleanup. General c,C are supplied descriptors; preparing arbitrary rational
+coefficients from a caller is not made free by this half-specific construction.
+The offset descriptor is C+1=1 for this actual source leaf and is preserved.
+
+For an actual complete source packet, group every coordinate before source0 as
+P, those between source0 and target3 as G, and those after target3 as S. Their
+extents may be enormous; the proof quantifies over them. No sorting, random
+access, hidden high-coordinate lookup or ordinary interchange is used. This
+binds the later-target half leaf on the complete-high-fiber interface. The
+finite executed fixtures compress these spectator dimensions and do not
+materialize the full source high matrix or prove the whole native invocation.
+Other later-target +/-1 and +/-1/2 slots have the same interface; no claim about
+reversed-field slots or unit_scale is implied.
+
+## Remaining obligations and decision
+
+This closes one physically priced ordered-affine primitive with a source-bound
+half descriptor. It does not construct PR4989's complete low-type cache, native
+canonical call, raw-body call, completed ordinary swap, ROW padding or the full
+compiled matcher. Installation in the whole recursive owner bank, matched
+physical tape allocation, reserve/precision/threshold constants and the P3
+recurrence remain open. Output/source separation is explicit; replacing the
+source owner by the output or erasing that original source needs the caller's
+paid ownership protocol. No selected frontier or multiplication exponent is
+changed. Continue only after one of those separate contracts is selected and
+its complete allowance is stated; another small coefficient fixture is not a
+new contribution.

research/fixed-tape-affine-shear/README.md

@@ -0,0 +1,134 @@
+# Runtime affine shear on nineteen literal tapes
+
+One fixed finite program realizes
+
+```
+(p,x,g,y,z) -> (p,x,g,y+c*x+C mod Q,z)
+```
+
+and its inverse for **all** positive binary-encoded `P,Q,G,S`, `0<=c,C<Q`,
+and every Boolean payload of volume `V=P Q^2 G S`. Each generic direction has
+**877 local microinstructions, nineteen tapes and seven symbols**. The complete
+bounds are **1024V transitions and 64V visited cells**, including conversion,
+coefficient loops, cyclic reset, payload copying, every rewind, scratch erasure
+and head return. Source and descriptors are preserved; output is separately
+owned. Nonunit and zero coefficients are allowed. These are conservative
+physical bills, not measured speedups or optimized constants.
+
+The actual [PR4989](https://github.com/CrocSwap/integer-mult-bounds/pull/4989)
+frame506 route includes the ordered shift from high coordinate0 to coordinate3
+with rational coefficient1/2. Its multiplier modulo `Q=q^(w-1)` is `(Q+1)/2`,
+which grows with width. Repeating that many whole unit-shear invocations would
+lose a growing factor. The new program advances unary split positions locally;
+all Q iterations together pay only O(Q^2), absorbed by the full pair volume.
+
+The retained **linked half program** additionally computes its actual binary
+coefficient descriptor from Q by a literal copy/ripple increment and erases
+that owned descriptor after use. Preparation is not a free host scalar inverse.
+Its total remains inside the same `1024V/64V` bill. General runtime c,C are
+supplied descriptors; preparing other rational coefficients remains a caller
+cost. No ordinary-interchange oracle, arithmetic callback, nonlocal tape access
+or extent-specific program is used.
+
+## Proof and source boundary
+
+[PROOF.md](PROOF.md) gives the all-size invariant, termination, complete
+transition ledger and visited-space proof. The advancing offset may have any
+period: a separate Q counter prevents early termination when c is a nonunit.
+A prefix makes exactly c complete cyclic resets across Q x-values. All buckets,
+markers and counters are physically cleared, including cells previously erased.
+
+This extends David Arias's [PR2776](https://github.com/CrocSwap/integer-mult-bounds/pull/2776)
+fixed unit shear and Charles Bethin's fixed unit-carry kernel. Their split/merge
+method, local instruction vocabulary and paid counters retain full credit.
+The actual matcher generator, serialized program and interpreter are pinned:
+source high-coordinate address0 precedes address3, and both fields range over
+the complete Q-element high fiber. Arbitrary intervening fields are the G
+spectator extent. The all-size proof covers that interface; finite executions
+compress the huge source spectators and do **not** materialize the full native
+high matrix or admit the whole matcher route.
+
+Unimplemented native/raw-body/ordinary callees, unit_scale, reversed-field
+routing, low-type cache/ROW padding and whole-bank ownership remain explicit.
+Installing this source-preserving, owned-output kernel in the original
+in-place caller still needs a paid source-retirement protocol. Complete P3
+stock, tape, precision, recurrence and threshold obligations remain open.
+No selected frontier or kappa is changed.
+
+## Evidence and reproduction
+
+The separate dense table interpreter imports no assembler or predecessor
+execution code; its direct **gather** coordinate oracle knows no split traversal.
+A second sparse interpreter executes the same saved tables and matches every
+step/span/transcript observation. The main bounded checks cover:
+
+- 610 directional executions and 38,850 payload bits: every c,C for Q<=8,
+  all one-hot columns at Q=3, nonunit Q=6,c=2, translated origins and nontrivial
+  prefix/gap/suffix layouts.
+- Ten complete linked half calls, plus 107 exact descriptor cases including
+  long binary carry chains through 40-bit Q. Zero, even and too-small half
+  moduli reject. These descriptor checks do not execute their large payloads.
+- Malformed extents, out-of-range/noncanonical coefficients, occupied scratch,
+  nonlocal motion, wrong orientation, lost coefficient/offset, corrupt output,
+  retained scratch, changed source and an endpoint-preserving extra-work mutant.
+
+The new lost-coefficient control initially used x=0 and could not distinguish
+that mutation; it now uses x=2. The payload mutant initially changed only an
+unreached bucket write; it now corrupts both output branches. These verifier
+corrections are retained in the substantive commit history. They are not
+claimed as defects in the mathematical source program.
+
+From the repository root, standard-library Python3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/fixed-tape-affine-shear
+```
+
+Four bounded registered commands run sparse/dense engines normally and under
+`-O`; explicit guards remain active. `verify.py` is read-only. Explicit
+`--write` regenerates the canonical receipt and gzip table; verification compares
+the decoded complete instruction tables, not gzip container bytes. The literal
+generic, linked half and descriptor tables are all in `TABLE.json.gz`.
+`SOURCES.json` binds live inputs by SHA256 and Git blob; catalogue and selected
+record are historical provenance. These source checks are not scientific
+acceptance. No Lean, Docker or unrelated historical suite is run.
+
+Validation on CPython 3.12.2 / macOS 27.0 arm64: all four registered modes
+pass. Committed-byte and source-history checks pass for 21 files; official
+export integrity and all four direct modes pass again with Git absent from
+PATH. Actual exported source, table and typed-receipt changes reject, including
+`schema_version: 1 -> true`; every original exported byte is restored. A
+separate read-only AI peer independently recounted the transfer/comparison,
+phase, cleanup, space and half-preparation ledgers and found no blocker.
+This is not independent human or scientific acceptance.
+
+## Open next questions
+
+1. Bind one complete actual route's source/output banks and source retirement,
+   including shared scratch lifetimes. This is needed to install the kernel;
+   full physical ownership and native/ROW protocols remain the blocker.
+2. Physically lower one actual unit_scale or reversed-field primitive, with its
+   full all-width tape bill. The current program does not cover those positive
+   costs. Begin with the source coefficient and explicit owner/tape contract,
+   rather than extending this same coefficient grid.
+
+[TASK.json](TASK.json) records the refined card and structured questions.
+Canonical [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4945#discussioncomment-19139354).
+Base: canonical main `bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority7.
+Entry overlap covered310open PRs (06:05:59UTC),4096Discussion records
+(06:06:48UTC) and all6690tracked local notes on October23,2026. These cached
+metadata searches do not cover arbitrary diffs or unpublished work and are not
+a novelty certificate.
+
+## Credit
+
+David Arias / PR2776 supplied the finite machine, counters and copy/erase macros;
+Charles Bethin supplied the unit-carry successor and explicit open carry
+question. Jose Manuel and the retained upstream authors supplied the selected
+stream reduction and ordered-affine method. ai-nanachi #4760/#4814/#4326,
+Chris R / Clear1nsight #4957, JoyboyBrian #4989 and the retained native,
+ROW/ordinary/stock/routing/precision/tape lineage supply the source boundary.
+All predecessor files remain unchanged. New runtime controller, literal half
+preparation, linked owned cleanup, proof and checks prepared by JoyboyBrian
+with substantial OpenAI Codex assistance. Apache-2.0. No independent human or
+proof-kernel acceptance is claimed.