结果族 024：An asymptotic formula for the number of totients · 学科：Number theory · 验证状态：暂无形式化证明，请以社区核验为准
欧拉函数 φ 是台”打折机”：整数 n 投进去，出来一个不超过 n 的数。不同的 n 可能打出同一个数，所以”机器到 x 为止总共能吐出多少种不同的值”比数整数难得多。这篇论文给出这个数目 V(x) 的精确渐近公式，还证明一条漂亮的”批发规律”：V(cx)/V(x)→c，回答了 Erdős 与 Hall 在 1976 年提出的问题。
关键词卡片
看个具体例子
小数据最容易看清”漏斗”：φ(1), …, φ(10) 依次为 1, 1, 2, 2, 4, 2, 6, 4, 6, 4——十个输入只吐出 {1, 2, 4, 6} 四种值，例如 4 和 6 都打出 2。机器越转越久，输出种类涨得比整数慢得多：Pillai 1929 年就知道取值密度为零，但精确数清它极难。
大尺度上，定理说 @@M@@V(x)\sim\frac{x}{\log x}G_m A(1;\theta)@@（系数由相位 θ 与有限算术数据决定），特别地 @@M@@V(2x)/V(x)\to 2@@：取值种数近似随端点线性伸缩。
为什么值得关心
“数函数值”比”数整数”深一层，是解析数论的代表性难题：Ford 1998 年的最好结果只能把 V(x) 夹在相差一个有界因子的两条渐近线之间，因为这个因子可能随相位永远振荡、上下界夹逼失效。本文精确保留离散尾部，让相位依赖的系数显式浮现，把估计推进成完整的渐近等价。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读的”打折机/漏斗”换成半数学语言：对象是一条整数流和它们经过欧拉函数后的输出流；操作是统计输出流到上限 x 为止出现过多少种不同的值。难点在于机器是多对一的：不同输入可以打出同一个输出，所以”数取值”不是”数整数”，差别在渐近主项层面是决定性的。导读末尾那条”批发规律”说：把上限从 x 拉伸到 cx，取值种数近似按比例 c 伸缩。
第二级台阶
用本科术语：欧拉函数 φ(n) 计数 1 到 n 中与 n 互素者的个数；V(x) 是 φ 在 [1,x] 内取到的不同值的个数。Pillai 1929 年已知取值密度为零；Maier–Pomerance（1988）定出主部为 (x/log x)·exp{(C₀+o(1))(log₃x)²}；Ford（1998）把误差压到只差一个有界乘性因子，但该因子可能随”相位”——迭代对数尺度上的小数部分——持续振荡，夹逼失效，渐近等价就此卡住。
第三级台阶
定理的语境：记 B=log₂x，m 由 B 的规模与更新序列的衰减常数决定，相位 θ 是相应量的小数部分，G_m 是 Ford 的计数尺度因子。主定理断言 V(x)～(x/log x)·G_m·A(1;θ)，其中系数 A 是一列只用有限算术数据（素数与整数的有界和、容斥、一致收敛极限）定义的函数的极限——定义不使用 V 自身，杜绝循环。结构起点是 Ford 的正则性定理：典型原像的大素因子按双对数坐标落在单纯形的窄带里；证明在两处切刀，长前缀交给连续体积计数，短尾与余因子精确保留离散算术——正是这一”不平均化”让相位依赖的系数显式浮现。批发规律的证明另有妙笔：对 t=x 与 t=x/c 共用同一未知质量，相减时直接消去，全程不需要系数连续。
论文给出欧拉函数不同取值个数 @@M@@V(x)@@ 的显式渐近等价 @@M@@V(x)\sim\frac{x}{\log x}G_mA(1;\theta)@@，系数是有限算术数据的一致极限；并证明 @@M@@V(cx)/V(x)\to c@@，正面回答了 Erdős 与 Hall 1976 年提出的固定伸缩问题。
欧拉函数（Euler’s totient function）@@M@@\varphi(n)@@ 计数 @@M@@1@@ 到 @@M@@n@@ 中与 @@M@@n@@ 互素的整数个数，@@M@@V(x)@@ 统计 @@M@@\varphi@@ 在 @@M@@[1,x]@@ 内取到的不同值的个数。计数取值比计数具有给定分解的整数更难：不同整数可以有相同的函数值，而这一差别在渐近公式层面是决定性的。Pillai 1929 年证明取值集密度为零，其后 Erdős、Erdős–Hall 与 Pomerance 逐步推进，Maier 与 Pomerance 1988 年定出主部 @@M@@V(x)=\frac{x}{\log x}\exp\{(C_0+o(1))(\log_3x)^2\}@@，Ford 1998 年又将其精化为只差一个有界乘性因子的估计。卡点在于这个有界因子可能随相位（phase）振荡，上下界夹逼失效。Erdős 与 Hall 1976 年在文末问道：固定 @@M@@c>1@@，是否 @@M@@V(cx)/V(x)\to c@@？Ford 只证得 @@M@@V(cx)-V(x)\asymp_cV(x)@@，极限比值多年悬而未决。
记 @@M@@\log_j@@ 为 @@M@@j@@ 重迭代对数。设 @@M@@a_j=\int_j^{j+1}\log t\,\mathrm dt@@，@@M@@\rho\in(0,1)@@ 为 @@M@@\sum_{j\ge1}a_j\rho^j=1@@ 的唯一根，@@M@@\lambda=\log(1/\rho)@@，@@M@@g_j@@ 为更新序列（renewal sequence）@@M@@g_j=\sum_{d\le j}a_dg_{j-d}@@。令 @@M@@B=\log_2x@@，@@M@@m=\lfloor(\log B-\log_2B)/\lambda\rfloor@@，相位 @@M@@\theta\in[0,1)@@ 为其小数部分，@@M@@G_j=\frac{B^j}{j!\prod_{i\le j}g_i}@@；@@M@@\frac{x}{\log x}G_m@@ 正是 Ford 的计数尺度。
主定理：存在 @@M@@[0,1)@@ 上正的有界函数 @@M@@A(1;\cdot)@@，使得 @@M@@V(x)\sim\frac{x}{\log x}G_mA(1;\theta)@@，且对每个固定实数 @@M@@c>0@@ 有 @@M@@V(cx)/V(x)\to c@@。系数是有限算术公式 @@M@@A_H(1;s)@@ 当 @@M@@H\to\infty@@ 的一致极限，其定义不使用 @@M@@V@@：固定相位 @@M@@s@@，一个尾部见证（tail witness）@@M@@\eta@@ 是满足规定双对数带条件与大小界的一组素数 @@M@@Q_h@@（@@M@@P\le h<H@@）及整数 @@M@@a@@，令 @@M@@w(\eta)=a\prod_hQ_h@@；对每个取值 @@M@@d@@ 收集满足 @@M@@\varphi(w(\eta))=d@@ 的见证集合（固定 @@M@@H@@ 时整体有限），对一族独立指数随机变量的尾事件取并集概率，经容斥（inclusion–exclusion）化为绝对收敛的显式指数级数，再配上前因子 @@M@@\rho^{H(H-1)/2}(\gamma/\alpha_s)^H@@ 即得 @@M@@A_H@@。
伴随定理（最小原像）：设 @@M@@\ell(v)=\min\{n\ge1:\varphi(n)=v\}@@，@@M@@N_k(x)@@ 计数满足 @@M@@v\le x@@ 且 @@M@@kx<\ell(v)\le(k+1)x@@ 的取值个数，则 @@M@@N_k(x)=\frac{x}{\log x}G_m(A(f_k;\theta)+o(1))@@，且二择一：若存在取值 @@M@@d@@ 使 @@M@@\ell(d)>kd@@，则 @@M@@N_k(x)\asymp_kV(x)@@；否则 @@M@@N_k(x)@@ 恒为零。@@M@@k=1,2@@ 属第一种情形；是否对一切 @@M@@k@@ 成立，等价于 @@M@@\ell(d)/d@@ 无界这一公开问题。
证明分三步。先提取长素数前缀：把原像的素因子从大到小排列为 @@M@@p_0\ge p_1\ge\cdots@@，Ford 的结构定理（定理 10、16）断言，几乎所有取值的每一个原像都使双对数坐标 @@M@@u_i=\log_2p_i@@ 落在中心为 @@M@@b_i=\alpha h_i\rho^{-h_i}@@ 的窄带内，且满足单纯形约束 @@M@@\sum_{r>i}a_{r-i}u_r\le\xi_iu_i@@。在两处不同位置切刀 @@M@@R=m-H@@ 与 @@M@@L=m-P@@（@@M@@P=\lfloor\log\log H\rfloor@@）：长前缀 @@M@@p_0,\ldots,p_R@@ 交由连续体积计数，短尾 @@M@@p_{R+1},\ldots,p_L@@ 与余因子 @@M@@a@@ 保留精确的离散算术，固定 @@M@@H@@ 时尾部整体有界；极限次序为先 @@M@@x\to\infty@@（@@M@@H@@ 固定）、再 @@M@@H\to\infty@@。
再控制前缀碰撞：不同长前缀给出同一取值的有序配对总数必须可忽略。抵消公共前缀后得到移位素数乘积的恒等式，证明沿用 Maier–Pomerance 的分层移位素数比较法，并把 Ford 的比较引理改写到本文所需的一组假设之下：先对齐两侧 @@M@@p_i-1@@ 的最大素因子（素数带彼此分离保证对齐位置唯一），再由单纯形的严格松弛取得指数节省 @@M@@\exp(-cB_y/h^4)@@，它足以吸收从残余因子中恢复元组数据的全部代价。随后一个初等的有限映射计数引理把”元组数”转换为”取值数”；并且典型取值的所有原像共享同一前缀，由此得到最小原像的乘法分解 @@M@@\ell(v)=p_0\cdots p_R\ell(d)@@。
最后数最大素数并取体积极限：对 @@M@@p_0@@ 用素数定理，且 @@M@@t=x@@ 与 @@M@@t=x/c@@ 共用同一质量 @@M@@M_1(x;H)@@ 与同一 @@M@@G_m@@，两式相减时未知质量直接消去，立刻得到 @@M@@V(cx)/V(x)\to c@@——这一路完全不需要系数的连续性。再把前缀的倒数素数和换成”尾部见证所允许区域之并”的体积，交集体积是显式的单纯形体积，容斥后令 @@M@@x\to\infty@@，恰收敛到 @@M@@A_H@@ 中的指数项与前因子；一致收敛则借助与 @@M@@H@@ 无关的比较量 @@M@@V(x)\log x/(xG_m)@@（Ford 的双侧估计给出上下界）与”精确相位序列”论证。绕开难点的关键在于：不把尾部平均化，而是精确保留离散尾部，让相位依赖的算术系数从有限容差中显式浮现。
本文暂无 Lean 形式化证明：发布包内 lean/docs/024.md 及比较器文件 TotientAsymptotic.lean 只给出主定理的陈述并留有 sorry，形式化是作为挑战命题而非已完成证明给出的，请以社区核验为准；OpenAI 官方亦声明”未经形式化的结果可能有问题”。论文的结构性起点与尺度估计直接引用 Ford 2013 年修订版（定理 10、16 与双侧估计），而碰撞控制、体积极限与系数构造等关键新步骤均在文内自证。文中引用的同批姊妹结果（存在满足 @@M@@\#\{n:\varphi(n)=v\}>v^{1-\varepsilon}@@ 的极大纤维）研究单个纤维的大小，与本文的取值计数相互独立，并非本文证明的输入。
问 1：证明里最脆弱的一环是什么？
（答：前缀碰撞控制。不同长前缀给出同一取值的有序配对必须可忽略，否则”体积换个数”的翻译就多计。论文把 Maier–Pomerance 的分层移位素数比较法与 Ford 的比较引理改写到本文所需的一组假设之下：对齐两侧 p_i−1 的最大素因子（素数带分离保证对齐位置唯一），再由单纯形的严格松弛取得指数节省 exp(−cB_y/h⁴)，它必须吞下从残余因子恢复元组数据的全部代价——这一不等式是整个计数的账本平衡点。）
问 2：系数 A_H 的一致收敛凭什么成立？
（答：论文借助一个与 H 无关的比较量 V(x)log x/(xG_m)——Ford 的双侧估计恰好给出它的上下界——配合”精确相位序列”论证，把固定相位下的收敛抬升为对相位一致。极限次序也是精心安排的：先 x→∞（H 固定）再 H→∞。若次序颠倒或一致性失守，主定理的系数就只剩次序列陈述。）
问 3：与 Ford 1998 相比真正的新意是什么？
（答：Ford 把 V(x) 定到只差一个有界乘性因子，但因子可能随相位振荡使夹逼失效；本文是此后第一个完整渐近等价，且系数显式保留有限算术数据。方法关键在”不把尾部平均化”——精确保留离散尾部，让相位依赖系数从有限容差中显式浮现。附带落定 Erdős–Hall 1976 年（Erdős 1979 年重提）的固定伸缩问题：V(cx)/V(x)→c。）
问 4：V(cx)/V(x)→c 为什么不需要系数连续？
（答：这是证明的巧妙设计：对 t=x 与 t=x/c，最大素数的素数定理计数共用同一质量 M₁(x;H) 与同一 G_m，两式相减时未知质量直接消去，正则变化性先于系数识别成立。引言明确”两个结论都不假设系数连续性”——绕开了正则变化定理通常需要的连续性条件，也回避了 A(1;θ) 是否连续这个论文未展开的问题。）
问 5：AI 生成证明在这篇上最可能的出错模式？
（答：切刀与极限次序的簿记。R=m−H 与 L=m−P 两处切刀的位置随 x 缓慢漂移，固定 H 时尾部整体有限、容斥并集的体积计算必须逐项对上 A_H 的指数级数与前因子 ρ^{H(H−1)/2}(γ/α_s)^H——这类”有限但结构繁复”的算术系数最易出符号与重数错。特别提示：发布包内 TotientAsymptotic.lean 只有主定理陈述并留有 sorry，形式化是挑战命题而非已完成证明，本文实为未经形式化（formalized: false）状态。另，对 Ford 结构定理的引用锚定 2013 年 7 月 14 日修订版 arXiv，版本敏感。）
问 6：下游还有什么没解决？
（答：伴随定理给出最小原像计数 N_k(x) 的二择一：有种子取值 d 使 ℓ(d)>kd 则 N_k(x)≍V(x)，否则恒为零；k=1,2 属前者，其余 k 的种子条件未判定。Erdős 的老问题”ℓ(d)/d 是否无界”仍开放。”保留离散尾部”的技术对其他数论函数（如 σ）的取值计数有迁移潜力，论文未展开。）
总评
（把二十多年的有界因子估计推进为显式渐近等价、顺手落定 Erdős–Hall 问题，是 totient 计数的主干进展；但 Lean 侧仅存含 sorry 的陈述、关键碰撞与系数构造全靠自证，核验仍需解析数论专家完整过账。）