Tarcha 3.15 affine interpolation commutes with reflection
ProvedTarchaBraids.thm_3_15_adjacent_braidInterp_reflection_v1algebraartin-presentationbraid-groupssymmetrytarcha
Affine interpolation between two reflected complex points is the reflection of their affine interpolation.
Preamble
import Mathlib import Definitions.Def_TarchaBraids_adjacent_path_data_v1
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem thm_3_15_adjacent_braidInterp_reflection_v1 :
∀ (u : ℝ) (c z w : ℂ),
braidInterp u (c - z) (c - w) = c - braidInterp u z w := by sorry
end TarchaBraidsSource
Generic affine symmetry lemma isolated from the failed monolithic right-reflection child.