lawref.cert

Сертифицированные границы ln/exp и ячейка округления §259.2/§64.2 (errata E-0136, DECISION-0154).

Не приближение, а УДОСТОВЕРЕНИЕ: терм возвращает точный рациональный отрезок вместе с деривацией, которая его породила, и ворота доказательств ПЕРЕСЧИТЫВАЮТ отрезок по деривации, а не сверяют поля с полями. Значение Bounds неподделываемо: литералом и записью §37 оно не строится, поэтому проверять «а не написал ли автор границы руками» на исполнении не нужно.

Алгоритм закреплён prose §259.2 ДОСЛОВНО: байтовый контракт держится на границах, а не на способе их получить, и «до сходимости» разошлось бы у двух реализаций на первом же входе. Всё считается на int/Fraction — Decimal зависит от контекста и здесь запрещён.

Attributes

Name	Description
BOUNDS_SCALE_LIMIT	No description.
BOUNDS_SIZE_LIMIT	No description.
BOUNDS_TERM_LIMIT	No description.
Interval	No description.
PROFILES	No description.

Classes

Name	Description
Bounds	Замкнутый рациональный отрезок с деривацией (§259.2).
CertError	Отказ сертифицированных границ; code — машинный код issue.

Functions

Name	Description
bounds_add	No description.
bounds_const	Точная константа как вырожденный отрезок — вход композиции (§259.2).
bounds_div	Деление на отрезок, содержащий ноль, не имеет ни значения, ни «границ
bounds_mul	No description.
bounds_scale	Умножение на точный рациональный коэффициент; знак меняет концы местами.
bounds_sub	No description.
cos_bounds	No description.
exp_bounds	Сертифицированные границы экспоненты (§259.2).
lift_bounds	Подъём монотонного листа на отрезок: [f(a.lo).lower, f(a.hi).upper].
lift_trig	Подъём синуса и косинуса на отрезок — по липшицевости (§259.2, E-0152).
ln_bounds	Сертифицированные границы натурального логарифма (§259.2).
parse_fraction	<n>/<d> → Fraction; иначе громкий отказ (канон §35, E-0005).
pi_bounds	Сертифицированные границы π по тождеству Мэчина (§259.2, E-0152).
rederive	ПЕРЕСЧЁТ отрезка по его деривации (§259.2) — независимый проверяющий.
round_bounds	Округление ОТРЕЗКА до одного значения (§259.2) — либо громкий отказ.
rounding_support	Опора §62 отношения округления (§64.2).
sin_bounds	No description.
sqrt_bounds	Сертифицированные границы квадратного корня (§259.2, E-0152).
verify	Сверка объявленных границ с ПЕРЕСЧИТАННЫМИ (§259.2).

BOUNDS_SCALE_LIMITattributemodule attribute#

View source

BOUNDS_SCALE_LIMIT = 4096

BOUNDS_SIZE_LIMITattributemodule attribute#

View source

BOUNDS_SIZE_LIMIT = 1 << 20

BOUNDS_TERM_LIMITattributemodule attribute#

View source

BOUNDS_TERM_LIMIT = 4096

Intervalattributemodule attribute#

View source

Interval = tuple[Fraction, Fraction]

PROFILESattributemodule attribute#

View source

PROFILES: dict[str, int] = {'p8/0.1': 8, 'p16/0.1': 16, 'p32/0.1': 32}

Boundsclassdataclass#

View source

class Bounds(lower: Fraction, upper: Fraction, derivation: str)

Замкнутый рациональный отрезок с деривацией (§259.2).

derivationattributeinstance attribute#

View source

derivation: str

lowerattributeinstance attribute#

View source

lower: Fraction

upperattributeinstance attribute#

View source

upper: Fraction

CertErrorclass#

View source

class CertError(code: str, message: str)

Bases: Exception

Отказ сертифицированных границ; code — машинный код issue.

codeattributeinstance attribute#

View source

code = code

messageattributeinstance attribute#

View source

message = message

bounds_addfunction#

View source

def bounds_add(a: Bounds, b: Bounds) -> Bounds

bounds_constfunction#

View source

def bounds_const(value: Fraction) -> Bounds

Точная константа как вырожденный отрезок — вход композиции (§259.2).

bounds_divfunction#

View source

def bounds_div(a: Bounds, b: Bounds) -> Bounds

Деление на отрезок, содержащий ноль, не имеет ни значения, ни «границ пошире» — отказ называет отрезок делителя.

bounds_mulfunction#

View source

def bounds_mul(a: Bounds, b: Bounds) -> Bounds

bounds_scalefunction#

View source

def bounds_scale(b: Bounds, factor: Fraction) -> Bounds

Умножение на точный рациональный коэффициент; знак меняет концы местами.

bounds_subfunction#

View source

def bounds_sub(a: Bounds, b: Bounds) -> Bounds

cos_boundsfunction#

View source

def cos_bounds(x: Fraction, profile: str) -> Bounds

exp_boundsfunction#

View source

def exp_bounds(x: Fraction, profile: str) -> Bounds

Сертифицированные границы экспоненты (§259.2).

lift_boundsfunction#

View source

def lift_bounds(head: str, a: Bounds, profile: str) -> Bounds

Подъём монотонного листа на отрезок: [f(a.lo).lower, f(a.hi).upper].

Домен проверяется на нижнем конце самим листом (ln при a.lo <= 0, sqrt при a.lo < 0); ширина определяется аргументом, а не профилем.

lift_trigfunction#

View source

def lift_trig(head: str, a: Bounds, profile: str) -> Bounds

Подъём синуса и косинуса на отрезок — по липшицевости (§259.2, E-0152).

|sin x − sin y| <= |x − y|, поэтому лист в нижнем конце, расширенный на ширину аргумента в обе стороны, содержит значение на всём отрезке. Так переводятся градусы: sin(scale(pi(p), 30/180)).

ln_boundsfunction#

View source

def ln_bounds(x: Fraction, profile: str) -> Bounds

Сертифицированные границы натурального логарифма (§259.2).

parse_fractionfunction#

View source

def parse_fraction(text: str) -> Fraction

<n>/<d> → Fraction; иначе громкий отказ (канон §35, E-0005).

pi_boundsfunction#

View source

def pi_bounds(profile: str) -> Bounds

Сертифицированные границы π по тождеству Мэчина (§259.2, E-0152).

rederivefunction#

View source

def rederive(derivation: str) -> Bounds

ПЕРЕСЧЁТ отрезка по его деривации (§259.2) — независимый проверяющий.

Он не доверяет полям lower/upper вовсе: они в пересчёт не входят, а сверяются с его результатом вызывающим (from_literal_term). Порча границы, остатка, аргумента или профиля отвергается по построению — испорченное поле просто не совпадёт с пересчитанным.

round_boundsfunction#

View source

def round_bounds(bounds: Bounds, precision: int, mode: str, round_fraction) -> Fraction

Округление ОТРЕЗКА до одного значения (§259.2) — либо громкий отказ.

Отношение §64.2 отвечает на вопрос «эта ли ячейка», а норме нужен и ответ «какая»: без него балл, предписанный актом, нечем ВЫВЕСТИ — переменная результата не связана ни одним позитивным конъюнктом, и правило отвергается range restriction §190 (замер MELD 06.09.2026).

Догадки здесь нет по построению: значение возвращается ТОЛЬКО когда оба конца отрезка округляются в одно, и BOUNDS_INSUFFICIENT иначе. Молчаливый выбор одной из двух ячеек был бы ровно тем правдоподобным числом, ради отказа от которого заведены сертификаты.

rounding_supportfunction#

View source

def rounding_support(bounds: Bounds, value: int, precision: int, mode: str, round_fraction) -> tuple[bool, bool]

Опора §62 отношения округления (§64.2).

Решение принимается на КОНЦАХ отрезка: все семь режимов §50 монотонно неубывающие, поэтому round(lower) == round(upper) == value равносильно I ⊆ C, а value вне [round(lower), round(upper)] — I ∩ C = ∅. Второго определения режима не заводится: round_fraction — тот же код, которым считает round §50.

sin_boundsfunction#

View source

def sin_bounds(x: Fraction, profile: str) -> Bounds

sqrt_boundsfunction#

View source

def sqrt_bounds(x: Fraction, profile: str) -> Bounds

Сертифицированные границы квадратного корня (§259.2, E-0152).

Не ряд, а целочисленный корень на сетке профиля: s = ⌊√⌊x·G²⌋⌋ даёт (s/G)² <= x < ((s+1)/G)², ширина 1/G = 10^(-2P) меньше объявленной полуширины, и концы лежат на сетке — выравнивать нечего. Точный корень (x·G² целое и s² = x·G²) даёт вырожденный отрезок.

verifyfunction#

View source

def verify(lower: Fraction, upper: Fraction, derivation: str) -> Bounds

Сверка объявленных границ с ПЕРЕСЧИТАННЫМИ (§259.2).