re_two_mul_nonneg_of_AttachmentWithMargin
plain-language theorem explainer
The theorem shows that the attachment-with-margin predicate on a set R of complex numbers forces Re(2J) to be nonnegative on R. Researchers working on the Riemann hypothesis via the Christmas route would cite this algebraic step to guarantee that the Cayley transform remains Schur. The proof is a one-line wrapper that unpacks the bundled predicate and invokes the quantitative core lemma.
Claim. Let $R$ be a set of complex numbers, let $J$ and $J_{cert}$ be functions from complex numbers to complex numbers, and let $m$ be a real number. Suppose $0 ≤ m$, $m ≤ Re(2 J_{cert}(s))$ for every $s ∈ R$, and $‖J(s) - J_{cert}(s)‖ ≤ m/4$ for every $s ∈ R$. Then $Re(2 J(s)) ≥ 0$ for every $s ∈ R$.
background
The module isolates purely algebraic consequences of the attachment-with-margin inequality from Riemann-Christmas.tex. The predicate AttachmentWithMargin(R, J, Jcert, m) asserts three conditions: m is nonnegative, Re(2 Jcert) is bounded below by m on R, and J stays within distance m/4 of Jcert in norm on R. This setup is designed so that the approximant J inherits nonnegativity of Re(2 Jcert) up to the margin, ensuring the Cayley transform theta(J) = (2J-1)/(2J+1) maps into the unit disk.
proof idea
The proof performs case analysis on the bundled hypothesis to extract the three components (nonnegativity of m, the margin lower bound on Re(2 Jcert), and the uniform approximation bound), then applies the quantitative lemma re_two_mul_nonneg_of_attachmentWithMargin directly to those components.
why it matters
This result supplies the algebraic closure step in the Christmas-route argument: attachment-with-margin implies the real-part nonnegativity required for the Cayley transform to be Schur. It therefore feeds the subsequent norm bound on theta. The module deliberately separates this algebraic implication from the analytic work of proving the uniform approximation bound itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.