IsSchur
plain-language theorem explainer
A complex map is Schur on a set when every value has modulus at most one (closed unit disk). Complex analysts and RS foundation workers cite it as the target class after the Cayley transform of a Herglotz function in the F4 pinch template. The body is a one-line universal bound on the complex norm; no proof content.
Claim. A function $f:\mathbb{C}\to\mathbb{C}$ is Schur on a set $D\subseteq\mathbb{C}$ when $\|f(z)\|\le 1$ for every $z\in D$.
background
Module F4 (phase-bound and Schur pinch) packages the classical Herglotz–Cayley–Schur pipeline used to exclude poles and force phase caps. A function is Herglotz on $D$ when its real part is nonnegative there. The Cayley transform $\Theta=(2H-1)/(2H+1)$ sends the right half-plane into the closed unit disk, so the image class is exactly the Schur condition: values of modulus at most one.
The predicate is pure set-theoretic: no holomorphy, continuity, or normalization is built in. Those extra hypotheses appear later in the pinch lemmas (schur_pinch_no_poles, normalization and non-cancellation). Upstream imports supply the cost and Cayley infrastructure; the dimension constants $D=3$ appearing in the dependency graph are ambient RS landmarks (T8), not parameters of this definition.
proof idea
Definitional, not a proved theorem. The Prop is the single quantified inequality $\forall z\in D,;|f(z)|\le 1$. No tactics, no lemmas unfolded.
why it matters
This is the codomain class for F4.1.3: if $f$ is Herglotz on $D$ and the Cayley denominator $2f+1$ never vanishes, then the Cayley composite is Schur on $D$ (cayley_schur_of_herglotz). That theorem is the bridge from half-plane positivity to disk bounds, and it feeds the later pinch that rules out poles under normalization. The module is cited by RH arguments and by the P-vs-NP certifier conjecture, both of which need a clean Schur target after Cayley. Within Recognition Science it sits in the foundation layer that turns phase and positivity constraints into rigid analytic exclusions, alongside the eight-tick and $D=3$ forcing chain elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.