Two independent unbounded gaps and one literal cut
Abstract
A physical order on the equal-first-two max-plus-one boundary
Theorem 1.1 (The entire boundary family).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/EqualFirstTwoMaxPlusOne/Endpoint.actualSource_equal_first_two_max_plus_one_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/EqualFirstTwoMaxPlusOne/Endpoint.actualSource_equal_first_two_max_plus_one_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every pair of natural numbers u,c with u>=2 and c>u, set a=b=u, d=c+1, k=2u+c+d and A=1+2^u+2^(2u)+2^(2u+c). There is one permutation sigma of the original physical Fin(k) labels for which OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,k-1)) both hold. In each order the full integer sum is zero and every natural take-prefix lies between zero and half the corresponding modulus. Empty, full and overlong takes are included. Repeated numerical values and nonprimitive seeds are included, since the construction retains physical occurrences.
The redistribution is the caller’s construction. Put x=2^u, z=2^c and t=2z. The old heads are A=x^2z+x^2+x+1, B=2z(x^2+x+1)+1, L=2z^2*(x+1)+z+1 and M=2xz^2+xz+x+1. The enlarged heads are 2A, Bp=2B-1, Lp=2L-1-z and Mp=2M-1-x-xz. SourceTable derives the actual centered old and enlarged recurrences, and PacketNormalForm.Source supplies their head bounds. For N=x^2zt-1 the physical U,V,W,X chains have lengths d,c,u,u and offsets 0,d,d+c,d+c+u. A positive chain occurrence at relative index i has value 2^i times its head. The terminal value is -(N-H)/2, where H is the successor head; the enlarged row uses modulus 2N+1 and its enlarged successor head. The fresh label k has enlarged value A.
Let v=c-u-1 and q=2^v. The actual positive occurrence V_v is moved to the X bag. When c<=2u-1, put p=0 and move no second V occurrence. When c>=2u, let w=c-2u and p=2^w, and move V_w to the W bag. In this chart w<v
The negative terminal order is U,W,V,X. The first positive bag is U_1 through U_(d-2). The second is W_0 through W_(u-2), then U_0, then V_w when present. The third is V_0 through V_(c-2) with V_v and the optional V_w erased; erasure preserves the remaining increasing order. The fourth is X_0 through X_(u-2), then V_v. Follow each bag by its own negative terminal. The final terminal is the original physical X_(u-1)=k-1. Insert label k immediately before it: the cut is literally k-1. The inventory proof uses list permutations and two distinct erasures to partition the whole label range; it does not identify labels whose values coincide.
Write s=2^(u-1) and r=2^(c-1), so x=2s and z=2r. The old bag masses are (z-2)A, (s-1)L+A+pB, (r-1-p-q)B and (s-1)M+qB. Their enlarged counterparts replace heads A,B,L,M by 2A,Bp,Lp,Mp; the last enlarged bag also contains the fresh value A. The negative values in terminal order are B-zA, M-sL, L-rB, A-sM, with the analogous enlarged expressions. All masses are derived from sums of the actual physical chains and the inventory identity.
The old post-terminal seams are B-2A, B-A+M-L+pB, M-A-qB and zero. The new seams are Bp-4A, Bp-2A+Mp-Lp+pBp, Mp-2A-qBp and zero. The successor heads in this terminal order are B,M,L,A and Bp,Mp,Lp,A. Thus the peak margin is (H-1)/2 minus the corresponding seam. The Arithmetic module proves the four seams and four peaks in both rows, as well as the terminal zero, by exact polynomial identities and nonnegativity.
The two charts exhaust all c>u. In the small chart c<=2u-1, q>=1, s>=2q, z=2xq and r=xq. Substitute q=1+j and s=2q+h with j,h>=0. Every required endpoint difference has nonnegative integer coefficients. Equivalently the caller’s chart uses ratio=2q>=2, x=2ratio+2h and z=xratio. In the large chart c>=2u, s>=2, p>=1, z=x^2p, q=sp and r=2s^2p. Substitute s=2+h and p=1+j with h,j>=0. Again every endpoint difference expands with nonnegative coefficients. These are unbounded symbolic estimates, with no enumeration of u or c and no numerical control used as an assumption.
The boundary c=u+1 has q=1, and u=2,c=3 has s=2 and h=0. The boundary c=2u-1 has s=2q in the small chart. The boundary c=2u has p=1 in the large chart, with distinct relative V indices zero and u-1. The non-strict inequalities retain every one of these boundary cases. Positivity inside each bag extends the endpoint bounds to all prefixes; lift_order and marked_word then produce the original Fin-label predicates with the same sigma and the stated literal cut.
This proves the independent two-parameter family a=b>=2, c>a, d=c+1. The full unrestricted four-gap joint-order assertion J remains OPEN.