back to table · edit · history · where entries came from · files · download
4292 bytes, as of the version from 2026-11-02 13:17 (current). Recorded here, not run.
# Numerical evidence for T677
The archived skill manifest is
`agents/runs/20261102T115856Z-build-skills/manifest.json` (attached as
`skill-manifest.json`). Both valid versions have SHA-256
`a2b28d9953264d7b0ca62663785c2952190c5be6d6d3597fd695d9a54d606278`.
The build and stored-value check ran with Python 3.12.3, SageMath 10.9 and
numberdb 0.1.10. `generate.py` uses 429-bit Arb arithmetic, returning balls
rather than floating-point centers or text. Its 96 extra bits are a working
margin; the accuracy claim comes from interval containment, not that margin.
The smallest reported Sage ball accuracy was 423 bits. Every stored decimal
has 100 significant digits and its corresponding interval of one unit in the
last place contains the entire generator enclosure.
For a least Gauss-map period of length l, the generator forms S, the weighted
sum over that period, and P, the product of the arguments. Since 0<P<1,
repetition gives B=S/(1-P). Exact polynomial transformations determine the
least period. All argument uncertainties are propagated through logarithms.
The independent checker does not use the cycle-sum identity to compute B.
It finds complete quotients 1/x_j=(sqrt(D)+h_j)/k_j by the separate exact
recurrence h_(j+1)=a_(j+1) k_j-h_j and
k_(j+1)=(D-h_(j+1)^2)/k_j. Its integer convergents have
p_-1=1, q_-1=0, p_0=0, q_0=1. At term j the weight is
|q_(j-1)x-p_(j-1)|, avoiding the generator's running product.
It sums 800 terms in 4096-bit balls. This precision accounts for subtraction
of large convergents; their uncertainty remains part of the enclosure.
To bound the remainder, if x_j<1/2 then x_j x_(j+1)<1/2. If x_j>1/2,
the next partial quotient is 1 and x_j x_(j+1)=1-x_j<1/2. Consequently the
weight in term j is at most 2^(-floor(j/2)). Each period has partial quotients
at most M<=9, so log(1/x_j)<log(M+1). Summing this geometric bound over
j>=800 gives 4 log(M+1) 2^-400. All summands are positive, so the independent
enclosure is the rounded partial-sum interval plus [0, tail bound].
Its width is less than 10^-118 for every row. The complete enclosure, not
merely its midpoint, is contained in the row's stored last-place interval.
Controls run before the full checker. Replacing the logarithms by 1 at
[0;overline(1)] and [0;overline(2)] gives the known sums 1/(1-x), which must
be strictly greater than 1; a checker returning zero fails. Restoring the
logarithms agrees with -log(x)/(1-x). The separate Programs implementation
uses products of 2-by-2 integer matrices to find each rotated periodic root;
it agrees with all 141 generated values. All nine fixed-point formulas and
B(1/phi)=phi^2 log(phi) pass.
The stored-value check independently recomputes all 141 sums, verifies their
containment in the actual database intervals, checks their exact radical
labels, and checks B(x)=log(1/x)+xB(T(x)) on all 141 stored intervals. The
residual intervals contain zero and have widths less than 10^-97. The
published regulator T131#5 supplies an external control for the golden input:
its written interval, divided by 1-1/phi, overlaps the stored Brjuno interval.
Both intervals have comparable 100-digit precision; this is not agreement
between unbounded or nonfinite enclosures. `verify(sample=None)` also reports
141/141 matched, no differing, missing or extra entries.
The exact enumeration independently agrees in two forms: primitive-polynomial
coefficient bounds and discriminant factorization. Both give 141 arguments,
40 discriminants and 45 complete cycles; each period and successor is checked.
`numerical-evidence.json` and `stored-evidence.json` include each polynomial,
least period, orbit identities, displayed decimal, independent interval and
tail bound. `additional-checks.json` records the Programs and fixed-point tests.
The generic audit reports one finding about numeric-parameter `param-latex`
labels. This is the canonical skill's explicit symbolic-real-argument
exception: `quad_A_B_mK` is an exact quadratic root identity, and its label
shows (-B+sqrt(D))/(2A), the argument itself. It never shows B(x). The real
parameter type is retained, and the value column is headed B(x). All 141
labels were checked against the generator on readback. `audit-assessment.md`
records why this finding is retained for independent critique.