tex-lean-derivation

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 个高亮宏。
• 避免引入复杂交互；优先静态可读性。
• 颜色服务于推导，不要喧宾夺主。

输出目标

读者应当能顺着“文字说明 -> 改写后的式子 -> 高亮变化块”一路看下去，而不是自己在长公式里找差异。