PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Model functions solve the constant curvature jacobi equation

Statement

For every real $k \in R$ the comparison functions ${sn}_{k}, {cs}_{k}$ of Comparison sine, cosine and cotangent functions satisfy, on all of $R$ , ${sn}_{k}^{''} + k {sn}_{k} = 0, {cs}_{k}^{''} + k {cs}_{k} = 0,$ with initial data ${sn}_{k} (0) = 0, {sn}_{k}^{'} (0) = {cs}_{k} (0) = 1, {cs}_{k}^{'} (0) = 0,$ and the Wronskian identity ${cs}_{k} (t)^{2} + k {sn}_{k} (t)^{2} = 1 for every t \in R .$ In particular, for $k > 0$ the pair $({sn}_{k}, {cs}_{k})$ is the solution of the scalar Jacobi equation with the spherical initial data, for $k = 0$ of the Euclidean initial-value problem, and for $k < 0$ of the hyperbolic initial-value problem. The identity shows that ${sn}_{k}$ and ${cs}_{k}$ never vanish simultaneously; for $k \leq 0$ , ${cs}_{k}$ is everywhere positive. The assertions are purely about the explicitly displayed model functions and use no geometric or choice hypothesis.

Facts & Assumptions

Given: A real number $k \in R$ and the piecewise formulas for ${sn}_{k}, {cs}_{k} = {sn}_{k}^{'}$ (Comparison sine, cosine and cotangent functions).

[F1]

The comparison functions are ${sn}_{k} (t) = \sin (\sqrt{k} t) / \sqrt{k}$ and ${cs}_{k} (t) = \cos (\sqrt{k} t)$ for $k > 0$ ; ${sn}_{k} (t) = t$ and ${cs}_{k} (t) = 1$ for $k = 0$ ; and ${sn}_{k} (t) = \sinh (\sqrt{- k} t) / \sqrt{- k}$ , ${cs}_{k} (t) = \cosh (\sqrt{- k} t)$ for $k < 0$ (Comparison sine, cosine and cotangent functions); ${cs}_{k} = {sn}_{k}^{'}$ is part of that definition.

[F2]

Sine and cosine are differentiable with $\sin^{'} = \cos$ , $\cos^{'} = - \sin$ , and the chain rule gives $(\sin (c t))^{'} = c \cos (c t)$ , $(\cos (c t))^{'} = - c \sin (c t)$ (The derivatives of sine and cosine are cosine and minus sine, The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ); moreover $\sin^{2} + \cos^{2} = 1$ (Parity and the Pythagorean identity for sine and cosine).

[F3]

The hyperbolic functions satisfy $\sinh^{'} = \cosh$ , $\cosh^{'} = \sinh$ and $\cosh^{2} - \sinh^{2} = 1$ (The six hyperbolic functions and their natural domains, Addition formulas, identities, parity, and derivatives of the hyperbolic functions); with the chain rule, $(\sinh (c t))^{'} = c \cosh (c t)$ and $(\cosh (c t))^{'} = c \sinh (c t)$ (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[F4]

A differentiable function with identically vanishing derivative on $R$ is constant (A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant).

Proof

1.1F1F2

The positive-curvature case. [F1, F2] Let $k > 0$ and $c : = \sqrt{k}$ . By [F1], ${sn}_{k} (t) = \sin (c t) / c$ and ${cs}_{k} (t) = \cos (c t)$ . Differentiating with [F2], ${sn}_{k}^{'} (t) = \cos (c t) = {cs}_{k} (t)$ , ${sn}_{k}^{''} (t) = - c \sin (c t) = - c^{2} {sn}_{k} (t) = - k {sn}_{k} (t)$ , and ${cs}_{k}^{'} (t) = - c \sin (c t)$ , ${cs}_{k}^{''} (t) = - c^{2} \cos (c t) = - k {cs}_{k} (t)$ . At $t = 0$ : ${sn}_{k} (0) = \sin 0 / c = 0$ , ${sn}_{k}^{'} (0) = \cos 0 = 1 = {cs}_{k} (0)$ and ${cs}_{k}^{'} (0) = - c \sin 0 = 0$ .

1.2F1

The flat case. [F1] Let $k = 0$ . By [F1], ${sn}_{0} (t) = t$ and ${cs}_{0} (t) = 1$ . Hence ${sn}_{0}^{''} = 0 = - 0 \cdot {sn}_{0}$ , ${cs}_{0}^{''} = 0 = - 0 \cdot {cs}_{0}$ , and the initial data are ${sn}_{0} (0) = 0$ , ${sn}_{0}^{'} (0) = 1 = {cs}_{0} (0)$ , ${cs}_{0}^{'} (0) = 0$ .

1.3F1F3

The negative-curvature case. [F1, F3] Let $k < 0$ and $c : = \sqrt{- k} > 0$ . By [F1], ${sn}_{k} (t) = \sinh (c t) / c$ and ${cs}_{k} (t) = \cosh (c t)$ . Differentiating with [F3], ${sn}_{k}^{'} = \cosh (c t) = {cs}_{k}$ , ${sn}_{k}^{''} = c \sinh (c t) = - k {sn}_{k}$ , and ${cs}_{k}^{''} = c^{2} \cosh (c t) = - k {cs}_{k}$ . At $t = 0$ : ${sn}_{k} (0) = 0$ , ${sn}_{k}^{'} (0) = \cosh 0 = 1$ , ${cs}_{k} (0) = 1$ and ${cs}_{k}^{'} (0) = \sinh 0 = 0$ .

2.1F1F4step 1.1step 1.2step 1.3∎

Assembly and the Wronskian identity. [F1, F4, step 1.1, step 1.2, step 1.3] Steps 1.1, 1.2 and 1.3 cover the three cases $k > 0$ , $k = 0$ and $k < 0$ , which exhaust $R$ : in every case ${sn}_{k}^{''} + k {sn}_{k} = 0$ and ${cs}_{k}^{''} + k {cs}_{k} = 0$ on all of $R$ , with ${sn}_{k} (0) = 0$ , ${cs}_{k} (0) = 1$ , ${cs}_{k}^{'} (0) = 0$ and ${cs}_{k} = {sn}_{k}^{'}$ , so ${sn}_{k}^{'} (0) = 1$ . For the remaining identity define $w (t) : = {cs}_{k} (t)^{2} + k {sn}_{k} (t)^{2}$ . By the product rule and the two differential equations just established, $w^{'} = 2 {cs}_{k} {cs}_{k}^{'} + 2 k {sn}_{k} {sn}_{k}^{'} = 2 {cs}_{k} (- k {sn}_{k}) + 2 k {sn}_{k} {cs}_{k} = 0$ on all of $R$ . Hence [F4] makes $w$ constant, and $w (0) = {cs}_{k} (0)^{2} + k {sn}_{k} (0)^{2} = 1$ . Therefore ${cs}_{k}^{2} + k {sn}_{k}^{2} = 1$ everywhere, so ${sn}_{k}$ and ${cs}_{k}$ never vanish simultaneously; the explicit case analysis shows that the same formulas continue to hold at every real $t$ , including $t = 0$ and the reflected negative times. No choice or completeness hypothesis is used.

Depends on

Used by

Diameter rigidity from toponogov under a sectional lower bound Corollary
Lower positive sectional curvature forces conjugate points Corollary
Upper sectional curvature bounds delay conjugate points Corollary
Bishop gromov ratio is constant in the model space Example
Bonnet-Myers for the round sphere Example
Cartan hadamard for hyperbolic space Example
Equality cases as diagnostics for all comparison signs Example
Model jacobi fields in positive zero and negative curvature Example
Rauch comparison between euclidean and spherical geodesics Example
Volume growth in euclidean and hyperbolic space Example
Higher sectional curvature makes jacobi fields spread faster False statement
Riccati comparison for scalar initial shape Lemma
Toponogov distance support inequality Lemma
Rigidity in bishop gromov on an interval Proposition
Rigidity in rauch comparison Proposition
Bonnet conjugate radius theorem Theorem
Bonnet myers Theorem
Hessian comparison for distance under sectional curvature bounds Theorem
Laplacian comparison for distance under a ricci lower bound Theorem
Rauch comparison theorem second form Theorem
Relative volume density comparison Theorem
Sturm comparison for scalar jacobi equations Theorem

Dependency tree · two levels

30 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Ved Datar, Lectures on Riemannian Geometry (2025) (standard reference, not scraped)
J.-H. Eschenburg, Comparison Theorems in Riemannian Geometry (standard reference, not scraped)