A literal ear and the remaining charge
Abstract
A physical joint order for all independent equal-first-three gaps
Theorem 1.1 (Every independent s,d at least two).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/EqualFirstThree/Endpoint.actualSource_equal_first_three_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/EqualFirstThree/Endpoint.actualSource_equal_first_three_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every two independent natural numbers s,d>=2, put k=3s+d and A=1+2^s+2^(2s)+2^(3s). There is a single list sigma permuting all Fin(k) physical labels and a natural numeric cut j<=k such that OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,j)). Each order asserts the exact integer total zero and the half-modulus strip for every natural take-prefix, including empty and overlong prefixes. The fresh label is k; all original labels retain their identity even when centered values repeat or the value sequence has a shorter period. No coprimality, supplied schedule, or primitive-period assumption appears.
Write R=2^s,D=2^d,C=R^2+R+1,A=RC+1,N=DR^3-1. The actual old coefficients are A,V=DC+1,W=DR^2+(D+1)R+1,X=(D+1)R^2+R+1. Physical chains U,V,W,X start at 0,d,d+s,d+2s and have lengths d,s,s,s. Their last labels are the four negative occurrences; the preceding labels form positive dyadic packets. The cyclic identities DA=N+V,RV=N+W,RW=N+X,RX=N+A determine the source. The source proof reuses centered ladder identities, including their range bounds. Applying them at d+1 and shifting by one gives the actual new coefficients 2A,2V-1,2W-R-1,2X-C. The actual fresh value is A.
If f_i is the old centered value, the nonnegative quotient q_i=(A*2^i-f_i)/N has positive bases 0,1,R+1,C and negative values 1,R/2+1,R(R+1)/2+1,(A+1)/2. Thus the actual new value at an old label is g_i=2f_i-q_i. Totals over physical labels are sum(f)=0,sum(q)=A,sum(g)=-A; the fresh ear restores new total zero. Before the ear the new height is 2h-P, where P is consumed charge. After the ear it is 2h+Q, where Q is remaining charge. These are different modes. Requiring h+Q to stay in the old half strip is an unnecessary stronger condition and would exclude valid small-d constructions.
The five parameter regions partition the whole domain. At d=s, natural physical order works with the ear first. At d=s+1, natural physical order uses the interior cut 3s+1, after U,V,W. The old seams are A-1,A-R-1,R^3,0; the old packet peaks are (N+next)/2-A and next<=2A-1. Before the interior ear the new seams are 2A-3,2A-3R-3,2R^3-C. Inserting A then gives height 3R^3. The last new positive peak is N-(A-1)/2, and the last actual negative is its opposite. This is why an interior ear resolves the apparent strong obstruction. In fact the actual slice s=2,d=3 also forbids every ear-first joint witness: before its first old negative any legal old order needs two positive labels, since a single old positive is at most 170 while every old negative has magnitude at least 171. Any two distinct actual new positive labels contribute at least 447; with the initial fresh ear 85 this gives 532>511. The natural word with the internal cut 7 remains legal. This arithmetic explanation is an ordinary obstruction argument, not a separately asserted Lean refutation theorem.
For d<s<=2d-1 put H=2^(s-d),n=H-1. Use all V positives,V-; all W positives,W-; all U positives and the X mask n,U-; then the X complement,X-. Insert the ear immediately before X-, at the numeric cut k-1. The mask and its complement partition actual X occurrences. The three old seams are R-D,(R-D)(R+1),nC; 2H<=D gives all old peak bounds. The new seams before the ear are R-2D,(R-2D)(R+1),(H-2)C, all nonnegative. Every earlier new height is 2h-P<=2h<=N-1. The ear raises the last peak to exactly -g_X-, within [0,N].
For s>=2d put H=2^(s-d),n=H-1,r=R/2,e=D/2,w=r-H,HU=(N-V)/2,U=HU-wW and x=floor(U/X). The physical word is all U positives,V mask n,W-; V complement,W mask n,V-; X complement of x,X-; remaining W positives,X mask x,U-. Insert the ear immediately before X-. All positive packets preserve increasing physical-label order. The floor gives S=U-xX>=0 and the arithmetic proof gives 1<=2S+Q<=L, where Q=1+(R+1)w+Cx and L=(A-1)/2. Consequently the new peak after the ear and before X- is 2S+Q+N-L<=N, and the following seam is 2S+Q>=0. This uses the actual remaining charge rather than a strong shadow bound.
The floor budget is unbounded: it proves (L-2X-Q0)X-CU>=0 for Q0=1+(R+1)w, using positive polynomial expansions in D-8 and R-D^2 when D>=8, and in R-64 when D=4,R>=64. The only remaining dyadic cases are D=4,R=16 or 32, discharged as inline arithmetic leaves. Their (w,x,S,Q,L) are (4,2,631,615,2184) and (8,5,3600,5550,16912). They are leaves of the universal proof, not separately retained finite positive results.
For d>=s+2 reserve the actual U occurrence of dyadic weight u=2^(d-s-1)=D/(2R). Use all other U positives,W-; all V positives,V-; all W positives,U-; reserved U occurrence and all X positives,X-. The ear is first. Substitution D=2Ru, R>=4,u>=2 proves nonnegative old and new seams and the required packet peaks. All these words are realized by binary masks and complementary masks on physical intervals; permutation proofs rearrange occurrences, never source values. Inside a positive packet both actual rows increase, so endpoint peaks and following nonnegative seams bound every interior prefix. Complete totals handle the last packet and every overlong prefix.
The result advances the equal-first-three subfamily of the physical four-gap joint-witness problem associated with Circle Conjecture 3.1 in Damasdi, Frankl, Pach and Palvolgyi, Monochromatic configurations on a circle, arXiv:2504.10687v2. The four gaps of the unrestricted problem remain independent; full four-gap J and Circle C3.1 remain open. No external novelty claim is made.