Moving one LARGE label across an arbitrary mixed suffix
Abstract
Retained LARGE exchange: retain an actual later same-sign LARGE after a native even expanding path, deriving its new gate and strict (G,H,U) descent with exact physical inventory.
Theorem 1.1 (E_keep_one with the proved singleton gate and exact energy cancellation).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/MixedSuffixRetainedLarge.mixed_suffix_retained_large_exchange (✓ std3). ∎
Source. Repository-derived.
Commentary.
The source is SourceWidth.actualSource on physical Fin(k), with k>=3, N=2^k-1 and C=N/2. LARGE means 2^(k-2)<=|s|. W=A++[x]++B is Nodup and legal from zero at capacity C. The actual modulo-k path from p has even length m>=2, consists of unused LARGE labels, and enters consumed x. d=3*|s(p)|-N is strictly positive. The suffix has exactly m LARGE labels and arbitrarily many SMALL labels in arbitrary positions. A physical z in B is LARGE, s(p)*s(z)>0, and |s(z)|<=|s(p)|. No minimizer, availability, endpoint, legal new gate, energy drop, or suffix viability is a hypothesis.
The delivered word is literally V=(A++path)++[z]. The proof consumes MixedSuffixEnergy.mixed_suffix_energy_exchange on the truncated legal old word A++[x], with an empty suffix. This supplies m<k, path.Nodup, legality of V0=A++path for every natural take, and H(V0)<H(A++[x]). It does not apply E_mix’s m-1 bound to the present m-LARGE suffix B. Unusedness in the full W separately proves disjointness from every physical old label, hence z is moved once and V remains Nodup.
The extra consumed helper unsigned_path_sum uses the existing SourceWidth.unsigned_step, ExpandingSourcePath.phase_step, SourceWidth.path_range and SourceWidth.path_sum. The unsigned potential is u(q)=s(q)+N when s(q)<0 and u(q)=s(q) otherwise. It gives sum(path)=u(x)-u(p) on the actual physical path, including the seam. ExpandingSourcePath.expanding_path_estimates, with orientation chosen from the sign of s(p), forces x to have that same sign and to be LARGE. The unsigned corrections therefore cancel, proving sum(path)=s(x)-s(p), rather than assuming this identity or duplicating the source profile proof.
Put a=sum(A) and b=sum(V0). The proved endpoint gives b+s(p)=a+s(x), while old legality bounds a+s(x) in [0,C] and the inherited path proof bounds b in [0,C]. For s(p)>0 the sign condition gives s(z)>0 and the magnitude bound gives s(z)<=s(p), so 0<=b+s(z)<=b+s(p)<=C. For s(p)<0 it gives s(z)<0 and s(p)<=s(z), so 0<=b+s(p)<=b+s(z)<=b<=C. This is the real singleton LARGE gate at its new position. Intervening SMALL or LARGE labels in old B supply no premise. Appending this singleton proves InStrip and all-natural zero-start prefix bounds, including empty and overlength takes.
Let R={x} union (B.toFinset minus {z}), S=W.toFinset and I=path.toFinset. The exact used partition is (S minus R) union I; the exact unused partition is (S complement minus I) union R. Both displayed unions are proved disjoint. Thus only z is retained from B, x is returned, and every other suffix occurrence is returned. All equal values and short numerical orbits still count as separate Fin(k) labels. No unit, numerical-injectivity, full numerical-period, seam, or tie exception is introduced.
MixedSuffixEnergy.G, H, U, J, largeUsed and smallUsed are reused unchanged. Each inserted label is LARGE, so largeUsed(path)=m. With x and z both LARGE, equality largeUsed(B)=m and physical conservation prove G(V)=G(W). Exact cardinality conservation proves U(V)+m=U(W)+B.length and therefore U(V)=U(W)+smallUsed(B). Nodup makes these list-weight calculations physical set inventories. The native zero-total source_cycle also gives the new complement sum equal to minus the new endpoint.
The retained term cancels using the actual physical permutation B ~ z::B.erase(z), not by identifying equal numerical values. The proof exports H(V)+3^|s(x)|+H(B.erase(z))=H(W)+H(path). The inherited source energy bound implies H(V0)<H(A++[x]); adding the same retained term and the nonnegative returned energy yields H(V)<H(W). Hence the first coordinate of the natural lexicographic J=(G,H,U) is equal and the second strictly decreases even though returning SMALL labels may increase U.
This is a conditional exchange for arbitrary even m and arbitrary mixed B. The numerical k=10,t=360 control is used only as a transient nonvacuity calculation, with no additional canonical numerical theorem. Full C3.1, universal exchange availability, and arbitrary-tail continuation remain OPEN. In particular the two later opposite-sign LARGE case still needs an actual physical SMALL-subset departure gate or a different exchange. k<3 and d=0 are outside the theorem; zeros cannot satisfy its strict same-sign retained-label hypothesis.