Честность

Как проверить каждое число на этом сайте

Здесь указаны версии, входные данные и команды для проверки опубликованных результатов. Таблицы относятся к сохранённому прогону Balansis 1.1.0 от 2026-09-08. Они не описывают автоматически поведение нового релиза или другой версии Python.

Правило провенанса

Провенанс опубликованного прогона

Повторить у себя

Для численных примеров используйте ту же минорную версию Python, что в прогоне (3.12.3), и указанные версии пакетов. Для проверки Lean отдельно нужны elan, toolchain проекта и зависимости Mathlib. Генераторы и исходные JSON доступны файлами; их sha256 лежат в /repro/manifest.json.

# 1. Бенчмарки — нужен только Python и сеть до PyPI
curl -O https://balansis.xteam.pro/repro/generate-benchmarks.py
curl -O https://balansis.xteam.pro/repro/benchmarks.json
python -m venv .venv && . .venv/bin/activate
python -m pip install "balansis==1.1.0" "numpy==1.26.4"
python generate-benchmarks.py --out mine.json

# 2. Доказательства — нужен Lean4 (elan) и кеш Mathlib
curl -O https://balansis.xteam.pro/repro/generate-lean-audit.py
git clone https://github.com/StudyLabPro/Balansis
BALANSIS_REPO=./Balansis python generate-lean-audit.py --out mine-lean.json

# 3. Сравнить значения; расхождения требуют проверки окружения и алгоритма
python - <<'EOF'
import json
mine, theirs = json.load(open("mine.json")), json.load(open("benchmarks.json"))
for a, b in zip(mine["scenarios"], theirs["scenarios"]):
    for x, y in zip(a.get("results") or [], b.get("results") or []):
        if isinstance(x, dict) and "abs_error" in x:
            print(a["id"], x["method"], x["value"] == y["value"], x["abs_error"] == y["abs_error"])
EOF

Расхождения ожидаемы в двух местах: тайминги зависят от машины и загрузки, а результаты BLAS-зависимых операций (numpy.dot, numpy.linalg.svd) могут отличаться на другой сборке NumPy. Различия Python, компилятора и условий underflow тоже нужно учитывать для EFT-примитивов. Сверяйте результат с рациональным эталоном и сохраняйте версии вместе с воспроизводимым примером расхождения. Запуск Lean на текущей ветке проверяет текущие исходники; опубликованный JSON не фиксирует отдельный SHA дерева Lean, поэтому побайтовое воспроизведение именно того аудита им не гарантировано.

Расхождения, найденные в опубликованном прогоне

Это история проверки версии 1.1.0 и документации на дату 2026-09-08. Текущий README и поведение новой версии могли измениться. Численные результаты ниже сохраняют первоначальную версию; их нельзя переносить на другой релиз без повторения.

Чего на сайте нет