Sphere curve eventual tangent
ProvedBirkhoffGlobalSection.sphere_curve_eventual_tangentdifferential-geometryreal-analysis
A differentiable curve locally lying on the sphere has sphere-tangent velocity at its base point.
All displayed regularity, tangency, normalization and supplied-data hypotheses of the exact formal statement are retained.
Preamble
import Theorems.Thm_BirkhoffGlobalSection_reverse_radial_variation_bundle open BirkhoffGlobalSection Set Filter SignType open scoped ContDiff Topology set_option linter.unusedVariables false set_option autoImplicit false set_option maxHeartbeats 800000
Formal statement
theorem BirkhoffGlobalSection.sphere_curve_eventual_tangent :
∀ (q : ℝ → Phase) (v : Phase) (t : ℝ)
(hq : ∀ᶠ s in 𝓝 t, q s ∈ unitThreeSphere) (hd : HasDerivAt q v t),
q t 0 * v 0 + q t 1 * v 1 + q t 2 * v 2 + q t 3 * v 3 = 0 := by sorrySource
Independent extraction of component 10 of the Proved theorem BirkhoffGlobalSection.reverse_radial_variation_bundle. Original verified source: Solutions/Sol_BirkhoffGlobalSection_reverse_radial_variation_bundle.lean. Exact original component retained.