and
plain-language theorem explainer
The theorem supplies an explicit bound on the logarithmic derivative of a holomorphic nonvanishing function g, given a disk bound M, producing the concrete angular Lipschitz constant M r on the circle of radius r. Workers on phase-lifted cost functionals and perturbation estimates in the J-action would cite it to replace opaque existentials with numerical constants. The argument is a direct chain-rule computation on the standard angular parametrization, with no additional lemmas required.
Claim. Let $g$ be holomorphic and nonvanishing in the disk of radius $r>0$ with $|g'/g|≤M$. Then the phase function $Θ$ obtained by lifting $g$ along the circle satisfies $|Θ'(θ)|≤Mr$ for all $θ$, furnishing an explicit angular Lipschitz constant.
background
The CirclePhaseLift module supplies continuous-phase infrastructure that converts holomorphic data on circles into the discrete winding constraints required by AnnularRingSample and AnnularMesh cost models. Phase is realized as a continuous lift $Θ:[0,2π]→ℝ$ whose net change encodes the winding number; sampling at 8n equispaced points yields increments compatible with the telescoping sum in the Recognition Composition Law. Upstream structures include LedgerFactorization.of (calibration of the J-cost on the positive reals) and PhiForcingDerived.of (the self-similar fixed-point forcing that fixes the functional J).
proof idea
One-line wrapper that applies the chain rule to the composition of log-derivative with the standard circle parametrization circleMap, substituting the supplied disk bound M to obtain the scaled constant M r directly.
why it matters
The result feeds the concrete Lipschitz control required by EnergyConservationDomainCert.applied, EulerLagrange.costRateEL_implies_const_one, and FunctionalConvexity.actionJ_convex_on_interp, all of which rely on phase perturbations remaining quantitatively bounded. It closes the gap between the holomorphic nonvanishing zero-charge lemma and the variational estimates in the eight-tick octave setting, supporting downstream claims that constant-1 paths are geodesics of the Hessian metric induced by J.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.