Proof-Carrying Analytic Approximation: Local-to-Global Evidence Transport at Encoding Cost

Abstract

Under quasi-uniform refinement, bounded local-encoding hypotheses, and local $W^{r,2}$ approximation of order $r\ge 2$ in a rational piecewise-polynomial presentation of $W^{1,2}(0,1)$, carrying the complete proof genealogy up to the level required by an accuracy $\epsilon$ costs the same asymptotic bit order as the finest-level conventional coefficient encoding. If $B_n=\Theta (M_n{\beta }_n)$ denotes that level-$n$ encoding size, our compiler transports supplied local approximation and overlap witnesses through exact partition-of-unity synthesis and geometric refinement to a represented limit with total certificate size $O(B_{m(\epsilon )})$, where $m(\epsilon )=O(\log (1/\epsilon )/(r-1))$. The construction makes no oracle query to an independently supplied semantic target name ($Q_{\mathrm{target}}=0$). When ${\beta }_n=O(n+1)$, this becomes $O({\epsilon }^{-1/(r-1)}(1+\log (1/\epsilon )))$. The surrounding framework is intentionally separated from this resource theorem. Every real computable Banach presentation admits a uniformly computable linear isometric embedding into standard computable $C([0,1])$, with computable inverse on its represented range. Complete metric evidence with rational strict slack collapses extensionally to the represented analytic metric once effective names are available, while chosen evidence transformations retain construction history and resource information. For the Lipschitz grammar used here, qualitative evidence-local lifting is canonical; the nontrivial question is therefore which evidence is retained and at what cost.

35 pages. Version 3 substantially reconstructs the paper. Main results include an effective linear isometric universality theorem for real computable Banach presentations and a quantitative proof-carrying PUFEM/refinement theorem with zero target-name queries and same-order retained-genealogy size. Version correspondence is recorded in the manuscript