发表机构
Stony Brook University（石溪大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对一维任意移动单区间的模板计算，提出基于总变差的调度，实现近线性工作量与精确结果，并在Lean 4中机器验证。
AI 中文摘要
模板计算（stencil computation）反复根据网格中每个单元在上一时间步的邻居值来更新该单元的值。直接在N个单元上模拟T步的代价为Theta(NT)，而自Ahmad等人开始的一系列工作通过将多个时间步组合成一个线性算子，并使用快速傅里叶变换（FFT）来应用该算子，从而降低了这一代价。该技术需要知道在组合步结束时哪些单元仍将遵循相同的算子，而在自由边界问题中，情况并非如此：由给定规则支配的区域由解确定，并随解的演化而移动。我们研究一维空间、具有时变系数的三点模板，以及一个计算区域，该区域是一个单一区间，其两个端点在每一步都会移动任意量，且该区域是实时揭示的。设B为时间范围加上边界轨迹的总变差。我们给出一个调度，其工作量为O((B+N) log T log(N+B))，跨度为O(T log T log(N+B))，并证明其计算出的值是精确的。对于移动区域，现有最佳界要求其边界每时间步最多移动一个单元。我们取消了这一要求，且并未因此损失任何东西：满足该要求的边界有B <= 3T，因此我们的界在先前结果覆盖的每条轨迹上仍保持近线性。在其他情况下，B仅随边界实际移动的距离增长——一次宽度为N的跳跃代价为T + 2N。总变差之所以足够，是因为两个端点在任意长度的时间窗口内所触及的一切都位于两个区间内，每个端点一个。这一条件无法放宽：对于p个区域，界会退化p倍，且当p = sqrt(T)时，存在一个实例，其工作量为Theta(T^{3/2})，而B + N = Theta(T)。所有结果均在Lean 4中经过机器验证，除了经典的卷积界，该界作为接口导入。
英文摘要
A stencil computation repeatedly updates every cell of a grid from its neighbours' values at the previous timestep. Simulating T steps on N cells directly costs Theta(NT), and a line of work beginning with Ahmad et al. reduces this by composing many timesteps into one linear operator and applying it with a Fast Fourier Transform. That technique needs to know which cells will still obey the same operator when the composed step ends, and in a free-boundary problem they do not: the region governed by a given rule is determined by the solution and moves as it evolves. We study one spatial dimension, a three-point stencil with time-varying coefficients, and a computed region that is a single interval whose two endpoints move by arbitrary amounts at every step, revealed online. Let B be the horizon plus the total variation of the boundary trajectory. We give a schedule whose work is O((B+N) log T log(N+B)) and whose span is O(T log T log(N+B)), and we prove that the values it computes are exact. The best existing bound for a region that moves requires its boundary to travel at most one cell per timestep. We drop that requirement and lose nothing by it: a boundary obeying it has B <= 3T, so our bound stays near-linear on every trajectory the earlier result covers. Elsewhere, B grows only by the distance the boundary actually travels -- one jump of width N costs T + 2N. The reason total variation suffices is that everything the two endpoints touch over a time window of any length lies in two intervals, one per endpoint. This cannot be relaxed: with p regions the bound degrades by a factor p, and at p = sqrt(T) there is an instance on which the work is Theta(T^{3/2}) while B + N = Theta(T). All results are machine-checked in Lean 4, apart from the classical convolution bound, which is imported as an interface.
