transfer-review.txt

FOCUSED ADVERSARIAL REVIEW OF THE FINITE-TO-TAPE TRANSFER
8 October 2026. This is a limited independent paper review, not a full machine
formalization or a complete re-review of every inherited analytic argument.

SOURCE PINS

All paths/line numbers below are relative to the repository checkout pinned at
CrocSwap/integer-mult-bounds 64ed4cbf872b86b81c22f104967b88d24b8e4548.
Its upstream/manifest.json pins the retained OpenAI text to
adc7f1241b42e322a6451854ab7e4b4c146bf78a. This is distinct from the newer
openai/math snapshot discussed in the accompanying addendum; these citations concern
the actual text inherited by this community baseline.
The new graph is PR62 ad0f25ff7b23cff7f08ad237c2254e6ecf74257e, with the
PR60 retired-slot priority e7a492dd8bee4e6f574ced784a62af2ce735edc4.

NARROW CONCLUSION

The inherited repository contains substantial written all-size arguments for
integer-width remainders, exact row divisibility, fixed-tape stack scheduling,
descriptor amortization, and choosing one eligible address prime. These are
not merely finite tests and should not be described as absent just because
they have not been formalized in Lean. No counterexample to those arguments
was found in this focused review.

The new ranked mixer is finite and input-size independent. Its extra XORs can
change the fixed linear-overhead constant C, without changing the power of the
width, provided the full framed-lift interface below is met. The four scalar
mixer sweeps do NOT require four copies of the variable-frame rank profile:
an explicit inherited early/middle/late frame assignment explains why only one
middle path is profiled. Scalar dirty-basis replay alone does not prove that
assignment or the all-size recurrence; they require the separate frame proof.

The most consequential remaining verification obligation is to connect the
concrete joint-compiler word, its terminal frames and copied-center dispatch
to the full ambient two-stage circuit and the generic all-size compiler in one
checked refinement. This is an application/proof-correspondence obligation;
it is not a demonstrated flaw in the mathematical framework, nor a claim that
no relevant paper proof exists. Analytic multiplication/recovery obligations
also remain outside this review.

1. SUFFICIENT HYPOTHESES FOR THE NORMALIZED RECURRENCE

Freeze m,W>=2, a finite scalar word, rational frame tables and factor tables,
and positive integer child multiplicities n_t with 1<=t<m. Let t*=max{t:n_t>0}.
Use complete lexicographic arrays with two equal q-radix chunks of width e,
an explicit row field preceding both, arbitrary complete intervening/prefix/
suffix spectators, and canonical binary length descriptors. Logical volume V
includes EVERY spectator record and all rows, rather than just selected axes.

The following hypotheses suffice:

(H1) A full finite framed circuit realizes the all-role interchange, including
arbitrary dirty auxiliaries, all source/sink gauges, both orientations, terminal
scatter, paid center copies, and endpoint correction. Every scalar gate has a
common address frame on its incident roles. Its residuals have certified
contiguous pivot blocks, producing exactly n_t recursive calls of width t f.
No arbitrary gathering of separated pivots is admitted.

(H2) For e=mf+r,0<=r<m, the two r-digit high parts are handled by a bounded
number of elementary moves; the remaining m equal fields each have width
f=floor(e/m). Each child runs on a complete role stream of volume exactly V/W.
Unused main digits, remainders, controls and all spectators remain present.
Rows have count divisible by W^D(e), where D(e)=0 below m and
D(e)=1+D(t*floor(e/m)) otherwise. Only whole rows are split; children receive
row count R/W and need no internal padding.

(H3) One fixed finite-alphabet machine implements every nonrecursive gate,
ordered-affine map, role split/merge, temporary copy and stack operation at a
node in at most C V steps, with C independent of e, field lengths, payloads,
recursion depth and original volume. Local descriptors have a fixed number
of collapsed intervals. All relevant rational coefficients are fixed before
the machine/input size is selected, and their chosen reductions are valid for
every modulus q^f.

(H4) Below e<m the normalized cost is uniformly bounded, including shape
preparation and cleanup. Completed calls preserve the row/spectator coordinates
and return work tapes to their boundary invariant, so sequential children and
outer zero-row removal are valid.

Then a uniform normalized upper-bound function F can be chosen with
  F(e) <= C + sum_t (n_t/W) F(t floor(e/m)), e>=m.
The physical children are FLOOR multiples, not ceilings. Choose a monotone
majorant f(n) of normalized costs for all admissible widths e<=n (or define
the displayed budget recursively with base constant and C large enough that
it is monotone). This gives the sufficient relaxed inequality
  f(n) <= C + sum_t (n_t/W) f(ceil(t n/m)).
Thus a Lean theorem for the latter recurrence applies only after introducing
this envelope and proving the physical interface; it is not a literal
description of the emitted child widths.

The stronger floor recurrence and its strong-induction proof are already
written in notes/batched-bit-rows.tex:9-30. Depth/divisibility is at32-46,
remainder layout at48-70, one outer row padding at72-106, and descriptors at
108-123. Constructive pseudocode appears in notes/batched-algorithms.tex:
115-132,174-226,228-265. The original power-width theorem and full field
contract are upstream/build/sections/04-swap.tex:129-143,145-211.

2. WHY THE FOUR MIXER SWEEPS DO NOT MULTIPLY FRAME COST BY FOUR

Write the chronological scalar wrapper as
  L ; J ; L^-1 ; V ; L ; J ; L^-1 ; V.
Here J only reads auxiliary output roles and XORs into the separate data-target
bank; V only reads the separate data-source bank and XORs into source roles.
Its scalar identity JLV=I and arbitrary-scratch cancellation are one part of
the argument. The address frame assignment is an additional part.

Within one tensor invocation suppress the fixed future line and set
  D0=B tensor F_h, D1=A tensor F_h,
  A=B orthogonal-direct-sum P,
  D_U=D0 orthogonal-direct-sum (P tensor U),
where P and the suppressed future factor are lines. The notation D_U here
denotes a subspace label; its actual address permutation is the partial swap
F_U. A local residual U->U' has ambient rank dim(U')-dim(U).

The forward phase assignment is:
* First L, early J, first L^-1: all auxiliary gates at the constant background
  D0. Their internal frame changes are zero, though their literal scalar XORs
  still cost a fixed number of full-stream passes.
* V: designated source copies at their source-line frames, with source data
  grown to the compatible common frame. This is the entrance to the recorded
  varying local path.
* Middle L: every emitted XOR uses its recorded common D_U frame, following
  the monotone per-role path. This is the SINGLE nonconstant mixer sweep.
* Second J: side outputs grow to their target-complement frame. Retained center
  outputs use a complete copied stream transformed back to D0 for reads; the
  original then grows directly to D1. These extra copy transformations and
  original cleanups are explicitly charged.
* Final L^-1 and V: cleanup at the constant D1. Every original role has already
  grown to D1 before its first cleanup incidence; no reverse traversal of the
  recorded U path is required in this forward invocation.

The explicit inherited assignments are notes/dag-construction.tex:94-139,
especially102-108 and133-139, and notes/incidence-construction.tex:94-123.
notes/paired-construction.tex:104-113 specifies the complementary reverse
orientation. Reverse the varying middle chronology and replace U by U^perp;
U⊆U' becomes (U')^perp⊆U^perp. Its residual projector is exactly
P_(U')-P_U again, since P_(U^perp)=I-P_U. Consequently it has the same
ordered rational profile, not a second independently charged forward path
inside the same invocation.

The center-copy contract and actual forward/reverse schedules are
notes/copied-centers-lemma.tex:15-35,37-76. The forward original center path
U->0->F is replaced by a paid copy U->0 plus original U->F; its cost is
r+(h-r), replacing r+h. The reverse schedule is the complementary reverse
of this. Lines79-103 derive hR+h(h-1) and retain all exterior/data corrections.

This assignment applies to any finite XOR word with monotone, common-frame
incidences and the same source/output interfaces. It does not require the
middle operation to be a cancellation-free two-input addition: row synthesis,
three-XOR swaps and paid retired-slot clearing have the same pointwise
commutation property. Arbitrary dirty values need not lie in the rational
address envelope; the envelope describes an address permutation, not a
restriction on payload bits. The ranked compiler's new XORs are therefore
eligible at this local level when the recorded inclusions hold.

One dispatch detail should be explicit in any final refinement: retained-center
reads must occur while their data targets still have D0, before side-output
target growth. Every J gate reads the auxiliary bank and writes the distinct
target bank; these XOR gates commute with one another, even if they share a
target. Therefore one may group center reads first and then side reads by
target without changing the scalar map or dropping any incidence. This does
not license arbitrary reordering of the middle L word. The serialized J is a
scalar order; a framed implementation may use this proved commuting dispatch.

The new checker verifies the literal J/output binding, common-frame monotone
middle incidences, unique designated output roles and required terminal labels.
It does not serialize every D0/D1 gate and tensor embedding in the full ambient
network. A mechanically checked full framed-lift theorem remains worthwhile.
The concern "four occurrences of L imply four profile charges" is resolved
by the written phase assignment above, not by the finite scalar replay alone.

3. ROW DIVISIBILITY, ROUNDING AND COMPLETE SPECTATORS

A direct failure if divisibility is removed: with W=2 and row count R=3,
cyclic splitting yields streams with2 and1 complete rows. They do not have
the same address domain, and neither has the claimed common volume V/2.
Pointwise gates on aligned role streams and the 1/W recurrence are then
unjustified. The inherited construction avoids this by taking D(e) as above,
reserving W^D(e), and padding only a complete outer row field.

It obtains row capacity from already-present high digits, not by appending
W^D(e) new copies. The joint high-digit range is q^(2rho)>=W^D(e); rounding
to its next divisible row count increases volume by less than2 once. Descendant
row splits preserve divisibility. Every added row includes the whole within-row
address set and is removed only after a completed all-role map. See
notes/batched-bit-rows.tex:72-106 and upstream04:303-388.

Padding the two chunk ranges or the row field by a factor near2 at EACH level
would introduce a factor exponential in recursion depth; the claimed C and
characteristic would not survive unchanged. That is an invalid variant, not
the written floor/remainder construction. Merely saying "ceil widths only
add a constant" would not establish the physical padding bound.

Complete spectators are essential to both volume and descriptors. If unused
root digits were removed from a child, one could have a constant-volume child
while still manipulating a descriptor of unbounded root length; no uniform
O(V_child) cost would follow. The actual proof retains all root chunk ranges
as spectators: V_j>=q^(2e_root) in the original power-width call, or at least
q^(2(e-rho)) in the mixed-width outer construction. Since depth is O(log e),
log V_root=O(log(2V_j)), allowing polynomial descriptor work to be absorbed
uniformly. References: upstream04:244-268; notes/batched-bit-rows.tex:108-123.

Mixed bit/complex stock requires a PRODUCT of divisors, because a complex
ancestor retains its split while a bit child runs. Replacing that product by
its maximum is explicitly rejected in references/copied-fixed/pr34/
ASSEMBLY_PROOF.md:92-109. For the selected later network,
notes/copied-centers-assembly.tex:36-53 proves stock p^2000 from halving
degrees9,20 and wire bitlengths28,30. The ranked-pair graph has the same maximum
bit child529 and bitlength28, so this stated stock bound remains sufficient;
its new W must nevertheless be bound to the actual certificate, as it is in
the package assembly verifier.

4. FIXED TAPES, PARKING AND DESCRIPTORS

upstream04:213-268 describes a fixed number of role/I/O/work tapes, parking and
descriptor stacks. Before each child, inactive streams are pushed at the active
stack top; the child's active stream is copied, parent role tapes are erased,
and the same tapes are reused. On return, inactive streams are popped into
known-length destinations in reverse writing direction. No scan crosses a
parked ancestor, and cleanup never sweeps a tape to an ancestor's historical
maximum extent. Every push/pop/copy/erase costs O(V_parent); the finite number
of children makes the node overhead O(V_parent).

The constant is not1 and can be enormous. In particular, four mixer sweeps,
all clearing XORs, and the fixed number of recursive children contribute to C.
Their number is fixed after selecting the graph; an input-dependent network
search or a mixer family growing with n would require a different analysis.
The new selected mixer has fixed149172/205915 local XORs and does not create
an input-dependent count. Thus one uniform C for all input widths is possible
under the stated lift/streaming contracts. A common C for any fixed finite set
of old/new networks can also be chosen by taking their maximum; no uniform
bound over all possible future network searches is claimed.

upstream/build/sections/02-streams.tex:98-118 amortizes ripple counters,
resets and fixed-size collapsed descriptors. Lines124-196 give ordered-affine
shifts and rational scaling. Polynomial b-bit offset work is charged once per
complete q^b target fiber, since b^C=O(q^b), not once per payload bit. Unrelated
spectator counters are not repeatedly read in full. These are written tape-
operation arguments and directly address common hidden-logarithm objections.

An implementation scanning the entire ancestor parking stack for each child,
or copying a growing list of all ancestor subdivisions, would not meet this
contract. The paper explicitly uses stack-local boundaries and combines
consecutive spectator fields into a fixed number of intervals.

5. ONE COMMON ELIGIBLE ADDRESS PRIME

The CRT primes used to certify rational ranks are NOT automatically the runtime
address radix. The runtime q is chosen once after the finite rational basis,
all projector residuals, triangular factors, inverses and nonzero pivot/diagonal
numerators are fixed. Exclude the finite union of bad primes for bit AND
complex tables. A prime beyond all nonzero forbidden integers exists; finite
rational elimination and trial division prepare it independently of width.
Every identity then holds modulo q^b for every positive b, with factors still
invertible. Sources: upstream04:48-101, especially67-77; notes/
partial-swap-construction.tex:16-37; references/copied-fixed/pr34/
ASSEMBLY_PROOF.md:70-79.

Counterexample to a weaker criterion: the integer projector
P=[[-2,3],[-2,3]] satisfies P^2=P. It has no denominator obstruction at q=3,
but its rational rightmost top pivot3 vanishes modulo3; the ordered pivot
position changes. Thus avoiding denominators alone does not preserve the
claimed contiguous pivot profile. The inherited criterion also excludes
nonzero minors/diagonal numerators and prevents this issue.

New reclamation can introduce new finite transitions. One must either rerun
the one-time rational preparation for the enlarged finite table, or prove the
previous prime avoided every transition in a predeclared universal finite
frame family. Reusing an unspecified old q without that argument is not
justified. This affects finite setup constants, not the asymptotic exponent.
Our exact CRT reconstruction validates rational profiles but does not itself
materialize that complete runtime factor table and common q.

6. BALANCED ROUTING AND ANALYTIC INTERFACES

The balanced proof does not get axis-major/group-major permutation for free.
references/copied-fixed/pr34/ASSEMBLY_PROOF.md:111-123 invokes a paid arbitrary-
coordinate router on complete records, K<=K_j<2K, identical supplied width
within each transform round, and disjoint row/control fields. It explicitly
preserves named FFT levels, twiddle order, inverse alignment and prime-box
normalization. Its two cited review files are written conditional transfer
arguments supported by finite tests, not substitutes for the base chunk lemma.

review-arbitrary-routing.md:16-44 requires active masks, inverses computed
from CURRENT addresses, and correction only of exceptional holes. Lines46-78
pay reservoir placement, small-n fallback, incomplete guards and polynomial
map setup. The extra setup is absorbed only in the intended large complete
tensor context; the review does not promise O(V) for an arbitrary supplied
permutation table with tiny V.

review-balanced-transform.md:20-81 proves actual named-slot moves, equal widths
per round and descriptor handling. This historical report retains older
separate-exposure margins; its arithmetic headline must not be combined with
the later bulk transfer by simply deleting terms. The assembly explicitly
switches to the separately reviewed bulk-resampling schedule.

review-bulk-resampling.md:47-55 repairs cyclic endpoint coupling and preserves
the original physical period cut;108-134 bounds fractional source padding and
persistent target halo volume;136-182 describes complete small-field moves,
alternating overlap buffers, ordered page catalogs and final row order;
184-201 gives the paid total cost. Simultaneously rounding every halo axis up
to2L would cause a2^D volume factor; its negative controls explicitly reject
that variant. Catalog setup absorption at166-174 uses D=d-1 tending to infinity
and many complete inner fields, not a free random-access table oracle.

Changing only the bit mixer leaves the Gaussian scalar operator, guard and
precision arguments untouched if its interchange interface still holds. That
conditional substitution is justified in ASSEMBLY_PROOF.md:70-90,111-123.
It does not independently verify phase-cell analysis, eligible analytic-prime
selection, normalized error, precision recovery or every uniform-machine
composition. Those hypotheses remain named and necessary.

RECOMMENDED NEXT FORMAL TARGET

Prove a generic framed-lift lemma parameterized by a literal monotone XOR word,
source-line map, side/center terminal interfaces and complete path events. Its
conclusion should expose the actual early/variable/late scalar phase schedule,
the commuting scatter dispatch, complementary reverse labels, paid copied
streams, and exact recursive-child multiset. Then instantiate it with the
new serialized words and connect it to the already written floor-width,
whole-row and fixed-tape construction. This would close the most consequential
gap between the finite checker and the existing all-size paper proof without
pretending that checking a rational moment already formalizes a machine.