Foundation Schur Pinch Cayley Schur Of Herglotz

The half-plane to disk map

The declaration cayley_schur_of_herglotz proves a classical result from complex analysis. It states that if a complex function f has a non-negative real part on a set D, then the transformed function Θ = (2f − 1)/(2f + 1) has modulus at most 1 on that same set. In plain terms: a function that stays in the right half of the complex plane (where the real part is not negative) is mapped by this formula into the unit disk (where the distance from zero is at most one).

This mapping is the Cayley transform, a standard tool that connects two fundamental classes of functions. A function with non-negative real part is called Herglotz; a function with modulus at most one is called Schur. The theorem, named cayley_schur_of_herglotz, formalizes the bridge between them. Its proof in the machine-checked library of formal theorems is direct: it applies a pointwise inequality to each value of f, using the hypothesis that the denominator 2f + 1 never vanishes on D.

In Recognition Science, this result is part of a framework for excluding poles. The idea is that if a function is Herglotz, its Cayley transform is Schur, and a Schur function cannot blow up to infinity. This exclusion template, called the Schur pinch, is cited as a primary tool in the framework's approach to the Riemann Hypothesis and the P versus NP problem. The declaration itself, however, is purely analytic: it establishes the half-plane-to-disk mapping and nothing more.

The theorem does not claim that any particular function is Herglotz, nor that any specific pole is absent. It requires the user to supply both the Herglotz condition and the non-vanishing denominator. The declaration also does not prove the master pinch theorem, which bundles additional hypotheses about poles and normalization; that result is stated as a separate structure. What this declaration establishes is the clean, conditional bridge: Herglotz in, Schur out.

/-- **F4.1.3 (Herglotz-to-Schur)**: If f is Herglotz on D, then cayley ∘ f is Schur on D
    (wherever the denominator is nonzero). -/
theorem cayley_schur_of_herglotz {f : ℂ → ℂ} {D : Set ℂ}
    (hH : IsHerglotz f D) (hden : ∀ z ∈ D, 2 * f z + 1 ≠ 0) :
    IsSchur (cayley ∘ f) D := by
  intro z hz
  exact cayley_norm_le_one (f z) (hH z hz) (hden z hz)

/-- A complex function is Herglotz on a set if its real part is non-negative. -/
def IsHerglotz (f : ℂ → ℂ) (D : Set ℂ) : Prop :=
  ∀ z ∈ D, 0 ≤ (f z).re

/-- A complex function is Schur on a set if its modulus is at most 1. -/
def IsSchur (f : ℂ → ℂ) (D : Set ℂ) : Prop :=
  ∀ z ∈ D, ‖f z‖ ≤ 1

What this page does not claim

The declaration does not prove that any specific function is Herglotz or that any particular pole is absent. The declaration does not establish the master pinch theorem, which requires additional hypotheses about poles and normalization. The declaration does not connect the Cayley transform to the Riemann Hypothesis or the P versus NP problem beyond being cited as a tool.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SchurPinch.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: