5.11 解题：找表示、找不变量、查边界

一步一步建立直观

先预测，再点“演示本步”核对右图。每一步都重设到指定情形，随后可以自由修改参数。

面对线性方程，先把未知数看作输入向量，把方程右侧看作期望输出。右图让矩阵两列成为基向量的去向，于是求解问题变成“哪一个输入能到达目标”。选择合适表示常常比立即展开计算更重要，因为它能先暴露问题的结构。

把两列调到共线，输出平面压成直线。此时某些目标不可达，某些目标又有许多原像，立即说明唯一解需要额外条件。一般公式中的非零分母常常对应这种几何退化；检查它，比在算完后才发现除以零更有效。

切到剪切，形状改变但面积倍率为一。若计算结果声称面积翻倍，就可以迅速定位错误。解题结束不只是写出一个表达式，还应代回原条件，核对单位、符号和特殊值，并说明结论在哪些情况下失效。图形提供检验线索，证明负责说明一般性。

已知 $x+y=7,xy=10$ ，要求 $x^2+y^2$ ，并不一定要先求出两个数。目标对交换 $x,y$ 不变，提示我们改用和与积。展开 $(x+y)^2$ 后立即得到答案 $49-20=29$ 。

这不是偶然的巧招，而是表示选择：若问题不关心两个数谁是谁，就没必要保留这份区分。二次方程的中心、矩阵的迹和行列式也在压缩类似的对称信息。

做小例子可以发现规律，极端例子可以暴露漏洞，图形可以提示不变量；但它们通常还没有覆盖全部情形。猜想形成后，要把观察变成对任意允许输入有效的推理，并记录用了哪些条件。

例如给定和 $s$ 与积 $p$ ，实数解的存在要求 $s^2-4p\ge0$ 。即使目标表达式能顺利算出，原问题也可能根本没有实数对象。计算简化之后仍需回头检查可行性。

建立自己的解题记录时，可以写三段：原表示哪里困难，新表示保留了什么，如何把结果返回原问题并检查边界。能解释为什么换表示，就更容易把方法迁移到下一道题。Lean 可以核验具体恒等式，但不会替你决定哪个表示最有启发性。

与本图相连的定义与证明：1.3 · 基向量的像决定整个映射。本节的具体条件与形式化范围见下文。

遇到困难时可以先做小例子、画图、改变表示，或寻找在变换下不变的量。目标是减少独立信息，而不是堆积运算。

对称表达式常改用和 $s=x+y$ 与积 $p=xy$ ，因为 $x^2+y^2=s^2-2p$ 。这种替换也连接到二次方程与矩阵的迹、行列式。

例 5.11.1 把概念用于具体计算

已知 $x+y=7,xy=10$ ，不必先求 $x,y$ ，就能得到 $x^2+y^2=49-20=29$ 。再求根会得到 $2,5$ ，作为交叉检查。

已知 $x+y=3,xy=1$ ，求 $x^3+y^3$ 。

展开解答与检查

用 $s^3-3ps$ 得 $27-9=18$ 。

Lean 对照 5.11.1 命题、证明与适用边界

完整验证对称二次式的代数变换。一般解题策略不是数学全称定理，不声称已被形式化证明。

Lockdown.symmetric_problem_reduction

theorem symmetric_problem_reduction (x y : ℝ) :
    x^2+y^2=(x+y)^2-2*x*y := by ring

原课对照观课问题、视频与图示

寻找能减少未知信息的表示，并在得到答案后返回原问题检查可行性。

点击后连接 YouTube；播放器不可用时可通过上方原链接观看。