被逼出的真实结构：如何把幂与开方劈开

Abstract

通常把 n 次开方看成幂族的一个取值：x^(1/n) 即 x^t 在 t = 1/n 处。在正实数上这个塌缩是对的：那里幂映射 p_n: x -> x^n 是自同构，其逆是单值的。本文证明这个塌缩是挠现象：它恰好在 n 次单位根平凡处成立。在每个交换群上，幂映射的核是子群 mu_n = {x : x^n = 1}，每个纤维是陪集 x * mu_n，而开方不再是函数，而是 n 叶覆盖的截面：在彼此相差 mu_n 因子的 n 个分支中选一个。塌缩判据 -- p_n 单射当且仅当 mu_n 平凡 -- 标出开方与分数次幂的等同在哪里存活。三条初等定理刻画了这一分裂（核、纤维、塌缩判据），并在 Lean 4 + Mathlib 中机器验证：零证明缺口。计算端给出机器认证的根式值与二次求解器：x^2 - b x - c = 0 有实根当且仅当 b^2 + 4c >= 0，此时显式给出两个根式解并证明多项式可分解。纲领继而爬上三次：判别式 (q/2)^2 + (p/3)^3 >= 0 时 Cardano 构造给出 x^3 + p x + q = 0 的实根，依赖立方映射在 R 上的满射（中值定理）。随后它不再爬升而变宽：sqrt[n]{x} = exp(ln x / n) 是 y^n = x 对每个自然数次 n 的唯一正解，于是五次开方与一切次数的开方是一条陈述而不是一架梯子。五次扣下的不是纯开方而是混合塔；一般五次能否用根式求解（Abel-Ruffini）在此只引用不证明。主推导中每一条陈述都经机器检查；可执行整数算术与被认证但不可执行的实数命题之间的边界被明确划出：R 上的化简是经认证的定理，不是数值迭代。

Keywords