AI 中文总结
研究黄金三角形的贝尔曼森林迷路问题，通过引入平衡支持校准等方法，得出从未知位置到其边界的最短曲线是对称七段路径，长度为\(C\)，这是底角小于\(45^{\circ}\)等腰三角形的首个精确最优解，Lean 4验证了相关证书和边界。
AI 中文摘要
我们解决了黄金三角形\(G\)（等腰三角形，腰长为\(1\)，顶角为\(108^{\circ}\)）的贝尔曼森林迷路问题：从未知起始位置和方向到达\(G\)边界的最短曲线是由线段、圆形肩部和切线组成的对称七段路径，长度精确为\(C = 1.282676025459\ldots\)。据我们所知，这是第一个证明的底角小于\(45^{\circ}\)的等腰三角形的精确最优解。曲线参数来自一个孤立的四次根，\(C\)是超越数。证明引入了平衡支持校准：基于三角形三条法线的线性关系构建一个加权的逃逸不等式族，通过十八个精确支持窗口由候选者精确饱和，并同时面对每个更短的竞争者。沿着法向扇进行聚合将校准压缩为一个有限的零和支持向量族；分部求和然后在运行后缀平衡（账本）保持在单位圆盘内时，根据路径长度对其总和进行界定。局部双间隙手术和循环双调性迫使最短的假设反例进入账本容忍的时间顺序。Lean 4验证了两个有限代数证书族以及可重复使用的离散账本恒等式和边界。
英文摘要
We solve Bellman's lost-in-a-forest problem for the golden gnomon $G$, the isosceles triangle with equal sides $1$ and apex angle $108^\circ$: the shortest curve guaranteed to reach the boundary of $G$ from an unknown starting position and heading is a symmetric seven-piece path of segments, circular shoulders, and tangents, of exactly determined length $C=1.282676025459\ldots$. To our knowledge, this is the first proved exact optimum for an isosceles triangle whose base angle is below $45^\circ$. The curve's parameters come from one isolated quartic root, and $C$ is transcendental. Equivalently, $C^{-1}G$ is the smallest homothetic golden-gnomon cover of all unit arcs. The proof introduces a balanced support calibration: one weighted family of escape inequalities, built on the linear relation among the triangle's three normals, exactly saturated by the candidate, through eighteen exact support windows, and confronting every shorter competitor at once. Aggregation along the normal fan compresses the calibration to a finite zero-sum family of supported vectors; summation by parts then bounds its total by path length whenever the running suffix balance, the ledger, stays in the unit disk. A local two-gap surgery and cyclic bitonicity force a shortest hypothetical counterexample into exactly the temporal order the ledger tolerates. Lean 4 verifies the two finite algebraic certificate families and the reusable discrete ledger identities and bounds.
Comments27 pages, 3 figures. Lean 4 formalization and independent audits are included as ancillary files and maintained at https://github.com/atemerev/gnomon
