master_pinch
plain-language theorem explainer
Under the F4.3.4 pinch package (Herglotz on the punctured domain, non-cancellation at candidate poles, Cayley normalization), the intended claim is that no poles sit in D. The formal theorem currently takes emptiness of poles ∩ D as an extra hypothesis and returns it unchanged, so it is an identity interface, not a derived exclusion. RH and P-vs-NP certifier work would cite the finished form. Proof is a one-line term: reuse hEmpty.
Claim. Let $f:\mathbb{C}\to\mathbb{C}$, domain $D\subseteq\mathbb{C}$, and candidate pole set $P$. Suppose the pinch hypotheses hold: $\operatorname{Re} f\ge 0$ on $D\setminus P$; $f$ blows up near every $p\in P\cap D$; and $\|\mathrm{Cayley}(f(z_0))\|<1$ for some $z_0\in D\setminus P$. If also $P\cap D=\emptyset$, then $P\cap D=\emptyset$.
background
Module F4 (Phase-Bound and Schur Pinch) sets up phase caps, Herglotz positivity, and a Cayley–Schur exclusion template aimed at RH and a P-vs-NP certifier conjecture.
Herglotz means $\operatorname{Re} f\ge 0$ on the stated set. The Cayley map $\Theta=(2H-1)/(2H+1)$ sends the right half-plane into the unit disk; the sibling cayley_schur_of_herglotz records that nonnegative real part yields a Schur function $|\Theta|\le 1$. Phase lemmas link $|\arg z|<\pi/2$ to $\operatorname{Re} z>0$.
PinchHypotheses packages three ingredients: Herglotz on $D\setminus\mathrm{poles}$; non-cancellation ($|f|\to\infty$ near each candidate pole in $D$); and normalization ($|\mathrm{cayley}(f(z_0))|<1$ at some interior regular point). The doc-comment for the structure states the intended conclusion: $f$ has no poles in $D$.
proof idea
Term-mode identity. The goal is poles ∩ D = ∅; the proof is exactly the supplied hypothesis hEmpty of the same type. The PinchHypotheses argument is bound as _H and never opened, so none of Herglotz, non-cancellation, Cayley, or Schur lemmas fire. Doc-comment sketches the intended chain (Herglotz ⇒ Schur via Cayley, Schur ⇒ removable singularity, removable + normalization ⇒ no boundary hit ⇒ no poles), but that chain is not executed here.
why it matters
Marks slot F4.3.4, the master pinch conclusion in the Foundation paper F4 template: poles empty in D under the packaged analytic hypotheses. Module doc lists RH as primary consumer and P-vs-NP certifier conjecture as secondary.
Intended logical spine is the F4 main-results ladder: phase bound ⇒ Herglotz half-plane ⇒ Cayley image Schur ⇒ pinch/removable ⇒ pole-free domain. That spine is what would feed zero-free or obstruction arguments downstream.
No used_by edges yet; the declaration is an interface placeholder whose mathematical content still needs the real exclusion proof (or a lemma such as the sketched schur_pinch_no_poles) before it constrains RH or complexity claims. Dimension constants named D elsewhere in the graph are unrelated name collisions, not inputs here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.