First terminal: lower bounds and successor caps
Abstract
Four polynomial bounds for the first paired seams
Use t=2xR, z=2xtZ and y=2zlambda with integer x>=4 and R,Z,lambda>=1. With D=y(z+1)+1, A=xD+1, B=xt(y+1)+t+1, M=tyz+D and Mn=2M-D, the module proves nonnegativity of B+M-2A, 2B-2A+Mn-1, 2A-B-1 and 2A-2B. These are the first four gates in Algebra.
The doubled first old seam is S=B+M-2A and its terminal successor is M. The first and third gates give 0<=S<=M-1. The doubled first enlarged seam is T=2B-2A+Mn-1 and its successor is Mn. The second and fourth gates give 0<=T<=Mn-1. These are paired bounds for the same first physical bank and terminal, rather than separately chosen orders.
Each internal proof expands its gate after x=4+u, R=1+v, Z=1+w and lambda=1+q, proves the polynomial equality by ring normalization, and proves the resulting terms nonnegative from u,v,w,q>=0. Selection imports these private proofs, and Schedule identifies the seam expressions with actual source sums. The module does not by itself construct a permutation or close the unrestricted Circle problem.