pick_gap_pos_of_re_pos
plain-language theorem explainer
If the real part of J is positive then the Pick gap at J is strictly positive. Analysts formalizing the Riemann hypothesis via operator theory on the zeta function would cite this to anchor the gap in the right half-plane. The proof unfolds the definition of pick_gap as one minus the norm of the Cayley transform theta, then applies norm-squared comparisons and linear arithmetic to show the image lies strictly inside the unit disk.
Claim. If $J$ is complex with real part strictly positive, then $1 - |Θ(J)| > 0$ where $Θ(J) = (2J-1)/(2J+1)$ is the Cayley transform of the doubled argument.
background
The Pick gap at a point J is defined as one minus the Euclidean norm of theta(J), where theta is the composition of the standard Cayley map with doubling: theta(J) = (2J-1)/(2J+1). This construction maps the right half-plane Re J > 0 into the open unit disk. The module treats the Riemann hypothesis as a persistence question for this spectral gap under the action of the zeta function and its Euler product. Upstream, the Cayley and theta definitions come from BRFPlumbing; the broader setting draws on the forcing axioms in PrimitiveDistinction and UniversalForcingSelfReference to supply the structural conditions under which the gap analysis is performed.
proof idea
The tactic proof first simplifies the definition of pick_gap. It establishes that twice J has positive real part and that 2J+1 is nonzero. A direct ring calculation then shows that the difference of the squared norms of (2J+1) and (2J-1) equals eight times Re J, which is positive. Division yields that the squared norm of theta(J) is strictly less than one. Taking square roots and applying norm nonnegativity produces the strict inequality on the norm, from which the gap positivity follows by linear arithmetic.
why it matters
This result supplies the base case for pick_gap_euler_region, which asserts a positive gap throughout the Euler product region σ > 1. It is an explicit step toward pick_gap_persistence_implies_RH, the theorem that converts gap persistence into the Riemann hypothesis. Within Recognition Science it closes the local analytic half of the spectral-gap argument that links the J-function (T5) to the eight-tick octave structure (T7) and the three-dimensional spatial embedding (T8). No open scaffolding remains inside this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.