AI 中文总结
该论文通过计算机辅助证明，验证了对数螺线在未知直线搜索问题中的最优性，其竞争比为13.8111351794611，方法涉及万有覆盖、松弛控制与区间算术验证。
AI 中文摘要
一艘船从平面上的某一点出发，以单位速度移动；它必须到达一条未知的直线，该直线的距离和方向均未知。一条路径的竞争比是，对所有可能的直线，到达该直线的时间与其距离之比的 supremum（上确界）。Baeza-Yates、Culberson 和 Rawlins 猜想，具有比率 $C_{\mathrm{sp}} = 13.8111351794611\ldots$ 的对数螺线是最优的。我们给出一个计算机辅助证明。路径是任意的：从起点出发的距离和极角都可以减小。该证明将已找到的方向集合提升到圆的万有覆盖上，在那里展开极角只能使其增大（直线上的 Kneser-Poulsen 定理）；一个带有单调最终源的簿记不等式，将覆盖的测度界定为三状态松弛控制问题的奖励，其中向内运动是普通控制，而低于保证圆盘的偏移是脉冲。一个显式的 $C^1$ 存储函数，即一个张量三次 B 样条加上一个闭式项，满足该问题在螺线水平上的耗散不等式，并且仅在螺线处取等号；这通过约 $10^6$ 个 Arb 区间算术盒子、一个精确的 jet 以及在螺线处的区间 Hessian 来验证。
英文摘要
A ship starts at a point of the plane and moves at unit speed; it has to reach an unknown straight line, of which neither the distance nor the direction is known. The competitive ratio of a path is the supremum, over all lines, of the time at which the line is reached divided by its distance. Baeza-Yates, Culberson and Rawlins conjectured that a logarithmic spiral, with ratio $C_{\mathrm{sp}} = 13.8111351794611\ldots$, is optimal. We give a computer-assisted proof. Paths are arbitrary: the distance from the start and the polar angle may both decrease. The proof lifts the set of found directions to the universal cover of the circle, where unfolding the polar angle can only increase it (Kneser-Poulsen on the line); a bookkeeping inequality with a monotone final source then bounds the covered measure by the reward of a three-state relaxed control problem, in which inward motion is an ordinary control and excursions below the guaranteed disk are impulses. An explicit $C^1$ storage function, a tensor cubic B-spline plus a closed-form term, satisfies the dissipation inequalities of that problem at the spiral's level and is tight only at the spiral; this is verified with about $10^6$ boxes of Arb ball arithmetic, an exact jet and an interval Hessian at the spiral.
Comments20 pages (13 of main text, then four appendices), 3 figures, 1 table
