We develop a certified continuation framework for inference and training in deep equilibrium networks (DEQs), with training posed as interpolation to accuracy $2^{-b}$. For inference, input homotopy selects an equilibrium branch from a supplied start root, and a rounded tracker follows it under quantitative conditioning, derivative, boundary, and tube-radius certificates. The framework includes structured factorized certificates, sequential block elimination, inheritance of contraction guarantees in adapted coordinates, and bordered continuation through simple folds. For smooth multidimensional DEQs, including tanh networks, rational local tests can construct and validate oriented continuation charts under explicit geometric promises. For training, programmable dormant bilinear rank-one channels provide output-preserving residual-aligned repairs. Loaded Tikhonov solves diagnose insufficient parameter-to-output directions, while certified gate realization, column stability, well-posed inference, and finite-update error budgets control each pass. Under polynomially bounded certificate, encoding, precision, and backend costs, both inference and training have bit complexity $O(\mathrm{poly}(L+b))$, where $L$ is the encoded instance length; training uses $O(b+\ell)$ passes and reserve channels from an initial residual bounded by $2^\ell$. A budgeted implementation returns either certified success or inconclusive termination. The quantitative core and local certificate machinery are machine-checked in Lean 4, while numerical experiments illustrate the training mechanism.

翻译：暂无翻译