[P2][corpus] `sorry` に推移的に依存する公開定理が verified として表示される

[uda-lab-agent]

sorry を含む宣言に依存している公開定理が、proof_status を持たないため site 上で verified として表示される。

schema の定義

docs/schemas/corpus.schema.json は contains-sorry を次のように定義している。

'contains-sorry' = the proof body has a literal sorry (directly or via a sorry-dependent private helper).

つまり推移的な依存も対象である。一方、proof_status の欠落は verified と解釈される（同 schema）。したがって依存側に印が無いと、未証明に依存する定理が完了済みとして提示される。

実測（PIN 2a0679058d97979a4fba589bd92d0786ed09b97f）

自身の証明本体に literal sorry を持つ宣言は 6 件で、いずれも corpus 側で contains-sorry が付いている（notes#74 Wave 12 / PR #145 で 1 件の欠落を復元し、test/issue74_proof_status_preserved.test.py で固定した）。

問題はその呼び出し側である。sorry を持つ宣言は private または同一ファイル内にあるため、呼び出し元を同一ファイル内で機械的に洗い出した結果:

呼び出し元（tier: full・public）	使っている sorry 宣言	呼び出し元の proof_status
LerayHopf.Bochner.timeConvL2_weakDeriv_comm	timeConv_prod_integrable（private）	なし → verified 扱い
LerayHopf.Bochner.timeMollification_of_w1pTime	timeMollification_exists	なし → verified 扱い
LerayHopf.Bochner.w1pTime_continuous_in_Vprime	isWeakTimeDeriv_primitive	なし → verified 扱い

いずれも Bochner の実験的な時間層のもので、本 issue 起票時点で 3 件とも corpus ファイルは存在するが proof_status を持たない。

1 件目は schema の文言に真正面から該当する

timeConv_prod_integrable は private であり、schema の「via a sorry-dependent private helper」にそのまま当てはまる。証明本体に呼び出しがあることをソースで確認済み。

-- TimeMollifierInterval.lean, timeConvL2_weakDeriv_comm の証明中
have hint_u := timeConv_prod_integrable hψ'cont hψ'cs hρ hu

なお残っている sorry は Fubini 適用の側条件（コンパクトな箱の上での $L^1$ 評価）であり、上流に ALLOW_SORRY の注記がある。入れ替えの等式そのものは無条件に証明されている。

2・3 件目は schema の文言が明示していない

timeMollification_exists と isWeakTimeDeriv_primitive は private ではない（それ自体が contains-sorry として印付けされている公開宣言）。schema の文言は private helper 経由の場合しか述べていないため、公開宣言経由の推移的依存を印付けするかどうかは方針判断になる。

判断が必要な点

• 推移的依存の印付けを、private helper 経由に限るか、公開宣言経由も含めるか（schema の文言を実態に合わせて更新する）
• 含める場合、どこまで推移閉包を辿るか（1 段か、全段か）。全段だと Bochner 実験層に依存する広い範囲に波及しうる
• 印付けの手段: 手作業か、extracted/decls.json の依存情報から機械生成するか

機械化の障害: decls.json の uses は今回の依存を捉えていない（timeConvL2_weakDeriv_comm の uses に timeConv_prod_integrable が現れない）。private 宣言が依存グラフに記録されていない可能性が高く、推移閉包を自動で出すには抽出側の変更か Lean 環境からの取得が要る。

Acceptance criteria

• 推移的依存の印付け方針が決まり、schema の記述が実態と一致している
• 上表の 3 件について、方針に沿った状態になっている（印を付けるか、付けない理由が記録されている）
• 機械的に検査する手段があるか、無い場合はその旨が記録されている

関連

• notes#74 PR feat(#74): Wave 12（最終波）— 残り 51 件の private gloss 手書き化・テンプレート残存ゼロへ #145（Wave 12）で timeConv_prod_integrable の proof_status 欠落を復元し、test/issue74_proof_status_preserved.test.py を追加した。同検査は自身の証明に sorry を持つ 6 件を固定するもので、本 issue の推移的依存は対象外である。
• 本 issue は PR feat(#74): Wave 12（最終波）— 残り 51 件の private gloss 手書き化・テンプレート残存ゼロへ #145 の codex レビュー round 3 の指摘から切り出した。指摘は正当だが、対象 3 件はいずれも PR feat(#74): Wave 12（最終波）— 残り 51 件の private gloss 手書き化・テンプレート残存ゼロへ #145 の diff 外の既存状態であり、レビュー上限に達していたため別 issue とした。

[uda-lab-agent]

具体的な 3 件は解消（PR #147, merged b352f14）— 本 issue は一般問題に再スコープ

起票時に挙げた具体的な 3 件は解消した。site 上で未証明の公開定理が verified として表示される状態は無くなっている。

宣言	依存先	対応
Bochner.timeConvL2_weakDeriv_comm	timeConv_prod_integrable（private）	contains-sorry + 散文の開示を追加
Bochner.timeMollification_of_w1pTime	timeMollification_exists（public）	contains-sorry を追加、依存先を wikilink で名指し
Bochner.w1pTime_continuous_in_Vprime	isWeakTimeDeriv_primitive（public）	contains-sorry を追加、statement_ja の「（証明済み）」を削除（印と矛盾していた）

schema の文言も実態に合わせた。 起票時に「2・3 件目は依存先が private ではないため schema の文言が該当するか方針判断になる」と書いた点について、codex レビューでも同じ指摘を受けた。可視性は証明の完了度と無関係なので、contains-sorry の定義から private の限定を外した。

contains-sorry = the proof is not complete: the proof body has a literal sorry, or it depends on a declaration that does. Visibility of the dependency is irrelevant — a proof resting on an unproved lemma is unproved whether that lemma is private or public.

test/issue74_proof_status_preserved.test.py を拡張し（23 検査）、直接 sorry を持つ 6 件と推移的に依存する 3 件を別集合として固定した。推移側には依存先の名前が散文に現れることも要求する。

---

残るスコープ: 機械的な閉包が取れない

本 issue はここから「一般の推移閉包を機械的に扱えるようにする」問題として残る。

現状の 3 件は閉包ではない。 依存先が private または同一ファイル内にあることを利用して、同一ファイル内の呼び出し元を走査して得た集合である。この方法は一般には使えない。

障害: extracted/decls.json の uses が private 宣言を記録していない。実測で timeConvL2_weakDeriv_comm の uses に timeConv_prod_integrable が現れない。したがって閉包を自動生成するには次のいずれかが要る。

• extract_notes（leray-hopf 側）が private 宣言も依存グラフに含めるようにする
• あるいは Lean 環境から依存情報を直接取得する経路を用意する
• そのうえで、sorry を持つ宣言の推移閉包を機械的に印付け（または検査）する手段を作る

優先度について: 現時点で判明している具体的な取りこぼしは解消済みなので、これは「同種の取りこぼしを将来にわたって機械的に防ぐ」ための投資であり、緊急ではない。閉包を取れないままでも、sorry を持つ宣言が増えたときに同一ファイル内の呼び出し元を手で確認する運用は続けられる（notes#74 の各波で使った手順と同じ）。