Every original natural 2<=a<=b=d<c
Abstract
Third peak with equal second and last gaps: the complete physical face
Theorem 1.1 (One old physical permutation and one literal fresh insertion).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/ThirdPeakEqualSecond/Endpoint.actualSource_third_peak_equal_second_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/ThirdPeakEqualSecond/Endpoint.actualSource_third_peak_equal_second_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural a,b,c with 2<=a<=b<c, put d=b, k=a+b+c+b and A=1+2^a+2^(a+b)+2^(a+b+c). There exist one permutation sigma of every original Fin k label and a natural cut j<=k such that OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,j)) both hold. The ear is the literal insertion of the sole fresh label k; old labels and their source values retain their original identities. For all natural m,n, every n-term prefix of m copies of sigma has sum in [0,modulus(k)/2], and every n-term prefix of m copies of the same ear word has sum in [0,modulus(k)]. For every natural m each repeated row has total zero separately. Zero repetitions, empty takes and takes beyond the finite word are included.
Let x=2^a, y=2^b, z=2^c, N=xyzy-1 and Q=2N+1. The old positive heads are A=1+x+xy+xyz, B=1+y+xy+xy^2, L=1+z+yz+xyz and K=1+y+yz+y^2z. Set H=1+y+yz, SU=2B-1, SV=2L-1-z and SW=2K-H. The four actual positive chains U,V,W,X start at labels 0,b,b+c,b+c+b, with b-1,c-1,b-1,a-1 occurrences. Their paired heads are (A,2A),(B,SU),(L,SV),(K,SW). The four following terminal labels are b-1,b+c-1,b+c+b-1,k-1, with terminal heads (B,SU),(L,SV),(K,SW),(A,A). The actual fresh label has new value A.
For a<b put r=2^(b-a-1) and m=2^(c-b), so y=2rx and z=my. A mask M denotes the increasing list of actual exponents whose bits occur in M; within a complete width ell stock its complement is (2^ell-1) XOR M. The selected and complementary lists partition those physical occurrences even when numerical source values coincide. Their masses are M times the head and (2^ell-1-M) times the head. These statements use full binary stocks and never infer containment in a partly spent stock from a numerical bound.
The paid schedule terminates in U,V,W,X order. Put q=1,w=2 if r=1 and q=0,w=r otherwise. Its positive banks are U(full)++V(m-1), V(full XOR (m-1)), W(full XOR w)++X(q), and W(w)++X(full XOR q). Insert fresh immediately before the fourth bank. Its first three old endpoints are mB-A, L-A and (q+1)K-A-wL; the new endpoints are mSU-2A, SV-2A and (q+1)SW-2A-wSV. The fourth endpoints vanish. The windows hold whenever 4m<=y, or r=1 and m<=x. In particular they cover both dyadic gaps m=2,4 for every strict a<b.
For every m>=8 use v=ceil((3A+1)/(2SU)), represented exactly as (3A+2SU)/(2SU) in integer division. The terminal order is V,W,X,U, fresh lies immediately before the second bank, and the banks are V(full XOR (v-1)), W(full XOR w), W(w)++X(full), and U(full)++V(v-1). Choose w=1 for r=1, w=2 for r=2, and w=floor(K/L)-1 for r>=4. These are all dyadic possibilities for r. The old endpoints are L-vB, K-wL-vB, A-vB and zero; the new endpoints are SV-vSU, SW-wSV+A-vSU, 2A-vSU and zero. Exact unbounded polynomial margins imply 1<=v<m, vB<A, vSU<2A and 2vSU>=3A+1. For r>=4, floor division gives L<=K-wL<2L and 0<=2w<=y-2, placing every bit of w in the full W stock. The adjacent and quadruple cases have their own exact second-window margins.
For every terminal the actual endpoint e and its positive terminal head T satisfy 0<=e and 2e<=T-1 in both rows. The native terminal identities and the nonnegative bank values convert these inequalities into all individual prefix bounds. The resulting finite physical certificate is interpreted by PacketNormalForm.actual_four_packet_iff. On a=b the exact EqualFirstTwoLast endpoint supplies the same original family directly. The existing zero-period transport extends each order to every natural finite repetition and prefix while preserving separate zero totals.
This result covers the entire d=b face with no bound on b-a or c-b. The parent target 2<=a<b<=d