Complex residual-band Newton invariance
Abstract
Actual derivative, center and forcing budgets imply a complex-ball self-map uniformly over a family of certified node choices.
Theorem 1.1 (complex sublevel newton ball invariant).
Lean statement: D5/S3/Quantum/Tomography/HolomorphicSublevelInvariance.complex_sublevel_newton_ball_invariant
Proof. Machine-checked in Lean as D5/S3/Quantum/Tomography/HolomorphicSublevelInvariance.complex_sublevel_newton_ball_invariant (✓ std3). ∎
Source. Repository-derived.
Commentary.
For each node use fixed C and actual derivative J. If norm(I-CJ) is at most q on the complex ball, center displacement is at most b, norm(C) is at most kappa, and b+kappa gamma+q r is at most r, then z-C(f(z)-e) stays in the same ball for all norm(e) at most gamma. No external PASS, root existence, inverse Jacobian or global cover is assumed. Exclusion and split nodes retain their set-theoretic semantics.