All a>c>max(b,d), b,d>=2, including b=d
Abstract
A common physical ear order over the full first-peak C-second region
Theorem 1.1 (One permutation, one literal cut, both actual source rows).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/FirstPeakCSecond/Endpoint.actualSource_first_peak_c_second_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/FirstPeakCSecond/Endpoint.actualSource_first_peak_c_second_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
Its exact natural telescope is (a,b,c,d), 2<=b, 2<=d, b<c, d<c, c<a, equivalent to a>c>max(b,d), b,d>=2. Put k=a+b+c+d and seed=1+2^a+2^(a+b)+2^(a+b+c). The public declaration constructs a single permutation sigma of all original Fin(k) physical labels and a single literal j<=k satisfying OriginalOrder(k,seed,sigma) and OriginalOrder(k+1,2*seed,earWord(k,sigma,j)). Both predicates include the complete permutation, exact zero total and every natural take-prefix, including empty, full and overlong takes. No feasibility certificate, favorable mask, unfinished proof, symmetry, cyclic covariance or finite cutoff is a premise. Equal numerical values never identify physical occurrences.
The full live proof first splits b<=d from d<b. The b<=d branch uses the consumed private CMiddle construction for a>c>d>=b, retaining equality b=d. The dc>b>d. No separate public regional target or named combination wrapper is retained. The module boundary separates the expensive 98 CMiddle certificate identities from its mask, inventory, rounding and dispatch proofs; the other 36 identities feed Arithmetic, then Banks, then the strict endpoint branch. All helpers support this single proof graph.
Set x=2^a,y=2^b,z=2^c,t=2^d,e=2^(c-d),h=2^(a-c),n=eh,N=xyzt-1,Q=2N+1,D=yz+y+1. The actual old bases on U,V,W,X are A=xD+1, B=xt(y+1)+t+1, L=xzt+zt+z+1, M=tyz+D. Their enlarged bases are 2A,Bn=2B-1,Ln=2L-z-1,Mn=2M-D. These are precisely the pinned source-table formulas, on lengths [d,c,b,a] and starts [0,d,d+c,d+c+b]. The four old terminal doubles are [B-N,L-N,M-N,A-N], and the enlarged terminal doubles are [Bn-Q,Ln-Q,Mn-Q,A-Q]. The enlarged X successor is A. The fresh source label k has value A.
At immutable repository pin 1add3bcde3f5768e7c5b7c84867d9758df1e6e6b, PacketNormalForm.Source supplies both physical source evaluations, positivity off the four negative labels, old total zero, enlarged old-label total -A and fresh value A. Its actual_nat_joint_iff transport converts the natural-label word into sigma by the label map, preserves the literal insertion cut by marked_word, and checks the actual OriginalOrder source sums and every natural take-prefix. It does not treat numerical equality of two source values as identity of the occurrences.
Within the b<=d branch, b
The X,U,V,W terminal order moves all native U positives to X, X mask p to U, X mask q to W and V mask w to W. Its first bank is X minus m followed by all U positives; its second is X mask p; its third is V minus w; its fourth is all W positives followed by X mask q and V mask w. Each bank is followed by its own negative terminal, in the order X,U,V,W. The exact finite-label multiset identity proves that every old label appears once. Insert fresh k immediately after terminal X, at j=a+d-1-popcount(s-1). The enlarged second bank therefore STARTS with fresh k. It is not moved to the first bank or rotated around the circle.
The doubled old first seam is tA-2sM; its later seams are B-rM, L-rM-wB,0. The enlarged first seam is (t-1)A-sMn BEFORE the ear, and its later seams are Bn-rMn,Ln-rMn-wBn,0 AFTER the ear. The matching successors are old [A,B,L,M], enlarged [A,Bn,Ln,Mn]. All lower seam gates and upper peak gates are checked using these exact successors. Within a positive bank every step increases both source coordinates, so the full endpoint bounds control every internal prefix, including the first inserted fresh-label prefix. The final zero seam is retained and follows from the actual source total and physical permutation.
The equality boundary b=d is separate. Its exact rank-two identities are A-L=C=(x-z)(t+1), B-M=tC, M=(t+1)(tz+1), B=(t+1)(tx+1). For h=2 the terminal order is V,U,X,W. Three UNBOUNDED charts choose (r,R): e=2,t>=4 uses (1,3); e>=4,t>=8 uses (e/2,3e/2+1); t=4,e>=16 uses the same latter formula. R is odd before any natural cast, R<x/2 and r-1<z/2. Move V mask r-1 to U, X local bit zero to U, and X mask R-1 to W. Oddness makes the bit-zero occurrence disjoint from R-1. The fresh label is immediately after terminal U. Its literal cut is c+d+1, since the two V submasks cancel in the combined bank length.
For that V,U,X,W order the old seams are [L-rB,M-C,L-RM,0], and the enlarged seams are [Ln-rBn,Mn-2C-z-1,Ln-RMn,0]. The first TWO enlarged seams precede the ear; the third includes it. Matching successors are old [L,B,A,M], enlarged [Ln,Bn,A,Mn]. In particular the X successor is A in both rows. Each chart retains fourteen named old/new lower/upper polynomial margins. The two identically zero final lower seams are proved inline in its sixteen-slot margin package; the transport obtains the final lower bounds from the exact source totals.
For h>=4 on b=d, the X,U,V,W construction has FIVE exhaustive unbounded charts: e=2,t>=8,h>=4 with s=h(t-1),w=1; e=2,t=4,h>=32 with the same s,w; e>=4,t>=8,h>=4 with g=n/4,s=g(2t-3),floor w; e>=8,t=4,h>=4 with that same floor recipe; and e=4,t=4,h>=8 with g=h,s=5h+r and floor w. The last recipe remains dependent on the actual ceiling r. Here p=5h and q=r-1<h occupy disjoint high and low bit ranges. No divisibility of s by h is inferred. Its first-gate proof uses the actual four ceil-dependent bounding polynomials rather than treating r as an arbitrary independent parameter.
Every CMiddle X chart proves F=Btyz-MMn>=0 and gMn>=B. Since Mn-M=tyz, the exact ceiling implies rM<B. The second enlarged seam is twice the second old seam plus rD-1. For w=1 the remaining two certificate inequalities are (L-B-M)Mn-BM>=0 and 2B-L-1>=0. For floor w they are L-2B-gD>=0 and zB-2L-1>=0. The floor remainder gives the third old gate, w<z/2 gives physical capacity, and K2=2S2+rD+w-z-1 together with D>=z+1 gives its enlarged lower gate. Its enlarged upper bound is 2K2<=4B+2gD-z-8<=2L-z-8<=Ln-1.
The consumed CMiddle source expands exactly 98 polynomials as explicit sums of nonnegative integer-coefficient monomials and supplies ring/positivity proof scripts for their equality and sign: sixteen strict margins and eighty-two equality margins. Strict expansion variables substitute y=4+Y,t=2y+T,h=2+H and either e=2 or e=4(1+E). Equality substitutions are h2/e2/t4+T; h2/e4(1+E)/t8+T; h2/e16(1+E)/t4; h4+H/e2/t8+T; h32+H/e2/t4; h4+H/e4(1+E)/t8+T; h4+H/e8(1+E)/t4; h8+H/e4/t4. Integer rounding, physical inventory and all-prefix transport have their own proof scripts and do not follow from coefficient signs alone.
Exactly six isolated parameter tuples use literal words, with insertion cut shown first: (5,2,3,2),j=7,[10,9,4,5,8,7,1,3,11,0,2,6]; (6,2,3,2),j=7,[11,10,4,3,8,7,1,5,9,12,0,2,6]; (7,2,3,2),j=8,[12,11,7,4,3,9,8,1,0,13,5,2,10,6]; (6,2,4,2),j=8,[4,11,8,5,6,10,9,1,12,2,13,0,3,7]; (5,2,4,2),j=6,[11,3,5,4,2,1,0,9,12,6,10,8,7]; (6,2,5,2),j=8,[5,4,9,6,0,11,10,1,13,3,14,7,12,2,8]. The concrete decide proofs check permutation; norm_num unfolds actual centered reductions and the recursive strip for these constants. These six words do not replace any unbounded corner family.
Exhaustion uses the natural exponents a-c,c-d,d, not bounded sampling. On h=2, the excluded t4/e4,e8 points are precisely the last two fixed tuples. On h>=4, t4/e2/h4,h8,h16 give the first three fixed tuples, and t4/e4/h4 gives the remaining fixed tuple. All larger exponents in CMiddle enter one of its ten unbounded charts.
For the strict d<b branch the tight dyadic quotient H=x/(2z)=2^(a-c-1) replaces the loose CMiddle sufficient bound F. The loose expression Btyz-MMn can be negative here and is not used in this branch. Default g=2^(a-d-2),s=g(2t-3); on t=4,y=8,z=16 use g=2^(a-5),s=11g for EVERY a>=5. The physical construction remains X,U,V,W with the fresh occurrence immediately after X.
The four unbounded polynomial charts are: C1 z=2y,t>=8, with t=8+T,y=2t(1+Y); C2 z=2y,y>=4t, with t=4+T,y=4t(1+Y); C3 z>=4y, with t=4+T,y=2t(1+Y),z=4y(1+E); C4 t=4,y=8,z=16 and EVERY a>=5. In every chart x=2z(1+J), H=1+J=x/(2z), and all chart variables are nonnegative. Exponent-gap cases prove exhaustion. Default g=x/(4t),s=g(2t-3); C4 uses g=x/(8t),s=11g for its whole infinite a-family. The source contains all 36 exact polynomial identities, 1,078 monomials, with explicit ring and positivity scripts. Their seven shared margins are tA-2sM, A-1-tA+2sM, 2(t-1)A-2sMn, A-1-2(t-1)A+2sMn, B-HM-1, HMn-B and g-H. The remaining margins are L-B-HM and 2B-L-1 on C1,C2,C4, and L-2B-HD and zB-2L-1 on C3. The false loose condition Btyz-MMn>=0 is never used.
Choose r=(B-1)/Mn+1=ceil(B/Mn). Exact floor bounds prove 1<=r<=H<=g, B<=rMn<B+Mn and rM<=B-1. For z=2y choose w=1; for z>=4y choose w=floor((L-rM)/B). The floor remainder and strict capacity margin give 0<=w<z/2. Set p=s-r,q=r-1,m=s-1. Since g is a power of two dividing s, the low grain bits of m are all ones; q is supported there and p is the exact complement within m. Thus p and q are disjoint, p+q=m and m<x/2. All integer capacities and nonnegativity facts precede casts to natural masks.
Move every U positive to the X bank, the X p-mask to U, the X q-mask to W and the V w-mask to W. The four banks are X outside p and q together with U, then p, then V outside w, then all W together with q and w. Terminal order is literally X,U,V,W. Physical support disjointness and the exhaustive complement prove one permutation of all original labels; no terminal bit is moved. Insert fresh k immediately after X. The first bank and its terminal have length j=a+d-1-popcount(s-1). Here popcount is exactly the cardinal of Nat.bitIndices.toFinset, not a numerical approximation.
The old seams after the terminals are tA/2-sM, B-rM, L-rM-wB,0. The enlarged seams are (t-1)A-sMn, Bn-rMn,Ln-rMn-wBn,0; the first is before the fresh ear and the last two include it. For a terminal successor Z and row modulus R, twice its value is Z-R. The nine margins and tight ceil/floor arithmetic prove 0<=2h<=Z-1 at each seam in each row. The enlarged U bank starts with the positive fresh A. Every positive bank rises from a nonnegative seam to a bounded peak; the pinned four_strip theorem transports these endpoint inequalities to all natural prefixes. The actual centered-source lift preserves this same sigma and literal cut.
The four strict charts retain all 36 exact polynomial identities (1,078 nonzero sparse monomials), including the zero grain-capacity margin on C4. Together with CMiddle there are 134 named certificate identities on 14 genuinely unbounded construction charts and exactly six isolated words. Each certificate is an explicit Lean polynomial identity and sign proof; the general rounding, mask, inventory, exhaustion and transport arguments are separate proof obligations.
The one typed Reg mirrors the complete nine-binder target with the existential sigma and literal cut, without the strict draft’s three construction lets in the public type. Its readout is the existing DependentFamily.realize template enrolled by Reg.Support.DependentFamily.enrollment_1. Both old and enlarged observations use actual OriginalOrder, with natural seed state and full four-coordinate dependent output. The arena law is exactly the whole chamber theorem. The typed realization includes actual-law, rejected whole-family law and deletion of each side. Actual observational dependence uses p=(5,2,3,2), which lies inside this full chamber: seed zero accepts the complete increasing physical word, whereas seed two has prefix -1 in both the 12-label and 13-label rows. These two dependence tests concern the readout family and do not replace either construction or its ear identity. The typed Contract.Registration contains the source realization proof, enrolled readout, complete sourceSelection paths over nine binders, continuation unknown and familyRecord none.
The mature ingredients are binary expansion and physical finite-set partition, integer Euclidean ceiling/floor bounds, exact polynomial identities with nonnegative coefficients, monotonicity of positive packet prefixes, and the existing centered-source/ear transport library. These are established methods, not claims of a new general theory. The new chamber construction, tight quotient and ordinary proofs are attributed to the caller.
The conclusion is confined to the complete first-peak C-second chamber. Full unrestricted physical J and Circle C3.1 remain OPEN.