From Mathematical to Executable Certificates for Machine Unlearning

# From Mathematical to Executable Certificates for Machine Unlearning
Source: [https://arxiv.org/html/2610.02268](https://arxiv.org/html/2610.02268)
Ziyu Zhao††thanks:Equal contribution\.Xinyu Wang11footnotemark:1Affiliation:McGill UniversityXiao\-Wen ChangAffiliation:McGill UniversityYixuan He††thanks:Corresponding author\.Affiliation:Arizona State University

###### Abstract

Machine unlearning is needed when data must be removed because of deletion requests, outdated records, or data\-quality concerns, while retraining from scratch can be costly\. Certified machine unlearning methods provide mathematical guarantees, while deployed systems release concrete finite\-precision artifacts produced by software\. To bridge the gap between mathematical guarantees and practical deployment, we introduce Executable Release Certification \(ExecCert\), a release\-time layer that certifies the candidate artifact considered for release\. ExecCert either closes a method’s native certificate for the executed candidate or applies Retraining\-Reference Release Verification \(RRV\) to certify fidelity to current retain\-set retraining\. Sequential deletion makes the latter nontrivial because the exact retain\-set reference and the stored numerical state evolve separately\. For frozen representations with a mutable ridge head, we develop an incremental realization of RRV that maintains certified evidence across deletion requests rather than reconstructing it at each release\. On four published unlearning implementations, ExecCert preserves valid certificates, changes release decisions, tightens conservative bounds, and identifies the retraining\-reference fidelity supported by concrete outputs\. In sequential\-service experiments, RRV eliminates false releases caused by stored\-equation verification while closely tracking realized error, and incremental certification remains cheaper than both fresh and maintained verified\-factor alternatives once release checks become sufficiently frequent\.

## 1Introduction

Machine\-learning models may need to remove the influence of training records when users withdraw consent, data become outdated, or errors are discovered; regulations such as the EU’s right to be forgotten provide an additional motivation\. Retraining from scratch on the retained data gives a natural reference but can be costly, motivating machine unlearning methods that seek to approximate retraining at lower deletion cost\([Ginart et al\., 2019](https://arxiv.org/html/2610.02268#bib.bib1);[Guo et al\., 2020](https://arxiv.org/html/2610.02268#bib.bib2);[Sekhari et al\., 2021](https://arxiv.org/html/2610.02268#bib.bib4);[Gupta et al\., 2021](https://arxiv.org/html/2610.02268#bib.bib5)\)\. Certified unlearning further provides mathematical guarantees relating an efficient deletion mechanism to this reference\([Guo et al\., 2020](https://arxiv.org/html/2610.02268#bib.bib2);[Sekhari et al\., 2021](https://arxiv.org/html/2610.02268#bib.bib4);[Gupta et al\., 2021](https://arxiv.org/html/2610.02268#bib.bib5);[Chien et al\., 2024](https://arxiv.org/html/2610.02268#bib.bib6);[Zhang et al\., 2024b](https://arxiv.org/html/2610.02268#bib.bib3);[Koloskova et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib12);[Pandey et al\., 2026](https://arxiv.org/html/2610.02268#bib.bib11)\)\. However, a deployed system releases a concrete finite\-precision artifact produced by software, rather than the mathematical object analyzed by the guarantee\. This raises a distinct deployment question:*does the artifact actually considered for release satisfy the intended certificate or retraining\-reference contract?*

Sequential deletion makes this deployment\-level question especially important\. After each request, the exact retain\-set system changes, while the deployed service advances a separate finite\-precision state through rounded updates\. These two systems do not always coincide: a candidate may solve the stored equation accurately, sometimes even with zero stored residual, but still violate the contract defined relative to current retain\-set retraining\. Verifying the stored computation alone is therefore insufficient; release\-time certification must connect the executed artifact to the intended reference\.

We introduce*Executable Release Certification*\(ExecCert\) to fill the gap between the two systems\. Before a candidate is released, the deployment fixes a release contract, and ExecCert certifies whether the concrete executed artifact satisfies that contract\. It supports two paths: when an unlearning method already exposes a certificate quantity,*native closure*rigorously encloses that quantity for the executed candidate; when the contract is defined relative to retraining on the current retain set,*Retraining\-Reference Release Verification*\(RRV\) instead certifies the candidate directly against that reference\. In both cases, the output generator, release contract, and verifier remain separate components\.

DeletionrequestsUnlearninggeneratorExecutable certificationNativeclosureRRVPolicygate✓Release✗Withhold /Repairrepair, recompute, or re\-encodeFigure 1:ExecCert certifies a concrete unlearning artifact before release\.The generator’s finite\-precision output is checked against a predeclared contract through native\-certificate closure or retraining\-reference verification \(RRV\)\. Only certified artifacts pass the policy gate; an inconclusive candidate is withheld or repaired and then recertified\.Our main sequential realization is*Incremental RRV*for ridge regression heads with symmetric positive\-definite \(SPD\) normal matrices\. RRV itself certifies only the concrete candidate considered for release\. During the preceding deletion sequence, Incremental RRV maintains certified relations between the service’s finite\-precision statistics and the exact retain\-set statistics, together with reusable inverse\-defect evidence\. Heredddenotes the feature dimension of each ridge regression head\. Guarded rank\-one transitions update this proof state inO⁡\(d2\)O\(d^\{2\}\)work\. When a candidate is considered for release, the maintained evidence is composed into its retraining\-reference certificate\. Alternatively, On\-demand RRV constructs the required evidence when certification is requested\.

Experiments on four published unlearning implementations and sequential services show that ExecCert changes release decisions, tightens or preserves existing certificates, and characterizes the retraining\-reference fidelity supported by emitted outputs\. In sequential services, RRV prevents false releases admitted by stored\-equation checking while closely tracking realized error; on frozen 3B representations with a mutable ridge head, Incremental RRV remains cheaper than both fresh and maintained verified\-factor alternatives once release checks become sufficiently frequent\.

Contributions\.We make three contributions\. First, we formalize*executable release certification*as a distinct layer between a mathematical unlearning mechanism and the concrete artifact considered for release\. ExecCert supports both rigorous closure of a method’s native certificate and certification against current retain\-set retraining \([Sections3](https://arxiv.org/html/2610.02268#S3)and[4\.1](https://arxiv.org/html/2610.02268#S4.SS1)\)\. Second, we develop Incremental RRV for sequential deletion, maintaining certified relations between finite\-precision service state and the exact retain\-set system together with reusable inverse\-defect evidence\. Guarded rank\-one transitions update this proof state inO⁡\(d2\)O\(d^\{2\}\)work \([Sections4](https://arxiv.org/html/2610.02268#S4)and[4\.3](https://arxiv.org/html/2610.02268#S4.SS3)\)\. Third, we evaluate ExecCert on four published unlearning implementations and sequential services, showing that executable certification has practical consequences: it can change release decisions, tighten or preserve existing certificates, prevent false releases, and amortize verification when certification is frequent \([Section5](https://arxiv.org/html/2610.02268#S5)\)\.

## 2Related Work

Full retraining on the retain set is a natural exact reference but incurs the cost of processing the surviving data\. Exact unlearning targets the same output distribution and need not literally rerun the original training algorithm; certified approximate removal instead applies an efficient update and bounds its deviation from the declared reference, through influence or Newton steps, randomized mechanisms, or guarantees that compose across a deletion sequence\([Guo et al\., 2020](https://arxiv.org/html/2610.02268#bib.bib2);[Sekhari et al\., 2021](https://arxiv.org/html/2610.02268#bib.bib4);[Gupta et al\., 2021](https://arxiv.org/html/2610.02268#bib.bib5);[Chien et al\., 2024](https://arxiv.org/html/2610.02268#bib.bib6);[Koloskova et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib12);[Zou et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib10);[Pandey et al\., 2026](https://arxiv.org/html/2610.02268#bib.bib11)\)\. These results differ in what they bound, but share an assumption: the analysis governs the mathematical update, and the deployed artifact is taken to realize it\. A second line asks instead how an external party can be convinced that deletion happened, auditing execution traces and provenance, probing the released model for residual influence of the deleted records, or attaching cryptographic proofs that a prescribed computation was carried out\([Thudi et al\., 2022](https://arxiv.org/html/2610.02268#bib.bib17);[Weng et al\., 2024](https://arxiv.org/html/2610.02268#bib.bib18);[Eisenhofer et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib19);[Zhang et al\., 2024a](https://arxiv.org/html/2610.02268#bib.bib20);[Maheri et al\., 2026](https://arxiv.org/html/2610.02268#bib.bib29)\)\. That evidence concerns*which computation ran*, for a verifier that distrusts the operator\. Ours is the complement: the verifier is internal, the computation known, and the question is whether the artifact about to be released meets a contract stated in exact arithmetic\. The two compose, since proving that the prescribed update ran says nothing about the rounding it accumulated\.

That numerical question has its own literature\. Finite precision is known to break guarantees derived in exact arithmetic, in differential privacy, robustness certification, and verified training\([Mironov, 2012](https://arxiv.org/html/2610.02268#bib.bib24);[Voracek and Hein, 2023](https://arxiv.org/html/2610.02268#bib.bib25);[Szász et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib26);[Jin et al\., 2024](https://arxiv.org/html/2610.02268#bib.bib21)\), and verified numerics supplies the countermeasure: rigorous enclosures for linear\-system residuals, approximate inverses, and low\-rank updates\([Krawczyk, 1969](https://arxiv.org/html/2610.02268#bib.bib13);[Oishi and Rump, 2002](https://arxiv.org/html/2610.02268#bib.bib15);[Rump, 2010](https://arxiv.org/html/2610.02268#bib.bib14);[Hager, 1989](https://arxiv.org/html/2610.02268#bib.bib16)\)\. These tools certify a solution against a*fixed*system\. Cholesky downdates and iterative refinement provide classical ways to update a numerical solve\([Higham, 2002](https://arxiv.org/html/2610.02268#bib.bib7);[Rump, 2010](https://arxiv.org/html/2610.02268#bib.bib14)\); maintaining such a factor does not by itself verify its relation to the changing exact system, so factor validation and residual enclosures remain part of a release certificate\. Sequential deletion removes that fixture, since the retain\-set system moves with every request while the service advances a separately rounded state, so our ridge regression realization maintains a certified relation between the two and converts it at release time into a certificate against the current reference\. ScaleGUN studies a related transfer for graph propagation\([Yi and Wei, 2025](https://arxiv.org/html/2610.02268#bib.bib27)\); RRV instead transfers from finite\-precision service state to the retain\-set system\.

## 3From Mathematical to Executable Certificates

An unlearning generator processes a declared set or sequence of deletion requests and produces a finite\-precision candidateθ~\\widetilde\{\\theta\}\. The deployment fixes an admissible set𝒜\\mathcal\{A\}independently of that candidate\. ExecCert returnsCertifiedonly after establishingθ~∈𝒜\\widetilde\{\\theta\}\\in\\mathcal\{A\}; otherwise the policy gate may repair, recompute, re\-encode, or withhold the candidate\.

For evaluation, a candidate is*conforming*when it belongs to𝒜\\mathcal\{A\}, and a*false release*is a nonconforming candidate returned asCertified\. AnInconclusivecandidate may still conform; a*released artifact*is one that passes the policy gate\.

Notation\.We writeθR\\theta^\{\\mathrm\{R\}\}for the exact\-real retraining reference after the declared deletions andθ~\\widetilde\{\\theta\}for the executed candidate\. Hats denote computed verifier quantities and circles exact\-real evaluations of computed intermediates;[SectionC\.1](https://arxiv.org/html/2610.02268#A3.SS1)gives the remaining floating\-point notation\.

### 3\.1Two ExecCert Paths

These paths correspond to two release requirements\. Some deployments need to verify a method’s own certificate after finite\-precision execution; others specify fidelity to retraining on the current retain set, which a native certificate may not express\. Native closure addresses the first requirement, whereas RRV addresses the second\.

##### Native\-certificate closure\.

This path is appropriate when an unlearning method already specifies a certificate of the formq⁡\(θ,ℐ\)≤bq\(\\theta;\\mathcal\{I\}\)\\leq b, whereqqis the source certificate quantity,bbits prescribed threshold, andℐ\\mathcal\{I\}any committed inputs or auxiliary state required by the source method\. This defines the admissible set𝒜native=\{θ:q⁡\(θ,ℐ\)≤b\}\\mathcal\{A\}^\{\\mathrm\{native\}\}=\\\{\\theta\\colon q\(\\theta;\\mathcal\{I\}\)\\leq b\\\}\. ExecCert does not change this condition: it constructs a rigorous upper boundq⁡\(θ~,ℐ\)≤q\+q\(\\widetilde\{\\theta\};\\mathcal\{I\}\)\\leq q^\{\+\}for the executed candidate and returnsCertifiedwheneverq\+≤bq^\{\+\}\\leq b\. Native closure therefore certifies the concrete finite\-precision artifact under the source method’s own certificate\.

##### Retraining\-reference certification\.

This path is needed when a method’s native certificate does not quantify how close its executed output is to retraining on the current retain set\. When a deployment requires this fidelity directly, ExecCert uses*Retraining\-Reference Release Verification*\(RRV\)\. RRV defines a uniquely specified exact\-real targetθR\\theta^\{\\mathrm\{R\}\}from the declared training objective, mutable model component, and contract inputs\. For a predeclared distanceddand toleranceτ\>0\\tau\>0, the release contract requiresd⁡\(θ~,θR\)≤τd\(\\widetilde\{\\theta\},\\theta^\{\\mathrm\{R\}\}\)\\leq\\tau\. Rather than computingθR\\theta^\{\\mathrm\{R\}\}exactly, RRV certifies this contract by constructing a rigorous upper bound on the distance\.

For the Euclidean parameter contract, this takes the form

‖θ~−θR‖F≤C\.\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq C\.\(1\)HowCCis obtained depends on the model class\. For ridge regression heads with symmetric positive\-definite \(SPD\) normal matrices, On\-demand RRV constructs the required proof information for the candidate, whereas Incremental RRV maintains it while deletion requests are processed\. The latter updates certified numerical state through rank\-one transitions\. For differentiable strongly convex heads, On\-demand RRV instead uses a post\-update gradient certificate, coveringL2L\_\{2\}\-regularized logistic and softmax heads\.

### 3\.2Contracts Derived from the RRV Bound

The absolute boundCCcan be translated into several release contracts\. For relative parameter fidelity, denote the predeclared tolerance byτpar\\tau\_\{\\rm par\}\. The reverse triangle inequality gives

‖θ~−θR‖F‖θR‖F≤C‖θ~‖F−C,\\frac\{\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\}\{\\left\\lVert\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\}\\leq\\frac\{C\}\{\\left\\lVert\\widetilde\{\\theta\}\\right\\rVert\_\{F\}\-C\},\(2\)whenever‖θ~‖F\>C\\left\\lVert\\widetilde\{\\theta\}\\right\\rVert\_\{F\}\>C, so the contract is certified when the right\-hand side is at mostτpar\\tau\_\{\\rm par\}\.

A deployment may instead care about outputs on a fixed set of input representationsZ∈ℝm×dZ\\in\\mathbb\{R\}^\{m\\times d\}, declared independently of the candidate\. For a parameter matrix withccoutput columns, it may require

‖Z⁡\(θ~−θR\)‖Fm​c≤τ,\\frac\{\\left\\lVert Z\(\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\)\\right\\rVert\_\{F\}\}\{\\sqrt\{mc\}\}\\leq\\tau,\(3\)for which the parameter certificate immediately gives‖Z⁡\(θ~−θR\)‖F≤‖Z‖2​C\\left\\lVert Z\(\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\)\\right\\rVert\_\{F\}\\leq\\left\\lVert Z\\right\\rVert\_\{2\}C, while[Section4](https://arxiv.org/html/2610.02268#S4)develops a tighter error\-centered certificate that preserves the error direction, and the margin conditions in[Corollary1](https://arxiv.org/html/2610.02268#Thmcorollary1)further imply per\-row decision agreement\. Contracts are checked separately; the same absolute bound also supports the randomized\-release and output\-format interfaces in[Sections4\.4](https://arxiv.org/html/2610.02268#S4.SS4)and[4\.4](https://arxiv.org/html/2610.02268#S4.SS4.SSS0.Px1)\.

## 4Retraining\-Reference Release Verification

Native\-certificate closure is method\-specific once the source certificate quantity is fixed; its concrete instantiations appear in[Section5\.3](https://arxiv.org/html/2610.02268#S5.SS3)\. The main technical development is therefore RRV, which must certify an executed candidate against a retraining reference that is not explicitly computed\.

RRV can construct certificate evidence in two ways\. On\-demand RRV constructs the required evidence when certification is requested, whereas Incremental RRV reuses numerical state maintained across deletion requests\. The latter introduces an additional obligation: the maintained finite\-precision state must itself be certified against the exact current retain\-set system before it can support a release certificate\. Our ridge regression realization supports both paths through residual and inverse\-defect bounds; for differentiable strongly convex heads, On\-demand RRV uses a post\-update gradient certificate\.

The interface in[Section3](https://arxiv.org/html/2610.02268#S3)concerns a single candidate after a declared deletion sequence\. From this point onward, we index internal service state by deletion stepttonly to describe how incremental evidence evolves\. The same machinery also accommodates long\-running services that expose intermediate snapshots, in which case a declared subset of internal states may serve as release checkpoints\.

### 4\.1Release\-Time RRV Certificates

For a candidate considered for release, RRV must bound its distance to the exact retraining referenceθR\\theta^\{\\mathrm\{R\}\}without explicitly computing that reference\. We give two constructions of this parameter\-error bound\.

##### Ridge regression forward certificate\.

Let the exact retraining reference satisfyH​θR=BH\\theta^\{\\mathrm\{R\}\}=BwithH∈ℝd×dH\\in\\mathbb\{R\}^\{d\\times d\}nonsingular, and letPPapproximateH−1H^\{\-1\}\. SinceP⁡\(B−H​θ~\)=P​H​\(θR−θ~\)P\(B\-H\\widetilde\{\\theta\}\)=PH\(\\theta^\{\\mathrm\{R\}\}\-\\widetilde\{\\theta\}\), the corrected residual would equal the parameter error ifP=H−1P=H^\{\-1\}\. With an approximate inverse, the verifier instead controls both the inverse defect and the corrected residual:

‖Id−P​H‖2≤δ<1,‖P⁡\(B−H​θ~\)‖F≤ρ\.\\left\\lVert I\_\{d\}\-PH\\right\\rVert\_\{2\}\\leq\\delta<1,\\qquad\\left\\lVert P\(B\-H\\widetilde\{\\theta\}\)\\right\\rVert\_\{F\}\\leq\\rho\.\(4\)
###### Lemma 1\(Retraining\-reference forward certificate\)\.

Under[Equation4](https://arxiv.org/html/2610.02268#S4.E4),

‖θ~−θR‖F≤C:=ρ1−δ\.\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq C:=\\frac\{\\rho\}\{1\-\\delta\}\.

##### Strongly\-convex post\-update certificate\.

For a differentiable strongly convex objective, RRV can instead construct the parameter certificate directly from the final candidate\. Ifg\+g^\{\+\}upper\-bounds its gradient norm under the current retain\-set objective andμ−\\mu^\{\-\}lower\-bounds the objective’s strong\-convexity constant, thenC=g\+/μ−C=g^\{\+\}/\\mu^\{\-\}bounds the candidate’s distance to the exact minimizer\. This post\-update construction requires no inverse proof state and applies, for example, toL2L\_\{2\}\-regularized logistic and softmax heads\. The formal statement and executable construction appear in[Propositions3](https://arxiv.org/html/2610.02268#Thmproposition3)and[D\.1](https://arxiv.org/html/2610.02268#A4.SS1)\.

For fixed readouts, the ridge regression construction admits a tighter directional refinement\. For a predeclared set of input representationsZ∈ℝm×dZ\\in\\mathbb\{R\}^\{m\\times d\}, the parameter certificate gives‖Z⁡\(θR−θ~\)‖F≤‖Z‖2​C\\left\\lVert Z\(\\theta^\{\\mathrm\{R\}\}\-\\widetilde\{\\theta\}\)\\right\\rVert\_\{F\}\\leq\\left\\lVert Z\\right\\rVert\_\{2\}C, which treats the direction of the parameter error as unknown\. The corrected residual also provides a computed centerΔ^\\widehat\{\\Delta\}for that error, allowing the remaining uncertainty to be bounded around an estimated direction\.

###### Proposition 1\(Error\-centered readout certificate\)\.

LetΔ=θR−θ~\\Delta=\\theta^\{\\mathrm\{R\}\}\-\\widetilde\{\\theta\}and suppose‖Δ‖F≤C\\left\\lVert\\Delta\\right\\rVert\_\{F\}\\leq Cand‖Δ−Δ^‖F≤RΔ\\left\\lVert\\Delta\-\\widehat\{\\Delta\}\\right\\rVert\_\{F\}\\leq R\_\{\\Delta\}\. Then, for any fixedZ∈ℝm×dZ\\in\\mathbb\{R\}^\{m\\times d\},

‖Z​Δ‖F≤min⁡\{‖Z‖2​C,‖Z​Δ^‖F\+‖Z‖2​RΔ\}\.\\left\\lVert Z\\Delta\\right\\rVert\_\{F\}\\leq\\min\\\!\\bigl\\\{\\left\\lVert Z\\right\\rVert\_\{2\}C,\\left\\lVert Z\\widehat\{\\Delta\}\\right\\rVert\_\{F\}\+\\left\\lVert Z\\right\\rVert\_\{2\}R\_\{\\Delta\}\\bigr\\\}\.\(5\)

We denote the resulting generic and centered bounds byCZball=‖Z‖2​CC\_\{Z\}^\{\\rm ball\}=\\left\\lVert Z\\right\\rVert\_\{2\}CandCZctr=‖Z​Δ^‖F\+‖Z‖2​RΔC\_\{Z\}^\{\\rm ctr\}=\\left\\lVert Z\\widehat\{\\Delta\}\\right\\rVert\_\{F\}\+\\left\\lVert Z\\right\\rVert\_\{2\}R\_\{\\Delta\}\. The centered bound preserves the estimated error direction and applies the worst\-case bound only to its remaining uncertainty\. Its executable construction appears in[SectionC\.5\.2](https://arxiv.org/html/2610.02268#A3.SS5.SSS2)\. The same certificate yields binary score\-sign and multiclass top\-1 agreement under the margin conditions in[Corollary1](https://arxiv.org/html/2610.02268#Thmcorollary1)\.

### 4\.2Maintaining Reference\-Transfer Evidence

When a deployment chooses to maintain certificate evidence incrementally, the verifier must relate the service’s evolving finite\-precision state to the exact current retain\-set system\. The release\-time certificate in[Section4\.1](https://arxiv.org/html/2610.02268#S4.SS1)ultimately concerns the latter, while the service updates a separate stored numerical state\. Incremental RRV therefore maintains certified evidence connecting these two systems throughout the deletion sequence\.

LetDt=\{\(xi,yi\)\}i=1ntD\_\{t\}=\\\{\(x\_\{i\},y\_\{i\}\)\\\}\_\{i=1\}^\{n\_\{t\}\}be the retain set afterttcommitted deletions, with feature and target matricesXtX\_\{t\}andYtY\_\{t\}\. Forλ\>0\\lambda\>0, define

Ht=Xt⊤​Xt\+λ​Id,Bt=Xt⊤​Yt,Ht​θtR=Bt\.H\_\{t\}=X\_\{t\}^\{\\top\}X\_\{t\}\+\\lambda I\_\{d\},\\qquad B\_\{t\}=X\_\{t\}^\{\\top\}Y\_\{t\},\\qquad H\_\{t\}\\theta\_\{t\}^\{\\mathrm\{R\}\}=B\_\{t\}\.\(6\)Deleting\(x,y\)\(x,y\)changes the exact statistics byHt\+1=Ht−x​x⊤H\_\{t\+1\}=H\_\{t\}\-xx^\{\\top\}andBt\+1=Bt−x​y⊤B\_\{t\+1\}=B\_\{t\}\-xy^\{\\top\}\.

The service instead stores finite\-precision statisticsH~t,B~t\\widetilde\{H\}\_\{t\},\\widetilde\{B\}\_\{t\}\. Incremental RRV tracks their discrepancy from the exact retain\-set statistics through componentwise enclosures

\|H~t−Ht\|≤𝒰H,t,\|B~t−Bt\|≤𝒰B,t\.\\left\\lvert\\widetilde\{H\}\_\{t\}\-H\_\{t\}\\right\\rvert\\leq\\mathcal\{U\}\_\{H,t\},\\qquad\\left\\lvert\\widetilde\{B\}\_\{t\}\-B\_\{t\}\\right\\rvert\\leq\\mathcal\{U\}\_\{B,t\}\.\(7\)These bounds certify how far the numerical state maintained by the service may have drifted from the exact retain\-set system\.

The second maintained component is reusable inverse evidence\. Rather than reconstructing an inverse certificate after every deletion, Incremental RRV carries an approximate inversePtP\_\{t\}, a computed defect trackerE^t\\widehat\{E\}\_\{t\}, and a certified radiusrtr\_\{t\}satisfying

‖Id−Pt​H~t−E^t‖F≤rt\.\\left\\lVert I\_\{d\}\-P\_\{t\}\\widetilde\{H\}\_\{t\}\-\\widehat\{E\}\_\{t\}\\right\\rVert\_\{F\}\\leq r\_\{t\}\.\(8\)For each signed rank\-one change, a guarded Sherman–Morrison transition updatesPtP\_\{t\}, the defect tracker, and the statistics enclosures\. The propagated radius accounts for the previous certified uncertainty together with arithmetic error in the update and tracker evaluation\. Every denominator, matrix\-vector product, and state transition is checked before commit; a failed guard invokes the configured rebuild\. A successful rank\-one transition costsO⁡\(d2\)O\(d^\{2\}\), compared withO⁡\(d3\)O\(d^\{3\}\)for dense inverse reconstruction\.

At release, these two maintained components are combined to recover the quantities required by the certificate in[Section4\.1](https://arxiv.org/html/2610.02268#S4.SS1)\. Suppressingtt, letE=Id−P​H~E=I\_\{d\}\-P\\widetilde\{H\}\. The exact retain\-set residual and inverse defect obey

B−H​θ~\\displaystyle B\-H\\widetilde\{\\theta\}=\(B~−H~​θ~\)\+\(B−B~\)−\(H−H~\)​θ~,\\displaystyle=\(\\widetilde\{B\}\-\\widetilde\{H\}\\widetilde\{\\theta\}\)\+\(B\-\\widetilde\{B\}\)\-\(H\-\\widetilde\{H\}\)\\widetilde\{\\theta\},\(9\)Id−P​H\\displaystyle I\_\{d\}\-PH=E\+P⁡\(H~−H\)\.\\displaystyle=E\+P\(\\widetilde\{H\}\-H\)\.The first identity transfers the stored\-system residual to the exact retain\-set residual; the second transfers the stored\-system inverse defect to the exact retain\-set system\.

Here and below, an overline denotes a certified upper bound on the enclosed norm, andup⁡\(⋅\)\\operatorname\{up\}\(\\cdot\)denotes componentwise outward\-rounded evaluation\.

LetR^=fl⁡\(B~−H~​θ~\)\\widehat\{R\}=\\operatorname\{fl\}\(\\widetilde\{B\}\-\\widetilde\{H\}\\widetilde\{\\theta\}\), let𝒰R\\mathcal\{U\}\_\{R\}enclose residual\-evaluation error together with the stored\-to\-retain\-set correction, and letεP​R^\\varepsilon\_\{P\\widehat\{R\}\}enclose the arithmetic error inP​R^P\\widehat\{R\}\. Combining the maintained statistics and inverse evidence gives

‖Id−P​H‖2≤δret:=up⁡\(δstored\+‖P‖2¯​‖𝒰H‖2¯\),‖P⁡\(B−H​θ~\)‖F≤ρret:=up⁡\(‖fl⁡\(P​R^\)‖F⏟corrected residual\+εP​R^⏟evaluation error\+‖up⁡\(\|P\|​𝒰R\)‖F⏟reference\-transfer error\),C=ρret1−δret\.\\boxed\{\\begin\{aligned\} \\left\\lVert I\_\{d\}\-PH\\right\\rVert\_\{2\}&\\leq\\delta\_\{\\rm ret\}:=\\operatorname\{up\}\\\!\\left\(\\delta\_\{\\rm stored\}\+\\overline\{\\left\\lVert P\\right\\rVert\_\{2\}\}\\,\\overline\{\\left\\lVert\\mathcal\{U\}\_\{H\}\\right\\rVert\_\{2\}\}\\right\),\\\\ \\left\\lVert P\(B\-H\\widetilde\{\\theta\}\)\\right\\rVert\_\{F\}&\\leq\\rho\_\{\\rm ret\}:=\\operatorname\{up\}\\\!\\left\(\\underbrace\{\\left\\lVert\\operatorname\{fl\}\(P\\widehat\{R\}\)\\right\\rVert\_\{F\}\}\_\{\\text\{corrected residual\}\}\+\\underbrace\{\\varepsilon\_\{P\\widehat\{R\}\}\}\_\{\\text\{evaluation error\}\}\+\\underbrace\{\\left\\lVert\\operatorname\{up\}\(\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{R\}\)\\right\\rVert\_\{F\}\}\_\{\\text\{reference\-transfer error\}\}\\right\),\\\\ C&=\\frac\{\\rho\_\{\\rm ret\}\}\{1\-\\delta\_\{\\rm ret\}\}\.\\end\{aligned\}\}\(10\)Thus the evidence maintained during the deletion sequence is converted only when certification is required into the exact retain\-set quantities consumed by the release\-time certificate\.

The componentwise outward\-rounded construction appears in[SectionC\.4](https://arxiv.org/html/2610.02268#A3.SS4); the rank\-one recurrence and propagation proofs appear in[SectionsB\.3](https://arxiv.org/html/2610.02268#A2.SS3),[C\.2](https://arxiv.org/html/2610.02268#A3.SS2)and[C\.6](https://arxiv.org/html/2610.02268#A3.SS6)\.

### 4\.3Transactional Release Conformance

A release\-time certificate may be constructed by either On\-demand RRV or Incremental RRV as in[Section4\.2](https://arxiv.org/html/2610.02268#S4.SS2)\. In either case, the certificate must apply to the exact artifact that becomes visible\.

Letℛ\\mathcal\{R\}denote the declared release checkpoints\. Att∉ℛt\\notin\\mathcal\{R\}, the service may commit verified internal state without emitting an artifact\. Att∈ℛt\\in\\mathcal\{R\}, the current candidate is released only after every declared contract certifies\. Any repair, recomputation, or re\-encoding that changes the candidate produces a new artifact and therefore requires recertification\. A proof\-state rebuild, by contrast, changes only the verifier evidence and leaves the candidate itself unchanged\.

###### Theorem 1\(Incremental RRV release conformance\)\.

Suppose Incremental RRV is initialized with valid statistics and inverse\-defect enclosures, accepts only guarded transitions that preserve both invariants, and at each declared release checkpoint applies[Equation10](https://arxiv.org/html/2610.02268#S4.E10)and the declared contract checks to the concrete candidate\. If candidate\-changing remediation is recorded as a new candidate and recertified, and release is atomic with respect to the certified artifact, then every released artifact satisfies every declared retraining\-reference contract\.

The theorem states the concrete Incremental RRV initialization, transition, reference\-transfer, contract\-checking, and transactional\-release obligations; On\-demand RRV is the special case that constructs sound evidence only at a release checkpoint\. Proofs and precise transactional assumptions appear in[SectionB\.4](https://arxiv.org/html/2610.02268#A2.SS4)\. Successful rank\-kkincremental propagation costsO⁡\(k​d2\+k​d​c\)O\(kd^\{2\}\+kdc\), excluding output generation; complete release and rebuild accounting appears in[SectionB\.4](https://arxiv.org/html/2610.02268#A2.SS4)\.

### 4\.4Derived Release Contracts

The same bound composes with Gaussian and Laplace release guarantees, including executable closure of Newton direct\-perturbation radii\([Pandey et al\., 2026](https://arxiv.org/html/2610.02268#bib.bib11);[Zou et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib10)\); the full interfaces appear in[SectionB\.2](https://arxiv.org/html/2610.02268#A2.SS2)\.

##### Format compatibility\.

A final representation may itself be incapable of satisfying the declared contract\. Letθ^\\widehat\{\\theta\}be a certified reference center with‖θ^−θR‖F≤rref\\left\\lVert\\widehat\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq r\_\{\\rm ref\}\. For a finite scalar formatℱ⊂ℝ\\mathcal\{F\}\\subset\\mathbb\{R\}, letd¯ℱ​\(θ^\)\\underline\{d\}\_\{\\mathcal\{F\}\}\(\\widehat\{\\theta\}\)be a certified lower bound on the distance fromθ^\\widehat\{\\theta\}toℱd×c\\mathcal\{F\}^\{d\\times c\}, and lets¯ref\\overline\{s\}\_\{\\rm ref\}be a certified upper bound on‖θ^‖F\\left\\lVert\\widehat\{\\theta\}\\right\\rVert\_\{F\}\.

###### Proposition 2\(Finite\-format impossibility\)\.

AssumeθR≠0\\theta^\{\\mathrm\{R\}\}\\neq 0\. If

d¯ℱ​\(θ^\)−rref\>τpar​\(s¯ref\+rref\),\\underline\{d\}\_\{\\mathcal\{F\}\}\(\\widehat\{\\theta\}\)\-r\_\{\\rm ref\}\>\\tau\_\{\\rm par\}\\left\(\\overline\{s\}\_\{\\rm ref\}\+r\_\{\\rm ref\}\\right\),\(11\)then noθℱ∈ℱd×c\\theta\_\{\\mathcal\{F\}\}\\in\\mathcal\{F\}^\{d\\times c\}satisfies the relative contract in[Equation2](https://arxiv.org/html/2610.02268#S3.E2)\.

The format is then infeasible for the declared contract; the proof and codebook construction appear in[SectionsB\.5](https://arxiv.org/html/2610.02268#A2.SS5)and[E\.4](https://arxiv.org/html/2610.02268#A5.SS4.SSS0.Px2)\.

## 5Experiments

Evaluation questions\.We ask whether reference transfer prevents false releases without making certificates overly conservative \([Section5\.1](https://arxiv.org/html/2610.02268#S5.SS1)\), whether incremental evidence reduces lifecycle cost without weakening certification \([Section5\.2](https://arxiv.org/html/2610.02268#S5.SS2)\), and how ExecCert affects four published methods without changing their update rules \([Section5\.3](https://arxiv.org/html/2610.02268#S5.SS3)\)\. We then test when producer precision or output representation limits the contract \([Section5\.4](https://arxiv.org/html/2610.02268#S5.SS4)\)\.

The sequential service certifies ad=3073d=3073binary ridge head on frozen Llama\-3\.2\-3B\-Instruct\([Meta AI, 2024](https://arxiv.org/html/2610.02268#bib.bib22)\)representations\. Controlled diagnostics use DINOv2\([Oquab et al\., 2024](https://arxiv.org/html/2610.02268#bib.bib30)\)on CIFAR\-10\([Krizhevsky, 2009](https://arxiv.org/html/2610.02268#bib.bib31)\)and RoBERTa\([Liu et al\., 2019](https://arxiv.org/html/2610.02268#bib.bib32)\)on AG\-News\([Zhang et al\., 2015](https://arxiv.org/html/2610.02268#bib.bib33)\); the published applications cover linear, logistic, and graph methods\. Comparisons hold the candidate and contract fixed\. Independent retraining and high\-precision intervals supply offline labels\. Protocols and provenance appear in[AppendicesD](https://arxiv.org/html/2610.02268#A4),[E](https://arxiv.org/html/2610.02268#A5)and[F](https://arxiv.org/html/2610.02268#A6)\.

### 5\.1Reference\-Transfer Soundness and Tightness

Stored\-equation verification admits nearly all nonconforming candidates on the matched stress population, whereas RRV produces no false release \([Table5](https://arxiv.org/html/2610.02268#A5.T5)\)\. On the FP32 stress population, Incremental RRV initially certifies 4,838 of 7,293 conforming outputs without a false release; proof\-only rebuilds raise conditional coverage to 67\.24%, compared with 99\.97% for fresh\-factor verification \([Section5\.4](https://arxiv.org/html/2610.02268#S5.SS4)\)\. On a separate fixed population, RRV encloses every realized error across the tolerance sweep, and its certificate remains within about 1% of the independent reference for 95% of outputs \([Figure2](https://arxiv.org/html/2610.02268#S5.F2)\)\.

Figure 2:RRV certificates closely track realized error\.Incremental componentwise RRV and independent retained\-row reconstruction evaluate the same fixed FP32 deletion outputs at every tolerance\. Coverage gap is the conforming fraction minus the certified fraction; certificate inflation isτcert/τtrue−1\\tau\_\{\\rm cert\}/\\tau\_\{\\rm true\}\-1\. No rebuild or producer remediation changes the population\.
### 5\.2Evidence Reuse in Sequential Services

We compare fresh and maintained verified factors with Incremental RRV on the same candidate outputs, fixed readout, and release contract\. A direction\-free incremental variant tests whether reuse alone is sufficient\.

Table 1:Verification of the same frozen 3B safety\-head outputs\.Latency summarizes 10 repetitions at each of 21 states\. No method scans retained rows; state excludes those rows\.The maintained factor removes the weak\-baseline explanation: it matches the coverage of fresh factor, while directional Incremental RRV uses roughly 40% of fresh\-factor latency at matched coverage \([Table1](https://arxiv.org/html/2610.02268#S5.T1)\)\. The norm\-ball variant fails on the same states, so reuse preserves strength only when the proof state retains contract\-relevant error direction\. This ordering holds throughout the nonempty tolerance sweep\. Replacing the readout\-norm upper bound by a certified lower bound still leaves every norm\-ball certificate above tolerance, ruling out readout\-norm looseness as the explanation\. A separate decision audit covers about 95% of declared safety\-head decisions; observed agreement is not used as certified coverage\.

Measured\-component lifecycle accounting combines complete stream replays with the paired release\-check timings\. Fresh factor is cheapest for sparse checks; directional Incremental RRV crosses it at about 22 checks per 1,000 requests and remains cheaper than maintained factor throughout the evaluated schedules \([Figure3](https://arxiv.org/html/2610.02268#S5.F3)\(a\)\)\. Under every\-request checking, it reduces lifecycle cost by 42\.7% relative to maintained factor\. The crossover is workload\-specific because it trades continuous proof maintenance against release\-time construction\.

### 5\.3Published\-Method Applications

We attach ExecCert to four existing unlearning methods: Newton\-update removal\([Guo et al\., 2020](https://arxiv.org/html/2610.02268#bib.bib2)\), Newton direct perturbation\([Zou et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib10)\), ScaleGUN\([Yi and Wei, 2025](https://arxiv.org/html/2610.02268#bib.bib27)\), and CEU\([Wu et al\., 2023](https://arxiv.org/html/2610.02268#bib.bib28)\)\. In each case, the original update rule and emitted candidate are left unchanged; ExecCert is applied only at release time\. The check closes either the method’s native certificate quantity or a predeclared retraining\-reference contract\.

Table 2:Executable certification on published unlearning methods\.ExecCert is applied to the emitted candidate without changing the underlying update rule\.Native closure can move Newton\-removal retraining earlier, while direct recertification identifies conservative source stops\. For Newton direct perturbation, direct certification remains tighter than direction\-free composition under both execution precisions; we report an absolute FP64 gap because the direct bound can approach zero\. ExecCert preserves the ScaleGUN cheap\-update certificates\. For CEU, the declared tolerance is not supported, but post\-update RRV certifies the weaker fidelity of the emitted heads\. These cases show that release\-time certification can change a decision, tighten or preserve a certificate, or identify the fidelity supported by an output\. Source instrumentation and supplementary results appear in[AppendicesD](https://arxiv.org/html/2610.02268#A4)and[D\.2](https://arxiv.org/html/2610.02268#A4.SS2)\.

\(a\) Evidence reuse

\(b\) Format feasibility

Figure 3:Deployment choices affect certification cost and feasibility\.\(a\) Full\-stream maintenance measurements combined with matched release\-check timings produce the lifecycle curves\. The maintained\-factor crossover with fresh construction lies beyond the plotted low\-frequency region, at about 214 checks per 1,000 requests\. \(b\) The horizontal axis is the minimum achievable relative errorτmin\\tau\_\{\\min\}\. A format is ruled out when its certified lower bound exceeds the declared contractτpar\\tau\_\{\\rm par\}; BF16 is unreachable, while equal\-size FP16 remains reachable\.
### 5\.4Precision and Representation Boundaries

The preceding experiments vary certificate construction for a fixed candidate\. We finally ask when the candidate or its representation, rather than the verifier, limits the contract\.

Producer precision\.With FP32 statistics, fresh\-factor On\-demand RRV covers materially more conforming candidates than Incremental RRV after proof\-only rebuilds; both paths attain complete coverage with the FP64 producer\. Changing precision also changes the emitted candidate, so this is a producer\-policy comparison rather than a certificate\-only comparison\. Full timing and state results appear in[Tables7](https://arxiv.org/html/2610.02268#A5.T7)and[E\.4](https://arxiv.org/html/2610.02268#A5.SS4)\.

Release format\.BF16 cannot represent any artifact satisfying the declared tolerance, whereas FP16 and FP32 remain feasible \([Figure3](https://arxiv.org/html/2610.02268#S5.F3)\(b\)\)\. Thus, some failures require changing the producer or encoding rather than tightening verification\.

## 6Discussion and Conclusion

Our results separate three release\-time failure modes: a mathematical certificate may not close for the executed artifact, a sound verifier may be too weak or costly for the release schedule, or the producer and output format may preclude the contract\. ExecCert identifies whether remediation should target verification or the released artifact\.

Certification strategy depends on the contract and release schedule\. Native closure uses the quantity governing a source guarantee; RRV targets fidelity to current retain\-set retraining\. On\-demand construction favors sparse checks, while incremental proof state amortizes frequent certification\. ExecCert supplements the upstream guarantee: parameter or fixed\-readout fidelity does not establish semantic forgetting or multi\-round adaptive privacy\. Our incremental implementation covers frozen representations with moderate\-dimensional mutable ridge heads;[AppendixA](https://arxiv.org/html/2610.02268#A1)gives the remaining conditions\.

### AI Use Statement

We used generative AI tools to assist with code implementation and refactoring, figure andLaTeXediting, and language polishing\. The authors reviewed and verified all mathematical statements, experimental designs, interpretations of source methods, code changes, results, and manuscript text\. We take responsibility for the final content of this work, including text, claims, and artifacts produced with the aid of generative AI\.

### Reproducibility Statement

The appendix provides complete proofs, executable\-verification details, published\-source provenance, experimental protocols, and independent reference construction\. The accompanying artifact contains the implementation, fixed configurations, source instrumentation patches, and canonical records used for the reported tables and figures\.

## References

- Chienet al\.\(2024\)E\. Chien, H\. Wang, Z\. Chen, and P\. LiCertified machine unlearning via noisy stochastic gradient descent\.InProceedings of the 38th International Conference on Neural Information Processing Systems,NIPS ’24,Red Hook, NY, USA\.External Links:ISBN 9798331314385Cited by:[§1](https://arxiv.org/html/2610.02268#S1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Eisenhoferet al\.\(2025\)T\. Eisenhofer, D\. Riepel, V\. Chandrasekaran, E\. Ghosh, O\. Ohrimenko, and N\. PapernotVerifiable and provably secure machine unlearning\.In2025 IEEE Conference on Secure and Trustworthy Machine Learning \(SaTML\),Vol\.,pp\. 479–496\.External Links:[Document](https://dx.doi.org/10.1109/SaTML64287.2025.00033)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Ginartet al\.\(2019\)A\. A\. Ginart, M\. Y\. Guan, G\. Valiant, and J\. ZouMaking ai forget you: data deletion in machine learning\.InProceedings of the 33rd International Conference on Neural Information Processing Systems,Cited by:[§1](https://arxiv.org/html/2610.02268#S1.p1.1)\.
- Guoet al\.\(2020\)C\. Guo, T\. Goldstein, A\. Hannun, and L\. Van Der MaatenCertified data removal from machine learning models\.InProceedings of the 37th International Conference on Machine Learning,ICML’20\.Cited by:[§D\.1](https://arxiv.org/html/2610.02268#A4.SS1.SSS0.Px1.p1.1),[§1](https://arxiv.org/html/2610.02268#S1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1),[§5\.3](https://arxiv.org/html/2610.02268#S5.SS3.p1.1)\.
- Guptaet al\.\(2021\)V\. Gupta, C\. Jung, S\. Neel, A\. Roth, S\. Sharifi\-Malvajerdi, and C\. WaitesAdaptive machine unlearning\.InProceedings of the 35th International Conference on Neural Information Processing Systems,NIPS ’21,Red Hook, NY, USA\.External Links:ISBN 9781713845393Cited by:[§1](https://arxiv.org/html/2610.02268#S1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Hager \(1989\)W\. W\. HagerUpdating the inverse of a matrix\.SIAM Review31\(2\),pp\. 221–239\.External Links:[Document](https://dx.doi.org/10.1137/1031049),[Link](https://doi.org/10.1137/1031049),https://doi\.org/10\.1137/1031049Cited by:[§B\.3](https://arxiv.org/html/2610.02268#A2.SS3.p1.3),[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Higham \(2002\)N\. J\. HighamAccuracy and stability of numerical algorithms\.2 edition,Society for Industrial and Applied Mathematics,Philadelphia, PA\.External Links:[Document](https://dx.doi.org/10.1137/1.9780898718027)Cited by:[§C\.1](https://arxiv.org/html/2610.02268#A3.SS1.SSS0.Px2.p1.1),[§C\.2](https://arxiv.org/html/2610.02268#A3.SS2.SSS0.Px3.p3.pic1.2.2.1),[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Jiet al\.\(2025\)J\. Ji, D\. Hong, B\. Zhang, B\. Chen, J\. Dai, B\. Zheng, T\. Qiu, J\. Zhou, K\. Wang, B\. Li, S\. Han, Y\. Guo, and Y\. YangPKU\-saferlhf: towards multi\-level safety alignment for llms with human preference\.External Links:2406\.15513,[Link](https://arxiv.org/abs/2406.15513)Cited by:[§E\.1](https://arxiv.org/html/2610.02268#A5.SS1.SSS0.Px1.p1.1)\.
- Jinet al\.\(2024\)J\. Jin, O\. Ohrimenko, and B\. I\. P\. RubinsteinGetting a\-round guarantees: floating\-point attacks on certified robustness\.InProceedings of the 2024 Workshop on Artificial Intelligence and Security,AISec ’24,New York, NY, USA,pp\. 53–64\.External Links:ISBN 9798400712289,[Link](https://doi.org/10.1145/3689932.3694761),[Document](https://dx.doi.org/10.1145/3689932.3694761)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Koloskovaet al\.\(2025\)A\. Koloskova, Y\. Allouah, A\. Jha, R\. Guerraoui, and S\. KoyejoCertified unlearning for neural networks\.InProceedings of the 42nd International Conference on Machine Learning,ICML’25\.Cited by:[§1](https://arxiv.org/html/2610.02268#S1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Krawczyk \(1969\)R\. KrawczykNewton\-algorithmen zur bestimmung von nullstellen mit fehlerschranken\.Computing4\(3\),pp\. 187–201\.External Links:[Document](https://dx.doi.org/10.1007/BF02234767)Cited by:[§B\.1](https://arxiv.org/html/2610.02268#A2.SS1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Krizhevsky \(2009\)A\. KrizhevskyLearning multiple layers of features from tiny images\.Technical reportUniversity of Toronto\.Cited by:[§5](https://arxiv.org/html/2610.02268#S5.p2.1)\.
- Liuet al\.\(2019\)Y\. Liu, M\. Ott, N\. Goyal, J\. Du, M\. Joshi, D\. Chen, O\. Levy, M\. Lewis, L\. Zettlemoyer, and V\. StoyanovRoBERTa: a robustly optimized bert pretraining approach\.External Links:1907\.11692,[Link](https://arxiv.org/abs/1907.11692)Cited by:[§5](https://arxiv.org/html/2610.02268#S5.p2.1)\.
- Maheriet al\.\(2026\)M\. M\. Maheri, S\. Cotterill, A\. Davidson, and H\. HaddadiZK\-APEX: ZERO\-KNOWLEDGE APPROXIMATE PERSONALIZED UNLEARNING WITH EXECUTABLE PROOFS\.InNinth Conference on Machine Learning and Systems,External Links:[Link](https://openreview.net/forum?id=bLx6orLvQM)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Meta AI \(2024\)Meta AILlama 3\.2\-3B\-Instruct model card\.Note:Hugging Face model repositoryExternal Links:[Link](https://huggingface.co/meta-llama/Llama-3.2-3B-Instruct)Cited by:[§E\.1](https://arxiv.org/html/2610.02268#A5.SS1.SSS0.Px1.p1.1),[§5](https://arxiv.org/html/2610.02268#S5.p2.1)\.
- Mironov \(2012\)I\. MironovOn significance of the least significant bits for differential privacy\.InProceedings of the 2012 ACM Conference on Computer and Communications Security,CCS ’12,New York, NY, USA,pp\. 650–661\.External Links:ISBN 9781450316514,[Link](https://doi.org/10.1145/2382196.2382264),[Document](https://dx.doi.org/10.1145/2382196.2382264)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Nesterov \(2004\)Y\. NesterovIntroductory lectures on convex optimization: a basic course\.Applied Optimization, Vol\.87,Springer,Boston, MA\.External Links:[Document](https://dx.doi.org/10.1007/978-1-4419-8853-9)Cited by:[§B\.1](https://arxiv.org/html/2610.02268#A2.SS1.p7.1)\.
- Ogitaet al\.\(2005\)T\. Ogita, S\. M\. Rump, and S\. OishiAccurate sum and dot product\.SIAM Journal on Scientific Computing26\(6\),pp\. 1955–1988\.External Links:[Document](https://dx.doi.org/10.1137/030601818),[Link](https://doi.org/10.1137/030601818),https://doi\.org/10\.1137/030601818Cited by:[§C\.1](https://arxiv.org/html/2610.02268#A3.SS1.SSS0.Px2.p1.1)\.
- Oishi and Rump \(2002\)S\. Oishi and S\. M\. RumpFast verification of solutions of matrix equations\.Numerische Mathematik90\(4\),pp\. 755–773\.External Links:[Document](https://dx.doi.org/10.1007/s002110100310)Cited by:[§B\.1](https://arxiv.org/html/2610.02268#A2.SS1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Oquabet al\.\(2024\)M\. Oquab, T\. Darcet, T\. Moutakanni, H\. Vo, M\. Szafraniec, V\. Khalidov, P\. Fernandez, D\. Haziza, F\. Massa, A\. El\-Nouby, M\. Assran, N\. Ballas, W\. Galuba, R\. Howes, P\. Huang, S\. Li, I\. Misra, M\. Rabbat, V\. Sharma, G\. Synnaeve, H\. Xu, H\. Jegou, J\. Mairal, P\. Labatut, A\. Joulin, and P\. BojanowskiDINOv2: learning robust visual features without supervision\.External Links:2304\.07193,[Link](https://arxiv.org/abs/2304.07193)Cited by:[§5](https://arxiv.org/html/2610.02268#S5.p2.1)\.
- Pandeyet al\.\(2026\)A\. Pandey, A\. Auddy, H\. Zou, A\. Maleki, and S\. KulkarniGaussian certified unlearning in high dimensions: a hypothesis testing approach\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=0FJYicpOj0)Cited by:[§B\.2](https://arxiv.org/html/2610.02268#A2.SS2.p1.1),[§1](https://arxiv.org/html/2610.02268#S1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1),[§4\.4](https://arxiv.org/html/2610.02268#S4.SS4.p1.1)\.
- Rump \(2010\)S\. M\. RumpVerification methods: rigorous results using floating\-point arithmetic\.InProceedings of the 2010 International Symposium on Symbolic and Algebraic Computation,ISSAC ’10,New York, NY, USA,pp\. 3–4\.External Links:ISBN 9781450301503,[Link](https://doi.org/10.1145/1837934.1837937),[Document](https://dx.doi.org/10.1145/1837934.1837937)Cited by:[§B\.1](https://arxiv.org/html/2610.02268#A2.SS1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Sekhariet al\.\(2021\)A\. Sekhari, J\. Acharya, G\. Kamath, and A\. T\. SureshRemember what you want to forget: algorithms for machine unlearning\.InProceedings of the 35th International Conference on Neural Information Processing Systems,NIPS ’21,Red Hook, NY, USA\.External Links:ISBN 9781713845393Cited by:[§1](https://arxiv.org/html/2610.02268#S1.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Szászet al\.\(2025\)A\. Szász, B\. Bánhelyi, and M\. JelasityNo soundness in the real world: on the challenges of the verification of deployed neural networks\.InForty\-second International Conference on Machine Learning,External Links:[Link](https://openreview.net/forum?id=c16m2kUTLZ)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Thudiet al\.\(2022\)A\. Thudi, H\. Jia, I\. Shumailov, and N\. PapernotOn the necessity of auditable algorithmic definitions for machine unlearning\.In31st USENIX Security Symposium \(USENIX Security 22\),Boston, MA,pp\. 4007–4022\.External Links:ISBN 978\-1\-939133\-31\-1,[Link](https://www.usenix.org/conference/usenixsecurity22/presentation/thudi)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Voracek and Hein \(2023\)V\. Voracek and M\. HeinSound randomized smoothing in floating\-point arithmetic\.InThe Eleventh International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=HaHCoGcpV9)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p2.1)\.
- Wenget al\.\(2024\)J\. Weng, S\. Yao, Y\. Du, J\. Huang, J\. Weng, and C\. WangProof of unlearning: definitions and instantiation\.Trans\. Info\. For\. Sec\.19,pp\. 3309–3323\.External Links:ISSN 1556\-6013,[Link](https://doi.org/10.1109/TIFS.2024.3358993),[Document](https://dx.doi.org/10.1109/TIFS.2024.3358993)Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Wuet al\.\(2023\)K\. Wu, J\. Shen, Y\. Ning, T\. Wang, and W\. H\. WangCertified edge unlearning for graph neural networks\.InProceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining,External Links:[Document](https://dx.doi.org/10.1145/3580305.3599271)Cited by:[§D\.1](https://arxiv.org/html/2610.02268#A4.SS1.SSS0.Px2.p1.1),[§5\.3](https://arxiv.org/html/2610.02268#S5.SS3.p1.1)\.
- Yi and Wei \(2025\)L\. Yi and Z\. WeiScalable and certifiable graph unlearning: overcoming the approximation error barrier\.InInternational Conference on Learning Representations,External Links:[Link](https://proceedings.iclr.cc/paper_files/paper/2025/hash/f43567631f608dd1317c227c69dae441-Abstract-Conference.html)Cited by:[§D\.1](https://arxiv.org/html/2610.02268#A4.SS1.SSS0.Px3.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p2.1),[§5\.3](https://arxiv.org/html/2610.02268#S5.SS3.p1.1)\.
- Zhanget al\.\(2024a\)B\. Zhang, Z\. Chen, C\. Shen, and J\. LiVerification of machine unlearning is fragile\.InProceedings of the 41st International Conference on Machine Learning,ICML’24\.Cited by:[§2](https://arxiv.org/html/2610.02268#S2.p1.1)\.
- Zhanget al\.\(2024b\)B\. Zhang, Y\. Dong, T\. Wang, and J\. LiTowards certified unlearning for deep neural networks\.InProceedings of the 41st International Conference on Machine Learning,ICML’24\.Cited by:[§1](https://arxiv.org/html/2610.02268#S1.p1.1)\.
- Zhanget al\.\(2015\)X\. Zhang, J\. J\. Zhao, and Y\. LeCunCharacter\-level convolutional networks for text classification\.InNIPS,Cited by:[§5](https://arxiv.org/html/2610.02268#S5.p2.1)\.
- Zouet al\.\(2025\)H\. Zou, A\. Auddy, Y\. Kwon, K\. R\. Rad, and A\. MalekiCertified machine unlearning under high dimensional regime\.Journal of Machine Learning Research26\(308\),pp\. 1–58\.External Links:[Link](http://jmlr.org/papers/v26/25-1751.html)Cited by:[§D\.2](https://arxiv.org/html/2610.02268#A4.SS2.p1.1),[§2](https://arxiv.org/html/2610.02268#S2.p1.1),[§4\.4](https://arxiv.org/html/2610.02268#S4.SS4.p1.1),[§5\.3](https://arxiv.org/html/2610.02268#S5.SS3.p1.1)\.

## Appendix AScope and Limitations

Native closure inherits the scope of the source method’s own certificate; RRV instead certifies only the declared distance to its uniquely specified retraining reference\.

Fixed\-readout claims apply to the input representations declared before the candidate is inspected, and say nothing about inputs outside that set\. Randomized\-release calibration assumes a predeclared common scale; adaptive release policies, in which the noise scale reacts to the candidate, require separate analysis\.

Our reusable proof state currently targets moderate\-dimensional mutable heads\. Extending incremental certification to larger trainable blocks will require exploiting additional structure, since dense inverse evidence does not scale to that regime\. Unlike statistical deletion capacity, proof\-state lifetime is instance\-dependent and governed by conditioning rather than a universal deletion count: a failed guard triggers certified rebuilding, which restores the invariants at higher cost but imposes no fixed bound on the number of deletions a service can absorb\.

## Appendix BProofs of Main Results

### B\.1Release\-Time RRV Certificates

We first establish the parameter\-error bound and its error\-centered fixed\-readout refinement\. The first is the classical residual–inverse\-defect argument from verified linear algebra\([Krawczyk, 1969](https://arxiv.org/html/2610.02268#bib.bib13);[Oishi and Rump, 2002](https://arxiv.org/html/2610.02268#bib.bib15);[Rump, 2010](https://arxiv.org/html/2610.02268#bib.bib14)\); we retain its short derivation because it is the main certificate interface\.

###### Proof of[Lemma1](https://arxiv.org/html/2610.02268#Thmlemma1)\.

LetΔ=θR−θ~\\Delta=\\theta^\{\\mathrm\{R\}\}\-\\widetilde\{\\theta\}\. SinceH​θR=BH\\theta^\{\\mathrm\{R\}\}=B,

Δ\\displaystyle\\Delta=\(I−P​H\)​Δ\+P⁡\(B−H​θ~\),\\displaystyle=\(I\-PH\)\\Delta\+P\(B\-H\\widetilde\{\\theta\}\),‖Δ‖F\\displaystyle\\left\\lVert\\Delta\\right\\rVert\_\{F\}≤‖I−P​H‖2​‖Δ‖F\+‖P⁡\(B−H​θ~\)‖F≤δ​‖Δ‖F\+ρ\.\\displaystyle\\leq\\left\\lVert I\-PH\\right\\rVert\_\{2\}\\left\\lVert\\Delta\\right\\rVert\_\{F\}\+\\left\\lVert P\(B\-H\\widetilde\{\\theta\}\)\\right\\rVert\_\{F\}\\leq\\delta\\left\\lVert\\Delta\\right\\rVert\_\{F\}\+\\rho\.Thus‖Δ‖F≤ρ/\(1−δ\)=C\\left\\lVert\\Delta\\right\\rVert\_\{F\}\\leq\\rho/\(1\-\\delta\)=C\. The reverse triangle inequality gives‖θR‖F≥‖θ~‖F−C\\left\\lVert\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\geq\\left\\lVert\\widetilde\{\\theta\}\\right\\rVert\_\{F\}\-C, so whenever‖θ~‖F\>C\\left\\lVert\\widetilde\{\\theta\}\\right\\rVert\_\{F\}\>C,

‖θ~−θR‖F‖θR‖F≤C‖θ~‖F−C\.\\frac\{\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\}\{\\left\\lVert\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\}\\leq\\frac\{C\}\{\\left\\lVert\\widetilde\{\\theta\}\\right\\rVert\_\{F\}\-C\}\.\(12\)∎

###### Proof of[Proposition1](https://arxiv.org/html/2610.02268#Thmproposition1)\.

The first bound follows from‖Z​Δ‖F≤‖Z‖2​‖Δ‖F≤‖Z‖2​C\\left\\lVert Z\\Delta\\right\\rVert\_\{F\}\\leq\\left\\lVert Z\\right\\rVert\_\{2\}\\left\\lVert\\Delta\\right\\rVert\_\{F\}\\leq\\left\\lVert Z\\right\\rVert\_\{2\}C\. For the second, writeΔ=Δ^\+\(Δ−Δ^\)\\Delta=\\widehat\{\\Delta\}\+\(\\Delta\-\\widehat\{\\Delta\}\)and apply the triangle inequality together with the stated center enclosure\. Taking the smaller of the two valid bounds gives[Equation5](https://arxiv.org/html/2610.02268#S4.E5)\. ∎

The absolute parameter bound also certifies decisions with sufficient margin\.

###### Corollary 1\(Certified linear\-decision agreement\)\.

Fix a representationz∈ℝdz\\in\\mathbb\{R\}^\{d\}\. For a binary head satisfying‖θ~−θR‖2≤C\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{2\}\\leq C, the executed and retraining\-reference signs agree when\|z⊤​θ~\|\>‖z‖2​C\\left\\lvert z^\{\\top\}\\widetilde\{\\theta\}\\right\\rvert\>\\left\\lVert z\\right\\rVert\_\{2\}C\. For a multiclass head, let‖Θ~−ΘR‖F≤C\\left\\lVert\\widetilde\{\\Theta\}\-\\Theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq Canda=arg​maxj⁡z⊤​θ~ja=\\operatorname\*\{arg\\,max\}\_\{j\}z^\{\\top\}\\widetilde\{\\theta\}\_\{j\}\. It remains the unique top class underΘR\\Theta^\{\\mathrm\{R\}\}when

z⊤​θ~a−z⊤​θ~j\>2​‖z‖2​Cfor every​j≠a\.z^\{\\top\}\\widetilde\{\\theta\}\_\{a\}\-z^\{\\top\}\\widetilde\{\\theta\}\_\{j\}\>\\sqrt\{2\}\\,\\left\\lVert z\\right\\rVert\_\{2\}C\\qquad\\text\{for every \}j\\neq a\.

ProofCauchy–Schwarz bounds the binary score change by‖z‖2​C\\left\\lVert z\\right\\rVert\_\{2\}C\. For the multiclass case, writingΔj=θjR−θ~j\\Delta\_\{j\}=\\theta\_\{j\}^\{\\mathrm\{R\}\}\-\\widetilde\{\\theta\}\_\{j\}gives\|z⊤​\(Δa−Δj\)\|≤‖z‖2​‖Δa−Δj‖2≤2​‖z‖2​C\.\\left\\lvert z^\{\\top\}\(\\Delta\_\{a\}\-\\Delta\_\{j\}\)\\right\\rvert\\leq\\left\\lVert z\\right\\rVert\_\{2\}\\left\\lVert\\Delta\_\{a\}\-\\Delta\_\{j\}\\right\\rVert\_\{2\}\\leq\\sqrt\{2\}\\,\\left\\lVert z\\right\\rVert\_\{2\}C\.The strict margins preserve the stated decisions\.

For differentiable strongly convex objectives, a post\-update gradient enclosure provides a separate construction of the parameter\-error bound\.

###### Proposition 3\(Strongly\-convex post\-update certificate\)\.

LetL:ℝd→ℝL:\\mathbb\{R\}^\{d\}\\to\\mathbb\{R\}be differentiable andμ\\mu\-strongly convex, with minimizerθR\\theta^\{\\mathrm\{R\}\}\. Suppose the verifier constructs

g\+≥‖∇L​\(θ~\)‖2,0<μ−≤μ\.g^\{\+\}\\geq\\left\\lVert\\nabla L\(\\widetilde\{\\theta\}\)\\right\\rVert\_\{2\},\\qquad 0<\\mu^\{\-\}\\leq\\mu\.Then

‖θ~−θR‖2≤g\+μ−=:C\.\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{2\}\\leq\\frac\{g^\{\+\}\}\{\\mu^\{\-\}\}=:C\.

The absolute bound is the standard gradient–distance consequence of strong convexity\([Nesterov, 2004](https://arxiv.org/html/2610.02268#bib.bib8)\)\. A relative contract follows by applying[Equation12](https://arxiv.org/html/2610.02268#A2.E12)\.

### B\.2Randomized Release Interfaces

These fixed\-state interfaces use a predeclared common noise scale\. If RRV certifies‖θ~−θR‖2≤C\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{2\}\\leq C, the equal\-covariance Gaussian testing identity of[Pandey et al\. \(2026\)](https://arxiv.org/html/2610.02268#bib.bib11)gives

ε∗=‖θ~−θR‖2σ≤Cσ\.\\varepsilon\_\{\*\}=\\frac\{\\left\\lVert\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{2\}\}\{\\sigma\}\\leq\\frac\{C\}\{\\sigma\}\.For isotropic radial Laplace releases with common predeclared scaless, we use the densityqμ\(z\)∝exp\(−‖z−μ‖2/s\)q\_\{\\mu\}\(z\)\\propto\\exp\(\-\\left\\lVert z\-\\mu\\right\\rVert\_\{2\}/s\)\. Sampling draws a uniform direction on the Euclidean unit sphere and an independent radius fromGamma⁡\(d,s\)\\operatorname\{Gamma\}\(d,s\); the same rule and scale apply to both centers\. The triangle inequality gives, for every measurable eventAA,

Qexec​\(A\)≤eC/s​Qref​\(A\),Qref​\(A\)≤eC/s​Qexec​\(A\)\.Q\_\{\\rm exec\}\(A\)\\leq e^\{C/s\}Q\_\{\\rm ref\}\(A\),\\qquad Q\_\{\\rm ref\}\(A\)\\leq e^\{C/s\}Q\_\{\\rm exec\}\(A\)\.Thusσ≥C/ε\\sigma\\geq C/\\varepsilongives the corresponding Gaussian trade\-off guarantee, whiles≥C/εs\\geq C/\\varepsilongives a two\-sided Laplace comparison\. Hereε∗\\varepsilon\_\{\*\}is the equal\-covariance Gaussian testing parameter; it is not by itself a conventional\(ε,δ\)\(\\varepsilon,\\delta\)\-DP guarantee\. If an upstream analysis supplies radiusrnomr\_\{\\rm nom\}and executable closure addsCexecC\_\{\\rm exec\}, the Laplace result applies withC=rnom\+CexecC=r\_\{\\rm nom\}\+C\_\{\\rm exec\}\.

### B\.3Nonsymmetric Defect Recurrence

All quantities in this subsection are evaluated in exact real arithmetic\. LetHs,P∈ℝd×dH\_\{s\},P\\in\\mathbb\{R\}^\{d\\times d\},x∈ℝdx\\in\\mathbb\{R\}^\{d\}, ands∈\{−1,\+1\}s\\in\\\{\-1,\+1\\\}\. Define

E\\displaystyle E=Id−P​Hs,\\displaystyle=I\_\{d\}\-PH\_\{s\},q\\displaystyle q=P​x,\\displaystyle=Px,z\\displaystyle z=P⊤​x,\\displaystyle=P^\{\\top\}x,α\\displaystyle\\alpha=1\+s​x⊤​q\.\\displaystyle=1\+sx^\{\\top\}q\.Forα≠0\\alpha\\neq 0, let

Hs\+=Hs\+s​x​x⊤,P\+=P−sα​q​z⊤\.H\_\{s\}^\{\+\}=H\_\{s\}\+sxx^\{\\top\},\\qquad P^\{\+\}=P\-\\frac\{s\}\{\\alpha\}qz^\{\\top\}\.The update forP\+P^\{\+\}is the Sherman–Morrison formula\([Hager, 1989](https://arxiv.org/html/2610.02268#bib.bib16)\)\. The following identity propagates the stored\-system inverse defect without assuming thatPPis symmetric\.[SectionC\.6](https://arxiv.org/html/2610.02268#A3.SS6)constructs its guarded floating\-point realization\.

###### Lemma 2\(Exact nonsymmetric defect recurrence\)\.

For arbitraryHs,P∈ℝd×dH\_\{s\},P\\in\\mathbb\{R\}^\{d\\times d\}withα≠0\\alpha\\neq 0, including nonsymmetricPP, the post\-update defectE\+=Id−P\+​Hs\+E^\{\+\}=I\_\{d\}\-P^\{\+\}H\_\{s\}^\{\+\}satisfies

E\+=E−q​sα​\(x⊤−z⊤​Hs\)\.E^\{\+\}=E\-q\\frac\{s\}\{\\alpha\}\\left\(x^\{\\top\}\-z^\{\\top\}H\_\{s\}\\right\)\.The recurrence requiresO⁡\(d2\)O\(d^\{2\}\)arithmetic andO⁡\(d2\)O\(d^\{2\}\)state\.

###### Proof of[Lemma2](https://arxiv.org/html/2610.02268#Thmlemma2)\.

Becausez⊤=x⊤​Pz^\{\\top\}=x^\{\\top\}P, expansion ofE\+=Id−P\+​Hs\+E^\{\+\}=I\_\{d\}\-P^\{\+\}H\_\{s\}^\{\+\}gives

E\+=E−s​q​x⊤\+sα​q​z⊤​Hs\+1α​q​\(z⊤​x\)​x⊤\.E^\{\+\}=E\-sqx^\{\\top\}\+\\frac\{s\}\{\\alpha\}qz^\{\\top\}H\_\{s\}\+\\frac\{1\}\{\\alpha\}q\(z^\{\\top\}x\)x^\{\\top\}\.Letβ=z⊤​x=x⊤​q\\beta=z^\{\\top\}x=x^\{\\top\}q\. Sinceα=1\+s​β\\alpha=1\+s\\beta, the coefficient ofq​x⊤qx^\{\\top\}equals

−s\+βα=−sα\.\-s\+\\frac\{\\beta\}\{\\alpha\}=\-\\frac\{s\}\{\\alpha\}\.Substitution yieldsE\+=E−\(s/α\)​q​\(x⊤−z⊤​Hs\)E^\{\+\}=E\-\(s/\\alpha\)q\(x^\{\\top\}\-z^\{\\top\}H\_\{s\}\)\. ∎

### B\.4Transactional Conformance and Cost

The transactional theorem applies to any sound verification backend\. Its incremental corollary combines the maintained statistics and inverse\-defect invariants with the release\-time contract checks\.

Here guarded committed transitions require every numerical denominator and interval to pass its guard, every certificate evaluation to remain within the certified arithmetic scope, and every rank\-one subupdate and invariant check to complete before commit\. At a release checkpoint, the service exposes an artifact only after every declared contract certifies\.

##### Transactional justification\.

The initialization hypotheses give the two proof\-state invariants at the first state\.[Theorems2](https://arxiv.org/html/2610.02268#Thmtheorem2)and[3](https://arxiv.org/html/2610.02268#Thmtheorem3)preserve them under every accepted guarded transition\. At a release checkpoint, the transfer and release constructions in[SectionsC\.4](https://arxiv.org/html/2610.02268#A3.SS4)and[C\.5](https://arxiv.org/html/2610.02268#A3.SS5)therefore establish every declared contract for the concrete candidate presented to the policy gate\. If remediation changes that candidate, the original certificate no longer authorizes release and the new candidate must be certified separately\. Atomic release ensures that the visible artifact is exactly the candidate covered by the successful certificates\.

##### Cost accounting\.

LetGtG\_\{t\}denote the cost of advancing the selected output generator at requesttt, letktk\_\{t\}be the number of rank\-one subupdates for that request, and setm=0m=0when no fixed readout is declared\. Each request addsO⁡\(kt​d2\+kt​d​c\)O\(k\_\{t\}d^\{2\}\+k\_\{t\}dc\)proof\-state work; a release addsO⁡\(d2​c\+m​d​c\)O\(d^\{2\}c\+mdc\)certificate work\. Rebuilding proof state from certified\(H~t,B~t\)\(\\widetilde\{H\}\_\{t\},\\widetilde\{B\}\_\{t\}\)costsO⁡\(d3\+d2​c\)O\(d^\{3\}\+d^\{2\}c\)\. Reconstructing those statistics from retained rows addsO⁡\(nt​d2\+nt​d​c\)O\(n\_\{t\}d^\{2\}\+n\_\{t\}dc\)\. LetMproofM\_\{\\rm proof\}count dense proof\-state rebuilds that reuse certified sufficient statistics, and letℛdata\\mathcal\{R\}\_\{\\rm data\}be the index set of requests whose rebuilds reconstruct those statistics fromntn\_\{t\}retained rows\. OverNNrequests, the total cost is

O⁡\(CLOSE\\displaystyle O\\\!\\biggl\(∑t=1NGt\+∑t=1N\(kt​d2\+kt​d​c\)\\displaystyle\\sum\_\{t=1\}^\{N\}G\_\{t\}\+\\sum\_\{t=1\}^\{N\}\(k\_\{t\}d^\{2\}\+k\_\{t\}dc\)\+\|ℛ\|​\(d2​c\+m​d​c\)\+Mproof​\(d3\+d2​c\)\\displaystyle\+\\left\\lvert\\mathcal\{R\}\\right\\rvert\(d^\{2\}c\+mdc\)\+M\_\{\\rm proof\}\(d^\{3\}\+d^\{2\}c\)\+∑t∈ℛdata\(ntd2\+ntdc\+d3\+d2c\)\)\.\\displaystyle\+\\sum\_\{t\\in\\mathcal\{R\}\_\{\\rm data\}\}\(n\_\{t\}d^\{2\}\+n\_\{t\}dc\+d^\{3\}\+d^\{2\}c\)\\biggr\)\.The every\-request\-release policy is the special case\|ℛ\|=N\\left\\lvert\\mathcal\{R\}\\right\\rvert=N\.

### B\.5Finite\-Format Impossibility

LetθR∈ℝd×c\\theta^\{\\mathrm\{R\}\}\\in\\mathbb\{R\}^\{d\\times c\}be the exact retraining target, and letθ^\\widehat\{\\theta\}satisfy‖θ^−θR‖F≤rref\\left\\lVert\\widehat\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq r\_\{\\rm ref\}\. For a finite scalar formatℱ⊂ℝ\\mathcal\{F\}\\subset\\mathbb\{R\}, letd¯ℱ​\(θ^\)\\underline\{d\}\_\{\\mathcal\{F\}\}\(\\widehat\{\\theta\}\)be a certified lower bound on the distance fromθ^\\widehat\{\\theta\}toℱd×c\\mathcal\{F\}^\{d\\times c\}, and lets¯ref\\overline\{s\}\_\{\\rm ref\}be a certified upper bound on‖θ^‖F\\left\\lVert\\widehat\{\\theta\}\\right\\rVert\_\{F\}\.

###### Proof of[Proposition2](https://arxiv.org/html/2610.02268#Thmproposition2)\.

For any representableθℱ∈ℱd×c\\theta\_\{\\mathcal\{F\}\}\\in\\mathcal\{F\}^\{d\\times c\}, the reverse triangle inequality and the certified reference enclosure give

‖θℱ−θR‖F\\displaystyle\\left\\lVert\\theta\_\{\\mathcal\{F\}\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}≥‖θℱ−θ^‖F−‖θ^−θR‖F\\displaystyle\\geq\\left\\lVert\\theta\_\{\\mathcal\{F\}\}\-\\widehat\{\\theta\}\\right\\rVert\_\{F\}\-\\left\\lVert\\widehat\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}≥d¯ℱ​\(θ^\)−rref\.\\displaystyle\\geq\\underline\{d\}\_\{\\mathcal\{F\}\}\(\\widehat\{\\theta\}\)\-r\_\{\\rm ref\}\.The ordinary triangle inequality gives

‖θR‖F≤s¯ref\+rref\.\\left\\lVert\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq\\overline\{s\}\_\{\\rm ref\}\+r\_\{\\rm ref\}\.Under[Equation11](https://arxiv.org/html/2610.02268#S4.E11), the lower bound on the numerator is strictly larger thanτpar\\tau\_\{\\rm par\}times this upper bound on the denominator\. Thus every representable tensor violates the declared relative contract\. ∎

## Appendix CSoundness of Incremental RRV

This appendix gives the executable verifier specification needed to establish the soundness of the incremental ridge regression backend of RRV\.[Algorithm1](https://arxiv.org/html/2610.02268#alg1)gives its transactional release protocol\.

Algorithm 1Incremental RRV release protocol1:Committed service and proof state, deletion request

tt, release schedule

ℛ\\mathcal\{R\}, output generator, and one or more declared contracts: parameter fidelity, fixed\-readout fidelity, or both

2:Provisionally update the statistics, their retain\-set enclosure, and the inverse\-defect proof state\.

3:ifa guard or proof\-state invariant check failsthen

4:Apply the configured proof\-state rebuild\.

5:ifthe rebuild does not reestablish the required invariantthen

6:Discard the transition;returninternalState\-Fail\.

7:endif

8:endif

9:Advance the output\-generator state for request

tt\.

10:if

t∉ℛt\\notin\\mathcal\{R\}then

11:Atomically commit the verified internal state; emit no output\.

12:returnNoRelease

13:endif

14:Materialize the current executed candidate artifact

θ~t\\widetilde\{\\theta\}\_\{t\}\.

15:Construct

\(δ,ρ,C\)\(\\delta,\\rho,C\)and every declared contract certificate\.

16:ifsome declared contract is inconclusivethen

17:Withhold the candidate and apply the configured remediation\.

18:Reconstruct proof state as needed and recertify any changed candidate\.

19:endif

20:ifevery declared contract now certifiesthen

21:Atomically commit state and certificates; release the candidate\.

22:returnCertified

23:else

24:Atomically commit verified internal state; withhold the candidate\.

25:returnInconclusive

26:endif

The verifier maintains statistics and inverse\-defect enclosures, transfers them to the exact retain\-set system, and constructs the release certificate in[SectionsC\.2](https://arxiv.org/html/2610.02268#A3.SS2),[C\.6](https://arxiv.org/html/2610.02268#A3.SS6),[C\.4](https://arxiv.org/html/2610.02268#A3.SS4)and[C\.5](https://arxiv.org/html/2610.02268#A3.SS5)\.

### C\.1Floating\-point conventions and notation map

##### Notation and exact\-real interpretation\.

We use the notation and shapes of[Section4\.2](https://arxiv.org/html/2610.02268#S4.SS2); array inequalities and absolute values remain componentwise\. A hat denotes a stored computed value, and a circle superscript denotes exact\-real evaluation of computed intermediates\. The symbol𝒰\\mathcal\{U\}denotes a componentwise enclosure,ε\\varepsilona local arithmetic bound, and\(δ,ρ\)\(\\delta,\\rho\)the hypotheses consumed by[Lemma1](https://arxiv.org/html/2610.02268#Thmlemma1)\. Stored entries are interpreted as their exact real values\.

##### Standard arithmetic facts\.

We use the componentwise floating\-point models for basic arithmetic, dot products, matrix–vector products, and matrix products from[Higham \(2002, Ch\. 3\)](https://arxiv.org/html/2610.02268#bib.bib7)\. Exact residuals returned byTwoSumuse the error\-free transformation of[Ogita et al\. \(2005\)](https://arxiv.org/html/2610.02268#bib.bib9)\. We invoke these standard facts without rederiving them below; every displayed endpoint is evaluated outward, and a failed arithmetic\-scope guard returnsInconclusive\.

##### Storage and verifier precision\.

The stored sufficient statistics may use𝔽s∈\{𝔽32,𝔽64\}\\mathbb\{F\}\_\{\\rm s\}\\in\\\{\\mathbb\{F\}\_\{32\},\\mathbb\{F\}\_\{64\}\\\}, with unit roundoffusu\_\{\\rm s\}\. The verifier and all outward endpoints use binary64,𝔽v=𝔽64\\mathbb\{F\}\_\{\\rm v\}=\\mathbb\{F\}\_\{64\}, withuv=2−53u\_\{\\rm v\}=2^\{\-53\}\. Stored FP32 statistics are promoted exactly to binary64 before verification; all other maintained proof state uses binary64\.

##### Outward evaluation\.

Defineγm\(q\)=m​uq/\(1−m​uq\)\\gamma\_\{m\}^\{\(q\)\}=mu\_\{q\}/\(1\-mu\_\{q\}\)form​uq<1mu\_\{q\}<1andu¯q=uq/\(1−uq\)\\bar\{u\}\_\{q\}=u\_\{q\}/\(1\-u\_\{q\}\), whereq∈\{s,v\}q\\in\\\{\\mathrm\{s\},\\mathrm\{v\}\\\}\. For verifier arithmetic, we writeγm:=γm\(v\)\\gamma\_\{m\}:=\\gamma\_\{m\}^\{\(\\mathrm\{v\}\)\}andu¯:=u¯v\\bar\{u\}:=\\bar\{u\}\_\{\\mathrm\{v\}\}\. Letη=2−1074\\eta=2^\{\-1074\}, and letω\\omegabe the largest finite binary64 number\. Forz∈𝔽64,≥0z\\in\\mathbb\{F\}\_\{64,\\geq 0\}, define

upm⁡\(z\):=nextafter⁡\(z1−γm\(v\),\+∞\)\.\\operatorname\{up\}\_\{m\}\(z\):=\\operatorname\{nextafter\}\\\!\\left\(\\frac\{z\}\{1\-\\gamma\_\{m\}^\{\(\\mathrm\{v\}\)\}\},\+\\infty\\right\)\.The shorthandup⁡\(⋅\)\\operatorname\{up\}\(\\cdot\)suppresses only this arity subscript: the implementation passes it explicitly, and each displayed use has the unique arity prescribed by the immediately enclosed operation\.down⁡\(z\)=nextafter⁡\(fl⁡\(z\),−∞\)\\operatorname\{down\}\(z\)=\\operatorname\{nextafter\}\(\\operatorname\{fl\}\(z\),\-\\infty\)for its lower endpoint\.m=ℓm=\\ellfor a sum ofℓ\\ellnonnegative terms,m=1m=1for one product or division, andm=2​p\+2m=2p\+2for a scale\-safe Frobenius\-norm reduction overppentries\.

##### Arithmetic scope\.

The dot\-product bounds permit any parenthesization of binary32 or binary64 products and sums within the stated operation count, so the proof does not depend on a particular threaded\-BLAS reduction order\. Fused multiply–add is covered conservatively because it incurs no more rounding than the separate product and addition modeled by the bound\. Algebraic reassociation throughfastmathis disabled\. TF32 and kernels with mixed\-precision accumulation are outside the certified arithmetic model\. Certified runs require IEEE gradual underflow; overflow, nonfinite values, unsafe subnormal intermediates, or an endpoint beyondω\\omegareturnsInconclusive\. Relative\-error bounds without an explicitη\\etaterm are used only after their intermediates are proved to remain in the normal range\. These binary64 conventions govern the ridge inverse realization\.

### C\.2Retain\-Set Statistics Proof State

##### Initialization\.

At initialization, letA^H=fls⁡\(\|X0\|⊤​\|X0\|\)\\widehat\{A\}\_\{H\}=\\operatorname\{fl\}\_\{\\rm s\}\(\\left\\lvert X\_\{0\}\\right\\rvert^\{\\top\}\\left\\lvert X\_\{0\}\\right\\rvert\)andA^B=fls⁡\(\|X0\|⊤​\|Y0\|\)\\widehat\{A\}\_\{B\}=\\operatorname\{fl\}\_\{\\rm s\}\(\\left\\lvert X\_\{0\}\\right\\rvert^\{\\top\}\\left\\lvert Y\_\{0\}\\right\\rvert\)\. Reverse dot\-product bounds instantiate the enclosure below\. The declared ridge is interpreted as the exact real value of its stored encoding; the displayed rounding term covers its addition to the stored diagonal\.

𝒰H\(0\)\\displaystyle\\mathcal\{U\}\_\{H\}^\{\(0\)\}=up⁡\(γn0\(s\)1−γn0\(s\)​A^H\+u¯s​\|H~0\|\)∈ℝ≥0d×d,\\displaystyle=\\operatorname\{up\}\\\!\\left\(\\frac\{\\gamma\_\{n\_\{0\}\}^\{\(\\mathrm\{s\}\)\}\}\{1\-\\gamma\_\{n\_\{0\}\}^\{\(\\mathrm\{s\}\)\}\}\\widehat\{A\}\_\{H\}\+\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widetilde\{H\}\_\{0\}\\right\\rvert\\right\)\\in\\mathbb\{R\}\_\{\\geq 0\}^\{d\\times d\},\(13\)𝒰B\(0\)\\displaystyle\\mathcal\{U\}\_\{B\}^\{\(0\)\}=up⁡\(γn0\(s\)1−γn0\(s\)​A^B\)∈ℝ≥0d×c,\\displaystyle=\\operatorname\{up\}\\\!\\left\(\\frac\{\\gamma\_\{n\_\{0\}\}^\{\(\\mathrm\{s\}\)\}\}\{1\-\\gamma\_\{n\_\{0\}\}^\{\(\\mathrm\{s\}\)\}\}\\widehat\{A\}\_\{B\}\\right\)\\in\\mathbb\{R\}\_\{\\geq 0\}^\{d\\times c\},

##### Shared initialization across precisions\.

When two storage precisions share one binary64 initialization, the lower\-precision path instead uses the direct cast enclosure

𝒰H,s\(0\)=up⁡\(𝒰H,v\(0\)\+\|casts⁡\(H~0,v\)−H~0,v\|\),\\mathcal\{U\}\_\{H,\{\\rm s\}\}^\{\(0\)\}=\\operatorname\{up\}\\\!\\left\(\\mathcal\{U\}\_\{H,\{\\rm v\}\}^\{\(0\)\}\+\\left\\lvert\\operatorname\{cast\}\_\{\\rm s\}\(\\widetilde\{H\}\_\{0,\{\\rm v\}\}\)\-\\widetilde\{H\}\_\{0,\{\\rm v\}\}\\right\\rvert\\right\),and analogously forBB\. This preserves a common exact data target while isolating the precision used to maintain the stored statistics\. We use this shared initialization only for the matched FP32/FP64 diagnostic in[SectionE\.4](https://arxiv.org/html/2610.02268#A5.SS4), so the two arms differ in subsequent storage precision rather than in their exact data target\.

##### Signed rank\-one updates\.

For an update signs∈\{−1,\+1\}s\\in\\\{\-1,\+1\\\}, letG^H:=fls⁡\(x​x⊤\)∈𝔽sd×d\\widehat\{G\}\_\{H\}:=\\operatorname\{fl\}\_\{\\rm s\}\(xx^\{\\top\}\)\\in\\mathbb\{F\}\_\{\\rm s\}^\{d\\times d\}andG^B:=fls⁡\(x​y⊤\)∈𝔽sd×c\\widehat\{G\}\_\{B\}:=\\operatorname\{fl\}\_\{\\rm s\}\(xy^\{\\top\}\)\\in\\mathbb\{F\}\_\{\\rm s\}^\{d\\times c\}\. The row entriesx,yx,yare values in𝔽s\\mathbb\{F\}\_\{\\rm s\}, interpreted exactly as reals\. The implementation sets

H~\+:=fls⁡\(H~\+s​G^H\),B~\+:=fls⁡\(B~\+s​G^B\)\\widetilde\{H\}^\{\+\}:=\\operatorname\{fl\}\_\{\\rm s\}\(\\widetilde\{H\}\+s\\widehat\{G\}\_\{H\}\),\\qquad\\widetilde\{B\}^\{\+\}:=\\operatorname\{fl\}\_\{\\rm s\}\(\\widetilde\{B\}\+s\\widehat\{G\}\_\{B\}\)and updates

𝒰H\+\\displaystyle\\mathcal\{U\}\_\{H\}^\{\+\}:=up⁡\(𝒰H\+u¯s​\|G^H\|\+u¯s​\|H~\+\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\mathcal\{U\}\_\{H\}\+\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widehat\{G\}\_\{H\}\\right\\rvert\+\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widetilde\{H\}^\{\+\}\\right\\rvert\\right\),\(14\)𝒰B\+\\displaystyle\\mathcal\{U\}\_\{B\}^\{\+\}:=up⁡\(𝒰B\+u¯s​\|G^B\|\+u¯s​\|B~\+\|\)\.\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\mathcal\{U\}\_\{B\}\+\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widehat\{G\}\_\{B\}\\right\\rvert\+\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widetilde\{B\}^\{\+\}\\right\\rvert\\right\)\.\(15\)
Each update adds the local outer\-product and storage\-rounding errors to the existing statistics enclosure\. The following theorem establishes that this enclosure remains valid after every committed update\.

###### Theorem 2\(Statistics\-error\-bound soundness\)\.

Suppose the current state satisfies\|H~−H\|≤𝒰H\\left\\lvert\\widetilde\{H\}\-H\\right\\rvert\\leq\\mathcal\{U\}\_\{H\}and\|B~−B\|≤𝒰B\\left\\lvert\\widetilde\{B\}\-B\\right\\rvert\\leq\\mathcal\{U\}\_\{B\}\. Fors∈\{−1,\+1\}s\\in\\\{\-1,\+1\\\}, letH\+=H\+s​x​x⊤H^\{\+\}=H\+sxx^\{\\top\}andB\+=B\+s​x​y⊤B^\{\+\}=B\+sxy^\{\\top\}\. Whenever the certified arithmetic\-scope guards pass, the updates in[Equations14](https://arxiv.org/html/2610.02268#A3.E14)and[15](https://arxiv.org/html/2610.02268#A3.E15)satisfy

\|H~\+−H\+\|≤𝒰H\+,\|B~\+−B\+\|≤𝒰B\+\.\\left\\lvert\\widetilde\{H\}^\{\+\}\-H^\{\+\}\\right\\rvert\\leq\\mathcal\{U\}\_\{H\}^\{\+\},\\qquad\\left\\lvert\\widetilde\{B\}^\{\+\}\-B^\{\+\}\\right\\rvert\\leq\\mathcal\{U\}\_\{B\}^\{\+\}\.The initialization in[Equation13](https://arxiv.org/html/2610.02268#A3.E13)also encloses the exact statistics represented byX0,Y0X\_\{0\},Y\_\{0\}and the declared ridge encoding\. A failed guard makes the transition noncommittable\.

Proof of statistics\-error\-bound soundnessForHH, inserting the exact outer product gives\|H~\+−H\+\|\\displaystyle\\left\\lvert\\widetilde\{H\}^\{\+\}\-H^\{\+\}\\right\\rvert≤\|H~−H\|\+\|G^H−x​x⊤\|\\displaystyle\\leq\\left\\lvert\\widetilde\{H\}\-H\\right\\rvert\+\\left\\lvert\\widehat\{G\}\_\{H\}\-xx^\{\\top\}\\right\\rvert\+\|H~\+−\(H~\+s​G^H\)\|\.\\displaystyle\+\\left\\lvert\\widetilde\{H\}^\{\+\}\-\(\\widetilde\{H\}\+s\\widehat\{G\}\_\{H\}\)\\right\\rvert\.The standard componentwise models of[Higham \(2002, Ch\. 3\)](https://arxiv.org/html/2610.02268#bib.bib7)bound the last two terms byu¯s​\|G^H\|\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widehat\{G\}\_\{H\}\\right\\rvertandu¯s​\|H~\+\|\\bar\{u\}\_\{\\rm s\}\\left\\lvert\\widetilde\{H\}^\{\+\}\\right\\rvert, respectively\. Combining them with the previous enclosure proves[Equation14](https://arxiv.org/html/2610.02268#A3.E14); the same argument applies toBB\. The standard dot\-product model gives the initialization radii, and induction establishes[Equation7](https://arxiv.org/html/2610.02268#S4.E7)after every committed update\.

### C\.3Exact\-Dyadic Retain\-Set\-Statistics Rebuild

A retained\-data rebuild constructs statistics enclosures independently of accumulated update errors\. For each statistic entry, integer accumulation computes the exact dyadic sumξ\\xi\. The procedure storesξ~=RN64⁡\(ξ\)\\widetilde\{\\xi\}=\\operatorname\{RN\}\_\{64\}\(\\xi\)and rounds\|ξ~−ξ\|\\left\\lvert\\widetilde\{\\xi\}\-\\xi\\right\\rvertoutward to obtain the enclosure radius\. Any nonfinite conversion returnsInconclusive\. Binary floating\-point products are dyadic, so integer accumulation is exact before the single final rounding\. The resulting entrywise radii therefore satisfy the initialization hypotheses of[Theorem2](https://arxiv.org/html/2610.02268#Thmtheorem2); successful inverse\-state initialization and recertification then permit release under[Theorem1](https://arxiv.org/html/2610.02268#Thmtheorem1)\.

We distinguish three event types in the implementation records\. An*evidence rebuild*replaces only inverse or factor proof state\. A*verifier\-statistics reconstruction*replaces the verifier’s retained statistics and their enclosures\. Neither event changes the candidate, and the producer does not read the rebuilt arrays\. A*producer remediation*instead changes producer state or recomputes the output; it creates a new candidate with a new hash and may alter subsequent outputs, so it is recorded and certified separately\. Same\-output comparisons include only the first two event types\.

Reconstruction visitsO⁡\(nt​d2\+nt​d​c\)O\(n\_\{t\}d^\{2\}\+n\_\{t\}dc\)dot\-product terms; subsequent proof\-state initialization and certification have the costs in[SectionB\.4](https://arxiv.org/html/2610.02268#A2.SS4)\.

### C\.4Stored\-to\-Retain\-Set Transfer

The retain\-set statistics enclosure from[SectionC\.2](https://arxiv.org/html/2610.02268#A3.SS2)and the propagated defect enclosure from[SectionC\.6](https://arxiv.org/html/2610.02268#A3.SS6)provide the executable\(δ,ρ\)\(\\delta,\\rho\)required by[Lemma1](https://arxiv.org/html/2610.02268#Thmlemma1)\. LetR^=fl⁡\(B~−H~​θ~\)\\widehat\{R\}=\\operatorname\{fl\}\(\\widetilde\{B\}\-\\widetilde\{H\}\\widetilde\{\\theta\}\)and define

𝒰R:=up⁡\(γd​\|H~\|​\|θ~\|\+u¯​\|R^\|\+𝒰B\+𝒰H​\|θ~\|\)\.\\mathcal\{U\}\_\{R\}:=\\operatorname\{up\}\\\!\\left\(\\gamma\_\{d\}\\left\\lvert\\widetilde\{H\}\\right\\rvert\\left\\lvert\\widetilde\{\\theta\}\\right\\rvert\+\\bar\{u\}\\left\\lvert\\widehat\{R\}\\right\\rvert\+\\mathcal\{U\}\_\{B\}\+\\mathcal\{U\}\_\{H\}\\left\\lvert\\widetilde\{\\theta\}\\right\\rvert\\right\)\.\(16\)The first two terms bound floating\-point evaluation of the stored residual\. The last two account for the difference between the stored statistics and the exact retain\-set statistics\. The envelope in[Equation16](https://arxiv.org/html/2610.02268#A3.E16), the standard matrix\-product and subtraction models, and[Equations7](https://arxiv.org/html/2610.02268#S4.E7)and[9](https://arxiv.org/html/2610.02268#S4.E9)give

\|B−H​θ~−R^\|≤𝒰R\.\\left\\lvert B\-H\\widetilde\{\\theta\}\-\\widehat\{R\}\\right\\rvert\\leq\\mathcal\{U\}\_\{R\}\.Withδstored=up⁡\(‖E^‖F\+r\)\\delta\_\{\\rm stored\}=\\operatorname\{up\}\(\\left\\lVert\\widehat\{E\}\\right\\rVert\_\{F\}\+r\), write‖A‖2¯\\overline\{\\left\\lVert A\\right\\rVert\_\{2\}\}for the quadratic\-cost upper bound

up⁡\(up⁡\(‖A‖1\)​up⁡\(‖A‖∞\)\)\.\\operatorname\{up\}\\\!\\left\(\\sqrt\{\\operatorname\{up\}\(\\left\\lVert A\\right\\rVert\_\{1\}\)\\operatorname\{up\}\(\\left\\lVert A\\right\\rVert\_\{\\infty\}\)\}\\right\)\.We next combine this residual enclosure with the stored inverse\-defect bound to obtain the two hypotheses required by[Lemma1](https://arxiv.org/html/2610.02268#Thmlemma1):

δret\\displaystyle\\delta\_\{\\rm ret\}=up⁡\(δstored\+‖P‖2¯​‖𝒰H‖2¯\),\\displaystyle=\\operatorname\{up\}\\\!\\left\(\\delta\_\{\\rm stored\}\+\\overline\{\\left\\lVert P\\right\\rVert\_\{2\}\}\\,\\overline\{\\left\\lVert\\mathcal\{U\}\_\{H\}\\right\\rVert\_\{2\}\}\\right\),\(17\)ρret\\displaystyle\\rho\_\{\\rm ret\}=up⁡\(‖fl⁡\(P​R^\)‖FCLOSE\\displaystyle=\\operatorname\{up\}\\\!\\left\(\\left\\lVert\\operatorname\{fl\}\(P\\widehat\{R\}\)\\right\\rVert\_\{F\}\\right\.\+‖up⁡\(γd​\|P\|​\|R^\|\)‖F\\displaystyle\\left\.\{\}\+\\left\\lVert\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert P\\right\\rvert\\left\\lvert\\widehat\{R\}\\right\\rvert\)\\right\\rVert\_\{F\}\\right\.OPEN\+‖up⁡\(\|P\|​𝒰R\)‖F\)\.\\displaystyle\\left\.\{\}\+\\left\\lVert\\operatorname\{up\}\(\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{R\}\)\\right\\rVert\_\{F\}\\right\)\.
Proof of the executable joint boundsThe matrix\-product model and the residual budget give‖P⁡\(B−H​θ~\)‖F\\displaystyle\\left\\lVert P\(B\-H\\widetilde\{\\theta\}\)\\right\\rVert\_\{F\}≤‖P​R^‖F\+‖\|P\|​𝒰R‖F\\displaystyle\\leq\\left\\lVert P\\widehat\{R\}\\right\\rVert\_\{F\}\+\\left\\lVert\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{R\}\\right\\rVert\_\{F\}≤‖fl⁡\(P​R^\)‖F\+‖up⁡\(γd​\|P\|​\|R^\|\)‖F\\displaystyle\\leq\\left\\lVert\\operatorname\{fl\}\(P\\widehat\{R\}\)\\right\\rVert\_\{F\}\+\\left\\lVert\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert P\\right\\rvert\\left\\lvert\\widehat\{R\}\\right\\rvert\)\\right\\rVert\_\{F\}\+‖up⁡\(\|P\|​𝒰R\)‖F≤ρret,\\displaystyle\+\\left\\lVert\\operatorname\{up\}\(\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{R\}\)\\right\\rVert\_\{F\}\\leq\\rho\_\{\\rm ret\},which proves the residual hypothesis in[Equation4](https://arxiv.org/html/2610.02268#S4.E4)\.For the defect, supposer∈ℝ≥0r\\in\\mathbb\{R\}\_\{\\geq 0\}satisfies‖E−E^‖F≤r\\left\\lVert E\-\\widehat\{E\}\\right\\rVert\_\{F\}\\leq r\. BecauseId−P​H=\(Id−P​H~\)\+P⁡\(H~−H\)I\_\{d\}\-PH=\(I\_\{d\}\-P\\widetilde\{H\}\)\+P\(\\widetilde\{H\}\-H\),‖Id−P​H‖2\\displaystyle\\left\\lVert I\_\{d\}\-PH\\right\\rVert\_\{2\}≤‖E^‖F\+r\+‖P‖2​‖H~−H‖2\\displaystyle\\leq\\left\\lVert\\widehat\{E\}\\right\\rVert\_\{F\}\+r\+\\left\\lVert P\\right\\rVert\_\{2\}\\left\\lVert\\widetilde\{H\}\-H\\right\\rVert\_\{2\}≤‖E^‖F\+r\+‖P‖2¯​‖𝒰H‖2¯≤δret\.\\displaystyle\\leq\\left\\lVert\\widehat\{E\}\\right\\rVert\_\{F\}\+r\+\\overline\{\\left\\lVert P\\right\\rVert\_\{2\}\}\\,\\overline\{\\left\\lVert\\mathcal\{U\}\_\{H\}\\right\\rVert\_\{2\}\}\\leq\\delta\_\{\\rm ret\}\.The second line follows from‖A‖2≤‖A‖1​‖A‖∞\\left\\lVert A\\right\\rVert\_\{2\}\\leq\\sqrt\{\\left\\lVert A\\right\\rVert\_\{1\}\\left\\lVert A\\right\\rVert\_\{\\infty\}\}and\|H~−H\|≤𝒰H\\left\\lvert\\widetilde\{H\}\-H\\right\\rvert\\leq\\mathcal\{U\}\_\{H\}, which implies‖H~−H‖1≤‖𝒰H‖1\\left\\lVert\\widetilde\{H\}\-H\\right\\rVert\_\{1\}\\leq\\left\\lVert\\mathcal\{U\}\_\{H\}\\right\\rVert\_\{1\}and likewise for the infinity norm\. The final inequalities are the two bounds in[Equation17](https://arxiv.org/html/2610.02268#A3.E17), which supply both hypotheses of[Lemma1](https://arxiv.org/html/2610.02268#Thmlemma1)\. The row and column sums used by the two induced\-norm bounds costO⁡\(d2\)O\(d^\{2\}\); the remaining residual products costO⁡\(d2​c\)O\(d^\{2\}c\)\. No dense matrix–matrix product is evaluated on this release path\.

Retaining componentwise arrays preserves the directional residual interaction\|P\|​𝒰R\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{R\}, while the defect transfer avoids forming the dense matrix product\|P\|​𝒰H\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{H\}\.

### C\.5Executable Release Certificates

#### C\.5\.1Parameter Certificate

Substituting the transferred bounds into[Lemma1](https://arxiv.org/html/2610.02268#Thmlemma1)gives the absolute parameter certificate, provided the bounds are finite andδret<1\\delta\_\{\\rm ret\}<1\. For the relative contract, letp=d​cp=dc, compute the scale\-safe floating\-point norms^=fl⁡\(‖θ~‖F\)\\widehat\{s\}=\\operatorname\{fl\}\(\\left\\lVert\\widetilde\{\\theta\}\\right\\rVert\_\{F\}\), and form the certified lower endpoint

s−:=down⁡\(s^1\+γ2​p\+2\),d−:=down⁡\(s−−C\)\.s^\{\-\}:=\\operatorname\{down\}\\\!\\left\(\\frac\{\\widehat\{s\}\}\{1\+\\gamma\_\{2p\+2\}\}\\right\),\\qquad d^\{\-\}:=\\operatorname\{down\}\(s^\{\-\}\-C\)\.The verifier requiresd−\>0d^\{\-\}\>0, then computesτrel\+:=up⁡\(C/d−\)\\tau\_\{\\rm rel\}^\{\+\}:=\\operatorname\{up\}\(C/d^\{\-\}\)and certifies only whenτrel\+≤τpar\\tau\_\{\\rm rel\}^\{\+\}\\leq\\tau\_\{\\rm par\}\. Thus the norm lower bound, denominator subtraction, and final division are all directed outward\.

#### C\.5\.2Fixed\-Readout Error Center

LetΔ=θR−θ~\\Delta=\\theta^\{\\mathrm\{R\}\}\-\\widetilde\{\\theta\}\. The corrected residual provides an approximate center for this parameter error\. Applying the fixed readout to the center preserves information about the error direction before the remaining uncertainty is bounded\. Define

Δ^\\displaystyle\\widehat\{\\Delta\}=fl⁡\(P​R^\),\\displaystyle=\\operatorname\{fl\}\(P\\widehat\{R\}\),𝒰cfl\\displaystyle\\mathcal\{U\}\_\{c\}^\{\\rm fl\}=up⁡\(γd​\|P\|​\|R^\|\),\\displaystyle=\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert P\\right\\rvert\\left\\lvert\\widehat\{R\}\\right\\rvert\),𝒰ctr\\displaystyle\\mathcal\{U\}\_\{c\}^\{\\rm tr\}=up⁡\(\|P\|​𝒰R\)\.\\displaystyle=\\operatorname\{up\}\(\\left\\lvert P\\right\\rvert\\mathcal\{U\}\_\{R\}\)\.Their sum enclosesΔ^−P⁡\(B−H​θ~\)\\widehat\{\\Delta\}\-P\(B\-H\\widetilde\{\\theta\}\), so the executable center\-evaluation radius is

ηc\\displaystyle\\eta\_\{c\}=up⁡\(‖𝒰cfl‖F\+‖𝒰ctr‖F\),\\displaystyle=\\operatorname\{up\}\\\!\\left\(\\left\\lVert\\mathcal\{U\}\_\{c\}^\{\\rm fl\}\\right\\rVert\_\{F\}\+\\left\\lVert\\mathcal\{U\}\_\{c\}^\{\\rm tr\}\\right\\rVert\_\{F\}\\right\),RΔ\\displaystyle R\_\{\\Delta\}=up⁡\(ηc\+δret​C\)\.\\displaystyle=\\operatorname\{up\}\(\\eta\_\{c\}\+\\delta\_\{\\rm ret\}C\)\.The inverse\-defect bound gives‖Δ−P⁡\(B−H​θ~\)‖F≤δret​C\\left\\lVert\\Delta\-P\(B\-H\\widetilde\{\\theta\}\)\\right\\rVert\_\{F\}\\leq\\delta\_\{\\rm ret\}C; therefore‖Δ−Δ^‖F≤RΔ\\left\\lVert\\Delta\-\\widehat\{\\Delta\}\\right\\rVert\_\{F\}\\leq R\_\{\\Delta\}, as required by[Proposition1](https://arxiv.org/html/2610.02268#Thmproposition1)\. For a fixed readoutZZ, computey^=fl⁡\(Z​Δ^\)\\widehat\{y\}=\\operatorname\{fl\}\(Z\\widehat\{\\Delta\}\)and

𝒰y=up⁡\(γd​\|Z\|​\|Δ^\|\)\.\\mathcal\{U\}\_\{y\}=\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert Z\\right\\rvert\\left\\lvert\\widehat\{\\Delta\}\\right\\rvert\)\.The two sound readout bounds used by the implementation are

CZball\\displaystyle C\_\{Z\}^\{\\rm ball\}=up⁡\(‖Z‖2¯​C\),\\displaystyle=\\operatorname\{up\}\(\\overline\{\\left\\lVert Z\\right\\rVert\_\{2\}\}\\,C\),CZctr\\displaystyle C\_\{Z\}^\{\\rm ctr\}=up⁡\(‖y^‖F\+‖𝒰y‖F\+‖Z‖2¯​RΔ\)\.\\displaystyle=\\operatorname\{up\}\\\!\\left\(\\left\\lVert\\widehat\{y\}\\right\\rVert\_\{F\}\+\\left\\lVert\\mathcal\{U\}\_\{y\}\\right\\rVert\_\{F\}\+\\overline\{\\left\\lVert Z\\right\\rVert\_\{2\}\}\\,R\_\{\\Delta\}\\right\)\.The fixed readout is preprocessed once with the rigorous bound

‖Z‖2¯=min⁡\{up⁡\(‖Z‖F\),up⁡\(u1​u∞\)\}\.\\overline\{\\left\\lVert Z\\right\\rVert\_\{2\}\}=\\min\\\!\\left\\\{\\operatorname\{up\}\(\\left\\lVert Z\\right\\rVert\_\{F\}\),\\operatorname\{up\}\\\!\\left\(\\sqrt\{u\_\{1\}u\_\{\\infty\}\}\\right\)\\right\\\}\.Hereu1=up⁡\(‖Z‖1\)u\_\{1\}=\\operatorname\{up\}\(\\left\\lVert Z\\right\\rVert\_\{1\}\)andu∞=up⁡\(‖Z‖∞\)u\_\{\\infty\}=\\operatorname\{up\}\(\\left\\lVert Z\\right\\rVert\_\{\\infty\}\)\. Both terms upper\-bound‖Z‖2\\left\\lVert Z\\right\\rVert\_\{2\}, so their minimum remains rigorous\. The verifier returnsmin⁡\{CZball,CZctr\}/m​c\\min\\\{C\_\{Z\}^\{\\rm ball\},C\_\{Z\}^\{\\rm ctr\}\\\}/\\sqrt\{mc\}for the normalized contract in[Equation3](https://arxiv.org/html/2610.02268#S3.E3)\. Every displayed operation is evaluated outward, and the range and finiteness guards from[SectionC\.1](https://arxiv.org/html/2610.02268#A3.SS1)apply before the minimum is used\. Formmfixed readout rows, the added work isO⁡\(m​d​c\)O\(mdc\); the center usesO⁡\(d​c\)O\(dc\)state, while storingZZrequiresO⁡\(m​d\)O\(md\)entries unless the service already retains the readout\.

### C\.6Sequential Inverse Proof State

#### C\.6\.1State invariant and strict initialization

The maintained inverse state consists ofPP, a computed defect trackerE^\\widehat\{E\}, and a certified radiusrrsatisfying

‖Id−P​H~−E^‖F≤r\.\\left\\lVert I\_\{d\}\-P\\widetilde\{H\}\-\\widehat\{E\}\\right\\rVert\_\{F\}\\leq r\.Strict initialization evaluates the defect directly and encloses its arithmetic error\.

Throughout this subsection,H~\\widetilde\{H\}denotes the exact\-real embedding of the entries of the stored floating\-point array, whether that array is held in binary32 or binary64\. WriteHHfor the exact retain\-set matrix\. Thus the tracked defect isE=Id−P​H~E=I\_\{d\}\-P\\widetilde\{H\}, while the statistics\-error bound later transfers this bound toId−P​HI\_\{d\}\-PH\.

At strict initialization, letE^0:=fl⁡\(Id−P0​H~0\)∈𝔽64d×d\\widehat\{E\}\_\{0\}:=\\operatorname\{fl\}\(I\_\{d\}\-P\_\{0\}\\widetilde\{H\}\_\{0\}\)\\in\\mathbb\{F\}\_\{64\}^\{d\\times d\}, whereP0,H~0∈𝔽64d×dP\_\{0\},\\widetilde\{H\}\_\{0\}\\in\\mathbb\{F\}\_\{64\}^\{d\\times d\}\. The standard product and subtraction models give

r0:=up⁡\(‖up⁡\(γd​\|P0\|​\|H~0\|\+u¯​\|E^0\|\)‖F\)∈ℝ≥0\.r\_\{0\}:=\\operatorname\{up\}\\\!\\left\(\\left\\lVert\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert P\_\{0\}\\right\\rvert\\left\\lvert\\widetilde\{H\}\_\{0\}\\right\\rvert\+\\bar\{u\}\\left\\lvert\\widehat\{E\}\_\{0\}\\right\\rvert\)\\right\\rVert\_\{F\}\\right\)\\in\\mathbb\{R\}\_\{\\geq 0\}\.It satisfies‖Id−P0​H~0−E^0‖F≤r0\\left\\lVert I\_\{d\}\-P\_\{0\}\\widetilde\{H\}\_\{0\}\-\\widehat\{E\}\_\{0\}\\right\\rVert\_\{F\}\\leq r\_\{0\}, establishing the base case before any rank\-one transition is attempted\.

Each accepted transition adds three local error budgets to the previous radius:

r\+=up⁡\(r\+ηalg\+ηstate\+ηfl\)\.r^\{\+\}=\\operatorname\{up\}\\\!\\left\(r\+\\eta\_\{\\mathrm\{alg\}\}\+\\eta\_\{\\mathrm\{state\}\}\+\\eta\_\{\\mathrm\{fl\}\}\\right\)\.Hereηalg\\eta\_\{\\rm alg\}encloses the use of computed low\-rank intermediates,ηstate\\eta\_\{\\rm state\}the storage error in the updated arrays, andηfl\\eta\_\{\\rm fl\}the evaluation error in the defect tracker\.

#### C\.6\.2Local arithmetic bounds

Before an update, letP,H~∈𝔽64d×dP,\\widetilde\{H\}\\in\\mathbb\{F\}\_\{64\}^\{d\\times d\},x∈𝔽64dx\\in\\mathbb\{F\}\_\{64\}^\{d\},s∈\{−1,\+1\}s\\in\\\{\-1,\+1\\\}, andE:=Id−P​H~E:=I\_\{d\}\-P\\widetilde\{H\}, with stored values embedded exactly in the reals\. Define

q\\displaystyle q=P​x,\\displaystyle=Px,z\\displaystyle z=P⊤​x,\\displaystyle=P^\{\\top\}x,β\\displaystyle\\beta=x⊤​q=z⊤​x,\\displaystyle=x^\{\\top\}q=z^\{\\top\}x,α\\displaystyle\\alpha=1\+s​β,\\displaystyle=1\+s\\beta,q^\\displaystyle\\widehat\{q\}=fl⁡\(P​x\),\\displaystyle=\\operatorname\{fl\}\(Px\),z^\\displaystyle\\widehat\{z\}=fl⁡\(P⊤​x\),\\displaystyle=\\operatorname\{fl\}\(P^\{\\top\}x\),β^\\displaystyle\\widehat\{\\beta\}=fl⁡\(x⊤​q^\),\\displaystyle=\\operatorname\{fl\}\(x^\{\\top\}\\widehat\{q\}\),α^\\displaystyle\\widehat\{\\alpha\}=fl⁡\(1\+s​β^\)\.\\displaystyle=\\operatorname\{fl\}\(1\+s\\widehat\{\\beta\}\)\.For comparison with the computed intermediates, set

β∘:=x⊤​q^,α∘:=1\+s​β∘\.\\beta^\{\\circ\}:=x^\{\\top\}\\widehat\{q\},\\qquad\\alpha^\{\\circ\}:=1\+s\\beta^\{\\circ\}\.The standard matrix–vector model gives

εq\\displaystyle\\varepsilon\_\{q\}:=up⁡\(γd​\|P\|​\|x\|\),\\displaystyle:=\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert P\\right\\rvert\\left\\lvert x\\right\\rvert\),\|q−q^\|\\displaystyle\\left\\lvert q\-\\widehat\{q\}\\right\\rvert≤εq,\\displaystyle\\leq\\varepsilon\_\{q\},εz\\displaystyle\\varepsilon\_\{z\}:=up⁡\(γd​\|P⊤\|​\|x\|\),\\displaystyle:=\\operatorname\{up\}\(\\gamma\_\{d\}\\left\\lvert P^\{\\top\}\\right\\rvert\\left\\lvert x\\right\\rvert\),\|z−z^\|\\displaystyle\\left\\lvert z\-\\widehat\{z\}\\right\\rvert≤εz\.\\displaystyle\\leq\\varepsilon\_\{z\}\.
##### Certified denominator guard\.

The implementation forms

εα,fl\\displaystyle\\varepsilon\_\{\\alpha,\\mathrm\{fl\}\}:=up⁡\(γd​up⁡\(\|x\|⊤​\|q^\|\)\+\|TwoSum⁡\(1,s​β^,α^\)\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\gamma\_\{d\}\\operatorname\{up\}\(\\left\\lvert x\\right\\rvert^\{\\top\}\\left\\lvert\\widehat\{q\}\\right\\rvert\)\+\\left\\lvert\\operatorname\{TwoSum\}\(1,s\\widehat\{\\beta\};\\widehat\{\\alpha\}\)\\right\\rvert\\right\),εα\\displaystyle\\varepsilon\_\{\\alpha\}:=up⁡\(εα,fl\+\|x\|⊤​εq\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\varepsilon\_\{\\alpha,\\mathrm\{fl\}\}\+\\left\\lvert x\\right\\rvert^\{\\top\}\\varepsilon\_\{q\}\\right\),εq​z\\displaystyle\\varepsilon\_\{qz\}:=up⁡\(\|x\|⊤​\(εq\+εz\)\)\.\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\left\\lvert x\\right\\rvert^\{\\top\}\(\\varepsilon\_\{q\}\+\\varepsilon\_\{z\}\)\\right\)\.The standard dot\-product model and exactTwoSumresidual give\|α−α^\|≤εα\\left\\lvert\\alpha\-\\widehat\{\\alpha\}\\right\\rvert\\leq\\varepsilon\_\{\\alpha\}\. Henceα^\>εα\\widehat\{\\alpha\}\>\\varepsilon\_\{\\alpha\}certifiesα\>0\\alpha\>0before any division\. An additionalu​\(1\+\|β^\|\)\\sqrt\{u\}\(1\+\\left\\lvert\\widehat\{\\beta\}\\right\\rvert\)policy floor sends numerically fragile positive denominators to the rebuild path; it is not used in the soundness argument\.

The guard ensuresα^≠0\\widehat\{\\alpha\}\\neq 0\. Define the exact\-real matrices formed from the computed low\-rank intermediates,

P\+⁣∘\\displaystyle P^\{\+\\circ\}:=P−s​q^​z^⊤α^,\\displaystyle:=P\-\\frac\{s\\widehat\{q\}\\widehat\{z\}^\{\\top\}\}\{\\widehat\{\\alpha\}\},H\+⁣∘\\displaystyle H^\{\+\\circ\}:=H~\+s​x​x⊤,\\displaystyle:=\\widetilde\{H\}\+sxx^\{\\top\},E\+⁣∘\\displaystyle E^\{\+\\circ\}:=Id−P\+⁣∘​H\+⁣∘\.\\displaystyle:=I\_\{d\}\-P^\{\+\\circ\}H^\{\+\\circ\}\.The implementation storesP\+P^\{\+\}in binary64 andH~\+\\widetilde\{H\}^\{\+\}in𝔽s\\mathbb\{F\}\_\{\\rm s\}, promoting the latter exactly before tracker evaluation\. With both arrays embedded in the reals, letEstore\+:=Id−P\+​H~\+E\_\{\\mathrm\{store\}\}^\{\+\}:=I\_\{d\}\-P^\{\+\}\\widetilde\{H\}^\{\+\}and define

𝒯s∘​\(Z\):=Z−q^​sα^​\(x⊤−z^⊤​H~\),Z∈ℝd×d\.\\mathcal\{T\}\_\{s\}^\{\\circ\}\(Z\):=Z\-\\widehat\{q\}\\frac\{s\}\{\\widehat\{\\alpha\}\}\\left\(x^\{\\top\}\-\\widehat\{z\}^\{\\top\}\\widetilde\{H\}\\right\),\\qquad Z\\in\\mathbb\{R\}^\{d\\times d\}\.For this map,[Theorem3](https://arxiv.org/html/2610.02268#Thmtheorem3)requires

‖E−E^‖F\\displaystyle\\left\\lVert E\-\\widehat\{E\}\\right\\rVert\_\{F\}≤r,\\displaystyle\\leq r,‖E\+⁣∘−𝒯s∘​\(E\)‖F\\displaystyle\\left\\lVert E^\{\+\\circ\}\-\\mathcal\{T\}\_\{s\}^\{\\circ\}\(E\)\\right\\rVert\_\{F\}≤ηalg,\\displaystyle\\leq\\eta\_\{\\mathrm\{alg\}\},‖Estore\+−E\+⁣∘‖F\\displaystyle\\left\\lVert E\_\{\\mathrm\{store\}\}^\{\+\}\-E^\{\+\\circ\}\\right\\rVert\_\{F\}≤ηstate,\\displaystyle\\leq\\eta\_\{\\mathrm\{state\}\},‖𝒯s∘​\(E^\)−E^\+‖F\\displaystyle\\left\\lVert\\mathcal\{T\}\_\{s\}^\{\\circ\}\(\\widehat\{E\}\)\-\\widehat\{E\}^\{\+\}\\right\\rVert\_\{F\}≤ηfl\.\\displaystyle\\leq\\eta\_\{\\mathrm\{fl\}\}\.The constructions below bound the final three terms\.

Computed\-intermediate mismatch boundThe exact vectors satisfyx⊤​z=x⊤​P⊤​x=\(x⊤​P​x\)⊤=x⊤​q,x^\{\\top\}z=x^\{\\top\}P^\{\\top\}x=\(x^\{\\top\}Px\)^\{\\top\}=x^\{\\top\}q,because both sides are real scalars\. Hence\|x⊤​\(z^−q^\)\|\\displaystyle\\left\\lvert x^\{\\top\}\(\\widehat\{z\}\-\\widehat\{q\}\)\\right\\rvert=\|x⊤​\(z^−z\)\+x⊤​\(q−q^\)\|\\displaystyle=\\left\\lvert x^\{\\top\}\(\\widehat\{z\}\-z\)\+x^\{\\top\}\(q\-\\widehat\{q\}\)\\right\\rvert≤\|x\|⊤​\(εz\+εq\)≤εq​z\.\\displaystyle\\leq\\left\\lvert x\\right\\rvert^\{\\top\}\(\\varepsilon\_\{z\}\+\\varepsilon\_\{q\}\)\\leq\\varepsilon\_\{qz\}\.ExpandingE\+⁣∘:=Id−P\+⁣∘​H\+⁣∘E^\{\+\\circ\}:=I\_\{d\}\-P^\{\+\\circ\}H^\{\+\\circ\}gives the exact identityE\+⁣∘−𝒯s∘​\(E\)\\displaystyle E^\{\+\\circ\}\-\\mathcal\{T\}\_\{s\}^\{\\circ\}\(E\)\(18\)=−s⁡\(q−q^\)​x⊤\+q^α^​\[s⁡\(α∘−α^\)\+x⊤​\(z^−q^\)\]​x⊤\.\\displaystyle=\-s\(q\-\\widehat\{q\}\)x^\{\\top\}\+\\frac\{\\widehat\{q\}\}\{\\widehat\{\\alpha\}\}\\left\[s\(\\alpha^\{\\circ\}\-\\widehat\{\\alpha\}\)\+x^\{\\top\}\(\\widehat\{z\}\-\\widehat\{q\}\)\\right\]x^\{\\top\}\.To verify the coefficient ofq^​x⊤\\widehat\{q\}x^\{\\top\}, observe that−s\+s\+x⊤​z^α^=s⁡\(α∘−α^\)\+x⊤​\(z^−q^\)α^,\-s\+\\frac\{s\+x^\{\\top\}\\widehat\{z\}\}\{\\widehat\{\\alpha\}\}=\\frac\{s\(\\alpha^\{\\circ\}\-\\widehat\{\\alpha\}\)\+x^\{\\top\}\(\\widehat\{z\}\-\\widehat\{q\}\)\}\{\\widehat\{\\alpha\}\},whereα∘=1\+s​x⊤​q^\\alpha^\{\\circ\}=1\+sx^\{\\top\}\\widehat\{q\}\. The componentwise budgets and‖a​b⊤‖F=‖a‖2​‖b‖2\\\|ab^\{\\top\}\\\|\_\{F\}=\\\|a\\\|\_\{2\}\\\|b\\\|\_\{2\}now implyηalg:=up⁡\(CLOSE\\displaystyle\\eta\_\{\\mathrm\{alg\}\}:=\\operatorname\{up\}\\\!\\Bigl\(‖εq‖2​‖x‖2\\displaystyle\\left\\lVert\\varepsilon\_\{q\}\\right\\rVert\_\{2\}\\left\\lVert x\\right\\rVert\_\{2\}OPEN\+εα,fl\+εq​z\|α^\|​‖q^‖2​‖x‖2\)∈ℝ≥0\.\\displaystyle\+\\frac\{\\varepsilon\_\{\\alpha,\\mathrm\{fl\}\}\+\\varepsilon\_\{qz\}\}\{\\left\\lvert\\widehat\{\\alpha\}\\right\\rvert\}\\left\\lVert\\widehat\{q\}\\right\\rVert\_\{2\}\\left\\lVert x\\right\\rVert\_\{2\}\\Bigr\)\\in\\mathbb\{R\}\_\{\\geq 0\}\.This quantity upper\-bounds the Frobenius norm of[Equation18](https://arxiv.org/html/2610.02268#A3.E18)\.

##### Stored\-state update error\.

LetΔP:=−sq^z^⊤/α^\\Delta P:=\-s\\widehat\{q\}\\widehat\{z\}^\{\\top\}/\\widehat\{\\alpha\},Δ​H:=s​x​x⊤\\Delta H:=sxx^\{\\top\},Δ​P^:=fl64⁡\(Δ​P\)\\widehat\{\\Delta P\}:=\\operatorname\{fl\}\_\{64\}\(\\Delta P\), and, for binary64 statistics,Δ​H^:=s​fl64⁡\(x​x⊤\)\\widehat\{\\Delta H\}:=s\\operatorname\{fl\}\_\{64\}\(xx^\{\\top\}\)\. The standard models in[SectionC\.1](https://arxiv.org/html/2610.02268#A3.SS1), including the exact componentwiseTwoSumresidualsSP=\(P\+Δ​P^\)−P\+S\_\{P\}=\(P\+\\widehat\{\\Delta P\}\)\-P^\{\+\}andSH=\(H~\+Δ​H^\)−H~\+S\_\{H\}=\(\\widetilde\{H\}\+\\widehat\{\\Delta H\}\)\-\\widetilde\{H\}^\{\+\}, give

𝒰Δ​P\\displaystyle\\mathcal\{U\}\_\{\\Delta P\}:=up⁡\(γ¯2​\|Δ​P^\|\+\|SP\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\bar\{\\gamma\}\_\{2\}\\left\\lvert\\widehat\{\\Delta P\}\\right\\rvert\+\\left\\lvert S\_\{P\}\\right\\rvert\\right\),\|P\+−\(P\+Δ​P\)\|\\displaystyle\\left\\lvert P^\{\+\}\-\(P\+\\Delta P\)\\right\\rvert≤𝒰Δ​P,\\displaystyle\\leq\\mathcal\{U\}\_\{\\Delta P\},𝒰Δ​H\\displaystyle\\mathcal\{U\}\_\{\\Delta H\}:=up⁡\(u¯​\|Δ​H^\|\+\|SH\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\bar\{u\}\\left\\lvert\\widehat\{\\Delta H\}\\right\\rvert\+\\left\\lvert S\_\{H\}\\right\\rvert\\right\),\|H~\+−\(H~\+Δ​H\)\|\\displaystyle\\left\\lvert\\widetilde\{H\}^\{\+\}\-\(\\widetilde\{H\}\+\\Delta H\)\\right\\rvert≤𝒰Δ​H,\\displaystyle\\leq\\mathcal\{U\}\_\{\\Delta H\},whereγ¯2:=γ2/\(1−γ2\)\\bar\{\\gamma\}\_\{2\}:=\\gamma\_\{2\}/\(1\-\\gamma\_\{2\}\)\. For binary32 statistics, the same quantity is obtained by promoting the post\-update array exactly and enclosing its difference from the nominal update\. A product\-difference expansion then gives

ηstate:=up⁡\(CLOSE\\displaystyle\\eta\_\{\\mathrm\{state\}\}:=\\operatorname\{up\}\\\!\\big\(‖𝒰Δ​P‖F​\(‖H~‖F\+‖Δ​H‖F\)\\displaystyle\\left\\lVert\\mathcal\{U\}\_\{\\Delta P\}\\right\\rVert\_\{F\}\(\\left\\lVert\\widetilde\{H\}\\right\\rVert\_\{F\}\+\\left\\lVert\\Delta H\\right\\rVert\_\{F\}\)\+\(‖P‖F\+‖Δ​P‖F\)​‖𝒰Δ​H‖F\\displaystyle\+\(\\left\\lVert P\\right\\rVert\_\{F\}\+\\left\\lVert\\Delta P\\right\\rVert\_\{F\}\)\\left\\lVert\\mathcal\{U\}\_\{\\Delta H\}\\right\\rVert\_\{F\}OPEN\+‖𝒰Δ​P‖F​‖𝒰Δ​H‖F\)≥‖Estore\+−E\+⁣∘‖F\.\\displaystyle\+\\left\\lVert\\mathcal\{U\}\_\{\\Delta P\}\\right\\rVert\_\{F\}\\left\\lVert\\mathcal\{U\}\_\{\\Delta H\}\\right\\rVert\_\{F\}\\big\)\\geq\\left\\lVert E\_\{\\mathrm\{store\}\}^\{\+\}\-E^\{\+\\circ\}\\right\\rVert\_\{F\}\.

##### Tracker\-evaluation error\.

The tracker evaluates

w^\\displaystyle\\widehat\{w\}:=fl⁡\(H~⊤​z^\),\\displaystyle:=\\operatorname\{fl\}\(\\widetilde\{H\}^\{\\top\}\\widehat\{z\}\),v^\\displaystyle\\widehat\{v\}:=fl⁡\(x−w^\),\\displaystyle:=\\operatorname\{fl\}\(x\-\\widehat\{w\}\),a^\\displaystyle\\widehat\{a\}:=fl⁡\(\(s/α^\)​v^\),\\displaystyle:=\\operatorname\{fl\}\(\(s/\\widehat\{\\alpha\}\)\\widehat\{v\}\),C^\\displaystyle\\widehat\{C\}:=fl⁡\(q^​a^⊤\)\.\\displaystyle:=\\operatorname\{fl\}\(\\widehat\{q\}\\widehat\{a\}^\{\\top\}\)\.The standard componentwise models give

𝒰w\\displaystyle\\mathcal\{U\}\_\{w\}:=up⁡\(γd​\|H~\|⊤​\|z^\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\gamma\_\{d\}\\left\\lvert\\widetilde\{H\}\\right\\rvert^\{\\top\}\\left\\lvert\\widehat\{z\}\\right\\rvert\\right\),𝒰v\\displaystyle\\mathcal\{U\}\_\{v\}:=up⁡\(𝒰w\+u¯​\|v^\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\mathcal\{U\}\_\{w\}\+\\bar\{u\}\\left\\lvert\\widehat\{v\}\\right\\rvert\\right\),𝒰a\\displaystyle\\mathcal\{U\}\_\{a\}:=up⁡\(𝒰v/\|α^\|\+γ¯2​\|a^\|\),\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\mathcal\{U\}\_\{v\}/\\left\\lvert\\widehat\{\\alpha\}\\right\\rvert\+\\bar\{\\gamma\}\_\{2\}\\left\\lvert\\widehat\{a\}\\right\\rvert\\right\),𝒰C\\displaystyle\\mathcal\{U\}\_\{C\}:=up⁡\(\|q^\|​𝒰a⊤\+u¯​\|C^\|\)\.\\displaystyle:=\\operatorname\{up\}\\\!\\left\(\\left\\lvert\\widehat\{q\}\\right\\rvert\\mathcal\{U\}\_\{a\}^\{\\top\}\+\\bar\{u\}\\left\\lvert\\widehat\{C\}\\right\\rvert\\right\)\.Finally, letSE:=\(E^−C^\)−E^\+S\_\{E\}:=\(\\widehat\{E\}\-\\widehat\{C\}\)\-\\widehat\{E\}^\{\+\}be the exactTwoSumresidual forE^\+:=fl⁡\(E^−C^\)\\widehat\{E\}^\{\+\}:=\\operatorname\{fl\}\(\\widehat\{E\}\-\\widehat\{C\}\), and set𝒰S:=\|SE\|\\mathcal\{U\}\_\{S\}:=\\left\\lvert S\_\{E\}\\right\\rvert\. Therefore

ηfl:=up⁡\(‖𝒰C\+𝒰S‖F\)≥‖𝒯s∘​\(E^\)−E^\+‖F\.\\eta\_\{\\mathrm\{fl\}\}:=\\operatorname\{up\}\\\!\\left\(\\left\\lVert\\mathcal\{U\}\_\{C\}\+\\mathcal\{U\}\_\{S\}\\right\\rVert\_\{F\}\\right\)\\geq\\left\\lVert\\mathcal\{T\}\_\{s\}^\{\\circ\}\(\\widehat\{E\}\)\-\\widehat\{E\}^\{\+\}\\right\\rVert\_\{F\}\.

#### C\.6\.3Radius propagation theorem

###### Theorem 3\(Sequential proof\-state invariant\)\.

Suppose‖E−E^‖F≤r\\left\\lVert E\-\\widehat\{E\}\\right\\rVert\_\{F\}\\leq r\. Letηalg\\eta\_\{\\rm alg\},ηstate\\eta\_\{\\rm state\}, andηfl\\eta\_\{\\rm fl\}satisfy

‖E\+⁣∘−𝒯s∘​\(E\)‖F\\displaystyle\\left\\lVert E^\{\+\\circ\}\-\\mathcal\{T\}\_\{s\}^\{\\circ\}\(E\)\\right\\rVert\_\{F\}≤ηalg,\\displaystyle\\leq\\eta\_\{\\rm alg\},‖Estore\+−E\+⁣∘‖F\\displaystyle\\left\\lVert E\_\{\\rm store\}^\{\+\}\-E^\{\+\\circ\}\\right\\rVert\_\{F\}≤ηstate,\\displaystyle\\leq\\eta\_\{\\rm state\},‖𝒯s∘​\(E^\)−E^\+‖F\\displaystyle\\left\\lVert\\mathcal\{T\}\_\{s\}^\{\\circ\}\(\\widehat\{E\}\)\-\\widehat\{E\}^\{\+\}\\right\\rVert\_\{F\}≤ηfl\.\\displaystyle\\leq\\eta\_\{\\rm fl\}\.Then

r\+=up⁡\(r\+ηalg\+ηstate\+ηfl\)r^\{\+\}=\\operatorname\{up\}\\\!\\left\(r\+\\eta\_\{\\rm alg\}\+\\eta\_\{\\rm state\}\+\\eta\_\{\\rm fl\}\\right\)satisfies

‖Estore\+−E^\+‖F≤r\+\.\\left\\lVert E\_\{\\rm store\}^\{\+\}\-\\widehat\{E\}^\{\+\}\\right\\rVert\_\{F\}\\leq r^\{\+\}\.All three local bounds can be evaluated inO⁡\(d2\)O\(d^\{2\}\)work per rank\-one update\.

Proof of propagated\-radius soundnessThe map𝒯s∘\\mathcal\{T\}\_\{s\}^\{\\circ\}has identity linear part, so𝒯s∘​\(E\)−𝒯s∘​\(E^\)=E−E^\\mathcal\{T\}\_\{s\}^\{\\circ\}\(E\)\-\\mathcal\{T\}\_\{s\}^\{\\circ\}\(\\widehat\{E\}\)=E\-\\widehat\{E\}\. Inserting the nominal exact update and applying the triangle inequality gives‖Estore\+−E^\+‖F\\displaystyle\\left\\lVert E\_\{\\mathrm\{store\}\}^\{\+\}\-\\widehat\{E\}^\{\+\}\\right\\rVert\_\{F\}≤‖Estore\+−E\+⁣∘‖F\\displaystyle\\leq\\left\\lVert E\_\{\\mathrm\{store\}\}^\{\+\}\-E^\{\+\\circ\}\\right\\rVert\_\{F\}\+‖E\+⁣∘−𝒯s∘​\(E\)‖F\\displaystyle\+\\left\\lVert E^\{\+\\circ\}\-\\mathcal\{T\}\_\{s\}^\{\\circ\}\(E\)\\right\\rVert\_\{F\}\+‖E−E^‖F\+‖𝒯s∘​\(E^\)−E^\+‖F\\displaystyle\+\\left\\lVert E\-\\widehat\{E\}\\right\\rVert\_\{F\}\+\\left\\lVert\\mathcal\{T\}\_\{s\}^\{\\circ\}\(\\widehat\{E\}\)\-\\widehat\{E\}^\{\+\}\\right\\rVert\_\{F\}≤r\+ηstate\+ηalg\+ηfl≤r\+\.\\displaystyle\\leq r\+\\eta\_\{\\mathrm\{state\}\}\+\\eta\_\{\\mathrm\{alg\}\}\+\\eta\_\{\\mathrm\{fl\}\}\\leq r^\{\+\}\.Strict initialization gives the base case; induction proves the invariant for every guarded tracker update\.

## Appendix DPublished\-Method Applications

Candidates are fixed before post\-hoc certification\. Independent reference intervals supply offline conformance labels and are excluded from online timing\. Service protocols and reference construction appear in[AppendicesE](https://arxiv.org/html/2610.02268#A5)and[F](https://arxiv.org/html/2610.02268#A6)\.

### D\.1Application Details

We use pinned official implementations and certify emitted candidates post hoc without changing their update rules\. Exact source revisions, instrumentation patches, and reproduction commands are recorded in the artifact\.

##### Newton\-update removal\.

We use the official MNIST 3\-vs\-8 configuration of[Guo et al\. \(2020\)](https://arxiv.org/html/2610.02268#bib.bib2), leaving its objective perturbation, update, cumulative budget, and threshold unchanged\. Native closure encloses the source terms through the first retraining action, and direct recertification checks the same candidate at that stop\. Strict closure can move retraining earlier, while the tighter direct certificate can expose a conservative source action\.

##### CEU supported\-fidelity characterization\.

Post\-update RRV evaluates the emitted CEU head under an independently declared retraining\-reference contract\([Wu et al\., 2023](https://arxiv.org/html/2610.02268#bib.bib28)\)\. We fixedτpar=10−3\\tau\_\{\\rm par\}=10^\{\-3\}before inspecting the outputs\. The reference is the unique minimizer of retained\-node mean softmax cross\-entropy plusλ​‖θ‖22/2\\lambda\\left\\lVert\\theta\\right\\rVert\_\{2\}^\{2\}/2, giving the curvature floorμ−=λ\\mu^\{\-\}=\\lambdain[Proposition3](https://arxiv.org/html/2610.02268#Thmproposition3)\. Directed arithmetic encloses the retained\-objective gradient; verified optimization is used only for offline tightness evaluation\. The certificates cover their reference intervals and quantify the weaker fidelity supported by the snapshots alongside CEU’s native randomized guarantee\.

##### ScaleGUN gradient application\.

Native closure evaluates the same aggregate gradient quantity consumed by ScaleGUN’s propagation and optimization budget\([Yi and Wei, 2025](https://arxiv.org/html/2610.02268#bib.bib27)\)\. The candidate is unchanged during certification\.

### D\.2Newton Direct\-Perturbation Calibration

We follow the Newton direct\-perturbation mechanism of[Zou et al\. \(2025\)](https://arxiv.org/html/2610.02268#bib.bib10)in its published synthetic logistic\-ridge configuration, evaluating one\- and two\-step Newton centers over 100 leave\-one\-out states\. Native closure bounds displacement from the exact\-real Newton center, while On\-demand RRV certifies the executed center against a verified retained\-set reference\.

To separate source slack from direction\-free composition, letp∈\{32,64\}p\\in\\\{32,64\\\}denote the execution precision and define

A\\displaystyle A=‖θ¯−θR‖2rnom,\\displaystyle=\\frac\{\\left\\lVert\\bar\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{2\}\}\{r\_\{\\rm nom\}\},B⁡\(p\)\\displaystyle B\(p\)=‖θp−θ¯‖2rnom,\\displaystyle=\\frac\{\\left\\lVert\\theta\_\{p\}\-\\bar\{\\theta\}\\right\\rVert\_\{2\}\}\{r\_\{\\rm nom\}\},C⁡\(p\)\\displaystyle C\(p\)=‖θp−θR‖2rnom\.\\displaystyle=\\frac\{\\left\\lVert\\theta\_\{p\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{2\}\}\{r\_\{\\rm nom\}\}\.Directed enclosures produceA\+,B\+​\(p\),C\+​\(p\)A^\{\+\},B^\{\+\}\(p\),C^\{\+\}\(p\)for every paired state \([Table3](https://arxiv.org/html/2610.02268#A4.T3)\)\. We form each reported ratio within a state before aggregating\. For FP64,C\+​\(64\)C^\{\+\}\(64\)is near zero in some states, so we report the absolute composition–direct gap rather than an unstable ratio\. Direction\-free composition remains looser under both execution precisions on this population\.

Table 3:Detailed published\-method application results\.Newton\-perturbation bounds are normalized by the nominal radius; ScaleGUN ratios report the source budget consumed\. Newton ratios are formed per state before aggregation; FP64 uses an absolute gap because its direct bound can be near zero\.\(a\) Newton removal

\(b\) Newton direct perturbation

\(c\) ScaleGUN

9 additional checkpoints use the source fallback\.

\(d\) CEU

Declared tolerance:τpar=0\.10%\\tau\_\{\\rm par\}=0\.10\\%\.

## Appendix EService Evaluation and Controls

### E\.1Experimental Systems and Common Protocols

##### 3B safety service\.

The deployment service uses a frozen Llama\-3\.2\-3B\-Instruct backbone\([Meta AI, 2024](https://arxiv.org/html/2610.02268#bib.bib22)\)with ad=3073d=3073binary ridge head on PKU\-SafeRLHF\-QA\([Ji et al\., 2025](https://arxiv.org/html/2610.02268#bib.bib23)\)\. We replay seven 1,000\-request deletion streams under a10−310^\{\-3\}release tolerance and evaluate fixed\-readout contracts on 3,000 sealed representations\.

##### Controlled diagnostics\.

The controlled experiments use DINOv2/CIFAR\-10 and RoBERTa/AG\-News multiclass ridge heads\. The tolerance study fixes 14,000 outputs, and the stress study crosses three deletion streams, three conditioning levels, and two statistics storage precisions, giving 18 trajectories\. Independent retained\-row reconstruction supplies all offline reference labels\.

##### Verification constructions\.

The guarantee\-matched comparison holds the candidate, fixed readout, release contract, and conformance labels constant while varying only how certificate evidence is constructed\. Three held\-out streams at seven declared checkpoints give 21 matched states\. The six constructions are summarized below\.

Table 4:Verification constructions in the guarantee\-matched comparison\.aPartial inverse reuse\.

### E\.2Reference\-Transfer Soundness and Tightness

##### Tolerance–coverage frontier\.

For each of the 14,000 fixed outputs, the independent retain\-set audit computes the realized minimum toleranceτtrue\\tau\_\{\\rm true\}, while RRV computes the certified thresholdτcert\\tau\_\{\\rm cert\}\. We sweep the deployment tolerance from10−510^\{\-5\}to10−210^\{\-2\}; every output satisfiesτcert≥τtrue\\tau\_\{\\rm cert\}\\geq\\tau\_\{\\rm true\}\.

##### Stored\-equation stress comparison\.

This experiment tests whether certifying the stored equation is equivalent to certifying the exact retain\-set reference as statistics drift\. The 18 trajectories defined above evaluate the stored equation and its certificate in binary64 while varying statistics storage precision\. Independent retained\-row reconstruction labels conformance atτpar=10−3\\tau\_\{\\rm par\}=10^\{\-3\}\. Coverage and false\-release counts appear in[Table5](https://arxiv.org/html/2610.02268#A5.T5)\.

Table 5:Matched\-output conformance on nine workload configurations per precision\.Coverage is conditional on a conforming output\. The incremental row reports the first check, before any proof\-only rebuild\. Four FP32 reference intervals remain unresolved and are not counted as conforming or nonconforming\.

### E\.3Evidence Reuse and Lifecycle Cost

##### Guarantee\-matched comparison\.

The On\-demand RRV constructions form a retained\-data residual, a corrected residual, or a fresh verified factor when certification is requested\. The maintained\-factor baseline instead downdates a factor after every deletion and validates its residual at release\. The two Incremental RRV constructions share the inverse\-defect proof state and differ only in their readout certificate\. The corrected\-residual construction is the only nonstandard baseline: it computes

θcorr=θ~\+P⁡\(B~−H~​θ~\)\\theta\_\{\\rm corr\}=\\widetilde\{\\theta\}\+P\(\\widetilde\{B\}\-\\widetilde\{H\}\\widetilde\{\\theta\}\)and evaluates a retained\-data residual atθcorr\\theta\_\{\\rm corr\}\. If this residual gives‖θcorr−θR‖F≤Ccorr\\left\\lVert\\theta\_\{\\rm corr\}\-\\theta^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq C\_\{\\rm corr\}, it still certifies the original candidate through

‖Z⁡\(θ~−θR\)‖F≤‖Z⁡\(θ~−θcorr\)‖F\+‖Z‖2​Ccorr\.\\left\\lVert Z\(\\widetilde\{\\theta\}\-\\theta^\{\\mathrm\{R\}\}\)\\right\\rVert\_\{F\}\\leq\\left\\lVert Z\(\\widetilde\{\\theta\}\-\\theta\_\{\\rm corr\}\)\\right\\rVert\_\{F\}\+\\left\\lVert Z\\right\\rVert\_\{2\}C\_\{\\rm corr\}\.All terms are evaluated outward, so every construction certifies the executed snapshot rather than substitutingθcorr\\theta\_\{\\rm corr\}for release\.

Table 6:Complete guarantee\-matched results on 21 fixed states\. Latency summarizes 10 repetitions per state; stored state excludes retained rows\.
##### Decision agreement\.

Across 56 checkpoints from seven streams, margin certificates cover95\.095\.0–95\.8%95\.8\\%of declared decisions\. The independent offline audit gives99\.96%99\.96\\%mean observed agreement rather than certificate coverage\.

##### Release\-frequency accounting\.

We measure output generation, certified\-statistics maintenance, and proof\-state maintenance across all 1,000 requests in each of three streams\. Release\-check cost is the per\-stream median over the seven declared checkpoints, with 10 paired repetitions per checkpoint\. We combine these measured components at 7, 25, 50, 100, 250, 500, and 1,000 checks per 1,000 requests\. The three routes share candidate\-generation work; fresh factor pays no per\-request proof maintenance, while maintained factor and directional Incremental RRV do\. No route produces a false release on the matched states, and maintained factor requires no rebuild during the stream replays\. Linear component accounting places the directional/fresh crossover at 21\.5 checks and the maintained/fresh crossover at 214\.3 checks per 1,000 requests\.

### E\.4Precision and Representation Boundaries

##### Producer\-precision stress\.

Within each producer configuration, Incremental RRV and verified\-factor On\-demand RRV inspect the same output; changing statistics precision defines a separate candidate population\. Lifecycle totals include all online work of the selected path, while independent reference audits are excluded\. The 4,162 lower\-precision proof refreshes are triggered by a bound above tolerance, not by invalid inverse state\. The median bound moves from1\.014​τ1\.014\\taubefore a committed refresh to0\.830​τ0\.830\\tauafterward; every commit recovers certification\. All attempts together consume 4\.39% of the FP32 lifecycle and no commit changes a candidate\.[Table5](https://arxiv.org/html/2610.02268#A5.T5)reports the first check, whereas[Table7](https://arxiv.org/html/2610.02268#A5.T7)reports the final decision on the same population\. Unresolved reference intervals are excluded from the conforming denominator\.

Table 7:Producer precision and certificate construction\.Rows change the emitted candidate; within each row, columns compare the same candidates\. Coverage is conditional on conformance and uses the final post\-rebuild decision; proof\-only rebuilds do not change candidates\.
##### Contract–format compatibility frontier\.

This protocol asks whether the final representation can express an artifact that satisfies the selected contract\. We encode each format from the same master head, exhaustively evaluate the BF16 and FP16 codebooks under round\-to\-nearest\-even, and rigorously enclose the minimum feasible toleranceτmin\\tau\_\{\\min\}shown in[Figure3](https://arxiv.org/html/2610.02268#S5.F3)\(b\)\.

## Appendix FIndependent Reference Construction

### F\.1Offline Verified Reference and Evaluation Labels

Offline labels are reconstructed from retained rows, independently of the service arrays and update path\. A verified inverse\-defect certificate encloses the retraining solution, and a high\-precision dyadic reconstruction confirms all classifications\. For its solutionθt⋆\\theta\_\{t\}^\{\\star\}, directed evaluation ofrt=Bt−Ht​θt⋆r\_\{t\}=B\_\{t\}\-H\_\{t\}\\theta\_\{t\}^\{\\star\}gives

rref,t=‖rt‖Fλ,‖θt⋆−θtR‖F≤rref,t\.r\_\{\\rm ref,t\}=\\frac\{\\left\\lVert r\_\{t\}\\right\\rVert\_\{F\}\}\{\\lambda\},\\qquad\\left\\lVert\\theta\_\{t\}^\{\\star\}\-\\theta\_\{t\}^\{\\mathrm\{R\}\}\\right\\rVert\_\{F\}\\leq r\_\{\\rm ref,t\}\.
Directed norm bounds and the triangle inequalities of[Equation2](https://arxiv.org/html/2610.02268#S3.E2)then give a rigorous relative\-error interval; precision is increased until each classification is resolved\.

### F\.2Newton Direct\-Perturbation Reference Construction

To close the Newton direct\-perturbation mechanism against its exact\-real rule, letsj=θj64−θj−164s\_\{j\}=\\theta\_\{j\}^\{64\}\-\\theta\_\{j\-1\}^\{64\}denote the exact\-real difference of two stored binary64 iterates\. The verifier represents this dyadic difference as the unevaluated sum returned byTwoSum; it does not identifysjs\_\{j\}with an ordinary rounded subtraction\. This definition also handles a solver step swallowed by the state addition: the realized step is then zero\. Letg⁡\(θ\)=∇Lret​\(θ\)g\(\\theta\)=\\nabla L\_\{\\rm ret\}\(\\theta\)andH⁡\(θ\)=∇2Lret​\(θ\)H\(\\theta\)=\\nabla^\{2\}L\_\{\\rm ret\}\(\\theta\)\. On a convex region containing the exact\-real and replay iterates, and hence the segments connecting them, assumem​I⪯H⁡\(θ\)⪯M​ImI\\preceq H\(\\theta\)\\preceq MIand‖H⁡\(θ\)−H⁡\(θ′\)‖2≤L​‖θ−θ′‖2\\left\\lVert H\(\\theta\)\-H\(\\theta^\{\\prime\}\)\\right\\rVert\_\{2\}\\leq L\\left\\lVert\\theta\-\\theta^\{\\prime\}\\right\\rVert\_\{2\}\. We define the Newton\-equation residualrj=H⁡\(θj−164\)​sj\+g⁡\(θj−164\)r\_\{j\}=H\(\\theta\_\{j\-1\}^\{64\}\)s\_\{j\}\+g\(\\theta\_\{j\-1\}^\{64\}\)\. Directed MPFR evaluation applies the Hessian to both components of the exact difference and bounds‖rj‖2\\left\\lVert r\_\{j\}\\right\\rVert\_\{2\}\. We propagate

ηj\\displaystyle\\eta\_\{j\}=ηj−1\+M​ηj−1\+L​ηj−1​‖sj‖2\+‖rj‖2m,\\displaystyle=\\eta\_\{j\-1\}\+\\frac\{M\\eta\_\{j\-1\}\+L\\eta\_\{j\-1\}\\left\\lVert s\_\{j\}\\right\\rVert\_\{2\}\+\\left\\lVert r\_\{j\}\\right\\rVert\_\{2\}\}\{m\},η0\\displaystyle\\eta\_\{0\}=0\.\\displaystyle=0\.Thusηj\\eta\_\{j\}bounds the replay center’s distance from the exact\-real Newton iterate, and‖θj32−θj64‖2\+ηj\\left\\lVert\\theta\_\{j\}^\{32\}\-\\theta\_\{j\}^\{64\}\\right\\rVert\_\{2\}\+\\eta\_\{j\}closes the execution error used by the compositional Laplace interface\. This route needs no retraining reference; the direct route instead encloses the candidate against a verified retained\-set reference\.