主要宣言に構成性・実行可能性の注釈を追加する

[t-uda]

目的

uda-lab/leray-hopf の成果が、

• kernel により検証された存在定理であること
• 数値的・実行可能な PDE solver を直接与えるものではないこと
• 非構成性が主に選択、部分列抽出、コンパクト性、極限の選択に現れること
• 明示的な witness／抽出データを外から与えれば、下流の組立てや極限通過を再利用できる部分があること

を、leray-hopf-notes 上で誤解なく示す。

全宣言を網羅的に分類しない。主定理、有限次元解データ、コンパクト性パッケージ、抽出、極限通過など、計算・構成性の境界を代表する少数の宣言だけを対象とする。

背景と設計上の注意

単純な computable / noncomputable 二値タグでは不十分である。

• theorem : Prop は通常、#eval 不能なのではなく、そもそも実行対象ではない。
• noncomputable def でも、明示的 witness を入力として受け取った後段は構成的に再利用できる場合がある。
• Classical.choice が証明部分だけに現れる場合と、返却データの選択に現れる場合を区別する必要がある。
• Σ 型・proof-carrying structure を返していても、その値の構成に古典的選択を使えば実行可能アルゴリズムにはならない。

この注釈は gap には入れない。gap は自然言語証明と Lean 証明の形式化上の隔たりを表す既存軸であり、構成性・実行可能性とは直交する。

対象候補

以下を初期対象とする。PIN 更新や宣言移動がある場合は、最新 extracted/decls.json の完全修飾名に合わせること。

A. 主定理

1. LerayHopf.exists_lerayHopf_torus3
2. LerayHopf.exists_lerayHopf_r3

示すべき点：

• Prop に属する存在定理で、直接 #eval する対象ではない。
• 弱解計算アルゴリズムを提供する主張ではない。
• T³ では NS forms と compactness limit、R³ ではさらに Galerkin basis/scheme 等の選択を含む。
• 明示的な package／抽出データを与えた後の assembly は別宣言として再利用可能。

B. proof-carrying data と自明な assembly

3. LerayHopf.Galerkin.SolutionData
4. LerayHopf.Galerkin.LerayHopfSolution
5. LerayHopf.Galerkin.CompactnessPackage
6. LerayHopf.Galerkin.exists_lerayHopf_from_package

示すべき点：

• これらは解曲線・極限曲線と正当性証明を束ねる proof-carrying structure である。
• exists_lerayHopf_from_package は、明示的な CompactnessPackage が与えられればフィールドをコピーして LerayHopfSolution を組み立てるだけであり、非構成的抽出の本体ではない。
• Nonempty への包装は実行可能 solver の提供とは異なる。

C. 有限次元 Galerkin 解データ

7. LerayHopf.Torus.galerkinSolutionData_torus
8. LerayHopf.galerkinSolutionData_unconditional（R³。最新の完全修飾名を確認）
9. LerayHopf.galSeq_of_torus
10. LerayHopf.galSeq_R3_of_basis

示すべき点：

• 有限次元 ODE 解と証明を返すデータ層であり、主定理よりアルゴリズムに近い。
• ただし現行宣言が noncomputable なら、その理由を「数値積分器が実装されていない」「ODE 存在定理から解曲線を選んでいる」等、ソースに即して短く記す。
• 「有限次元だから自動的に #eval 可能」とは書かない。

D. witness を入力として受け取る package builder

11. LerayHopf.build_galerkin_package_of_galSeq
12. LerayHopf.build_galerkin_package_R3_of_galSeq
13. LerayHopf.build_galerkin_package_of_torus
14. LerayHopf.build_galerkin_package_R3_of_basis

示すべき点：

• *_of_galSeq は Galerkin 列を明示入力として受け取るため、非構成部分と後段 assembly の境界を説明する代表例である。
• ただし内部で Aubin–Lions／limit-passage の存在結果から極限曲線を選ぶ場合、その返却 package はなお noncomputable である。
• 明示的な部分列・極限・収束証明まで入力化できれば、より下流の検証部分を再利用できる、という条件付きの構成的再利用可能性を記す。

E. 抽出と極限通過の境界

15. LerayHopf.exists_galerkin_modewise_extraction
16. LerayHopf.torusAubinLionsPackage_of_galSeq
17. LerayHopf.torus_galerkin_limit_passage_of_energyClass
18. LerayHopf.galerkin_spacetime_precompact_of_goodSampling
19. LerayHopf.galerkin_limit_passage_R3

この群は全件必須ではない。T³ と R³ からそれぞれ最低 1 件ずつ、次の対照が見える宣言を選ぶ。

• 抽出宣言：部分列・極限等の存在を得る場所。古典的選択／背理法への依存がデータ選択へ流れ込む境界。
• 極限通過宣言：部分列・極限・収束仮定が与えられた後、それが弱方程式・エネルギー条件等を満たすことを示す場所。外部 witness を与えた場合に再利用できる度合いを説明する。

宣言名・型・証明本文を確認し、実態と合わない一般論を付けないこと。

注釈 schema

corpus.schema.json に、任意項目 computability を追加する。全 corpus への付与は要求しない。

推奨する最小 schema：

computability:
  role: proposition | proof-carrying-data | data-constructor
  execution: not-applicable | noncomputable | executable
  classical_boundary: none | proof-only | data-selection | compactness-extraction
  reuse: direct | after-explicit-witness | not-applicable
  note_ja: |
    1〜3文の補足。

各フィールドの意味

• role

  • proposition: Prop を返す theorem/lemma。直接の実行対象ではない。
  • proof-carrying-data: 解曲線・極限・証明を束ねる structure／その値。
  • data-constructor: Galerkin 列や package 等を構成する def。

• execution

  • not-applicable: theorem/lemma であり #eval 可否を問う対象ではない。
  • noncomputable: Type 側の値を返すが、現行定義は非計算的選択等に依存する。
  • executable: 実際にコンパイル・評価可能であることをソースまたはテストで確認した場合のみ使う。

• classical_boundary

  • none: 対象宣言および主要依存に古典的選択が実質的に不要と確認できる。
  • proof-only: 古典論理への依存が proof-erased な証明側に留まる。
  • data-selection: Classical.choose / Nonempty.some 等で Type 側のデータを選択する。
  • compactness-extraction: 部分列・極限・コンパクト性 witness の抽出が主要な非構成境界。

• reuse

  • direct: 必要な明示入力があれば、そのまま下流で再利用できる。
  • after-explicit-witness: 部分列、極限、収束証明等を外から与えれば、後段の検証を再利用できる。
  • not-applicable: 単なる構造体定義等で、この軸を評価しない。

note_ja は常設の長文解説にしない。原則 1〜3 文、最大でも一段落とし、次の四点のうち必要なものだけを書く。

1. #eval の対象か否か
2. 非構成性がどこでデータ側へ入るか
3. 外部 witness を与えた場合に何が再利用できるか
4. 数値 solver／認証付き数値計算を提供する宣言ではないこと

表示方針

宣言ページに、computability が存在する場合だけ小さな「構成性・実行可能性」パネルを表示する。

表示例：

役割：存在命題
実行可能性：直接評価する対象ではない
古典論理の境界：コンパクト性による部分列・極限の抽出
明示的 witness を与えた場合：極限通過以降の検証を再利用可能

要件：

• 生の enum 値をそのまま日本語 UI に露出しない。
• gap、proof_status、provenance と混同しない独立パネルにする。
• 未付与宣言にはパネルも空欄も表示しない。
• 一覧画面やグラフ上に多数のバッジを追加する必要はない。まず宣言詳細のみでよい。
• tags は検索補助に留め、意味論的分類の正典は computability object とする。

実装手順

1. 最新の leray-hopf main と notes の extracted/PIN／decls.json を照合する。
2. 上記候補の型、宣言種別、noncomputable 修飾、Classical.choose／Nonempty／by_contra の実際の流入箇所を確認する。
3. 初期対象を 8〜12 宣言程度に絞る。必須内訳：
   • T³/R³ 主定理 2件
   • generic proof-carrying structure/assembly 2〜3件
   • 有限次元 Galerkin data 1〜2件
   • package builder 1〜2件
   • extraction/limit-passage の対照 2〜3件
4. schema と validator を更新する。
5. 対象 corpus YAML に computability を付与する。
6. build_site_data.py で項目を生成 JSON へ通す。
7. site/app.js に条件付きパネルを追加する。
8. schema/validator/rendering のテストを追加する。
9. README または corpus 作成ガイドに、短い記入基準と YAML 例を追記する。

受け入れ条件

• computability は任意項目であり、既存 corpus を一括変更せず検証が通る。
• 8〜12 の代表宣言に、ソース確認済みの注釈が付く。
• theorem を単に「noncomputable」「#eval 不能」と誤分類していない。
• noncomputable def を一律に「構成的再利用不能」としていない。
• Σ／proof-carrying structure と実行可能アルゴリズムを同一視していない。
• T³ と R³ の双方で、抽出と極限通過の境界が最低 1 例ずつ説明される。
• パネルは注釈のある宣言だけに表示される。
• python3 scripts/validate.py、python3 scripts/build_site_data.py、npm test が通る。

非目標

• 全宣言の構成性監査
• #print axioms の宣言単位での自動分類
• 実行可能な Navier–Stokes solver の実装
• leray-hopf 本体の主定理を Σ 型へ変更するリファクタリング
• 古典的存在定理を構成的証明へ置換すること

まずは本成果の論理的・計算的な立ち位置を、代表宣言に限って正確に可視化する。自動分類は誤判定しやすいため、初期版は手動注釈を正典とする。