norm_theta_le_one_of_AttachmentWithMargin
plain-language theorem explainer
The attachment-with-margin predicate on a region R implies that the Cayley transform theta of the approximant J obeys the unit-disk Schur bound on R. Analysts working on the Riemann hypothesis via the Christmas-route attachment inequality cite this algebraic step to obtain the disk property directly from the gap condition. The proof is a one-line wrapper that unpacks the bundled hypothesis into its three components and invokes the component-wise Schur theorem.
Claim. If the attachment-with-margin condition holds for set $R$, functions $J$ and $J_{cert}$, and margin $m$ (that is, $0 ≤ m$, $m ≤ Re(2 J_{cert}(s))$ for all $s ∈ R$, and $‖J(s) - J_{cert}(s)‖ ≤ m/4$ for all $s ∈ R$), then $‖θ(J(s))‖ ≤ 1$ for all $s ∈ R$, where $θ(J) = (2J-1)/(2J+1)$ is the Cayley transform.
background
The module isolates the purely algebraic consequences of the attachment-with-margin inequality from Riemann-Christmas.tex (equation eq:attachment). The predicate AttachmentWithMargin(R, J, Jcert, m) is defined as the conjunction of nonnegative margin, the lower bound m ≤ Re(2 Jcert(s)) on R, and the uniform approximation error bound ‖J(s) - Jcert(s)‖ ≤ m/4 on R. This setup yields Re(2 J) ≥ 0 on R and therefore places the Cayley image inside the unit disk. The upstream theorem norm_theta_le_one_of_attachmentWithMargin proves the identical bound from the three hypotheses stated separately; the present declaration simply bundles them under the single predicate.
proof idea
The proof destructures the hypothesis h into the three conjuncts (nonnegativity of m, the margin lower bound, and the error bound) via rcases, then applies the component-wise theorem norm_theta_le_one_of_attachmentWithMargin to those three pieces.
why it matters
This wrapper supplies the algebraic closure step for the Christmas-route approach to the Riemann hypothesis, converting the attachment-with-margin gap directly into the Schur property of the Cayley transform without invoking any number theory. It sits immediately downstream of the AttachmentWithMargin definition and the component theorem, allowing the analytic effort to remain concentrated on proving the uniform approximation bound itself. The module documentation states that the analytic difficulty is entirely in establishing that bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.