The Proper-Fit Boundary: A Semi-Heuristic Criterion in Error Approximation and Its Formalization Limits

There is a stopping problem in error approximation: at what point can the error be said to be "exactly right", rather than "still reducible" or "already fitting noise"? This paper writes the answer to that question as a criterion, IsOptimalFit(W, gamma) := E_W(gamma) = inf over gamma' of E_W(gamma'), where E_W is the error function induced by a bias-variance type profile, and at the same time delimits the scope within which the criterion applies. The strict core of the criterion is fully formalized. Once the noise scale sigma is paired with a boundary point it is locked by that profile to inf E_W (Theorem 3.2), so the criterion contains no free parameter; uniqueness derives entirely from strict convexity, cannot be weakened to convexity and cannot be replaced by monotonicity (Theorems 6.1, 6.4, 6.5); any criterion that reads only the error sequence cannot, in terms of expressiveness, decide the existence of a boundary (Theorems 5.2-5.4). The heuristic shell of the criterion is marked out just as explicitly: reading inf E_W as a statistical noise scale is a semantic convention, and "the geometric-combinatorial double bound determines satisfiability" is a modelling assumption; neither is a theorem. Accordingly the paper separates the criterion into a theorem layer, a convention layer, and an empirical layer, and argues that conflating the three is precisely the source of the long-standing difficulty of discussing such criteria rigorously. An auxiliary combinatorial result tightens the constants of computability: for a single-valued encoding with n thresholds per dimension, the cell count is at most (n+1)^d rather than 2^(dn), and this bound is attainable, hence Theta((n+1)^d) (Theorem 10.7 and its sharpness); correspondingly the computability ceiling changes from log2(B)/d to B^(1/d) - 1. Experiments on real data show that the left-hand side of this inequality is insufficient to predict the optimal resolution, because the transfer from cell width to error depends on a Lipschitz assumption, and that assumption is falsified on two of the public datasets (Section 11.6). The conclusion is conditional: given an operable noise scale, the boundary exists, is unique (under strict convexity), and can be fully characterized; otherwise no criterion that reads only the error sequence can decide whether the boundary exists. All rigorous statements have been machine-verified in Lean 4 and Mathlib, with no sorry and no custom axioms. Contents of this deposit. The paper is provided as PDF and LaTeX source. The file proper-fit-boundary-package.zip contains the complete artifact: the paper in both English and Chinese (Markdown and Word), a standalone appendix on the formalization engineering, the full reference list, the experiment design record, the Lean 4 library (44 modules, 679 theorems, 182 definitions, no sorry), the verification scripts, and the experiment code and data.