back to table · edit · history · where entries came from · files · download
6690 bytes, as of the version from 2026-10-27 01:03 (current). Recorded here, not run.
"""Independent checks for remaining-values generators, without API writes.
pip install numberdb python-flint mpmath
python checks.py T206 --document table.json
Without --document, read the current website document using numberdb.
Delay models are also checked against archived, separately implemented Sage
generators by sage_controls.py; those run results are in checks-evidence.json.
"""
import argparse
import importlib.metadata
import json
from decimal import Decimal
from fractions import Fraction
from pathlib import Path
import mpmath as mp
import numberdb
from flint import arb
from remaining_values import (GUARD_BITS, PARAMETER, RemainingValues, as_ball,
as_interval, compute, dawson, dawson_root, precision)
def written_bounds(text):
text = str(text)
if '/' in text or ('.' not in text and 'e' not in text.lower()):
exact = Fraction(text)
return exact, exact
center = Fraction(Decimal(text))
unit = Fraction(10) ** Decimal(text).as_tuple().exponent
return center - unit, center + unit
def mp_fraction(value):
return mp.mpf(value.numerator) / value.denominator
def mp_value(tid, params):
identity = params[PARAMETER[tid]]
if identity == 'dawson-critical-1':
argument = mp.findroot(lambda point: 1 - mp.sqrt(mp.pi) * point *
mp.exp(-point ** 2) * mp.erfi(point), (mp.mpf('.9'), 1))
else:
argument = mp_fraction(Fraction(identity))
if tid == 'T188':
return mp.ei(argument) if params['normalisation'] == 'Ei' else mp.e1(argument)
if tid == 'T191':
return mp.li(argument)
if tid == 'T194':
return mp.quad(lambda point: mp.sinh(point) / point if point else 1, [0, argument])
if tid == 'T195':
return mp.euler + mp.log(argument) + mp.quad(
lambda point: (mp.cosh(point) - 1) / point if point else 0, [0, argument])
if tid in ('T205', 'T206'):
integral = mp.quad(lambda point: mp.exp(point ** 2), [0, argument])
return 2 * integral / mp.sqrt(mp.pi) if tid == 'T205' else mp.exp(-argument ** 2) * integral
if tid == 'T423':
return (0 if argument == 1 else
-mp.lambertw(-mp.exp(-1 / argument) / argument, -1) - 1 / argument)
if tid == 'T433' and argument <= 3:
return (mp.mpf(1) if argument == 1 else 1 - mp.log(argument) +
(mp.quad(lambda point: mp.log(point - 1) / point, [2, argument])
if argument > 2 else 0))
if tid == 'T434' and argument <= 3:
return (1 if argument <= 2 else 1 + mp.log(argument - 1)) / argument
if tid == 'T422' and argument <= 5:
return 2 * mp.exp(mp.euler) / argument * (1 + (
mp.quad(lambda point: mp.log(point - 2) / (point - 1), [3, argument])
if argument > 3 else 0))
return None
def leaf(numbers, params):
value = numbers
for identity in params.values():
value = value[str(identity)]
return value
def verify_document(tid, document):
records = []
generator = RemainingValues(tid)
for params in generator.enumerate():
entry = leaf(document['Numbers'], params)
written = entry['number'] if isinstance(entry, dict) else entry
lower, upper = written_bounds(written)
with precision(numberdb.bits(130, losing=GUARD_BITS)):
result = compute(tid, params)
interval = as_interval(result) if isinstance(result, arb) else numberdb.RealInterval(result, result)
if not lower <= interval.lower <= interval.upper <= upper:
raise ArithmeticError(tid + ': enclosure outside retained/new decimal: ' + str(params))
extra = compute(tid, params, 130, extra_bits=80, degree=420)
extra_interval = (as_interval(extra) if isinstance(extra, arb)
else numberdb.RealInterval(extra, extra))
if not lower <= extra_interval.lower <= extra_interval.upper <= upper:
raise ArithmeticError('higher-order enclosure outside stored decimal')
accuracy = result.rel_accuracy_bits() if isinstance(result, arb) else None
independent = []
for digits in (150, 200):
with mp.workdps(digits):
reference = mp_value(tid, params)
if reference is not None:
if not mp.isfinite(reference) or not mp_fraction(lower) <= reference <= mp_fraction(upper):
raise ArithmeticError(tid + ': mpmath mismatch: ' + str(params))
independent.append(digits)
records.append({'params': params, 'written': written,
'enclosure_contained_in_written_interval': True,
'arb_relative_accuracy_bits': accuracy,
'higher_precision_order_check': True,
'independent_mpmath_precisions': independent})
evidence = {'table': tid, 'digits': 100, 'records': records,
'working_bits': numberdb.bits(100, losing=GUARD_BITS),
'delay_degree': 320, 'second_delay_degree': 420,
'versions': {name: importlib.metadata.version(name)
for name in ('python-flint', 'mpmath')}}
if tid == 'T206':
with precision(numberdb.bits(100, losing=GUARD_BITS)):
root, left, right = dawson_root(100, numberdb.bits(100, losing=GUARD_BITS))
if not (1 - 2 * as_ball(left) * dawson(as_ball(left)) > 0 and
1 - 2 * as_ball(right) * dawson(as_ball(right)) < 0):
raise ArithmeticError('Dawson bracket failed')
if not (dawson(root) - 1 / (2 * root)).contains(0):
raise ArithmeticError('Dawson extremal-height identity failed')
evidence['critical_argument'] = {
'left_exact': str(left), 'right_exact': str(right),
'bracket_width': str(right - left),
'strict_endpoint_signs': [1, -1],
'root_uncertainty_propagated': True,
'uniqueness': 'F is positive for x>0 and F"=-2F at every stationary point; every crossing is downward, so the bracketed positive stationary point is unique.'}
return evidence
if __name__ == '__main__':
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument('table')
parser.add_argument('--document', type=Path)
arguments = parser.parse_args()
document = (json.loads(arguments.document.read_text()) if arguments.document
else numberdb.table(arguments.table))
print(json.dumps(verify_document(arguments.table, document), indent=2))