diff --git a/research/selected-rank2-intertwiner/CORRECTION.json b/research/selected-rank2-intertwiner/CORRECTION.json new file mode 100644 index 0000000000..273c2bff58 --- /dev/null +++ b/research/selected-rank2-intertwiner/CORRECTION.json @@ -0,0 +1,77 @@ +{ + "rank": 3, + "left": { + "matrix_rows": [ + 8, + 17, + 33, + 65, + 1, + 130, + 262, + 2, + 4 + ], + "offset": 0, + "quadratic_rows": [ + 1, + 4, + 6, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 2, + 3, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 6, + 480, + 64, + 9, + 18, + 28, + 16, + 160, + 448 + ], + "offset": 5, + "quadratic_rows": [ + 8, + 22, + 30, + 13, + 6, + 352, + 32, + 256, + 416 + ], + "linear_Z4": [ + 0, + 3, + 3, + 3, + 0, + 1, + 0, + 2, + 1 + ], + "phase": 1 + } +} diff --git a/research/selected-rank2-intertwiner/EARLY-CORRECTION.json b/research/selected-rank2-intertwiner/EARLY-CORRECTION.json new file mode 100644 index 0000000000..80c0162339 --- /dev/null +++ b/research/selected-rank2-intertwiner/EARLY-CORRECTION.json @@ -0,0 +1,77 @@ +{ + "rank": 3, + "left": { + "matrix_rows": [ + 10, + 19, + 33, + 1, + 3, + 68, + 128, + 260, + 4 + ], + "offset": 0, + "quadratic_rows": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "linear_Z4": [ + 3, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "phase": 0 + }, + "right": { + "matrix_rows": [ + 6, + 27, + 416, + 25, + 18, + 12, + 288, + 64, + 384 + ], + "offset": 7, + "quadratic_rows": [ + 3, + 13, + 14, + 6, + 0, + 160, + 0, + 160, + 0 + ], + "linear_Z4": [ + 3, + 2, + 3, + 2, + 2, + 3, + 0, + 3, + 2 + ], + "phase": 3 + } +} diff --git a/research/selected-rank2-intertwiner/PROOF.md b/research/selected-rank2-intertwiner/PROOF.md new file mode 100644 index 0000000000..367282cee1 --- /dev/null +++ b/research/selected-rank2-intertwiner/PROOF.md @@ -0,0 +1,246 @@ +# One selected sequential child pair: exact coupling and cost + +All maps below are linear over Q(i), and hence over any characteristic-zero +extension containing i. The inherited coordinate kernel is +`C_q=((1+i)I+(1-i)X_q)/2`. This note uses primary Clifford/native circuit +algebra together with the operator-space viewpoint from linear systems: +the ADD is a coupling channel whose transfer map must be retained. + +## Exact boundary and the intervening region + +Pin the selected source archive and member hashes in `verify.py`. In the +forward phase-B word, events 12806 and 13402 act on register195 by the +recipes `A:0→2` and `B:2→252`. Their ranks are1 and1. The available direct +recipe `C:0→252` has rank2. Let `D:2→559` denote the next donor521 child, +at event14191, of rank2. Frame vectors are + +``` +0: [] 2: [30] 252: [224,30] 559: [416,19,13]. +``` + +There are597 inclusive events:139 climbs and458 scalar ADDs. The only +interior operation touching195 or521 is event12807, +`L195 += (1/2) L521`. The other594 interior events have neither register as +source or target. The verifier reads every event, not just a same-target +subsequence. These operations commute with the two-register macro because +they act on disjoint registers; they remain in their recorded order and are +carried unchanged. No source, centre or dirty helper is silently deleted. + +Let x,y be arbitrary physical values of195 and521 at entry. No zero or +clean-donor premise is imposed. The exact local boundary map is + +``` +M(x,y) = (B A x + (1/2) B y, y). +``` + +Fresh sparse Gaussian-rational evaluation of the serialized left/right +monomials and the coordinate kernel checks every one of512 basis columns. +It proves `BA=C`, including scalar global phases; equality of frame endpoints +alone is not used as proof. Thus + +``` +M = [[C, B/2], [0,I]]. (1) +``` + +Linearity makes the complete512-column check a proof of the entire finite +operator identity. It also checks1024 basis inputs of the two-register +boundary, inverses on arbitrary donor vectors, and the maps below. + +The missing transport has a particularly small witness. Set `x=0,y=e_0`. +The correct target is +`((1+i)e_0+(1-i)e_224)/4`; replacing the pair by C and retaining an ordinary +ADD gives `e_0/2`. Moreover `rank(B-I)=256` over Q(i), computed by exact +Gaussian elimination. This ordinary matrix rank measures a defect; it is +not a native-child tariff or a Fourier width. + +## Unique transport, in both orderings + +After applying C to x, an ordinary ADD with donor transformed by J gives +`Cx+Jy/2`. Equation(1) for every y forces **J=B**. The donor can be restored +immediately by B inverse. Alternatively, move the ADD before C. Its donor +must be transformed by `J=C^-1 B=A^-1`, also uniquely. These are equalities +of operators, without a commutativity assumption on distinct frames. + +If restoration is deferred until donor521's next touch, the intervening +source trace has no other521 operation. In the first ordering its required +next child is uniquely `D B^-1=T559 T252^-1`; in the second it is +`D A=T559 T0^-1`. Both exact maps have eight nonzero entries in every column. +Any monomial--width-r coordinate child--monomial factorization has at most +`2^r` nonzeros per column: the two monomials only permute/phase entries and +the child branches into at most `2^r` positions. Thus each correction needs +r≥3 in this particular one-child normal form. The separately serialized +`CORRECTION.json` and `EARLY-CORRECTION.json` give width3 factorizations; +the fresh checker verifies all512 columns, including phases. The width is +therefore exactly3. Their generation used the credited inherited Clifford +compiler; replay does not import or trust that compiler. + +After the corrected next child, donor521 again has exactly its original +value and frame559, before its following scalar use. Its later work and +existing dirty-return wrappers are preserved. The target ends in frame252 +and its original subsequent ADD is preserved. This is a valid boundary +identity, not a claim that new hosting or a complete supplier is admitted. + +## A different joint-macro class also fails + +Allow any number of vector registers, arbitrary coordinate-uniform scalar +linear mixing between them, and **one invocation of any fixed linear +operator Q on one whole vector register**. Grant scalar work for free. +Clean auxiliary registers start at zero; dirty auxiliary values are arbitrary +independent inputs, with no free input-dependent pre-encoding. The specified +boundary and restoration must hold. All mixing is fixed and linear. A single +call on a larger concatenated register is outside this class. All coordinate-independent scalar operations +before the invocation collapse to `P tensor I`, and those after it to +`R tensor I`. The invocation is +`I + E_jj tensor (Q-I)`. Therefore the complete map is + +``` +(RP) tensor I + (R E_jj P) tensor (Q-I). +``` + +Every input-output vector block lies in `span{I,Q}`. Fixing clean auxiliaries +to zero or requiring dirty auxiliaries to be restored cannot enlarge this +span for the x,y boundary blocks. Equation(1) requires I,B,C all to lie in +that space. But rows `(output,input)=(0,0),(30,0),(224,0)` give, in columns +I,B,C, the exact minor + +``` +[1, (1+i)/2, i/2 ] +[0, 0, -i/2 ] +[0, (1-i)/2, 1/2 ], +``` + +whose determinant is `(1+i)/4 ≠ 0`. Thus this entire scalar-mixing/one-call +class is excluded, even when Q is not a Clifford child. This is not a +no-go theorem for arbitrary joint native macros: coordinate-dependent +permutations or quadratic phases between mixing operations fall outside +`P tensor I`; several coupled operator calls or a different joint primitive +also change the contract. The current prescribed child normal-form adapters +are already absorbed into A,B,C. Treating *new* adapters as scalar mixing +would invalidate this argument. + +## Uniform lifting, rather than a sampled input claim + +For every positive column multiplicity f, define the inherited tensor lifts +`A_f=A^tensor f`, and likewise B,C,D. Tensor functoriality gives +`B_f A_f=C_f`, `C_f A_f^-1=B_f`, and the two correction identities for all f. +All claims also tensor with an arbitrary identity spectator. The dependency +separation of the source word remains valid for these lifts. + +The minor for I,B_f,C_f uses input0 in every factor, and output patterns +`(0,...,0)`, `(30,0,...,0)`, `(224,0,...,0)`. Its determinant is + +``` +((1+i)/4) * ((-1+i)/4)^(f-1), +``` + +which never vanishes. The one-call scalar-mixing obstruction therefore holds +for all f. Each deferred correction column has `8^f=2^(3f)` nonzeros; the +factorwise recipe supplies width3f and the same support bound forces width +at least3f in the monomial/one-child class. This is a uniform algebraic +identity and obstruction for the stated tensor lifts. It does not discharge +the repository's inherited all-size compiler, hosting or analytic assumptions. + +## Positive finite native fusion and its uniform channel bill + +The transfer has an explicit Pauli decomposition, checked on every column: + +``` +B = a I + b P, a=(1+i)/2, b=(1-i)/2, +P e_x = (-1)^parity(96 & x) e_(x xor224). +``` + +`P^2=I`, since parity(96&224)=0. Thus (1) has a legal finite implementation: +apply C to the target, then accumulate `(a/2)y` and `(b/2)Py`, restoring the +donor. With rational scalar ADDs only, a literal schedule is + +``` +x <- Cx +x += y/4; y <- i y; x += y/4; y <- -i y +y <- P y +x += y/4; y <- -i y; x += y/4; y <- i y +y <- P y +``` + +The six source transforms are four scalar unit phases and two signed-XOR +monomials. Each signed XOR is one address permutation plus one sign phase; +calling it one monomial map does not identify it with one scalar CPU operation. +This schedule has four rational array ADDs, six monomial source maps, no new +register, one rank2 target child, and an exactly restored arbitrary dirty +donor. The full1024-column boundary replay verifies this schedule. These are physical +coordinate ADDs in a new macro: the target/donor intermediate frame labels +are not all equal. It is not a drop-in replacement sequence admitted by the +inherited standard scalar-word common-frame checker. A compiler admitting +this new coupled boundary must be supplied before changing the selected word. Its +rank-only recursive expression saves `2-2^(1-a)>0`; the finite arithmetic +increases from one to four array ADDs plus the six stated maps. This is a +constructive finite result, not merely an optimistic endpoint match. + +For every f the same idea expands as + +``` +B_f = sum over S subset {1,...,f} of a^(f-|S|) b^|S| P_S, +``` + +where P_S applies P in factors S. Every coefficient is nonzero. The +`2^f` masks are distinct, so every column of B_f has exactly `2^f` nonzeros. +Consider the explicit accumulation contract: the donor is changed only by +invertible monomial maps and is restored; the target accumulates k scalar +multiples of monomial images of the original donor. Every counted ADD source +must be one such image: no uncounted source additions, precomputed donor +mixtures or additional source registers supplying mixtures are granted. Target monomial charts may be +inserted, but there is no feedback from the target into the donor and no +additional operator call on the donor. Each accumulation contributes at +most one entry per input column to the donor-to-target block. Consequently +**k≥2^f**. The displayed expansion attains this number of Gaussian scalar +channels. It is a sharp result for this accumulation alphabet, not a bound +for all native programs or coupled algorithms. + +Splitting each Gaussian coefficient into real and imaginary rational parts +gives at most `2^(f+1)` rational ADDs and `4*2^f-2` monomial source maps (the +empty-set term needs no P_S/undo pair). Coefficients have an explicit common +denominator `2^(f+1)` and integer numerators of O(f) bits, so their preparation +and arithmetic precision must be charged; they are not fixed-size constants. +For lane volume V=`2^(9f)` times any spectator multiplicity, the schedule +uses at least `V 2^f` coordinate accumulation operations in this literal +array-ADD model, with the stated upper number of array passes. The inherited +volume-linear child expression is `A V (r f)^(1-a)` for a fixed positive A. +Thus this literal expansion cannot have a fixed O(V) adapter invoice or +improve that expression uniformly as f grows: `2^f/f^(1-a)` is unbounded. +This is an asymptotic comparison under the explicit array-cost contract, +not a claimed universal complexity lower bound. A complete selected finite +invoice, encoding costs, hosting and all-size admission are still unproved. + +## Fully charged optimistic screen and decision + +The pinned selected moment source assigns a width-r child the normalized +recursive charge `r^(1-a)` (a common positive factor `m^(a-1)/W` is omitted). +For multiplicity f all expressions acquire the common positive factor +`f^(1-a)`. The selected positive exponent lies in0>i&1) + p+=2*sum((quadratic[i] & x & ~((1<<(i+1))-1)).bit_count()%2 for i in range(n) if x>>i&1) + table.append((y,p%4)) + require(len({y for y,p in table})==1<len(rows): + rows.append(row);locations.append([i,j]) + if len(rows)==3:break + if len(rows)==3:break + require(len(rows)==3,'operator span dimension three') + determinant=ZERO + import itertools + for perm in itertools.permutations(range(3)): + term=ONE + for i,j in enumerate(perm):term=mul(term,rows[i][j]) + inversions=sum(perm[i]>perm[j] for i in range(3) for j in range(i+1,3)) + determinant=add(determinant,neg(term) if inversions%2 else term) + require(determinant!=ZERO,'nonzero exact minor') + # All 1024 basis columns of the two-register block operator are checked. + # On x-inputs: original BA = C. On y-inputs: original B/2 = transported B/2. + for i,e in enumerate(bases): + require(sumcols(cols['B'],sumcols(cols['A'],e))==cols['C'][i],'x block') + by=scaled(cols['B'][i],(F(1,2),F(0))) + require(by==scaled(sumcols(cols['B'],e),(F(1,2),F(0))),'y block') + require(sumcols(Binv,cols['B'][i])==e,'restored arbitrary dirty donor') + require(sumcols(correction,cols['B'][i])==cols['D'][i],'deferred donor restoration') + # Meaningful controls: wrong global phase, wrong ADD coefficient, discarded + # transport, and omitted donor inverse must violate an exact boundary map. + bad=copy.deepcopy(C);bad['right']['phase']=(bad['right']['phase']+1)%4 + require(apply(bases[0],bad)!=cols['C'][0],'global phase control') + witness=next(i for i in range(512) if cols['B'][i]!=bases[i]) + require(scaled(cols['B'][witness],(F(1,2),F(0)))!=scaled(bases[witness],(F(1,2),F(0))),'missing transport control') + require(cols['B'][witness]!=scaled(cols['B'][witness],(F(1,2),F(0))),'coefficient control') + require(cols['B'][witness]!=bases[witness],'dirty restoration control') + require(next(i for i in range(512) if correction[i]!=cols['D'][i])>=0,'unchanged next child control') + return dict(region_events=len(region),region_tag_counts=dict(collections.Counter(e[0] for e in region)), + disjoint_interior_events=594,source_frames={str(i):word['frames'][i] for i in [0,2,252,559]}, + region_sha256=digest(region),complete_basis_columns_per_map=512,two_register_basis_columns=1024, + exact_BA_equals_C=True,donor_correction_column_supports={str(k):v for k,v in supports.items()},donor_correction_minimum_fourier_width=3, + residual_B_minus_I_rank=rr,transport_pauli={'xor':224,'sign_mask':96},finite_native_macro={'rational_adds':4,'monomial_source_maps':6,'new_registers':0,'dirty_donor_restored':True,'rank_profile':{'2':1}},tensor_transfer_channels='2^f exactly in source-monomial accumulation class',operator_span_dimension=3,operator_minor_locations=locations,operator_minor=[[[str(a),str(b)] for a,b in r] for r in rows],operator_minor_determinant=[str(x) for x in determinant],early_correction_minimum_fourier_width=3,first_missing_transport_basis=witness, + missing_transport_original_target=encoded(scaled(cols['B'][witness],(F(1,2),F(0)))), + missing_transport_wrong_target=encoded(scaled(bases[witness],(F(1,2),F(0)))), + map_digests={k:digest([encoded(v) for v in c]) for k,c in cols.items()}, + correction_sha256=digest([encoded(v) for v in correction]),controls_rejected=5, + profiles={'original_target':{'1':2},'immediate_restore_target_and_donor':{'1':2,'2':1}, + 'original_through_next_donor_child':{'1':2,'2':1},'deferred_restore_target_and_donor':{'1':1,'2':1,'3':1}}, + normalized_moment_deltas={'immediate':'2^(1-a)','deferred':'3^(1-a)-1'}, + delta_positive_for='0