Upper-quarter tail: actual SMALL return and native descent
Abstract
An actual quarter-parent in the early or terminal SMALL batches supplies a signed SMALL return batch and a full physical strict J competitor in the upper-quarter three-negative region, without assumptions on the half-parent’s placement.
Theorem 1.1 (Arrival-free upper-quarter exchange with exact returned occurrences).
Lean statement: D5/S3/Combinatorics/Circle/UpperTerminalQuarterExchange.actualSource_threeNegative_upper_quarter_tail_exchange_full
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/UpperTerminalQuarterExchange.actualSource_threeNegative_upper_quarter_tail_exchange_full (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural k,t with k>=3, let the physical universe be Fin k, rho=finRotate k, N=2^k-1, Q=2^(k-2), C=floor(N/2)=2Q-1 and f(i)=((2^i*t+C) mod N)-C. Thus N=4Q-1 and Q>=2. The parameter t is arbitrary: zero, nonunits and shorter numerical periods are included in the source quantifiers. Every list is a list of physical labels; equal source values at distinct labels remain distinct occurrences. Write m(L)=sum(map(f,L)), SMALL for abs(f(i))<Q and LARGE for Q<=abs(f(i)). Legal means physical Nodup and 0<=m(take(j,L))<=C for EVERY natural j, starting at zero. G counts unused physical LARGE labels, H is the sum of 3^abs(f(i)) over used LARGE occurrences, U counts unused physical labels, and J=(G,H,U) in lexicographic order.
Choose arbitrary physical p,y,zpen,z and arbitrary lists A,T0,T1,T2,E. Define n=rho(p), x=rho^2(p), b=rho inverse(y), c=rho inverse(b) and W=A++[x]++T0++[y]++T1++[zpen]++T2++[z]++E. Put P=f(p), D=abs(f(n)), Y=-f(y), theta=Y/4, B=C-P, h=m(W). Set sigma=theta if c is in E and sigma=0 otherwise; low=Y-P-sigma; S=T0++T1++[c] if c is in E and S=T0++T1 otherwise; E0=E.erase(c) if c is in E and E0=E otherwise. The complete premises are P>0; n LARGE; N<3P; original-zero Legal(W); p and n absent from ALL W; every occurrence of T0++T1++T2++E SMALL; Q<=Y, Q<=-f(zpen), Q<=-f(z); B<h<D; Y>P; Y mod 4=0; 3Y>4P; and the ACTUAL c in T0++T1++E. A can contain positive or negative LARGE labels, and x is not required to be the first LARGE. No hypothesis concerns the actual half-parent b’s placement or availability. Neither numerical injectivity, global minimality, favorable reordered prefixes nor an available return batch is assumed.
There exist physical V,I,Ret with I=[p,n], original-zero Legal(V), V.Nodup, InStrip(f,C,0,V), every natural take bound, Inventory(k,t,W,V,I,Ret), (V++Ret).Perm(W++I) and strict J(V)<J(W). The full conclusion distinguishes two literal low-arrival cuts from the rich signed-return construction below. All Inventory fields use the same original W, even when SMALL occurrences are returned. In particular the baseline is never W plus an extra SMALL label.
Let Fpen=A++[x]++T0++[y]++T1++[zpen], Rpen=T2++[z]++E and Fz=Fpen++T2++[z]. If m(Fpen)<=B, set V=Fpen++[p,n], Ret=Rpen. Existing small_weights gives zero LARGE count for T2,E, so Ret has exactly one LARGE and G(V)+1=G(W). Otherwise, if m(Fz)<=B, set V=Fz++[p,n], Ret=E, with zero LARGE returns and G(V)+2=G(W). Both constructions invoke actualSource_prefix_pair_truncation on their literal original prefix and discarded suffix. Their old prefix retains all zero-start gates, while the new heights u+P and u+P-D are in [0,C] because 0<=u<=B and 0<D<P. Thus all natural prefixes, physical Inventory and strict G and J descent hold. The actual discarded suffix can contain SMALL occurrences; these branches do not assert all-SMALL retention or strict H descent.
For the remaining branch, BOTH actual old arrivals m(Fpen) and m(Fz) are strictly greater than B. native_geometry gives f(n)=-D, f(x)=r=abs(f(x)), Q<=D<P<r<=C, 2P+D=N, r=2P-D and 2P<=C+Q=3Q-1. Centered source bounds give every abs(f(i))<=C, hence 0<=B and Y<=C. The actual inverse-source theorem negative_parent is used twice, first at y and then at b. Odd N makes both outer successor values odd. Since Y is divisible by four, the two successive even negative successor equations are 2f(b)=-Y and 2f(c)=f(b). Therefore Y=4theta, f(b)=-2theta and f(c)=-theta. This uses actual inverse physical rotations, including the cyclic seam, and does not select a label merely having the same value.
The scalar reserve bounds are consequences of these exact source equations. Y>=Q and Y=4theta give theta>0. From 4theta<=2Q-1 and 2P<=3Q-1, integrality gives theta<=C-P=B. The strict upper-quarter hypothesis 3Y>4P gives 3theta>P, which with the native budget implies theta>=P-Q-1. If sigma=theta then low=3theta-P>0; if sigma=0 then low=Y-P>0 by Y>P. In both cases 0<=sigma<=theta. Also D<P and 2P+D=N give 3D<=N-1=2C. Combining this with 4theta<=C and C>0 yields D+theta<C. No inequality comparing Y with r and no assumption on an available b is used.
Put a0=m(A) and beta=a0+P-D. The untouched old prefix immediately before x gives a0>=0 and the actual x arrival gives a0+r<=C. Thus the replacement pair p,n has legal intermediate heights a0+P and beta, with 0<=beta<=B. All internal prefixes of arbitrary A are literally their old zero-start prefixes. Let B1=A++[x]++T0++[y]++T1 and B2=B1++[zpen]++T2. Define d1=m(B1), a1=d1+f(zpen), d2=m(B2), a2=d2+f(z). Original Legal supplies each of d1,a1,d2,a2 in [0,C]. The failed cut tests give a1>B and a2>B; the two retained negative LARGE hypotheses give d1>=a1+Q and d2>=a2+Q.
The physical batch S is extracted before selection. When c is in E, the actual erasure gives ([c]++E0).Perm(E), and S adds exactly this removed occurrence. Otherwise actual tail membership forces c to be in T0++T1, so S=T0++T1 and E0=E. Thus in both cases c is in S and (S++E0).Perm(T0++T1++E), whose right side is an actual sublist of W. Original physical Nodup proves S.Nodup and precludes duplicating c across these regions; every S occurrence is SMALL. The exact masses are m(S)=m(T0)+m(T1)-sigma and m(E0)=m(E)+sigma. Direct mass calculation gives beta+m(S)=d1+low, using r=2P-D, Y=4theta and low=Y-P-sigma. Since d1>beta, m(S)>low. Existing positive_mass_dominates proves m(S)<=m(filter(0<f,S)); this establishes actual positive supply, rather than inserting a supply premise into the telescope.
The exact call to signed_short_reserve_select is f, T=S, P0=[], N0=[c], width B, M=Q-1, target low. Its full assumptions are verified as follows. S is physically Nodup, B>=0 and M>0. The empty positive reserve is a subpermutation of its positive-short filter. The singleton negative reserve [c] is a subpermutation of the ACTUAL negative-short filter of S with bound B+1, since 0<-f(c)=theta<=B. Every positive S entry is at most Q-1. Target low is positive and the positive filter supplies it. Finally M-B-1=P-Q-1<=theta=m(f,[])+m(-f,[c]). Thus the existing signed selector produces physical R,K with (R++K).Perm(S) and low<=m(R)<=low+B. Commuting the two batches gives (K++R).Perm(S), and its subpermutation property gives R.Subperm(S). Both selected and complementary batches are SMALL because every S occurrence is SMALL.
Only the selector’s public contract is used: physical partition and exact mass bounds. It need not expose a positive-only or positive-plus-c support description. Therefore the conclusion asserts no retention of the actual b, wherever it occurs. Since m(R)>=low>0, R is nonempty and its length is at least one. Put eta=low-m(R), so -B<=eta<=0. Each of the four retained LARGE boundary heights d1+eta,a1+eta,d2+eta,a2+eta is in [0,C]. The lower bounds use a1,a2>B and eta>=-B, with departures no lower than their corresponding arrivals. The upper bounds use eta<=0 and actual old legality. No old internal SMALL prefix is translated.
The uniform endpoint is e=h+Y-P-m(R)=h+sigma+eta. The blocking lower bound h>B, sigma>=0 and eta>=-B give e>=h-B>0. The upper bound h<D, sigma<=theta, eta<=0 and D+theta<C give e<=h+theta<D+theta<C. Actual partition masses provide the three exact identities beta+m(K)=d1+eta, a1+eta+m(T2)=d2+eta and a2+eta+m(E0)=e; the last uses a2+m(E)=h and m(E0)=m(E)+sigma. These are the full physical batches, including all signed occurrences, not subsets guessed from numerical sums.
For a positive SMALL i and negative SMALL j, integrality gives f(i)-f(j)<=2Q-2<C=2Q-1. SmallStepOrdering.exists_order_between is invoked EXACTLY three times: on K from beta to d1+eta, on T2 from a1+eta to d2+eta, and on E0 from a2+eta to e. It gives L01.Perm(K), L2.Perm(T2), LE.Perm(E0), each with every internal prefix in its prescribed strip. Assemble V=A++[p,n]++L01++[zpen]++L2++[z]++LE. InStrip concatenation joins the original A, the checked p,n gates, the three complete SMALL strips and both retained negative gates. Thus every natural zero-start prefix is covered, including zero, all block joins, the final prefix and saturated overlength takes.
Actual occurrence counts in the three ordering permutations, the selector partition and the uniform source partition prove (V++([x,y]++R)).Perm(W++[p,n]). Ret=[x,y]++R consists of actual old occurrences: x,y lie in W and R.Subperm(S) with S drawn from the old T0,T1,E. Both inserted labels are distinct LARGE and fresh in ALL W. A single inventory_of_perm application over W supplies the entire physical Inventory; it reuses the existing physical_balance proof and full physical source-cycle sum zero. W++[p,n] is Nodup, so the full permutation also shows returned occurrences are absent from V and all occurrences are counted once. The retained zpen,z are present. Every old SMALL outside R, including any such occurrence in A, is retained.
For completeness the Inventory has twelve separate fields, all over the full Fin k universe. They are: V.Nodup; used(V)=(used(W) minus used(Ret)) union used(I); disjointness of those two used pieces; unused(V)=(unused(W) minus used(I)) union used(Ret); disjointness of those two unused pieces; G(V)+largeUsed(I)=G(W)+largeUsed(Ret); H(V)+H(Ret)=H(W)+H(I); U(V)+length(I)=U(W)+length(Ret); remainingMass(V)=-m(V); m(V)+m(Ret)=m(W)+m(I); remainingSmall(V)=remainingSmall(W) union the SMALL support of Ret; and disjointness of the last two pieces. These fields count physical occurrences even when values repeat. They also apply unchanged to the low-prefix branches with their actual discarded suffixes.
In the rich branch, small_weights gives zero LARGE count and zero energy for R. Exactly two LARGE are inserted and two returned, yielding G(V)=G(W) and U(V)=U(W)+length(R). The SMALL support of [x,y]++R is exactly R.toFinset, so remainingSmall(V)=remainingSmall(W) union R.toFinset with those pieces disjoint. Exact energy is H(V)+3^abs(f(x))+3^abs(f(y))=H(W)+3^abs(f(p))+3^abs(f(n)). The native expanding-path energy inequality 3^P+3^D<3^r implies H(V)<H(W), and equal G then gives strict J descent despite the precisely accounted increase in U. The Inventory source balance and r=2P-D give m(V)=e. Its full-source complement field yields remainingMass(V)=-e. No claim that all old SMALL are retained is made.
The external context is Damasdi–Frankl–Pach–Palvolgyi, Monochromatic configurations on a circle, arXiv:2504.10687v2, Conjecture 3.1, DOI 10.5070/C6.68671. The target capacity there is C=(N-1)/2 for every positive k. This theorem constructs a competitor only under its stated native three-negative, upper-quarter and actual c-in-T0++T1++E hypotheses; it makes no literature-novelty claim and does not settle full original-quantifier Circle C3.1. At a genuine global J minimum among ALL original-zero Legal physical words, its actual competitor excludes this region. It supplies neither global resource availability nor an exclusion for c blocked in A or T2, or for other parity and ancestor configurations.
The earlier lower-quarter argument applies under all of its original native premises, including actual c in E and 3Y<=4P; it supplies no generalized lower-quarter exclusion for c in T0 or T1. A fresh c can be appended under its actual native premises: theta<=B<h and f(c)=-theta give 0<h-theta<C, unchanged G,H and one fewer unused SMALL. Within the strict upper-quarter region of the theorem here, these fresh-c and tail competitors restrict c at a genuine global minimum to A or T2. Across both quarter regions, retaining all actual premises of those earlier arguments gives only the weaker necessary placement c in A,T0,T1 or T2, using their c-in-E case. These conditional consequences do not resolve c-in-A, c-in-T2, other ancestor or parity configurations, general resource availability or full original-quantifier C3.1.