| name | tex-lean-derivation |
| description | 在 TeX 文档里把数学推导写成 Lean4 风格的逐步改写。适用于用户希望把长串连等式改成“文字说明 + 改写后的公式 + 高亮本次变化块”的场景。 |
TeX Lean Derivation
用于把数学推导改写成更易读的逐步重写风格。
什么时候用
- 用户嫌连等式太长、太机械。
- 用户希望像 Lean4 证明那样一步步改写。
- 用户明确提到
enter、rw、simp、done 这类风格。
- 需要在 TeX 中把“每一步改了什么”讲清楚。
- 用户希望把主文档和细节推导拆开，做成
main + 子推导 PDF 的结构。
默认写法
- 不把整段推导塞成一大串连等式。
- 先给当前目标式。
- 每一步先用一句短文字说明“这次做什么”。
- 下一行只写改写后的公式。
- 用颜色高亮本次被改写的块，不要整行乱染色。
- 颜色分工要稳定；同一段推导里不要频繁换语义。
模式
新手详细模式
- 默认优先用这个模式，尤其是用户要“从基础讲清楚”“不要跳步”“面向初学者”时。
- 尽量多用
rw，少用 simp。
- 能拆成多个小步骤，就不要合并成一个大步骤。
- 每一步都明确说本次到底调用了什么：定义、独立性、零均值、协方差定义、矩阵恒等式。
- 不要把“独立且零均值所以为 0”压成一句；应拆成：
- 先用独立性把联合期望拆开。
- 再单独调用零均值。
- 最后代回得到 0。
- 如果某个中间事实后面会反复用，可以先单独写成一个临时 lemma，再在主推导里调用。
专家简洁模式
- 用户明确要简洁、默认知识较强、或正文已经很长时用这个模式。
- 可以把显然的小步合并，但不能跳过关键理由。
simp 可以用，但要说明它到底简化了什么，而不是把多个不同性质混成一句。- 目标是更短，不是更黑箱。
推荐节奏
enter：把定义或上一步结果代入。rw：按某个恒等式、展开式、矩阵规则改写。have：先单独提出一个接下来要反复调用的中间事实或临时 lemma。simp：只在“已经说明理由后”的收尾简化里用；不要拿它一口气吞掉多个逻辑点。done：合并前面几步，落到最终结果。
这些标签只是写作提示，不要求机械照搬；重点是让读者看懂“每次改动发生在哪一块”。
临时 Lemma
- 当某个中间结论会复用，或单独拿出来更利于阅读时，可以先立一个临时 lemma。
- 临时 lemma 适合承载这类内容：
- 零均值推出某项期望为 0
- 协方差定义改写成二阶矩
- 某个矩阵可从期望外提出来
- 两个交叉项完全同理
- lemma 要短，只服务当前段落，不要写成教科书式正式定理。
- 主推导里引用 lemma 时，要让读者看得出“这里是在调用前面哪个中间结论”。
文档组织
- 优先把“主线叙述”和“细节推导”分开。
- 主文档
main 只保留主结论、主流程、必要的短公式和跳转入口。
- 细节推导尽量拆成独立子块；一个重要推导对应一个独立 section。
- 导言区不要在每个文件里重复写；优先抽成共享
preamble.tex、.sty 或同等公共头文件。
需要多文件布局时，读 references/modular-pdf-layout.md。
TeX 侧约束
- 若文档里已有颜色/步骤宏，优先复用。
- 若没有，可临时定义少量宏，例如步骤标题宏和 2 到 3 个高亮宏。
- 避免引入复杂交互；优先静态可读性。
- 颜色服务于推导，不要喧宾夺主。
输出目标
读者应当能顺着“文字说明 -> 改写后的式子 -> 高亮变化块”一路看下去，而不是自己在长公式里找差异。
