Foundation Schur Pinch Cayley Norm Le One

The Cayley bound

The Cayley transform is a standard map on complex numbers. For a complex number H, it is defined as (2H - 1) / (2H + 1). The declaration cayley_norm_le_one states a precise bound: if the real part of H is non-negative, and the denominator is not zero, then the modulus of the transformed value is at most 1. In plain terms, the transform sends the closed right half-plane into the closed unit disk, a classical fact about this map.

This bound has a direct consequence for functions. A function is called Herglotz on a set if its real part is non-negative everywhere on that set. A function is called Schur on a set if its modulus is at most 1 everywhere there. The theorem cayley_schur_of_herglotz uses the pointwise bound to show that composing the Cayley transform with a Herglotz function yields a Schur function, wherever the denominator is non-zero. This is the half-plane-to-disk passage that the framework's library formalizes.

In Recognition Science, this passage is part of a template called the Schur pinch. The template aims to exclude poles: if a function is Herglotz, grows without bound at candidate pole points, and normalizes to a finite value at the right edge, the framework's master pinch statement concludes that the poles are empty. The library states this as a structure bundling the hypotheses, and the conclusion is that the intersection of the pole set with the domain is empty.

What the declaration does not claim is broader. It does not assert that any particular function satisfies the Herglotz condition. It does not prove that any pole set is empty on its own; the master pinch conclusion relies on the bundled hypotheses, and the library's statement of that conclusion takes the emptiness as an input. The bound is a tool, not a finished result about a specific function.

/-- **F4.1.3**: The Cayley transform of a point with Re H ≥ 0 has modulus ≤ 1.
    This is the half-plane-to-disk map. -/
theorem cayley_norm_le_one (H : ℂ) (hre : 0 ≤ H.re) (_hden : 2 * H + 1 ≠ 0) :
    ‖cayley H‖ ≤ 1 := by
  change ‖Verification.RecognitionStabilityAudit.cayley (2 * H)‖ ≤ 1
  simpa using Verification.RecognitionStabilityAudit.norm_cayley_le_one_of_re_nonneg (z := 2 * H)
    (by simpa using (mul_nonneg (by norm_num : (0 : ℝ) ≤ 2) hre))

/-- **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)

/-- **F4.3.4**: The master pinch conclusion: poles are empty in D.
    The proof uses: Herglotz ⟹ Schur (via Cayley), Schur ⟹ removable singularity,
    removable + normalization ⟹ no boundary hit ⟹ no poles. -/
theorem master_pinch {f : ℂ → ℂ} {D : Set ℂ} {poles : Set ℂ}
    (_H : PinchHypotheses f D poles)
    (hEmpty : poles ∩ D = ∅) :
    poles ∩ D = ∅ := hEmpty

What this page does not claim

The declaration does not prove that any particular function is Herglotz. The master pinch theorem does not prove that a pole set is empty without the bundled hypotheses.

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: