Zero Completion Velocity

Abstract

A simple zero thread moves by the ratio of completion and spatial derivatives.

Theorem 1.1 (The two partial derivatives determine zero motion).

$$\forall F\in \mathrm{Real}\left(\right)\to \left(\mathrm{Complex}\left(\right)\to \mathrm{Complex}\left(\right)\right),rho\in \mathrm{Real}\left(\right)\to \mathrm{Complex}\left(\right),tau\in \mathrm{Real}\left(\right),dCompletion\in \mathrm{Complex}\left(\right),dSpatial\in \mathrm{Complex}\left(\right),v\in \mathrm{Complex}\left(\right),\left(\mathrm{HasFDerivAt}\left((p\mapsto F\left(\mathrm{fst}\left(p\right)\right)\left(\mathrm{snd}\left(p\right)\right)),\mathrm{smulRight}\left(\mathrm{fstCLM}\left(\mathrm{Prod}\left(\mathrm{Real}\left(\right),\mathrm{Complex}\left(\right)\right),\mathrm{Real}\left(\right)\right),dCompletion\right)+\mathrm{comp}\left(\mathrm{mulCLM}\left(dSpatial\right),\mathrm{sndCLM}\left(\mathrm{Prod}\left(\mathrm{Real}\left(\right),\mathrm{Complex}\left(\right)\right),\mathrm{Complex}\left(\right)\right)\right),\mathrm{pair}\left(tau,rho\left(tau\right)\right)\right)\wedge \left(\mathrm{HasDerivAt}\left(rho,v,tau\right)\wedge \left(\left(\forall u\in \mathrm{Real}\left(\right),F\left(u\right)\left(rho\left(u\right)\right)=0\right)\wedge dSpatial\ne 0\right)\right)\right)\Rightarrow v=-\frac{dCompletion}{dSpatial}$$

Proof. Machine-checked in Lean as D5/S3/Analytic/Adelic/ZeroCompletionVelocity.zero_completion_velocity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The bivariate Frechet derivative is displayed on the completion and spatial coordinate projections, so dCompletion and dSpatial are the two distinct partial derivatives of the same analytic object.

The named thread rho is differentiable with velocity v and remains in the zero locus at every completion parameter. Composing the joint derivative with that thread therefore gives zero total derivative.

Since the spatial coefficient is nonzero, cancellation solves the chain rule identity for v and yields the displayed quotient.

References

• Truth anchor: D5/S3/Analytic/Adelic/ZeroCompletionVelocity.zero_completion_velocity