Foundation Schur Pinch Is Herglotz

The Herglotz condition

A complex function is called Herglotz on a region when its real part is non-negative everywhere in that region. The definition is simple: for every point z in the set D, the real part of f(z) is at least 0. This positivity condition is a workhorse in analysis because it rules out many pathological behaviors and opens the door to powerful transformation tools. The name comes from the mathematician Gustav Herglotz, who studied such functions in the early twentieth century in connection with moment problems and integral representations.

The key fact about Herglotz functions is that they can be mapped to bounded functions via the Cayley transform. The transform Θ = (2H − 1)/(2H + 1) sends the right half-plane (where real parts are positive) to the unit disk (where moduli are at most 1). A result in the framework's machine-checked library proves that if f is Herglotz on D, then the composed function cayley ∘ f is Schur on D, meaning its modulus is at most 1 everywhere, provided the denominator never vanishes. This half-plane-to-disk conversion is what makes Herglotz functions tractable: bounded functions are far easier to control than unbounded ones.

In Recognition Science, the Herglotz condition appears as a structural hypothesis in a template for excluding poles. The framework's library states a pinch result: given a Herglotz function that blows up at candidate pole points and normalizes to a finite value at the right edge, the conclusion is that the function has no poles in the region. The proof strategy runs through the Cayley transform to get a Schur function, then uses the fact that Schur functions have removable singularities. This is a classical argument pattern, formalized in the library as a reusable template for later results.

The declaration IsHerglotz itself is just the definition: a predicate that a function has non-negative real part on a set. It establishes no theorem on its own. The theorems that use it, such as cayley_schur_of_herglotz and master_pinch, carry the mathematical content. The definition is a building block, not a conclusion. What the framework proves is the conditional statements: if a function is Herglotz and satisfies certain extra conditions, then certain conclusions follow.

The practical upshot is a clean division of labor. The positivity condition is checkable in many concrete settings, and once established, it gives access to the Cayley machinery automatically. The library's formalization means these implications are machine-checked, not merely asserted. For a reader, the Herglotz condition is a lens: when you can verify non-negative real part, you gain access to a suite of controlled consequences. When you cannot, the template simply does not apply.

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

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

IsHerglotz by itself proves no theorem; it is only a definition. The master_pinch theorem does not construct the absence of poles; it assumes the pole set is empty as a hypothesis. The framework does not claim that every Herglotz function arises from a physical recognition process.

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: