#!/usr/bin/env bash
set -euo pipefail

ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
CHECK="$ROOT/check_answer"

cat <<'HASHES' | (cd "$ROOT" && sha256sum --check --status)
9648ac30c99606682084af3c96e43ec496007c36be2b18187d68e92fd1ef4cd8  check_answer/references/erdosproblems_662_2026-07-12.html
dee92433847a446118c3c3a2d2b8de9301a901c376883b59ad8f0a9bee57facf  check_answer/references/erdosproblems_662_forum_2026-07-12.html
328367c685878e6c02f05c029b9ea8125859a450e1ae08d02433dc2bb99d0746  check_answer/references/Mathematica_Japonica_46_3_TOC.html
79c50c3e7e40fbe23dc4677c4d9c27ef0a406cec96cda77655682be7c536cb99  check_answer/references/Erdos_Lovasz_Vesztergombi_1989_graph_large_distances.pdf
a9c9c2d7ff458986c340190c2666e8bf1da0c6d288f050389f7a6ca9a1307e8e  check_answer/references/Packomania_cci38_original.txt
cf97a53b80e0d9bab3d4d0d741cc02e7de0a5ba26f8bbab8ead2e0b53b277572  check_answer/references/Packomania_25_36_table.pdf
63bbc227ca70c9e45ac61f001ab62268e2a53d4efff75f5796c7801e48e5b44f  check_answer/references/erdos662_reconstruction_2026-04.pdf
4f6857ed7abdc5371d27b0c76a69248ae4b864c1fdce02ffd1309366c8e30136  check_answer/references/Vesztergombi_1987_small_distances_pp95-101.pdf
fcc19491810c101fd7567ec0247063e4300a0fcb023429a2f1d8217d00a51ac8  check_answer/references/ndl_primary/audit_primary_ocr.py
7ccc12bba061106495eeb72e8cd9eb96578c6f395fcb7cfa172ffbbf90e7c0f5  check_answer/references/ndl_primary/item_api.json
80fcd75d70f727af636a1466df8d293350dd6709db52135404f70ad940189fdf  check_answer/references/ndl_primary/ndl_search_sru.xml
91dd6f7c70bb4343a25aa5e2863cca113977d539480aafe63eedd375663b891d  check_answer/references/ndl_primary/reconstructed_ocr.txt
e32422447b61a0de50a62a7ef472c0b0538325371ded2be95e990015e362f2b4  check_answer/references/ndl_primary/retrieve_primary_ocr.py
f8456b67e3ee1264251c2e74df6072cd907afc610322aabb73699737a66237c7  check_answer/references/ndl_primary/snippet_api_capture.json
8c5aaab6e1efdec7f7f9f65cc0de77461c36a46e6b7c9ee7a35299dd6e8449ee  check_answer/references/ndl_primary/snippet_permission_api.json
HASHES

echo '[verify] source and provenance hashes: PASS'
python3 "$CHECK/references/ndl_primary/audit_primary_ocr.py"
echo '[verify] primary Er97e OCR provenance audit: PASS'
python3 "$CHECK/numerics/exact_shell_six.py"
python3 "$CHECK/numerics/exact_strict_shells.py"
echo '[verify] independent exact-integer closed/strict shell audits: PASS'
export PATH="$HOME/.elan/bin:$PATH"
cd "$CHECK/lean"
rm -rf .lake/build
lake build
lake env lean AxiomAudit.lean

if grep -R -n -E '\b(sorry|admit|native_decide)\b' \
  Research.lean AxiomAudit.lean Research; then
  echo '[verify] FAIL: forbidden proof token found' >&2
  exit 1
fi

echo '[verify] PASS: closed and strict local/global shell readings are kernel-refuted (with the below-sqrt(3) clause proved)'
