t200_values.py

back to table · edit · history · where entries came from · files · download

4391 bytes, as of the version from 2026-10-27 01:01 (current). Recorded here, not run.

"""Certified values at the T200 relevance selection, without API writes.

    pip install numberdb python-flint mpmath
    python generate.py

Download this file as t200_values.py beside generate.py. Arguments are
computed as Arb balls from their defining expressions, never rounded input
strings. The branch point and inverse-normalization values are exact by
W_k(y exp(y)) = y on the specified real branch. In particular the branch
point is not evaluated numerically on a ball crossing the real domain.

The 160 guard bits supplement the requested decimal precision. Checks reject
nonfinite or insufficiently narrow balls and verify the branch inequalities
and defining equation. Independent root brackets and mpmath comparisons are
implemented in t200_checks.py.
"""

import math
from contextlib import contextmanager
from fractions import Fraction

import numberdb
from flint import arb, ctx


GUARD_BITS = 160
SELECTION = {
    '0': ('0', '1', 'e', '-1/e', '-3*exp(-3)', '-5*exp(-5)'),
    '-1': ('-1/e', '-exp(-1/2)/2'),
}
LABELS = {
    'e': '$e$',
    '-1/e': '$-e^{-1}$',
    '-3*exp(-3)': '$-3e^{-3}$',
    '-5*exp(-5)': '$-5e^{-5}$',
    '-exp(-1/2)/2': '$-e^{-1/2}/2$',
}
EXACT = {('0', '0'): 0, ('0', 'e'): 1,
         ('0', '-1/e'): -1, ('-1', '-1/e'): -1}


@contextmanager
def precision(bits):
    previous = ctx.prec
    ctx.prec = bits
    try:
        yield
    finally:
        ctx.prec = previous


def endpoint(value):
    mantissa, exponent = value.man_exp()
    return Fraction(int(mantissa)) * Fraction(2) ** int(exponent)


def as_interval(value):
    if not value.is_finite():
        raise ArithmeticError('nonfinite ball')
    return numberdb.RealInterval(endpoint(value.lower()), endpoint(value.upper()))


def argument(identity):
    if identity in ('0', '1'):
        return arb(identity)
    if identity == 'e':
        return arb(1).exp()
    if identity == '-1/e':
        return -arb(-1).exp()
    if identity == '-3*exp(-3)':
        return -3 * arb(-3).exp()
    if identity == '-5*exp(-5)':
        return -5 * arb(-5).exp()
    if identity == '-exp(-1/2)/2':
        return -(arb(-1) / 2).exp() / 2
    raise ValueError('argument is outside the documented selection')


def compute(branch, identity, digits=100, extra_bits=0):
    if identity not in SELECTION.get(str(branch), ()):
        raise ValueError('branch/argument pair is outside the documented selection')
    key = (str(branch), identity)
    if key in EXACT:
        return EXACT[key]
    with precision(numberdb.bits(digits, losing=GUARD_BITS + extra_bits)):
        source = argument(identity)
        result = source.lambertw(int(branch))
        required = math.ceil((digits + 12) * math.log2(10))
        if not result.is_finite() or result.rel_accuracy_bits() < required:
            raise ArithmeticError('insufficient finite relative accuracy')
        if str(branch) == '0' and not result > -1:
            raise ArithmeticError('principal branch inequality failed')
        if str(branch) == '-1' and not result < -1:
            raise ArithmeticError('lower branch inequality failed')
        residual = result * result.exp() - source
        if not residual.is_finite() or not residual.contains(0):
            raise ArithmeticError('defining equation failed')
        if residual.abs_upper() > arb(10) ** (-(digits + 10)):
            raise ArithmeticError('uninformative defining-equation enclosure')
        return result


class LambertValues(numberdb.Generator):
    table = 'T200'
    parameters = ('branch', 'x')
    type = 'R'
    digits = 100
    rigour = 'proven'
    files = ('generate.py', 't200_values.py', 't200_checks.py',
             'checks-evidence.json', 'relevance-audit.json')

    def enumerate(self):
        for branch, identities in SELECTION.items():
            for identity in identities:
                yield {'branch': branch, 'x': identity}

    def value(self, params, digits):
        with precision(numberdb.bits(digits, losing=GUARD_BITS)):
            value = compute(params['branch'], params['x'], digits)
            result = {'number': as_interval(value) if isinstance(value, arb) else value}
            if params['x'] in LABELS:
                result['param-latex'] = LABELS[params['x']]
            if params == {'branch': '0', 'x': '1'}:
                result['comment'] = 'This is the omega constant.'
            return result