cayley
plain-language theorem explainer
Defines the scaled Cayley map sending a complex value H to (2H−1)/(2H+1). It is the half-plane-to-disk bridge used throughout the F4 Schur-pinch template: Herglotz data (Re H ≥ 0) become Schur data (|Θ| ≤ 1). Anyone citing the Herglotz-to-Schur step or the master pinch hypotheses will invoke this map. The body is a one-line noncomputable definition.
Claim. Define the (scaled) Cayley transform $\mathrm{Cayley}:\mathbb{C}\to\mathbb{C}$ by $\mathrm{Cayley}(H)=(2H-1)/(2H+1)$. It is the standard Möbius map that sends the closed right half-plane into the closed unit disk (away from the pole $H=-1/2$).
background
Module F4 builds the phase-bound and Schur-pinch exclusion template used for RH and related certifier arguments. The local vocabulary is Herglotz versus Schur: a function is Herglotz on a domain $D$ when its real part is nonnegative there, and Schur when its values stay inside the closed unit disk.
The classical Cayley transform $(z-1)/(z+1)$ sends the right half-plane to the unit disk. The audit library already defines that unscaled map and proves $|\mathrm{cayley}(z)|\le 1$ whenever $\mathrm{Re},z\ge 0$. The present definition is the same Möbius map composed with the linear stretch $z\mapsto 2H$, i.e. $\mathrm{Cayley}(H)=(2H-1)/(2H+1)$. The factor of two is a normalization convenience for the cost-side object $H$ (the shifted cost $H=J+1=\tfrac12(x+x^{-1})$ in the Recognition Composition Law), so that the pinch statements can be written directly in $H$-coordinates.
Downstream lemmas then reduce modulus bounds for this scaled map to the unscaled audit lemma by rewriting $|\mathrm{Cayley}(H)|=|\mathrm{cayley}(2H)|$.
proof idea
Pure definition: the body is the single term $(2H-1)/(2H+1)$. No tactics, no lemmas. Noncomputable only because division in $\mathbb{C}$ is noncomputable in Lean’s default setup. Callers supply a nonzero-denominator side condition when they need a well-defined value.
why it matters
This map is the geometric engine of F4.1.3. The theorem cayley_norm_le_one states that $\mathrm{Re},H\ge 0$ implies $|\mathrm{Cayley}(H)|\le 1$ (half-plane to disk). Lifting pointwise gives cayley_schur_of_herglotz: a Herglotz $f$ yields a Schur function $\mathrm{Cayley}\circ f$ wherever the denominator stays nonzero.
The master pinch package PinchHypotheses uses the same map in its normalization clause ($|\mathrm{Cayley}(f(z_0))|<1$ at a right-edge witness) and then concludes pole-freeness on $D$. That pinch is the exclusion template cited for RH and for the P vs NP certifier conjecture in the module header.
In the broader Recognition chain the object $H$ is the shifted J-cost satisfying the d’Alembert form of the Recognition Composition Law; the Cayley step converts Herglotz positivity of analytic continuations of that cost into Schur boundedness, which is what the pinch needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.