theta_comp_differentiableOn
plain-language theorem explainer
If J is differentiable on S and avoids the pole of the Cayley transform, then theta composed with J remains differentiable on S. Analysts formalizing holomorphic mappings for the Riemann zeta function or Pick functions cite this auxiliary lemma. The proof is a direct term-mode verification that applies the arithmetic rules for differentiability to the explicit rational expression (2J-1)/(2J+1).
Claim. Let $J:ℂ→ℂ$ be differentiable on a set $S⊆ℂ$. If $2J(s)+1≠0$ for all $s∈S$, then the composition $s↦θ(J(s))$ is differentiable on $S$, where $θ$ is the rational Cayley transform.
background
The PickGapPersistence module treats the Riemann Hypothesis as a spectral-gap persistence question in operator theory applied to the zeta function. The Cayley transform $θ$ maps the right half-plane to the unit disk, allowing Schur-type arguments once holomorphy is secured. J_val denotes the complex extension of the Recognition Science J-cost function whose minimum lies at 1 and whose convexity follows from the upstream PhiForcingDerived structure.
proof idea
The term proof introduces a point s in S, extracts the DifferentiableWithinAt fact from the given DifferentiableOn hypothesis, records the non-vanishing denominator, and reduces the goal by applying the differentiability of constant multiplication, subtraction, addition and division to the numerator and denominator of the Cayley expression; simpa then matches the definitions of theta and cayley.
why it matters
The lemma is invoked inside schur_pinch to guarantee that θ∘J is holomorphic on the punctured domain, which closes the argument that a positive Pick gap excludes zeros. It therefore supports the main result pick_gap_persistence_implies_RH that derives the Riemann Hypothesis from gap persistence. In the broader framework the result secures the holomorphic properties required for the J-function before the eight-tick octave and D=3 spatial structure are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.