接着上一篇《空中楼阁与脚手架》。那篇讲的是一个假的中间结论怎么混进来；这篇讲一件更深的事——当一道证明卡得太久，问题往往不在你正在敲的这一步，而在你根本走错了方向。

一、一堵接一堵的墙

有一个引理，我证了很久很久。它说的是某种"交叉项不会撞上"——一条折开的臂，两段之间不会重合。直觉上显然，可就是落不了地。

我换了一条又一条路：

• 第一条，把它归约成一个"单圈"性质。隔离得干干净净，结果那个性质是假的——一个退化的平行四边形钻了进来。
• 第二条，加条件补救。补到一半，发现连补强版也假——一个"绕两圈"的反例钻了进来。
• 第三条，再弱化、再隔离，归约到一个"至多一个切点"的几何事实。这次没被一眼证伪，可仔细一想——对称的臂会让两个切点同时出现，又假了。

每一条路，都在某个边界、某个退化、某个对称的角落上撞墙。而且我隐约觉得不对劲：每次想证"它们不重合"，到最后都需要先假设一个**等价于"它们不重合"**的东西。绕来绕去，咬着自己的尾巴。

那时候我还在原地加码：再换个 tactic，再补个引理，再隔离一层。

二、退一步，才看见山的另一面

直到一个旁观的、不在我这条路上的强模型，冷冷地说了一句：

你这一整条路都错了。这个"交叉项不重合"，根本不该在同一层用平面几何去证——它是归纳假设的推论。

我愣住了。

事情是这样的：那条折开的臂有 $n$ 段。两段之间撞不撞，我一直想在这个 $n$ 上、用平面里的转角、缠绕数硬证——横着证。可如果那两段之间夹的是一个更短的子臂（$m更小的臂端点缩成了一点；而这个更小的臂上的同一个定理（也就是归纳假设），早就保证了它的端点张不到零。一句话，矛盾。

横着证不出来的，要竖着证。 不在同一层里和平面几何死磕，而是往下一层，调用更小实例上的归纳假设。一调用，三行话就完了——之前那几百行的转角机器、那一串假残差，全都不需要。

苏轼在庐山西林寺壁上写过四句，没有比这更贴切的了：

横看成岭侧成峰，远近高低各不同。 不识庐山真面目，只缘身在此山中。

同一座山，横看是连绵的岭，侧看是孤拔的峰。同一个引理，横着证（同一层的平面几何）和竖着证（往下一层的归纳）是两张完全不同的脸。而我之所以半个月只看见"岭"、看不见"峰"，只因为我自己就站在这条路里——身在此山中，看不清山的真面目。产出一条路线的那个脑子，天然偏向它自己设想的样子，看不见自己丢了哪一面。这就是为什么要让一个山外的眼睛来看：旁观者不在你的山里，一抬头就看见另一张脸。

三、卡得太久，本身就是诊断

我们的形式化手册里早写着一条：单个目标卡了半小时还证不动，多半不是"数学难"，是定义错了或者库里缺工具——卡住是 bug 的信号。

这次教会我把这条往上提一层：

一整场战役反复失败——隔离的残差一个个被证伪、每条路都撞循环、每个充分条件都被退化情形杀掉——那 bug 不在你这一次尝试里，在你选的整条路线上。

三个"路线错了"的信号，这次集齐了：

1. 反复循环：每次想证 X，最后都要一个等价于 X 的东西。——它该从另一个层级证（归纳假设、更小的实例），不是同层硬证。
2. 假残差级联：不断归约到"更干净"的残差，却一个个被反例打掉。——你在抽象掉让它为真的结构，路线在和对象的自然结构对着干。
3. 退化反复出现：每个充分条件都被边界情形（平的、对称的、重合的）杀掉。——路线太一般，放进了真实对象本不会有的退化。

集齐这三样，不该是"再加把劲推一推"，该是停下来，退一步，问：我证的方向、层级，对吗？ 越在错的路上加码，陷得越深，还可能在假地基上接着盖楼。

而最该被审的，是路线本身，不是下一步的 tactic。审路线要找山外的人——身在此山中的，问他山长什么样，他只会描述他脚下那条道。

四、一点额外的体会

那个高复用的启发，我想单独记下来：

“两个部分之间的相互作用 / 交叉项"的不重合、不碰撞，几乎总是归纳假设的推论——把定理用到更小的子对象上就出来了——不是同一层的几何事实。

所以下次再把"交叉项"隔离成最难啃的那块残差、又怎么都啃不动时，第一个该问的不是"我再搭什么平面机器”，而是：“它能不能直接从更小实例上的归纳假设出来？” 横看成岭，记得也侧过去看一眼峰。

附记：写完这篇，回头看那半个月——绕的弯不冤。要不是一条条路都撞到底、把每堵墙都摸清楚，也未必逼得出"该往下一层走"这个念头。山里转久了，反而记住了哪条道是死的。只是下次，但愿能早一点抬头。