pith. machine review for the scientific record. sign in
theorem other other moderate

and

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 160theorem and an explicit log-derivative bound `M`.
 161
 162The caller supplies `M` (intended as a bound on `|g'/g|` on the disk).
 163The resulting `logDerivBound = M * r` is the angular Lipschitz constant
 164on the circle of radius `r` (chain rule). This makes `logDerivBound`
 165a known value rather than an opaque existential, enabling downstream
 166perturbation estimates. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (15)

Lean names referenced from this declaration's body.