Tarcha 3.15 right interpolation distinguished-to-outside separation

Proved

TarchaBraids.thm_3_15_adjacent_right_outside_separation_v1

by WillR · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

artin-presentationboundsbraid-groupsgeometryseparationtarcha

Each of the three distinguished strands of the right interpolation remains distinct from every outside strand throughout the interpolation square.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_outer_outside_facts_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_right_interp_re_bounds_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_right_outside_separation_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
      (∀ (u q : ℝ), 0 ≤ u → u ≤ 1 →
        ∀ (k : Fin n),
          (k : ℕ) ≠ (i : ℕ) →
          (k : ℕ) ≠ (i : ℕ) + 1 →
          (k : ℕ) ≠ (i : ℕ) + 2 →
          rightOuterInterpFun n i j u q (strandIdx i) ≠
            rightOuterInterpFun n i j u q k) ∧
      (∀ (u q : ℝ), 0 ≤ u → u ≤ 1 →
        ∀ (k : Fin n),
          (k : ℕ) ≠ (i : ℕ) →
          (k : ℕ) ≠ (i : ℕ) + 1 →
          (k : ℕ) ≠ (i : ℕ) + 2 →
          rightOuterInterpFun n i j u q (strandIdxSucc i) ≠
            rightOuterInterpFun n i j u q k) ∧
      (∀ (u q : ℝ), 0 ≤ u → u ≤ 1 →
        ∀ (k : Fin n),
          (k : ℕ) ≠ (i : ℕ) →
          (k : ℕ) ≠ (i : ℕ) + 1 →
          (k : ℕ) ≠ (i : ℕ) + 2 →
          rightOuterInterpFun n i j u q (strandIdxSucc j) ≠
            rightOuterInterpFun n i j u q k) := by sorry

end TarchaBraids

Source

Derived from the right interpolation strip bounds and the accepted outside-strand coordinate facts.

View graph