Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Whole-suffix boundaries and a negative prefix pair

Abstract

Reconstruct an arbitrary mixed suffix at its actual LARGE boundaries, and exchange a compatible negative prefix occurrence and a native positive LARGE for the unused native pair.

Theorem 1.1 (Positive substitution across the entire mixed suffix).

Lean statement: D5/S3/Combinatorics/Circle/LargeBoundarySubstitution.actualSource_largeBoundary_substitution_full

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/LargeBoundarySubstitution.actualSource_largeBoundary_substitution_full (✓ std3). ∎

Source. Repository-derived.

Commentary.

Use the actual source f=s(k,t) on physical Fin k labels, with k>=3, Q=2^(k-2), N=2^k-1 and C=2Q-1. Legal means a Nodup physical word whose EVERY natural take, starting at zero, has mass in [0,C]. G counts unused LARGE labels, H is the sum of 3^abs(f) over used LARGE labels, U counts all unused labels, and J is the lexicographic objective (G,H,U). Equal numerical values do not identify physical occurrences.

Let W=A++[y]++B be Legal and let p be unused in ALL W. Suppose Q<=P=f(p)<R=f(y), delta=R-P<Q, and mass(W)>=delta. For EVERY actual decomposition B=B0++[i]++B1 with Q<=abs(f(i)), require OLD zero-start arrival mass(A++[y]++B0++[i])>=delta if f(i)<0, or OLD departure mass(A++[y]++B0)>=delta if f(i)>0. There may be arbitrarily many LARGE of either sign. No old SMALL prefix bound after shifting, supplied batch order, new Legal word or first-LARGE choice is assumed.

The private reconstruct_suffix derives BOTH shifted boundaries at every actual LARGE and invokes LargeSkeletonOrdering.exists_order_preserving_large once. At a negative LARGE, its old arrival >=delta and magnitude >=Q>delta put both shifted endpoints in [0,C]. At a positive LARGE, its old departure >=delta and magnitude >=Q give the same result. Old upper bounds survive subtraction. The shared generic theorem scans the whole suffix with the complete intervening SMALL batch, invokes the unchanged SmallStepOrdering.exists_order_between for each batch and the final batch, and retains every LARGE in physical order. Only that generic theorem performs the reconstruction induction. The adapter permits any nonnegative shift <Q, including zero.

The replacement height mass(A)+P=mass(A)+R-delta is legal. Assemble unchanged A, p and the reconstructed suffix Bprime. Export Bprime.Perm(B), equality of its LARGE filter with that of B as LISTS of physical labels, Legal, InStrip, EVERY natural zero-start take including zero and overlength, Nodup and Inventory(W,V,[p],[y]). The total physical permutation (V++[y]).Perm(W++[p]) supplies exact disjoint used and unused partitions, LARGE and total counts, source balance, SMALL balance and full-source complement through inventory_of_perm. In particular G and U and remainingSmall are unchanged, H(V)+3^R=H(W)+3^P, H and J strictly decrease, mass(V)=mass(W)-delta lies in [0,C], and remainingMass(V)=-(mass(W)-delta).

Theorem 1.2 (Exchange a compatible negative prefix and the native positive gate).

Lean statement: D5/S3/Combinatorics/Circle/LargeBoundarySubstitution.actualSource_negativePrefix_pair_exchange_full

Proof. Machine-checked in Lean as D5/S3/Combinatorics/Circle/LargeBoundarySubstitution.actualSource_negativePrefix_pair_exchange_full (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take the native two-step path n=rho(p), x=rho^2(p), f(p)=P>0, f(n)=-D and f(x)=r. The source hypotheses Q<=abs(f(n)) and N<3abs(f(p)) give Q<=D<P<r<=C, D=N-2P, r=4P-N=2P-D and d=P-D=r-P with 0<d<Q. Use the existing native_geometry, including its actual-source inequality 3^P+3^D<3^r. These scalar facts are derived, not independent replacements for the physical source path.

Let the ORIGINAL zero-start W=A0++[c]++K++[x]++B be Legal, with p and n unused in ALL W. Assume f(c)=-M and D<=M<=P. Thus c,n,p,x are all LARGE. Require K to be pairwise compatible: for every actual i,j in K with f(i)>0 and f(j)<0, f(i)-f(j)<=C. K is otherwise arbitrary and may contain LARGE of either sign, with no old order imposed on its new arrangement. Set e=P-M, so 0<=e<=d<Q. Assume endpoint mass(W)>=e. At EVERY actual LARGE in WHOLE B, require old negative arrival >=e or old positive departure >=e, exactly as in the first theorem with old prefix A0++[c]++K++[x].

Write a=mass(A0), u=a-M, q=u+mass(K). Old Legal supplies a in [0,C], u>=0, q>=0 and q+r<=C, and leaves the literal zero-start A0 legal. Replacing c by n has arrival a-D=u+M-D>=0 and <=a<=C. The desired K endpoint is (a-D)+mass(K)=q+M-D>=0. It is <=q+M-D+P=q+r-e<=C. Apply the unchanged exists_order_between to ALL K, its compatible opposite pairs and these two endpoints. This produces Kprime.Perm(K) with every internal new prefix legal, without translating any old K prefix. Appending p gives height q+M-D+P=q+r-e in [0,C].

Now invoke the SAME reconstruct_suffix on the WHOLE B, from old start q+r to new start q+r-e. Each actual negative LARGE has old departure at least Q>e and assumed arrival at least e; each positive LARGE has old arrival at least Q>e and assumed departure at least e. Both shifted endpoints are legal. Complete intervening SMALL batches, including the final batch, are ordered by the canonical ordering theorem. The assumed endpoint gives mass(W)-e>=0. This also applies when M=P and e=0; no strictly positive shift premise or duplicate tail reconstruction is introduced.

Output Kprime.Perm(K), Bprime.Perm(B), equality of the physical LARGE filters of Bprime and B, and V=A0++[n]++Kprime++[p]++Bprime. Assemble the literal A0, n, the constructed Kprime, p and repaired Bprime to get InStrip and every natural zero-start prefix. The physical permutation is (V++[c,x]).Perm(W++[n,p]). Distinct n,p follows from the native opposite signs; whole-W freshness separates both from every old label. Old Nodup separates the two returned occurrences c,x. No global source-value injectivity assumption is needed.

Apply the unchanged inventory_of_perm with I=[n,p] and R=[c,x], deriving V.Nodup and both exact disjoint physical partitions. All four exchanged labels are LARGE, hence G(V)=G(W), U(V)=U(W) and remainingSmall(V)=remainingSmall(W). Every old SMALL and every other physical occurrence is retained. Exact source balance gives mass(V)=mass(W)-e in [0,C] and remainingMass(V)=-(mass(W)-e). Exact energy balance is H(V)+3^M+3^r=H(W)+3^D+3^P. Since 3^P+3^D<3^r, H(V)<H(W), hence J(V)<J(W), including at M=P and e=0. Only B’s LARGE order is preserved. LARGE inside K can change order; there is no whole-V LARGE order assertion.

First-valley application at a genuine global minimum

Consider W=A++[x]++T0++[y]++T1++[zpen]++T2++[z]++E in the native positive orientation, with y,zpen,z negative LARGE and all T0,T1,T2,E SMALL. Assume whole-W unused p,n, the native geometry, B0=C-P<h=mass(W)<D, and genuine minimality of J over ALL original-zero Legal physical words. Minimality here ranges over all words, so it also excludes competitors that truncate the old suffix.

The arrival after zpen is >B0: otherwise cut at the literal prefix Fpen ending at zpen. Its remaining suffix T2++[z]++E has exactly one LARGE. FirstNegativeShiftExchange.actualSource_prefix_pair_truncation applies with F=Fpen, R=T2++[z]++E, cut mass(F)<=C-P and largeUsed(R)=1, yielding a Legal strict-J competitor with G smaller by one. Likewise a cut through z leaves only SMALL E, so largeUsed(E)=0 and the same theorem lowers G by two if that arrival is <=B0. Thus both actual last-two arrivals are >B0, independently of the parity or magnitude comparison of Y=-f(y). No arrival conditions have been added to the original configuration.

The source bounds give d<=B0, since r=P+d<=C. Hence h>B0>=d. If v, the actual arrival after y, were >=d, all three later negative LARGE arrivals would be >=d. Apply the first theorem with replaced gate x, replacement p and shift d. It retains every other LARGE and every SMALL, has equal G/U and strict H/J descent. Therefore v<d at the global minimum. This locates the first later negative LARGE using the independently derived last-two bands; the substitution theorem alone only forces SOME offending LARGE boundary. No first-used-LARGE selection is made for x inside the entire word.

More generally an actually consumed positive LARGE q with f(q)>P can be replaced by unused p when delta=f(q)-P=delta. At a genuine global minimum the first theorem then forces an actual later negative-LARGE arrival below delta or a positive-LARGE departure below delta. Locating this boundary relative to named later negatives needs their separate arrival bands; the mixed-suffix conclusion alone gives no such location.

Negative prefix and odd unused-parent applications

For any ACTUAL c in A, write the literal decomposition A=A0++[c]++K. If f(c)=-M with D<=M<=P and its actual suffix K is pairwise compatible, set e=P-M. If v>=e, the last-two bands >B0>=d>=e and h>B0>=e establish every whole-tail boundary and endpoint premise of the new theorem. The resulting strict-J competitor contradicts global minimality. Consequently v<e is necessary for every such compatible actual prefix occurrence. This is conditional prefix compatibility, not a claim that all prefixes have compatible suffixes. In particular a compatible occurrence with M=P is impossible at a minimum, because e=0 while v>=0.

In the odd unused-parent branch let Y=-f(y)>P be odd, beta=rho^(-1)(y) unused with odd L=f(beta), and let its actual parent gamma=rho^(-1)(beta) occur in A with f(gamma)=-M and D<L<M<P<Y. Put delta=Y-P>=1. The parent equations give M=(N+Y)/4 and e=P-M=(d-delta)/4. The failed triple-insertion gate is 2(v+d)>=Y+1, or v>=(Y+1)/2-d. These are the specific parent and gate premises for this application.

Native geometry also gives D>2d: 2d=N-3D<=Q-1=Q. Thus P=D+d>3d, so 2P>6d. The failed gate yields 4v>=2P+2delta+2-4d>d-delta=4e. Hence v>e. If the actual A-suffix K STRICTLY AFTER gamma were compatible, the preceding negative-prefix application would require v<e. It must therefore be incompatible: there are actual i,j in K with f(i)>0, f(j)<0 and f(i)-f(j)>C. An opposite SMALL pair has difference at most 2Q-2<C, so at least one witness is another LARGE strictly after gamma. In particular gamma cannot be the last LARGE of A. This identifies a necessary physical obstruction, without asserting availability of another exchange.

Combining the first-valley integer bound v<=d-1 with the same odd unused-parent failed gate gives Y<=4d-3. Since Y>=P+1, this gives P<=4d-4 and D<=3d-4. Consequently D>=3d-3, equivalently 11P<=4N+3, excludes this unused-parent branch. When the native parent-location alternative has already shown beta lies in A or is unused, exclusion forces beta into A. If the unused-parent branch survives, its actual grandparent in A, Y<=4d-3 and D<=3d-4 restrict the remaining strip further. These consequences require the stated native parent-location and failed-gate hypotheses; neither exchange theorem establishes them universally.

The separate literal prefix-energy claims max Z<=P, with the stated tie bound min Z<=D, require their own prefix construction. They are not supplied by either theorem here, nor is any Zlast<=D conclusion asserted without the applicable terminal substitution hypotheses. Full Circle C3.1 remains open: these conditional exchanges and minimality consequences do not establish universal favorable-path or resource availability, remove the actual incompatible prefix LARGE obstruction, or settle all remaining physical source configurations.

References