book集

section 結論と範囲
txt Thmは形式的なものとし、Thmの変換とtrustで受理条件を指定する方針を維持します。◀に対象論理を暗黙に割り当てません。
txt 今回、◀ … h; の暗黙の受理と、結論の補助検査が翻訳先を一階側へ戻していた不具合を訂正しました。ただし、三点すべての数学的・実装的な完了を確認したわけではありません。以下で閉じた点と残る点を明記します。

section 一点目：trustの仕様と実装
txt Bookのtrust文は受理条件の数学仕様です。現在の.thmelの実行可能な宣言はbackend、target、sort、translate等で、trust文そのもののパーサと認証記録は未実装です。現在の査読成功を、新しいtrust仕様を実装した結果と取り違えません。
txt 認証記録は、元のThm、選択したtrust、翻訳と規則・DBの版、生成した記号と補助仮定、対象論理、実際に検査した問題、証明または証明器の結果を結び付ける必要があります。backendの追加はtrustの追加とは別です。
txt 追加修正：BookReviewKnownThmにevidence_relationを設け、実際に確認した一階側・多ソート側の経路を記録しました。これは形式的なThmに意味を付ける欄ではなく、そのThmを認めた証拠の出所です。thm行の◀から推測せず、実際の結論検査の経路から記録します。
txt 公開、import、環境の保存・読込み、Hyperionへの登録までこの欄を保持します。同じ形式的なThmの両経路の証拠は別々に保持します。経路を欠く旧記録や未知の経路名は、査読側で元Bookの再査読を要求します。保存・表示の制限は増やしません。
txt W.の差引き展開とprime定義の利用でも、確認した経路を落とさないよう制限しました。多ソート側の証明を、これらの補助処理から一階側の証明へ替えることはできません。
txt 未完了：trustそのものの識別子、翻訳・DBの版、補助仮定の依存、証明内容までをまとめた認証記録です。今回の経路欄は二つの既存経路を区別する実装であり、それだけで第三のtrustや任意の証明器の追加を実装したわけではありません。

section 二点目：二つの翻訳の比較
txt 外延性：一般の多ソート経路はクラス等号の使用時に外延性を生成していました。クラス外延性の例を実際のコンパイラからTFFへ出し、VampireはTheoremを返しました。以前のBookで外延性の追加が抜けていたことを訂正します。
txt 命題変数：修正前、内包中の裸のP^を含む例は多ソート出力で翻訳エラーでした。最初から命題定数|P^を書いた対照例は、生成した内包定義とgoalで定数を共有し、Theoremでした。調査の結果、一階側の定数化処理mathel_v_elimへ進む前に、多ソート側が分岐していたことが分かりました。今回、同じ定数化処理を多ソート側の内包展開前にも接続しました。修正後は裸のP^を含む元のBookも査読成功し、生成入力はVampireでTheoremでした。P^ ◀ P^と、⊥ ◀ P^ ,, ¬P^の二つの陰性対照はCounterSatisfiableとなり、別propの定数が混同されないことも確認しました。
txt A(T)ならB(T)、および一階翻訳が定義されるTについてB(T)ならA(T)という一般的な含意は未証明です。外延性と一つの内包例の確認を、この一般定理の証明に置き換えません。他のcvt定義、変数の範囲、生成仮定の相互作用を含む適用範囲の指定が必要です。

section 旧調査で構成した反例モデル（2_thmel.bookから移動）
txt 上の外延性・命題変数の不一致は、実装確認の前に、それぞれ具体的な多ソート構造の構成によって見つけていました。移動前の記録として残します。
txt 外延性の反例モデル：新しいクラス定数<code>|A_</code>, <code>|B_</code>について<code>(|A_ =_ |B_ ⇔ ∀ x (x ∈_ |A_ ⇔ x ∈_ |B_)) ◀ O</code>を考えます。s領域を1要素、c領域を異なる2要素a,bとし、所属関係を空にします。<code>|A_</code>をa、<code>|B_</code>をbと解釈すると、両者の要素は同じですが等号は偽になり、外延性を追加しないcls-elim側の翻訳ではgoalが偽・sosが空という反例が構成できます。上の二点目のとおり、現行実装はクラス等号の使用時に外延性を生成するため、この構造は現行の翻訳後のsosを満たしません。
txt 命題変数の反例モデル：<code>T = (∀x (x ∈ {y | P^} ⇔ P^)) ◀ O</code>を数学の記法で考えます。cls-elim側でgoalの中のP^とsosの中のP^を独立に定数化すると、goalの定数Aとsosの定数Bが別物になります。s領域を1要素、kを空クラス、Aを真、Bを偽と解釈すると、sosは真でgoalは偽という反例が構成できます。上の二点目のとおり、現行実装はcls-elimの内包展開前にmathel_v_elimで定数化するため、この構成は現行の出力を反映しません。
txt どちらも、当時の--|側の受理条件（クラス外延性を追加しない・内包展開後に命題変数を定数化する）に対する反例であり、現行の受理条件に対する反例ではありません。一般のA(T)・B(T)の定式化はsoundness.bookにまとめました。

section 三点目：hyperionとの接続
txt ◀ … h;：旧実装はこれを多ソート側の結論へ暗黙に割り当てていました。その扱いを撤回し、査読で理由付きで拒否します。保存・コンパイル・表示は可能です。形式的なThmを記述するthm行の◀はそのまま使います。
txt -| … h; と --| … h;：対象の翻訳経路を指定した結論検査です。結論検査が失敗して補助的な合成を試す場合にも、指定した経路を保持します。以前はこの補助検査で既定の一階側を使い、多ソートの認証なしで成功する場合がありました。今回、その経路の取り違えを修正しました。
txt 異なる経路の利用：既存のhyperion_relation_admitsは、経路をまたぐ際に再認証を要求します。ただし、これだけでhyperion全体の健全性や輸出済みThmの依存保持を証明したことにはなりません。
txt 存在導入：内包項の所属条件を認めた前段から、内包項を消した存在主張へ進むと、翻訳で生成した仮定が消える場合があります。全体クラスの存在を直接翻訳した対照例はVampireでCounterSatisfiableでした。2_thmel.bookのNBG例は、所属条件の証明と、未認証の存在主張を区別する形に書き直しました。
txt hyperionは開発途上です。構造的な存在導入のテストに通ることと、その規則がtrust条件の閉包性を満たすことを区別します。生成した仮定・命題定数の対応を運ぶ証明変換、独立な再認証、または明示的な追加trustのどれを採るかが残ります。

section 確認方法と、標準Bookを進める範囲
txt 今回の専用検査では、-| … h; と --| … h; の同経路の結論成功、◀ … h; の拒否とThmを追加しないこと、翻訳先を取り違える補助検査の拒否、◀ … h; を含むBookの表示可能性を確認しました。修正前に不適切な受理を再現し、修正後に拒否されることも確認しました。
txt 検査結果：専用8検査、既存の合成9検査、存在導入32検査が成功しました。書き直した命題変数のBookは5インスタンス、クラスのBookは4件のThm査読が成功しました。存在導入32検査は構造的な側条件の検査であり、上記のtrustの閉包性の未解決事項を解消するものではありません。
txt 証跡は作業領域mathelia_foundation_closure_20260908にあります。probe.phpが実コンパイラから問題を生成し、ext.tff・propvar.tff・constant.tff・exists.tffとVampireの結果を保存しています。check.phpは査読の結論検査を直接検査します。before・after・manifestには修正内容とハッシュがあります。
txt DBと標準Bookの執筆は、翻訳結果と根拠を個別に確認できる部分から進められます。ただし、生成仮定が消える存在導入や、完全なtrust認証記録については未完了です。Book間の受け渡しで経路が失われる不具合は上記のとおり修正しました。これらを閉じることが、基礎全体を固まったと言うための残る作業です。

section Book間の受け渡しの検証
txt 実際のBookで一階側と多ソート側の定理を証明して公開し、importと環境の往復で経路が保持されることを確認しました。多ソート側の定理をimportした後、--| … h; の結論は成功し、-| … h; への流用は失敗しました。経路のない記録の拒否、二つの証拠の共存、W.の差引き展開にも陽性・陰性対照を置きました。
txt 回帰検査は.claude/test_book_evidence_relation.php、変更前後のファイルと検証用Book生成スクリプトは作業領域mathelia_provenance_20260908に保存しています。

section W+.追加後の監査と再検証（2026-09-08）
txt --|の定義に従って、使用したW+の語の定義を添え、その定義に現れる語の定義も収集する実装を確認しました。⊊_の定義に必要な⊂_を落としていた処理は修正済みです。また、明示的なscと暗黙のscが別の記号に翻訳されていた処理を統一し、内部ノードの必須項目の欠落を修正しました。sc.とExi.は、修正後に一階側・多ソート側とも実証明器で証明できました。
txt 非schemaで穴のない定義29件を再検査した結果、多ソート側は22件がTheorem、7件が未対応の量化子による翻訳エラーでした。これらの有限個の検査を一般的な同値の証明とはしません。偽の包含と偽のクラス等号の陰性対照はCounterSatisfiableでした。
txt 訂正：この例は同値性の反例ではありません。<code>T = (x ∈_ |B_) ◀ (x ∈_ A_)</code> に第3節のcvt+を機械的に適用すると、goalは新しい述語 <code>|?p^ (x)</code> に替わります。A_はクラス変数なのでwordに対する置換規則を適用できず、sosの <code>x ∈_ A_</code> は残ります。W+の∈_が残るため、続く <code>|1+v^</code> はエラーです。したがって、この例の-|は定義上意味を持ちません。
txt 実装がこの例を一階側でCounterSatisfiable、多ソート側でTheoremとした実測は、両者が定義上意味を持つことを示しません。一階側がA_を固定した述語に替えて受け付けていることが、定義との不一致です。この実装の受理範囲の修正は未完了です。
txt --|側の全称的な扱いは、0_tutorial/4_high.book第3節の仕様に従っています。そこでは <code>⊥ ◀ x {/}= y</code> が成立し、sosから <code>x {/}= x</code> を得ます。仮定の自由変数を固定パラメータと読む別の規則を持ち込んではいけません。
txt 現在の結論：-|と--|の両方が定義上意味を持つ範囲について、同値性を否定する確認済みの反例はありません。ただし一般的な同値性の証明は未完了です。判定は厳密な定義と機械的な規則適用に基づき、実装の受理や証明器の成功で定義を補いません。

misc/soundness_status.book

`misc/soundness_status.book`