formula-derivation

公式推导：研究理论脉络构建

构建一份诚实的推导材料，而不是一套粉饰过的定理叙述。

常量

• DEFAULT_DERIVATION_DOC = 项目根目录中的 DERIVATION_PACKAGE.md
• STATUS = COHERENT AS STATED | COHERENT AFTER REFRAMING / EXTRA ASSUMPTION | NOT YET COHERENT

背景：$ARGUMENTS

目标

准确产出以下其中一项：

1. 针对原始目标的连贯推导材料
2. 对象 / 假设 / 范围经过修正的重构版推导材料
3. 一份阻碍报告，说明为什么现有笔记尚不足以支持连贯的推导

输入

提取并规范以下内容：

• 目标现象、公式、关系或理论脉络
• 推导的预期作用：
  • 精确恒等式 / 代数
  • 命题 / 局部定理
  • 近似
  • 机制解释
• 明确假设
• 符号和定义
• 用户提供的任何公式链、草稿、杂乱笔记或当前草案
• 请求中提及的相关本地理论文件
• 如有指定，期望的输出风格：
  • 内部对齐说明
  • 论文风格理论草稿
  • 阻碍报告

如果目标、对象、符号或假设含糊不清，应在开始推导前说明所采用的具体解释。

工作流

步骤 1：收集推导背景

按以下优先级确定目标推导文件：

1. 用户明确指定的文件路径
2. 本地笔记中已引用的推导草稿
3. 项目根目录中的 DERIVATION_PACKAGE.md（默认目标）

阅读相关本地背景：

• 已存在的目标推导文件
• 用户明确提及的任何本地理论笔记、公式草稿、附录笔记或文件

提取：

• 目标公式 / 理论目标
• 当前公式链
• 假设
• 符号
• 已知阻碍
• 期望的输出模式

步骤 2：固定目标

明确说明：

• 正在解释、推导或论证的内容
• 当前的直接目标是：
  • 恒等式 / 代数
  • 命题
  • 近似
  • 解释
• 推导最终预期产出什么

在固定目标之前，不要开始进行符号运算。

步骤 3：选择不变量对象

确定一个应作为推导主线的单一量或概念对象。

常见选项包括：

• 目标函数 / 效用 / 损失
• 总成本 / 能量 / 福利
• 守恒量 / 状态变量
• 期望指标 / 有效速率 / 有效成本

如果当前笔记从一个范围更窄的量开始，应明确判断它是：

• 真正的顶层对象
• 代理量
• 局部切片
• 近似量

不要让一个方便的代理量在不作说明的情况下取代实际的概念对象。

步骤 4：规范假设和符号

重述：

• 所有假设
• 所有符号
• 各种情形的边界或特殊情况
• 哪些量是固定的、自适应的或依赖状态的

识别：

• 隐含假设
• 未定义的符号
• 范围含糊之处
• 当前公式链是否已混合精确步骤与近似步骤

除非为保证连贯性确有必要，否则保留用户原有符号。 如果采用更清晰的内部表述，应将其用作推导手段，而不要在不作说明的情况下替换用户的目标。

步骤 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 中明确标出；不要用润色过的文字掩盖。
• 连贯性比优雅更重要。