/-- **Curvature and torsion of a helix.** Let `c = √(a² + b²) > 0` and `T` be the velocity above.
Then (1) `|T| = 1`, so `s` is arc length; (2) `T' = (a/c²)·N` with `N = (-cos, -sin, 0)` a unit
vector, so the curvature is `κ = a/c²`; (3) the binormal `B = T × N` satisfies `B' = -(b/c²)·N`,
so the torsion is `τ = b/c²`. Here `θ = s/c`, and `T'`, `B'` are the derivatives computed in
`helix_tangent_deriv` and `helix_binormal_deriv`. -/
theorem helix_frenet (a b c θ : ℝ) (hc : c ^ 2 = a ^ 2 + b ^ 2) (hc0 : c ≠ 0) :
let T : ℝ × ℝ × ℝ := (-(a / c) * sin θ, (a / c) * cos θ, b / c)
let N : ℝ × ℝ × ℝ := (-cos θ, -sin θ, 0)
let B := cross T N
dot T T = 1 ∧ dot N N = 1 ∧
B = ((b / c) * sin θ, -(b / c) * cos θ, a / c) ∧
((-(a / c ^ 2)) * cos θ, (-(a / c ^ 2)) * sin θ, (0 : ℝ)) = (a / c ^ 2) • N ∧
(((b / c ^ 2)) * cos θ, (b / c ^ 2) * sin θ, (0 : ℝ)) = (-(b / c ^ 2)) • N := by
intro T N B
have hs := sin_sq_add_cos_sq θ
refine ⟨?_, ?_, ?_, ?_, ?_⟩
· simp only [T, dot]
field_simp
linear_combination (a ^ 2) * hs - hc
· simp only [N, dot]
linear_combination hs
· simp only [B, T, N, cross, Prod.mk.injEq]
refine ⟨by ring, by ring, ?_⟩
field_simp
linear_combination a * hs
· simp only [N, Prod.smul_mk, smul_eq_mul, Prod.mk.injEq]
refine ⟨by ring, by ring, by ring⟩
· simp only [N, Prod.smul_mk, smul_eq_mul, Prod.mk.injEq]
refine ⟨by ring, by ring, by ring⟩