Foundation Schur Pinch

The pinch exclusion

In complex analysis, a Herglotz function is one whose real part is never negative on a given set; a Schur function is one whose modulus never exceeds 1. The classical Cayley transform, written Θ = (2H − 1)/(2H + 1), maps the half-plane of non-negative real part onto the unit disk. The pinch is the act of applying that map to a Herglotz function and using the resulting Schur function's boundedness to rule out poles.

The framework proves three results. First, a nonzero complex number with argument strictly less than π/2 has strictly positive real part. Second, the Cayley transform of a Herglotz point has modulus at most 1. Third, the composition of the Cayley transform with a Herglotz function is Schur wherever the denominator is nonzero. These are the lemmas that make the pinch work.

The master pinch theorem bundles the hypotheses: f is Herglotz off a set of pole candidates, f blows up at each candidate (non-cancellation), and f normalizes to a finite value at the right edge. The conclusion is that the pole set is empty. The proof route is Herglotz to Schur via Cayley, Schur to removable singularity, removable plus normalization to no boundary hit, hence no poles.

In Recognition Science, this exclusion template is cited as primary support for the Riemann Hypothesis and the P vs NP certifier conjecture. The framework's machine-checked library of formal theorems records these results. The framework does not itself prove either conjecture; it supplies a reusable method for excluding poles in functions that arise in those contexts.

What the pinch changes is the shape of a proof. Instead of analyzing a function's poles directly, one transforms the problem into a boundedness question on the unit disk, where classical tools apply. That transfer is the framework's contribution.

/-- **F4.2.1**: A nonzero complex number with argument strictly less than π/2
    has strictly positive real part. -/
theorem phase_lt_half_pi_re_pos (z : ℂ) (hz : z ≠ 0) (harg : |z.arg| < π / 2) :
    0 < z.re := by
  have hpos_or_zero : 0 < z.re ∨ z = 0 :=
    (Complex.abs_arg_lt_pi_div_two_iff).1 harg
  rcases hpos_or_zero with hre | hz0
  · exact hre
  · exact (hz hz0).elim

/-- **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 Master Pinch Theorem (statement)**:
    Given:
    1. f is Herglotz on D (Re f ≥ 0)
    2. At each pole candidate p, f(z) → ∞ (non-cancellation)
    3. f normalizes to a finite value at the right edge

    Conclude: f has no poles in D.

    We state this as a structure bundling the hypotheses. -/
structure PinchHypotheses (f : ℂ → ℂ) (D : Set ℂ) (poles : Set ℂ) where
  herglotz : IsHerglotz f (D \ poles)
  non_cancellation : ∀ p ∈ poles ∩ D, ∀ ε > 0, ∃ z ∈ D, ‖f z‖ > 1/ε
  normalization : ∃ z₀ ∈ D \ poles, ‖cayley (f z₀)‖ < 1

What this page does not claim

The framework does not prove the Riemann Hypothesis or the P vs NP conjecture. The master pinch theorem as stated in the pack assumes the pole set is already empty; the full exclusion argument is not formalized here. The Cayley transform requires a nonzero denominator, a condition not always satisfied.

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: