Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Restricted halfpower source rigidity

Abstract

Remote actual source data force initial factors and exclude low 4/1 successors.

Work on the original physical Fin(k) with s(v)=centered(2^k-1,2^v*t), N=2^k-1 and Q=2^(k-2). Physical advance is the cyclic group action generated by finRotate(k). Sorting the actual inclusive LARGE offsets from x defines the existing sourceParent, sourceLength and sourceSeed. Put M=card(largeOffsets(t,x)), L_i=sourceLength(t,x,i), T_i=sourceSeed(t,x,i), z=T_0 and delta=b-z. The cut at M is the physical closing cut k. Repeated values never identify distinct labels.

Theorem 1.1 (Actual factors and every real 4/1 successor).

Lean statement: D5/S3/Combinatorics/Circle/HalfpowerSourceRigidity.restricted_source_rigidity

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

Source. Repository-derived.

Commentary.

Assume OriginalRowBounds.RowCore(k,t,2,a,b,p): k>=2, nonzero source, 0<a<=b, universal negative-magnitude and positive minima a,b, attainment of -a, maximal physical p and its actual OwnRow of length two. In addition b is attained, d is a physical minimum, x is positive LARGE, M>=8, sourceParent(t,x,1)=d, L_0=L_1=L_2=2, L_4=1, 10a<N, delta>0 and T_4<=2a-3. The RESTRICTED source hypotheses are L_6=L_7=1 (F=4 and g_src=2) and the ORIGINAL T_8>=2b+1. No upper bound T_8<=z, five-pair count, gcd or value injectivity is assumed. Even L_3<2 is unnecessary.

Then L_5=0 and L_3=1; 19N+2b+384<=256a; 16N+135<10240delta; 262160delta<=467N-9; 29077N+1<=262160z; and 640z<71N. For EVERY natural i with i+1<M, a positive actual parent at i, L_i=2 and L_(i+1)=0, the actual successor R=T_(i+2) obeys 3N+2b+384<=16R, N<5R and 2N+z+1<14R. These are integer inequalities with rational bounds cross-multiplied; no integer floor quotient is substituted. The universal statement permits i+2=M and therefore includes the real seam successor.

The physical proof uses cut_own_row, the strict increase of actual cuts, row_terminal, and the original centered positive/negative LARGE steps. For either parent sign, the actual next LARGE magnitude is 2^L_i*T_i, and its wrapped successor has magnitude N-2 times that magnitude. Hence T_(i+1)=N-2^(L_i+1)*T_i at every real row, including the last. The sign cases use actual source values, not freely chosen signs. Attained extrema identify T_1=b, so N=8z+b=8b+T_2. Every signed seed is at least a by the original minima.

OriginalRowBounds.computed_row_bounds gives every real length at most two. The row-eight guard and L_6=L_7=1 imply 16T_6>=3N+2b+1 and T_6>N/5. But 5T_4+15<N. The possibilities L_5=1 or 2 give T_6=16T_4-3N or 32T_4-7N and contradict these inequalities. Thus L_5=0, T_6=8T_4-N, 128T_4>=19N+2b+1 and 256a>=19N+2b+385. If L_3=0, the recurrence and T_2>=a imply 14a<=N-3, contradicting this lower bound. If L_3=2, then 9T_4=N-4096delta<N, contradicting 128T_4>=19N+2b+1. Therefore L_3=1.

Substitution now gives 9T_4=5N-2048delta, 9T_6=31N-16384delta and 9T_8=469N-262144delta. The hard T_4 upper bound and the original T_8 guard give exactly the stated delta and z bounds, retaining the integer +1. For any actual negative-4/positive-1 pair, its negative seed S is at least a by the actual negative minimum, while its literal recurrence is R=16S-N. The lower bound on a therefore forces 16R>=3N+2b+384, R>N/5 and R>(2N+z+1)/14. A low 4/1 branch admitted by weaker local envelopes is consequently absent under this stronger source conjunction.

This is restricted-source rigidity. F4, g2 and the original seed-eight guard remain hypotheses; they have not been established for every original initial source. Source-core examples occur at k=32,t=1909298013 and k=64,t=8200372526062080861, the latter with repeated 32-value blocks on distinct labels. They do not populate the full retained hardSH/FIRST-h2/TRAP/formerV/LOW/OPEN2222 executed history. An application keeps the original source, immutable prefix, physical spent labels and every historical assumption. No operation pays or restores an occurrence here. Neither 4/2 existence, viability, arbitrary survival nor full continuation follows.

The setting is Damasdi, Frankl, Pach and Palvolgyi, Monochromatic configurations on a circle, arXiv:2504.10687v2, Conjecture 3.1, DOI 10.5070/C6.68671. The argument combines attained global extrema and remote initial rows with the cyclic action on physical labels. The full circle conjecture remains open.

References