back to table · edit · history · where entries came from · files · download
6635 bytes, as of the version from 2026-11-11 00:55 (current). Recorded here, not run.
# T712 build evidence
The quantity is the squared sequence-space distance in the draft definition.
There are 58 selected rows: all N=2..30 for each of `all`, `squarefree`.
This report records builder checks; it is not an independent critic's verdict.
## Definition and formulas
Bagchi's paper supplies the weighted space, basis, distance and squarefree
variant (locators and PDF hashes in research.md and sources.json). On
(1/(m+1),1/m), rho_k-rho_1/k equals {m/k}; interval length is 1/[m(m+1)].
For any fixed finite set of denominators, these sequences are independent:
if their linear combination vanishes, consecutive differences give
sum alpha_k/k - sum_{k|m}alpha_k=0. At m=1 the first sum is zero; induction
m=2..N then gives alpha_m=0. Hence the Gram matrix is positive definite.
The target is outside each finite span because every basis vector vanishes
at every multiple of the common period. Thus every finite squared distance
is positive, irrespective of RH.
Summation by parts gives the exact finite target sum
H_M/k - H_floor(M/k)/k - {M/k}/(M+1). Its limit is log(k)/k.
The projection formula 1-b^T K^-1 b follows by completing the positive
quadratic form; the optimizer solves K alpha=b. Anchoring the fractional-part
functions gives K_ij=G_ij-G_i1/j-G_1j/i+G_11/(ij). BBLS Proposition 89 gives
the rational G entries via finite cotangent sums. Exact rational arguments are
converted into balls before transcendental evaluation. Nothing is rounded on
input, and the calculation has no infinite numerical series truncation.
The independent checker regroups the original infinite sequence sum modulo
L=lcm(i,j), using W_L(r)=[psi((r+1)/L)-psi(r/L)]/L. The weights follow from
1/[m(m+1)]=1/m-1/(m+1) and the convergent digamma difference series.
The checker uses complex Arb psi at positive rational arguments (whose
values are real) and real interval LDL^T elimination. It shares Sage/Arb and
the definition, but no autocorrelation formula, cotangent code or linear solver
with the generator. Every LDL pivot is certified positive.
## Actual offline checks
`offline.py` runs the existing agents/table-build/dry_run.py and check.py
without modification. All 58 native return values are RealBall, finite and
narrow; no disguised-exactness, prose or import findings. The dry-run block is
12.5 KB and the longest raw ball representation has 170 characters. Working
precision: 513 bits; minimum result accuracy: 461 bits; maximum result radius:
6.9947058e-142. All normal-equation residuals contain zero; both quadratic
forms of the error agree. The settled 100-digit strings, all Gram entries,
optimizer enclosures and dependency versions are in offline-results.json.
`independent_check.py` verified all 58 proposed stored intervals, all 435
symmetric Gram entries, 29 target inner products and 45 distinct optimizer
systems. Working precision: 640 bits; minimum result accuracy: 565 bits;
maximum distance radius: less than 5.51e-173; minimum LDL pivot is greater
than 0.0023676. No discrepancies. Each independent ball is wholly inside the
corresponding stored last-place interval, not merely overlapping it.
Control N=2 gives 1-log(2), K22=log(2)/4, b2=log(2)/2 and alpha2=2;
the empty-span control is 1. A 1e-6 perturbation, NaN and radius-2 ball are
rejected. Strict decreases at genuine enlargements, every squarefree plateau,
and the inter-support inequality were checked across the whole selection.
`relations_check.py` verifies, at 640 bits, all 29 constrained-correction
identities relative to a freshly computed unrestricted system. It recomputes
both constructive errors, proves exact zero-tail coefficient sums, checks
squarefree support for V_N, and verifies both comparison inequalities at every
endpoint. Its direct finite residual sums at (all,2), (all,10), (all,30),
(squarefree,30) use M=10000 and tail upper bound
(1+sum |alpha_k|)^2/(M+1). These are coarse normalization controls, not a claim
of 100-digit accuracy from truncating at M. The relation checks share the
kernel with the generator; only the periodic checker supplies independent
full-precision numerical evidence.
The two initial probe/check failures were API/import matters, not discrepant
numbers: real Arb lacks `.digamma()` (complex `.psi()` works); matrix
construction needs the named Laurent ring initialization; radius comparisons
need coercion back to the ball parent; Möbius is `sage.arith.misc.moebius`,
not an Integer method in this runtime. Failed logs are retained. No guess was
uploaded in response to these failures.
## Reproduction and checkpoints
Install SageMath 10.9 and numberdb 0.1.10 (actual builder versions in
`offline-results.json`). Run:
sage -python generate.py
sage -python independent_check.py stored-input.json > check.log
sage -python relations_check.py > relations.log
The generator's default is read-only `verify(sample=None)`; a private draft
requires its author's configured key. `--publish` is an explicit additive
entry upload, distinct from offering/publishing a table. Session attribution
is supplied from the environment, never embedded in the generator.
Save CHECKPOINT_JSON lines from the independent log as a JSON list named
periodic-checkpoint.json. Passing that file alongside the checker resumes
completed Gram pairs; the exact precision and method identifier are checked.
All expensive components have durable checkpoints and SHA-256 inventories.
The controller's critic must independently assess the final live revision;
no mathematical or argument-selection verdict is supplied by this builder.
Instruction archive: ../20261111T001542Z-build-skills/manifest.json, also
attached as skill-manifest.json; SHA-256
c5ee30e128246f511fb7c0e8e37f8b7d2419d5fad25227688a6111fdf9686049.
All local/live resource hashes were checked and match, bundle SHA-256
d6661c2f21613524889fa3a57d3c95f8330344ca62e5a856211c08a282b7dbab.
## Stored-value verification
After API readback, the native generator's `verify(sample=None)` reported
58/58 matched, zero differing, missing or extra entries. The unchanged
independent numerical method was applied to stored-input.json, reusing the
saved periodic Gram checkpoint and resolving the systems. All 58 independent
balls are contained in the intervals actually stored. Results and controls
are in check-results.json; input hashes bind them to stored-input.json.
The self-contained Sage program shown on the page was also executed and
returns the squarefree N=10 value. The generator's installation command was
made explicit after the audit; this docstring-only change was followed by
the full native-generator verification just described.