Every natural 2<=a<c<b with c=d
Abstract
Second peak, equal-tail: complete dyadic-mask joint lift
Theorem 1.1 (One original permutation and one literal fresh insertion).
Lean statement: D5/S3/Combinatorics/Circle/FourNegative/SecondPeakEqualTail/Endpoint.actualSource_second_peak_equal_tail_joint_lift
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/FourNegative/SecondPeakEqualTail/Endpoint.actualSource_second_peak_equal_tail_joint_lift (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every natural a,b,c with 2<=a<c<b and the original equal tail c=d, put k=a+b+c+c and A=1+2^a+2^(a+b)+2^(a+b+c). The theorem supplies a permutation sigma of every original Fin k label and a cut j<=k. Both OriginalOrder(k,A,sigma) and OriginalOrder(k+1,2A,earWord(k,sigma,j)) hold with the unchanged actualSource family.
The selector is unbounded in r=c-a and t=b-c-1. It chooses alpha,m0,v,j0 and an early Boolean branch from six polynomially certified windows. The physical masks use T_s(m)=s(m+1)-1, preserve sparse submask containment and partition every W bank, including the sole small tuple (a,c,b)=(2,3,4).
Both original orders retain every physical occurrence exactly once. The fresh label is inserted literally in either of the two selector modes; no source relabeling, rotation or finite feasibility assumption is used. The endpoint also records every natural repeated prefix and take, including zero repetitions and overlong prefixes, together with separate zero totals for the old and fresh words.
The proof reuses PacketNormalForm source values, terminal masses and zero-period transport. The old bound is modulus(k)/2 and the new bound is modulus(k); the identity modulus(k+1)/2=modulus(k) transfers the new repeated-prefix result. This is the complete second-peak equal-tail face and leaves the unchanged wholeCircle J/C3.1 objective open.
Original ceiling application: source and verification scope
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.
For the original lower cone assume s>=2, 2<=a, a+1<=s and 2s+1<=b. The current existence supplier has parameters (a,b,c)=(a,b,s), hence 2<=a<c<b, and uses the same original seed A, length k and literal earWord as the five-binder union described in SecondPeakSecondMaximum/Endpoint. The notation in this section is local to the original ceiling construction: x=2^a,y=2^b,z=2^s,D=y(z+1)+1,N=xyz^2-1,Q=2N+1; A=xD+1,B=xz(y+1)+z+1,L=xz^2+z^2+z+1,M=yz^2+D,Bn=2B-1,Ln=2L-z-1,Mn=2M-D. The physical chain offsets are 0,s,2s,2s+b with lengths s,s,b,a. The eight source recurrences and terminal formulas are those in the original adaptive source section; the old total is zero and the new inherited total -A is canceled by fresh A.
Original ceiling construction: LowerPolynomial
Write x=4+u, z=2x+v and y=2z^2+w for nonnegative integers u,v,w. With the source heads A,B,L,M and enlarged Bn,Ln,Mn, the thirteen polynomials are B+M-2A; 2A-B-1; Bn+Mn-4A; 4A-Bn-1; 2B-A-L; A-B-L; L(2Bn-3A-Ln)+Az^2; L(3A-Bn-1-Ln)-Az^2; A-2L; Az^2; L(A-1-2Ln)-Az^2; M-L; and L(y-3)-M+1.
Each polynomial is strictly positive throughout this coordinate orthant. The source contains the complete positive coefficient expressions: ring proves their equality to the defining head polynomial, then positivity uses u,v,w>=0. The boundary w=0 is included. Supplied integer coefficients are expression literals; their external generation is not used as a proof assumption.
The first eleven inequalities feed the lower seam bounds, while M-L>0 makes the ceiling numerator positive and L(y-3)-M+1>0 supplies its capacity bound. Actual dyadic parameters are connected to this orthant by LowerCeiling. These thirteen expressions are distinct from the ninety-six upper-chart seam gates.
Original ceiling construction: LowerCeiling
Assume 2<=a, a+1<=s and 2s+1<=b. The natural differences u=2^a-4, v=2^s-22^a and w=2^b-22^s*2^s are nonnegative, and their safe casts give x=4+u,z=2x+v,y=2z^2+w. Equality b=2s+1 gives w=0, so the polynomial estimates include this boundary without another hypothesis.
The actual mask is C=ceil((M-L)/(2L)), implemented by (M-L+2L-1).toNat/(2L).toNat. Positivity of M-L and L justifies the conversions. Natural quotient-remainder arithmetic gives M-L<=2LC<=M+L-1; the capacity polynomial L(y-3)-M+1>0 then proves C<=F=2^(b-1)-1.
Only F is an all-ones mask. The arbitrary submask C and F XOR C are bounded by the positive W capacity, and F XOR C=F-C both naturally and after casting to integers. These exact bit facts feed the lower physical partition; no upper-cone condition a>=s+1 or adaptive X allocation is imposed.
Original ceiling construction: LowerSeams
The lower allocation rows in chain order U,V,W,X are (u,0,0,0), (0,0,C,E), (0,u,0,0), (0,0,F-C,0), where u=z/2-1 and E=x/2-1. Terminal order remains W,U,X,V. The complement F-C appears only in bank 4. The individual doubled old increments are d1=B+M-2A, d2=A+B-2M+2CL and d3=L-2B+A. The enlarged increments are e1=Bn+Mn-4A, e2=A+Bn-2Mn+2CLn and e3=Ln-2Bn+3A; e3 includes the fresh 2A.
The cumulative doubled seams are D1=d1, D2=2B-A-M+2CL, D3=(2C+1)L-M and E1=e1, E2=2Bn-3A-Mn+2CLn, E3=(2C+1)Ln-Mn. The source recurrences prove both the local identities and their cumulative sums. The final bank makes both fourth seams exactly zero.
The identity MLn-MnL=Az^2 transfers the ceiling bounds M-L<=2LC<=M+L-1 to the enlarged row. Together with the thirteen positive polynomials it gives all twelve gates, with old/new caps (M-1,Mn-1), (B-1,Bn-1) and (A-1,A-1). The rounding residual M-2CL lies between L-A+1 and L and may be negative; the proof does not assume a positive residual.
Original ceiling construction: LowerPhysical
For 2<=a=2s+1, use the native ceiling C and capacity F from LowerCeiling. Bank 1 is all U positives followed by W terminal. Bank 2 is all X positives and W mask C, followed by U terminal. Bank 3 is all V positives followed by X terminal. Bank 4 is W mask F XOR C followed by V terminal.
The exact split C together with F XOR C partitions all W positive occurrences. Complete positive chains and the four terminals account for every other occurrence. The resulting concatenation is a permutation of List.range k with actual chain-offset labels. In both centered rows every bank entry is nonnegative.
The old positive bank masses are (uA, EM+CL, uB, (F-C)L), and the enlarged masses use the same coefficients on (2A,Mn,Bn,Ln). The pre word comprises the first two banks and terminals; post comprises the last two. Its length determines the literal insertion cut. No W complement is moved to bank 3, so the physical inventory matches the lower seam allocation exactly.
Original ceiling construction: LowerSchedule
Under s>=2, 2<=a, a+1<=s and 2s+1<=b, the lower cumulative gates satisfy the packet Checks conditions. Nonnegative positive banks and actual nonpositive terminals let checks_strip bound every natural prefix. The enlarged packets retain the same four banks and put the true fresh label k at the start of bank 3, including its contribution in the corresponding peak and seam.
The physical inventory makes lowerPre++lowerPost a permutation of all old labels. Mapping to Fin k produces sigma, and j=lowerPre.length is at most k. The marked-word identity turns insertion after the first two terminals into exactly earWord(k,sigma,j), with the same inherited Fin.castSucc occurrences.
The source equalities identify both strips with the actual centered residue rows for amplitude A and 2A. The old total is zero, and the enlarged inherited total -A is canceled by the fresh value A. The resulting two OriginalOrder conclusions retain physical permutations, both zero totals and all natural take-prefixes. This construction closes only the third cone used by Endpoint; the unrestricted Circle J problem remains open.
Original ceiling derivation, bounds and limits
For arbitrary integers t,d>=1 the original rounding helper defines ceilMask(t,d)=(t+d-1).toNat/d.toNat and establishes t<=d*ceilMask(t,d)<=t+d-1. Applying it with t=M-L and d=2L gives the stated lowerC. The bounds are derived before masks are decoded; a numeric mass alone cannot replace the physical W subset.
The original LowerPolynomial expressions assert strict positivity for all integers u,v,w>=0, including w=0, not merely for powers of two. The original exposition reports 373 positive coefficient literals, degree caps (7,5,1) and an integer identity difference-coefficient l1 bound 82850052<2^128. These are attributed original expression/diagnostic bounds, not a current recount, scoped verification of the original proof closure, or an assumption of the current supplier theorem.
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.
The original LowerSeams identity Delta=MLn-MnL=A*z^2 transfers rounding to the same enlarged physical row; separate marginal optima do not supply these joint seams. The signed residual L-A+1<=M-2CL<=L may be negative. Fresh doubled mass 2A enters the third local increment, the two fourth seams vanish, and the exact inventory and marked_word map give both original orders with the very same sigma and j. The coefficient expressions and their ring/positivity strategy describe the original method; its current proof-closure verification remains unestablished.
Attribution: the original lower-a ceiling construction supplies the rounding choice, orthant inequalities and fixed W,U,X,V bank word. The reused APIs are PacketNormalForm.Source, FirstPeakSecondMaximum.Native, Chambers.Masks, SourceWidth, Checks/checks_strip, lift_order and marked_word. The current SecondPeakEqualTail supplier chooses sparse masks by selector/dilation, terminal order W,X,U,V and its two cut modes. Its existential witnesses are not asserted equal to lowerC or lowerPre.length. The original ceiling method covers 2<=a=2s+1; its own b<2s+1 region and other complementary regions remain outside these method claims. The current supplier separately covers the complete equal-tail face 2<=a<s<b. No literature novelty, general group-action transport or unrestricted J/C3.1 is asserted.