formula-derivation

数式の導出：理論ラインの構築

見せかけの、洗練された定理のストーリーではなく、誠実な導出パッケージを作成します。

定数

• DEFAULT_DERIVATION_DOC = プロジェクトルートの DERIVATION_PACKAGE.md
• STATUS = COHERENT AS STATED | COHERENT AFTER REFRAMING / EXTRA ASSUMPTION | NOT YET COHERENT

コンテキスト：$ARGUMENTS

目標

次のいずれかを、正確に 1 つ作成します。

1. 元の対象に対する一貫した導出パッケージ
2. 対象／仮定／適用範囲を修正して再構成した導出パッケージ
3. 現在のメモでは一貫した導出をまだ裏付けられない理由を説明する阻害要因レポート

入力

以下を抽出して正規化します。

• 対象となる現象、数式、関係、または理論ライン
• 導出の意図された役割：
  • 厳密な恒等式／代数
  • 命題／局所定理
  • 近似
  • メカニズムの解釈
• 明示された仮定
• 記法と定義
• ユーザーが提示した数式の連鎖、概略、未整理のメモ、または現在の草稿
• 依頼で指定された関連するローカル理論ファイル
• 指定がある場合は、希望する出力形式：
  • 内部調整用メモ
  • 論文形式の理論草稿
  • 阻害要因レポート

対象、オブジェクト、記法、または仮定が曖昧な場合は、導出を始める前に、採用する解釈を明記します。

ワークフロー

Step 1：導出のコンテキストを収集する

次の優先順位に従って、対象となる導出ファイルを決定します。

1. ユーザーが明示的に指定したファイルパス
2. ローカルメモですでに参照されている導出草稿
3. デフォルトの対象ファイルとして、プロジェクトルートの DERIVATION_PACKAGE.md

関連するローカルコンテキストを読み取ります。

• 選択した導出ファイル（すでに存在する場合）
• ローカルの理論メモ、数式の草稿、付録のメモ、またはユーザーが明示したファイル

以下を抽出します。

• 対象となる数式／理論上の目標
• 現在の数式の連鎖
• 仮定
• 記法
• 既知の阻害要因
• 希望する出力モード

Step 2：対象を確定する

次の点を明示します。

• 説明、導出、または裏付けの対象
• 直近の目標が次のどれか：
  • 恒等式／代数
  • 命題
  • 近似
  • 解釈
• 導出の最終的な出力

これを確定する前に、記号操作を始めないでください。

Step 3：不変の対象を選ぶ

導出の軸となる、単一の量または概念的なオブジェクトを特定します。

一般的な候補には、次のものがあります。

• 目的関数／効用／損失
• 総コスト／エネルギー／厚生
• 保存量／状態変数
• 期待指標／実効率／実効コスト

現在のメモがより限定的な量から始まっている場合、それが次のどれに当たるかを明示的に判断します。

• 真の最上位オブジェクト
• 代理指標
• 局所的な切り出し
• 近似

扱いやすい代理指標で、実際の概念的なオブジェクトを暗黙のうちに置き換えないでください。

Step 4：仮定と記法を正規化する

以下を言い換えて明確にします。

• すべての仮定
• すべての記号
• 適用範囲の境界または特殊ケース
• 固定されている量、適応的な量、状態依存の量

以下を特定します。

• 暗黙の仮定
• 未定義の記法
• 適用範囲の曖昧さ
• 現在の数式の連鎖に、厳密なステップと近似がすでに混在しているかどうか

一貫性を保つために整理が必要な場合を除き、ユーザーが元々使っている記法を維持します。 より明確な内部定式化を採用する場合は、それを導出上の手段として保ち、ユーザーの対象と暗黙のうちに置き換えないでください。

Step 5：導出の各ステップを分類する

重要な各ステップについて、次のどれに当たるかを判断します。

• 恒等式：厳密な代数的変形
• 命題：条件を要する主張
• 近似：モデルの簡略化または代理指標
• 解釈：数式の文章上の意味

これらの分類を、移行を明示せずに混同しないでください。 ある部分が解釈にすぎない場合、数学的に証明されたかのように提示しないでください。

ステップ 6：導出マップを作成する

導出の方針を選びます。たとえば、次のようなものがあります。

• 定義 -> 代入 -> 簡約
• 基本法則 -> 中間変数 -> 目標の式
• 大域的な量 -> 摂動 -> 分解
• 厳密なモデル -> 近似 -> 解釈可能な閉形式
• 一般的な動的対象 -> 簡略化した断面 -> 局所定理 -> 一般の場合に戻る

次に、導出マップを作成します。

• 目標の公式または理論上の記述
• 必要な中間恒等式または補題
• 各自明でないステップで使う仮定
• 近似を導入する箇所
• 特殊ケースと一般ケースの領域が分岐または一致する箇所

導出に分解が必要な場合は、選択した大域的な量からその分解を導出してください。 単一の局所変数だけから、分割が突然現れるようにしてはいけません。

ステップ 7：導出ドキュメントを作成する

選択した対象の導出ファイルに書き込みます。

対象の導出ファイルがすでに存在する場合：

• まず読みます
• 該当するセクションを更新します
• 既存の内容をむやみに重複させません

ユーザーが対象を指定しない場合は、プロジェクトルートの DERIVATION_PACKAGE.md を既定とします。

ユーザーがその対象を明示的に指定しない限り、論文のセクションや付録の .tex ファイルに直接書き込んではいけません。

導出パッケージには、次の内容を含める必要があります。

• 目標
• ステータス
• 不変対象
• 仮定
• 表記法
• 導出方針
• 導出マップ
• 主な導出ステップ
• 注記／解釈
• 適用範囲と主張しない事項

執筆ルール：

• 「明らかに」「自明に」「同様に」といった言葉で論理の欠落を隠してはいけません
• 各記号は使用前に定義します
• 近似を明示します
• 導出の本文と注記を分けます
• 真の対象が動的または状態依存であり、より単純な断面を分析する場合は、そのことを明示します
• 数式の行がヒューリスティックにすぎない場合は、そのように正直に表示します

ステップ 8：最終確認

対象の導出ファイルを仕上げる前に、次の点を確認します。

• 目標が明示されている
• 不変対象が導出全体を通じて安定している
• 使用するすべての仮定が記載されている
• 各数式のステップが恒等式／命題／近似／解釈のいずれかとして正しく表示されている
• 導出の途中で対象が暗黙に切り替わっていない
• 特殊ケースと一般ケースが、引き続き同一の理論的な流れに属している
• 適用範囲と主張しない事項が記載されている

一貫した対象、安定した仮定、または前提から結論までの誠実な道筋がまだない場合は、筋の通った説明を無理に作るのではなく、ステータスを下げてブロッカーレポートを記述します。

必須のファイル構成

対象の導出ファイルを次の構成で作成します。

# Derivation Package

## Target
[what is being derived or explained]

## Status
COHERENT AS STATED / COHERENT AFTER REFRAMING / NOT YET COHERENT

## Invariant Object
[top-level quantity organizing the derivation]

## Assumptions
- ...

## Notation
- ...

## Derivation Strategy
[chosen route and why]

## Derivation Map
1. Target depends on ...
2. Intermediate step A uses ...
3. Approximation enters at ...

## Main Derivation
Step 1. ...
Step 2. ...
...

## Remarks and Interpretation
- ...

## Boundaries and Non-Claims
- ...

## Open Risks
- ...

出力モード

導出が記述どおりに一貫している場合

上記の構成全体を、整理された導出パッケージとして記述します。

メモは完成に近いものの、まだ一貫していない場合

次の内容を記述します。

• 正確な不一致点
• 修正した不変対象、仮定、または適用範囲
• 再構成した導出パッケージ

導出を誠実に一貫したものにできない場合

次の内容を記述します。

• Status: NOT YET COHERENT
• 正確なブロッカー：
  • 対象の欠落
  • 仮定の不安定さ
  • 表記法の衝突
  • 裏付けのない近似
  • 十分な条件を欠いた定理レベルの主張
• 必要となる追加の仮定、再構成、または中間導出

proof-writerとの関係

ユーザーが次のように述べた場合は、formula-derivationを使用します。

• 「我不知道怎么起这条推导主线」
• 「这个公式到底该从哪个量出发」
• 「帮我把理论搭顺」
• 「把说明文档变成可写进论文的公式文档」
• 「这几段公式之间逻辑不通」

proof-writerは、次の条件を満たした後にのみ使用します。

• 具体的な主張が確定している
• 仮定が安定している
• 表記法が定まっている
• タスクが、その主張を厳密に証明または反証する段階にある

具体的な主張とその仮説が定まった後で、ユーザーがLeanを求める場合、または特定の証明義務に形式的な実装と検証が有効な場合は、 /lean-formalizeを使用します。 通常の代数的導出には必要ありません。

チャットでの応答

対象の導出ファイルに書き込んだ後、次の内容を簡潔に回答します。

• ステータス
• 目標を変更せずに維持できたか、再構成が必要だったか
• 更新したファイル

主なルール

• 対象、前提、または適用範囲が導出を裏付けていない場合、筋の通った導出を捏造しないでください。
• 過大な主張をするのではなく、導出を別の形で捉え直してください。
• 前提、恒等式、命題、近似、解釈を区別してください。
• 可能な限り、特殊なケースと一般的なケースで同じ不変の対象を維持してください。
• パラメーターを定数とする単純化されたケースは、概念上の主対象ではなく、分析の一断面として扱ってください。
• 不確実性が残る場合は、Open Risksに明示してください。洗練された文章に紛れ込ませないでください。
• 洗練さよりも一貫性を重視してください。