Foundation Schur Pinch Phase Lt Half Pi Re Pos

The phase cap

A complex number has two parts: a real part and an imaginary part, often drawn as a point on a plane. The number's argument is the angle that a line from the origin to that point makes with the positive real axis, measured in radians. The theorem phase_lt_half_pi_re_pos states a simple geometric fact: for any nonzero complex number whose argument has absolute value strictly less than π/2, the real part is strictly greater than zero. In plain terms, if the point lies strictly within the right half of the complex plane, its horizontal coordinate is positive.

This is a ledger (a discrete record of events) of a basic property, not a deep discovery. The proof in the framework's machine-checked library of formal theorems is immediate: it invokes a standard equivalence about arguments and real parts, then handles the two possible cases. The statement is a theorem, meaning it is proved from definitions and axioms, not assumed. It establishes a connection between a geometric condition (the angle bound) and an algebraic condition (the sign of the real part).

In Recognition Science, this phase cap is a building block. The framework uses it in a chain that connects functions with non-negative real parts, called Herglotz functions, to functions bounded in magnitude by one, called Schur functions, via the Cayley transform. That connection matters because it lets the framework exclude poles, points where a function blows up, in certain settings. The phase cap is the first step: it guarantees that points in the right half-plane stay in the right half-plane under the relevant maps.

The theorem does not claim anything about the imaginary part of the number, which can be positive, negative, or zero. It also does not apply to zero, since zero has no defined argument. The strict inequalities matter: if the argument equals exactly π/2, the real part can be zero, and the theorem's conclusion of strict positivity fails. The declaration is a precise, narrow result, and the framework's use of it inherits that precision.

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

What this page does not claim

The theorem says nothing about the imaginary part of the complex number. The theorem does not apply to the number zero, which has no argument. The strict inequalities are essential; equality at π/2 would not yield strict positivity.

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: