Tarcha 3.15 right interpolation has the required time boundaries

import Mathlib
import Definitions.Def_TarchaBraids_right_interp_config_data_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_raw_zero_endpoints_v1
import Theorems.Thm_TarchaBraids_thm_3_15_right_interp_one_fun_v1

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_right_interp_time_boundaries_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
      (∀ u : unitInterval,
        configProj n (rightOuterInterpConfig i j hji u 0) = baseUnordered n) ∧
      (∀ u : unitInterval,
        configProj n (rightOuterInterpConfig i j hji u 1) = baseUnordered n) := by sorry

end TarchaBraids