cayleyInv
plain-language theorem explainer
Inverse Cayley transform on the complex plane: maps a Schur parameter Θ to the Herglotz value (1+Θ)/(2(1-Θ)). Analysts working the F4 phase-cap / Schur-pinch template (RH and certifier pipelines) cite it as the left inverse of the forward Cayley map used in cayley_schur_of_herglotz. Pure definitional abbreviation; no proof obligations.
Claim. For $\Theta \in \mathbb{C}$, the inverse Cayley transform is defined by $\frac{1+\Theta}{2(1-\Theta)}$.
background
Module F4 (Phase-Bound and Schur Pinch Framework) develops the analytic template that turns a phase cap into Herglotz positivity and then into a Schur bound. The three headline results are: argument strictly less than $\pi/2$ forces positive real part; a Herglotz function $H$ (Re $H \ge 0$) pushes forward under the Cayley map $\Theta = (2H-1)/(2H+1)$ to a Schur function ($|\Theta| \le 1$); and Schur plus normalization plus non-cancellation excludes poles.
The forward Cayley map sends the closed right half-plane to the closed unit disk. This definition is the algebraic inverse of that map: solving $\Theta = (2H-1)/(2H+1)$ for $H$ yields exactly $(1+\Theta)/(2(1-\Theta))$. Sibling predicates IsHerglotz and IsSchur name the two sides of the correspondence; the phase lemmas phase_lt_half_pi_re_pos and phase_le_half_pi_re_nonneg supply the half-plane side.
proof idea
Definitional. The body is the closed-form rational expression $(1+\Theta)/(2(1-\Theta))$ on $\mathbb{C}$; marked noncomputable only because complex division lives in a noncomputable instance. No lemmas are applied.
why it matters
F4 is the foundation paper that packages phase caps, Herglotz positivity, and the Cayley–Schur pinch exclusion template. The module is cited primarily by the RH line and secondarily by the P vs NP certifier conjecture. The inverse is the bookkeeping dual of the forward Cayley map that appears in cayley_schur_of_herglotz (Re $H \ge 0$ on the domain implies $|\Theta| \le 1$). Without an explicit inverse, round-trip identities and normalization checks in the pinch hypotheses stay informal. No downstream consumers are wired yet in the graph; the declaration sits ready for the master pinch and pole-free lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.