# Definition, derivations and checks for T709

Instruction record: skill-manifest.json, archived from
agents/runs/20261110T211830Z-build-skills/manifest.json. Both valid bundles match:
d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab.
This is build evidence, not an independent scientific verdict.

## Exact convention

Báez-Duarte, math/0011254v1, §1.2 equation (1.19) defines the dual F_n as
sum_{k=1}^n [M(n/k)-M(n/(k+1))] rho(k/(nx)) - rho(1/(nx)).
We call it D_N to distinguish the untapered F_n in math/0202141v2 (1.1), which
math/0011254v1 calls S_n in (1.18). Here rho is ordinary fractional part,
M(y)=sum_{1<=m<=floor(y)} mu(m), with M(y)=0 for 0<=y<1 and mu(1)=1.
The table's single output is E_N=integral_0^infinity (chi(x)+D_N(x))² dx,
chi=1_(0,1); the positive integer N is the sole parameter. No square root,
weighted measure, minimization or branch choice is involved. Logs are natural.
The finite computation is every N=1,...,30, not the natural domain's boundary.

Put w_k=M(N/k)-M(N/(k+1))-delta_{k,1}. Grouping by k=floor(N/m) gives
sum k w_k=sum_{m<=N} mu(m) floor(N/m)-1=0, since the double sum is
sum_{r<=N} sum_{m|r} mu(m)=1. This proves D_N(x)=0 for x>1. The two coefficient
implementations use respectively cumulative Mertens sums and independently
trial-factored mu values grouped by floor(N/m). This is a mathematical identity,
not an inference from 30 checks.

## Generating quadratic form

For rho_a(x)={1/(ax)}, change variables t=1/(ax):
K(a,b)=A(a/b)/a, where A(lambda)=integral_0^infinity {t}{lambda t}/t² dt.
For a>=1, the target inner product is b(a)=(log(a)+1-gamma)/a.
Indeed the integral from 1/a to 1 contributes log(a), and the rest is 1-gamma.
Thus E_N=1+2 sum w_k b(N/k)+sum w_j w_k (j/N)A(k/j).
If G_jk=A(j/k)/j is the ordinary integer-dilation Gram matrix, the dual
entry equals (jk/N)G_jk by A(lambda)=lambda A(1/lambda).
All exact rational arguments and integer weights are enclosed before use.

BBLS, math/0306251v1 §4 defines
V(p,q)=sum_{m=1}^{q-1} {(mp)/q} cot(pi*m/q), with V(p,1)=0.
For coprime positive p,q, Proposition 89 gives
A(p/q)=[(1-p/q)log(p/q)+(1+p/q)(log(2pi)-gamma)]/2
       -pi[V(p,q)+V(q,p)]/(2q).
These signs and factors were checked in the source. generate.py evaluates this
finite formula in Arb real balls at 461 bits for 100 requested digits. Its
128-bit guard leaves a measured minimum of 446 relative accuracy bits;
maximum radius is below 2.35e-136. No stored sibling values are input.

## Independent whole-residual integration

Set t=1/(N*x) and P_N(t)=1+sum w_k {kt}. Exact cancellation makes this the
period-one step function 1-sum w_k floor(kt). For x<1, t>1/N and dx=dt/(N*t²).
Consequently E_N=(1/N) integral_{1/N}^infinity P_N(t)²/t² dt.
Split [0,1] at the exact rational points r/k for 1<=k<=N, 0<=r<=k.
On each open interval (l,r), P_N²=c² is a nonnegative exact integer. Merge
adjacent intervals only when their squared values coincide.
The finite interval [1/N,1] contributes c²(1/max(l,1/N)-1/r) when r>1/N.
Periodicity and the absolutely convergent digamma difference series give
sum_{m=1}^infinity integral_l^r c²/(m+u)² du
  =c²[psi(1+r)-psi(1+l)].
checks.py uses this formula at 720 bits for ALL 30 norms. It shares Arb with
the generator but shares neither cotangent sums, Gram assembly, target inner
products nor the coefficient implementation. Radii are below 9.43e-215.

For N=1,2,3,4,30, a second tail route avoids digamma. It directly integrates
m=1,...,15 using enclosed rational functions and logarithms, then expands
1/(m+u)²=sum_{h>=0} (-1)^h(h+1)u^h/m^(h+2) for m>=16, 0<=u<=1.
After h=125 the absolute error is at most B times
127/16^128 + 1/16^127, where B=max P_N² on [0,1]. This follows from the
pointwise alternating-series bound (127)*zeta(128,16) and the integral test.
All moments are exact rationals; Arb encloses the Hurwitz zeta values and adds
this explicit error. This is not a heuristic quadrature or precision comparison.
The reusable rational-kernel integration and series constants come from
integral_kernel.py, whose source ancestry is stated in its docstring.

## Small controls and scope

D_1=0, so E_1=1 exactly. For N=3,4, P_N² is 1 on (0,1/N) and
(1-1/N,1), and zero on the remaining part of the period. The preceding integral
then gives E_N=1+[psi(1/N)-psi(1-1/N)]/N. Digamma reflection yields
E_3=1-pi/(3sqrt(3)), E_4=1-pi/4. For N=2, w=(-2,1) gives
P_2=1-floor(2t) on (0,1), so P_2² is 1 on (0,1/2) and 0 on (1/2,1).
Its integral is [psi(3/2)-psi(1)]/2=1-log(2).

checks.py checks exact E_1, the three nonzero constants,
psi(1)=-gamma, psi(1/2)=-gamma-2log2, and an elementary rational-kernel integral.
It rejects an added 1e-80, a radius-one ball, NaN, omission of -rho_N and
omission of the dual Gram scale. All arithmetic types and all coefficient
cancellations are checked. Nonsquarefree endpoints remain in the selection.
No monotonicity, limit, RH conclusion or lower bound from T641 is asserted.
The integer and dual dilation spaces differ. Readback checks must establish
that each full stored last-place interval contains the generating and direct
integral enclosures, not merely that rounded midpoints agree.