AdmissibleCrossingPath.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A complete local path, including its normal-plane constraint, from the preferred normal to one having positive pairing with both crossing vectors.

lemma OAI.ClosedSurfaceR4.VelocityFrame.unit_not_negative_normalize line 13

theorem OAI.ClosedSurfaceR4.VelocityFrame.admissible_crossing_path line 22

Source documentation

The path remains in every linear hyperplane containing the original normal and the first pure vector. Thus it remains in the normal plane.

theorem admissible_crossing_path {n p q : Vec} (hn : n ⬝ᵥ n = 1)
    (hchoice : (0 < p ⬝ᵥ n ∧ 0 < q ⬝ᵥ n) ∨
      (0 < p ⬝ᵥ q ∧ ∃ m : Vec, n ⬝ᵥ m = 0 ∧ 0 < p ⬝ᵥ m ∧ 0 < q ⬝ᵥ m)) :
    ∃ γ : ℝ → Vec, ContDiffOn ℝ ∞ γ (Icc (0 : ℝ) 1) ∧ γ 0 = n ∧
      (∀ t ∈ Icc (0 : ℝ) 1,
        γ t ⬝ᵥ γ t = 1 ∧ γ t ≠ -normalize p ∧ γ t ≠ -normalize q ∧
        ∀ v : Vec, v ⬝ᵥ n = 0 → v ⬝ᵥ p = 0 → v ⬝ᵥ γ t = 0) ∧
      0 < p ⬝ᵥ γ 1 ∧ 0 < q ⬝ᵥ γ 1 := by
…

Mentions: OAI.ClosedSurfaceR4.VelocityFrame.normalize