Two generations and complete SMALL-prefix normalization
Abstract
An odd first negative in the actual three-negative source word gives a strict physical competitor, or forces a LARGE occurrence in the original prefix together with the exact parent or grandparent placement alternative.
Theorem 1.1 (Unconditional physical placement alternative).
Lean statement: D5/S3/Combinatorics/Circle/OddFirstNegativePlacement.actualSource_threeNegative_oddFirstNegative_placement
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/OddFirstNegativePlacement.actualSource_threeNegative_oddFirstNegative_placement (✓ std3). ∎
Source. Repository-derived.
Commentary.
For arbitrary natural k,t with k>=3, the labels are the physical elements of Fin k, rho=finRotate k, and f(i)=centered(2^k-1,2^it). Put Q=2^(k-2), N=4Q-1 and C=N/2=2Q-1. Quantify arbitrary p,y,zpen,z:Fin k and arbitrary physical lists A,T0,T1,T2,E. Define n=rho(p), x=rho(n), P=f(p), D=abs(f(n)), r=abs(f(x)), S=T0++T1++T2++E and W=A++[x]++T0++[y]++T1++[zpen]++T2++[z]++E. The complete assumptions are P>0, Q<=abs(f(n)), N<3abs(f(p)), Legal(W), p and n absent from ALL W, abs(f(i))<Q for every occurrence in S, Q<=-f(y), Q<=-f(zpen), Q<=-f(z), C-P<mass(f,W)<D, P<-f(y), and (-f(y)) mod 2=1. Legal means W.Nodup and 0<=mass(f,W.take j)<=C for EVERY natural j. There is no coprimality or numerical-period hypothesis. A can contain arbitrary positive or negative LARGE occurrences; the SMALL hypothesis applies only to S.
Set Y=-f(y), Z1=-f(zpen), Z2=-f(z), F=A++[x]++T0++[y], R=T1++[zpen]++T2++[z]++E, v=mass(f,F), beta=rho^(-1)(y), gamma=rho^(-1)(beta), L=(N-Y)/2, d=P-D and delta=Y-P. Native geometry gives f(n)=-D, f(x)=r, Q<=D<P<r<=C, D=N-2P and r=2P-D. Old legality immediately before and after y gives 0<=v<=C-Y. Also r=D+2d<=C and D>=Q give 2d<=Q-1. These are actual old-prefix bounds, without any assumed valley, selected cut or new ordering.
The public theorem asserts a full physical strict-J competitor OR the conjunction of an actual LARGE occurrence in the ORIGINAL A and the original two-generation placement alternative. The latter says beta is in A with max(Z1,Z2)<=P and max(Z1,Z2)=P implying min(Z1,Z2)<=D, or ALL of these hold: beta is unused in W, gamma is in the ACTUAL A, f(beta)=L, 1<=delta, 3delta<=d-2, (Y+1)/2-d<=v<=C-Y, Q<=D<L<P, 2d<=Q-1, max(Z1,Z2)<=L, and max(Z1,Z2)=L implies min(Z1,Z2)<=D. Even L gives f(gamma)=L/2>0 with abs(f(gamma))<Q; odd L gives f(gamma)=-M for M=(N-L)/2 and D<L<M<P<Y. Neither predecessor availability nor a LARGE occurrence in A is an assumption. The competitor retains Legal(V), V.Nodup, InStrip(f,C,0,V), every natural prefix bound, inserted and returned physical lists I,Ret, the exact (V++Ret).Perm(W++I), and J(V)<J(W).
The rich competitor uses batches A’ and T0’. Either A’=A and T0’=T0, or A’=[] and T0’=Aprime++T0 for an explicit physical Aprime with Aprime.Perm A. Put W’=oldWord(p,y,zpen,z,A’,T0’,T1,T2,E), S’=T0’++T1++T2++E and F’=A’++[x]++T0’++[y]. The conclusion records Legal(W’), W’.Perm W, the SAME used set, source mass, G,H,U,J, and that all S’ occurrences are SMALL. The six rich branch descriptions below use F’,S’,A’,W’ when the word was normalized; their Inventory, strict J, G/H/U and physical set conclusions are all relative to ORIGINAL W. Also mass(f,F’)=mass(f,F)=v, so the gate 2(v+d)<=Y-1 keeps its original height. In particular a normalized literal V=F’++I is not identified with F++I.
Here is the actual normalization when A has no LARGE occurrence. Classical integer order gives abs(f(i))=0 and 0<=a0+r<=C, while native geometry gives 0<r=f(x)<=C. For opposite signed occurrences i,j of A, SMALL means f(i)<=Q-1 and -f(j)<=Q-1, so f(i)-f(j)<=2Q-2<C. Apply exists_order_between to the ENTIRE list A at start r and endpoint r+a0. It constructs Aprime.Perm A and InStrip(f,C,r,Aprime). The word W’=[x]++Aprime++T0++[y]++T1++[zpen]++T2++[z]++E is therefore zero-start Legal: the literal x gate is legal, every reordered Aprime prefix lies in the strip, and the SAME old tail beginning with T0 resumes at r+mass(f,Aprime)=a0+r. This does not move the old order of A unchanged and does not assume any new Legal word. The original A order can have peaks exceeding C-r.
The complete word permutation W’.Perm W gives W’.Nodup, the same physical used set and complement, the same source mass and endpoint, and the same G,H,U,J. Freshness of p,n is unchanged. Represent W’ with A’=[] and T0’=Aprime++T0; all its SMALL-tail hypotheses hold by Aprime.Perm A. Apply the private two-generation classifier to that actual word. Its parent-in-A’ and grandparent-in-A’ branches are impossible because A’ is empty, so one of its six full physical competitors is constructed. If A contains a LARGE occurrence instead, apply the same private classifier to the untouched original word. Thus a single public arbitrary-A classifier consumes both the existing two-generation argument and the physical complete-batch construction.
For a negative source occurrence y, the physical inverse-parent parity formula gives either even Y with 2f(beta)=-Y and beta negative SMALL, or odd Y with 2f(beta)=N-Y and beta positive LARGE. Thus the odd hypothesis gives f(beta)=L. For the positive beta, apply the actual source-cycle equation at gamma=rho^(-1)(beta), so rho(gamma)=beta, including the cyclic seam. Its carry identity implies (2f(gamma)) mod N=f(beta) mod N. Centered representative uniqueness, centered bounds and centered_double give doubleStep(N,f(gamma))=f(beta). The three doubling branches and odd modulus yield f(gamma)=L/2 for even L and (L-N)/2 for odd L. These are identities of centered integer representatives; they do not assert injectivity of the physical source values.
For the following two-generation proof, read A,T0,S,F,W as the chosen representative A’,T0’,S’,F’,W’. All source labels and scalar identities are unchanged, as are the total height h and the first-negative height v. If the original prefix contains a LARGE occurrence, this representative is the literal original word. If the original prefix is all SMALL, the representative has the constructed empty prefix and enlarged first SMALL batch. The final transport paragraph returns all physical conclusions to the original W.
Before making any assumption on beta’s placement, test max(Z1,Z2)>P or max(Z1,Z2)=P with min(Z1,Z2)>D. The old literal y gate gives 0<=v<=C-Y
If beta is outside A, its positive LARGE value L<P<r excludes p,n,x,y,zpen,z and every SMALL occurrence in S. Hence beta is unused in W. First test 2(v+d)<=Y-1. When it holds, choose I=[p,n,beta], V=F++I and Ret=R. Every old F prefix is retained. The three new heights are v+P, v+d and v+d+L. The first is <=C because v<=C-Y and Y>P, the second is nonnegative and below the first, and the last is <=C by 2C=N-1 and 2L=N-Y. All inserted labels are fresh, distinct and LARGE. R has exactly two LARGE occurrences, so G(V)+1=G(W) and strict J follows at the first coordinate. SMALL occurrences in R really are returned.
If that gate fails, oddness of Y gives 2(v+d)>=Y+1. Combining with v<=C-Y gives 3Y<=N+2d-2. Since d=3P-N, this is 3delta<=d-2. Thus (Y+1)/2-d<=v and Y<r, whence 2(L-D)=r-Y>0. No inequality v<d is used. In this surviving region test max(Z1,Z2)>L, or max(Z1,Z2)=L with min(Z1,Z2)>D. If either holds, choose I=[beta,n], V=F++I and Ret=R. The two new heights v+L and v+L-D lie in [0,C], since L<Y and D<L. Here G(V)=G(W), and the exact energy equation is H(V)+3^Z1+3^Z2=H(W)+3^L+3^D. If the maximum exceeds L, its power is at least 3^(L+1)>3^L+3^D; at equality, cancel 3^L and use the strict minimum inequality. Thus H(V)<H(W), giving strict J with no condition on U.
Otherwise max(Z1,Z2)<=L, and equality of the maximum with L forces min(Z1,Z2)<=D. For odd L put M=(N-L)/2. The native identities and the failed gate imply D<L<M<P<Y. If gamma is outside A, its actual value -M excludes x,y, both later negatives whose magnitudes are <=L, and all SMALL occurrences. Thus gamma is unused. Choose I=[beta,gamma,p,n], V=F++I and Ret=R. Write w=v+L-M. The lower bound for v gives 2w>=L+1-2d>=2, using L>=Q and 2d<=Q-1. Also w<v<C-P. The four new heights are v+L, w, w+P and w+d, all in [0,C]. The four inserted LARGE occurrences are pairwise distinct by their displayed signed values. Therefore G(V)+2=G(W), again a strict first-coordinate descent. If gamma is in A, the entire residual conjunction already holds.
For even L the actual gamma value is a=L/2, with 0<a<Q. If gamma is unused, choose the literal V=W++[gamma], I=[gamma], Ret=[]. The endpoint satisfies h+a<D+a<=C, where h=mass(f,W): indeed 2D+L<2D+P=2N-3P<N. The only new height is legal and all old prefixes survive. The exact physical conclusions are Used(V)=Used(W) disjoint-union {gamma}, Unused(V)=Unused(W) minus {gamma}, and remainingSmall(V)=remainingSmall(W) minus {gamma}. Further G(V)=G(W), H(V)=H(W), U(V)+1=U(W), mass(f,V)=mass(f,W)+f(gamma), and remainingMass(f,V)=-mass(f,V). Hence the THIRD lexicographic coordinate strictly decreases. The LARGE-only Inventory formula is not used for this SMALL insertion.
If even-L gamma is used but outside A, its positive SMALL value excludes x,y,zpen,z, so gamma lies in the actual S. Invoke the existing actualSource_threeLarge_singleAnchor_exchange_full with q=beta and physical anchor a=gamma. Its assumptions are derived: beta is fresh, Q<=f(beta)=L<P, Z2<=L, f(gamma)>0, f(gamma)<=C-L+1, and every other positive SMALL value u is at most f(gamma)+(C-L)+1. The latter follows from u<=Q-1 and f(gamma)=L/2<Q; the anchor bound follows from 3L<N. This gives actual lists B,K with B.Subperm(positive(t,S)), (K++B).Perm S and every B occurrence positive SMALL. Its literal V=A++[p,n]++K++[z,beta], I=[p,n,beta], Ret=[x,y,zpen]++B has full Inventory, G(V)=G(W), U(V)=U(W)+B.length and H(V)<H(W), hence strict J. This private construction retains the chosen representative prefix A; in the normalized application that prefix is empty. The complete single-anchor construction supplies all gates and all natural prefixes.
For each of the four literal LARGE truncations and for the single-anchor case, Inventory is precisely the existing physical proposition. It states the disjoint used partition Used(V)=(Used(W) minus Used(Ret)) union Used(I), the disjoint unused partition Unused(V)=(Unused(W) minus Used(I)) union Used(Ret), G(V)+largeUsed(I)=G(W)+largeUsed(Ret), U(V)+length(I)=U(W)+length(Ret), H(V)+H(Ret)=H(W)+H(I), and mass(f,V)+mass(f,Ret)=mass(f,W)+mass(f,I). It also states remainingMass(f,V)=-mass(f,V) and the disjoint remaining-SMALL union with the returned SMALL labels. Physical freshness, Nodup and the whole-word permutation establish these facts through inventory_of_perm; no new inventory structure is needed. Total source zero is used only for the complete Fin k source in physical_balance, never asserted for proper W. InStrip and inStrip_prefix include take 0 and every overlength take, whose height is the endpoint.
For the normalized competitor, compose (V++Ret).Perm(W’++I) with W’.Perm W appended by the SAME I to obtain the exact original-W permutation. Transfer each existing Inventory field using equality of the original and normalized used sets, source mass and G,H,U. This preserves the complete physical used/unused disjoint partitions, returned SMALL union, complement sum and source/count/energy balances. For the fresh even-L SMALL branch, keep its literal V=W’++[gamma], but transfer gamma unusedness, Used(V)=Used(W) disjoint-union {gamma}, Unused(V)=Unused(W) minus {gamma}, remainingSmall(V)=remainingSmall(W) minus {gamma}, exact G/H equality, U(V)+1=U(W), source mass increment and complement sum to ORIGINAL W. No all-LARGE Inventory assertion is made in that branch. Finally J(W’)=J(W) transfers its strict descent. These are physical permutation and set arguments and require no distinctness of numerical source values.
At a global J minimum over ALL zero-start Legal words for the same source, the competitor alternative is impossible. Thus the ORIGINAL A contains a LARGE physical occurrence, and either beta is in A with max(Z1,Z2)<=P and equality forcing min(Z1,Z2)<=D, or the unused beta and used gamma in A satisfy the entire original narrow strip and parity alternatives. If A is all SMALL, its complete-batch normalization makes both predecessor-in-empty-prefix alternatives impossible and constructs a strict competitor. This also covers A=[] without a further named theorem. Together with the existing arrival-free first-negative exchange for Y<=P, the all-SMALL-prefix configuration cannot be minimal for any odd first Y. The minimum ranges over words of every legal endpoint, including zero; there is no fixed-endpoint or retained-SMALL restriction. In the remaining signed-LARGE-prefix region, 3(Y-P)>=d-1 is incompatible with the residual strip and therefore forces beta into A at a global minimum.
The source context is G. Damasdi, P. Frankl, J. Pach and D. Palvolgyi, Monochromatic configurations on a circle, arXiv:2504.10687v2, Conjecture 3.1, DOI 10.5070/C6.68671. The source definitions and exchange results used here are those of SourceWidth, ZeroSumSubsets, ExpandingSourcePath, MixedSuffixEnergy, TwoOppositeLargeExchange, ThreeLargePacketExchange, FirstNegativeShiftExchange and SingleAnchorLargeExchange. The ordering step is SmallStepOrdering.exists_order_between on the entire actual prefix batch. Arbitrary signed A containing a LARGE occurrence and either the parent with the necessary P energy bounds, or an unused parent with its grandparent in A in the surviving strip, remains unresolved. The argument does not prove that x can be selected as the first used LARGE occurrence, and it does not establish full Circle C3.1.