神经网络找到高幅水波候选解，区间算术与Lean把残差界变成可核验的数学陈述
核心概要
物理信息神经网络此前只能给出采样点上的小残差，无法说明连续域上的误差有多大。这条流程让网络在共形坐标的Babenko方程上搜索高幅重力—毛细波，经多级神经修正、傅里叶投影与牛顿抛光把最大采样残差降低约七个数量级，再把候选冻结为显式三角多项式，用区间算术给出连续残差的严格一致上界，并在Lean中机器核验从数值界到最终残差定理的推导。
深度剖析
高幅非线性水波的候选解现在可以带一份严格的连续残差证书，而不只是若干采样点上的小残差。 此前物理信息神经网络能给出残差极小的数值解，但采样残差小并不构成对连续残差或相对精确解误差的严格界。 对冻结后的显式三角多项式，区间算术给出近机器精度的一致残差上界，与网络阶段观测到的近双精度残差处于同一量级。
搜索在共形坐标下的Babenko方程上直接进行，波面、波速以及延续实验中的表面张力参数一并由方程本身学出，不使用训练数据。 同一套网络结构与基于残差的优化框架配合不同的物理与归一化约束，分别复现纯重力Stokes波、纯毛细Crapper波和重力—毛细Wilton涟漪三类高幅解族。 以高幅Wilton涟漪为种子、让表面张力随波面与波速一起变化做延续，得到傅里叶成分、参数取值与自由面几何都明显偏离原Wilton分支的新候选解。
认证把神经网络产物冻结为固定系数的余弦级数，此后证明与网络权重和训练轨迹无关。 浮点舍入、傅里叶截断、非线性项混叠以及从网格到连续域的四类误差被合并进同一个显式上界。 Julia/Arb以区间算术完成主体计算并导出精确有理端点，Lean 4把这些端点作为显式数值假设，核验到最终残差定理的推导，且证明不含sorry占位。
启示与展望
报告认证的是一个给定有限三角多项式在固定有理参数下的Babenko方程残差一致上界，以及毛细分母的正下界；这是关于所给有限级数的残差定理，不是精确邻近水波解的存在性或唯一性定理。
作者指出，要证明附近存在精确解，还需对受约束的线性化Babenko算子给出严格逆界并控制非线性余项，这些不在本次证书之内。新候选解族在可及的数值延续范围内始终表现为有限振幅，作者据此推测它可能不来自线性模态的分岔，但确认其是否真正与小幅谱断开仍需进一步分析。Lean并不独立重算Arb的区间计算，数值界仍是形式化层的信任输入。