Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Uniform actual finite-head tails

Abstract

Uniform coefficient lower tails for the full arithmetic divided-difference column on nonempty finite integer heads.

Theorem 1.1 (A constant and cutoff uniform in every complex head coefficient vector).

Lean statement: D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_finite_head_uniform_tail_lower

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_finite_head_uniform_tail_lower (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural c with 2 <= c, every finite set S of integers, and a proof that S is nonempty, there exist a real C > 0 and a natural N0 such that, for every function v from integers to complex numbers and every natural N with N0 <= N, the following two assertions hold. The sequence indexed by natural j with value norm(couplingColumn(c,S,v,Int.ofNat(N+j+1)))^2 + norm(couplingColumn(c,S,v,-Int.ofNat(N+j+1)))^2 is summable. Its actual infinite sum is at least C times the finite sum of norm(v(n))^2 over n in S, divided by ((N : Real)+1)^(2*card(S)-1). C and N0 are quantified before v and N. The zero function, singleton heads, arbitrary complex coefficients, and c=2 are included.

The actual column is the sum over n in S of the complex cast of (arithmeticBoundarySymbol(c,n)-arithmeticBoundarySymbol(c,m))/(pi*((m : Real)-(n : Real))), multiplied by v(n). The boundary symbol retains the pole term, the entire infinite Gamma series and the finite prime sum. Let d=card(S) and choose A=max(1, the supremum of natAbs(n) over n in S). The nodal polynomials D, P and Q in ActualNodalCoercivity give pi*D(m)couplingColumn(c,S,v,m)=P(m)-arithmeticBoundarySymbol(c,m)Q(m) outside S, with both numerator degrees below d. Their uniform reconstruction constant is lambda=1/(d^2A^(2(d-1))).

Dilate P and Q by the positive integer scale N and split their coefficients into even and odd parts Pe, Po, Qe and Qo without reducing their degrees. Put gamma=pi/4, F1=Pe+gammaQo, F2=Po+gammaQe, B1=Qo and B2=Qe. For positive m, write p(m) for the actual finite prime symbol and delta(m)=m^2*smoothWeight(c,m)-gamma. The exact smooth split gives s(m)=-(gamma+p(m)+delta(m)), and the existing boundary reflection identity gives s(-m)=-s(m). At t=m/N the positive numerator is U1(t)+U2(t), and the negative numerator is U1(t)-U2(t), where Ui=Fi+(p(m)+delta(m))Bi. The parallelogram identity gives paired numerator energy 2(norm(U1)^2+norm(U2)^2).

For E=sum over r<d of N^(2r)(norm(P_r)^2+norm(Q_r)^2), the two F channel coefficient energies add to EP+gamma^2EQ and the two B channel energies add to EQ. Disjoint coefficient parities remove their cross terms. Since 0<gamma<1, gamma^2E <= EF <= E and EB <= E. No head coefficient, moment or parity condition is imposed.

The degree-only discrete sampling constant kappa is chosen before N and every polynomial. Let R=sum over r<d of 4^r and H=primeFirstMoment(c). Signed polynomial interference is controlled by Abel summation before taking its absolute value. The Gamma estimate chooses K before m with abs(delta(m))<=K/m. Finite Cauchy-Schwarz on t in [1,2] bounds evaluation energy by R times coefficient energy. For arbitrary real p and delta, retain the complete nonnegative square (p+delta)^2norm(B)^2 in the exact norm expansion. The sole smooth loss is at most abs(delta)(norm(F)^2+norm(B)^2), using 2abs(Re(Fconj(B)))<=norm(F)^2+norm(B)^2. This needs no pointwise bound on p. Summing the smooth error over the exactly N modes N<m<=2N costs at most KR*(EF+EB), hence at most 2KRE. Consequently the channel annulus energy is at least (kappagamma^2N-T)E, where T=R(4H+2*K).

Choose N0 beyond 1, 2A, 2d and 2T/(kappagamma^2). The channel annulus then has energy at least kappagamma^2NE/2. Both signs are outside S; their nonzero nodal denominators have norm at most (3N)^d. Combining this bound with the exact polynomial model, the factor two from the parallelogram identity and nodal reconstruction gives the positive witness C=kappagamma^2lambda/(pi^23^(2d)). The identity 2d=(2d-1)+1 cancels the positive scale factor N, including d=1. Monotonicity replaces N by N+1 in the final denominator.

ActualFullSymbolTail.paired_coupling_column_tail establishes summability at the internally verified head separation. Reindexing the annulus as j in range(N) and applying Summable.sum_le_tsum compares its nonnegative energy with this genuine infinite tail. The constant and cutoff depend only on the data chosen before the coefficient vector.

The mathematical ingredients are classical finite Lagrange interpolation and integer node separation, finite Cauchy-Schwarz, the parallelogram identity, discrete polynomial sampling, Abel summation for finite prime phases, and the positive Gamma integral comparison. This is an estimate for the defined arithmetic column. It asserts no physical Weil positivity, Fourier or physical operator identification, Robin inequality, or Riemann hypothesis result.

For every natural c>=3, finite integer head S, natural cutoff N and complex coefficient function v, the complete paired tail energy vanishes exactly when v vanishes on S. The empty head and zero vector are included.

ActualUniformFiniteHeadTail.actual_finite_head_uniform_tail_lower provides the coefficient-uniform lower bound for c>=2: positive C and a cutoff N0 are chosen before all coefficient functions and all later cutoffs. Its summability at N+N0, reindexing of both signed columns and Summable.comp_nat_add give summability at every N.

A retained nonzero coefficient gives strictly positive original coefficient mass. The uniform lower bound gives a positive complete tail at max(N,N0), and nonnegative tail cropping transfers positivity to N. This is a consequence of the uniform estimate; ActualThreeNodeSourceHeadBridge uses that consequence on the literal three-node head.

Theorem 1.2 (actual tail summable all).

Lean statement: D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_tail_summable_all

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_tail_summable_all (✓ std3). ∎

Source. Repository-derived.

Commentary.

lemma actual_tail_summable_all {c : ℕ} (hc : 3 ≤ c) (S : Finset ℤ) (hS : S.Nonempty) (N : ℕ) (v : ℤ → ℂ) : Summable (pairedColumnTerm c N S v)

Theorem 1.3 (actual finite head tail pos).

Lean statement: D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_finite_head_tail_pos

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_finite_head_tail_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

theorem actual_finite_head_tail_pos {c : ℕ} (hc : 3 ≤ c) (S : Finset ℤ) (N : ℕ) (v : ℤ → ℂ) (hv : ∃ k ∈ S, v k ≠ 0) : 0 < ∑’ j : ℕ, pairedColumnTerm c N S v j

Theorem 1.4 (actual finite head tail zero iff).

Lean statement: D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_finite_head_tail_zero_iff

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaBridge/ActualUniformFiniteHeadTail.actual_finite_head_tail_zero_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

theorem actual_finite_head_tail_zero_iff {c : ℕ} (hc : 3 ≤ c) (S : Finset ℤ) (N : ℕ) (v : ℤ → ℂ) : (∑’ j : ℕ, pairedColumnTerm c N S v j) = 0 ↔ ∀ k ∈ S, v k = 0

References