ガイド & 信頼ポリシー

手元のマシンで証明をローカル検証する方法と、暗号的信頼モデルについて解説します。

1. ローカル検証（監査の実行）

独立した監査は、Nano Proof Auditor の中心的な価値です。以下の手順に従って、手元のマシンで証明を暗号的に検証することができます。

システムに Rust ツールチェーンと Cargo がインストールされていることを確認します。
以下のコマンドを実行して、ソースまたはパッケージマネージャーから NPA CLI ツールをインストールします。
```
cargo install npa-cli
```
パッケージのインデックスディレクトリ（例: npa-mathlib）に移動し、ローカルで検証コマンドを実行します。
```
npa package verify-certs --root ../npa-mathlib --checker reference --json
```

NPAは論理的健全性を監査するため、数学的定数と公理を分類しています。

決定論的ハッシュ値、検証ログ、およびチェッカー署名（.npcert）は、信頼された証拠を代表します。ソースコードテキスト、証明のリプレイステップ、およびドキュメントオーバーレイは、表示用のみに検証された信頼されていないサイドカーアセットです。

論理的矛盾（Falseの導出など）を防ぐため、定理は厳格な公理ポリシーに照らして監査されます。Leanの標準的な古典公理（Quot.sound、Propext、Classical.choice）はホワイトリストに登録されています。未検証の公理や独自の仮定はポリシー違反をトリガーします。

このレジストリで使用される形式検証の概念の簡単な定義です。

健全な証明項がチェックされたことを示す暗号証明書（.npcert）によって検証された数学的命題。

証明なしに仮定される命題。公理は論理の基礎ですが、チェックされていない独自の公理は矛盾を導入する可能性があります。

コンストラクタによって定義されるデータ型（例: ゼロと後続者によって定義される自然数）。

カリー・ハワード同型対応のもとで、定理の証明を表現する数学的表現式。

カーネル内で証明項の妥当性を検証するための、証明ステップの逐次的な再構築。