Sequence Estimation of the Noise Scale: A Two-Channel Stopping Criterion

The stopping criterion writes "the error falls exactly on the boundary between fitting and overfitting" as E_W(gamma) = inf E_W. The predecessor (DOI 10.5281/zenodo.23752685) fully formalizes this criterion and at the same time establishes a negative result: if the noise scale sigma can be obtained only from the profile W, or only from a criterion that reads the error sequence, then it is non-identifiable. This paper identifies and implements a third route: estimate sigma from the residual history sequence, and substitute it back into the criterion. It differs from both routes that the predecessor closed off, because the former reads only the profile and the latter reads only ratios of the sequence, whereas the present method reads both the profile (which supplies the error landscape) and the sequence (which supplies the scale). Hence neither of the two separation theorems of the predecessor applies. The formalization provides eleven theorems, two of which form the backbone of this paper: once the estimate satisfies the criterion it is locked to the infimum of the profile (Theorem 5.1); if the estimate differs from the infimum, then no boundary exists (Theorem 5.2). The latter turns sigma from an irrefutable convention into a hypothesis that can be refuted by data. The experiments are tested on four public datasets against pre-registered criteria. Three of the four pass: under the construction in which the two-channel data blocks are disjoint, the model is fixed, and the estimator is the root mean square, the relative deviations between the sequence estimate and the profile infimum are 1.6%, 4.8% and 39%, respectively (the fourth is 68%, in the opposite direction, and unexplained). The window dependence of the estimator is a factor of 1.1 to 1.7. We also state the three conditions of this route and one unresolved exception, and set out one by one, as controls, why the remaining four estimation routes for sigma are closed. Contents of this deposit. The paper is provided as PDF and LaTeX source. The file sigma-from-sequence-package.zip contains the complete artifact: the paper and its three appendices in both English and Chinese (Markdown and Word), the experiment design record, the Lean 4 library (45 modules, 696 theorems, no sorry), the verification scripts, and the experiment code and data.