A fourth-order envelope for actual square-displacement counts
Abstract
The actual quotient return counts in the Bajnok-Beatty lattice setting have a fourth-order correction with a uniform finite remainder 2439/(8000p^6), even though the negative logarithmic displacement is unbounded in q.
Let p and q be signed integers with p>=5, q>=3, Odd p and Odd q. Neither integer is required to be prime: all odd composites are included, and there is no upper bound on q. The time t is a natural number satisfying ((q+1)/2).toNat<=t. Put m=2q(t as Integer)-1 and n=(p*m).toNat. The ambient plane is Fin 2 -> Integer.
The actual generators are v1a=![p*(m-1)/2,p*(m+1)/2], v2a=![p*(m-q^2)/2,-(p*(m+q^2)/2)], v1q=![p*(m-q)/2,p*(m+q)/2], and v2q=![p*(m-q)/2,-(p*(m+q)/2)]. All four divisions by 2 are integer divisions made exact by parity. Let Ka=Submodule.span Integer (Set.range ![v1a,v2a]) and Kq=Submodule.span Integer (Set.range ![v1q,v2q]); these are the complete integer spans, with no selection of a smaller sublattice. Their quotient maps are Fa=Ka.mkQ.toAddMonoidHom and Fq=Kq.mkQ.toAddMonoidHom. The pair square_return_pair p q t is exactly (W Fa n,W Fq n). Write this natural count pair as (Wa,Wq).
Theorem 1.1 (Uniform finite fourth-order control on the full signed domain).
Lean statement: D5/S3/FiniteGroups/BajnokBeattySquareDisplacementFourthEnvelope.actual_square_displacement_fourth_envelope
Proof. Machine-checked in Lean as D5/S3/FiniteGroups/BajnokBeattySquareDisplacementFourthEnvelope.actual_square_displacement_fourth_envelope (✓ std3). ∎
Source. Repository-derived.
Commentary.
Set P=(p as Real), Q=(q as Real), nReal=P*(2Q(t as Real)-1), s=(Q^2-1)P^2/(2(nReal+1)), and nu=Q^2. Define C=2*(nu+1)/(3*(nu-1)^2), E=4/(3*(nu-1)^2), and Bcoef=16*(nu^2+nu+1)/(15*(nu-1)^4). The uncorrected profile is G(s)=exp(s)+exp(-nus). Its second-order coefficient is H(s)=Cs^3*(exp(s)-nu^2exp(-nus)). The fourth-order coefficient is K(s)=-Es^3(exp(s)-nuexp(-nus))+Bcoefs^5(exp(s)-nu^3exp(-nus))+(C^2/2)s^6(exp(s)+nu^4exp(-nus)).
For every p,q,t in the stated domain, the additional band condition 2/3<=s<=5/7 implies |2*(Wa as Real)/(Wq as Real)-G(s)-H(s)/P^2-K(s)/P^4|<=2439/(8000*P^6). Since P>=5 and 2439/8000<1, this remainder is strictly smaller than 1/P^6. The theorem states the sharper bound alone. Its hypotheses contain no assumed count comparison, logarithmic expansion, remainder estimate, sign, or finite envelope.
The exact lattice classification supplies natural n,a,r with (n as Integer)=p*(2qt-1), n+p.toNat=2a, 2r=(q.toNat-1)*p.toNat, and a+(q.toNat+1)r<=n. It also supplies Wa=2(choose(n,a)+choose(n,a+(q.toNat+1)r)) and Wq=4choose(n,a+r). Thus nReal=(n as Real). With A=choose(n,a), B=choose(n,a+r), and D=choose(n,a+(q.toNat+1)*r), the actual ratio 2Wa/Wq is exactly (A+D)/B. The fit inequality gives B>0 before division. This classification is reused from ThresholdBracket.state_data and SingleCrossing.square_return_pair, rather than assumed.
Let R=nReal+1. The existing choose_ratio_centered_prod supplies the exact finite products A/B=product(i<r)((1+x_i)/(1-x_i)) and B/D=product(i<q.toNatr)((1+y_i)/(1-y_i)), where x_i=(P+2i+1)/R and y_i=(QP+2i+1)/R. On the band one has 0<=x_i<=15/(28P) and 0<=y_i<=45/(28P), so every factor and every logarithm argument is positive. Put Lx=log(A/B), Ly=log(B/D), and eps=P^(-2).
The existing AP sum_linear and sum_cubic identities supply the first and third moments. The additional generic fifth identity uses F5(x)=x^6-5x^4+7x^2: 12sum(i<r)(a+2i+1)^5=F5(a+2r)-F5(a). It follows by finite induction from F5(x+2)-F5(x)=12(x+1)^5. Applying this same identity to both blocks gives (2/5)sum(x_i^5)=Bcoefs^5eps^2-Us^5eps^3+Vs^5eps^4 and (2/5)sum(y_i^5)=nu^3Bcoefs^5eps^2-nu^2Us^5eps^3+nuVs^5eps^4, where U=16(nu+1)/(3*(nu-1)^4) and V=112/(15*(nu-1)^4).
The finite n=3 lower and upper log truncations retain 2z+(2/3)z^3+(2/5)z^5 and bound the remaining tail between zero and 2z^7/(1-z^2). For 0<=z<=k/P and P>=5, z^2<=k^2eps and eps<=1/25. Consequently this tail is at most [3k^4/(1-k^2/25)]eps^2((2/3)z^3). Summing and using the exact cubic moments yields nonnegative Tx,Ty with Tx<=[3(15/28)^4/(1-(15/28)^2/25)]axeps^3 and Ty<=[3*(45/28)^4/(1-(45/28)^2/25)]ayeps^3.
The full logarithmic expansions are Lx=s+axeps+bxeps^2+rx and Ly=nus+ayeps+byeps^2+ry, with ax=Cs^3, bx=Bcoefs^5-Es^3, ay=nu^2Cs^3, by=nu^3Bcoefs^5-nuEs^3, rx=-Us^5eps^3+Vs^5eps^4+Tx, and ry=-nu^2Us^5eps^3+nuVs^5eps^4+Ty. The first-moment log lower bound separately proves dx=Lx-s>=0 and dy=Ly-nu*s>=0; no sign is assumed for bx or by.
For nu>=9 the existing coefficient certificate gives C<=5/48, E<=1/48, and nu^2C<=(15/16)nu. The additional rational certificates give Bcoef<=91/3840, nu^2Bcoef<=2457/1280, U<=5/384, nuU<=15/128, and V<=7/3840. Clearing positive denominators reduces these to the factored positive polynomials (nu-9)(91nu^3+455nu^2+545nu+445), (nu-9)(3275z^3+84320z^2+725120z+2082816) with z=nu-9, (nu-9)(5nu^3+25nu^2+255nu+227), and (nu-9)(3nu+5)*(15nu^2+50nu-1), together with (nu-1)^4>=4096.
These finite certificates imply 0<=ax<=1/20, |bx|<=1/50, |rx|<=eps^3/50, 0<=ay<=(7/20)nu, |by|<=(2/5)nu, and |ry|<=8nueps^3. The residual numerical certificates are 1991705/133380352<1/50 and 71086166275/9074166528<8. In particular dx<=eps/10 and |dx-ax*eps|<=(13/625)eps^2, whereas dy<=(2/5)nueps and |dy-ayeps|<=(18/25)nueps^2.
The decisive analytic step treats every u>=0: |exp(-u)-1+u-u^2/2|<=u^3/6. For P3(u)=1-u+u^2/2-u^3/6, the derivative of P3(u)*exp(u) is -(u^3/6)*exp(u)<=0 on the nonnegative ray. Antitonicity therefore gives P3(u)<=exp(-u). Combining this with the existing global negative quadratic upper bound exp(-u)<=1-u+u^2/2 proves the absolute cubic inequality. Only the positive block uses a bounded displacement: dx<=eps/10<=1 permits the pinned finite Real.exp_bound’ with n=3 and quadratic_le_exp_of_nonneg.
Assuming dy<=1 would be false on the stated domain: its leading correction ayeps grows proportionally to nueps as q grows along band states with fixed p. The proof never uses that assumption. It obtains |exp(dx)-1-ax*eps-(bx+ax^2/2)*eps^2|<=(141/6250)eps^3 and |exp(-dy)-1+ayeps-(-by+ay^2/2)*eps^2|<=[8nu+(27/100)nu^2+(4/375)nu^3]*eps^3 from the global negative cubic bound and the exact finite logarithmic residuals.
The existing FourthCoefficient.quartic_tail gives nu^4exp(-2nu/3)<6561/400. For j=1,2,3, multiplying nu^jexp(-nus) by nu^(4-j)>=9^(4-j), and using s>=2/3, gives nu^jexp(-nu*s)<=9^j/400. This reuses one quartic certificate without repeating its exponential lower bound or derivative calculation. Together with exp(s)<=9/4, it bounds the weighted positive error by (1269/25000)*eps^3 and the weighted negative error by (50823/200000)*eps^3. Their sum is exactly (2439/8000)*eps^3.
Finally A/B=exp(s)exp(dx) and D/B=exp(-nus)*exp(-dy). Adding their degree-one and degree-two polynomials in eps reconstructs H(s)*eps and K(s)*eps^2 exactly. This is a finite statement about natural binomial coefficients and the complete quotient counts. The Bajnok-Beatty setting, lattice return classification, centered finite products, cubic moments, quadratic estimates, and Gaussian profile come from the repository priors. No literature novelty, refined threshold, interpolation, or equality claim is made.