# lawref.cert

*module*

Сертифицированные границы ln/exp и ячейка округления [§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)/[§64.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#642-отношение-округления-над-сертифицированными-границами-errata-e-0136)
(errata E-0136, DECISION-0154).

Не приближение, а УДОСТОВЕРЕНИЕ: терм возвращает точный рациональный отрезок
вместе с деривацией, которая его породила, и ворота доказательств
ПЕРЕСЧИТЫВАЮТ отрезок по деривации, а не сверяют поля с полями. Значение
`Bounds` неподделываемо: литералом и записью [§37](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#37-value-records) оно не строится, поэтому
проверять «а не написал ли автор границы руками» на исполнении не нужно.

Алгоритм закреплён prose [§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154) ДОСЛОВНО: байтовый контракт держится на
границах, а не на способе их получить, и «до сходимости» разошлось бы у двух
реализаций на первом же входе. Всё считается на `int`/`Fraction` — `Decimal`
зависит от контекста и здесь запрещён.

## lawref.cert.BOUNDS_SCALE_LIMIT

*attribute* · *module attribute*

```python
BOUNDS_SCALE_LIMIT = 4096
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L46-L46)

## lawref.cert.BOUNDS_SIZE_LIMIT

*attribute* · *module attribute*

```python
BOUNDS_SIZE_LIMIT = 1 << 20
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L52-L52)

## lawref.cert.BOUNDS_TERM_LIMIT

*attribute* · *module attribute*

```python
BOUNDS_TERM_LIMIT = 4096
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L48-L48)

## lawref.cert.Interval

*attribute* · *module attribute*

```python
Interval = tuple[Fraction, Fraction]
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L313-L313)

## lawref.cert.PROFILES

*attribute* · *module attribute*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L36-L36)

## lawref.cert.Bounds

*class* · *dataclass*

```python
class Bounds
```

Замкнутый рациональный отрезок с деривацией ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L55-L61)

### lawref.cert.Bounds.derivation

*attribute* · *instance attribute*

```python
derivation: str
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L61-L61)

### lawref.cert.Bounds.lower

*attribute* · *instance attribute*

```python
lower: Fraction
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L59-L59)

### lawref.cert.Bounds.upper

*attribute* · *instance attribute*

```python
upper: Fraction
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L60-L60)

## lawref.cert.CertError

*class*

```python
class CertError(Exception)
```

Bases: `Exception`

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L23-L29)

### lawref.cert.CertError.code

*attribute* · *instance attribute*

```python
code = code
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L28-L28)

### lawref.cert.CertError.message

*attribute* · *instance attribute*

```python
message = message
```

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L29-L29)

## lawref.cert.bounds_add

*function*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L218-L220)

## lawref.cert.bounds_const

*function*

```python
def bounds_const(value: Fraction) -> Bounds
```

Точная константа как вырожденный отрезок — вход композиции ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L213-L215)

## lawref.cert.bounds_div

*function*

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

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L394-L403)

## lawref.cert.bounds_mul

*function*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L389-L391)

## lawref.cert.bounds_scale

*function*

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

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L228-L233)

## lawref.cert.bounds_sub

*function*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L223-L225)

## lawref.cert.cos_bounds

*function*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L385-L386)

## lawref.cert.exp_bounds

*function*

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

Сертифицированные границы экспоненты ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L158-L210)

## lawref.cert.lift_bounds

*function*

```python
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`); ширина определяется аргументом, а не профилем.

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L422-L431)

## lawref.cert.lift_trig

*function*

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

Подъём синуса и косинуса на отрезок — по липшицевости ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154), E-0152).

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L409-L419)

## lawref.cert.ln_bounds

*function*

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

Сертифицированные границы натурального логарифма ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L115-L155)

## lawref.cert.parse_fraction

*function*

```python
def parse_fraction(text: str) -> Fraction
```

`<n>/<d>` → `Fraction`; иначе громкий отказ (канон [§35](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#35-встроенные-типы-данных), E-0005).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L444-L460)

## lawref.cert.pi_bounds

*function*

```python
def pi_bounds(profile: str) -> Bounds
```

Сертифицированные границы π по тождеству Мэчина ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154), E-0152).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L302-L310)

## lawref.cert.rederive

*function*

```python
def rederive(derivation: str) -> Bounds
```

ПЕРЕСЧЁТ отрезка по его деривации ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)) — независимый проверяющий.

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L480-L529)

## lawref.cert.round_bounds

*function*

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

Округление ОТРЕЗКА до одного значения ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)) — либо громкий отказ.

Отношение [§64.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#642-отношение-округления-над-сертифицированными-границами-errata-e-0136) отвечает на вопрос «эта ли ячейка», а норме нужен и ответ
«какая»: без него балл, предписанный актом, нечем ВЫВЕСТИ — переменная
результата не связана ни одним позитивным конъюнктом, и правило отвергается
range restriction [§190](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/27-part-xxvi-static-semantics-and-diagnostics.ru.md#190-rule-safety) (замер MELD 06.09.2026).

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L549-L574)

## lawref.cert.rounding_support

*function*

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

Опора [§62](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#62-support-pair) отношения округления ([§64.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/10-part-x-propositions-and-four-valued-support.ru.md#642-отношение-округления-над-сертифицированными-границами-errata-e-0136)).

Решение принимается на КОНЦАХ отрезка: все семь режимов [§50](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#50-money) монотонно
неубывающие, поэтому `round(lower) == round(upper) == value` равносильно
`I ⊆ C`, а `value` вне `[round(lower), round(upper)]` — `I ∩ C = ∅`.
Второго определения режима не заводится: `round_fraction` — тот же код,
которым считает `round` [§50](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/08-part-viii-type-system.ru.md#50-money).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L577-L598)

## lawref.cert.sin_bounds

*function*

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L381-L382)

## lawref.cert.sqrt_bounds

*function*

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

Сертифицированные границы квадратного корня ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154), E-0152).

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

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L245-L272)

## lawref.cert.verify

*function*

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

Сверка объявленных границ с ПЕРЕСЧИТАННЫМИ ([§259.2](https://github.com/arxohq/law/blob/master/spec/SPEC.ru/34-part-xxxiii-standard-library.ru.md#2592-сертифицированные-границы-errata-e-0136-decision-0154)).

[View source](https://github.com-arxohq/arxo-io/law/blob/2edc2b92ce22b52e03f4081d2769a58229684379/engines/lawref/lawref/cert.py#L532-L542)