max_modulus_constant
plain-language theorem explainer
The maximum modulus principle states that a holomorphic function on a connected open set in the complex plane attaining its maximum modulus at an interior point must be constant. Number theorists working on analytic continuations and zero-free regions for zeta-like functions cite it to close the Schur pinch argument. The proof is a term-mode wrapper that packages the given bound into an IsMaxOn predicate and invokes Mathlib's Complex.eqOn_of_isPreconnected_of_isMaxOn_norm.
Claim. Let $f : ℂ → ℂ$ be differentiable on a connected open set $U ⊆ ℂ$. If there exists $ρ ∈ U$ such that $‖f(s)‖ ≤ $‖f(ρ)‖ for all $s ∈ U$, then $f(s) = f(ρ)$ for all $s ∈ U$.
background
This theorem sits in the PickGapPersistence module, which recasts the Riemann Hypothesis as persistence of a spectral gap under the Pick operator applied to the zeta function. The module proves that a positive gap in the Euler region implies the RH, with the Schur pinch as the central step that excludes zeros when Re J ≥ 0 and the Cayley transform θ satisfies a strict bound at one point.
proof idea
The term proof first builds an IsMaxOn instance for (norm ∘ f) at ρ from the supplied universal bound. It then applies the Mathlib lemma Complex.eqOn_of_isPreconnected_of_isMaxOn_norm, passing preconnectedness (from IsConnected), openness, differentiability on U, membership of ρ, and the max condition. The final intro and simpa steps extract the pointwise equality.
why it matters
It is invoked directly by schur_pinch, which derives a contradiction from any zero inside U by showing that a pole would force the transformed function to attain the boundary value 1, violating the strict interior bound. This supports the parent result pick_gap_persistence_implies_RH. In the Recognition Science setting it supplies the analytic closure for the maximum-modulus step in the zero-exclusion argument, consistent with the removable-singularity infrastructure listed in the module's proof sketch.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.