Every independent natural 2<=c,d<a<=b
Abstract
Second peak and first-second maximum: complete physical joint lift
Theorem 1.1 (One original permutation and one literal fresh insertion).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakSecondMaximum/Endpoint.actualSource_second_peak_second_maximum_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakSecondMaximum/Endpoint.actualSource_second_peak_second_maximum_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
For all independent natural a,b,c,d with 2<=c, 2<=d, c<a, d<a and a<=b, put k=a+b+c+d and A=1+2^a+2^(a+b)+2^(a+b+c). There exist one permutation sigma of the original Fin k labels and a natural cut j<=k such that OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,j)) both hold. The very same witnesses satisfy every old repeated-prefix bound in [0,(2^k-1)/2] and every new repeated-prefix bound in [0,2^k-1], for every natural repetition count m and prefix length n. Both scalar totals are zero for every m. This includes zero repetitions, empty prefixes and prefixes beyond the repeated finite word. No rotation, reflection or change of source is used. The unrestricted all-gap Circle J and C3.1 remain open.
Write x=2^a, y=2^b, z=2^c, w=2^d, N=xyzw-1 and Q=2N+1. The old heads are A=1+x+xy+xyz, B=1+w+wx+wxy, L=1+z+wz+wxz and K=1+y+yz+wyz. Put H=1+y+yz, S=1+x+xy, SU=2B-1, SV=2L-1-z and SW=2K-H. PacketNormalForm identifies the actual centered source rows: U_j=d-j-1, V_j=d+c-j-1, W_j=d+c+b-j-1 and X_j=k-j-1 have vectors 2^(d-j-1)(A,2A), 2^(c-j-1)(B,SU), 2^(b-j-1)(L,SV) and 2^(a-j-1)(K,SW), respectively. The four terminal labels are d-1, d+c-1, d+c+b-1 and k-1. Their old and new increments are one half of the difference between the corresponding successor head and N or Q. The one fresh label k has vector (0,A). Equal vectors always remain distinct occurrences.
The partition d<c, c=d, d=c+1 or c+2<=d is exhaustive. The d<c branch directly uses the complete SecondPeakMiddleGap construction. Every other branch has terminal order W,X,U,V. In all three, W receives W depths 1 through a-1; every V positive and the W tail at depths a through b-1 go to V. Let q=2^(b-a), D=K-qL and Dprime=SW-qSV. The W endpoint is (D,Dprime). Every omitted tail remains in the physical inventory, including when b=a or a=d+1 makes a range empty.
On c=d, put t=2^(a-d-1), so x=2wt. Define alpha=2tH-S and gamma=tH-S. If alpha<=D, X receives X depths 1 through d-1 and fresh before its terminal, while U receives all its own positives and X_d. The literal fresh cut is a+d-1. If alpha>D, X receives X depths 1 through d-2, the actual U_(d-1) at index 0, and X_d; U receives U depths 1 through d-2, X_(d-1), and fresh before its terminal. The cut is a+2d. V receives every X depth strictly greater than d in either allocation. These complementary paired exchanges preserve all original occurrences and exactly one fresh occurrence.
For c=d, the X endpoint is (D-alpha,Dprime-2gamma) on the first allocation, and (D+(A-3alpha)/2,Dprime-3gamma) on the second. The old correction has denominator two. Both allocations then reach (B+D-tK,SU+Dprime-tSW) after U and (0,0) after V. The identities 2tK=A+alpha and tSW=A+gamma determine these endpoints from the actual dyadic masses. Here alpha>0, 4alpha<A and gamma<0. With h=tH and g=-gamma=h-alpha, Dprime<=h and A-1=2wh give the new X windows for multipliers two and three. The alpha comparison gives the old X windows. The W and U windows follow from exact nonnegative margins in w-4,t-1,q-1. This includes d=2 and q=t=1.
On d=c+1, use t=2^(a-d-1). X receives X depths 1 through d-1 and fresh; U receives all its own positives. V receives all X depths d through a-1. The literal cut is a+d-1. The endpoints after X and U are (D+A-2tK,Dprime+2A-2tSW) and (B+D-2tK,SU+Dprime-2tSW), and V ends at (0,0). Here w=2z and x=2wt. Every lower margin and every terminal half-head upper margin is proved as an exact nonnegative polynomial in z-4,t-1,q-1. In particular the new U margin retains the residual -z and its compensation from (2t-1)(H-2wz); no positivity assumption from d<c is imported.
On c+2<=d, the existing broad certificate is used directly. Set r=2^(a-d), so x=rw, and E=B+D-rK, F=SU+Dprime-rSW, J=F-2E. X contains its own depths 1 through d-1 and fresh. A bit selector u=floor(E/A) sends precisely those actual U labels to V, with their complements remaining in U; all X depths d through a-1 also go to V. The estimates 0<E<(w/2)A and 0<J<A prove 0<=u<2^(d-1) and put the U endpoint (E-uA,F-2uA) in both windows. The canonical binary mask sum and split lemmas establish the physical occurrence and complete partition, rather than assuming scalar stock is available.
The broad transfer changes (E,F) by (-uA,-2uA), preserving J. The unimodular change of coordinates (E,F) to (E,F-2E) interprets the quotient by the lattice generated by (A,2A) as a residue modulo A and an integer invariant. This quotient interpretation explains the selector; the proof uses the concrete binary label action and its invariant. A quotient or a transitive abstract action alone would not establish that the required physical labels occur. The diagonal alternatives similarly act by actual paired transpositions, preserving their common U endpoint.
For every packet, all assigned positives are nonnegative in both coordinates. If its endpoint is e and its terminal successor head is T, then its preterminal peak is e+(N-T)/2 in the old row, or e+(Q-T)/2 in the new row. The proved windows 0<=e and 2e<=T-1 therefore bound every prefix. Complete physical inventory, canonical source identities and these six windows construct unconditional PacketNormalForm certificates. Its equivalence supplies both original physical orders and the literal ear. The existing zero-period transport then gives all natural repeated prefixes and zero totals. These are exact statements about the stated discrete source family; no claim of literature novelty, unrestricted joint lifting or official acceptance is made.
Original equal-tail application: scope and parameter map
The adaptive-mask and ceiling-mask methods below are attributed to the original SecondPeakEqualTailCones exposition in https://github.com/the-omega-institute/trureturing/pull/25303. They describe that specified construction and its source proof strategy. Current verification of its literal constructor, all general integer chart gates and all orthant inequalities is unestablished here. The current endpoint supplies existence through a different physical construction; it does not identify its witnesses with these masks or fixed word. Statements about the original source below are made within this boundary. No literature novelty or unrestricted Circle J/C3.1 conclusion is asserted.
The original five-binder family is (a,b,s: natural), hs:2<=s and hcone:((2s+2<=a and a+1<=b) or (s+1<=a and max(a+1,3s+1)<=b)) or (2<=a and a+1<=s and 2s+1<=b). Set k=a+b+s+s and A=1+2^a+2^(a+b)+2^(a+b+s). In the first two cones instantiate actualSource_second_peak_second_maximum_joint_lift at (a,b,c,d)=(a,b,s,s): each cone implies s<a and a<=b, and hs gives both tail bounds. In the third cone instantiate SecondPeakEqualTail.actualSource_second_peak_equal_tail_joint_lift at (a,b,c)=(a,b,s): its hypotheses 2<=a<s<b follow directly. Each application supplies one sigma and one j<=k, both complete OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,j)), their exact zero totals and every natural take-prefix. The same witnesses also satisfy all natural repeated-prefix bounds and zero totals; projecting the two orders recovers the original existential contract without another hypothesis. This parameter map establishes existence, not equality with the original specified constructor.
Original adaptive construction: Source
For natural a,b,s, put k=a+b+2s and A=1+2^a+2^(a+b)+2^(a+b+s). The physical chains U,V,W,X start at 0,s,2s,2s+b and have lengths s,s,b,a. They are occurrences in the original word, not a sorting of residue values. Write x=2^a,y=2^b,z=2^s,D=y(z+1)+1 and N=xyz^2-1. Their old heads are A=xD+1, B=xz(y+1)+z+1, L=xz^2+z^2+z+1 and M=yz^2+D. The enlarged heads are 2A, Bn=2B-1, Ln=2L-z-1 and Mn=2M-D; its modulus is Q=2N+1.
The recurrences are zA=N+B, zB=N+L, yL=N+M, xM=N+A, and z(2A)=Q+Bn, zBn=Q+Ln, yLn=Q+Mn, xMn=Q+A. With a,b,s at least 2, each nonterminal occurrence is its head times its local power of two and is positive; every terminal is negative, with doubled value equal to successor minus modulus. These facts specialize the existing physical centered-source arithmetic to the equal-tail layout.
The old complete sum is zero. The enlarged values on inherited labels sum to -A, while the actual fresh label k has value A, so its complete sum is also zero. These are the exact row formulas consumed by both schedules. Source preparation alone does not choose a permutation or prove the full Circle J statement.
Original adaptive construction: Native
Assume s>=2 and either 2s+2<=a with a+1<=b, or s+1<=a with max(a+1,3s+1)<=b. These premises imply a>=s+1, b>=a+1 and b>=2s. With x=2^a,y=2^b,z=2^s, set lambda=2^(b-a-1), epsilon=0 for b=a+1 and epsilon=2^(b-a-2) otherwise. The W allocation is p=y/(2z)+y/z^2-1-epsilon. Its nested capacities are H=2^(b-s)-1 and F=2^(b-1)-1.
The adaptive X allocation is C=2^(a-s-1)-delta, where delta=1 when b>=3s+1 and delta=0 otherwise; its capacity is E=2^(a-1)-1. Exact power factorizations justify the natural quotients and integer casts, including every subtraction. The bounds are 0<=p<=H<=F and 0<=C<=E. Only the capacities H,F,E are required to be all-ones masks: C may be an arbitrary submask of E when delta=0, and C=0 is allowed.
The bitwise complement identities become H XOR p=H-p, F XOR H=F-H and E XOR C=E-C, with safe integer casts. The low-bit bound ensures every decoded set bit is a legal local positive position. These facts support a partition of physical occurrences, without replacing the masks by merely equal numerical masses.
Original adaptive construction: Seams
Use source heads (A,B,L,M), enlarged heads (2A,Bn,Ln,Mn), and terminal order W,U,X,V. For u=z/2-1, capacities h,f,e and allocations p,c, the four bank rows in chain order U,V,W,X are (u,0,p,0), (0,u,h-p,c), (0,0,f-h,0) and (0,0,0,e-c). A dot product with either head vector gives the corresponding positive mass.
The first doubled postterminal seam is twice bank 1 mass plus the W successor minus the row modulus. The second adds twice bank 2 mass and the U terminal. The third adds bank 3 and the X terminal; in the enlarged row it also adds the true fresh contribution 2A. Thus these seams are cumulative prefixes, not individual bank increments. For each of the first three seams the four gates are the old seam, old successor minus 1 minus that seam, the new seam, and new successor minus 1 minus that seam.
All twelve nonnegative gates bound both rows at the required terminal interfaces. The final bank returns both doubled sums exactly to zero by the eight source recurrences and 2(u+1)=z, 2(f+1)=y, 2(e+1)=x. This algebra is shared by the native upper allocation and the lower-cone ceiling allocation; positivity and physical inventory are separate obligations.
Original adaptive construction: Dyadic
The chart table has eight rows and eleven slots: x,y,z,z/2,y/z,y/(2z),y/z^2,x/(2z),y/2,x/2,lambda. Each slot is an integer monomial in chart variables u,v,w, so no division is performed inside a polynomial gate proof. The associated epsilon row is (0,w,vw,0,v,4u^2v,2uv^2w,uv), and the adaptive delta row is (1,1,1,0,0,1,1,1).
The actual row uses powers 2^a,2^b,2^s,2^(s-1),2^(b-s),2^(b-s-1),2^(b-2s),2^(a-s-1),2^(b-1),2^(a-1),2^(b-a-1). Natural exponent equalities are proved before translating these powers into monomials. Under s>=2, a>=s+1, b>=a+1 and b>=2s, equality of the eleven slots plus the epsilon and delta identities transports the entire native allocation matrix to the selected chart.
This is the interface between natural-gap case splitting and integer ring positivity. It preserves the actual W and X masks, including the zero X allocation on the first low-a boundary; it does not create a new ordering theorem.
Original adaptive construction: Charts
For s>=2, the two upper clauses are (2s+2<=a and a+1<=b) or (s+1<=a and max(a+1,3s+1)<=b). The first clause splits at a=3s, then at adjacency b=a+1, or at b=3s+1 when a<3s. This yields the high-adjacent, high-separated, high-b/low-a, low-b-adjacent and low-b-separated charts.
The remaining range s+1<=a<=2s+1 has b>=3s+1. It splits into a=s+1, s+2<=a<=2s, and a=2s+1. Each chart proves equality of all eleven dyadic slots and of epsilon and delta, using natural gap inequalities to prevent truncated-exponent errors. All chart variables are powers of two and hence at least 1, including endpoint equalities.
Transport then applies the corresponding twelve integer polynomial gates to the native allocation. The eight chart cases therefore supply the first three old and new seam bounds throughout the two-clause upper union. The lower cone 2<=a<s, b>=2s+1 uses the separate ceiling construction; neither this case split nor the endpoint asserts all of Circle J.
Original adaptive construction: HighAdjacent
For s>=2 and a>=3s and b=a+1, choose u=2^(s-2), v=2^(a-3s), w=1. Then z=4u, x=64u^3v, y=128u^3v, with lambda=1, epsilon=0 and delta=1. The native X allocation is C=8u^2v-1. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 0 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: HighSeparated
For s>=2 and a>=3s and b>=a+2, choose u=2^(s-2), v=2^(a-3s), w=2^(b-a-2). Then z=4u, x=64u^3v, y=256u^3vw, with lambda=2w, epsilon=w and delta=1. The native X allocation is C=8u^2v-1. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 1 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: HighBLowA
For s>=2 and 2s+2<=a<3s and b>=3s+1, choose u=2^(a-2s-2), v=2^(3s-a-1), w=2^(b-3s-1). Then z=8uv, x=256u^3v^2, y=1024u^3v^3w, with lambda=2vw, epsilon=vw and delta=1. The native X allocation is C=16u^2v-1. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 2 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: LowBAdjacent
For s>=2 and 2s+2<=a, b<=3s and b=a+1, choose u=2^(a-2s-2), v=2^(3s-b), w=1. Then z=8uv, x=256u^3v^2, y=512u^3v^2, with lambda=1, epsilon=0 and delta=0. The native X allocation is C=16u^2v. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 3 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: LowBSeparated
For s>=2 and 2s+2<=a, b<=3s and b>=a+2, choose u=2^(a-2s-2), v=2^(b-a-2), w=2^(3s-b). Then z=16uvw, x=1024u^3v^2w^2, y=4096u^3v^3w^2, with lambda=2v, epsilon=v and delta=0. The native X allocation is C=32u^2vw. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 4 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: LowAFirst
For s>=2 and a=s+1 and b>=3s+1, choose u=2^(s-2), v=2^(b-3s-1), w=1. Then z=4u, x=8u, y=128u^3v, with lambda=8u^2v, epsilon=4u^2v and delta=1. The native X allocation is C=0. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 5 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: LowAMiddle
For s>=2 and s+2<=a<=2s and b>=3s+1, choose u=2^(a-s-2), v=2^(2s-a), w=2^(b-3s-1). Then z=4uv, x=16u^2v, y=128u^3v^3w, with lambda=4uv^2w, epsilon=2uv^2w and delta=1. The native X allocation is C=2u-1. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 6 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: LowALast
For s>=2 and a=2s+1 and b>=3s+1, choose u=2^(s-2), v=2^(b-3s-1), w=1. Then z=4u, x=32u^2, y=128u^3v, with lambda=2uv, epsilon=uv and delta=1. The native X allocation is C=4u-1. All natural gaps are nonnegative, and every chart variable is at least 1. Charts proves the complete eleven-slot coordinate identity and transports the native allocation to row 7 of Dyadic.
For each of the first three terminal seams, this module proves four inequalities: nonnegativity of the old doubled cumulative seam, its old successor-minus-one cap gap, the new doubled cumulative seam, and its new successor-minus-one cap gap. These are twelve exact inequalities for the actual head and mask polynomials, not numerical samples.
The proof shifts u=U+1,v=V+1,w=W+1 with U,V,W>=0. Each gate is identified by ring with its complete positive-coefficient Horner expression, whose nonnegativity follows by positivity. The expression literals do not introduce an external axiom. Charts consumes these bounds on this region; Physical and Schedule separately provide the occurrence inventory and all-prefix transport.
Original adaptive construction: Physical
The terminal order is W,U,X,V. Bank 1 consists of all U positives and W mask p, followed by the W terminal. Bank 2 consists of all V positives, W mask H XOR p and X mask C, followed by the U terminal. Bank 3 consists of W mask F XOR H, followed by the X terminal. Bank 4 consists of X mask E XOR C, followed by the V terminal.
Increasing set-bit decoding maps each mask to actual labels at its chain offset. The nested split of F into p, H XOR p and F XOR H partitions every W positive exactly once; the split of E into C and E XOR C does the same for X. Together with U,V and the four terminals, the concatenated word is a permutation of List.range k, not just a list with the correct total mass.
The paired bank sums use the same decoded subsets in both rows: (uA+pL, uB+(H-p)L+CM, (F-H)L, (E-C)M) and the identical coefficients on (2A,Bn,Ln,Mn). All bank entries are nonnegative in each row. The pre word includes banks 1 and 2 and their terminals; the post word includes banks 3 and 4. Its literal cut is pre.length, where the true fresh label is inserted before bank 3.
Original adaptive construction: Schedule
The twelve chart gates bound the cumulative old and new postterminal seams. The fourth seam is exactly zero. The packet Checks predicate combines these interfaces with nonnegative positive-bank entries and nonpositive actual terminals. The existing checks_strip theorem then controls every take-prefix within each bank as well as the terminal boundaries.
The old packets are the four physical banks with terminals W,U,X,V. The enlarged packets use the same inherited labels, and place the true fresh label k at the start of bank 3. Its doubled mass 2A is included in the third-bank calculation. Both strips are therefore proved for one literal physical word, rather than separately selected orders in the two rows.
The inventory bounds j=pre.length by k=a+b+2s and permits mapping inherited labels into Fin k. The marked-word identity identifies the enlarged word with earWord(k,sigma,j), preserving Fin.castSucc on every inherited occurrence. Finally the exact old zero total and enlarged zero total give both actual OriginalOrder conclusions, with all natural prefix lengths, including zero and lengths beyond the complete word. The premises remain the two upper clauses and s>=2.
Original adaptive seams, threshold and coefficient bounds
On the old two-clause union let lambda=2^(b-a-1), epsilon=0 when b=a+1 and lambda/2 otherwise. The W mask is p=y/(2z)+y/z^2-1-epsilon, with capacities H=y/z-1 and F=y/2-1. The stronger native X allocation is C=x/(2z)-delta, delta=1 when b>=3s+1 and 0 otherwise; E=x/2-1 is its full capacity. Natural exponent identities prove divisibility and all cast/subtraction bounds before any bit allocation. Under a>=s+1, 2lambda<=y/(2z) gives p>=0; z>=4 gives p<=H. Also 0<=C<=E. Only H,F,E must be all-ones masks. When delta=0, C itself can be a general submask of E. When a=s+1 and b>=3s+1, C=0 exactly; no X label or chain is removed.
The old inventory gives the cumulative factorization 2S1=(z-2)A+2Lp-N+M, 2T1=2(z-2)A+2Lnp-Q+Mn, 2S2=(z-2)(A+B)+2LH+2MC-2N+M+B, 2T2=(z-2)(2A+Bn)+2LnH+2Mn*C-2Q+Mn+Bn, 2S3=(2C+2)M-A-L and 2T3=(2C+2)Mn-A-Ln. These follow by source recurrences and literal inventory, including fresh A precisely from seam 3. In particular the second seam is independent of p. The late mask and early mask have different arithmetic jobs. Switching delta from 1 to 0 raises the third doubled seams by 2M and 2Mn while preserving the exact physical partition.
The original eight chart modules give 8 times 3 times 4 = 96 integer seam-gate inequalities, for all integer u,v,w>=1, not only the dyadic instantiations. Their shifted Horner expressions use U=u-1,V=v-1,W=w-1>=0; ring identification with the head/mask polynomials precedes positivity. The original exposition reports 6145 positive shifted coefficients; this coefficient count is attributed and has not been recounted here. Source expression literals are not an external truth axiom.
The fourth seams vanish by the eight recurrences and total native capacities. Within each bank, both source rows have nonnegative increments, with the fresh new increment A positive at bank 3. If a terminal has old successor R, its doubled magnitude is N-R and its post-terminal seam is at most (R-1)/2; thus the preceding bank peak is at most (N-1)/2. The analogous new bound is (Q-1)/2=N. The pinned checks_strip and lift_order proofs consume these gates for every natural prefix; exact zero totals also cover takes beyond the complete word. The final literal marked_word transport identifies the second physical word with earWord at the very same j.
Multiplication by 2 acts on residues modulo 2^k-1 and 2^(k+1)-1; the actual centered sections produce these arithmetic source rows. The eight recurrences link four physical chains in each action. Inserting k is a marked extension of the physical occurrence set, and its fresh A cancels the exact -A total of inherited new labels. The adaptive native mask is an integral allocation of these same orbit labels compatible with both strips. For delta=1 the critical lower seam has z*(2S3)=x(y+1)-xz^3-xz-z^3-z^2-2z; y>=2z^3,x>=2z imply it is at least z^2(2z-3)(z+1)>0. This explains the 3s+1 threshold independently of large a, while the complete gate proofs keep all other obligations.
The original strengthened threshold and wide ordinary constructions provide the adaptive allocation and exhaustive charts. PacketNormalForm.Source, FirstPeakSecondMaximum.Native, Chambers.Masks, SourceWidth, the existing Checks/strip bridge and marked-ear transport provide the reused physical source interfaces. For the fixed upper constructor, sigma is the label map of pre++post, j=pre.length, and the fresh label starts bank 3 with terminal order W,U,X,V. The present diagonal supplier instead uses W,X,U,V and paired exchanges; no identity of these constructors is claimed. EqualLastTwo lies in the opposite b<a region. A general group-action transport, unrestricted second-gap theorem and full J/C3.1 remain outside this application.